*** This is a model of the second train door example given on Figure 5 in
*** the Verification of Cyberphysical Systems paper.


omod TRAINDOOR-V2 is 
  including LF-REPR .
  protecting LF-VALUE-TIME .
 
  ops moving locked : -> BVarId [ctor] .
  ops controller train door : -> ReactorId [ctor] .
  ops move lock unlock stop : -> BPortId [ctor] .
  ops startup external : -> BActionId .
  op init : -> Configuration .
  
  eq init = 
     < controller : Reactor | 
       inports : none,
       outports : < lock : Port | value : [false] > 
                  < move : Port | value : [false] >
 		 < unlock : Port | value : [false] > 
                  < stop : Port | value : [false] >, 
       state : empty,
       timers : none,
       actions : < startup : LogicalAction | minDelay : 0, 
                                minSpacing : 0, 
                                policy : defer, 
                                payload : [0] >
                 < external : PhysicalAction | 
                                minDelay : 0, 
                                minSpacing : 0, 
                                policy : defer, 
                                payload : [false] >,
       reactions : 
         (reaction when startup do { skip })
         reaction when external --> lock ; unlock ; move ; stop do
 	{ if external then (lock <- [true] ) ; (move <- [true])
 	  else (unlock <- [true]) ; (stop <- [true]) fi}  
     >
 --- the startup stuff does not really do anything ...
 
 
     < train : Reactor | 
         inports : < move : Port | value : [false] >
 	          < stop : Port | value : [false] >,
         outports : none,
         state : (moving |-> [false]), 
         timers : none,
         actions : none,
         reactions : (reaction when move do { moving := [true] })
 		    reaction when stop do {  moving := [false] } 
     >
     
     < door : Reactor | 
         inports : < lock : Port | value : [false] >
 	          < unlock : Port | value : [false] >,
         outports : none,
         state : (locked |-> [false]),
         timers : none,
         actions : none,
         reactions : (reaction when lock do { locked := [true] })
 		    reaction when unlock do { locked := [false] } 
     >
 
     (controller : lock --> door : lock)
     (controller : unlock -- 100 --> door : unlock)
     (controller : move -- 100 --> train : move)
     (controller : stop --> train : stop) .
    
endom
