
omod ALARM is 
  including LF-REPR .
  protecting LF-VALUE-TIME .
  protecting RUNTIME-APG .

  ops fault : -> RVarId [ctor] .
  ops controller : -> ReactorId [ctor] .
  ops out out2 : -> RPortId [ctor] .
  ops startup turnOff : -> RActionId [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} > .
endom

omod TEST-ALARM is
  including ALARM .
  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 >} .
endom

omod SIMULATE-ALARM is
  including TEST-ALARM .
  including SIMULATION-DYNAMICS .
endom  

rew initSystem .

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

omod CHECK-ALARM is
  including TEST-ALARM .
  including UNBOUNDED-ANALYSIS-DYNAMICS .
endom  

search initSystem =>* {none} .

***( 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 .

should be done in rtm!
)***

