Add non-regression test for AF

imitator-model-checker · Jan 19, 2024 · 4d4db56 · 4d4db56
1 parent 7d481df
commit 4d4db56
Showing 1 changed file with 30 additions and 0 deletions.
diff --git a/tests/regression_tests_data.py b/tests/regression_tests_data.py
@@ -16208,6 +16208,36 @@
 
 	,
 
+	#------------------------------------------------------------
+	{
+		# Test version             : 1
+		# Test author              : Étienne André
+		# Test since               : 2024/01/19
+		# Last modified            : 2024/01/19
+		# Test for IMITATOR version: 3.4
+		'purpose'    : 'Test AF: simple reachability',
+		'tags'       : 'AF',
+		'input_files': ['AF/AF-simple.imi' , 'basic-properties/synth-AF-accepting.imiprop'],
+		'options'    : '',
+		'expectations' : [
+			{'file': 'AF-simple.res' , 'content' : """
+BEGIN CONSTRAINT
+  5 >= p
+ & p > 2
+ OR
+   2 > p
+ & p >= 0
+END CONSTRAINT
+
+		"""
+			} # end result file
+			,
+		] # end expectations
+	} # end test case
+	#------------------------------------------------------------
+
+	,
+
 	#*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-
 	# ??
 	#*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-