Grcov report - thermostat_thermostat

1

// Do not edit this file as it will be overwritten if codegen is rerun

2

3

use data::*;

4

5

macro_rules! implies {

6

  ($lhs: expr, $rhs: expr) => {

7

    !$lhs || $rhs

8

};

9

10

11

macro_rules! impliesL {

12

  ($lhs: expr, $rhs: expr) => {

13

    !$lhs | $rhs

14

};

15

16

17

294

pub fn Temp_Lower_Bound() -> i32

18

294

19

294

  95i32

20

294

21

22

294

pub fn Temp_Upper_Bound() -> i32

23

294

24

294

  104i32

25

294

26

27

/** I-Assm: Integration constraint on thermostat's incoming data port current_temp

28

29

  * assume ASSM_CT_Range

30

*/

31

294

pub fn I_Assm_current_temp(current_temp: Isolette_Data_Model::Temp) -> bool

32

294

33

294

  (Temp_Lower_Bound() <= current_temp.degrees) &

34

294

    (current_temp.degrees <= Temp_Upper_Bound())

35

294

36

37

/** Initialize EntryPointContract

38

39

  * guarantee initlastCmd

40

  * @param lastCmd post-state state variable

41

*/

42

200

pub fn initialize_initlastCmd(lastCmd: Isolette_Data_Model::On_Off) -> bool

43

200

44

200

  lastCmd == Isolette_Data_Model::On_Off::Off

45

200

46

47

/** Initialize EntryPointContract

48

49

  * guarantee REQ_THERM_1

50

  *   The Heat Control command shall be Off initially.

51

  * @param api_heat_control outgoing data port

52

*/

53

200

pub fn initialize_REQ_THERM_1(api_heat_control: Isolette_Data_Model::On_Off) -> bool

54

200

55

200

  api_heat_control == Isolette_Data_Model::On_Off::Off

56

200

57

58

/** IEP-Guar: Initialize Entrypoint for thermostat

59

60

  * @param lastCmd post-state state variable

61

  * @param api_heat_control outgoing data port

62

*/

63

200

pub fn initialize_IEP_Guar(

64

200

  lastCmd: Isolette_Data_Model::On_Off,

65

200

  api_heat_control: Isolette_Data_Model::On_Off) -> bool

66

200

67

200

  initialize_initlastCmd(lastCmd) &&

68

200

  initialize_REQ_THERM_1(api_heat_control)

69

200

70

71

/** IEP-Post: Initialize Entrypoint Post-Condition

72

73

  * @param lastCmd post-state state variable

74

  * @param api_heat_control outgoing data port

75

*/

76

200

pub fn initialize_IEP_Post(

77

200

  lastCmd: Isolette_Data_Model::On_Off,

78

200

  api_heat_control: Isolette_Data_Model::On_Off) -> bool

79

200

80

200

  initialize_IEP_Guar(lastCmd, api_heat_control)

81

200

82

83

/** Compute Entrypoint Contract

84

85

  * assumes ASSM_LDT_LE_UDT

86

  * @param api_desired_temp incoming data port

87

*/

88

294

pub fn compute_spec_ASSM_LDT_LE_UDT_assume(api_desired_temp: Isolette_Data_Model::Set_Points) -> bool

89

294

90

294

  api_desired_temp.lower.degrees <= api_desired_temp.upper.degrees

91

294

92

93

/** CEP-T-Assm: Top-level assume contracts for thermostat's compute entrypoint

94

95

  * @param api_desired_temp incoming data port

96

*/

97

294

pub fn compute_CEP_T_Assm(api_desired_temp: Isolette_Data_Model::Set_Points) -> bool

98

294

99

294

  let r0: bool = compute_spec_ASSM_LDT_LE_UDT_assume(api_desired_temp);

100

294

101

294

  return r0;

102

294

103

104

/** CEP-Pre: Compute Entrypoint Pre-Condition for thermostat

105

106

  * @param In_lastCmd pre-state state variable

107

  * @param api_current_temp incoming data port

108

  * @param api_desired_temp incoming data port

109

*/

110

294

pub fn compute_CEP_Pre(

111

294

  In_lastCmd: Isolette_Data_Model::On_Off,

112

294

  api_current_temp: Isolette_Data_Model::Temp,

113

294

  api_desired_temp: Isolette_Data_Model::Set_Points) -> bool

114

294

115

294

  // I-Assm-Guard: Integration constraints for thermostat's incoming ports

116

294

  let r0: bool = I_Assm_current_temp(api_current_temp);

117

294

118

294

  // CEP-Assm: assume clauses of thermostat's compute entrypoint

119

294

  let r1: bool = compute_CEP_T_Assm(api_desired_temp);

120

294

121

294

  return r0 && r1;

122

294

123

124

/** Compute Entrypoint Contract

125

126

  * guarantee lastCmd

127

  *   Set lastCmd to value of output Cmd port

128

  * @param lastCmd post-state state variable

129

  * @param api_heat_control outgoing data port

130

*/

131

206

pub fn compute_spec_lastCmd_guarantee(

132

206

  lastCmd: Isolette_Data_Model::On_Off,

133

206

  api_heat_control: Isolette_Data_Model::On_Off) -> bool

134

206

135

206

  lastCmd == api_heat_control

136

206

137

138

/** CEP-T-Guar: Top-level guarantee contracts for thermostat's compute entrypoint

139

140

  * @param lastCmd post-state state variable

141

  * @param api_heat_control outgoing data port

142

*/

143

206

pub fn compute_CEP_T_Guar(

144

206

  lastCmd: Isolette_Data_Model::On_Off,

145

206

  api_heat_control: Isolette_Data_Model::On_Off) -> bool

146

206

147

206

  let r0: bool = compute_spec_lastCmd_guarantee(lastCmd, api_heat_control);

148

206

149

206

  return r0;

150

206

151

152

/** guarantee REQ_THERM_2

153

  *   If Current Temperature is less than

154

  *   the Lower Desired Temperature, the Heat Control shall be set to On.

155

  * @param api_current_temp incoming data port

156

  * @param api_desired_temp incoming data port

157

  * @param api_heat_control outgoing data port

158

*/

159

206

pub fn compute_case_REQ_THERM_2(

160

206

  api_current_temp: Isolette_Data_Model::Temp,

161

206

  api_desired_temp: Isolette_Data_Model::Set_Points,

162

206

  api_heat_control: Isolette_Data_Model::On_Off) -> bool

163

206

164

206

  implies!(

165

206

    api_current_temp.degrees < api_desired_temp.lower.degrees,

166

66

    api_heat_control == Isolette_Data_Model::On_Off::Onn)

167

206

168

169

/** guarantee REQ_THERM_3

170

  *   If the Current Temperature is greater than

171

  *   the Upper Desired Temperature, the Heat Control shall be set to Off.

172

  * @param api_current_temp incoming data port

173

  * @param api_desired_temp incoming data port

174

  * @param api_heat_control outgoing data port

175

*/

176

206

pub fn compute_case_REQ_THERM_3(

177

206

  api_current_temp: Isolette_Data_Model::Temp,

178

206

  api_desired_temp: Isolette_Data_Model::Set_Points,

179

206

  api_heat_control: Isolette_Data_Model::On_Off) -> bool

180

206

181

206

  implies!(

182

206

    api_current_temp.degrees > api_desired_temp.upper.degrees,

183

32

    api_heat_control == Isolette_Data_Model::On_Off::Off)

184

206

185

186

/** guarantee REQ_THERM_4

187

  *   If the Current Temperature is greater than or equal

188

  *   to the Lower Desired Temperature

189

  *   and less than or equal to the Upper Desired Temperature, the value of

190

  *   the Heat Control shall not be changed.

191

  * @param In_lastCmd pre-state state variable

192

  * @param api_current_temp incoming data port

193

  * @param api_desired_temp incoming data port

194

  * @param api_heat_control outgoing data port

195

*/

196

206

pub fn compute_case_REQ_THERM_4(

197

206

  In_lastCmd: Isolette_Data_Model::On_Off,

198

206

  api_current_temp: Isolette_Data_Model::Temp,

199

206

  api_desired_temp: Isolette_Data_Model::Set_Points,

200

206

  api_heat_control: Isolette_Data_Model::On_Off) -> bool

201

206

202

206

  implies!(

203

206

    (api_current_temp.degrees >= api_desired_temp.lower.degrees) &

204

206

      (api_current_temp.degrees <= api_desired_temp.upper.degrees),

205

108

    api_heat_control == In_lastCmd)

206

207

208

/** CEP-T-Case: Top-Level case contracts for thermostat's compute entrypoint

209

210

  * @param In_lastCmd pre-state state variable

211

  * @param api_current_temp incoming data port

212

  * @param api_desired_temp incoming data port

213

  * @param api_heat_control outgoing data port

214

*/

215

206

pub fn compute_CEP_T_Case(

216

206

  In_lastCmd: Isolette_Data_Model::On_Off,

217

206

  api_current_temp: Isolette_Data_Model::Temp,

218

206

  api_desired_temp: Isolette_Data_Model::Set_Points,

219

206

  api_heat_control: Isolette_Data_Model::On_Off) -> bool

220

206

221

206

  let r0: bool = compute_case_REQ_THERM_2(api_current_temp, api_desired_temp, api_heat_control);

222

206

  let r1: bool = compute_case_REQ_THERM_3(api_current_temp, api_desired_temp, api_heat_control);

223

206

  let r2: bool = compute_case_REQ_THERM_4(In_lastCmd, api_current_temp, api_desired_temp, api_heat_control);

224

206

225

206

  return r0 && r1 && r2;

226

206

227

228

/** CEP-Post: Compute Entrypoint Post-Condition for thermostat

229

230

  * @param In_lastCmd pre-state state variable

231

  * @param lastCmd post-state state variable

232

  * @param api_current_temp incoming data port

233

  * @param api_desired_temp incoming data port

234

  * @param api_heat_control outgoing data port

235

*/

236

206

pub fn compute_CEP_Post(

237

206

  In_lastCmd: Isolette_Data_Model::On_Off,

238

206

  lastCmd: Isolette_Data_Model::On_Off,

239

206

  api_current_temp: Isolette_Data_Model::Temp,

240

206

  api_desired_temp: Isolette_Data_Model::Set_Points,

241

206

  api_heat_control: Isolette_Data_Model::On_Off) -> bool

242

206

243

206

  // CEP-Guar: guarantee clauses of thermostat's compute entrypoint

244

206

  let r0: bool = compute_CEP_T_Guar(lastCmd, api_heat_control);

245

206

246

206

  // CEP-T-Case: case clauses of thermostat's compute entrypoint

247

206

  let r1: bool = compute_CEP_T_Case(In_lastCmd, api_current_temp, api_desired_temp, api_heat_control);

248

206

249

206

  return r0 && r1;

250

206