first draft of the train-intruder imitator model

pta2maude/tests/examples/train-intruder-intrpr.imi

+
+var
+  xtrain, xintruder, xgate : clock;
+  pfar, papproaching, pverynear, pwalkingsensor, pwalkinghouse, pwaiting, plowering, pemergencywaiting, pemergencylowering : parameter;
+  choice, gatedown, sensoractive, start : discrete;
+
+(************************************************************)
+ automaton train
+(************************************************************)
+synclabs : sensorfar, sensorclose, pass, noaction;
+
+loc inittrain : invariant True
+  when start = 1 sync noaction goto far ;
+
+loc far : invariant xtrain <= pfar
+  when xtrain < pfar & sensoractive = 0 sync noaction do { xtrain := 0 } goto approaching ;
+  when xtrain < pfar & sensoractive = 1 sync sensorfar do { xtrain := 0} goto approaching ;
+
+loc approaching : invariant xtrain <= papproaching - pverynear
+  when xtrain = papproaching - pverynear sync sensorclose goto verynear ;
+
+loc verynear : invariant xtrain <= papproaching
+  when xtrain = papproaching & gatedown = 0 sync pass do {xtrain := 0} goto gone ;
+  when xtrain = papproaching & gatedown = 1 sync pass do {xtrain := 0} goto crash ;
+
+loc gone : invariant xtrain <= 0
+
+loc crash : invariant xtrain <= 0
+
+end (* train *)
+
+
+(************************************************************)
+ automaton intruder
+(************************************************************)
+synclabs : choosehouse, choosesensor, breaksensor, powercut;
+
+loc choosing : invariant True
+  when choice = 0 sync choosesensor do { start := 1 } goto walkingsensor ;
+  when choice = 1 sync choosehouse do { start := 1 } goto walkinghouse ;
+
+loc walkingsensor : invariant xintruder <= pwalkingsensor
+  when xintruder = pwalkingsensor sync breaksensor do { xintruder := 0, sensoractive := 0} goto intruderdone ;
+
+loc walkinghouse : xintruder <= pwalkinghouse
+  when xintruder = pwalkinghouse sync powercut do { xintruder := 0, sensoractive := 0} goto intruderdone ;
+
+loc intruderdone : invariant True
+
+end (* intruder *)
+
+(************************************************************)
+ automaton gate
+(************************************************************)
+synclabs : noaction, pass, sensorclose, powercut, sensorfar, startlowering, endlowering ;
+
+
+loc initgate : invariant True
+  when start = 1 sync noaction goto up ;
+
+loc up : invariant True
+  when True sync pass do {xgate:=0} goto up ;
+  when True sync sensorclose do {xgate:=0} goto emergencylowering ;
+  when True sync powercut do {xgate:=0} goto nopower ;
+  when True sync sensorfar do {xgate:=0} goto waiting ;
+
+loc waiting : invariant xgate <= plowering
+  when True sync powercut do {xgate:=0} goto nopower ;
+  when True sync sensorclose do {xgate:=0} goto emergencylowering ;
+  when True sync pass do {xgate:=0} goto up ;
+  when xgate = pwaiting sync startlowering do {xgate:=0} goto lowering ;
+
+loc lowering : invariant xgate <= plowering
+  when True sync powercut goto lowering;
+  when True sync sensorclose goto lowering;
+  when True sync pass do {xgate:=0} goto up;
+  when xgate=plowering sync endlowering do {xgate:=0, gatedown:=1} goto down;
+
+loc down : invariant True
+  when True sync powercut goto down ;
+  when True sync sensorclose goto down ;
+  when True sync pass do {xgate:=0} goto up ;
+
+loc nopower : invariant xgate <= pemergencywaiting
+  when True sync sensorfar do {xgate:=0} goto nopower ;
+  when True sync pass do {xgate:=0} goto nopower ;
+  when True sync sensorclose do {xgate:=0} goto emergencylowering ;
+  when xgate = pemergencywaiting sync startlowering do {xgate:=0} goto emergencylowering ;
+
+loc emergencylowering : invariant xgate <= pemergencylowering
+  when True sync powercut goto emergencylowering ;
+  when True sync sensorclose goto emergencylowering ;
+  when True sync pass do {xgate:=0} goto up ;
+  when xgate = pemergencylowering sync endlowering do {xgate:=0, gatedown:=1} goto down ;
+
+end (* gate *)
+
+
+(************************************************************)
+(* Initial state *)
+(************************************************************)
+
+init :=
+	(*------------------------------------------------------------*)
+	(* Initial location *)
+	(*------------------------------------------------------------*)
+	& loc[train] = inittrain
+	& loc[intruder] = choosing
+	& loc[gate] = initgate
+;
+
+(************************************************************)
+(* the end *)
+(************************************************************)
+end