Profile

 1 ```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 ``` ```--@ ensures OK; ``` ```node top (igsw, ccd, cconoff, bpa, cccanc, battok, gearok, ``` ``` qfok, sdok, accok, ccseti, ccsetd, ccr: bool; vs: int) ``` ``` returns (OK : bool); ``` ```var ``` ``` ccont, cca: bool; ``` ``` env : bool; ``` ```let ``` ``` (ccont, cca) = main(igsw, ccd, cconoff, bpa, cccanc, battok, ``` ``` gearok, qfok, sdok, accok, ccseti, ccsetd, ``` ``` ccr, vs); ``` ``` env = not igsw -> true; ``` ``` OK = if PosEdge(cca) then PosEdge(ccseti) or ``` ``` PosEdge(ccsetd) or PosEdge(ccr) else true; ``` ``` --%MAIN; ``` ``` --%PROPERTY OK=true; ``` ```tel ```