Update syntax of PS80 benchmark

imitator-model-checker · Jan 16, 2024 · 8c17832 · 8c17832
1 parent 0c0f67a
commit 8c17832
Show file tree

Hide file tree

Showing 6 changed files with 39 additions and 39 deletions.
diff --git a/benchmarks/Fischer/FischerPS08/FischerPS08-10.imi b/benchmarks/Fischer/FischerPS08/FischerPS08-10.imi
@@ -35,7 +35,7 @@ var
 	: parameter;
 
 automaton process1
-	synclabs: Start1, SetX1, Enter1, SetX01;
+	actions: Start1, SetX1, Enter1, SetX01;
 
 	loc idle1: invariant True
 		when True sync Start1 do {x1 := 0} goto trying1;
@@ -52,7 +52,7 @@ automaton process1
 end
 
 automaton process2
-	synclabs: Start2, SetX2, Enter2, SetX02;
+	actions: Start2, SetX2, Enter2, SetX02;
 
 	loc idle2: invariant True
 		when True sync Start2 do {x2 := 0} goto trying2;
@@ -69,7 +69,7 @@ automaton process2
 end
 
 automaton process3
-	synclabs: Start3, SetX3, Enter3, SetX03;
+	actions: Start3, SetX3, Enter3, SetX03;
 
 	loc idle3: invariant True
 		when True sync Start3 do {x3 := 0} goto trying3;
@@ -86,7 +86,7 @@ automaton process3
 end
 
 automaton process4
-	synclabs: Start4, SetX4, Enter4, SetX04;
+	actions: Start4, SetX4, Enter4, SetX04;
 
 	loc idle4: invariant True
 		when True sync Start4 do {x4 := 0} goto trying4;
@@ -103,7 +103,7 @@ automaton process4
 end
 
 automaton process5
-	synclabs: Start5, SetX5, Enter5, SetX05;
+	actions: Start5, SetX5, Enter5, SetX05;
 
 	loc idle5: invariant True
 		when True sync Start5 do {x5 := 0} goto trying5;
@@ -120,7 +120,7 @@ automaton process5
 end
 
 automaton process6
-	synclabs: Start6, SetX6, Enter6, SetX06;
+	actions: Start6, SetX6, Enter6, SetX06;
 
 	loc idle6: invariant True
 		when True sync Start6 do {x6 := 0} goto trying6;
@@ -137,7 +137,7 @@ automaton process6
 end
 
 automaton process7
-	synclabs: Start7, SetX7, Enter7, SetX07;
+	actions: Start7, SetX7, Enter7, SetX07;
 
 	loc idle7: invariant True
 		when True sync Start7 do {x7 := 0} goto trying7;
@@ -154,7 +154,7 @@ automaton process7
 end
 
 automaton process8
-	synclabs: Start8, SetX8, Enter8, SetX08;
+	actions: Start8, SetX8, Enter8, SetX08;
 
 	loc idle8: invariant True
 		when True sync Start8 do {x8 := 0} goto trying8;
@@ -171,7 +171,7 @@ automaton process8
 end
 
 automaton process9
-	synclabs: Start9, SetX9, Enter9, SetX09;
+	actions: Start9, SetX9, Enter9, SetX09;
 
 	loc idle9: invariant True
 		when True sync Start9 do {x9 := 0} goto trying9;
@@ -188,7 +188,7 @@ automaton process9
 end
 
 automaton process10
-	synclabs: Start10, SetX10, Enter10, SetX010;
+	actions: Start10, SetX10, Enter10, SetX010;
 
 	loc idle10: invariant True
 		when True sync Start10 do {x10 := 0} goto trying10;
@@ -205,7 +205,7 @@ automaton process10
 end
 
 automaton variable
-	synclabs:
+	actions:
 	Start1, SetX1, Enter1, SetX01, Start2, SetX2, Enter2, SetX02, Start3, SetX3, Enter3, SetX03, Start4, SetX4, Enter4, SetX04, Start5, SetX5, Enter5, SetX05, Start6, SetX6, Enter6, SetX06, Start7, SetX7, Enter7, SetX07, Start8, SetX8, Enter8, SetX08, Start9, SetX9, Enter9, SetX09, Start10, SetX10, Enter10, SetX010;
 
 	loc Val0: invariant True

diff --git a/benchmarks/Fischer/FischerPS08/FischerPS08-2.imi b/benchmarks/Fischer/FischerPS08/FischerPS08-2.imi
@@ -15,10 +15,10 @@
  * License          : 
  * 
  * Created          : 
- * Last modified    : 2021/08/30
+ * Last modified    : 2024/01/16
  * Model version    : 
  * 
- * IMITATOR version : 3.1
+ * IMITATOR version : 3.4
  ******************************************************************************)
 
 
@@ -35,7 +35,7 @@ var
 	: parameter;
 
 automaton process1
-	synclabs: Start1, SetX1, Enter1, SetX01;
+	actions: Start1, SetX1, Enter1, SetX01;
 
 	loc idle1: invariant True
 		when True sync Start1 do {x1 := 0} goto trying1;
@@ -52,7 +52,7 @@ automaton process1
 end
 
 automaton process2
-	synclabs: Start2, SetX2, Enter2, SetX02;
+	actions: Start2, SetX2, Enter2, SetX02;
 
 	loc idle2: invariant True
 		when True sync Start2 do {x2 := 0} goto trying2;
@@ -69,7 +69,7 @@ automaton process2
 end
 
 automaton variable
-	synclabs:
+	actions:
 	Start1, SetX1, Enter1, SetX01, Start2, SetX2, Enter2, SetX02;
 
 	loc Val0: invariant True

diff --git a/benchmarks/Fischer/FischerPS08/FischerPS08-3.imi b/benchmarks/Fischer/FischerPS08/FischerPS08-3.imi
@@ -15,10 +15,10 @@
  * License          : 
  * 
  * Created          : 
- * Last modified    : 2021/08/30
+ * Last modified    : 2024/01/16
  * Model version    : 
  * 
- * IMITATOR version : 3.1
+ * IMITATOR version : 3.4
  ******************************************************************************)
 
 
@@ -35,7 +35,7 @@ var
 	: parameter;
 
 automaton process1
-	synclabs: Start1, SetX1, Enter1, SetX01;
+	actions: Start1, SetX1, Enter1, SetX01;
 
 	loc idle1: invariant True
 		when True sync Start1 do {x1 := 0} goto trying1;
@@ -52,7 +52,7 @@ automaton process1
 end
 
 automaton process2
-	synclabs: Start2, SetX2, Enter2, SetX02;
+	actions: Start2, SetX2, Enter2, SetX02;
 
 	loc idle2: invariant True
 		when True sync Start2 do {x2 := 0} goto trying2;
@@ -69,7 +69,7 @@ automaton process2
 end
 
 automaton process3
-	synclabs: Start3, SetX3, Enter3, SetX03;
+	actions: Start3, SetX3, Enter3, SetX03;
 
 	loc idle3: invariant True
 		when True sync Start3 do {x3 := 0} goto trying3;
@@ -86,7 +86,7 @@ automaton process3
 end
 
 automaton variable
-	synclabs:
+	actions:
 	Start1, SetX1, Enter1, SetX01, Start2, SetX2, Enter2, SetX02, Start3, SetX3, Enter3, SetX03;
 
 	loc Val0: invariant True

diff --git a/benchmarks/Fischer/FischerPS08/FischerPS08-4.imi b/benchmarks/Fischer/FischerPS08/FischerPS08-4.imi
@@ -15,7 +15,7 @@
  * License          : 
  * 
  * Created          : 
- * Last modified    : 2021/08/30
+ * Last modified    : 2024/01/16
  * Model version    : 
  * 
  * IMITATOR version : 3.1
@@ -35,7 +35,7 @@ var
 	: parameter;
 
 automaton process1
-	synclabs: Start1, SetX1, Enter1, SetX01;
+	actions: Start1, SetX1, Enter1, SetX01;
 
 	loc idle1: invariant True
 		when True sync Start1 do {x1 := 0} goto trying1;
@@ -52,7 +52,7 @@ automaton process1
 end
 
 automaton process2
-	synclabs: Start2, SetX2, Enter2, SetX02;
+	actions: Start2, SetX2, Enter2, SetX02;
 
 	loc idle2: invariant True
 		when True sync Start2 do {x2 := 0} goto trying2;
@@ -69,7 +69,7 @@ automaton process2
 end
 
 automaton process3
-	synclabs: Start3, SetX3, Enter3, SetX03;
+	actions: Start3, SetX3, Enter3, SetX03;
 
 	loc idle3: invariant True
 		when True sync Start3 do {x3 := 0} goto trying3;
@@ -86,7 +86,7 @@ automaton process3
 end
 
 automaton process4
-	synclabs: Start4, SetX4, Enter4, SetX04;
+	actions: Start4, SetX4, Enter4, SetX04;
 
 	loc idle4: invariant True
 		when True sync Start4 do {x4 := 0} goto trying4;
@@ -103,7 +103,7 @@ automaton process4
 end
 
 automaton variable
-	synclabs:
+	actions:
 	Start1, SetX1, Enter1, SetX01, Start2, SetX2, Enter2, SetX02, Start3, SetX3, Enter3, SetX03, Start4, SetX4, Enter4, SetX04;
 
 	loc Val0: invariant True

diff --git a/benchmarks/Fischer/FischerPS08/FischerPS08-5.imi b/benchmarks/Fischer/FischerPS08/FischerPS08-5.imi
@@ -15,7 +15,7 @@
  * License          : 
  * 
  * Created          : 
- * Last modified    : 2021/08/30
+ * Last modified    : 2024/01/16
  * Model version    : 
  * 
  * IMITATOR version : 3.1
@@ -35,7 +35,7 @@ var
 	: parameter;
 
 automaton process1
-	synclabs: Start1, SetX1, Enter1, SetX01;
+	actions: Start1, SetX1, Enter1, SetX01;
 
 	loc idle1: invariant True
 		when True sync Start1 do {x1 := 0} goto trying1;
@@ -52,7 +52,7 @@ automaton process1
 end
 
 automaton process2
-	synclabs: Start2, SetX2, Enter2, SetX02;
+	actions: Start2, SetX2, Enter2, SetX02;
 
 	loc idle2: invariant True
 		when True sync Start2 do {x2 := 0} goto trying2;
@@ -69,7 +69,7 @@ automaton process2
 end
 
 automaton process3
-	synclabs: Start3, SetX3, Enter3, SetX03;
+	actions: Start3, SetX3, Enter3, SetX03;
 
 	loc idle3: invariant True
 		when True sync Start3 do {x3 := 0} goto trying3;
@@ -86,7 +86,7 @@ automaton process3
 end
 
 automaton process4
-	synclabs: Start4, SetX4, Enter4, SetX04;
+	actions: Start4, SetX4, Enter4, SetX04;
 
 	loc idle4: invariant True
 		when True sync Start4 do {x4 := 0} goto trying4;
@@ -103,7 +103,7 @@ automaton process4
 end
 
 automaton process5
-	synclabs: Start5, SetX5, Enter5, SetX05;
+	actions: Start5, SetX5, Enter5, SetX05;
 
 	loc idle5: invariant True
 		when True sync Start5 do {x5 := 0} goto trying5;
@@ -120,7 +120,7 @@ automaton process5
 end
 
 automaton variable
-	synclabs:
+	actions:
 	Start1, SetX1, Enter1, SetX01, Start2, SetX2, Enter2, SetX02, Start3, SetX3, Enter3, SetX03, Start4, SetX4, Enter4, SetX04, Start5, SetX5, Enter5, SetX05;
 
 	loc Val0: invariant True

diff --git a/benchmarks/Fischer/FischerPS08/script/fischer_novar_gen.py b/benchmarks/Fischer/FischerPS08/script/fischer_novar_gen.py
@@ -13,9 +13,9 @@
  # Script authors  : Michal Knapick, Étienne André
  #
  # Created         : 2015/05/15
- # Last modified   : 2021/09/01
+ # Last modified   : 2024/01/16
  #
- # IMITATOR version: 3.1
+ # IMITATOR version: 3.4
  ############################################################
 
 import sys
@@ -32,7 +32,7 @@ def getVars(n):
 def getProcess(i):
 
     autStr = """automaton process{0}
-\tsynclabs: Start{0}, SetX{0}, Enter{0}, SetX0{0};
+\tactions: Start{0}, SetX{0}, Enter{0}, SetX0{0};
 
 \tloc idle{0}: invariant True
 	\twhen True sync Start{0} do {{x{0} := 0}} goto trying{0};
@@ -70,7 +70,7 @@ def getloc(i):
 
     print("automaton variable")
 
-    print("\tsynclabs:")
+    print("\tactions:")
     labs = ["Start", "SetX", "Enter", "SetX0"]
     print("\t"+", ".join([lab + str(i) for i in range(1, n+1) for lab in labs]) + ";")