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

2

pub fn Temp_Lower_Bound() -> i32

18

2

19

2

  95i32

20

2

21

22

2

pub fn Temp_Upper_Bound() -> i32

23

2

24

2

  104i32

25

2

26

27

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

28

29

  * assume ASSM_CT_Range

30

*/

31

2

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

32

2

33

2

  (Temp_Lower_Bound() <= current_temp.degrees) &

34

2

    (current_temp.degrees <= Temp_Upper_Bound())

35

2

36

37

/** Initialize EntryPointContract

38

39

  * guarantee initlastCmd

40

  * @param lastCmd post-state state variable

41

*/

42

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

43

44

  lastCmd == Isolette_Data_Model::On_Off::Off

45

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

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

54

55

  api_heat_control == Isolette_Data_Model::On_Off::Off

56

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

pub fn initialize_IEP_Guar(

64

  lastCmd: Isolette_Data_Model::On_Off,

65

  api_heat_control: Isolette_Data_Model::On_Off) -> bool

66

67

  initialize_initlastCmd(lastCmd) &&

68

  initialize_REQ_THERM_1(api_heat_control)

69

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

pub fn initialize_IEP_Post(

77

  lastCmd: Isolette_Data_Model::On_Off,

78

  api_heat_control: Isolette_Data_Model::On_Off) -> bool

79

80

  initialize_IEP_Guar(lastCmd, api_heat_control)

81

82

83

/** Compute Entrypoint Contract

84

85

  * assumes ASSM_LDT_LE_UDT

86

  * @param api_desired_temp incoming data port

87

*/

88

2

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

89

2

90

2

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

91

2

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

2

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

98

2

99

2

  let r0: bool = compute_spec_ASSM_LDT_LE_UDT_assume(api_desired_temp);

100

2

101

2

  return r0;

102

2

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

2

pub fn compute_CEP_Pre(

111

2

  In_lastCmd: Isolette_Data_Model::On_Off,

112

2

  api_current_temp: Isolette_Data_Model::Temp,

113

2

  api_desired_temp: Isolette_Data_Model::Set_Points) -> bool

114

2

115

2

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

116

2

  let r0: bool = I_Assm_current_temp(api_current_temp);

117

2

118

2

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

119

2

  let r1: bool = compute_CEP_T_Assm(api_desired_temp);

120

2

121

2

  return r0 && r1;

122

2

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

2

pub fn compute_spec_lastCmd_guarantee(

132

2

  lastCmd: Isolette_Data_Model::On_Off,

133

2

  api_heat_control: Isolette_Data_Model::On_Off) -> bool

134

2

135

2

  lastCmd == api_heat_control

136

2

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

2

pub fn compute_CEP_T_Guar(

144

2

  lastCmd: Isolette_Data_Model::On_Off,

145

2

  api_heat_control: Isolette_Data_Model::On_Off) -> bool

146

2

147

2

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

148

2

149

2

  return r0;

150

2

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

2

pub fn compute_case_REQ_THERM_2(

160

2

  api_current_temp: Isolette_Data_Model::Temp,

161

2

  api_desired_temp: Isolette_Data_Model::Set_Points,

162

2

  api_heat_control: Isolette_Data_Model::On_Off) -> bool

163

2

164

2

  implies!(

165

2

    api_current_temp.degrees < api_desired_temp.lower.degrees,

166

    api_heat_control == Isolette_Data_Model::On_Off::Onn)

167

2

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

2

pub fn compute_case_REQ_THERM_3(

177

2

  api_current_temp: Isolette_Data_Model::Temp,

178

2

  api_desired_temp: Isolette_Data_Model::Set_Points,

179

2

  api_heat_control: Isolette_Data_Model::On_Off) -> bool

180

2

181

2

  implies!(

182

2

    api_current_temp.degrees > api_desired_temp.upper.degrees,

183

    api_heat_control == Isolette_Data_Model::On_Off::Off)

184

2

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

2

pub fn compute_case_REQ_THERM_4(

197

2

  In_lastCmd: Isolette_Data_Model::On_Off,

198

2

  api_current_temp: Isolette_Data_Model::Temp,

199

2

  api_desired_temp: Isolette_Data_Model::Set_Points,

200

2

  api_heat_control: Isolette_Data_Model::On_Off) -> bool

201

2

202

2

  implies!(

203

2

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

204

2

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

205

2

    api_heat_control == In_lastCmd)

206

2

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

2

pub fn compute_CEP_T_Case(

216

2

  In_lastCmd: Isolette_Data_Model::On_Off,

217

2

  api_current_temp: Isolette_Data_Model::Temp,

218

2

  api_desired_temp: Isolette_Data_Model::Set_Points,

219

2

  api_heat_control: Isolette_Data_Model::On_Off) -> bool

220

2

221

2

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

222

2

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

223

2

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

224

2

225

2

  return r0 && r1 && r2;

226

2

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

2

pub fn compute_CEP_Post(

237

2

  In_lastCmd: Isolette_Data_Model::On_Off,

238

2

  lastCmd: Isolette_Data_Model::On_Off,

239

2

  api_current_temp: Isolette_Data_Model::Temp,

240

2

  api_desired_temp: Isolette_Data_Model::Set_Points,

241

2

  api_heat_control: Isolette_Data_Model::On_Off) -> bool

242

2

243

2

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

244

2

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

245

2

246

2

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

247

2

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

248

2

249

2

  return r0 && r1;

250

2