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


omod TRAINDOOR-V3 is 
  including LF-REPR .
  protecting LF-VALUE-TIME .

  op counter1 : -> RVarId [ctor] .
  ops isOpen locked : -> BVarId [ctor] .
  ops controller train door : -> ReactorId [ctor] .
  ops close lock unlock open : -> BPortId [ctor] .
  ops startup external extOpen : -> BActionId .
  op init : -> Configuration .
  
  eq init = 
     < controller : Reactor | 
       inports : none,
       outports : < lock : Port | value : [false] > 
                  < open : Port | value : [false] >
 		 < unlock : Port | value : [false] > 
                  < close : Port | value : [false] >, 
       state : empty,
       timers : none,
       actions : < startup : LogicalAction | minDelay : 0, 
                                minSpacing : 0, 
                                policy : defer, 
                                payload : [false] >
                 < external : PhysicalAction | 
                                minDelay : 0, 
                                minSpacing : 0, 
                                policy : defer, 
                                payload : [false] >,
       reactions : 
         (reaction when startup do { skip })
         reaction when external --> close ; lock ; open ; unlock do
 	{ if external then (close <- [true] ) ; (lock <- [true]) 
 	  else (open <- [true]) ; (unlock <- [true]) fi }
     >
 --- the startup stuff does not really do anything ...
 
     
     < door : Reactor | 
         inports : < lock : Port | value : [false] >
 	          < unlock : Port | value : [false] >
 		  < open : Port | value : [false] >
 	          < close : Port | value : [false] >,
         outports : none,
         state : (locked |-> [false])  ; (isOpen |-> [false]) ; (counter1 |-> [0]),
         timers : none,
         actions : < extOpen : PhysicalAction | 
                                minDelay : 0, 
                                minSpacing : 0, 
                                policy : defer, 
                                payload : [false] >,
         reactions : (reaction when close do {isOpen := [false]})
                     (reaction when lock do
 		       { if isOpen === [false] then locked := [true] fi })
                     (reaction when unlock do { locked := [false] }) 
                     (reaction when (extOpen ; open) do                     *** new!
 		       { if locked === [false] then isOpen := [true] fi  ;  (counter1 := counter1 + [1]) }) 
              ---     (reaction when extOpen do
 	---	       { if locked === [false] then isOpen := [true] fi   ;  (counter1 := counter1 + [1])}) 
 
    >
 
     (controller : lock -- 5 --> door : lock)
     (controller : unlock -- 4 --> door : unlock)
     (controller : open -- 7 --> door : open)
     (controller : close -- 3 --> door : close) .
    
endom
