in dynamics.maude
   
--- directions: 0: not moving, 1: up, 2: down   


omod ELEVATOR is including RUNTIME-APG .

  ops floor doorIsOpen stopPressed direction doorState counter1 : -> IVarId [ctor] .
  ops control simulator : -> ReactorId [ctor] .
  ops call1 call2 stop reachFloor doorStatus motorUp motorDown doorCommand : -> IPortId [ctor] .
  ops motorDone checkDoor resetDirection : -> IActionId [ctor] .
  ops call1Pressed call2Pressed simStopPressed : -> TimerId [ctor] .

  op init : -> Configuration .

  eq init
   = < control : Reactor |
          inports : < call1 : Port | value : [0] >  < call2 : Port | value : [0] >
	            < stop : Port | value : [0] >   < reachFloor : Port | value : [0] >
		    < doorStatus : Port | value : [0] >,
	  outports : < motorUp : Port | value : [0] >  < motorDown : Port | value : [0] >
	             < doorCommand : Port | value : [0] >,
	  state : (floor |-> [0]) ; (doorIsOpen |-> [0]) ; (stopPressed |-> [0]) ; (direction |-> [0]) ;
	          (counter1 |-> [0]),  
	  timers : none,
	  actions : none,
	  reactions :
	    (reaction when call1 --> (motorDown ; doorCommand) do
	        { (counter1 :=  [78]) ;      --- executed
		if ((stopPressed ==/= [1])
		      &&
		      (doorIsOpen ==/= [1])
		      &&
		      (floor ==/= [1])
		      &&
		      (direction === [0]))
		  then ( (counter1 := [99]) ; (doorCommand <- [0]) ; (motorDown <- [1])) fi}) --- triggered
            (reaction when call2 --> (motorUp ; doorCommand) do
	        { if ((stopPressed ==/= [1])
		      &&
		      (doorIsOpen ==/= [1])
		      &&
		      (floor ==/= [2])
		      &&
		      (direction === [0]))
		  then ((doorCommand <- [0]) ; (motorUp <- [1])) fi})
            (reaction when stop --> doorCommand do
	        { if (stopPressed === [0]) then ((stopPressed := [1]) ; (doorCommand <- [1]))
		  else ((stopPressed := [0]) ; (doorCommand <- [0])) fi })
            (reaction when reachFloor --> doorCommand do
 	        {  (floor := reachFloor) ; (doorCommand <- [1]) })
            (reaction when doorStatus do {doorIsOpen := doorStatus})       >	

    < simulator : Reactor |
          inports : < motorUp : Port | value : [0] >  < motorDown : Port | value : [0] >
	            < doorCommand : Port | value : [0] >,
	  outports : < call1 : Port | value : [0] >  < call2 : Port | value : [0] >
	             < stop : Port | value : [0] >   < reachFloor : Port | value : [0] >
		     < doorStatus : Port | value : [0] >,
	  state : (direction |-> [0]) ; (doorState |-> [0]),
	  timers : < call1Pressed : Timer | offset : 0, period : 15 >
	           < call2Pressed : Timer | offset : 5, period : 15 >
		   < simStopPressed : Timer | offset : 10, period : 15 >,
	  actions : < motorDone : LogicalAction | minDelay : 5, 
                                                  minSpacing : 0, 
                                                  policy : defer, 
                                                  payload : [0] >
                    < checkDoor : LogicalAction | minDelay : 2, 
                                                  minSpacing : 0, 
                                                  policy : defer, 
                                                  payload : [0] >
                    < resetDirection : LogicalAction | minDelay : 0, 
                                                  minSpacing : 0, 
                                                  policy : defer, 
                                                  payload : [0] >,

	  reactions :
	     (reaction when call1Pressed --> call1 do { (call1 <- [1]) }) --- executed
	     (reaction when call2Pressed --> call2 do { call2 <- [1] })
	     (reaction when simStopPressed --> stop do { stop <- [1] })
--- (reaction when (motorUp ; motorDown) --> motorDone do {direction := [12345678]}) ----
--- (reaction when (motorDown) --> motorDone do {direction := [12345678]}) ----

(reaction when (motorUp ; motorDown) --> motorDone do
	         { if (isPresent(motorUp)
		       &&
                      (! isPresent(motorDown)))
		   then ((direction := [1]) ; (schedule(motorDone, [0], [0])))
		   else (if (isPresent(motorDown)
		             &&
			     (! isPresent(motorUp)))
			 then ((direction := [2]) ; (schedule(motorDone, [0], [0]))) fi)       
                   fi })
            (reaction when motorDone --> (reachFloor ; resetDirection) do
	        { (if (direction === [1]) then (reachFloor <- [2])
		  else  (if (direction === [2]) then (reachFloor <- [1]) fi)
		  fi)  ;
		  schedule(resetDirection, [0], [0])  })
            (reaction when resetDirection do {direction := [0]})
	    (reaction when doorCommand --> checkDoor do
	        { (doorState := doorCommand) ; (schedule(checkDoor, [0], [0])) })
            (reaction when checkDoor --> doorStatus do { doorStatus <- doorState })  	>	
		     
    (control : motorUp --> simulator : motorUp)
    (control : motorDown --> simulator : motorDown)
    (control : doorCommand --> simulator : doorCommand)
    (simulator : call1 --> control : call1)
    (simulator : call2 --> control : call2)
    (simulator : stop --> control : stop)
    (simulator : reachFloor --> control : reachFloor)
    (simulator : doorStatus --> control : doorStatus)   .

endom



red generateAPG(event(simulator, call1Pressed, [0]),  addReactionIndices(init)) .


***(   From LF repository:
-------------------
Safety Requirements
-------------------

The controller is supposed to satisfy the following safety requirements:

R1  The elevator shall move only when the door is closed and the stop switch 
    is off.
R2  [Not applicable for this implementation] The elevator shall not try to pass the end positions
    (that is, try go through the roof or the floor).
R3  [Not applicable for this implementation] A moving elevator shall halt only if the stop switch is on, or the door 
    is open, or the elevator has arrived at the destination floor.
R4  [Not applicable for this implementation] The elevator shall halt before changing direction.
R5  The signals sent to the motor shall not be contradictory.
R6  The elevator shall move when it should. 
R7  [Not a safety property] The elevator shall stay on a floor indefinitely 
    while there is no call to the other floor.
)***




--- 7  desired properties:
---    i. elevator moves only when door is closed and stop is off
---    ii. (not applicable to this aplication)
---    iii.   --"--
---    iv.   --"--
---    v. the signals sent to the motor should not be contradictory
---    vi. the elevator should move when it should (??)
---    vii. do not move unless called



omod TEST-ELEVATOR is
  including ELEVATOR .
  including DYNAMICS-WITHOUT-TICK .

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

  op initSystem : -> GlobalSystem .
  eq initSystem =
      {< env : Environment | physicalActions : none >
       addReactionIndices(init)
       < queue : EventQueue | queue : addInitialTimers(init, empty) >
       < rxns : Invoked | reactions : none >} .
endom

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

rew [100] initSystem .

omod UNBOUNDED-ELEVATOR is
  including TEST-ELEVATOR .
  including UNBOUNDED-ANALYSIS-DYNAMICS  .
endom  

search [1] initSystem =>* {none} .

*** Property 1:
--- elevator moves only when door is closed and stop is off
--- simulator's (???) direction should be diff from 0 only when its
---    doorState is closed and

--- Main property: if it is moving, the door mst be closed:
---    this guy assumes that doorState = 1 means open, and direction greater than zero means moving:
search [1] initSystem =>*
             {REST:Configuration
	      < simulator : Reactor | state : ((direction |-> [NZ:NzNat]) ; (doorState |-> [0])),
	                              AS1:AttributeSet >} .

--- this finds a bad state, also when doorState is 1 it finds a state

--- We must have misunderstood something ... now let's check the controller:
search [1] initSystem =>*
             {REST:Configuration
	      < control : Reactor |
	          state : ((direction |-> [NZ:NzNat]) ; (doorIsOpen |-> [0]) ; RS:ReactorState),
	                              AS1:AttributeSet >} .
--- this gives no solution:
---(
search [1] in UNBOUNDED-ELEVATOR : initSystem =>* {REST:Configuration
< control : Reactor |
       AS1:AttributeSet,
       state : (RS:ReactorState ; (doorIsOpen |-> [1]) ; direction |-> [NZ:NzNat]) >}  .

No solution.
states: 53  rewrites: 7060 in 25ms cpu (25ms real) (281847 rewrites/second)
)---

search [1] initSystem =>*
             {REST:Configuration
	      < control : Reactor |
	          state : ((direction |-> [NZ:NzNat]) ; RS:ReactorState),
	                              AS1:AttributeSet >} .

*** NOTICE: we look at the LF code, and the control's 'direction' variable is never changed!!!

*** Final attempt:
search [1] initSystem =>*
             {REST:Configuration
	      < simulator : Reactor | state : ((direction |-> [NZ:NzNat]) ; RS1:ReactorState),
	                              AS1:AttributeSet >
	      < control : Reactor | AS2:AttributeSet,
                                    state : (RS2:ReactorState ; (doorIsOpen |-> [1])) >} .

*** No solution.  Good!!

--- Final sanity check: the thing can move when doors are closed:
search [1] initSystem =>*
             {REST:Configuration
	      < simulator : Reactor | state : ((direction |-> [NZ:NzNat]) ; RS1:ReactorState),
	                              AS1:AttributeSet >
	      < control : Reactor | AS2:AttributeSet,
                                    state : (RS2:ReactorState ; (doorIsOpen |-> [0])) >} .

--- Good! finds state!

*** Conclusion: their model is wrong/strange. Their analysis takes forever, whereas
***   ours only encounters 53 states and model checks in short time.

*** What we SHOULD do is:
---  a. add nondeterministic physical actions modeling the user, so that all the interesting
---        properties can be model checked in temporal logic
--- b. maybe add analysis for the 'flow' stuff.      DONE, in general ...
--- However, the example and (erroneous) LF code is so confusing so
--- it is probably better to move on.

--- All commands in less than 39ms


***(   In the LF benchmarks repository, the property is written as follows:

spec="G[0, 15 sec]((Elevator_s_reaction_3 && (Elevator_s_direction != 0)) 
                   ==> (Elevator_s_doorStatus == 0 && Elevator_c_StopPressed == 0))",
CT=15, expect=true

)***

--- The spec is a mess, but we can obviously analyze this property in three ways:
---   1. Directly with bounded behaviors up to 15 in Maude itself, since
---      apart from the initial G[0,15] there are no other timed temporal operators.
---   2. Do the whole thing using Real-Time Maude's timed CTL model checker.
---   3. Prove in Maude the stronger property [] (...)
---      which of course implies G[0,15] (...)
--- Obviously, case 3 is very strong and more general than 1 and 2.

--- NOTE!  In the above LF requirement spec, we do not know what && really means.
--- What is its semantics???   Because it combines a state properties with flow properties,
---  and talk about the same state (there are no temporal operators in the formula)
--- do they refer to the state variable values after or before Elevator_s_reaction_3
--- is executed???    We have sent an email to Edward asking for clariifcation.

--- We can of course do LTL model checking, but here search is enough, since this is a state property:
--- Search for a BAD state where the state prop does not hold:

search [1] initSystem =>*
             {REST:Configuration
	      < simulator : Reactor | state : ((direction |-> [NZ:NzNat]) ; (doorState |-> [N2:Nat])),
	                              AS1:AttributeSet >
	      < control : Reactor | AS2:AttributeSet,
                                    state : (RS2:ReactorState ; (stopPressed |-> [N3:Nat])) >
	      < rxns : Invoked | reactions : (simulator . 4) ; RIDS:ReactionIdSet >}
         such that N2:Nat =/= 0   or   N3:Nat =/= 0  .	      

***(    Result:
search [1] in UNBOUNDED-ELEVATOR : initSystem =>* {REST:Configuration
< control : Reactor |
       AS2:AttributeSet,
       state : (RS2:ReactorState ; stopPressed |-> [N3:Nat]) >
< simulator : Reactor |
       AS1:AttributeSet,
       state : ((direction |-> [NZ:NzNat]) ; doorState |-> [N2:Nat]) >
< rxns : Invoked |
       reactions : (RIDS:ReactionIdSet ; (simulator . 4)) >}  such that N2:Nat =/= 0 or N3:Nat =/= 0 = true .

Solution 1 (state 5)
states: 6  rewrites: 1389 in 3ms cpu (4ms real) (353885 rewrites/second)
REST:Configuration --> < env : Environment |
       physicalActions : none >
< queue : EventQueue |
       queue : ((event(simulator, resetDirection, [0]) at tag(0, 1)) :: (event(simulator, checkDoor, [0]) at tag(2, 0))
    :: ((event(simulator, motorDone, [0]) event(simulator, simStopPressed, [0])) at tag(5, 0)) :: (event(simulator,
    call1Pressed, [0]) at tag(10, 0)) :: event(simulator, call2Pressed, [0]) at tag(15, 0)) >
...
NZ:NzNat --> 1
N2:Nat --> 1
RIDS:ReactionIdSet --> (control . 2) ; (control . 4) ; (simulator . 2) ; (simulator . 5) ; (simulator . 7)
Maude> 
)***


--- We found an unexpected counterexample.  show path 5 gives us the whole path leading to the bad state.
--- Our model checking is based on our current understand of the seamntics of LF property spec language,
--- so that could explain the undesired result.  Or, the spec, which seems a little bit messy, could
--- have a flaw ...