From 0f4147ea870e72dd54e8ef780034dd005c1c1fca Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?=C3=89tienne=20Andr=C3=A9?= <Andre.Etienne@lipn13.fr>
Date: Fri, 19 Jan 2024 08:46:13 +0100
Subject: [PATCH] Add non-regression model for AF

---
 tests/testcases/AF/AF-timelocks.imi | 99 +++++++++++++++++++++++++++++
 1 file changed, 99 insertions(+)
 create mode 100644 tests/testcases/AF/AF-timelocks.imi

diff --git a/tests/testcases/AF/AF-timelocks.imi b/tests/testcases/AF/AF-timelocks.imi
new file mode 100644
index 00000000..4cea8177
--- /dev/null
+++ b/tests/testcases/AF/AF-timelocks.imi
@@ -0,0 +1,99 @@
+(************************************************************
+ *                                IMITATOR MODEL
+ *
+ * Title            : Toy model to test AF
+ * Description      : Toy model to test AF: example where all paths syntactically reach the accepting location, but some of them violate AF due to timelocks
+ * Correctness      : AF accepting
+ * Scalable         : no
+ * Generated        : no
+ * Categories       : TBD
+ * Source           : Own work
+ * bibkey           : 
+ * Author           : Étienne André
+ * Modeling         : Étienne André
+ * Input by         : Étienne André
+ * License          : Creative Commons Attribution-ShareAlike 4.0 International (CC BY-SA 4.0)
+ *
+ * Created          : 2024/01/19
+ * Last modified    : 2024/01/19
+ * Model version    : 0.1
+ *
+ * IMITATOR version : 3.4-beta
+ ************************************************************)
+
+var
+
+(* Clocks *)
+ 	x,
+		: clock;
+
+(* Parameters *)
+	p,
+		: parameter;
+
+
+
+(************************************************************)
+  automaton pta
+(************************************************************)
+actions: ;
+
+loc l1: invariant x <= 5
+	when x = p goto lF; (* AF holds if p = 5 *)
+	when x = p & x <= 4 goto l2; (* AF holds if 0 <= p <= 4 *)
+	when x = p & x = 1 goto l3; (* AF does not hold if p = 1 *)
+	when x = p & 2 <= x & x <= 3 goto l4; (* AF does not hold if p \in [2, 3] *)
+
+loc l2: invariant x <= 3
+	when True goto lF;
+
+(* AF does not hold for any p *)
+loc l3: invariant x <= 10
+	when x = 5 goto lF;
+
+(* AF does not hold for any p *)
+loc l4: invariant x <= p
+	when x < p goto lF;
+
+accepting loc lF: invariant True
+
+end (* pta *)
+
+
+
+(************************************************************)
+(* Initial state *)
+(************************************************************)
+
+init := {
+	
+    discrete =
+		(*------------------------------------------------------------*)
+		(* Initial location *)
+		(*------------------------------------------------------------*)
+		loc[pta] := l1,
+
+		(*------------------------------------------------------------*)
+		(* Initial discrete variables assignments *)
+		(*------------------------------------------------------------*)
+
+    ;
+
+    continuous =        
+		(*------------------------------------------------------------*)
+		(* Initial clock constraints *)
+		(*------------------------------------------------------------*)
+		& x = 0
+
+		(*------------------------------------------------------------*)
+		(* Parameter constraints *)
+		(*------------------------------------------------------------*)
+		& 0 <= p & p <= 10
+	;
+}
+
+
+(************************************************************)
+(* The end *)
+(************************************************************)
+end