diff --git a/src/test/resources/de/hhu/stups/codegenerator/StringLaws.mch b/src/test/resources/de/hhu/stups/codegenerator/StringLaws.mch index 080563cfcb202d2a3b92bfb8324a985190aab9ec..fed239107035492987ed147ab6190be461cc36ac 100644 --- a/src/test/resources/de/hhu/stups/codegenerator/StringLaws.mch +++ b/src/test/resources/de/hhu/stups/codegenerator/StringLaws.mch @@ -1,3 +1,7 @@ +/* +From ProB Examples, originally used to test ProB, +rewritten for B2Program +*/ MACHINE StringLaws DEFINITIONS laws == ((s1=s2 <=> s2=s1) & diff --git a/src/test/resources/de/hhu/stups/codegenerator/SubstitutionLaws.mch b/src/test/resources/de/hhu/stups/codegenerator/SubstitutionLaws.mch index 777be9a20fe47512b1ff2676629797fd2d91eaca..7a40cf0b64c695da01146cb37d551a63a83ef7cc 100644 --- a/src/test/resources/de/hhu/stups/codegenerator/SubstitutionLaws.mch +++ b/src/test/resources/de/hhu/stups/codegenerator/SubstitutionLaws.mch @@ -1,3 +1,7 @@ +/* +From ProB Examples, originally used to test ProB, +rewritten for B2Program +*/ MACHINE SubstitutionLaws SETS ID={aa,bb} diff --git a/src/test/resources/de/hhu/stups/codegenerator/Train_1_beebook_TLC.mch b/src/test/resources/de/hhu/stups/codegenerator/Train_1_beebook_TLC.mch index 6d28f16d21f06ac325b1bf67ee0471f6628f850d..53c6091c75dbcd6214541238d152eebf1977f4b2 100644 --- a/src/test/resources/de/hhu/stups/codegenerator/Train_1_beebook_TLC.mch +++ b/src/test/resources/de/hhu/stups/codegenerator/Train_1_beebook_TLC.mch @@ -1,3 +1,9 @@ +/* +Original model: +J.-R. Abrial. Modeling in Event-B: System and Software Engineering. Cambridge University Press, 2010. + +Rewritten for TLC +*/ MACHINE Train_1_beebook_TLC SETS /* enumerated */ BLOCKS={A,B,C,D,E,F,G,H,I,J,K,L,M,N}; diff --git a/src/test/resources/de/hhu/stups/codegenerator/Train_1_beebook_deterministic.mch b/src/test/resources/de/hhu/stups/codegenerator/Train_1_beebook_deterministic.mch index 5bd11dca65a14af297b76db04af7f242b77ac90c..eb8ebe15e5d73cfdc4b010b952d68907fe338ed7 100644 --- a/src/test/resources/de/hhu/stups/codegenerator/Train_1_beebook_deterministic.mch +++ b/src/test/resources/de/hhu/stups/codegenerator/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/src/test/resources/de/hhu/stups/codegenerator/Train_1_beebook_deterministic_MC.mch b/src/test/resources/de/hhu/stups/codegenerator/Train_1_beebook_deterministic_MC.mch index 225cbd969652455e9b0bb419712a3e001073bafe..3a5066521205f4dcace640eda409566bae09086b 100644 --- a/src/test/resources/de/hhu/stups/codegenerator/Train_1_beebook_deterministic_MC.mch +++ b/src/test/resources/de/hhu/stups/codegenerator/Train_1_beebook_deterministic_MC.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 SETS /* enumerated */ BLOCKS={A,B,C,D,E,F,G,H,I,J,K,L,M,N}; diff --git a/src/test/resources/de/hhu/stups/codegenerator/Train_1_beebook_deterministic_MC_POR.mch b/src/test/resources/de/hhu/stups/codegenerator/Train_1_beebook_deterministic_MC_POR.mch index 69c95a793dd28cd6ed5a9b6ebe4034cfe2d6094a..3173c5ec3b68e9580ea7333a4fc9181731fe1a87 100644 --- a/src/test/resources/de/hhu/stups/codegenerator/Train_1_beebook_deterministic_MC_POR.mch +++ b/src/test/resources/de/hhu/stups/codegenerator/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/src/test/resources/de/hhu/stups/codegenerator/Train_1_beebook_deterministic_MC_POR_v2.mch b/src/test/resources/de/hhu/stups/codegenerator/Train_1_beebook_deterministic_MC_POR_v2.mch index 98968f824d39ad7611d5dcf40facc650dec39ff7..c55c9a88becd13d54684aec902622cb72f3ae47f 100644 --- a/src/test/resources/de/hhu/stups/codegenerator/Train_1_beebook_deterministic_MC_POR_v2.mch +++ b/src/test/resources/de/hhu/stups/codegenerator/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/src/test/resources/de/hhu/stups/codegenerator/Train_1_beebook_deterministic_MC_POR_v3.mch b/src/test/resources/de/hhu/stups/codegenerator/Train_1_beebook_deterministic_MC_POR_v3.mch index 4a4d1018281a21e7208d7476dc40ea55ef5df204..585d1ed7b38bcc0b56f6ee9dbb30aa36d1252aa2 100644 --- a/src/test/resources/de/hhu/stups/codegenerator/Train_1_beebook_deterministic_MC_POR_v3.mch +++ b/src/test/resources/de/hhu/stups/codegenerator/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/src/test/resources/de/hhu/stups/codegenerator/sort_m2_data1000.mch b/src/test/resources/de/hhu/stups/codegenerator/sort_m2_data1000.mch index c37ac180f49466038864708ed05285d2746d144e..941e2d3e2a03b82477d3e78154c8428d559bda84 100644 --- a/src/test/resources/de/hhu/stups/codegenerator/sort_m2_data1000.mch +++ b/src/test/resources/de/hhu/stups/codegenerator/sort_m2_data1000.mch @@ -1,3 +1,7 @@ +/* +Original Model: +V. Rivera, N. Catano, T. Wahls, and C. Rueda. Code generation for Event-B. STTT, 19(1):31–52, 2017. +*/ MACHINE sort_m2_data1000 // a version where some assertions and invariants are simplified/removed // so that TLC4B can infer a function type for f and g diff --git a/src/test/resources/de/hhu/stups/codegenerator/sort_m2_data1000_MC.mch b/src/test/resources/de/hhu/stups/codegenerator/sort_m2_data1000_MC.mch index 13d7644099dd73c5bda36e189ec5bfb48d67ed2f..b932db0c11536ee66380e297d97e1b3680edb83d 100644 --- a/src/test/resources/de/hhu/stups/codegenerator/sort_m2_data1000_MC.mch +++ b/src/test/resources/de/hhu/stups/codegenerator/sort_m2_data1000_MC.mch @@ -1,3 +1,7 @@ +/* +Original Model: +V. Rivera, N. Catano, T. Wahls, and C. Rueda. Code generation for Event-B. STTT, 19(1):31–52, 2017. +*/ MACHINE sort_m2_data1000_MC // a version where some assertions and invariants are simplified/removed // so that TLC4B can infer a function type for f and g diff --git a/src/test/resources/de/hhu/stups/codegenerator/tictac.mch b/src/test/resources/de/hhu/stups/codegenerator/tictac.mch index 9e573e23ed507aa545b5ebf400a10da15d9cd69e..06918e383373150a5d7d7bd9891cca029406159a 100644 --- a/src/test/resources/de/hhu/stups/codegenerator/tictac.mch +++ b/src/test/resources/de/hhu/stups/codegenerator/tictac.mch @@ -1,3 +1,6 @@ +/* +From ProB Examples +*/ MACHINE tictac ABSTRACT_VARIABLES square, turn