From 213edbd2046277e8698299b5c92a8d0d2b23ad33 Mon Sep 17 00:00:00 2001
From: Fabian Vu <Fabian.Vu@hhu.de>
Date: Sun, 24 Nov 2024 20:43:52 +0100
Subject: [PATCH] Add more information on machines
---
.../resources/de/hhu/stups/codegenerator/Generated100.mch | 3 +++
.../resources/de/hhu/stups/codegenerator/INTEGERSET_Laws.mch | 4 ++++
.../codegenerator/IncrementalStatePackingTestLargeSlow.mch | 3 +++
.../codegenerator/IncrementalStatePackingTestLargeSlow2.mch | 3 +++
.../resources/de/hhu/stups/codegenerator/NatRangeLaws.mch | 4 ++++
.../resources/de/hhu/stups/codegenerator/Ref5_Switch.mch | 5 +++++
.../resources/de/hhu/stups/codegenerator/RelLaws_BOOL1.mch | 4 ++++
src/test/resources/de/hhu/stups/codegenerator/SeqLaws.mch | 4 ++++
src/test/resources/de/hhu/stups/codegenerator/SetLaws.mch | 5 ++++-
src/test/resources/de/hhu/stups/codegenerator/SetLawsNat.mch | 4 ++++
.../resources/de/hhu/stups/codegenerator/SetLawsNatural.mch | 4 ++++
src/test/resources/de/hhu/stups/codegenerator/SetLawsPow.mch | 5 ++++-
.../resources/de/hhu/stups/codegenerator/SetLawsPow2.mch | 5 ++++-
.../resources/de/hhu/stups/codegenerator/SetLawsPowPow.mch | 5 ++++-
.../de/hhu/stups/codegenerator/SetLawsPowPowCart.mch | 5 ++++-
.../de/hhu/stups/codegenerator/SetRelLaws_NatBool.mch | 4 ++++
.../de/hhu/stups/codegenerator/SetRelationConstructs.mch | 3 +++
src/test/resources/de/hhu/stups/codegenerator/Sieve.mch | 3 +++
.../resources/de/hhu/stups/codegenerator/SieveParallel.mch | 3 +++
.../de/hhu/stups/codegenerator/Simpson_Four_Slot.mch | 3 +++
src/test/resources/de/hhu/stups/codegenerator/nota.mch | 3 +++
src/test/resources/de/hhu/stups/codegenerator/nota_v2.mch | 4 ++++
.../resources/de/hhu/stups/codegenerator/prob_oneway8seq.mch | 4 +++-
src/test/resources/de/hhu/stups/codegenerator/scheduler.mch | 3 +++
24 files changed, 87 insertions(+), 6 deletions(-)
diff --git a/src/test/resources/de/hhu/stups/codegenerator/Generated100.mch b/src/test/resources/de/hhu/stups/codegenerator/Generated100.mch
index 4d782cc77..52c0f94db 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 eff993f40..75c6e21d0 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 c31ed8ae2..96975e52b 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 3bac7243a..ebd4c606e 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 0a110e423..9f99738b1 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 abd6e688f..5a52b76a8 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 e578a5752..3805d1aac 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 90f4bde70..b1edd4bd2 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 f22efe31b..2f6d48c9d 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 0e6b7e92a..f06e7cbaf 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 e34107c16..22a131133 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 07f12a25d..fde22caa3 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 033693490..48041f861 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 5fdde3a1b..bbbd7ad20 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 82b5eda85..81e80769a 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 7b1f003f0..67e31e66d 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 c82b411c5..2da5f835f 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 d38d5da3c..e9e61da67 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 83c126dd7..afb9e49b4 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 ea04239f9..9b98ace54 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 abd49c52f..49c9c47e0 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 62b04c894..6d9a12175 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 1e38e37ca..0de14d3d8 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 84f5f3593..dbf71c9a6 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
--
GitLab