in dynamics

(tomod ALARM is 
  including RUNTIME-APG .

  ops fault : -> IVarId [ctor] .
  ops controller : -> ReactorId [ctor] .
  ops out out2 : -> IPortId [ctor] .
  ops startup turnOff : -> IActionId [ctor] .
  op init : -> Configuration .

  eq init
   = < controller : Reactor |
      inports : none,
	  outports : < out : Port | value : [0] >
	             < out2 : Port | value : [0] >,
	  state : (fault |-> [0]),
	  timers : none,
	  actions : < turnOff : LogicalAction | minDelay : 1, 
                                                minSpacing : 0, 
                                                policy : defer, 
                                                payload : [0] >
                                                    
                < startup : LogicalAction | minDelay : 0, 
                                                minSpacing : 0, 
                                                policy : defer, 
                                                payload : [0] >,
	  reactions :
	    (reaction when startup --> out ; out2 ; turnOff do { (fault := [1] ); (if fault === [1] then (schedule(turnOff, [0], [0]); (out <- [5]) ; (out2 <- [10])) fi)}) 
         reaction when turnOff do {if (turnOff === [1]) then fault := [0] fi} > .
endtom)

(tomod TEST-ALARM is
  including ALARM .
  including DYNAMICS-WITHOUT-TICK .
  including SIMULATION-DYNAMICS .

  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)

(red initSystem .)
***(
(rew initSystem .)

)***

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

  search in TEST-ALARM : initSystem =>! GS:GlobalSystem .

  No solution.

  rewrites: 61705 in 20ms cpu (21ms real) (2947315 rewrites/second)

***)

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

  op reaction_invoked : ReactionId -> Prop [ctor] .

  var REST : Configuration .
  var RID : ReactionId .
  var RIDS : ReactionIdSet .
  var T : Time .
  var O : Oid .

  eq {REST
      < O : Invoked | reactions : (RID ; RIDS) >}
     |=  reaction RID invoked = true .

  eq {REST}
     |=  reaction RID invoked = false [owise] .

  eq {REST
      < O : Invoked | reactions : (RID ; RIDS) >}  in time T
     |=  reaction RID invoked = true .

  eq {REST}  in time T
     |=  reaction RID invoked = false [owise] .

endtom)

***(
(search initSystem =>* {none} .)

  search in TCTL-CHECK-ALARM : initSystem =>* {none} .

  No solution.

  rewrites: 27006 in 24ms cpu (25ms real) (1085406 rewrites/second)

***)

(mc-tctl initSystem |= AG[<= than 1] ((reaction (controller . 1) invoked) implies (AF[<= than 1] (reaction (controller . 2) invoked))) .)
***(
Introduced timed module: TCTL-CHECK-ALARM

rewrites: 27055 in 29ms cpu (30ms real) (906183 rewrites/second)

Check
mc-tctl_|=_. initSystem |= AG[<= than 1] (reaction controller . 1 invoked implies AF[<= than 1] reaction controller . 2 invoked) .
in TCTL-CHECK-ALARM with mode deterministic time increase


Checking equivalent property:
mc-tctl_|=_. initSystem |= not (E tt U[c 0,1 c] reaction controller . 1 invoked and (E not reaction controller . 2 invoked U[o 1,INF o] tt)) .

Property satisfied

***)

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

spec="G[0, 1 sec]((Alarm_c_reaction_0) ==> F(0, 1 sec](Alarm_c_reaction_1)))", expect=true .

)***

