Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / test / src / kind_fmcad08 / simulation / fast_2.lus @ 22fe1c93

History | View | Annotate | Download (5.1 KB)

1
--
2
-- Source: Magnus Ljung
3
-- This is the Lustre source to the specication of a cruise controller
4
-- that Nielsen presents in Nie98b. This is only an implementation of part
5
-- of the speci cation. A subset of all requirements are given as the
6
-- properties , , and . p1 p2 p3 p4
7

    
8
-- PosEdge(X) defines a positive edge of X,
9
-- i.e. X was false and becomes true
10
node PosEdge (X: bool) returns (Y: bool);
11
let
12
    Y = false -> X and not pre(X);
13
tel
14

    
15
-- Edge(X) defines an edge of X,
16
-- i.e. X was false and becomes true or vice versa
17
node Edge (X: bool) returns (Y: bool);
18
let
19
    Y = false -> (X and not pre(X) or not X and pre(X));
20
tel
21

    
22
-- AtLeastOnceSince(X, Y) is true if X has been true once
23
-- since Y became true
24
node AtLeastOnceSince(X, Y: bool) returns (XsinceY: bool);
25
let
26
    XsinceY = if Y then X else (true -> X or pre(XsinceY));
27
tel
28

    
29
-- MoreThanOneSec(X) is true when X has been true more than 1
30
-- time instance
31
node MoreThanOneSec(X: bool) returns (Y: bool);
32
let
33
    Y = false -> pre(X) and X;
34
tel
35

    
36
-- MoreThanTwoSec(X) is true when X has been true more than 2
37
-- time instances
38
node MoreThanTwoSec(X: bool) returns (Y: bool);
39
let
40
    Y = false -> pre(false -> pre(X) and X) and X;
41
tel
42

    
43
-- one_button(ccseti, ccsetd, ccr) defines the event when
44
-- only one button is pressed
45
node one_button (ccseti, ccsetd, ccr: bool) returns (ob: bool);
46
let
47
    ob = ccseti and not ccsetd and not ccr or
48
         not ccseti and ccsetd and not ccr or
49
         not ccseti and not ccsetd and ccr;
50
tel
51

    
52
-- prev_no_button(ccseti, ccsetd, ccr) defines the event when no
53
-- button is pressed in the previous time instance
54
node prev_no_button (ccseti, ccsetd, ccr: bool)
55
returns (pnb: bool);
56
let
57
    pnb = true -> pre(not ccseti and not ccsetd and not ccr);
58
tel
59

    
60
-- one_button_accept(ccseti, ccsetd, ccr, ccont, cca) defines the
61
-- event when one button is pressed and accepted
62
node one_button_accept (ccseti, ccsetd, ccr, ccont, cca: bool)
63
returns (oba: bool);
64
var
65
   ob, pnb: bool;
66

    
67
let
68
    pnb = prev_no_button(ccseti, ccsetd, ccr);
69
    ob = one_button(ccseti, ccsetd, ccr);
70
    oba = if pnb and ob then
71
              if not ccr then true
72
              else AtLeastOnceSince(cca, PosEdge(ccont))
73
          else false;
74
tel
75

    
76
-- cc_allowed(ccont,...) defines when the cruise control is
77
-- allowed to be active, i.e. cca is allowed to be true
78
node cc_allowed (ccont, igsw, bpa, cccanc, battok, gearok,
79
         qfok, sdok, accok: bool; vs: int)
80
returns (ccall: bool);
81
let
82
   ccall = ccont and not bpa and battok and gearok and
83
           qfok and MoreThanOneSec(sdok) and 35 <= vs and
84
           vs <= 200 and MoreThanTwoSec(accok) and not cccanc;
85
tel
86

    
87
node main (igsw, ccd, cconoff, bpa, cccanc, battok, gearok,
88
     qfok, sdok, accok, ccseti, ccsetd, ccr: bool; vs: int)
89
     returns (ccont, cca: bool);
90
var
91
  ccall: bool;
92
let
93
   -- ccont - indicates whether the cc is on or not
94
   -- igsw - indicates whether the ignition switch is turned
95
   --        on or not
96
   -- ccd - indicates whether there is a detected error or not
97
   -- cconoff - indicates if the driver presses the on/off button
98
   ccont = false -> if Edge(igsw) or ccd or
99
             pre(ccont) and PosEdge(cconoff) then false
100
             else if pre(not ccont) and
101
             PosEdge(cconoff) then true
102
             else pre(ccont);
103

    
104
   -- bpa - true when driver presses the break pedal
105
   -- cccanc - true when driver presses the cancel button
106
   -- battok - true when the voltage of the battery >= 9 volt
107
   -- gearok - true when the gear lever is in position
108
   --           Drive or Drive_L
109
   -- qfok - true when the quality signals for vsa, vs and
110
   --        atglp is ok
111
   -- sdok - true when the speed deviation is ok
112
   -- accok - true when the acceleration is ok
113
   -- vs - indicates the speed of the vehicle
114
   ccall = cc_allowed(ccont, igsw, bpa, cccanc, battok,
115
                  gearok, qfok, sdok, accok, vs);
116

    
117
   -- ccseti - true when driver presses the set/plus button
118
   -- ccsetd - true when driver presses the set/minus button
119
   -- ccr - true when driver presses the resume button
120
   cca = false ->
121
        if one_button_accept(ccseti, ccsetd, ccr, ccont,
122
           pre(cca))
123
           and ccall then true else if not ccall then false
124
           else pre(cca);
125
tel
126

    
127
-- Verify node is used to verify properties p1..pn
128
node top (igsw, ccd, cconoff, bpa, cccanc, battok, gearok,
129
         qfok, sdok, accok, ccseti, ccsetd, ccr: bool; vs: int)
130
         returns (OK: bool);
131
var
132
   p1, p2, p3, p4: bool;
133
   ccont, cca: bool;
134
   env : bool;
135
let
136
    env = not igsw -> true;
137

    
138
    p1 = if PosEdge(cca) then PosEdge(ccseti) or
139
                PosEdge(ccsetd) or PosEdge(ccr) else true;
140

    
141
    p2 = if not cc_allowed(ccont, igsw, bpa, cccanc, battok,
142
                           gearok, qfok, sdok, accok, vs)
143
             then not cca
144
         else true;
145

    
146
    p3 = if PosEdge(ccont) then not Edge(igsw) and
147
            not ccd and PosEdge(cconoff) else true;
148

    
149
    p4 = if Edge(igsw) then not cca
150
         else true;
151

    
152
    (ccont, cca) = main(igsw, ccd, cconoff, bpa, cccanc, battok,
153
                      gearok, qfok, sdok, accok, ccseti, ccsetd,
154
                      ccr, vs);
155
    OK = p1 and p2 and p3 and p4;
156
    --%PROPERTY OK=true;
157
    --%MAIN;
158
tel