diff --git a/src/test/resources/de/hhu/stups/codegenerator/ArithmeticExpLaws.mch b/src/test/resources/de/hhu/stups/codegenerator/ArithmeticExpLaws.mch
index d16ab4a6991c07a1a47831857f11b6df8268ca52..5d45942edfe70b75acc2b44bc26d1406b00f7201 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/ArithmeticExpLaws.mch
+++ b/src/test/resources/de/hhu/stups/codegenerator/ArithmeticExpLaws.mch
@@ -1,3 +1,7 @@
+/*
+From ProB Examples, originally used to test ProB,
+rewritten for B2Program
+*/
MACHINE ArithmeticExpLaws
// some specific laws about exponentiation
// kept separate from other laws because of CLP(FD) overflow issues
diff --git a/src/test/resources/de/hhu/stups/codegenerator/ArithmeticLaws.mch b/src/test/resources/de/hhu/stups/codegenerator/ArithmeticLaws.mch
index 25a1ec2e96eb58e178bb93a7dcb1c6b55e58bfc9..afa6b8c6c4c73aba681f1605c66f233e1bb507b1 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/ArithmeticLaws.mch
+++ b/src/test/resources/de/hhu/stups/codegenerator/ArithmeticLaws.mch
@@ -1,4 +1,7 @@
-
+/*
+From ProB Examples, originally used to test ProB,
+rewritten for B2Program
+*/
MACHINE ArithmeticLaws
ABSTRACT_VARIABLES
x,
diff --git a/src/test/resources/de/hhu/stups/codegenerator/Bakery0.mch b/src/test/resources/de/hhu/stups/codegenerator/Bakery0.mch
index cbcf70ae33aefd5fc3500128a59704f33dd58751..26adc5f92d9841c1fa3eb562de2d0b725039cf06 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/Bakery0.mch
+++ b/src/test/resources/de/hhu/stups/codegenerator/Bakery0.mch
@@ -1,3 +1,6 @@
+/*
+From ProB Examples
+*/
MACHINE Bakery0
VARIABLES aa
diff --git a/src/test/resources/de/hhu/stups/codegenerator/BoolLaws.mch b/src/test/resources/de/hhu/stups/codegenerator/BoolLaws.mch
index f7628abc487ddf422c4bc3ec563e5d5d39cef381..8cf511b424ef1a714ede8fb2fbe74a0f6e97d414 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/BoolLaws.mch
+++ b/src/test/resources/de/hhu/stups/codegenerator/BoolLaws.mch
@@ -1,3 +1,7 @@
+/*
+From ProB Examples, originally used to test ProB,
+rewritten for B2Program
+*/
MACHINE BoolLaws
CONSTANTS
TT,FF
diff --git a/src/test/resources/de/hhu/stups/codegenerator/BoolLaws_SetCompr.mch b/src/test/resources/de/hhu/stups/codegenerator/BoolLaws_SetCompr.mch
index a2240f792372b3a09eb0d6e84a220288f0dad630..721902d3711932a552651e12436b1f9d9e5dfa25 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/BoolLaws_SetCompr.mch
+++ b/src/test/resources/de/hhu/stups/codegenerator/BoolLaws_SetCompr.mch
@@ -1,3 +1,7 @@
+/*
+From ProB Examples, originally used to test ProB,
+rewritten for B2Program
+*/
MACHINE BoolLaws_SetCompr
/* Boolean Laws expressed using set comprehensions */
CONSTANTS
diff --git a/src/test/resources/de/hhu/stups/codegenerator/BoolWithArithLaws.mch b/src/test/resources/de/hhu/stups/codegenerator/BoolWithArithLaws.mch
index bd0d86d2019979c0c3f2afc0b6b58e06362bcfd4..fd5dd768abd36159088ca387532b6c432a78cb37 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/BoolWithArithLaws.mch
+++ b/src/test/resources/de/hhu/stups/codegenerator/BoolWithArithLaws.mch
@@ -1,4 +1,6 @@
-
+/*
+From ProB Examples, originally used to test ProB
+*/
MACHINE BoolWithArithLaws
/* ada(x>2)ed version of BoolLaws, to check b_interpreter_check, which
has a special (1<=1)eatment for arithmetic operators */
diff --git a/src/test/resources/de/hhu/stups/codegenerator/CAN_BUS_tlc.mch b/src/test/resources/de/hhu/stups/codegenerator/CAN_BUS_tlc.mch
index 515fba702b65f99665dd020b4e93057b90c86fe2..a26e163f370a96da624c232f53f114d8199f080c 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/CAN_BUS_tlc.mch
+++ b/src/test/resources/de/hhu/stups/codegenerator/CAN_BUS_tlc.mch
@@ -1,3 +1,6 @@
+/*
+Developed by J.Colley
+*/
MACHINE CAN_BUS_tlc
SETS
diff --git a/src/test/resources/de/hhu/stups/codegenerator/EqualityLaws.mch b/src/test/resources/de/hhu/stups/codegenerator/EqualityLaws.mch
index c4d44b2fba6d10fde02736b93995dda5ecf64ce6..4fbae5acdecf23eaecff1a48158994ca5842e8ab 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/EqualityLaws.mch
+++ b/src/test/resources/de/hhu/stups/codegenerator/EqualityLaws.mch
@@ -1,4 +1,8 @@
-MACHINE EqualityLaws // rewritten from prob_examples for b2program
+/*
+From ProB Examples, originally used to test ProB,
+rewritten for B2Program
+*/
+MACHINE EqualityLaws
SETS
ID={i1,i2,i3}
VARIABLES a,b,c, s1, d,e
diff --git a/src/test/resources/de/hhu/stups/codegenerator/ExplicitChecks.mch b/src/test/resources/de/hhu/stups/codegenerator/ExplicitChecks.mch
index 336fbcda26d5fc8a9d1eda845bc409ed32e83ca0..45e6dd5cd3244000b576692942183e3ddaf11f28 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/ExplicitChecks.mch
+++ b/src/test/resources/de/hhu/stups/codegenerator/ExplicitChecks.mch
@@ -1,3 +1,7 @@
+/*
+From ProB Examples, originally used to test ProB,
+rewritten for B2Program
+*/
MACHINE ExplicitChecks
VARIABLES
x
diff --git a/src/test/resources/de/hhu/stups/codegenerator/ExplicitChecks_Old.mch b/src/test/resources/de/hhu/stups/codegenerator/ExplicitChecks_Old.mch
index 1052fe81a7da09a52f2879e782be4aa52de7c34c..39db8701e52259b8a35bc6fc558037b7a9e7bde5 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/ExplicitChecks_Old.mch
+++ b/src/test/resources/de/hhu/stups/codegenerator/ExplicitChecks_Old.mch
@@ -1,3 +1,7 @@
+/*
+From ProB Examples, originally used to test ProB,
+rewritten for B2Program
+*/
MACHINE ExplicitChecks_Old
VARIABLES
x
diff --git a/src/test/resources/de/hhu/stups/codegenerator/ExplicitComputations.mch b/src/test/resources/de/hhu/stups/codegenerator/ExplicitComputations.mch
index 0845b51d4ced0382b14c7d8213df88a841b1021a..b80c461ff44de9495574aa33b853f041b7aa27c3 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/ExplicitComputations.mch
+++ b/src/test/resources/de/hhu/stups/codegenerator/ExplicitComputations.mch
@@ -1,3 +1,7 @@
+/*
+From ProB Examples, originally used to test ProB,
+rewritten for B2Program
+*/
MACHINE ExplicitComputations
/* A machine with some explicitly given results for certain computations */
SETS
diff --git a/src/test/resources/de/hhu/stups/codegenerator/ExplicitComputations2.mch b/src/test/resources/de/hhu/stups/codegenerator/ExplicitComputations2.mch
index 0ed5c3949d993c7bf6234fa7329fcd399682785c..b6d9c5cac86b09e7dc738affb5781d4ea1f62908 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/ExplicitComputations2.mch
+++ b/src/test/resources/de/hhu/stups/codegenerator/ExplicitComputations2.mch
@@ -1,3 +1,7 @@
+/*
+From ProB Examples, originally used to test ProB,
+rewritten for B2Program
+*/
MACHINE ExplicitComputations2
/* A machine with some explicitly given results for certain computations */
SETS
diff --git a/src/test/resources/de/hhu/stups/codegenerator/FunLaws.mch b/src/test/resources/de/hhu/stups/codegenerator/FunLaws.mch
index d2818eccbc93981eb698ad8b8c185138415797d4..2c668d083e3012d2f19691d62e9b9737dc922b99 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/FunLaws.mch
+++ b/src/test/resources/de/hhu/stups/codegenerator/FunLaws.mch
@@ -1,3 +1,7 @@
+/*
+From ProB Examples, originally used to test ProB,
+rewritten for B2Program
+*/
MACHINE FunLaws
/* This machine is intended so that you can check whether ProB deals
with basic laws associated to functions and relations. ProB should
@@ -164,14 +168,14 @@ INVARIANT
( card(setX <| ff) <= card(ff) & card(setX <<| ff) <= card(ff)) &
( ff: SETX +-> SETY => card(setX <<| ff) >= card(ff)-card(setX)) &
/* TO DO: more rules about |> , |>>, <|, <<| */
-
+
/* functionality propagation laws */
( ff: setX >+> setY => ff~: setY +-> setX) &
- ( ff: SETX +-> SETY => setX <| ff: setX +-> SETY) &
- ( ff: SETX +-> SETY => setX <<| ff: (SETX-setX) +-> SETY) &
- ( ff: SETX +-> SETY => ff |> setY : SETX +-> setY) &
- ( ff: SETX +-> SETY => ff |>> setY : SETX +-> (SETY-setY)) &
+ ( ff: SETX +-> SETY => setX <| ff: setX +-> SETY) &
+ ( ff: SETX +-> SETY => setX <<| ff: (SETX-setX) +-> SETY) &
+ ( ff: SETX +-> SETY => ff |> setY : SETX +-> setY) &
+ ( ff: SETX +-> SETY => ff |>> setY : SETX +-> (SETY-setY)) &
( ff: SETX +-> SETY & gg: SETX +-> SETY => ff <+ gg : SETX +-> SETY) &
/* TO DO: injectivitiy propagation laws */
@@ -182,7 +186,7 @@ INVARIANT
!x.(x:(ff/\gg) => (x:ff & x:gg)) &
!(x,y).(x:setX & y : setY & x|->y:ff => y: ff[setX]) &
/* TO DO: add more */
-
+
/* ran, dom propagation laws */
/* some laws already above, law1 .. la26: dom(ff \/ gg) = dom(ff) \/ dom(gg) etc */
dom(setX <| ff) = dom(ff) /\ setX &
@@ -195,11 +199,11 @@ INVARIANT
dom(ff |>> setY) <: dom(ff) &
dom(ff<+gg) = dom(ff) \/ dom(gg) &
ran(gg) <: ran(ff<+gg) &
-
-
+
+
/* some new laws */
- ( ff: SETX +-> SETY => !x.(x:dom(ff) => ff(x):ran(ff)))
-
+ ( ff: SETX +-> SETY => !x.(x:dom(ff) => ff(x):ran(ff)))
+
&
(ff |> setY = ff |>> (SETY - setY)) &
(ff |>> setY = ff |> (SETY - setY)) &
@@ -226,7 +230,7 @@ INVARIANT
//gg |> ran(ff) = {a,b| (a,b):gg & b:ran(ff)} &
//dom(ff) <<| gg = {a,b| (a,b):gg & a/:dom(ff)} &
//gg |>> ran(ff) = {a,b| (a,b):gg & b/:ran(ff)} &
-
+
/* Definitions from page 80 of B-Book */
ff[dom(gg)] = ran(dom(gg) <| ff) & /* p[w] = ran(w <| p) with w=dom(gg) */
gg <+ ff = (dom(ff) <<| gg) \/ ff & /* q<+ r = ... in book, error in book p should be r */
@@ -234,13 +238,13 @@ INVARIANT
//prj1(setX,setY) = (id(setX) >< (setX * setY))~ &
//prj2(setX,setY) = ((setY*setX) >< id(setY))~ & // Not supported for C++ code gen
//(ff||gg) = (prj1(SETX,SETX);ff) >< (prj2(SETX,SETX);gg) &// Not supported for C++ code gen
-
+
//ff[dom(gg)] = {b| #a.(a:dom(gg) & (a,b):ff)} & /* again error in B-Book (a,b) instead of (x,y) */
//gg <+ ff = {a,b | ( (a,b):gg & a/:dom(ff) ) or (a,b):ff} &
//prj1(setX,setY) = {a,b,c| (a,b,c) : setX*setY*setX & c=a} &
//prj2(setX,setY) = {a,b,c| (a,b,c) : setX*setY*setY & c=b} &
//(ff||gg) = {ab,cd | #(a,b,c,d).(ab=(a,b) & cd = (c,d) & (a,c):ff & (b,d):gg)} &
-
+
/* Inclusion Properties from page 98 of B-Book (not complete) */
id(dom(ff)) <: (ff; ff~) &
id(ran(ff)) <: (ff~;ff) &
@@ -252,7 +256,7 @@ INVARIANT
ran(ff) - ran(gg) <: ran(ff-gg) &
(ff /\ gg)[setX] <: ff[setX] /\ gg[setX] &
ff[setX] - gg[setX] <: (ff-gg) [setX] &
-
+
/* Inverse Properties from page 100 of B-Book */
(ff~)~ = ff &
(ff ; (gg~))~ = ((gg~)~ ; ff~) &
@@ -269,7 +273,7 @@ INVARIANT
{1|->2}~ = {2|->1} &
(ff={} => ff~={}) &
//(setX * setY)~ = setY*setX &
-
+
/* Domain Properties from pages 100-101 of B-Book */
(ff: setX --> SETY => (dom(ff) = setX)) &
dom(ff~) = ran(ff) &
@@ -284,7 +288,7 @@ INVARIANT
//dom(ff><gg) = dom(ff) /\ dom(gg) & // Not supported for C++ code gen
//dom(ff||gg) = dom(ff) * dom(gg) &
dom(ff \/ gg) = dom(ff) \/ dom(gg) &
- (ff:SETX +-> SETY & gg:SETX +-> SETY &
+ (ff:SETX +-> SETY & gg:SETX +-> SETY &
dom(ff) <| gg = dom(gg) <| ff
=> (dom(ff /\ gg) = dom(ff) /\ dom(gg) &
dom(ff - gg) = dom(ff) - dom(gg))
@@ -292,7 +296,7 @@ INVARIANT
dom({ 1|-> 2}) = {1} &
(ff={} => dom(ff) = {}) &
(setY /= {} => dom(setX*setY) = setX) &
-
+
/* Range Properties from pages 102-103 of B-Book */
(ff: SETX +->> setY => (ran(ff) = setY)) &
ran(ff~) = dom(ff) &
@@ -307,7 +311,7 @@ INVARIANT
//ran(ff><gg) = (ff~ ; gg) & // Not supported for C++ code gen
//ran(ff||gg) = ran(ff)*ran(gg) &
ran(ff \/ gg) = ran(ff) \/ ran(gg) &
- (ff~:SETY +-> SETX & gg~:SETY +-> SETX &
+ (ff~:SETY +-> SETX & gg~:SETY +-> SETX &
ff |> ran(gg) = gg |> ran(ff)
=> (ran(ff /\ gg) = ran(ff) /\ ran(gg) &
ran(ff - gg) = ran(ff) - ran(gg))) &
diff --git a/src/test/resources/de/hhu/stups/codegenerator/GCD.mch b/src/test/resources/de/hhu/stups/codegenerator/GCD.mch
index 4078dcfb15276e46863009983bf4f689f0736e31..c042f61f2949c86e9bfc38b419272f34bb889955 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/GCD.mch
+++ b/src/test/resources/de/hhu/stups/codegenerator/GCD.mch
@@ -1,3 +1,6 @@
+/*
+From ProB Examples
+*/
MACHINE GCD
VARIABLES x,y
INVARIANT
diff --git a/src/test/resources/de/hhu/stups/codegenerator/blackbox/HighwayEnvironment.mch b/src/test/resources/de/hhu/stups/codegenerator/blackbox/HighwayEnvironment.mch
index 785216594d434332ade18b988a14c24e5e428091..98f7f306c7288387c7529d7f0115a6c45168ee92 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/blackbox/HighwayEnvironment.mch
+++ b/src/test/resources/de/hhu/stups/codegenerator/blackbox/HighwayEnvironment.mch
@@ -1,3 +1,6 @@
+/*
+Developed by Fabian Vu for Open AI Environment
+*/
MACHINE HighwayEnvironment
SETS
diff --git a/src/test/resources/de/hhu/stups/codegenerator/blackbox/HighwayEnvironment2.mch b/src/test/resources/de/hhu/stups/codegenerator/blackbox/HighwayEnvironment2.mch
index 11e18f62d290234f8f72754faf8d3a7b760ddea9..5e6739670a569e11840a5d7a8f524f073472491a 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/blackbox/HighwayEnvironment2.mch
+++ b/src/test/resources/de/hhu/stups/codegenerator/blackbox/HighwayEnvironment2.mch
@@ -1,3 +1,6 @@
+/*
+Developed by Fabian Vu for Open AI Environment
+*/
MACHINE HighwayEnvironment2
SETS
diff --git a/src/test/resources/de/hhu/stups/codegenerator/blackbox/LunarLander.mch b/src/test/resources/de/hhu/stups/codegenerator/blackbox/LunarLander.mch
index 143613293007d09a88bbe83bcbe69c6b1924e36e..4c31b0fac58a66cf42cb2feb87b3d001e187d297 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/blackbox/LunarLander.mch
+++ b/src/test/resources/de/hhu/stups/codegenerator/blackbox/LunarLander.mch
@@ -1,3 +1,6 @@
+/*
+Developed by Fabian Vu for OpenAI Environment
+*/
MACHINE LunarLander
VARIABLES x, y, v_x, v_y, angle, v_angular, left_leg_on_ground, right_leg_on_ground
diff --git a/src/test/resources/de/hhu/stups/codegenerator/landing_gear/LandingGear_R6.mch b/src/test/resources/de/hhu/stups/codegenerator/landing_gear/LandingGear_R6.mch
index 72bd1819e166f1370614ab88f8b30a4c1927338b..0c757ca067c37034036d77d487566ccae7b49376 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/landing_gear/LandingGear_R6.mch
+++ b/src/test/resources/de/hhu/stups/codegenerator/landing_gear/LandingGear_R6.mch
@@ -1,3 +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 LandingGear_R6
SETS /* enumerated */
DOOR_STATE={open,closed,door_moving};
diff --git a/src/test/resources/de/hhu/stups/codegenerator/landing_gear/architecture.svg b/src/test/resources/de/hhu/stups/codegenerator/landing_gear/architecture.svg
index 81bba719c8c6819b864376d7f6a1046752211c32..415a3c1ddb5c4bd0f18cecc4113f4bfe281a1e0a 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/landing_gear/architecture.svg
+++ b/src/test/resources/de/hhu/stups/codegenerator/landing_gear/architecture.svg
@@ -1,5 +1,5 @@
<?xml-stylesheet href="landinggear.css" type="text/css"?>
-
+<!-- From 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. !-->
<svg width="947" height="728" xmlns="http://www.w3.org/2000/svg" id="landinggear" xmlns:xlink="http://www.w3.org/1999/xlink">
<metadata id="metadata3467">image/svg+xml</metadata>
diff --git a/src/test/resources/de/hhu/stups/codegenerator/landing_gear/physical.svg b/src/test/resources/de/hhu/stups/codegenerator/landing_gear/physical.svg
index 6b9a224c00c47cd67d52084428ed6287e5f958ac..15b5728d1bab0cc8d050c9d3eff066f1ee1df432 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/landing_gear/physical.svg
+++ b/src/test/resources/de/hhu/stups/codegenerator/landing_gear/physical.svg
@@ -1,3 +1,4 @@
+<!-- From 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. !-->
<svg width="947" height="728" xmlns="http://www.w3.org/2000/svg" id="landinggear" xmlns:xlink="http://www.w3.org/1999/xlink">
<metadata id="metadata3467">image/svg+xml</metadata>
diff --git a/src/test/resources/de/hhu/stups/codegenerator/sievebenchmarks/Sieve.mch b/src/test/resources/de/hhu/stups/codegenerator/sievebenchmarks/Sieve.mch
index 5ebd5b1327a2370b659f5b62ff3f926571a91b82..2b6beda57f949b40e88741edba0be11639b6f0cd 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/sievebenchmarks/Sieve.mch
+++ b/src/test/resources/de/hhu/stups/codegenerator/sievebenchmarks/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/visualisation/BlinkLamps_v3.mch b/src/test/resources/de/hhu/stups/codegenerator/visualisation/BlinkLamps_v3.mch
index 78ad6fc069a5c106451640dfd93ee5dee8866a22..a3efb1a4a7982750f9f367339251323b556c409d 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/visualisation/BlinkLamps_v3.mch
+++ b/src/test/resources/de/hhu/stups/codegenerator/visualisation/BlinkLamps_v3.mch
@@ -1,3 +1,7 @@
+/*
+Formal Model and VisB Visualization from
+M. Leuschel, M. Mutz, and M. Werth. Modelling and Validating an Automotive System in Classical B and Event-B. In Proceedings ABZ, LNCS 12071, pages 335–350, 2020.
+*/
MACHINE BlinkLamps_v3
// Manage Blinking Lights Actuators (blinkLeft, blinkRight)
// and manage timing cycles
diff --git a/src/test/resources/de/hhu/stups/codegenerator/visualisation/GenericTimersMC.mch b/src/test/resources/de/hhu/stups/codegenerator/visualisation/GenericTimersMC.mch
index 80cb34ee6e39fa2c24e7c861f016a4b06508eb8f..35ded86c5c2ab5403f46959ef8f44961603c11cc 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/visualisation/GenericTimersMC.mch
+++ b/src/test/resources/de/hhu/stups/codegenerator/visualisation/GenericTimersMC.mch
@@ -1,3 +1,7 @@
+/*
+Formal Model and VisB Visualization from
+M. Leuschel, M. Mutz, and M. Werth. Modelling and Validating an Automotive System in Classical B and Event-B. In Proceedings ABZ, LNCS 12071, pages 335–350, 2020.
+*/
MACHINE GenericTimersMC
SETS TIMERS = {blink_deadline, tip_deadline}
diff --git a/src/test/resources/de/hhu/stups/codegenerator/visualisation/Lift.mch b/src/test/resources/de/hhu/stups/codegenerator/visualisation/Lift.mch
index 1f67802f192388d44614bf194a992e5b3f8f73e7..d0eef20cbd3ffe2f1d077b8c24130e5b2d025113 100755
--- a/src/test/resources/de/hhu/stups/codegenerator/visualisation/Lift.mch
+++ b/src/test/resources/de/hhu/stups/codegenerator/visualisation/Lift.mch
@@ -1,3 +1,6 @@
+/*
+From ProB Examples
+*/
MACHINE Lift
/* A simple model of a lift without a controller; The controller
will be added in a refinement (by refining the lift moving operations) or
diff --git a/src/test/resources/de/hhu/stups/codegenerator/visualisation/PitmanController_TIME_MC_v4.mch b/src/test/resources/de/hhu/stups/codegenerator/visualisation/PitmanController_TIME_MC_v4.mch
index ec414ba4488245d3eae9bcb9759839ac5cb65f50..02367bae4c4cf3aff2cfcafe40478363504fc0bf 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/visualisation/PitmanController_TIME_MC_v4.mch
+++ b/src/test/resources/de/hhu/stups/codegenerator/visualisation/PitmanController_TIME_MC_v4.mch
@@ -1,3 +1,7 @@
+/*
+Formal Model and VisB Visualization from
+M. Leuschel, M. Mutz, and M. Werth. Modelling and Validating an Automotive System in Classical B and Event-B. In Proceedings ABZ, LNCS 12071, pages 335–350, 2020.
+*/
MACHINE PitmanController_TIME_MC_v4
INCLUDES BlinkLamps_v3, Sensors, GenericTimersMC
diff --git a/src/test/resources/de/hhu/stups/codegenerator/visualisation/Sensors.mch b/src/test/resources/de/hhu/stups/codegenerator/visualisation/Sensors.mch
index 1b3342e7a1df7afc251865a4a2797ce5edeb4915..007a51f8accd9e08996da6e1756d6aeeec2d7629 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/visualisation/Sensors.mch
+++ b/src/test/resources/de/hhu/stups/codegenerator/visualisation/Sensors.mch
@@ -1,3 +1,7 @@
+/*
+Formal Model and VisB Visualization from
+M. Leuschel, M. Mutz, and M. Werth. Modelling and Validating an Automotive System in Classical B and Event-B. In Proceedings ABZ, LNCS 12071, pages 335–350, 2020.
+*/
MACHINE Sensors
/*
Sensors and sensor value updates
diff --git a/src/test/resources/de/hhu/stups/codegenerator/visualisation/TravelAgency.mch b/src/test/resources/de/hhu/stups/codegenerator/visualisation/TravelAgency.mch
index 0abaafa730e6e2d69c7f83ddc32be90ddf779c81..b9de871a2041f019992f962d902c62c89b41eeff 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/visualisation/TravelAgency.mch
+++ b/src/test/resources/de/hhu/stups/codegenerator/visualisation/TravelAgency.mch
@@ -1,3 +1,4 @@
+
MACHINE TravelAgency
/* contains an error that can be found by model checking */
/* machine developed by Carla Ferreira (the final machine contains no errors) */