-
Notifications
You must be signed in to change notification settings - Fork 1
/
TempSensorPeriodic_p_tcproc_tempSensor.scala
65 lines (54 loc) · 2.03 KB
/
TempSensorPeriodic_p_tcproc_tempSensor.scala
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
// #Sireum #Logika
package tc.TempSensor
import org.sireum._
import tc._
// This file will not be overwritten so is safe to edit
object TempSensorPeriodic_p_tcproc_tempSensor {
def initialise(api: TempSensorPeriodic_p_Initialization_Api): Unit = {
Contract(
Modifies(api),
Ensures(
// BEGIN INITIALIZES ENSURES
// guarantee initializes
api.currentTemp.degrees == 72.0f
// END INITIALIZES ENSURES
)
)
api.put_currentTemp(Temperature_i(72.0f))
}
def timeTriggered(api: TempSensorPeriodic_p_Operational_Api): Unit = {
Contract(
Modifies(api)
)
// read temperature from HARDWARE temperature sensor,
// via interface realized via Slang Extension "TempSensorNative"
var temp = TempSensorDevice.currentTempGet()
// set the out data port currentTemp to hold the read temperature
// BUG - unauthorized mod of temperature data
// val adjDegrees = temp.degrees + 13.0f // adjust temperature upward
// temp = Temperature_i(adjDegrees)
api.put_currentTemp(temp)
}
def activate(api: TempSensorPeriodic_p_Operational_Api): Unit = { }
def deactivate(api: TempSensorPeriodic_p_Operational_Api): Unit = { }
def finalise(api: TempSensorPeriodic_p_Operational_Api): Unit = { }
def recover(api: TempSensorPeriodic_p_Operational_Api): Unit = { }
}
//=================================================
//
// Slang extension used to interface with non-Slang
// code to retreive a temperature value.
//
// In this case, the extension is abstracting a call
// to underlying communication/hardware infrastructure
// to retrieve a sensor value.
//
// Early in development we may choose to simulate the
// sensor. Later we may construct a extension implementation that
// reads from actual hardware.
//=================================================
@ext("TempSensorDevice_Ext_Sim") object TempSensorDevice {
def currentTempGet(): Temperature_i = Contract.Only(
Ensures(Res[Temperature_i].degrees >= -50.0f & Res[Temperature_i].degrees <= 150.0f)
)
}