in dynamics.maude


omod AIRCRAFT-DOOR is including RUNTIME-APG .

  ops ramp doorOpen : -> IVarId [ctor] .
  ops controller vision door : -> ReactorId [ctor] .
  ops in out : -> IPortId [ctor] .
  op startup : -> IActionId [ctor] .

  op init : -> Configuration .

  eq init
   = < controller : Reactor |
          inports : none,
	  outports : < out : Port | value : [0] >,
	  state : empty,
	  timers : none,
	  actions : < startup : LogicalAction | minDelay : 0, 
                                                minSpacing : 0, 
                                                policy : defer, 
                                                payload : [0] >,
	  reactions :
	    (reaction when startup --> out do {out <- [1]}) >

    < vision : Reactor |
          inports : < in : Port | value : [0] >,
	  outports : < out : Port | value : [0] >,
	  state : ramp |-> [0],
	  timers : none,
	  actions : none,
	  reactions : reaction when in --> out do {if (ramp === [1]) then out <- [0] else out <- [1] fi} > 

    < door : Reactor |
          inports : < in : Port | value : [0] >,
	  outports : none,
	  state : doorOpen |-> [0],
	  timers : none,
	  actions : none,
	  reactions : reaction when in do {doorOpen := in} > 

    (controller : out --> vision : in)
    (vision : out --> door : in) .
endom

--- red generateAPG(event(controller, startup, [0]),  addReactionIndices(init)) .


--- desired property: (vision.ramp == 0) => (G[0sec] door-reaction-invoked => doorOpen == 1) .
--- whem ramp is 0, the door reaction should be invoced and the doorOpen should be 1.

omod TEST-AIRCRAFT-DOOR is
  including AIRCRAFT-DOOR .
  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 SIMULATE-AIRCRAFT-DOOR is
  including TEST-AIRCRAFT-DOOR .
  including SIMULATION-DYNAMICS .
endom  

rew initSystem .

search initSystem =>! GS:GlobalSystem .    --- obvious trivial result

*** Not covered by us:
--- 1. a property denoting that an action has been performed.
---     can be solved by TLR model checking
--- 2. timed temporal logic properties

omod CHECK-AIRCRAFT-DOOR is
  including TEST-AIRCRAFT-DOOR .
  including UNBOUNDED-ANALYSIS-DYNAMICS .
endom  

search initSystem =>* {none} .

***( NOTICE: Even though it may not really be necessary, the main property
     in the LF repository is

spec="((AircraftDoor_vision_ramp == 0) ==> (G[0 sec](AircraftDoor_door_reaction_0 ==> (AircraftDoor_door_doorOpen == 1))))"

We could easily solve this by having time bound 0, and run a standard safety check.
However, we have done the corresponding timed CTL model checking using Real-Time Maude,
please see file rtm-aircraft-door.maude  in the corresponding directory.

)***

