### Profile

Download (3.06 KB) Statistics
| Branch: | Tag: | Revision:
 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 ``` ```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 ```
(455-455/908)