--- Very simple thermostat specified and analyzed in Real-Time Maude. --- This is supposed to be an example of a HYBRID system. load real-time-maude.maude *** start Real-Time Maude --- Keep temp between 62 and 74 degrees: (tmod THERMOSTAT is protecting POSRAT-TIME-DOMAIN . *** Dense time domain sort ThermoState . ops on off : -> ThermoState [ctor] . op _`,_ : ThermoState PosRat -> System [ctor] . rl [turn-on] : off , 62 => on , 62 . rl [turn-off] : on , 74 => off , 74 . vars R R' : Time . crl [tick-on] : {on, R} => {on, R + (2 * R')} in time R' if R' <= ((74 - R) / 2) [nonexec] . crl [tick-off] : {off, R} => {off, R - R'} in time R' if R' <= (R - 62) [nonexec] . endtm) *** Dense time domain *** Nondeterministic tick rule ... we must define a strategy for *** advancing time to execute the system. We choose to always *** increase time by 1/2: (set tick def 1/2 .) *** We should never be able to reach a very cold or very hot temperature: *** (tsearch [1] {on, 70} =>* {T:ThermoState, X:PosRat} such that X:PosRat < 62 or X:PosRat > 74 in time <= 100 .) *** We should reach the very pleasant temperature 65 many times: *** (tsearch {on, 70} =>* {T:ThermoState, 65} in time <= 100 .) *** Since the system is finitestate without the clocks and *** with the current strategy for advancing time, we *** can use untimked search to check properties without time *** bounds. In particular, the following search ensures that we never *** reach a unacceptable temperature: *** (utsearch {on, 70} =>* {T:ThermoState, X:PosRat} such that X:PosRat < 62 or X:PosRat > 74 .) *** Use of temporal logic model checking to prove that we will always *** be a non-bad state. The following module defines the proposition *** 'badState' which holds in all states where the temperature is either *** too warm or too cold: (tmod CHECK-THERMOSTAT is including TIMED-MODEL-CHECKER . protecting THERMOSTAT . op badState : -> Prop . eq {T:ThermoState, TEMP:PosRat} |= badState = (TEMP:PosRat < 62) or (TEMP:PosRat > 74) . endtm) *** First we check whether the temperature is always pleasant within *** time 100 at least: *** (mc {on, 70} |=t [] ~ badState in time < 100 .) *** A untimed model checking command ensures that the temperature is *** always pleasant, at least wrt to the chosen time advance strategy: *** (mc {on, 70} |=u [] ~ badState .) *** Finally, we illustrate the use of tick mode. We set the tick mode *** to advance time by four: (set tick def 4 .) *** Even so, the total time elapse may not always be a multiple of 4 *** since the maximal time elapse is used when this is less than 4: *** (trew {on, 70} in time < 10 .)