
omod TRAINDOOR is 
  including LF-REPR .
  protecting LF-VALUE-TIME .
  
  ops received : -> RVarId [ctor] .
  ops controller train door : -> ReactorId [ctor] .
  ops in out1 out2 : -> RPortId [ctor] .
  ops startup : -> RActionId .
  op init : -> Configuration .
  
  eq init = 
     < controller : Reactor | 
       inports : none,
       outports : < out1 : Port | value : [0] > 
                  < out2 : Port | value : [0] >, 
       state : empty,
       timers : none,
       actions : < startup : LogicalAction | minDelay : 0, 
                                minSpacing : 0, 
                                policy : defer, 
                                payload : [0] >,
       reactions : 
         reaction when startup --> out1 ; out2 do { (out1 <- [1] ) ; (out2 <- [2])}   
     >

    < train : Reactor | 
         inports : < in : Port | value : [0] >,
         outports : none,
         state : (received |-> [0]), 
         timers : none,
         actions : none,
         reactions : reaction when in do { received := in }       
     >
     
     < door : Reactor | 
         inports : < in : Port | value : [0] >,
         outports : none,
         state : (received |-> [0]),
         timers : none,
         actions : none,
         reactions : reaction when in do { received := in }       
     >
 
     (controller : out1 -- 1 --> train : in)
     controller : out2 -- 1 --> door : in .
endom

omod TEST-TRAINDOOR is
  including TRAINDOOR .
  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 CHECK-TRAINDOOR is
  including TEST-TRAINDOOR .
  including UNBOUNDED-ANALYSIS-DYNAMICS .
endom  

rew [5] initSystem .

omod TIME-BOUNDED-TRAINDOOR is
  including TEST-TRAINDOOR .
  including TIME-BOUNDED-DYNAMICS .
  eq timeBound = 1 .
endom 


omod MODEL-CHECK-TRAINDOOR is
  including MODEL-CHECKER .
  including TIME-BOUNDED-TRAINDOOR .
  including LF-PROP .
endom


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

spec="(!TrainDoor_t_reaction_0)U[0, 1 sec](TrainDoor_d_reaction_0)", expect=false

)***

red modelCheck(initSystem, ~ ((train . 1) invoked) U ((door . 1) invoked)) .


***( Result:
reduce in MODEL-CHECK-TRAINDOOR : modelCheck(initSystem, ~ reaction train . 1 invoked U reaction door . 1 invoked) .
rewrites: 120 in 0ms cpu (0ms real) (~ rewrites/second)
result ModelCheckResult: counterexample({{< controller : Reactor | inports : none, outports : (< out1 : Port | value : [0] > < out2 : Port | value : [0] >), state : empty, reactions :
    reaction 1 when startup --> out1 ; out2 do{(out1 <- [1]) ; out2 <- [2]}, timers : none, actions : < startup : LogicalAction | minDelay : 0, minSpacing : 0, policy : defer, payload
    : [0] > > < train : Reactor | inports : < in : Port | value : [0] >, outports : none, state : received |-> [0], reactions : reaction 1 when in --> none do{received := in}, timers
    : none, actions : none > < door : Reactor | inports : < in : Port | value : [0] >, outports : none, state : received |-> [0], reactions : reaction 1 when in --> none do{received
    := in}, timers : none, actions : none > < env : Environment | physicalActions : none > < queue : EventQueue | queue : event(controller, startup, [0], [true]) at tag(0, 1) > < rxns
    : Invoked | reactions : (none).ReactionIdSet > (controller : out1 -- 1 --> train : in) controller : out2 -- 1 --> door : in} ,'step}, {{< controller : Reactor | inports : none,
    outports : (< out1 : Port | value : [1] > < out2 : Port | value : [2] >), state : empty, reactions : reaction 1 when startup --> out1 ; out2 do{(out1 <- [1]) ; out2 <- [2]},
    timers : none, actions : < startup : LogicalAction | minDelay : 0, minSpacing : 0, policy : defer, payload : [0] > > < train : Reactor | inports : < in : Port | value : [0] >,
    outports : none, state : received |-> [0], reactions : reaction 1 when in --> none do{received := in}, timers : none, actions : none > < door : Reactor | inports : < in : Port |
    value : [0] >, outports : none, state : received |-> [0], reactions : reaction 1 when in --> none do{received := in}, timers : none, actions : none > < env : Environment |
    physicalActions : none > < queue : EventQueue | queue : (event(train, in, [1], [true]) event(door, in, [2], [true])) at tag(1, 0) > < rxns : Invoked | reactions : (controller . 1)
    > (controller : out1 -- 1 --> train : in) controller : out2 -- 1 --> door : in} ,deadlock})
)***
