From f1718240a2868ad4c186801a5a1889b8ca774e8c Mon Sep 17 00:00:00 2001
From: Fabian Vu <Fabian.Vu@hhu.de>
Date: Sun, 24 Nov 2024 20:38:13 +0100
Subject: [PATCH] Add information to machines
---
.../stups/codegenerator/ArithmeticExpLaws.mch | 4 ++
.../stups/codegenerator/ArithmeticLaws.mch | 5 ++-
.../de/hhu/stups/codegenerator/Bakery0.mch | 3 ++
.../de/hhu/stups/codegenerator/BoolLaws.mch | 4 ++
.../stups/codegenerator/BoolLaws_SetCompr.mch | 4 ++
.../stups/codegenerator/BoolWithArithLaws.mch | 4 +-
.../hhu/stups/codegenerator/CAN_BUS_tlc.mch | 3 ++
.../hhu/stups/codegenerator/EqualityLaws.mch | 6 ++-
.../stups/codegenerator/ExplicitChecks.mch | 4 ++
.../codegenerator/ExplicitChecks_Old.mch | 4 ++
.../codegenerator/ExplicitComputations.mch | 4 ++
.../codegenerator/ExplicitComputations2.mch | 4 ++
.../de/hhu/stups/codegenerator/FunLaws.mch | 40 ++++++++++---------
.../de/hhu/stups/codegenerator/GCD.mch | 3 ++
.../blackbox/HighwayEnvironment.mch | 3 ++
.../blackbox/HighwayEnvironment2.mch | 3 ++
.../codegenerator/blackbox/LunarLander.mch | 3 ++
.../landing_gear/LandingGear_R6.mch | 6 +++
.../landing_gear/architecture.svg | 2 +-
.../codegenerator/landing_gear/physical.svg | 1 +
.../codegenerator/sievebenchmarks/Sieve.mch | 3 ++
.../visualisation/BlinkLamps_v3.mch | 4 ++
.../visualisation/GenericTimersMC.mch | 4 ++
.../codegenerator/visualisation/Lift.mch | 3 ++
.../PitmanController_TIME_MC_v4.mch | 4 ++
.../codegenerator/visualisation/Sensors.mch | 4 ++
.../visualisation/TravelAgency.mch | 1 +
27 files changed, 111 insertions(+), 22 deletions(-)
diff --git a/src/test/resources/de/hhu/stups/codegenerator/ArithmeticExpLaws.mch b/src/test/resources/de/hhu/stups/codegenerator/ArithmeticExpLaws.mch
index d16ab4a69..5d45942ed 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 25a1ec2e9..afa6b8c6c 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 cbcf70ae3..26adc5f92 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 f7628abc4..8cf511b42 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 a2240f792..721902d37 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 bd0d86d20..fd5dd768a 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 515fba702..a26e163f3 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 c4d44b2fb..4fbae5acd 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 336fbcda2..45e6dd5cd 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 1052fe81a..39db8701e 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 0845b51d4..b80c461ff 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 0ed5c3949..b6d9c5cac 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 d2818eccb..2c668d083 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 4078dcfb1..c042f61f2 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 785216594..98f7f306c 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 11e18f62d..5e6739670 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 143613293..4c31b0fac 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 72bd1819e..0c757ca06 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 81bba719c..415a3c1dd 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 6b9a224c0..15b5728d1 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 5ebd5b132..2b6beda57 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 78ad6fc06..a3efb1a4a 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 80cb34ee6..35ded86c5 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 1f67802f1..d0eef20cb 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 ec414ba44..02367bae4 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 1b3342e7a..007a51f8a 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 0abaafa73..b9de871a2 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) */
--
GitLab