in dynamics

(tomod THERMOSTAT is 
  including RUNTIME-APG .

  ops mode heat temp : -> IVarId [ctor] .
  ops environment thermostat : -> ReactorId [ctor] .
  ops heatOn temperature : -> IPortId [ctor] .
  ops startup changeMode : -> IActionId [ctor] .
  op t : -> TimerId [ctor] .
  op init : -> Configuration .

  eq init
   = < environment : Reactor |
      inports : < heatOn : Port | value : [0] >,
	  outports : < temperature : Port | value : [0] >,
	  state : (heat |-> [0]) ; (temp |-> [0]),
	  timers : < t : Timer | offset : 1, period : 10 >,
	  actions : < startup : LogicalAction | minDelay : 0, 
                                            minSpacing : 0, 
                                            policy : defer, 
                                            payload : [0] >,
	  reactions :
	    (reaction when startup do { temp := [19] })
	    (reaction when t --> temperature do {
	        (if (heat === [0]) then (temp := temp - [1])
	        else (temp := temp + [1]) fi) ;
	        (temperature <- temp)
	     }) 
         reaction when heatOn do { heat := heatOn } 
     >
     
     < thermostat : Reactor |
      inports : < temperature : Port | value : [0] >,
	  outports : < heatOn : Port | value : [0] >,
	  state : mode |-> [0],
	  timers : none,
	  actions : < changeMode : LogicalAction | minDelay : 0, 
                                            minSpacing : 0, 
                                            policy : defer, 
                                            payload : [0] >
                < startup : LogicalAction | minDelay : 0, 
                                            minSpacing : 0, 
                                            policy : defer, 
                                            payload : [0] >,
	  reactions :
	    (reaction when startup do { mode := [0] })
	    (reaction when temperature --> heatOn ; changeMode do {
	        *** something is wrong in the LF code, tried to fix here, hope I got the idea correctly!!!
	        if (mode === [0]) then if (temperature <= [18]) then ((heatOn <- [1]) ; schedule(changeMode,[0],[0])) fi
	        else if (temperature >= [22]) then ((heatOn <- [0]) ; schedule(changeMode,[0],[0])) fi fi
	     }) 
         reaction when changeMode do { if (mode === [0]) then mode := [1] else mode := [0] fi } 
     > 
     
     (environment : temperature --> thermostat : temperature)
     thermostat : heatOn --> environment : heatOn .
endtom)

(tomod TEST-THERMOSTAT is
  including THERMOSTAT .
  including DYNAMICS-WITHOUT-TICK .

  ops env queue rxns : -> Oid [ctor] .

  op initSystem : -> GlobalSystem .
  eq initSystem =
      {< env : Environment | physicalActions : none >
       addReactionIndices(init)
       < queue : EventQueue | queue : addStartup(startup, init, empty) >
       < rxns : Invoked | reactions : none >} .
endtom)

(tomod SIMULATE-THERMOSTAT is
  including TEST-THERMOSTAT .
  including SIMULATION-DYNAMICS .
endtom)

(rew initSystem .)

(search initSystem =>! GS:GlobalSystem .)    --- obvious trivial result

(tomod CHECK-THERMOSTAT is
  including TEST-THERMOSTAT .
  including UNBOUNDED-ANALYSIS-DYNAMICS .
endtom)

(search initSystem =>* {none} .)


(tomod TCTL-CHECK-THERMOSTAT is
   including TEST-THERMOSTAT .
   including TCTL-MODEL-CHECKER  .

   ops modeChanged : -> Prop [ctor] .

   var REST : Configuration .  
   vars N N0 N1 : Nat . 
   var T : Time .
   var O O1 : Oid .
   

   op modeIs_ : Nat -> Prop [ctor] .
   eq {REST  < thermostat : Reactor | state : (mode |-> [ N0 ]) >
              } in time T
              |= modeIs N = N0 == N .

   eq {REST  < thermostat : Reactor | state : (mode |-> [ N0 ]) >
              }
              |= modeIs N = N0 == N .





op lessThan_ : Nat -> Prop [ctor] .
eq {REST 
    < thermostat : Reactor | inports : < temperature : Port | value : [N1] > >
  } in time T
   |= lessThan N = (N1 <= N) .

eq {REST 
    < thermostat : Reactor | inports : < temperature : Port | value : [N1] > >
  }
   |= lessThan N = (N1 <= N) .


op greaterThan_ : Nat -> Prop [ctor] .
eq {REST 
    < thermostat : Reactor | inports : < temperature : Port | value : [N1] > >
  } in time T
   |= greaterThan N = (N1 >= N) .

eq {REST 
    < thermostat : Reactor | inports : < temperature : Port | value : [N1] > >
  }
   |= greaterThan N = (N1 >= N) .

endtom)


***( the main property in the LF repository is

spec="G[0, 20 sec](((Thermostat_t_temperature <= 18) ==> F[0](Thermostat_t__mode == 1))  &&  ((Thermostat_t_temperature >= 22) ==> F[0](Thermostat_t__mode == 0)))", expect=true

should be done in rtm!
)***

(mc-tctl initSystem |= AG[<= than 20] ((lessThan 18 ) implies (AF[<= than 0] (modeIs 1 ))) .)

***(Introduced timed module: TCTL-CHECK-THERMOSTAT

rewrites: 18577 in 28ms cpu (29ms real) (642869 rewrites/second)
Check
mc-tctl_|=_. initSystem |= AG[<= than 20] (lessThan 18 implies AF[<= than 0] modeIs 1) .
in TCTL-CHECK-THERMOSTAT with mode deterministic time increase


Checking equivalent property:
mc-tctl_|=_. initSystem |= not (E tt U[c 0,20 c] lessThan 18 and (E not modeIs 1 U[o 0,INF o] tt)) .

Property satisfied
)***


(mc-tctl initSystem |= AG[<= than 20] ((greaterThan 22 ) implies (AF[<= than 0] (modeIs 0 ))) .)

***(
rewrites: 18350 in 7ms cpu (8ms real) (2302095 rewrites/second)

Check
mc-tctl_|=_. initSystem |= AG[<= than 20] (greaterThan 22 implies AF[<= than 0] modeIs 0) .
in TCTL-CHECK-THERMOSTAT with mode deterministic time increase


Checking equivalent property:
mc-tctl_|=_. initSystem |= not (E tt U[c 0,20 c] greaterThan 22 and (E not modeIs 0 U[o 0,INF o] tt)) .

Property satisfied
)***
