diff --git a/benchmarks/code_gen/Train_1_beebook_deterministic_MC_POR_v3.mch b/benchmarks/code_gen/Train_1_beebook_deterministic_MC_POR_v3.mch
index 4a4d1018281a21e7208d7476dc40ea55ef5df204..585d1ed7b38bcc0b56f6ee9dbb30aa36d1252aa2 100644
--- a/benchmarks/code_gen/Train_1_beebook_deterministic_MC_POR_v3.mch
+++ b/benchmarks/code_gen/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/benchmarks/execution/ProB/Train_1_beebook_deterministic.mch b/benchmarks/execution/ProB/Train_1_beebook_deterministic.mch
index 8793824d8eac2df19b4c5d882261efaf14372921..fcfb7b1c5039edd1ed0ecfbc2cb8124891f7b36f 100644
--- a/benchmarks/execution/ProB/Train_1_beebook_deterministic.mch
+++ b/benchmarks/execution/ProB/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/benchmarks/model_checking/ProB/Train_1_beebook_deterministic_MC_POR.mch b/benchmarks/model_checking/ProB/Train_1_beebook_deterministic_MC_POR.mch
index bc2fa7808beca49b89da5c6db921c6fb8a3f9321..7345139fe9e501a5d57a6ace9aabc9615eb6f85e 100644
--- a/benchmarks/model_checking/ProB/Train_1_beebook_deterministic_MC_POR.mch
+++ b/benchmarks/model_checking/ProB/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/benchmarks/model_checking/ProB/Train_1_beebook_deterministic_MC_POR_v2.mch b/benchmarks/model_checking/ProB/Train_1_beebook_deterministic_MC_POR_v2.mch
index 40a4dc747dda7a17e0f51b6ae90f4940fdc25c82..89cc1d2c9976f40d4fa20ebe101e22006322d830 100644
--- a/benchmarks/model_checking/ProB/Train_1_beebook_deterministic_MC_POR_v2.mch
+++ b/benchmarks/model_checking/ProB/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/benchmarks/model_checking/TLC/Train_1_beebook_deterministic_MC_POR.mch b/benchmarks/model_checking/TLC/Train_1_beebook_deterministic_MC_POR.mch
index bc2fa7808beca49b89da5c6db921c6fb8a3f9321..f11ca712a51faae5827e6eba10fc748de56c7aea 100644
--- a/benchmarks/model_checking/TLC/Train_1_beebook_deterministic_MC_POR.mch
+++ b/benchmarks/model_checking/TLC/Train_1_beebook_deterministic_MC_POR.mch
@@ -1,3 +1,8 @@
+/*
+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/benchmarks/model_checking/TLC/Train_1_beebook_deterministic_MC_POR_v2.mch b/benchmarks/model_checking/TLC/Train_1_beebook_deterministic_MC_POR_v2.mch
index 40a4dc747dda7a17e0f51b6ae90f4940fdc25c82..89cc1d2c9976f40d4fa20ebe101e22006322d830 100644
--- a/benchmarks/model_checking/TLC/Train_1_beebook_deterministic_MC_POR_v2.mch
+++ b/benchmarks/model_checking/TLC/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/benchmarks/model_checking_opreuse/ProB/Train_1_beebook_deterministic_MC_POR_v3.mch b/benchmarks/model_checking_opreuse/ProB/Train_1_beebook_deterministic_MC_POR_v3.mch
index 4a4d1018281a21e7208d7476dc40ea55ef5df204..585d1ed7b38bcc0b56f6ee9dbb30aa36d1252aa2 100644
--- a/benchmarks/model_checking_opreuse/ProB/Train_1_beebook_deterministic_MC_POR_v3.mch
+++ b/benchmarks/model_checking_opreuse/ProB/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}