From 15ebbfd7f42c6e0885a1c843e8b3a79a51b5c06b Mon Sep 17 00:00:00 2001 From: Fabian Vu <Fabian.Vu@hhu.de> Date: Sun, 24 Nov 2024 22:58:04 +0100 Subject: [PATCH] Update information on models in benchmarks --- .../Train_1_beebook_deterministic_MC_POR_v3.mch | 10 +++++++++- .../execution/ProB/Train_1_beebook_deterministic.mch | 4 ++++ .../ProB/Train_1_beebook_deterministic_MC_POR.mch | 6 ++++++ .../ProB/Train_1_beebook_deterministic_MC_POR_v2.mch | 7 +++++++ .../TLC/Train_1_beebook_deterministic_MC_POR.mch | 5 +++++ .../TLC/Train_1_beebook_deterministic_MC_POR_v2.mch | 7 +++++++ .../ProB/Train_1_beebook_deterministic_MC_POR_v3.mch | 10 +++++++++- 7 files changed, 47 insertions(+), 2 deletions(-) diff --git a/benchmarks/code_gen/Train_1_beebook_deterministic_MC_POR_v3.mch b/benchmarks/code_gen/Train_1_beebook_deterministic_MC_POR_v3.mch index 4a4d10182..585d1ed7b 100644 --- a/benchmarks/code_gen/Train_1_beebook_deterministic_MC_POR_v3.mch +++ b/benchmarks/code_gen/Train_1_beebook_deterministic_MC_POR_v3.mch @@ -1,4 +1,12 @@ -MACHINE Train_1_beebook_deterministic_MC_POR_v3 // this version is very close to Train_1_beebook_tlc_POR. For instance, top-level ANY substitutions are not re-written to PRE as done in Train_1_beebook_deterministic_MC_POR_v2. DEFINITIONS are still inlined. +/* +Original model: +J.-R. Abrial. Modeling in Event-B: System and Software Engineering. Cambridge University Press, 2010. + +Model applies Partial Order Reduction manually. +Rewritten version for B2Program. +This version is very close to Train_1_beebook_tlc_POR. For instance, top-level ANY substitutions are not re-written to PRE as done in Train_1_beebook_deterministic_MC_POR_v2. DEFINITIONS are still inlined. +*/ +MACHINE Train_1_beebook_deterministic_MC_POR_v3 SETS /* enumerated */ BLOCKS={A,B,C,D,E,F,G,H,I,J,K,L,M,N}; ROUTES={R1,R2,R3,R4,R5,R6,R7,R8,R9,R10} diff --git a/benchmarks/execution/ProB/Train_1_beebook_deterministic.mch b/benchmarks/execution/ProB/Train_1_beebook_deterministic.mch index 8793824d8..fcfb7b1c5 100644 --- a/benchmarks/execution/ProB/Train_1_beebook_deterministic.mch +++ b/benchmarks/execution/ProB/Train_1_beebook_deterministic.mch @@ -1,3 +1,7 @@ +/* +Original model: +J.-R. Abrial. Modeling in Event-B: System and Software Engineering. Cambridge University Press, 2010. +*/ MACHINE Train_1_beebook_deterministic SETS /* enumerated */ BLOCKS={A,B,C,D,E,F,G,H,I,J,K,L,M,N}; diff --git a/benchmarks/model_checking/ProB/Train_1_beebook_deterministic_MC_POR.mch b/benchmarks/model_checking/ProB/Train_1_beebook_deterministic_MC_POR.mch index bc2fa7808..7345139fe 100644 --- a/benchmarks/model_checking/ProB/Train_1_beebook_deterministic_MC_POR.mch +++ b/benchmarks/model_checking/ProB/Train_1_beebook_deterministic_MC_POR.mch @@ -1,3 +1,9 @@ +/* +Original model: +J.-R. Abrial. Modeling in Event-B: System and Software Engineering. Cambridge University Press, 2010. + +Model applies Partial Order Reduction manually. +*/ MACHINE Train_1_beebook_deterministic_MC_POR SETS /* enumerated */ BLOCKS={A,B,C,D,E,F,G,H,I,J,K,L,M,N}; diff --git a/benchmarks/model_checking/ProB/Train_1_beebook_deterministic_MC_POR_v2.mch b/benchmarks/model_checking/ProB/Train_1_beebook_deterministic_MC_POR_v2.mch index 40a4dc747..89cc1d2c9 100644 --- a/benchmarks/model_checking/ProB/Train_1_beebook_deterministic_MC_POR_v2.mch +++ b/benchmarks/model_checking/ProB/Train_1_beebook_deterministic_MC_POR_v2.mch @@ -1,3 +1,10 @@ +/* +Original model: +J.-R. Abrial. Modeling in Event-B: System and Software Engineering. Cambridge University Press, 2010. + +Model applies Partial Order Reduction manually. +Rewritten version for B2Program. +*/ MACHINE Train_1_beebook_deterministic_MC_POR_v2 SETS /* enumerated */ BLOCKS={A,B,C,D,E,F,G,H,I,J,K,L,M,N}; diff --git a/benchmarks/model_checking/TLC/Train_1_beebook_deterministic_MC_POR.mch b/benchmarks/model_checking/TLC/Train_1_beebook_deterministic_MC_POR.mch index bc2fa7808..f11ca712a 100644 --- a/benchmarks/model_checking/TLC/Train_1_beebook_deterministic_MC_POR.mch +++ b/benchmarks/model_checking/TLC/Train_1_beebook_deterministic_MC_POR.mch @@ -1,3 +1,8 @@ +/* +Original model: +J.-R. Abrial. Modeling in Event-B: System and Software Engineering. Cambridge University Press, 2010. + +Model applies Partial Order Reduction manually.*/ MACHINE Train_1_beebook_deterministic_MC_POR SETS /* enumerated */ BLOCKS={A,B,C,D,E,F,G,H,I,J,K,L,M,N}; diff --git a/benchmarks/model_checking/TLC/Train_1_beebook_deterministic_MC_POR_v2.mch b/benchmarks/model_checking/TLC/Train_1_beebook_deterministic_MC_POR_v2.mch index 40a4dc747..89cc1d2c9 100644 --- a/benchmarks/model_checking/TLC/Train_1_beebook_deterministic_MC_POR_v2.mch +++ b/benchmarks/model_checking/TLC/Train_1_beebook_deterministic_MC_POR_v2.mch @@ -1,3 +1,10 @@ +/* +Original model: +J.-R. Abrial. Modeling in Event-B: System and Software Engineering. Cambridge University Press, 2010. + +Model applies Partial Order Reduction manually. +Rewritten version for B2Program. +*/ MACHINE Train_1_beebook_deterministic_MC_POR_v2 SETS /* enumerated */ BLOCKS={A,B,C,D,E,F,G,H,I,J,K,L,M,N}; diff --git a/benchmarks/model_checking_opreuse/ProB/Train_1_beebook_deterministic_MC_POR_v3.mch b/benchmarks/model_checking_opreuse/ProB/Train_1_beebook_deterministic_MC_POR_v3.mch index 4a4d10182..585d1ed7b 100644 --- a/benchmarks/model_checking_opreuse/ProB/Train_1_beebook_deterministic_MC_POR_v3.mch +++ b/benchmarks/model_checking_opreuse/ProB/Train_1_beebook_deterministic_MC_POR_v3.mch @@ -1,4 +1,12 @@ -MACHINE Train_1_beebook_deterministic_MC_POR_v3 // this version is very close to Train_1_beebook_tlc_POR. For instance, top-level ANY substitutions are not re-written to PRE as done in Train_1_beebook_deterministic_MC_POR_v2. DEFINITIONS are still inlined. +/* +Original model: +J.-R. Abrial. Modeling in Event-B: System and Software Engineering. Cambridge University Press, 2010. + +Model applies Partial Order Reduction manually. +Rewritten version for B2Program. +This version is very close to Train_1_beebook_tlc_POR. For instance, top-level ANY substitutions are not re-written to PRE as done in Train_1_beebook_deterministic_MC_POR_v2. DEFINITIONS are still inlined. +*/ +MACHINE Train_1_beebook_deterministic_MC_POR_v3 SETS /* enumerated */ BLOCKS={A,B,C,D,E,F,G,H,I,J,K,L,M,N}; ROUTES={R1,R2,R3,R4,R5,R6,R7,R8,R9,R10} -- GitLab