From d8512968fbe32e2acfc3e3b621da0dd72249448c Mon Sep 17 00:00:00 2001
From: Fabian Vu <Fabian.Vu@hhu.de>
Date: Sun, 24 Nov 2024 20:47:58 +0100
Subject: [PATCH] Add information on formal models

---
 .../de/hhu/stups/codegenerator/StringLaws.mch          |  4 ++++
 .../de/hhu/stups/codegenerator/SubstitutionLaws.mch    |  4 ++++
 .../de/hhu/stups/codegenerator/Train_1_beebook_TLC.mch |  6 ++++++
 .../codegenerator/Train_1_beebook_deterministic.mch    |  4 ++++
 .../codegenerator/Train_1_beebook_deterministic_MC.mch |  6 ++++++
 .../Train_1_beebook_deterministic_MC_POR.mch           |  6 ++++++
 .../Train_1_beebook_deterministic_MC_POR_v2.mch        |  7 +++++++
 .../Train_1_beebook_deterministic_MC_POR_v3.mch        | 10 +++++++++-
 .../de/hhu/stups/codegenerator/sort_m2_data1000.mch    |  4 ++++
 .../de/hhu/stups/codegenerator/sort_m2_data1000_MC.mch |  4 ++++
 .../resources/de/hhu/stups/codegenerator/tictac.mch    |  3 +++
 11 files changed, 57 insertions(+), 1 deletion(-)

diff --git a/src/test/resources/de/hhu/stups/codegenerator/StringLaws.mch b/src/test/resources/de/hhu/stups/codegenerator/StringLaws.mch
index 080563cfc..fed239107 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/StringLaws.mch
+++ b/src/test/resources/de/hhu/stups/codegenerator/StringLaws.mch
@@ -1,3 +1,7 @@
+/*
+From ProB Examples, originally used to test ProB,
+rewritten for B2Program
+*/
 MACHINE StringLaws
 DEFINITIONS
   laws ==  ((s1=s2 <=> s2=s1) &
diff --git a/src/test/resources/de/hhu/stups/codegenerator/SubstitutionLaws.mch b/src/test/resources/de/hhu/stups/codegenerator/SubstitutionLaws.mch
index 777be9a20..7a40cf0b6 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/SubstitutionLaws.mch
+++ b/src/test/resources/de/hhu/stups/codegenerator/SubstitutionLaws.mch
@@ -1,3 +1,7 @@
+/*
+From ProB Examples, originally used to test ProB,
+rewritten for B2Program
+*/
 MACHINE SubstitutionLaws
 SETS
  ID={aa,bb}
diff --git a/src/test/resources/de/hhu/stups/codegenerator/Train_1_beebook_TLC.mch b/src/test/resources/de/hhu/stups/codegenerator/Train_1_beebook_TLC.mch
index 6d28f16d2..53c6091c7 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/Train_1_beebook_TLC.mch
+++ b/src/test/resources/de/hhu/stups/codegenerator/Train_1_beebook_TLC.mch
@@ -1,3 +1,9 @@
+/*
+Original model:
+J.-R. Abrial. Modeling in Event-B: System and Software Engineering. Cambridge University Press, 2010.
+
+Rewritten for TLC
+*/
 MACHINE Train_1_beebook_TLC
 SETS /* enumerated */
   BLOCKS={A,B,C,D,E,F,G,H,I,J,K,L,M,N};
diff --git a/src/test/resources/de/hhu/stups/codegenerator/Train_1_beebook_deterministic.mch b/src/test/resources/de/hhu/stups/codegenerator/Train_1_beebook_deterministic.mch
index 5bd11dca6..eb8ebe15e 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/Train_1_beebook_deterministic.mch
+++ b/src/test/resources/de/hhu/stups/codegenerator/Train_1_beebook_deterministic.mch
@@ -1,3 +1,7 @@
+/*
+Original model:
+J.-R. Abrial. Modeling in Event-B: System and Software Engineering. Cambridge University Press, 2010.
+*/
 MACHINE Train_1_beebook_deterministic
 SETS /* enumerated */
   BLOCKS={A,B,C,D,E,F,G,H,I,J,K,L,M,N};
diff --git a/src/test/resources/de/hhu/stups/codegenerator/Train_1_beebook_deterministic_MC.mch b/src/test/resources/de/hhu/stups/codegenerator/Train_1_beebook_deterministic_MC.mch
index 225cbd969..3a5066521 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/Train_1_beebook_deterministic_MC.mch
+++ b/src/test/resources/de/hhu/stups/codegenerator/Train_1_beebook_deterministic_MC.mch
@@ -1,3 +1,9 @@
+/*
+Original model:
+J.-R. Abrial. Modeling in Event-B: System and Software Engineering. Cambridge University Press, 2010.
+
+Model applies Partial Order Reduction manually
+*/
 MACHINE Train_1_beebook_deterministic_MC
 SETS /* enumerated */
   BLOCKS={A,B,C,D,E,F,G,H,I,J,K,L,M,N};
diff --git a/src/test/resources/de/hhu/stups/codegenerator/Train_1_beebook_deterministic_MC_POR.mch b/src/test/resources/de/hhu/stups/codegenerator/Train_1_beebook_deterministic_MC_POR.mch
index 69c95a793..3173c5ec3 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/Train_1_beebook_deterministic_MC_POR.mch
+++ b/src/test/resources/de/hhu/stups/codegenerator/Train_1_beebook_deterministic_MC_POR.mch
@@ -1,3 +1,9 @@
+/*
+Original model:
+J.-R. Abrial. Modeling in Event-B: System and Software Engineering. Cambridge University Press, 2010.
+
+Model applies Partial Order Reduction manually
+*/
 MACHINE Train_1_beebook_deterministic_MC_POR
 SETS /* enumerated */
   BLOCKS={A,B,C,D,E,F,G,H,I,J,K,L,M,N};
diff --git a/src/test/resources/de/hhu/stups/codegenerator/Train_1_beebook_deterministic_MC_POR_v2.mch b/src/test/resources/de/hhu/stups/codegenerator/Train_1_beebook_deterministic_MC_POR_v2.mch
index 98968f824..c55c9a88b 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/Train_1_beebook_deterministic_MC_POR_v2.mch
+++ b/src/test/resources/de/hhu/stups/codegenerator/Train_1_beebook_deterministic_MC_POR_v2.mch
@@ -1,3 +1,10 @@
+/*
+Original model:
+J.-R. Abrial. Modeling in Event-B: System and Software Engineering. Cambridge University Press, 2010.
+
+Model applies Partial Order Reduction manually.
+Rewritten version for B2Program
+*/
 MACHINE Train_1_beebook_deterministic_MC_POR_v2
 SETS /* enumerated */
   BLOCKS={A,B,C,D,E,F,G,H,I,J,K,L,M,N};
diff --git a/src/test/resources/de/hhu/stups/codegenerator/Train_1_beebook_deterministic_MC_POR_v3.mch b/src/test/resources/de/hhu/stups/codegenerator/Train_1_beebook_deterministic_MC_POR_v3.mch
index 4a4d10182..585d1ed7b 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/Train_1_beebook_deterministic_MC_POR_v3.mch
+++ b/src/test/resources/de/hhu/stups/codegenerator/Train_1_beebook_deterministic_MC_POR_v3.mch
@@ -1,4 +1,12 @@
-MACHINE Train_1_beebook_deterministic_MC_POR_v3 // this version is very close to Train_1_beebook_tlc_POR. For instance, top-level ANY substitutions are not re-written to PRE as done in Train_1_beebook_deterministic_MC_POR_v2. DEFINITIONS are still inlined.
+/*
+Original model:
+J.-R. Abrial. Modeling in Event-B: System and Software Engineering. Cambridge University Press, 2010.
+
+Model applies Partial Order Reduction manually.
+Rewritten version for B2Program.
+This version is very close to Train_1_beebook_tlc_POR. For instance, top-level ANY substitutions are not re-written to PRE as done in Train_1_beebook_deterministic_MC_POR_v2. DEFINITIONS are still inlined.
+*/
+MACHINE Train_1_beebook_deterministic_MC_POR_v3
 SETS /* enumerated */
   BLOCKS={A,B,C,D,E,F,G,H,I,J,K,L,M,N};
   ROUTES={R1,R2,R3,R4,R5,R6,R7,R8,R9,R10}
diff --git a/src/test/resources/de/hhu/stups/codegenerator/sort_m2_data1000.mch b/src/test/resources/de/hhu/stups/codegenerator/sort_m2_data1000.mch
index c37ac180f..941e2d3e2 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/sort_m2_data1000.mch
+++ b/src/test/resources/de/hhu/stups/codegenerator/sort_m2_data1000.mch
@@ -1,3 +1,7 @@
+/*
+Original Model:
+V. Rivera, N. Catano, T. Wahls, and C. Rueda. Code generation for Event-B. STTT, 19(1):31–52, 2017.
+*/
 MACHINE sort_m2_data1000
 // a version where some assertions and invariants are simplified/removed
 // so that TLC4B can infer a function type for f and g
diff --git a/src/test/resources/de/hhu/stups/codegenerator/sort_m2_data1000_MC.mch b/src/test/resources/de/hhu/stups/codegenerator/sort_m2_data1000_MC.mch
index 13d764409..b932db0c1 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/sort_m2_data1000_MC.mch
+++ b/src/test/resources/de/hhu/stups/codegenerator/sort_m2_data1000_MC.mch
@@ -1,3 +1,7 @@
+/*
+Original Model:
+V. Rivera, N. Catano, T. Wahls, and C. Rueda. Code generation for Event-B. STTT, 19(1):31–52, 2017.
+*/
 MACHINE sort_m2_data1000_MC
 // a version where some assertions and invariants are simplified/removed
 // so that TLC4B can infer a function type for f and g
diff --git a/src/test/resources/de/hhu/stups/codegenerator/tictac.mch b/src/test/resources/de/hhu/stups/codegenerator/tictac.mch
index 9e573e23e..06918e383 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/tictac.mch
+++ b/src/test/resources/de/hhu/stups/codegenerator/tictac.mch
@@ -1,3 +1,6 @@
+/*
+From ProB Examples
+*/
 MACHINE tictac
 
 ABSTRACT_VARIABLES  square, turn
-- 
GitLab