From 1ab50739ade03d27749589c038b463773bae799c Mon Sep 17 00:00:00 2001 From: Fabian Vu <Fabian.Vu@hhu.de> Date: Sun, 24 Nov 2024 23:06:17 +0100 Subject: [PATCH] Update information on used models --- benchmarks/code_gen/QueensWithEvents_4.mch | 3 +++ benchmarks/model_checking/ProB/QueensWithEvents_4.mch | 3 +++ benchmarks/model_checking/ProB/QueensWithEvents_8.mch | 3 +++ benchmarks/model_checking/ProB/QueensWithEvents_Original_4.mch | 3 +++ benchmarks/model_checking/ProB/QueensWithEvents_Original_8.mch | 3 +++ benchmarks/model_checking/TLC/QueensWithEvents_4.mch | 3 +++ benchmarks/model_checking/TLC/QueensWithEvents_8.mch | 3 +++ benchmarks/model_checking/TLC/QueensWithEvents_Original_4.mch | 3 +++ benchmarks/model_checking/TLC/QueensWithEvents_Original_8.mch | 3 +++ .../ProB/QueensWithEvents_Original_4.mch | 3 +++ .../ProB/QueensWithEvents_Original_8.mch | 3 +++ .../model_checking_opreuse/TLC/QueensWithEvents_Original_4.mch | 3 +++ .../model_checking_opreuse/TLC/QueensWithEvents_Original_8.mch | 3 +++ .../de/hhu/stups/codegenerator/QueensWithEvents_4.mch | 3 +++ .../de/hhu/stups/codegenerator/QueensWithEvents_8.mch | 3 +++ 15 files changed, 45 insertions(+) diff --git a/benchmarks/code_gen/QueensWithEvents_4.mch b/benchmarks/code_gen/QueensWithEvents_4.mch index f4b1b5103..5ba3826a4 100644 --- a/benchmarks/code_gen/QueensWithEvents_4.mch +++ b/benchmarks/code_gen/QueensWithEvents_4.mch @@ -1,3 +1,6 @@ +/* +From ProB examples +*/ MACHINE QueensWithEvents_4 // rewritten for B2Program by inlining DEFINITIONS // v2: rewrote perm(1..n) for B2Program diff --git a/benchmarks/model_checking/ProB/QueensWithEvents_4.mch b/benchmarks/model_checking/ProB/QueensWithEvents_4.mch index fd9a28417..c0af85162 100644 --- a/benchmarks/model_checking/ProB/QueensWithEvents_4.mch +++ b/benchmarks/model_checking/ProB/QueensWithEvents_4.mch @@ -1,3 +1,6 @@ +/* +From ProB examples +*/ MACHINE QueensWithEvents_4 // rewritten for B2Program by inlining DEFINITIONS // v2: rewrote perm(1..n) for B2Program diff --git a/benchmarks/model_checking/ProB/QueensWithEvents_8.mch b/benchmarks/model_checking/ProB/QueensWithEvents_8.mch index 5e04d9f92..d1ef48c58 100644 --- a/benchmarks/model_checking/ProB/QueensWithEvents_8.mch +++ b/benchmarks/model_checking/ProB/QueensWithEvents_8.mch @@ -1,3 +1,6 @@ +/* +From ProB examples +*/ MACHINE QueensWithEvents_8 // rewritten for B2Program by inlining DEFINITIONS // v2: rewrote perm(1..n) for B2Program diff --git a/benchmarks/model_checking/ProB/QueensWithEvents_Original_4.mch b/benchmarks/model_checking/ProB/QueensWithEvents_Original_4.mch index f47a158fa..eeb4d3ceb 100644 --- a/benchmarks/model_checking/ProB/QueensWithEvents_Original_4.mch +++ b/benchmarks/model_checking/ProB/QueensWithEvents_Original_4.mch @@ -1,3 +1,6 @@ +/* +From ProB examples +*/ MACHINE QueensWithEvents_Original_4 // close to the original // rewritten for B2Program by inlining DEFINITIONS // but not rewriting perm diff --git a/benchmarks/model_checking/ProB/QueensWithEvents_Original_8.mch b/benchmarks/model_checking/ProB/QueensWithEvents_Original_8.mch index 58a1018b5..3b7748b18 100644 --- a/benchmarks/model_checking/ProB/QueensWithEvents_Original_8.mch +++ b/benchmarks/model_checking/ProB/QueensWithEvents_Original_8.mch @@ -1,3 +1,6 @@ +/* +From ProB examples +*/ MACHINE QueensWithEvents_Original_8 // close to the original // rewritten for B2Program by inlining DEFINITIONS // but not rewriting perm diff --git a/benchmarks/model_checking/TLC/QueensWithEvents_4.mch b/benchmarks/model_checking/TLC/QueensWithEvents_4.mch index fd9a28417..c0af85162 100644 --- a/benchmarks/model_checking/TLC/QueensWithEvents_4.mch +++ b/benchmarks/model_checking/TLC/QueensWithEvents_4.mch @@ -1,3 +1,6 @@ +/* +From ProB examples +*/ MACHINE QueensWithEvents_4 // rewritten for B2Program by inlining DEFINITIONS // v2: rewrote perm(1..n) for B2Program diff --git a/benchmarks/model_checking/TLC/QueensWithEvents_8.mch b/benchmarks/model_checking/TLC/QueensWithEvents_8.mch index 06b69b954..432a591d2 100644 --- a/benchmarks/model_checking/TLC/QueensWithEvents_8.mch +++ b/benchmarks/model_checking/TLC/QueensWithEvents_8.mch @@ -1,3 +1,6 @@ +/* +From ProB examples +*/ MACHINE QueensWithEvents // rewritten for B2Program by inlining DEFINITIONS // v2: rewrote perm(1..n) for B2Program diff --git a/benchmarks/model_checking/TLC/QueensWithEvents_Original_4.mch b/benchmarks/model_checking/TLC/QueensWithEvents_Original_4.mch index 8d5db0c90..748ead23f 100644 --- a/benchmarks/model_checking/TLC/QueensWithEvents_Original_4.mch +++ b/benchmarks/model_checking/TLC/QueensWithEvents_Original_4.mch @@ -1,3 +1,6 @@ +/* +From ProB examples +*/ MACHINE QueensWithEvents_Original_4 // close to the original // rewritten for B2Program by inlining DEFINITIONS // but not rewriting perm diff --git a/benchmarks/model_checking/TLC/QueensWithEvents_Original_8.mch b/benchmarks/model_checking/TLC/QueensWithEvents_Original_8.mch index 58a1018b5..3b7748b18 100644 --- a/benchmarks/model_checking/TLC/QueensWithEvents_Original_8.mch +++ b/benchmarks/model_checking/TLC/QueensWithEvents_Original_8.mch @@ -1,3 +1,6 @@ +/* +From ProB examples +*/ MACHINE QueensWithEvents_Original_8 // close to the original // rewritten for B2Program by inlining DEFINITIONS // but not rewriting perm diff --git a/benchmarks/model_checking_opreuse/ProB/QueensWithEvents_Original_4.mch b/benchmarks/model_checking_opreuse/ProB/QueensWithEvents_Original_4.mch index fe5b9db76..ffb61136f 100644 --- a/benchmarks/model_checking_opreuse/ProB/QueensWithEvents_Original_4.mch +++ b/benchmarks/model_checking_opreuse/ProB/QueensWithEvents_Original_4.mch @@ -1,3 +1,6 @@ +/* +From ProB examples +*/ MACHINE QueensWithEvents_Original_4 // close to the original // rewritten for B2Program by inlining DEFINITIONS // but not rewriting perm diff --git a/benchmarks/model_checking_opreuse/ProB/QueensWithEvents_Original_8.mch b/benchmarks/model_checking_opreuse/ProB/QueensWithEvents_Original_8.mch index 824f2059b..27ae27729 100644 --- a/benchmarks/model_checking_opreuse/ProB/QueensWithEvents_Original_8.mch +++ b/benchmarks/model_checking_opreuse/ProB/QueensWithEvents_Original_8.mch @@ -1,3 +1,6 @@ +/* +From ProB examples +*/ MACHINE QueensWithEvents_Original_8 // close to the original // rewritten for B2Program by inlining DEFINITIONS // but not rewriting perm diff --git a/benchmarks/model_checking_opreuse/TLC/QueensWithEvents_Original_4.mch b/benchmarks/model_checking_opreuse/TLC/QueensWithEvents_Original_4.mch index fe5b9db76..ffb61136f 100644 --- a/benchmarks/model_checking_opreuse/TLC/QueensWithEvents_Original_4.mch +++ b/benchmarks/model_checking_opreuse/TLC/QueensWithEvents_Original_4.mch @@ -1,3 +1,6 @@ +/* +From ProB examples +*/ MACHINE QueensWithEvents_Original_4 // close to the original // rewritten for B2Program by inlining DEFINITIONS // but not rewriting perm diff --git a/benchmarks/model_checking_opreuse/TLC/QueensWithEvents_Original_8.mch b/benchmarks/model_checking_opreuse/TLC/QueensWithEvents_Original_8.mch index 824f2059b..27ae27729 100644 --- a/benchmarks/model_checking_opreuse/TLC/QueensWithEvents_Original_8.mch +++ b/benchmarks/model_checking_opreuse/TLC/QueensWithEvents_Original_8.mch @@ -1,3 +1,6 @@ +/* +From ProB examples +*/ MACHINE QueensWithEvents_Original_8 // close to the original // rewritten for B2Program by inlining DEFINITIONS // but not rewriting perm diff --git a/src/test/resources/de/hhu/stups/codegenerator/QueensWithEvents_4.mch b/src/test/resources/de/hhu/stups/codegenerator/QueensWithEvents_4.mch index f4b1b5103..5ba3826a4 100644 --- a/src/test/resources/de/hhu/stups/codegenerator/QueensWithEvents_4.mch +++ b/src/test/resources/de/hhu/stups/codegenerator/QueensWithEvents_4.mch @@ -1,3 +1,6 @@ +/* +From ProB examples +*/ MACHINE QueensWithEvents_4 // rewritten for B2Program by inlining DEFINITIONS // v2: rewrote perm(1..n) for B2Program diff --git a/src/test/resources/de/hhu/stups/codegenerator/QueensWithEvents_8.mch b/src/test/resources/de/hhu/stups/codegenerator/QueensWithEvents_8.mch index a266ddb07..333eed239 100644 --- a/src/test/resources/de/hhu/stups/codegenerator/QueensWithEvents_8.mch +++ b/src/test/resources/de/hhu/stups/codegenerator/QueensWithEvents_8.mch @@ -1,3 +1,6 @@ +/* +From ProB examples +*/ MACHINE QueensWithEvents_8 // rewritten for B2Program by inlining DEFINITIONS // v2: rewrote perm(1..n) for B2Program -- GitLab