diff --git a/src/test/resources/de/hhu/stups/codegenerator/Generated100.mch b/src/test/resources/de/hhu/stups/codegenerator/Generated100.mch index 4d782cc77b7287a2ac309960874828088b7d6851..52c0f94dbd009b4953f2228ec655207833cb68d5 100644 --- a/src/test/resources/de/hhu/stups/codegenerator/Generated100.mch +++ b/src/test/resources/de/hhu/stups/codegenerator/Generated100.mch @@ -1,3 +1,6 @@ +/* +From ProB Examples +*/ MACHINE Generated100 CONSTANTS c100, diff --git a/src/test/resources/de/hhu/stups/codegenerator/INTEGERSET_Laws.mch b/src/test/resources/de/hhu/stups/codegenerator/INTEGERSET_Laws.mch index eff993f40b7247d94c99faab283b9c63ba342d37..75c6e21d0ca1a9d12a60e893ed4caf5eddb4efde 100644 --- a/src/test/resources/de/hhu/stups/codegenerator/INTEGERSET_Laws.mch +++ b/src/test/resources/de/hhu/stups/codegenerator/INTEGERSET_Laws.mch @@ -1,3 +1,7 @@ +/* +From ProB Examples, originally used to test ProB, +rewritten for B2Program +*/ MACHINE INTEGERSET_Laws INVARIANT (0..4 = 1..4 \/ {0}) & diff --git a/src/test/resources/de/hhu/stups/codegenerator/IncrementalStatePackingTestLargeSlow.mch b/src/test/resources/de/hhu/stups/codegenerator/IncrementalStatePackingTestLargeSlow.mch index c31ed8ae2bde0a3cb30982f8b9ee61d03db71792..96975e52b182243b5988753b13c4f52b5f369417 100644 --- a/src/test/resources/de/hhu/stups/codegenerator/IncrementalStatePackingTestLargeSlow.mch +++ b/src/test/resources/de/hhu/stups/codegenerator/IncrementalStatePackingTestLargeSlow.mch @@ -1,3 +1,6 @@ +/* +From ProB Examples +*/ MACHINE IncrementalStatePackingTestLargeSlow SETS ID={aa,bb,cc} diff --git a/src/test/resources/de/hhu/stups/codegenerator/IncrementalStatePackingTestLargeSlow2.mch b/src/test/resources/de/hhu/stups/codegenerator/IncrementalStatePackingTestLargeSlow2.mch index 3bac7243a69af1100853335786767209c0cd2ac5..ebd4c606e838807bd09c0879d1d55287f3a7d80e 100644 --- a/src/test/resources/de/hhu/stups/codegenerator/IncrementalStatePackingTestLargeSlow2.mch +++ b/src/test/resources/de/hhu/stups/codegenerator/IncrementalStatePackingTestLargeSlow2.mch @@ -1,3 +1,6 @@ +/* +From ProB Examples +*/ MACHINE IncrementalStatePackingTestLargeSlow2 SETS ID={aa,bb,cc} diff --git a/src/test/resources/de/hhu/stups/codegenerator/NatRangeLaws.mch b/src/test/resources/de/hhu/stups/codegenerator/NatRangeLaws.mch index 0a110e423ec3eb64e89dd62b4ca1f86d5302b374..9f99738b14bf2f7f42bc7f5dae263c9386de0f56 100644 --- a/src/test/resources/de/hhu/stups/codegenerator/NatRangeLaws.mch +++ b/src/test/resources/de/hhu/stups/codegenerator/NatRangeLaws.mch @@ -1,3 +1,7 @@ +/* +From ProB Examples, originally used to test ProB, +rewritten for B2Program +*/ MACHINE NatRangeLaws VARIABLES xx,zz INVARIANT diff --git a/src/test/resources/de/hhu/stups/codegenerator/Ref5_Switch.mch b/src/test/resources/de/hhu/stups/codegenerator/Ref5_Switch.mch index abd6e688fd1ad3b86239094b4a502e8175023f1a..5a52b76a8cac96ab9764eb7b5daa68abc896222e 100644 --- a/src/test/resources/de/hhu/stups/codegenerator/Ref5_Switch.mch +++ b/src/test/resources/de/hhu/stups/codegenerator/Ref5_Switch.mch @@ -1,4 +1,9 @@ +/* +Original model from Event-B: +L. Ladenberger, D. Hansen, H. Wiegard, J. Bendisposto, and M. Leuschel. Validation of the ABZ landing gear system using ProB. In Int. J. Softw. Tools Technol. Transf., 19(2):187–203, Apr. 2017. +Translated to Classical B manually +*/ MACHINE Ref5_Switch SETS /* enumerated */ DOOR_STATE={open,closed,door_moving}; diff --git a/src/test/resources/de/hhu/stups/codegenerator/RelLaws_BOOL1.mch b/src/test/resources/de/hhu/stups/codegenerator/RelLaws_BOOL1.mch index e578a57523c27d8ec740f98f789578f80bdc1217..3805d1aac23a310ea9f9b32de7a46409ba2006cb 100644 --- a/src/test/resources/de/hhu/stups/codegenerator/RelLaws_BOOL1.mch +++ b/src/test/resources/de/hhu/stups/codegenerator/RelLaws_BOOL1.mch @@ -1,3 +1,7 @@ +/* +From ProB Examples, originally used to test ProB, +rewritten for B2Program +*/ MACHINE RelLaws_BOOL1 // BOOL is BOOL /* This machine is intended so that you can check whether ProB deals diff --git a/src/test/resources/de/hhu/stups/codegenerator/SeqLaws.mch b/src/test/resources/de/hhu/stups/codegenerator/SeqLaws.mch index 90f4bde702b3eac779b44bf52ea40da4f897d955..b1edd4bd249144e3202526c000275f22063a9d4f 100644 --- a/src/test/resources/de/hhu/stups/codegenerator/SeqLaws.mch +++ b/src/test/resources/de/hhu/stups/codegenerator/SeqLaws.mch @@ -1,3 +1,7 @@ +/* +From ProB Examples, originally used to test ProB, +rewritten for B2Program +*/ MACHINE SeqLaws SETS setY = {y1,y2} diff --git a/src/test/resources/de/hhu/stups/codegenerator/SetLaws.mch b/src/test/resources/de/hhu/stups/codegenerator/SetLaws.mch index f22efe31bdafc55660269e83b070530d945faeeb..2f6d48c9d6d66191f6e75650387c4749ca548be5 100644 --- a/src/test/resources/de/hhu/stups/codegenerator/SetLaws.mch +++ b/src/test/resources/de/hhu/stups/codegenerator/SetLaws.mch @@ -1,4 +1,7 @@ - +/* +From ProB Examples, originally used to test ProB, +rewritten for B2Program +*/ MACHINE SetLaws SETS /* enumerated */ setX={el1,el2,el3} diff --git a/src/test/resources/de/hhu/stups/codegenerator/SetLawsNat.mch b/src/test/resources/de/hhu/stups/codegenerator/SetLawsNat.mch index 0e6b7e92afc927c5ac9f3ce9027a47dfaed127fa..f06e7cbaffa97287dcbbcf48dc3e07f254a0b1ad 100644 --- a/src/test/resources/de/hhu/stups/codegenerator/SetLawsNat.mch +++ b/src/test/resources/de/hhu/stups/codegenerator/SetLawsNat.mch @@ -1,3 +1,7 @@ +/* +From ProB Examples, originally used to test ProB, +rewritten for B2Program +*/ MACHINE SetLawsNat VARIABLES SS, TT, VV diff --git a/src/test/resources/de/hhu/stups/codegenerator/SetLawsNatural.mch b/src/test/resources/de/hhu/stups/codegenerator/SetLawsNatural.mch index e34107c16dabb0bf282ed223ac638be09fd33cd8..22a131133a6401d6908a19f7efd7c487026109c8 100644 --- a/src/test/resources/de/hhu/stups/codegenerator/SetLawsNatural.mch +++ b/src/test/resources/de/hhu/stups/codegenerator/SetLawsNatural.mch @@ -1,3 +1,7 @@ +/* +From ProB Examples, originally used to test ProB, +rewritten for B2Program +*/ MACHINE SetLawsNatural VARIABLES SS, TT, VV diff --git a/src/test/resources/de/hhu/stups/codegenerator/SetLawsPow.mch b/src/test/resources/de/hhu/stups/codegenerator/SetLawsPow.mch index 07f12a25d60e50728bacdc6729064987fbb49f66..fde22caa3f22f099f15387d532480d6c97c226f2 100644 --- a/src/test/resources/de/hhu/stups/codegenerator/SetLawsPow.mch +++ b/src/test/resources/de/hhu/stups/codegenerator/SetLawsPow.mch @@ -1,4 +1,7 @@ - +/* +From ProB Examples, originally used to test ProB, +rewritten for B2Program +*/ MACHINE SetLawsPow SETS /* enumerated */ elements={el1} diff --git a/src/test/resources/de/hhu/stups/codegenerator/SetLawsPow2.mch b/src/test/resources/de/hhu/stups/codegenerator/SetLawsPow2.mch index 0336934905a445505f0533446af5bb347b516ac7..48041f861d622b0a2064d1908e53861562c16551 100644 --- a/src/test/resources/de/hhu/stups/codegenerator/SetLawsPow2.mch +++ b/src/test/resources/de/hhu/stups/codegenerator/SetLawsPow2.mch @@ -1,4 +1,7 @@ - +/* +From ProB Examples, originally used to test ProB, +rewritten for B2Program +*/ MACHINE SetLawsPow2 SETS /* enumerated */ elements={el1,el2} diff --git a/src/test/resources/de/hhu/stups/codegenerator/SetLawsPowPow.mch b/src/test/resources/de/hhu/stups/codegenerator/SetLawsPowPow.mch index 5fdde3a1bd26b0cb6c4ef5cee09a9f35c84acdfd..bbbd7ad206e7e3ade2e42bdf3e38011df9e34028 100644 --- a/src/test/resources/de/hhu/stups/codegenerator/SetLawsPowPow.mch +++ b/src/test/resources/de/hhu/stups/codegenerator/SetLawsPowPow.mch @@ -1,4 +1,7 @@ - +/* +From ProB Examples, originally used to test ProB, +rewritten for B2Program +*/ MACHINE SetLawsPowPow SETS /* enumerated */ elements={el1} diff --git a/src/test/resources/de/hhu/stups/codegenerator/SetLawsPowPowCart.mch b/src/test/resources/de/hhu/stups/codegenerator/SetLawsPowPowCart.mch index 82b5eda853f2b896092bb3d9eec30bc06b889bec..81e80769aabed429a428918ba4425a05c254b70f 100644 --- a/src/test/resources/de/hhu/stups/codegenerator/SetLawsPowPowCart.mch +++ b/src/test/resources/de/hhu/stups/codegenerator/SetLawsPowPowCart.mch @@ -1,4 +1,7 @@ - +/* +From ProB Examples, originally used to test ProB, +rewritten for B2Program +*/ MACHINE SetLawsPowPowCart SETS /* enumerated */ elements={el1} diff --git a/src/test/resources/de/hhu/stups/codegenerator/SetRelLaws_NatBool.mch b/src/test/resources/de/hhu/stups/codegenerator/SetRelLaws_NatBool.mch index 7b1f003f0533cac98a4957174fadda3bb8319683..67e31e66d67c90e84dc2f68d673943e21e541e34 100644 --- a/src/test/resources/de/hhu/stups/codegenerator/SetRelLaws_NatBool.mch +++ b/src/test/resources/de/hhu/stups/codegenerator/SetRelLaws_NatBool.mch @@ -1,3 +1,7 @@ +/* +From ProB Examples, originally used to test ProB, +rewritten for B2Program +*/ MACHINE SetRelLaws_NatBool /* SETS diff --git a/src/test/resources/de/hhu/stups/codegenerator/SetRelationConstructs.mch b/src/test/resources/de/hhu/stups/codegenerator/SetRelationConstructs.mch index c82b411c51d806c0154f827406c8b6f9fa8edf66..2da5f835f371ba999532571990366250b54ba393 100644 --- a/src/test/resources/de/hhu/stups/codegenerator/SetRelationConstructs.mch +++ b/src/test/resources/de/hhu/stups/codegenerator/SetRelationConstructs.mch @@ -1,3 +1,6 @@ +/* +From ProB Examples, originally used to test ProB +*/ MACHINE SetRelationConstructs VARIABLES basea, a, baseb, b, basec, c INVARIANT diff --git a/src/test/resources/de/hhu/stups/codegenerator/Sieve.mch b/src/test/resources/de/hhu/stups/codegenerator/Sieve.mch index d38d5da3cf4379f155cf577f8db1bde578c0fc42..e9e61da67e1b6090c007ccf1f0875a24733ee115 100644 --- a/src/test/resources/de/hhu/stups/codegenerator/Sieve.mch +++ b/src/test/resources/de/hhu/stups/codegenerator/Sieve.mch @@ -1,3 +1,6 @@ +/* +Written by Michael Leuschel +*/ MACHINE Sieve VARIABLES numbers,cur, limit INVARIANT diff --git a/src/test/resources/de/hhu/stups/codegenerator/SieveParallel.mch b/src/test/resources/de/hhu/stups/codegenerator/SieveParallel.mch index 83c126dd7866836df1a9eefe23413adb7df51816..afb9e49b48eef9ebe577c9e712e3475d71109f31 100644 --- a/src/test/resources/de/hhu/stups/codegenerator/SieveParallel.mch +++ b/src/test/resources/de/hhu/stups/codegenerator/SieveParallel.mch @@ -1,3 +1,6 @@ +/* +Written by Michael Leuschel +*/ MACHINE SieveParallel VARIABLES numbers,cur, limit INVARIANT diff --git a/src/test/resources/de/hhu/stups/codegenerator/Simpson_Four_Slot.mch b/src/test/resources/de/hhu/stups/codegenerator/Simpson_Four_Slot.mch index ea04239f94748a1d5c43037c8a18dc4259b9bf3e..9b98ace546d011f9e7fb025cd7af3c58ebf8324b 100644 --- a/src/test/resources/de/hhu/stups/codegenerator/Simpson_Four_Slot.mch +++ b/src/test/resources/de/hhu/stups/codegenerator/Simpson_Four_Slot.mch @@ -1,3 +1,6 @@ +/* +Model of Simpson's four slot algorithm +*/ MACHINE Simpson_Four_Slot SETS INDEX = {p0,p1,s0,s1}; diff --git a/src/test/resources/de/hhu/stups/codegenerator/nota.mch b/src/test/resources/de/hhu/stups/codegenerator/nota.mch index abd49c52f4e5f25ae8033d385e8ef444848f952b..49c9c47e0668dab14e5dd29c11238cf57815984b 100755 --- a/src/test/resources/de/hhu/stups/codegenerator/nota.mch +++ b/src/test/resources/de/hhu/stups/codegenerator/nota.mch @@ -1,3 +1,6 @@ +/* +I. Oliver. Experiences in Using B and UML in Industrial Development. In Proceedings Formal Specification and Development in B, B’07, page 248–251, 2007. +*/ MACHINE nota /* these represent the classes */ diff --git a/src/test/resources/de/hhu/stups/codegenerator/nota_v2.mch b/src/test/resources/de/hhu/stups/codegenerator/nota_v2.mch index 62b04c894ec187289c298f92c2828edf0ad21a2c..6d9a121751c39ec366061c6953c48d14d82cddd3 100644 --- a/src/test/resources/de/hhu/stups/codegenerator/nota_v2.mch +++ b/src/test/resources/de/hhu/stups/codegenerator/nota_v2.mch @@ -1,3 +1,7 @@ +/* +I. Oliver. Experiences in Using B and UML in Industrial Development. In Proceedings Formal Specification and Development in B, B’07, page 248–251, 2007. +Simplified version for B2Program +*/ MACHINE nota_v2 // a simplified version of nota for B2Program diff --git a/src/test/resources/de/hhu/stups/codegenerator/prob_oneway8seq.mch b/src/test/resources/de/hhu/stups/codegenerator/prob_oneway8seq.mch index 1e38e37cafba21d979201aa2ff2e1c50b17fd2e5..0de14d3d82535caaba557e5f870e12ec60dc1b28 100644 --- a/src/test/resources/de/hhu/stups/codegenerator/prob_oneway8seq.mch +++ b/src/test/resources/de/hhu/stups/codegenerator/prob_oneway8seq.mch @@ -1,6 +1,8 @@ /* https://www3.hhu.de/stups/prob/index.php/Summary_of_B_Syntax */ /* Model from https://mars-workshop.org/repository/020-CBTC.html */ - +/* +F. Mazzanti and A. Ferrari. Ten diverse formal models for a cbtc automatic train supervision system. Electronic Proceedings in Theoretical Computer Science, 268:104–149, Mar. 2018. +*/ MACHINE prob_oneway8seq DEFINITIONS diff --git a/src/test/resources/de/hhu/stups/codegenerator/scheduler.mch b/src/test/resources/de/hhu/stups/codegenerator/scheduler.mch index 84f5f3593d45ef710782a59fd163b11c20a47765..dbf71c9a608f7c8325b37ba8837ce20e58d90ad6 100644 --- a/src/test/resources/de/hhu/stups/codegenerator/scheduler.mch +++ b/src/test/resources/de/hhu/stups/codegenerator/scheduler.mch @@ -1,3 +1,6 @@ +/* +From ProB examples +*/ MACHINE scheduler SETS