Update library to v2.1 release

imitator-model-checker · Nov 13, 2023 · 4f542fb · 4f542fb
1 parent 6d90ad1
commit 4f542fb
Show file tree

Hide file tree

Showing 129 changed files with 1,419 additions and 372 deletions.
diff --git a/benchmarks/ATM/fig1_DCLXZL18-fixed.imi b/benchmarks/ATM/fig1_DCLXZL18-fixed.imi
@@ -38,7 +38,7 @@ var
 (************************************************************)
   automaton pta
 (************************************************************)
-synclabs: ;
+actions: ;
 
 loc Idle: invariant True
 	when True do {x := 0 , y := 0 , z := 0} goto Start;

diff --git a/benchmarks/BRP/BRPAAPP21/BRPAAPP21_GFSinRC.imi b/benchmarks/BRP/BRPAAPP21/BRPAAPP21_GFSinRC.imi
@@ -57,7 +57,7 @@ var
 automaton monitor
 (************************************************************)
 
-synclabs: S_in, sndD;
+actions: S_in, sndD;
 
 loc s0: invariant True
     	when True sync sndD goto s0;
@@ -72,7 +72,7 @@ end (* monitor *)
 (****************************************************)
 automaton sender
 (****************************************************)
-synclabs: S_in, rcvA, sndD, S_DK, S_NOK, S_OK;
+actions: S_in, rcvA, sndD, S_DK, S_NOK, S_OK;
 
 loc idleS: invariant x>=0
 	when True sync S_in do {b1:=True,x:=0} goto next_frame;
@@ -100,7 +100,7 @@ end (* sender *)
 (****************************************************)
 automaton receiver
 (****************************************************)
-synclabs: rcvD, sndA, R_NOK, R_OK, R_FST, R_INC;
+actions: rcvD, sndA, R_NOK, R_OK, R_FST, R_INC;
 
 loc new_file: invariant True
 	when True sync rcvD do {z:=0} goto fst_safe;
@@ -132,7 +132,7 @@ end (* receiver *)
 (****************************************************)
 automaton channelK
 (****************************************************)
-synclabs: sndD, rcvD, lostK;
+actions: sndD, rcvD, lostK;
 
 loc startK: invariant u>=0
 	when True sync sndD do {u:=0} goto in_transitK;
@@ -149,7 +149,7 @@ end (* channelK *)
 (****************************************************)
 automaton channelL
 (****************************************************)
-synclabs: sndA, rcvA, lostL;
+actions: sndA, rcvA, lostL;
 
 loc startL: invariant v>=0
 	when True sync sndA do {v:=0} goto in_transitL;

diff --git a/benchmarks/BRP/BRPAAPP21/BRPAAPP21_GSinFSdk.imi b/benchmarks/BRP/BRPAAPP21/BRPAAPP21_GSinFSdk.imi
@@ -58,7 +58,7 @@ AUTOMATA
 automaton monitor
 (************************************************************)
 
-synclabs: S_in, S_OK, S_NOK, S_DK, sndD;
+actions: S_in, S_OK, S_NOK, S_DK, sndD;
 
 loc s0: invariant True
     	when True sync sndD goto s0;
@@ -77,7 +77,7 @@ end (* monitor *)
 (****************************************************)
 automaton sender
 (****************************************************)
-synclabs: S_in, rcvA, sndD, S_DK, S_NOK, S_OK;
+actions: S_in, rcvA, sndD, S_DK, S_NOK, S_OK;
 
 loc idleS: invariant x>=0
 	when True sync S_in do {b1:=True,x:=0} goto next_frame;
@@ -105,7 +105,7 @@ end (* sender *)
 (****************************************************)
 automaton receiver
 (****************************************************)
-synclabs: rcvD, sndA, R_NOK, R_OK, R_FST, R_INC;
+actions: rcvD, sndA, R_NOK, R_OK, R_FST, R_INC;
 
 loc new_file: invariant True
 	when True sync rcvD do {z:=0} goto fst_safe;
@@ -137,7 +137,7 @@ end (* receiver *)
 (****************************************************)
 automaton channelK
 (****************************************************)
-synclabs: sndD, rcvD, lostK;
+actions: sndD, rcvD, lostK;
 
 loc startK: invariant u>=0
 	when True sync sndD do {u:=0} goto in_transitK;
@@ -154,7 +154,7 @@ end (* channelK *)
 (****************************************************)
 automaton channelL
 (****************************************************)
-synclabs: sndA, rcvA, lostL;
+actions: sndA, rcvA, lostL;
 
 loc startL: invariant v>=0
 	when True sync sndA do {v:=0} goto in_transitL;

diff --git a/benchmarks/BRP/BRPAAPP21/BRPAAPP21_GSinFSnok.imi b/benchmarks/BRP/BRPAAPP21/BRPAAPP21_GSinFSnok.imi
@@ -58,7 +58,7 @@ AUTOMATA
 automaton monitor
 (************************************************************)
 
-synclabs: S_in, S_OK, S_NOK, sndD;
+actions: S_in, S_OK, S_NOK, sndD;
 
 loc s0: invariant True
     	when True sync sndD goto s0;
@@ -77,7 +77,7 @@ end (* monitor *)
 (****************************************************)
 automaton sender
 (****************************************************)
-synclabs: S_in, rcvA, sndD, S_DK, S_NOK, S_OK;
+actions: S_in, rcvA, sndD, S_DK, S_NOK, S_OK;
 
 loc idleS: invariant x>=0
 	when True sync S_in do {b1:=True,x:=0} goto next_frame;
@@ -105,7 +105,7 @@ end (* sender *)
 (****************************************************)
 automaton receiver
 (****************************************************)
-synclabs: rcvD, sndA, R_NOK, R_OK, R_FST, R_INC;
+actions: rcvD, sndA, R_NOK, R_OK, R_FST, R_INC;
 
 loc new_file: invariant True
 	when True sync rcvD do {z:=0} goto fst_safe;
@@ -137,7 +137,7 @@ end (* receiver *)
 (****************************************************)
 automaton channelK
 (****************************************************)
-synclabs: sndD, rcvD, lostK;
+actions: sndD, rcvD, lostK;
 
 loc startK: invariant u>=0
 	when True sync sndD do {u:=0} goto in_transitK;
@@ -154,7 +154,7 @@ end (* channelK *)
 (****************************************************)
 automaton channelL
 (****************************************************)
-synclabs: sndA, rcvA, lostL;
+actions: sndA, rcvA, lostL;
 
 loc startL: invariant v>=0
 	when True sync sndA do {v:=0} goto in_transitL;

diff --git a/benchmarks/BRP/BRPAAPP21/BRPAAPP21_RC.imi b/benchmarks/BRP/BRPAAPP21/BRPAAPP21_RC.imi
@@ -57,7 +57,7 @@ AUTOMATA
 (****************************************************)
 automaton sender
 (****************************************************)
-synclabs: S_in, rcvA, sndD, S_DK, S_NOK, S_OK;
+actions: S_in, rcvA, sndD, S_DK, S_NOK, S_OK;
 
 loc idleS: invariant x>=0
 	when True sync S_in do {b1:=True,x:=0} goto next_frame;
@@ -85,7 +85,7 @@ end (* sender *)
 (****************************************************)
 automaton receiver
 (****************************************************)
-synclabs: rcvD, sndA, R_NOK, R_OK, R_FST, R_INC;
+actions: rcvD, sndA, R_NOK, R_OK, R_FST, R_INC;
 
 loc new_file: invariant True
 	when True sync rcvD do {z:=0} goto fst_safe;
@@ -121,7 +121,7 @@ end (* receiver *)
 (****************************************************)
 automaton channelK
 (****************************************************)
-synclabs: sndD, rcvD, lostK;
+actions: sndD, rcvD, lostK;
 
 loc startK: invariant u>=0
 	when True sync sndD do {u:=0} goto in_transitK;
@@ -138,7 +138,7 @@ end (* channelK *)
 (****************************************************)
 automaton channelL
 (****************************************************)
-synclabs: sndA, rcvA, lostL;
+actions: sndA, rcvA, lostL;
 
 loc startL: invariant v>=0
 	when True sync sndA do {v:=0} goto in_transitL;

diff --git a/benchmarks/BRP/BRPDKRT97/BRPDKRT97.imi b/benchmarks/BRP/BRPDKRT97/BRPDKRT97.imi
@@ -62,7 +62,7 @@ var
 (************************************************************)
 automaton sender
 (************************************************************)
-synclabs: Sin, B, F, Sout_DK, Sout_NOK, Sout_OK;
+actions: Sin, B, F, Sout_DK, Sout_NOK, Sout_OK;
 
 
 loc idleS: invariant x>=0
@@ -107,7 +107,7 @@ end (*sender*)
 (************************************************************)
 automaton receiver
 (************************************************************)
-synclabs: G, A, Rout_NOK, Rout_OK, Rout_FST, Rout_INC;
+actions: G, A, Rout_NOK, Rout_OK, Rout_FST, Rout_INC;
 
 
 loc new_file: invariant z>=0
@@ -170,7 +170,7 @@ end (*receiver*)
 (************************************************************)
 automaton channelK
 (************************************************************)
-synclabs: F,G;
+actions: F,G;
 
 loc startK: invariant u>=0
 
@@ -217,7 +217,7 @@ end (*channelK*)
 (************************************************************)
 automaton channelL
 (************************************************************)
-synclabs: A,B;
+actions: A,B;
 
 loc startL: invariant v>=0
 
@@ -240,7 +240,7 @@ end (*channelL*)
 (************************************************************)
 automaton Sclient
 (************************************************************)
-synclabs: Sin, Sout_OK, Sout_DK, Sout_NOK;
+actions: Sin, Sout_OK, Sout_DK, Sout_NOK;
 
 loc startSC: invariant ys<=SYNC 	(*invariant ys>=0*)
 
@@ -259,7 +259,7 @@ end (*Sclient*)
 (************************************************************)
 automaton Rclient
 (************************************************************)
-synclabs: Rout_FST, Rout_OK, Rout_INC, Rout_NOK;
+actions: Rout_FST, Rout_OK, Rout_INC, Rout_NOK;
 
 loc startRC: invariant yr>=0
 

diff --git a/benchmarks/CSMACD/CSMACD-bc1.imi b/benchmarks/CSMACD/CSMACD-bc1.imi
@@ -42,7 +42,7 @@ var
 (************************************************************)
 automaton medium
 (************************************************************)
-synclabs: send1, send2, end1, end2, busy1, busy2, cd;
+actions: send1, send2, end1, end2, busy1, busy2, cd;
 
 loc Init: invariant True
 		when True sync send1 do {y := 0} goto Transmit;
@@ -68,7 +68,7 @@ end (* medium *)
 (************************************************************)
   automaton sender1
 (************************************************************)
-synclabs: send1, end1, busy1, cd, prob1;
+actions: send1, end1, busy1, cd, prob1;
 
 loc Init1: invariant True
 	when True sync send1 do {} goto Transmit1;
@@ -110,7 +110,7 @@ end (* sender1 *)
 (************************************************************)
   automaton sender2
 (************************************************************)
-synclabs: send2, end2, busy2, cd, prob2;
+actions: send2, end2, busy2, cd, prob2;
 
 loc Init2: invariant x2 = 0
 	when x2 = 0 sync send2 do {} goto Transmit2;

diff --git a/benchmarks/CSMACD/CSMACD-bc10.imi b/benchmarks/CSMACD/CSMACD-bc10.imi
@@ -43,7 +43,7 @@ var
 (************************************************************)
   automaton medium
 (************************************************************)
-synclabs: send1, send2, end1, end2, busy1, busy2, cd;
+actions: send1, send2, end1, end2, busy1, busy2, cd;
 
 loc Init: invariant True
 		when True sync send1 do {y := 0} goto Transmit;
@@ -69,7 +69,7 @@ end (* medium *)
 (************************************************************)
   automaton sender1
 (************************************************************)
-synclabs: send1, end1, busy1, cd, prob1;
+actions: send1, end1, busy1, cd, prob1;
 
 loc Init1: invariant True
 	when True sync send1 do {} goto Transmit1;
@@ -20584,7 +20584,7 @@ end (* sender1 *)
 (************************************************************)
   automaton sender2
 (************************************************************)
-synclabs: send2, end2, busy2, cd, prob2;
+actions: send2, end2, busy2, cd, prob2;
 
 loc Init2: invariant x2 = 0
 	when x2 = 0 sync send2 do {} goto Transmit2;

diff --git a/benchmarks/CSMACD/CSMACD-bc5.imi b/benchmarks/CSMACD/CSMACD-bc5.imi
@@ -40,7 +40,7 @@ var
 (************************************************************)
   automaton medium
 (************************************************************)
-synclabs: send1, send2, end1, end2, busy1, busy2, cd;
+actions: send1, send2, end1, end2, busy1, busy2, cd;
 
 loc Init: invariant True
 		when True sync send1 do {y := 0} goto Transmit;
@@ -66,7 +66,7 @@ end (* medium *)
 (************************************************************)
   automaton sender1
 (************************************************************)
-synclabs: send1, end1, busy1, cd, prob1;
+actions: send1, end1, busy1, cd, prob1;
 
 loc Init1: invariant True
 	when True sync send1 do {} goto Transmit1;
@@ -725,7 +725,7 @@ end (* sender1 *)
 (************************************************************)
   automaton sender2
 (************************************************************)
-synclabs: send2, end2, busy2, cd, prob2;
+actions: send2, end2, busy2, cd, prob2;
 
 loc Init2: invariant x2 = 0
 	when x2 = 0 sync send2 do {} goto Transmit2;

diff --git a/benchmarks/CSMACD/CSMACD-bc6.imi b/benchmarks/CSMACD/CSMACD-bc6.imi
@@ -43,7 +43,7 @@ var
 (************************************************************)
   automaton medium
 (************************************************************)
-synclabs: send1, send2, end1, end2, busy1, busy2, cd;
+actions: send1, send2, end1, end2, busy1, busy2, cd;
 
 loc Init: invariant True
 		when True sync send1 do {y := 0} goto Transmit;
@@ -69,7 +69,7 @@ end (* medium *)
 (************************************************************)
   automaton sender1
 (************************************************************)
-synclabs: send1, end1, busy1, cd, prob1;
+actions: send1, end1, busy1, cd, prob1;
 
 loc Init1: invariant True
 	when True sync send1 do {} goto Transmit1;
@@ -1371,7 +1371,7 @@ end (* sender1 *)
 (************************************************************)
   automaton sender2
 (************************************************************)
-synclabs: send2, end2, busy2, cd, prob2;
+actions: send2, end2, busy2, cd, prob2;
 
 loc Init2: invariant x2 = 0
 	when x2 = 0 sync send2 do {} goto Transmit2;

diff --git a/benchmarks/CSMACD/CSMACD-bc9.imi b/benchmarks/CSMACD/CSMACD-bc9.imi
@@ -43,7 +43,7 @@ var
 (************************************************************)
   automaton medium
 (************************************************************)
-synclabs: send1, send2, end1, end2, busy1, busy2, cd;
+actions: send1, send2, end1, end2, busy1, busy2, cd;
 
 loc Init: invariant True
 		when True sync send1 do {y := 0} goto Transmit;
@@ -69,7 +69,7 @@ end (* medium *)
 (************************************************************)
   automaton sender1
 (************************************************************)
-synclabs: send1, end1, busy1, cd, prob1;
+actions: send1, end1, busy1, cd, prob1;
 
 loc Init1: invariant True
 	when True sync send1 do {} goto Transmit1;
@@ -10340,7 +10340,7 @@ end (* sender1 *)
 (************************************************************)
   automaton sender2
 (************************************************************)
-synclabs: send2, end2, busy2, cd, prob2;
+actions: send2, end2, busy2, cd, prob2;
 
 loc Init2: invariant x2 = 0
 	when x2 = 0 sync send2 do {} goto Transmit2;

diff --git a/benchmarks/Coffee/Coffee/coffee.imi b/benchmarks/Coffee/Coffee/coffee.imi
@@ -40,7 +40,7 @@ var
 (************************************************************)
   automaton machine
 (************************************************************)
-synclabs: press, cup, coffee, sleep;
+actions: press, cup, coffee, sleep;
 
 loc idle: invariant True
 	when True sync press do {x := 0, y := 0} goto add_sugar;

diff --git a/benchmarks/Coffee/CoffeeDrinker/coffeeDrinker.imi b/benchmarks/Coffee/CoffeeDrinker/coffeeDrinker.imi
@@ -59,7 +59,7 @@ var
 (************************************************************)
   automaton machine
 (************************************************************)
-synclabs: press, cup, coffee, sleep;
+actions: press, cup, coffee, sleep;
 
 loc idle: invariant True
 	when True sync press do {x1 := 0, x2 := 0} goto add_sugar;
@@ -83,7 +83,7 @@ end (* machine *)
 (************************************************************)
   automaton researcher
 (************************************************************)
-synclabs: press, coffee;
+actions: press, coffee;
 
 loc researching: invariant y1 <= p_work_max
 	when y1 >= p_work_min sync press do {y1 := 0, y2 := 0, nb_sugar := 0} goto add_sugar;