gistfile1.txt

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;