From b452379e31fe94ddb639ed8d84aca6fcb626097e Mon Sep 17 00:00:00 2001
From: Fabian Vu <Fabian.Vu@hhu.de>
Date: Sun, 24 Nov 2024 23:00:18 +0100
Subject: [PATCH] Update information on benchmark files
---
benchmarks/model_checking/ProB/Train_1_beebook_tlc_POR.mch | 7 +++++++
.../ProB/Train_1_beebook_tlc_POR.mch | 7 +++++++
.../model_checking_opreuse/TLC/Train_1_beebook_tlc_POR.mch | 7 +++++++
3 files changed, 21 insertions(+)
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 6cc273050..70b843e09 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 6cc273050..70b843e09 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 6cc273050..70b843e09 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};
--
GitLab