From 8c17832c5d44ffdb90938d78cbd73ab4b8cc5166 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?=C3=89tienne=20Andr=C3=A9?= Date: Tue, 16 Jan 2024 13:30:21 +0100 Subject: [PATCH] Update syntax of PS80 benchmark --- .../Fischer/FischerPS08/FischerPS08-10.imi | 22 +++++++++---------- .../Fischer/FischerPS08/FischerPS08-2.imi | 10 ++++----- .../Fischer/FischerPS08/FischerPS08-3.imi | 12 +++++----- .../Fischer/FischerPS08/FischerPS08-4.imi | 12 +++++----- .../Fischer/FischerPS08/FischerPS08-5.imi | 14 ++++++------ .../FischerPS08/script/fischer_novar_gen.py | 8 +++---- 6 files changed, 39 insertions(+), 39 deletions(-) diff --git a/benchmarks/Fischer/FischerPS08/FischerPS08-10.imi b/benchmarks/Fischer/FischerPS08/FischerPS08-10.imi index 70b8e2f66..f187686ff 100644 --- 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 index 4c3107273..10ccbc53b 100644 --- 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 index 120a81831..5b8595ea3 100644 --- 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 index 4df62926d..bed76cae0 100644 --- 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 index 66c743f22..98b08140b 100644 --- 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 index bc1777389..4e24035e9 100644 --- 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]) + ";")