CristalCaveGem » LustreC

--

-- Source: Magnus Ljung

-- This is the Lustre source to the specication of a cruise controller

-- that Nielsen presents in Nie98b. This is only an implementation of part

-- of the speci cation. A subset of all requirements are given as the

-- properties , , and . p1 p2 p3 p4

-- PosEdge(X) defines a positive edge of X,

-- i.e. X was false and becomes true

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

let

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

tel

-- Edge(X) defines an edge of X,

-- i.e. X was false and becomes true or vice versa

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

let

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

tel

-- AtLeastOnceSince(X, Y) is true if X has been true once

-- since Y became true

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

let

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

tel

-- MoreThanOneSec(X) is true when X has been true more than 1

-- time instance

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

let

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

tel

-- MoreThanTwoSec(X) is true when X has been true more than 2

-- time instances

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

let

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

tel

-- one_button(ccseti, ccsetd, ccr) defines the event when

-- only one button is pressed

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

-- prev_no_button(ccseti, ccsetd, ccr) defines the event when no

-- button is pressed in the previous time instance

node prev_no_button (ccseti, ccsetd, ccr: bool)

returns (pnb: bool);

let

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

tel

-- one_button_accept(ccseti, ccsetd, ccr, ccont, cca) defines the

-- event when one button is pressed and accepted

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

-- cc_allowed(ccont,...) defines when the cruise control is

-- allowed to be active, i.e. cca is allowed to be true

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 - indicates whether the cc is on or not

   -- igsw - indicates whether the ignition switch is turned

   --        on or not

   -- ccd - indicates whether there is a detected error or not

   -- cconoff - indicates if the driver presses the on/off button

   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);

   -- bpa - true when driver presses the break pedal

   -- cccanc - true when driver presses the cancel button

   -- battok - true when the voltage of the battery >= 9 volt

   -- gearok - true when the gear lever is in position

   --           Drive or Drive_L

   -- qfok - true when the quality signals for vsa, vs and

   --        atglp is ok

   -- sdok - true when the speed deviation is ok

   -- accok - true when the acceleration is ok

   -- vs - indicates the speed of the vehicle

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

                  gearok, qfok, sdok, accok, vs);

   -- ccseti - true when driver presses the set/plus button

   -- ccsetd - true when driver presses the set/minus button

   -- ccr - true when driver presses the resume button

   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

-- Verify node is used to verify properties p1..pn

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

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

         returns (OK: bool);

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);

    OK = p1 and p2 and p3 and p4;

    --%PROPERTY OK=true;

    --%MAIN;

tel