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


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

 ops counter1 counter2 counter3 : -> 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 : < close : Port | value : [false] >
                 < lock : Port | value : [false] >
                 < unlock : Port | value : [false] >
                 < open : Port | value : [false] >, 
      state : (counter3 |-> [0]),
      timers : none,
      actions :  < external : PhysicalAction | 
                               minDelay : 0, 
                               minSpacing : 0, 
                               policy : defer, 
                               payload : [false] >,
      reactions : 
        reaction when external --> close ; lock ; open ; unlock do
	{ if external then skip
	  else ((open <- [true]) ; counter3 := counter3 + [1]) fi }
    >
--- the startup stuff does not really do anything ...

    
    < door : Reactor | 
        inports : 
		  < open : Port | value : [false] >,
        outports : none,
        state : (locked |-> [false])  ; (isOpen |-> [false]) ; (counter1 |-> [0]) ; (counter2 |-> [0]),
        timers : none,
        actions : < extOpen : PhysicalAction | 
                               minDelay : 0, 
                               minSpacing : 0, 
                               policy : defer, 
                               payload : [false] >,
        reactions : 
                    
                    (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   ;  (counter2 := counter2 + [1])}) 

   >

  
  
    (controller : open -- 7 --> door : open) .
  
   
endom
