CristalCaveGem » LustreC » Lustrec-Tests

node PosEdge (X: bool) returns (Y: bool);

let

    Y = false -> X and not pre(X);

tel

node Edge (X: bool) returns (Y: bool);

let

    Y = false -> (X and not pre(X) and not X and pre(X));

tel

node AtLeastOnceSince(X, Y: bool) returns (XsinceY: bool);

let

    XsinceY = if Y then X else (true -> X and pre(XsinceY));

tel

node MoreThanOneSec(X: bool) returns (Y: bool);

let

    Y = false -> pre(X) and X;

tel

node MoreThanTwoSec(X: bool) returns (Y: bool);

let

    Y = false -> pre(false -> pre(X) and X) and X;

tel

node one_button (ccseti, ccsetd, ccr: bool) returns (ob: bool);

let

    ob = ccseti and not ccsetd and not ccr or

         not ccseti and ccsetd and not ccr or

         not ccseti and not ccsetd and ccr;

tel

node prev_no_button (ccseti, ccsetd, ccr: bool)

returns (pnb: bool);

let

    pnb = true -> pre(not ccseti and not ccsetd and not ccr);

tel

node one_button_accept (ccseti, ccsetd, ccr, ccont, cca: bool)

returns (oba: bool);

var

   ob, pnb: bool;

let

    pnb = prev_no_button(ccseti, ccsetd, ccr);

    ob = one_button(ccseti, ccsetd, ccr);

    oba = if pnb and ob then

              if not ccr then true

              else AtLeastOnceSince(cca, PosEdge(ccont))

          else false;

tel

node cc_allowed (ccont, igsw, bpa, cccanc, battok, gearok,

         qfok, sdok, accok: bool; vs: int)

returns (ccall: bool);

let

   ccall = ccont and not bpa and battok and gearok and

           qfok and MoreThanOneSec(sdok) and 35 <= vs and

           vs <= 200 and MoreThanTwoSec(accok) and not cccanc;

tel

node main (igsw, ccd, cconoff, bpa, cccanc, battok, gearok,

     qfok, sdok, accok, ccseti, ccsetd, ccr: bool; vs: int)

     returns (ccont, cca: bool);

var

  ccall: bool;

let

   ccont = false -> if Edge(igsw) or ccd or

             pre(ccont) and PosEdge(cconoff) then false

             else if pre(not ccont) and

             PosEdge(cconoff) then true

             else pre(ccont);

   ccall = cc_allowed(ccont, igsw, bpa, cccanc, battok,

                  gearok, qfok, sdok, accok, vs);

   cca = false ->

        if one_button_accept(ccseti, ccsetd, ccr, ccont,

           pre(cca))

           and ccall then true else if not ccall then false

           else pre(cca);

tel

node top (igsw, ccd, cconoff, bpa, cccanc, battok, gearok,

         qfok, sdok, accok, ccseti, ccsetd, ccr: bool; vs: int)

         returns (OK: bool);

--@ contract guarantees OK;

var

   p1, p2, p3, p4: bool;

   ccont, cca: bool;

   env : bool;

let

    env = not igsw -> true;

    p1 = if PosEdge(cca) then PosEdge(ccseti) or

                PosEdge(ccsetd) or PosEdge(ccr) else true;

    p2 = if not cc_allowed(ccont, igsw, bpa, cccanc, battok,

                           gearok, qfok, sdok, accok, vs)

             then not cca

         else true;

    p3 = if PosEdge(ccont) then not Edge(igsw) and

            not ccd and PosEdge(cconoff) else true;

    p4 = if Edge(igsw) then not cca

         else true;

    (ccont, cca) = main(igsw, ccd, cconoff, bpa, cccanc, battok,

                      gearok, qfok, sdok, accok, ccseti, ccsetd,

                      ccr, vs);

  --%MAIN;

    OK = p1 and p2 and p3 and p4;

    --%PROPERTY OK=true;

tel