diff --git a/benchmarks/model_checking/ProB/Train_1_beebook_tlc_POR.mch b/benchmarks/model_checking/ProB/Train_1_beebook_tlc_POR.mch
index 6cc2730505abe2c33a24377ea003870e229cc16e..70b843e0954d9421a5926d37f48e0a4299dd3e72 100644
--- a/benchmarks/model_checking/ProB/Train_1_beebook_tlc_POR.mch
+++ b/benchmarks/model_checking/ProB/Train_1_beebook_tlc_POR.mch
@@ -1,3 +1,10 @@
+/*
+Original model:
+J.-R. Abrial. Modeling in Event-B: System and Software Engineering. Cambridge University Press, 2010.
+
+Rewritten for TLC
+Applies Partial Order Reduction
+*/
 MACHINE Train_1_beebook_tlc_POR
 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_tlc_POR.mch b/benchmarks/model_checking_opreuse/ProB/Train_1_beebook_tlc_POR.mch
index 6cc2730505abe2c33a24377ea003870e229cc16e..70b843e0954d9421a5926d37f48e0a4299dd3e72 100644
--- a/benchmarks/model_checking_opreuse/ProB/Train_1_beebook_tlc_POR.mch
+++ b/benchmarks/model_checking_opreuse/ProB/Train_1_beebook_tlc_POR.mch
@@ -1,3 +1,10 @@
+/*
+Original model:
+J.-R. Abrial. Modeling in Event-B: System and Software Engineering. Cambridge University Press, 2010.
+
+Rewritten for TLC
+Applies Partial Order Reduction
+*/
 MACHINE Train_1_beebook_tlc_POR
 SETS /* enumerated */
   BLOCKS={A,B,C,D,E,F,G,H,I,J,K,L,M,N};
diff --git a/benchmarks/model_checking_opreuse/TLC/Train_1_beebook_tlc_POR.mch b/benchmarks/model_checking_opreuse/TLC/Train_1_beebook_tlc_POR.mch
index 6cc2730505abe2c33a24377ea003870e229cc16e..70b843e0954d9421a5926d37f48e0a4299dd3e72 100644
--- a/benchmarks/model_checking_opreuse/TLC/Train_1_beebook_tlc_POR.mch
+++ b/benchmarks/model_checking_opreuse/TLC/Train_1_beebook_tlc_POR.mch
@@ -1,3 +1,10 @@
+/*
+Original model:
+J.-R. Abrial. Modeling in Event-B: System and Software Engineering. Cambridge University Press, 2010.
+
+Rewritten for TLC
+Applies Partial Order Reduction
+*/
 MACHINE Train_1_beebook_tlc_POR
 SETS /* enumerated */
   BLOCKS={A,B,C,D,E,F,G,H,I,J,K,L,M,N};