fischer example with forall in properties

tests/testcases/templates/properties/fischer.imi

@@ -0,0 +1,41 @@
+var
+    id : int;
+    k = 2 : constant;
+    IDLE = -1 : int;
+    N = 3 : int;
+
+synt_var
+    x : clock array (N);
+
+template p(i : int)
+
+loc A: invariant True
+  when id = IDLE do { x[i] := 0 } goto req;
+
+loc req: invariant x[i] <= k
+  when x[i] <= k do { x[i] := 0; id := i } goto waiting;
+
+loc waiting: invariant True
+  when id = IDLE do { x[i] := 0 } goto req;
+  when id = i & x[i] > k goto cs;
+
+loc cs: invariant True
+  when True do { id := IDLE } goto A;
+
+end
+
+forall i in [0, N - 1]: instantiate p[i] := p(i);
+
+init := {
+
+    discrete =
+        forall i in [0, N - 1]: loc[p[i]] := A,
+        id := IDLE,
+    ;
+
+    continuous =
+        forall i in [0, N - 1]: x[i] = i &
+    ;
+}
+
+end

tests/testcases/templates/properties/fischer.imiprop

@@ -0,0 +1 @@
+property := #synth AGnot(forall i in [0, N - 1]: loc[p[i]] = cs)