in TrainDoor_v3.maude

omod TEST-TRAIN is
  including TRAINDOOR-V3 .
  including DYNAMICS-WITHOUT-TICK .

  ops env queue rxns : -> Oid [ctor] .

  op initSystem : -> GlobalSystem .
  eq initSystem =
     { < env : Environment |
           physicalActions : < (controller . external) : PhysAct |
	                           leftOfPeriod : 0,
				   period : 10, --- 10 is correct
				   possibleValues : ([true] : [false]),
				   timeNonDet : false >
                             < (door . extOpen) : PhysAct |
	                           leftOfPeriod : 0,
				   period : 11,   --- should be 11, user can block if 2 
 				   possibleValues : ([true]),
				   timeNonDet : true >    ---- should be true
       >
       addReactionIndices(init)
       < queue : EventQueue | queue : empty >
       < rxns : Invoked | reactions : none >} .
endom


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



rew [10] initSystem .



---(
search [1] initSystem =>*
             {REST:Configuration
	      < door : Reactor | state : (locked |-> [true]) ; RS2:ReactorState,
	                          ATTS2:AttributeSet >} in time T:Time .
)--- finds a good state



omod UNCLOCKED-TRAIN is
  including TEST-TRAIN .
  including UNBOUNDED-ANALYSIS-DYNAMICS  .
endom  

---(
rew [33] initSystem .
)---

---(
search [1] initSystem =>*
             {REST:Configuration
	      < door : Reactor | state : (locked |-> [true]) ; RS2:ReactorState, ATTS2:AttributeSet >} .
)---

--- New for EMSOFT paper around deadline:
---(
search [1] initSystem =>*
             {REST:Configuration
	      < door : Reactor | state : (locked |-> [true]) ; (isOpen |-> [true]) ; RS2:ReactorState, ATTS2:AttributeSet >} .
)---


---( New, for EMSOFT deadline; time-bounded analysis is pointless
      here, but we do it anyways, just to illustrate
      that it is possible, and we use a mixed property:
      can reaction 2 of door have been
      invoked and yet the door is unlocked?

omod TIME-BOUNDED-TRAIN is including TEST-TRAIN .
including TIME-BOUNDED-DYNAMICS .
 eq timeBound = 150 .
endom 

search [1] initSystem in time 0 =>*
             {REST:Configuration
	      < door : Reactor | state : (locked |-> [false]) ; RS:ReactorState, ATTS:AttributeSet >
< rxns : Invoked | reactions : (door . 2) ; R:ReactionIdSet >
} in time T:Time .

--- oops finds such a state
)---




omod MODEL-CHECK-TRAIN3 is
  including MODEL-CHECKER .
  including UNCLOCKED-TRAIN .
  including LF-PROP .
endom


--- red modelCheck(initSystem, <> (locked in door is [true])) .

--- red modelCheck(initSystem, <> (locked in door is [true])) .
--- gives counterexample, as Marjan said it would.
--- however, it seems to be the trivial counterxample,
--- where the external button, to start the train, is never pushed.

--- What we need is to say that if an event is inf often in the queue,
--- then the door should eventually be opened

--- If the external event that starts the train is
--- infinitely often in the queue, then it must be guaranteed
--- that the door is locked:

red modelCheck(initSystem,
               (((~ event(controller, external, [false]) inQueue) W
	       (locked in door == [true]))
	       /\ ([] <> (event(controller, external, [true]) inQueue)))
	       ->  <> (locked in door == [true])) .


eof


--- Holds when period of extOpen is 11 and external is NOT timeNonDet.
--- Does not hold when external is timeNonDet.

--- What about if period of extOpen is 2, then ...

--- Note that the simpler property will not hold even with good
--- parameters, since we may have many false external events:
red modelCheck(initSystem,
                ([] <> (event(controller, external, [true]) inQueue))
	       ->  <> (locked in door == [true])) .



---  EMSOFT DEADLINE STUFF:
red modelCheck(initSystem, <> (locked in door == [false] /\ (door . 2) invoked)) .

--- returns counterexample
red modelCheck(initSystem, ~ <> (locked in door == [false] /\ (door . 2) invoked)) .

--- Now I change extOpen nondet to false, and model check.
--- Remember to reset this value back.
red modelCheck(initSystem, <> [] (locked in door == [false])) .
