in dynamics.maude

in TrainDoor_v1.maude

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

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

  op initSystem : -> GlobalSystem .
  eq initSystem =
     { < env : Environment |
           physicalActions : < (controller . external) : PhysAct |
	                           leftOfPeriod : 0,
				   period : 5,
				   possibleValues : ([true] : [false]),
				   timeNonDet : true > >
       addReactionIndices(init)
       < queue : EventQueue | queue : addStartup(startup,init, empty) >
       < rxns : Invoked | reactions : none >} .
                              
     
endom


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


red initSystem .

rew [33] initSystem .

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

rew [33] initSystem .

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



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


rew initSystem in time 0 .


--- time-bounded reachability
search initSystem in time 0 =>*
             {REST:Configuration
	      < train : Reactor | state : (moving |-> [true]) ; RS1:ReactorState,
	                          ATTS1:AttributeSet >
	      < door : Reactor | state : (locked |-> [false]) ; RS2:ReactorState,
	                          ATTS2:AttributeSet >} in time T:Time .

***(  Result:

search in TIME-BOUNDED-TRAIN : initSystem in time 0 =>* {REST:Configuration
< train : Reactor |
       ATTS1:AttributeSet,
       state : (RS1:ReactorState ; moving |-> [true]) >
< door : Reactor |
       ATTS2:AttributeSet,
       state : (RS2:ReactorState ; locked |-> [false]) >}  in time T:Time .

No solution.
states: 87  rewrites: 4499 in 24ms cpu (27ms real) (180429 rewrites/second)
Maude> 
)***

