Test files from Github issues

Author: Christoph sticksel

tests/lustre/test-issue-116-1.lus

@@ -0,0 +1,208 @@
+node main(
+  a : bool;
+  b : bool;
+  c : bool;
+  d : bool
+) returns (
+  cost : int
+);
+var
+  torch : bool;
+  at_least_one_travelers : bool;
+  no_more_than_two_travelers : bool;
+  solved : bool;
+  prop1 : bool;
+  prop2 : bool;
+  traveler__0__state : bool;
+  traveler__0__torch : bool;
+  traveler__0__ok : bool;
+  traveler__1__state : bool;
+  traveler__1__torch : bool;
+  traveler__1__ok : bool;
+  traveler__2__state : bool;
+  traveler__2__torch : bool;
+  traveler__2__ok : bool;
+  traveler__3__state : bool;
+  traveler__3__torch : bool;
+  traveler__3__ok : bool;
+  b2i__0__x : bool;
+  b2i__0__y : int;
+  b2i__1__x : bool;
+  b2i__1__y : int;
+  b2i__2__x : bool;
+  b2i__2__y : int;
+  b2i__3__x : bool;
+  b2i__3__y : int;
+  max__0__x : int;
+  max__0__y : int;
+  max__0__z : int;
+  max__0__w : int;
+  max__0__out : int;
+  changed__0__x : bool;
+  changed__0__c : bool;
+  changed__1__x : bool;
+  changed__1__c : bool;
+  changed__2__x : bool;
+  changed__2__c : bool;
+  changed__3__x : bool;
+  changed__3__c : bool;
+  cost__0__state : bool;
+  cost__0__value : int;
+  cost__0__out : int;
+  cost__1__state : bool;
+  cost__1__value : int;
+  cost__1__out : int;
+  cost__2__state : bool;
+  cost__2__value : int;
+  cost__2__out : int;
+  cost__3__state : bool;
+  cost__3__value : int;
+  cost__3__out : int;
+  max__0__max2__0__x : int;
+  max__0__max2__0__y : int;
+  max__0__max2__0__out : int;
+  max__0__max2__1__x : int;
+  max__0__max2__1__y : int;
+  max__0__max2__1__out : int;
+  max__0__max2__2__x : int;
+  max__0__max2__2__y : int;
+  max__0__max2__2__out : int;
+let
+  traveler__0__state = a;
+
+  traveler__0__torch = torch;
+
+  traveler__0__ok = ((traveler__0__state = false) -> ((traveler__0__state <> (pre traveler__0__state)) => ((pre traveler__0__state) = traveler__0__torch)));
+
+  traveler__1__state = b;
+
+  traveler__1__torch = torch;
+
+  traveler__1__ok = ((traveler__1__state = false) -> ((traveler__1__state <> (pre traveler__1__state)) => ((pre traveler__1__state) = traveler__1__torch)));
+
+  traveler__2__state = c;
+
+  traveler__2__torch = torch;
+
+  traveler__2__ok = ((traveler__2__state = false) -> ((traveler__2__state <> (pre traveler__2__state)) => ((pre traveler__2__state) = traveler__2__torch)));
+
+  traveler__3__state = d;
+
+  traveler__3__torch = torch;
+
+  traveler__3__ok = ((traveler__3__state = false) -> ((traveler__3__state <> (pre traveler__3__state)) => ((pre traveler__3__state) = traveler__3__torch)));
+
+  torch = (true -> (not (pre torch)));
+
+  at_least_one_travelers = (true -> ((((a <> (pre a)) or (b <> (pre b))) or (c <> (pre c))) or (d <> (pre d))));
+
+  no_more_than_two_travelers = ((((b2i__0__y + b2i__1__y) + b2i__2__y) + b2i__3__y) <= 2);
+
+  cost = (0 -> ((pre cost) + max__0__out));
+
+  solved = (((a and b) and c) and d);
+
+  prop1 = (not (solved and (cost < 15)));
+
+  prop2 = (not (solved and (cost = 15)));
+
+  b2i__0__x = changed__0__c;
+
+  b2i__0__y = (if b2i__0__x then 1 else 0);
+
+  b2i__1__x = changed__1__c;
+
+  b2i__1__y = (if b2i__1__x then 1 else 0);
+
+  b2i__2__x = changed__2__c;
+
+  b2i__2__y = (if b2i__2__x then 1 else 0);
+
+  b2i__3__x = changed__3__c;
+
+  b2i__3__y = (if b2i__3__x then 1 else 0);
+
+  max__0__x = cost__0__out;
+
+  max__0__y = cost__1__out;
+
+  max__0__z = cost__2__out;
+
+  max__0__w = cost__3__out;
+
+  max__0__out = max__0__max2__0__out;
+
+  changed__0__x = a;
+
+  changed__0__c = (false -> (changed__0__x <> (pre changed__0__x)));
+
+  changed__1__x = b;
+
+  changed__1__c = (false -> (changed__1__x <> (pre changed__1__x)));
+
+  changed__2__x = c;
+
+  changed__2__c = (false -> (changed__2__x <> (pre changed__2__x)));
+
+  changed__3__x = d;
+
+  changed__3__c = (false -> (changed__3__x <> (pre changed__3__x)));
+
+  cost__0__state = a;
+
+  cost__0__value = 1;
+
+  cost__0__out = (0 -> (if (cost__0__state <> (pre cost__0__state)) then cost__0__value else 0));
+
+  cost__1__state = b;
+
+  cost__1__value = 2;
+
+  cost__1__out = (0 -> (if (cost__1__state <> (pre cost__1__state)) then cost__1__value else 0));
+
+  cost__2__state = c;
+
+  cost__2__value = 5;
+
+  cost__2__out = (0 -> (if (cost__2__state <> (pre cost__2__state)) then cost__2__value else 0));
+
+  cost__3__state = d;
+
+  cost__3__value = 8;
+
+  cost__3__out = (0 -> (if (cost__3__state <> (pre cost__3__state)) then cost__3__value else 0));
+
+  max__0__max2__0__x = max__0__x;
+
+  max__0__max2__0__y = max__0__max2__1__out;
+
+  max__0__max2__0__out = (if (max__0__max2__0__x >= max__0__max2__0__y) then max__0__max2__0__x else max__0__max2__0__y);
+
+  max__0__max2__1__x = max__0__y;
+
+  max__0__max2__1__y = max__0__max2__2__out;
+
+  max__0__max2__1__out = (if (max__0__max2__1__x >= max__0__max2__1__y) then max__0__max2__1__x else max__0__max2__1__y);
+
+  max__0__max2__2__x = max__0__z;
+
+  max__0__max2__2__y = max__0__w;
+
+  max__0__max2__2__out = (if (max__0__max2__2__x >= max__0__max2__2__y) then max__0__max2__2__x else max__0__max2__2__y);
+
+  assert traveler__0__ok;
+
+  assert traveler__1__ok;
+
+  assert traveler__2__ok;
+
+  assert traveler__3__ok;
+
+  assert at_least_one_travelers;
+
+  assert no_more_than_two_travelers;
+
+  --%PROPERTY prop1;
+  --%PROPERTY prop2;
+
+tel;

tests/lustre/test-issue-116-2.lus

@@ -0,0 +1,21 @@
+node integ(x : int) returns (sum : int);
+let
+  sum = x + (0 -> pre sum);
+tel;
+
+node main(x : int; y : int; r : real) returns (z : int);
+var
+  history : bool;
+  prop1 : bool;
+  prop2 : bool;
+let
+  z = integ(x);
+
+  history = x > 0 and (true -> pre history);
+  prop1 = history => z > 0;
+
+  --%PROPERTY prop1;
+
+  prop2 = integ(x) + integ(y) = integ(x + y) -> pre(integ(x) + integ(y) = integ(x + y) -> not(0.0 < r and r < 1.0));
+  --%PROPERTY prop2;
+tel;