diff --git a/benchmarks/code_gen/QueensWithEvents_4.mch b/benchmarks/code_gen/QueensWithEvents_4.mch index f4b1b5103e75174f8ab410695bc8deebfbf49454..5ba3826a4cf52dade25c612c4474420c826162dc 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 fd9a28417358d9401c5a10290c9adc166df2d2f1..c0af851622cc1f69fd6f53fa615f36a73ecca32e 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 5e04d9f92a6858a60123d3c4db5a58727e8c0a37..d1ef48c589399aa3765ce78563aaa250628fba2e 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 f47a158fa344572ae50776294f9662165e82380e..eeb4d3ceb8d7ed839e82b59f1149d56180aff172 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 58a1018b52c879f6d34dc26766500d072573906f..3b7748b182f23cc8d17a122ae4753cbfdb2360ce 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 fd9a28417358d9401c5a10290c9adc166df2d2f1..c0af851622cc1f69fd6f53fa615f36a73ecca32e 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 06b69b9540a39635ba03f945921e5048096090fc..432a591d2fe90ec7a37e1daf46a54ac0244a93bf 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 8d5db0c9079e3fc5e9e6c7e429597d8035719476..748ead23f936ef18b0d6a1e64e0d702b8de1fb82 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 58a1018b52c879f6d34dc26766500d072573906f..3b7748b182f23cc8d17a122ae4753cbfdb2360ce 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 fe5b9db768af3145063cad2ec8eaf2200b1b567e..ffb61136fad19591a35e01c16efa85b6ff430941 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 824f2059b763f16767fe6d130345fdc35abcfc6d..27ae2772922b983a0d2dfcc63db7c5b14eb0644f 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 fe5b9db768af3145063cad2ec8eaf2200b1b567e..ffb61136fad19591a35e01c16efa85b6ff430941 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 824f2059b763f16767fe6d130345fdc35abcfc6d..27ae2772922b983a0d2dfcc63db7c5b14eb0644f 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 f4b1b5103e75174f8ab410695bc8deebfbf49454..5ba3826a4cf52dade25c612c4474420c826162dc 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 a266ddb071b6106280101420f1e4de1563bb5942..333eed23997aab241999e5df85ef6d411a0b21b7 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