Add non-regression tests for IM+IH (on CSMA/CD example)

imitator-model-checker · Oct 11, 2024 · f8c5454 · f8c5454
1 parent ab7dd59
commit f8c5454
Show file tree

Hide file tree

Showing 6 changed files with 1,890 additions and 0 deletions.
diff --git a/tests/regression_tests_data.py b/tests/regression_tests_data.py
@@ -21836,7 +21836,9 @@
 		] # end expectations
 	} # end test case
 	#------------------------------------------------------------
+
 	,
+
 	#------------------------------------------------------------
 	{
 		'purpose'    : 'Test IM on an incomplete example',
@@ -21883,6 +21885,182 @@
 
 	,
 
+	#------------------------------------------------------------
+	{
+		'purpose'    : 'Test IM: CSMA/CD (BC=1)',
+		'input_files': ['IH/CSMACD-bc1.imi', 'IH/CSMACD-IM.imiprop'],
+		'options'    : '',
+		'expectations' : [
+			{'file': 'CSMACD-bc1.res' , 'content' : """
+BEGIN CONSTRAINT
+  lambda > 15*timeslot
+ & sigma > 0
+ & timeslot > sigma
+ & 16*timeslot > lambda
+END CONSTRAINT
+"""
+			} # end result file
+			,
+		] # end expectations
+	} # end test case
+	#------------------------------------------------------------
+
+	,
+
+	#------------------------------------------------------------
+	{
+		'purpose'    : 'Test IM: CSMA/CD (BC=1) + IH',
+		'input_files': ['IH/CSMACD-bc1.imi', 'IH/CSMACD-IM.imiprop'],
+		'options'    : '-ih',
+		'expectations' : [
+			{'file': 'CSMACD-bc1.res' , 'content' : """
+BEGIN CONSTRAINT
+  lambda > 15*timeslot
+ & sigma > 0
+ & timeslot > sigma
+ & 16*timeslot > lambda
+END CONSTRAINT
+"""
+			} # end result file
+			,
+		] # end expectations
+	} # end test case
+	#------------------------------------------------------------
+
+	,
+
+	#------------------------------------------------------------
+	{
+		'purpose'    : 'Test IM: CSMA/CD (BC=2)',
+		'input_files': ['IH/CSMACD-bc2.imi', 'IH/CSMACD-IM.imiprop'],
+		'options'    : '',
+		'expectations' : [
+			{'file': 'CSMACD-bc2.res' , 'content' : """
+BEGIN CONSTRAINT
+  lambda > 15*timeslot
+ & sigma > 0
+ & timeslot > sigma
+ & 16*timeslot > lambda
+END CONSTRAINT
+"""
+			} # end result file
+			,
+		] # end expectations
+	} # end test case
+	#------------------------------------------------------------
+
+	,
+
+	#------------------------------------------------------------
+	{
+		'purpose'    : 'Test IM: CSMA/CD (BC=2) + IH',
+		'input_files': ['IH/CSMACD-bc2.imi', 'IH/CSMACD-IM.imiprop'],
+		'options'    : '-ih',
+		'expectations' : [
+			{'file': 'CSMACD-bc2.res' , 'content' : """
+BEGIN CONSTRAINT
+  lambda > 15*timeslot
+ & sigma > 0
+ & timeslot > sigma
+ & 16*timeslot > lambda
+END CONSTRAINT
+"""
+			} # end result file
+			,
+		] # end expectations
+	} # end test case
+	#------------------------------------------------------------
+
+	,
+
+	#------------------------------------------------------------
+	{
+		'purpose'    : 'Test IM: CSMA/CD (BC=3)',
+		'input_files': ['IH/CSMACD-bc3.imi', 'IH/CSMACD-IM.imiprop'],
+		'options'    : '',
+		'expectations' : [
+			{'file': 'CSMACD-bc3.res' , 'content' : """
+BEGIN CONSTRAINT
+  lambda > 15*timeslot
+ & sigma > 0
+ & timeslot > sigma
+ & 16*timeslot > lambda
+END CONSTRAINT
+"""
+			} # end result file
+			,
+		] # end expectations
+	} # end test case
+	#------------------------------------------------------------
+
+	,
+
+	#------------------------------------------------------------
+	{
+		'purpose'    : 'Test IM: CSMA/CD (BC=3) + IH',
+		'input_files': ['IH/CSMACD-bc3.imi', 'IH/CSMACD-IM.imiprop'],
+		'options'    : '-ih',
+		'expectations' : [
+			{'file': 'CSMACD-bc3.res' , 'content' : """
+BEGIN CONSTRAINT
+  lambda > 15*timeslot
+ & sigma > 0
+ & timeslot > sigma
+ & 16*timeslot > lambda
+END CONSTRAINT
+"""
+			} # end result file
+			,
+		] # end expectations
+	} # end test case
+	#------------------------------------------------------------
+
+	,
+
+	#------------------------------------------------------------
+	{
+		'purpose'    : 'Test IM: CSMA/CD (BC=4)',
+		'input_files': ['IH/CSMACD-bc4.imi', 'IH/CSMACD-IM.imiprop'],
+		'options'    : '',
+		'expectations' : [
+			{'file': 'CSMACD-bc4.res' , 'content' : """
+BEGIN CONSTRAINT
+  lambda > 15*timeslot
+ & sigma > 0
+ & timeslot > sigma
+ & 16*timeslot > lambda
+END CONSTRAINT
+"""
+			} # end result file
+			,
+		] # end expectations
+	} # end test case
+	#------------------------------------------------------------
+
+	,
+
+	#------------------------------------------------------------
+	{
+		'purpose'    : 'Test IM: CSMA/CD (BC=4) + IH',
+		'input_files': ['IH/CSMACD-bc4.imi', 'IH/CSMACD-IM.imiprop'],
+		'options'    : '-ih',
+		'expectations' : [
+			{'file': 'CSMACD-bc4.res' , 'content' : """
+BEGIN CONSTRAINT
+  lambda > 15*timeslot
+ & sigma > 0
+ & timeslot > sigma
+ & 16*timeslot > lambda
+END CONSTRAINT
+"""
+			} # end result file
+			,
+		] # end expectations
+	} # end test case
+	#------------------------------------------------------------
+
+	,
+
 	#------------------------------------------------------------
 	{
 		# Test version             : 1

diff --git a/tests/testcases/IH/CSMACD-IM.imiprop b/tests/testcases/IH/CSMACD-IM.imiprop
@@ -0,0 +1,29 @@
+(************************************************************
+ *                      IMITATOR MODEL                      
+ *
+ * CSMA/CD Protocol
+ *
+ * Description     : CSMA/CD Protocol
+ * Correctness     : TODO
+ * Source          : Non-probabilistic model deduced from the probabilistic model in "Symbolic Model Checking for Probabilistic Timed Automata" (M. Kwiatkowska, G. Norman, J. Sproston and F. Wang., FORMATS/FTRTFT'2004). See figures on http://www.prismmodelchecker.org/casestudies/csma.php
+ * Author          : M. Kwiatkowska, G. Norman, J. Sproston and F. Wang. 
+ * Modeling        : M. Kwiatkowska, G. Norman, J. Sproston and F. Wang. 
+ * Input by        : Laurent Fribourg and Etienne Andre
+ *
+ * Created         : 2007
+ * Last modified   : 2020/08/14
+ *
+ * IMITATOR version: 3
+ ************************************************************)
+
+property := #synth IM(
+	(* IEEE VALUE *)
+ 	& lambda   = 808
+ 	& sigma    = 26
+ 	& timeslot = 52
+
+	(* RESCALED PRISM VALUE *)
+(*	& lambda   = 96
+	& sigma    = 3
+	& timeslot = 6*)
+);