From 654afb331d3ceb7cb5a2ff13bd3186217a506b27 Mon Sep 17 00:00:00 2001
From: Fabian Vu <Fabian.Vu@hhu.de>
Date: Sun, 24 Nov 2024 21:04:48 +0100
Subject: [PATCH] Update information

---
 visualizations/LandingGear/GearsDoors/LandingGear_R6.mch    | 6 ++++++
 visualizations/LandingGear/GearsDoors/physical.svg          | 1 +
 .../LandingGear/HydraulicCircuit/LandingGear_R6.mch         | 6 ++++++
 .../LandingGear/HydraulicCircuit/architecture.svg           | 1 +
 visualizations/LandingGear/HydraulicCircuit/physical.svg    | 1 +
 visualizations/LightModel/BlinkLamps_v3.mch                 | 4 ++++
 visualizations/LightModel/GenericTimersMC.mch               | 4 ++++
 visualizations/LightModel/PitmanController_TIME_MC_v4.mch   | 4 ++++
 visualizations/LightModel/Sensors.mch                       | 4 ++++
 9 files changed, 31 insertions(+)

diff --git a/visualizations/LandingGear/GearsDoors/LandingGear_R6.mch b/visualizations/LandingGear/GearsDoors/LandingGear_R6.mch
index 72bd1819e..0c757ca06 100644
--- a/visualizations/LandingGear/GearsDoors/LandingGear_R6.mch
+++ b/visualizations/LandingGear/GearsDoors/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/visualizations/LandingGear/GearsDoors/physical.svg b/visualizations/LandingGear/GearsDoors/physical.svg
index 6b9a224c0..15b5728d1 100644
--- a/visualizations/LandingGear/GearsDoors/physical.svg
+++ b/visualizations/LandingGear/GearsDoors/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/visualizations/LandingGear/HydraulicCircuit/LandingGear_R6.mch b/visualizations/LandingGear/HydraulicCircuit/LandingGear_R6.mch
index 72bd1819e..0c757ca06 100644
--- a/visualizations/LandingGear/HydraulicCircuit/LandingGear_R6.mch
+++ b/visualizations/LandingGear/HydraulicCircuit/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/visualizations/LandingGear/HydraulicCircuit/architecture.svg b/visualizations/LandingGear/HydraulicCircuit/architecture.svg
index 81bba719c..66c9f0ca8 100644
--- a/visualizations/LandingGear/HydraulicCircuit/architecture.svg
+++ b/visualizations/LandingGear/HydraulicCircuit/architecture.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. !-->
 <?xml-stylesheet href="landinggear.css" type="text/css"?>
 
 <svg width="947" height="728" xmlns="http://www.w3.org/2000/svg" id="landinggear" xmlns:xlink="http://www.w3.org/1999/xlink">
diff --git a/visualizations/LandingGear/HydraulicCircuit/physical.svg b/visualizations/LandingGear/HydraulicCircuit/physical.svg
index 6b9a224c0..15b5728d1 100644
--- a/visualizations/LandingGear/HydraulicCircuit/physical.svg
+++ b/visualizations/LandingGear/HydraulicCircuit/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/visualizations/LightModel/BlinkLamps_v3.mch b/visualizations/LightModel/BlinkLamps_v3.mch
index 78ad6fc06..a3efb1a4a 100644
--- a/visualizations/LightModel/BlinkLamps_v3.mch
+++ b/visualizations/LightModel/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/visualizations/LightModel/GenericTimersMC.mch b/visualizations/LightModel/GenericTimersMC.mch
index 80cb34ee6..35ded86c5 100644
--- a/visualizations/LightModel/GenericTimersMC.mch
+++ b/visualizations/LightModel/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/visualizations/LightModel/PitmanController_TIME_MC_v4.mch b/visualizations/LightModel/PitmanController_TIME_MC_v4.mch
index bc7ab486d..3192f969d 100644
--- a/visualizations/LightModel/PitmanController_TIME_MC_v4.mch
+++ b/visualizations/LightModel/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/visualizations/LightModel/Sensors.mch b/visualizations/LightModel/Sensors.mch
index 1b3342e7a..007a51f8a 100644
--- a/visualizations/LightModel/Sensors.mch
+++ b/visualizations/LightModel/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
-- 
GitLab