Project

General

Profile

Revision af44cb25

View differences:

regression_tests/lustre_files/failed/aut1.lus
1

  
2
node top (x :int) returns (y:bool) 
3
var l:int;
4
let
5
 automaton parity
6
 state Even :
7
 unless (x mod 2 = 1) restart Odd
8
 let
9
   l = x -> pre (l/2);
10
 tel
11
 state Odd  :
12
 unless (x mod 2 = 0) restart Even
13
 let
14
  l = x -> pre (3*l + 1);
15
 tel
16
 y = (l = 1);
17
tel
regression_tests/lustre_files/failed/aut1.lusi
1
(* Generated Lustre Interface file from aut1.lus *)
2
(* by Lustre-C compiler version 1.3-458, 2016/10/21, 12:58:29 *)
3
(* Feel free to mask some of the definitions by removing them from this file. *)
4

  
5
type parity__type = enum {Even, Odd }; 
6

  
7
node parity__Even_handler_until (parity__restart_act: bool; x: int) returns (parity__restart_in: bool; parity__state_in: parity__type; l_out: int);
8

  
9
function parity__Even_unless (parity__restart_in: bool; x: int) returns (parity__restart_act: bool; parity__state_act: parity__type);
10

  
11
node parity__Odd_handler_until (parity__restart_act: bool; x: int) returns (parity__restart_in: bool; parity__state_in: parity__type; l_out: int);
12

  
13
function parity__Odd_unless (parity__restart_in: bool; x: int) returns (parity__restart_act: bool; parity__state_act: parity__type);
14

  
15
node top (x: int) returns (y: bool);
16

  
regression_tests/lustre_files/failed/aut1_top__output_values
1
'y': '0' 
2
'y': '0' 
3
'y': '0' 
4
'y': '1' 
5
'y': '0' 
6
'y': '0' 
7
'y': '0' 
8
'y': '0' 
9
'y': '0' 
10
'y': '0' 
11
'y': '0' 
12
'y': '0' 
13
'y': '0' 
14
'y': '0' 
15
'y': '0' 
16
'y': '0' 
17
'y': '0' 
18
'y': '0' 
19
'y': '1' 
20
'y': '0' 
21
'y': '0' 
22
'y': '0' 
23
'y': '0' 
24
'y': '0' 
25
'y': '0' 
26
'y': '0' 
27
'y': '0' 
28
'y': '0' 
29
'y': '0' 
30
'y': '0' 
31
'y': '0' 
32
'y': '0' 
33
'y': '0' 
34
'y': '0' 
35
'y': '0' 
36
'y': '0' 
37
'y': '0' 
38
'y': '0' 
39
'y': '0' 
40
'y': '0' 
41
'y': '0' 
42
'y': '0' 
43
'y': '0' 
44
'y': '0' 
45
'y': '0' 
46
'y': '0' 
47
'y': '0' 
48
'y': '0' 
49
'y': '0' 
50
'y': '0' 
51
'y': '0' 
52
'y': '0' 
53
'y': '0' 
54
'y': '0' 
55
'y': '0' 
56
'y': '0' 
57
'y': '0' 
58
'y': '0' 
59
'y': '0' 
60
'y': '0' 
61
'y': '0' 
62
'y': '0' 
63
'y': '0' 
64
'y': '0' 
65
'y': '0' 
66
'y': '0' 
67
'y': '0' 
68
'y': '0' 
69
'y': '0' 
70
'y': '0' 
71
'y': '1' 
72
'y': '0' 
73
'y': '0' 
74
'y': '1' 
75
'y': '0' 
76
'y': '0' 
77
'y': '0' 
78
'y': '0' 
79
'y': '0' 
80
'y': '0' 
81
'y': '0' 
82
'y': '0' 
83
'y': '0' 
84
'y': '0' 
85
'y': '0' 
86
'y': '0' 
87
'y': '0' 
88
'y': '0' 
89
'y': '0' 
90
'y': '0' 
91
'y': '0' 
92
'y': '0' 
93
'y': '0' 
94
'y': '1' 
95
'y': '0' 
96
'y': '0' 
97
'y': '0' 
98
'y': '0' 
99
'y': '0' 
100
'y': '0' 
regression_tests/lustre_files/failed/aut1_top__timeout60_xml.xml
1
<?xml version="1.0"?>
2
   <Results xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance">
3
     <Property name="top">
4
      <Date>2016-11-30 00:18</Date>
5
      <Lustre2Horn unit="sec">0.00</Lustre2Horn>
6
      <Parse unit="sec">0.00</Parse>
7
      <Query unit="sec">0.09</Query>
8
      <Answer>CEX</Answer>
9
      <Counterexample>
10
         <Node name ="parity__Even_unless">
11
            <Stream name="parity__Even_unless.parity__restart_act" type="unk">
12
                <Value instant="0">1</Value>
13
           </Stream>
14
            <Stream name="parity__Even_unless.parity__state_act" type="unk">
15
                <Value instant="0">Even</Value>
16
           </Stream>
17
            <Stream name="parity__Even_unless.parity__restart_in" type="unk">
18
                <Value instant="0">1</Value>
19
           </Stream>
20
            <Stream name="parity__Even_unless.x" type="unk">
21
                <Value instant="0">0</Value>
22
           </Stream>
23
         </Node>
24
 <Node name ="top">
25
            <Stream name="top.__top_13_x" type="unk">
26
                <Value instant="0">Even</Value>
27
           </Stream>
28
            <Stream name="top.__top_13_x" type="unk">
29
                <Value instant="0">Even</Value>
30
           </Stream>
31
            <Stream name="top.__top_12_x" type="unk">
32
                <Value instant="0">1</Value>
33
           </Stream>
34
            <Stream name="top.ni_1.parity__Odd_handler_until.__parity__Odd_handler_until_2_c" type="unk">
35
                <Value instant="0">5</Value>
36
           </Stream>
37
            <Stream name="top.ni_0.parity__Even_handler_until.__parity__Even_handler_until_2_x" type="unk">
38
                <Value instant="0">0</Value>
39
           </Stream>
40
            <Stream name="top.ni_1.parity__Odd_handler_until.__parity__Odd_handler_until_2_x" type="unk">
41
                <Value instant="0">0</Value>
42
           </Stream>
43
            <Stream name="top.__top_12_c" type="unk">
44
                <Value instant="0">1</Value>
45
           </Stream>
46
            <Stream name="y" type="bool">
47
                <Value instant="0">1</Value>
48
           </Stream>
49
            <Stream name="x" type="int">
50
                <Value instant="0">0</Value>
51
           </Stream>
52
            <Stream name="top.__top_13_c" type="unk">
53
                <Value instant="0">Even</Value>
54
           </Stream>
55
         </Node>
56
 <Node name ="parity__Even_handler_until">
57
            <Stream name="parity__Even_handler_until.l_out" type="unk">
58
                <Value instant="0">0</Value>
59
           </Stream>
60
            <Stream name="parity__Even_handler_until.parity__restart_in" type="unk">
61
                <Value instant="0">1</Value>
62
           </Stream>
63
            <Stream name="parity__Even_handler_until.__parity__Even_handler_until_2_x" type="unk">
64
                <Value instant="0">0</Value>
65
           </Stream>
66
            <Stream name="parity__Even_handler_until.parity__state_in" type="unk">
67
                <Value instant="0">Even</Value>
68
           </Stream>
69
            <Stream name="parity__Even_handler_until.x" type="unk">
70
                <Value instant="0">0</Value>
71
           </Stream>
72
            <Stream name="parity__Even_handler_until.__parity__Even_handler_until_2_c" type="unk">
73
                <Value instant="0">6</Value>
74
           </Stream>
75
            <Stream name="parity__Even_handler_until.parity__restart_act" type="unk">
76
                <Value instant="0">1</Value>
77
           </Stream>
78
         </Node>
79

  
80
      </Counterexample>
81
     </Property>
82
   </Results>
83

  
regression_tests/lustre_files/failed/aut1_top_input_values
1
49
2
6
3
58
4
44
5
98
6
41
7
15
8
89
9
79
10
51
11
70
12
29
13
29
14
49
15
17
16
94
17
37
18
86
19
1
20
84
21
67
22
62
23
87
24
67
25
49
26
70
27
67
28
25
29
32
30
5
31
84
32
52
33
98
34
8
35
69
36
40
37
11
38
34
39
10
40
46
41
29
42
18
43
67
44
78
45
40
46
65
47
30
48
19
49
40
50
67
51
45
52
5
53
22
54
2
55
95
56
18
57
6
58
12
59
96
60
41
61
14
62
91
63
52
64
81
65
28
66
2
67
53
68
79
69
49
70
62
71
1
72
4
73
6
74
94
75
37
76
63
77
57
78
13
79
17
80
94
81
6
82
95
83
74
84
86
85
93
86
15
87
90
88
0
89
87
90
24
91
56
92
80
93
48
94
94
95
23
96
43
97
54
98
24
99
33
100
17
regression_tests/lustre_files/failed/aut2.lus
1
  type parity__type = enum {Even, Odd };
2
  
3
  
4
  function parity__Odd_unless (parity__restart_in: bool; parity__state_in: parity__type; l: int) returns (parity__restart_act: bool; parity__state_act: parity__type)
5
var __parity__Odd_unless_1: bool;
6
let
7
    
8
    parity__restart_act, parity__state_act = (if __parity__Odd_unless_1 then (true,Even) else (parity__restart_in,parity__state_in));
9
    __parity__Odd_unless_1 = ((l mod 2) = 0);
10
     
11
tel
12
 
13
node parity__Odd_handler_until (parity__restart_act: bool; parity__state_act: parity__type; x: int) returns (parity__restart_in: bool; parity__state_in: parity__type; l_out: int)
14
var __parity__Odd_handler_until_2: int;
15
    __parity__Odd_handler_until_1: bool;
16
    l: int;
17
let
18
    
19
    parity__restart_in, parity__state_in = (parity__restart_act,parity__state_act);
20
    l_out = l;
21
    l = (if __parity__Odd_handler_until_1 then x else __parity__Odd_handler_until_2);
22
    __parity__Odd_handler_until_2 = pre ((3 * l) + 1);
23
    __parity__Odd_handler_until_1 = (true -> false);
24
     
25
tel
26
 
27
function parity__Even_unless (parity__restart_in: bool; parity__state_in: parity__type; l: int) returns (parity__restart_act: bool; parity__state_act: parity__type)
28
var __parity__Even_unless_1: bool;
29
let
30
    
31
    parity__restart_act, parity__state_act = (if __parity__Even_unless_1 then (true,Odd) else (parity__restart_in,parity__state_in));
32
    __parity__Even_unless_1 = ((l mod 2) = 1);
33
     
34
tel
35
 
36
node parity__Even_handler_until (parity__restart_act: bool; parity__state_act: parity__type; x: int) returns (parity__restart_in: bool; parity__state_in: parity__type; l_out: int)
37
var __parity__Even_handler_until_2: int;
38
    __parity__Even_handler_until_1: bool;
39
    l: int;
40
let
41
    
42
    parity__restart_in, parity__state_in = (parity__restart_act,parity__state_act);
43
    l_out = l;
44
    l = (if __parity__Even_handler_until_1 then x else __parity__Even_handler_until_2);
45
    __parity__Even_handler_until_2 = pre (l / 2);
46
    __parity__Even_handler_until_1 = (true -> false);
47
     
48
tel
49

  
50
node top (x: int) returns (y: bool)
51
var __test1_12: bool;
52
    __test1_13: parity__type;
53
    __test1_11: bool;
54
    __test1_8: bool;
55
    __test1_9: parity__type;
56
    __test1_10: int;
57
    __test1_5: bool;
58
    __test1_6: parity__type;
59
    __test1_7: int;
60
    __test1_3: bool;
61
    __test1_4: parity__type;
62
    __test1_1: bool;
63
    __test1_2: parity__type;
64
    parity__next_restart_in: bool;
65
    parity__restart_in: bool;
66
    parity__restart_act: bool;
67
    parity__next_state_in: parity__type;
68
    parity__state_in: parity__type clock;
69
    parity__state_act: parity__type clock;
70
    l: int;
71
let
72
    
73
    parity__restart_in, parity__state_in = (if __test1_11 then (false,Even) else (__test1_12,__test1_13));
74
    __test1_12, __test1_13 = pre (parity__next_restart_in,parity__next_state_in);
75
    __test1_11 = (true -> false);
76

  
77
    parity__next_restart_in, parity__next_state_in, l = merge parity__state_act (Even -> (__test1_8,__test1_9,__test1_10))
78
                                                                                (Odd -> (__test1_5,__test1_6,__test1_7));
79
    __test1_8, __test1_9, __test1_10 = parity__Even_handler_until (parity__restart_act when Even(parity__state_act),
80
                                                                   parity__state_act when Even(parity__state_act),
81
                                                                   x when Even(parity__state_act))
82
                                       every (parity__restart_act);
83
    __test1_5, __test1_6, __test1_7 = parity__Odd_handler_until (parity__restart_act when Odd(parity__state_act),
84
                                                                 parity__state_act when Odd(parity__state_act),
85
                                                                 x when Odd(parity__state_act))
86
                                      every (parity__restart_act);
87

  
88

  
89
    parity__restart_act, parity__state_act = merge parity__state_in (Even -> (__test1_3,__test1_4))
90
                                                                    (Odd -> (__test1_1,__test1_2));
91
    __test1_3, __test1_4 = parity__Even_unless (parity__restart_in when Even(parity__state_in),
92
                                                parity__state_in when Even(parity__state_in),
93
                                                l when Even(parity__state_in))
94
                           every (parity__restart_in);
95
    __test1_1, __test1_2 = parity__Odd_unless (parity__restart_in when Odd(parity__state_in),
96
                                               parity__state_in when Odd(parity__state_in),
97
                                               l when Odd(parity__state_in))
98
                           every (parity__restart_in);
99

  
100
    y = (l = 1);
101
     
102
tel
regression_tests/lustre_files/failed/aut2.lusi
1
(* Generated Lustre Interface file from aut2.lus *)
2
(* by Lustre-C compiler version 1.3-458, 2016/10/21, 12:58:30 *)
3
(* Feel free to mask some of the definitions by removing them from this file. *)
4

  
5
type parity__type = enum {Even, Odd }; 
6

  
7
node parity__Even_handler_until (parity__restart_act: bool; parity__state_act: parity__type; x: int) returns (parity__restart_in: bool; parity__state_in: parity__type; l_out: int);
8

  
9
function parity__Even_unless (parity__restart_in: bool; parity__state_in: parity__type; l: int) returns (parity__restart_act: bool; parity__state_act: parity__type);
10

  
11
node parity__Odd_handler_until (parity__restart_act: bool; parity__state_act: parity__type; x: int) returns (parity__restart_in: bool; parity__state_in: parity__type; l_out: int);
12

  
13
function parity__Odd_unless (parity__restart_in: bool; parity__state_in: parity__type; l: int) returns (parity__restart_act: bool; parity__state_act: parity__type);
14

  
15
node top (x: int) returns (y: bool);
16

  
regression_tests/lustre_files/failed/aut2_top_input_values
1
91
2
45
3
85
4
83
5
27
6
22
7
75
8
8
9
76
10
70
11
44
12
55
13
9
14
63
15
74
16
15
17
62
18
21
19
57
20
86
21
89
22
94
23
97
24
21
25
19
26
19
27
52
28
5
29
57
30
88
31
77
32
62
33
66
34
59
35
8
36
87
37
27
38
74
39
82
40
23
41
54
42
53
43
46
44
63
45
42
46
14
47
66
48
60
49
95
50
34
51
88
52
51
53
14
54
54
55
92
56
40
57
67
58
40
59
15
60
64
61
10
62
90
63
86
64
43
65
30
66
39
67
33
68
86
69
57
70
74
71
31
72
55
73
54
74
41
75
91
76
43
77
8
78
13
79
45
80
33
81
22
82
31
83
83
84
29
85
33
86
33
87
88
88
66
89
82
90
19
91
50
92
29
93
35
94
77
95
72
96
12
97
10
98
63
99
75
100
56
regression_tests/lustre_files/failed/heater.lus
1

  
2
const low = 5;
3

  
4
const high = 5;
5

  
6
const delay_on = 200;
7

  
8
const delay_off = 500;
9

  
10
node edge(c : bool) returns (edge_c : bool)
11
let
12
  edge_c = false -> c && not (pre c);
13
tel
14

  
15
node count(d : int; t : bool) returns (ok : bool)
16
var cpt:int;
17
let
18
  ok = (cpt = 0);
19
  cpt = 0 -> (if t then pre cpt + 1 else pre cpt) mod d;
20
tel
21

  
22
(* controling the heat *)
23
(* returns [true] when [expected_temp] does not agree with [actual_temp] *)
24
node heat(expected_temp, actual_temp : int) returns (ok : bool)
25
let
26
  automaton heat_control
27
    state Stop :
28
          unless (actual_temp <= expected_temp - low) resume Start
29
          let
30
            ok = false; 
31
          tel
32
    state Start :
33
          unless (actual_temp >= expected_temp + high) resume Stop
34
          let
35
            ok = true;
36
          tel
37
tel
38

  
39
(* a cyclic two mode automaton with an internal timer *)
40
(* [open_light = true] and [open_gas = true] for [delay_on millisecond] *)
41
(* then [open_light = false] and [open_gas = false] for *)
42
(* [delay_off millisecond] *)
43
node command(millisecond : bool) returns (open_light, open_gas : bool)
44
let
45
  automaton command_control
46
    state Open :
47
          let
48
            open_light = true;
49
            open_gas = true;
50
          tel
51
          until count(delay_on, millisecond) restart Silent
52
    state Silent :
53
          let
54
            open_light = false;
55
            open_gas = false;
56
          tel
57
          until count(delay_off, millisecond) restart Open
58
tel
59

  
60
(* the main command which control the opening of the light and gas *)
61
node light(millisecond : bool; on_heat, on_light : bool) returns (open_light, open_gas, nok : bool)
62
let
63
  automaton light_control
64
    state Light_off :
65
          let
66
            nok = false;
67
            open_light = false;
68
            open_gas = false;
69
          tel
70
          until on_heat restart Try
71
    state Light_on :
72
          let
73
            nok = false;
74
            open_light = false;
75
            open_gas = true;
76
          tel
77
          until not on_heat restart Light_off
78
    state Try :
79
          let
80
            nok = false;
81
            (open_light, open_gas) = command(millisecond);
82
          tel
83
          until on_light restart Light_on
84
          until count(3, edge(not open_light)) restart Failure
85
    state Failure :
86
          let
87
            nok = true; 
88
            open_light = false;
89
            open_gas = false;
90
          tel
91
tel
92

  
93
(* the main function *)
94
node top(millisecond : bool; reset : bool; expected_temp, actual_temp : int; on_light : bool) returns ( ok : bool)
95
var on_heat, nok , open_light, open_gas: bool;
96
let
97
  on_heat = heat(expected_temp,actual_temp) every reset;
98
  (open_light, open_gas, nok) = light(millisecond, on_heat, on_light) every reset;
99
  ok = not nok;
100
tel
regression_tests/lustre_files/failed/heater.lusi
1
(* Generated Lustre Interface file from heater.lus *)
2
(* by Lustre-C compiler version 1.3-458, 2016/10/21, 12:58:29 *)
3
(* Feel free to mask some of the definitions by removing them from this file. *)
4

  
5
const low = 5;
6

  
7
const high = 5;
8

  
9
const delay_on = 200;
10

  
11
const delay_off = 500;
12

  
13
type heat_control__type = enum {Stop, Start }; 
14

  
15
type command_control__type = enum {Open, Silent }; 
16

  
17
type light_control__type = enum {Light_off, Light_on, Try, Failure }; 
18

  
19
node count (d: int; t: bool) returns (ok: bool);
20

  
21
node command_control__Open_handler_until (command_control__restart_act: bool; millisecond: bool) returns (command_control__restart_in: bool; command_control__state_in: command_control__type; open_gas_out: bool; open_light_out: bool);
22

  
23
function command_control__Open_unless (command_control__restart_in: bool) returns (command_control__restart_act: bool; command_control__state_act: command_control__type);
24

  
25
node command_control__Silent_handler_until (command_control__restart_act: bool; millisecond: bool) returns (command_control__restart_in: bool; command_control__state_in: command_control__type; open_gas_out: bool; open_light_out: bool);
26

  
27
function command_control__Silent_unless (command_control__restart_in: bool) returns (command_control__restart_act: bool; command_control__state_act: command_control__type);
28

  
29
node command (millisecond: bool) returns (open_light: bool; open_gas: bool);
30

  
31
node edge (c: bool) returns (edge_c: bool);
32

  
33
function heat_control__Start_handler_until (heat_control__restart_act: bool) returns (heat_control__restart_in: bool; heat_control__state_in: heat_control__type; ok_out: bool);
34

  
35
function heat_control__Start_unless (heat_control__restart_in: bool; expected_temp: int; actual_temp: int) returns (heat_control__restart_act: bool; heat_control__state_act: heat_control__type);
36

  
37
function heat_control__Stop_handler_until (heat_control__restart_act: bool) returns (heat_control__restart_in: bool; heat_control__state_in: heat_control__type; ok_out: bool);
38

  
39
function heat_control__Stop_unless (heat_control__restart_in: bool; expected_temp: int; actual_temp: int) returns (heat_control__restart_act: bool; heat_control__state_act: heat_control__type);
40

  
41
function light_control__Failure_handler_until (light_control__restart_act: bool) returns (light_control__restart_in: bool; light_control__state_in: light_control__type; nok_out: bool; open_gas_out: bool; open_light_out: bool);
42

  
43
function light_control__Failure_unless (light_control__restart_in: bool) returns (light_control__restart_act: bool; light_control__state_act: light_control__type);
44

  
45
function light_control__Light_off_handler_until (light_control__restart_act: bool; on_heat: bool) returns (light_control__restart_in: bool; light_control__state_in: light_control__type; nok_out: bool; open_gas_out: bool; open_light_out: bool);
46

  
47
function light_control__Light_off_unless (light_control__restart_in: bool) returns (light_control__restart_act: bool; light_control__state_act: light_control__type);
48

  
49
function light_control__Light_on_handler_until (light_control__restart_act: bool; on_heat: bool) returns (light_control__restart_in: bool; light_control__state_in: light_control__type; nok_out: bool; open_gas_out: bool; open_light_out: bool);
50

  
51
function light_control__Light_on_unless (light_control__restart_in: bool) returns (light_control__restart_act: bool; light_control__state_act: light_control__type);
52

  
53
node light_control__Try_handler_until (light_control__restart_act: bool; millisecond: bool; on_light: bool) returns (light_control__restart_in: bool; light_control__state_in: light_control__type; nok_out: bool; open_gas_out: bool; open_light_out: bool);
54

  
55
function light_control__Try_unless (light_control__restart_in: bool) returns (light_control__restart_act: bool; light_control__state_act: light_control__type);
56

  
57
node heat (expected_temp: int; actual_temp: int) returns (ok: bool);
58

  
59
node light (millisecond: bool; on_heat: bool; on_light: bool) returns (open_light: bool; open_gas: bool; nok: bool);
60

  
61
node top (millisecond: bool; reset: bool; expected_temp: int; actual_temp: int; on_light: bool) returns (ok: bool);
62

  
regression_tests/lustre_files/failed/microwave.lus
1
node microwave_basic (start, clear: bool; door_closed: bool; steps_to_cook: int) returns (mode: int);
2
var steps_remaining: int;
3
let
4
  automaton microwave_basic_automaton
5
  state BSETUP :
6
  let
7
    mode = 1;
8
    steps_remaining = steps_to_cook;
9
  tel until start && steps_remaining > 0 restart BRUNNING
10
  
11
  state BRUNNING :
12
--  unless clear && pre mode = 3 restart BSETUP
13
  let
14
    automaton microwave_basic_running
15
    state BRUNNING_ENTRY :
16
    unless door_closed restart BCOOKING
17
    unless not door_closed restart BSUSPENDED
18
    let
19
      -- nothing is computed
20
      mode = 1; -- but this assign is transient and invisible
21
      steps_remaining = pre steps_remaining;
22
    tel
23
    
24
    state BCOOKING :
25
    unless clear || not door_closed restart BSUSPENDED
26
    let
27
      mode = 2;
28
      steps_remaining = pre steps_remaining - 1;
29
    tel
30

  
31
    state BSUSPENDED :
32
    unless start && door_closed restart BCOOKING
33
    let
34
      mode = 3;
35
      steps_remaining = pre steps_remaining;
36
    tel
37
  tel
38
  until steps_remaining <= 0 restart BSETUP
39
  until clear && mode = 3 restart BSETUP
40

  
41
  
42
tel
43

  
44
node push_n_relaxed (kp_0, kp_1, kp_2, kp_3, kp_4, kp_5, kp_6, kp_7, kp_8, kp_9:  bool) returns (ok:  bool; value:  int);
45
var only_one_pushed,  none_pushed:  bool;
46
let
47
  only_one_pushed = 
48
    (kp_0 && not (kp_1 || kp_2 || kp_3 || kp_4 || kp_5 || kp_6 || kp_7 || kp_8 || kp_9)) ||
49
    (kp_1 && not (kp_0 || kp_2 || kp_3 || kp_4 || kp_5 || kp_6 || kp_7 || kp_8 || kp_9)) ||
50
    (kp_2 && not (kp_0 || kp_1 || kp_3 || kp_4 || kp_5 || kp_6 || kp_7 || kp_8 || kp_9)) ||
51
    (kp_3 && not (kp_0 || kp_1 || kp_2 || kp_4 || kp_5 || kp_6 || kp_7 || kp_8 || kp_9)) ||
52
    (kp_4 && not (kp_0 || kp_1 || kp_2 || kp_3 || kp_5 || kp_6 || kp_7 || kp_8 || kp_9)) ||
53
    (kp_5 && not (kp_0 || kp_1 || kp_2 || kp_3 || kp_4 || kp_6 || kp_7 || kp_8 || kp_9)) ||
54
    (kp_6 && not (kp_0 || kp_1 || kp_2 || kp_3 || kp_4 || kp_5 || kp_7 || kp_8 || kp_9)) ||
55
    (kp_7 && not (kp_0 || kp_1 || kp_2 || kp_3 || kp_4 || kp_5 || kp_6 || kp_8 || kp_9)) ||
56
    (kp_8 && not (kp_0 || kp_1 || kp_2 || kp_3 || kp_4 || kp_5 || kp_6 || kp_7 || kp_9)) ||
57
    (kp_9 && not (kp_0 || kp_1 || kp_2 || kp_3 || kp_4 || kp_5 || kp_6 || kp_7 || kp_8 ));
58

  
59
  none_pushed =  not (kp_0 || kp_1 || kp_2 || kp_3 || kp_4 || kp_5 || kp_6 || kp_7 || kp_8 || kp_9);
60

  
61
  ok = only_one_pushed && (true -> pre none_pushed); 
62

  
63
  value = if kp_0 then 0 else if kp_1 then 1 else if kp_2 then 2 else if kp_3
64
          then 3 else if kp_4 then 4 else if kp_5 then 5 else if kp_6 then 6 else
65
          if kp_7 then 7 else if kp_8 then 8 else if kp_9 then 9 else 10;
66

  
67
tel
68

  
69
node keypad (kp_0, kp_1, kp_2, kp_3, kp_4, kp_5, kp_6, kp_7, kp_8, kp_9:  bool) returns (left,  middle,  right:  int);
70
var ok: bool; value: int;
71
let
72
  ok,  value = push_n_relaxed (kp_0, kp_1, kp_2, kp_3, kp_4, kp_5, kp_6, kp_7, kp_8, kp_9);
73
  left,  middle,  right = (0, 0, 0) ->
74
    if ok then
75
      (pre middle,  pre right,  value)
76
    else
77
      (pre left,  pre middle,  pre right);
78
    
79
tel
80

  
81
node microwave (kp_start, kp_clear: bool;
82
                kp_0, kp_1, kp_2, kp_3, kp_4, kp_5, kp_6, kp_7, kp_8, kp_9:  bool;
83
                door_closed:  bool) returns (light_on:  bool);
84
var 
85
  CLEAR_PRESSED, START_PRESSED:  bool; 
86
  steps_remaining, steps_to_cook: int;
87
  left, middle, right: int;
88
mode : int;
89
let
90

  
91
  CLEAR_PRESSED = kp_clear -> (kp_clear and (not (pre kp_clear)));
92
  START_PRESSED = kp_start -> (kp_start and (not (pre kp_start)));
93
  light_on = not door_closed || mode = 2;
94

  
95
  automaton microwave_automaton
96
  state SETUP :
97
  let
98
    mode = 1;
99

  
100
    -- used to setup setps_to_cook
101
    left, middle, right = 
102
      if kp_clear then 
103
        (0, 0, 0) 
104
      else 
105
        keypad (kp_0, kp_1, kp_2, kp_3, kp_4, kp_5, kp_6, kp_7, kp_8, kp_9);
106
  
107
    steps_to_cook = right + middle * 10  + left * 60;
108
  
109
    steps_remaining = steps_to_cook;
110
  
111
  tel until START_PRESSED && steps_remaining > 0 restart RUNNING
112
  
113
  state RUNNING :
114
 -- unless CLEAR_PRESSED && mode = 3 restart SETUP
115
  let
116
    -- we print current remaining steps
117
    left = steps_remaining div 60;
118
    middle = (steps_remaining - (left * 60)) div 10;
119
    right = steps_remaining - (left * 60) - (middle * 10);
120
    steps_to_cook = pre steps_to_cook;
121

  
122
    -- running automaton
123
    automaton microwave_running
124
    state RUNNING_ENTRY :
125
    unless door_closed restart COOKING
126
    unless not door_closed restart SUSPENDED
127
    let
128
      -- nothing is computed
129
      mode = 1; -- but this assign is transient and invisible
130
      steps_remaining = pre steps_remaining;
131
    tel
132
    
133
    state COOKING :
134
    unless CLEAR_PRESSED || not door_closed restart SUSPENDED
135
    let
136
      mode = 2;
137
      steps_remaining = pre steps_remaining - 1;
138
    tel
139

  
140
    state SUSPENDED :			
141
    unless START_PRESSED && door_closed restart COOKING
142
    let
143
      mode = 3;
144
      steps_remaining = pre steps_remaining;
145
    tel
146
  tel
147
  until steps_remaining <= 0 restart SETUP
148
  until CLEAR_PRESSED && mode = 3 restart SETUP
149
tel
regression_tests/lustre_files/failed/microwave.lusi
1
(* Generated Lustre Interface file from microwave.lus *)
2
(* by Lustre-C compiler version 1.3-458, 2016/10/21, 12:58:32 *)
3
(* Feel free to mask some of the definitions by removing them from this file. *)
4

  
5
type microwave_basic_automaton__type = enum {BSETUP, BRUNNING }; 
6

  
7
type microwave_basic_running__type = enum {BRUNNING_ENTRY, BCOOKING, BSUSPENDED };
8

  
9

  
10
type microwave_automaton__type = enum {SETUP, RUNNING }; 
11

  
12
type microwave_running__type = enum {RUNNING_ENTRY, COOKING, SUSPENDED }; 
13

  
14
node push_n_relaxed (kp_0: bool; kp_1: bool; kp_2: bool; kp_3: bool; kp_4: bool; kp_5: bool; kp_6: bool; kp_7: bool; kp_8: bool; kp_9: bool) returns (ok: bool; value: int);
15

  
16
node microwave_basic_running__BCOOKING_handler_until (microwave_basic_running__restart_act: bool) returns (microwave_basic_running__restart_in: bool; microwave_basic_running__state_in: microwave_basic_running__type; _mode_out_1: int; _steps_remaining_out_1: int);
17

  
18
function microwave_basic_running__BCOOKING_unless (microwave_basic_running__restart_in: bool; clear: bool; door_closed: bool) returns (microwave_basic_running__restart_act: bool; microwave_basic_running__state_act: microwave_basic_running__type);
19

  
20
node microwave_basic_running__BRUNNING_ENTRY_handler_until (microwave_basic_running__restart_act: bool) returns (microwave_basic_running__restart_in: bool; microwave_basic_running__state_in: microwave_basic_running__type; _mode_out_1: int; _steps_remaining_out_1: int);
21

  
22
function microwave_basic_running__BRUNNING_ENTRY_unless (microwave_basic_running__restart_in: bool; door_closed: bool) returns (microwave_basic_running__restart_act: bool; microwave_basic_running__state_act: microwave_basic_running__type);
23

  
24
node microwave_basic_running__BSUSPENDED_handler_until (microwave_basic_running__restart_act: bool) returns (microwave_basic_running__restart_in: bool; microwave_basic_running__state_in: microwave_basic_running__type; _mode_out_1: int; _steps_remaining_out_1: int);
25

  
26
function microwave_basic_running__BSUSPENDED_unless (microwave_basic_running__restart_in: bool; start: bool; door_closed: bool) returns (microwave_basic_running__restart_act: bool; microwave_basic_running__state_act: microwave_basic_running__type);
27

  
28
node microwave_running__COOKING_handler_until (microwave_running__restart_act: bool) returns (microwave_running__restart_in: bool; microwave_running__state_in: microwave_running__type; _mode_out_1: int; _steps_remaining_out_1: int);
29

  
30
function microwave_running__COOKING_unless (microwave_running__restart_in: bool; door_closed: bool; CLEAR_PRESSED: bool) returns (microwave_running__restart_act: bool; microwave_running__state_act: microwave_running__type);
31

  
32
node microwave_running__RUNNING_ENTRY_handler_until (microwave_running__restart_act: bool) returns (microwave_running__restart_in: bool; microwave_running__state_in: microwave_running__type; _mode_out_1: int; _steps_remaining_out_1: int);
33

  
34
function microwave_running__RUNNING_ENTRY_unless (microwave_running__restart_in: bool; door_closed: bool) returns (microwave_running__restart_act: bool; microwave_running__state_act: microwave_running__type);
35

  
36
node microwave_running__SUSPENDED_handler_until (microwave_running__restart_act: bool) returns (microwave_running__restart_in: bool; microwave_running__state_in: microwave_running__type; _mode_out_1: int; _steps_remaining_out_1: int);
37

  
38
function microwave_running__SUSPENDED_unless (microwave_running__restart_in: bool; door_closed: bool; START_PRESSED: bool) returns (microwave_running__restart_act: bool; microwave_running__state_act: microwave_running__type);
39

  
40
node keypad (kp_0: bool; kp_1: bool; kp_2: bool; kp_3: bool; kp_4: bool; kp_5: bool; kp_6: bool; kp_7: bool; kp_8: bool; kp_9: bool) returns (left: int; middle: int; right: int);
41

  
42
node microwave_basic_automaton__BRUNNING_handler_until (microwave_basic_automaton__restart_act: bool; start: bool; clear: bool; door_closed: bool) returns (microwave_basic_automaton__restart_in: bool; microwave_basic_automaton__state_in: microwave_basic_automaton__type; mode_out: int; steps_remaining_out: int);
43

  
44
function microwave_basic_automaton__BRUNNING_unless (microwave_basic_automaton__restart_in: bool) returns (microwave_basic_automaton__restart_act: bool; microwave_basic_automaton__state_act: microwave_basic_automaton__type);
45

  
46
function microwave_basic_automaton__BSETUP_handler_until (microwave_basic_automaton__restart_act: bool; start: bool; steps_to_cook: int) returns (microwave_basic_automaton__restart_in: bool; microwave_basic_automaton__state_in: microwave_basic_automaton__type; mode_out: int; steps_remaining_out: int);
47

  
48
function microwave_basic_automaton__BSETUP_unless (microwave_basic_automaton__restart_in: bool) returns (microwave_basic_automaton__restart_act: bool; microwave_basic_automaton__state_act: microwave_basic_automaton__type);
49

  
50
node microwave_automaton__RUNNING_handler_until (microwave_automaton__restart_act: bool; door_closed: bool; CLEAR_PRESSED: bool; START_PRESSED: bool) returns (microwave_automaton__restart_in: bool; microwave_automaton__state_in: microwave_automaton__type; left_out: int; middle_out: int; mode_out: int; right_out: int; steps_remaining_out: int; steps_to_cook_out: int);
51

  
52
function microwave_automaton__RUNNING_unless (microwave_automaton__restart_in: bool) returns (microwave_automaton__restart_act: bool; microwave_automaton__state_act: microwave_automaton__type);
53

  
54
node microwave_automaton__SETUP_handler_until (microwave_automaton__restart_act: bool; kp_clear: bool; kp_0: bool; kp_1: bool; kp_2: bool; kp_3: bool; kp_4: bool; kp_5: bool; kp_6: bool; kp_7: bool; kp_8: bool; kp_9: bool; START_PRESSED: bool) returns (microwave_automaton__restart_in: bool; microwave_automaton__state_in: microwave_automaton__type; left_out: int; middle_out: int; mode_out: int; right_out: int; steps_remaining_out: int; steps_to_cook_out: int);
55

  
56
function microwave_automaton__SETUP_unless (microwave_automaton__restart_in: bool) returns (microwave_automaton__restart_act: bool; microwave_automaton__state_act: microwave_automaton__type);
57

  
58
node microwave_basic (start: bool; clear: bool; door_closed: bool; steps_to_cook: int) returns (mode: int);
59

  
60
node microwave (kp_start: bool; kp_clear: bool; kp_0: bool; kp_1: bool; kp_2: bool; kp_3: bool; kp_4: bool; kp_5: bool; kp_6: bool; kp_7: bool; kp_8: bool; kp_9: bool; door_closed: bool) returns (light_on: bool);
61

  
regression_tests/lustre_files/failed/microwave_microwave_input_values
1
1
2
0
3
0
4
0
5
0
6
1
7
0
8
0
9
1
10
0
11
1
12
0
13
0
14
0
15
1
16
0
17
1
18
0
19
1
20
0
21
0
22
0
23
0
24
1
25
0
26
1
27
1
28
1
29
0
30
0
31
0
32
1
33
0
34
0
35
0
36
0
37
1
38
1
39
0
40
0
41
0
42
0
43
0
44
0
45
0
46
0
47
0
48
0
49
0
50
1
51
1
52
1
53
0
54
0
55
1
56
1
57
0
58
1
59
1
60
0
61
1
62
1
63
1
64
1
65
1
66
0
67
0
68
0
69
1
70
1
71
0
72
0
73
1
74
0
75
1
76
0
77
1
78
1
79
1
80
1
81
1
82
1
83
0
84
0
85
0
86
1
87
0
88
1
89
1
90
1
91
1
92
1
93
0
94
0
95
1
96
1
97
0
98
0
99
1
100
0
regression_tests/lustre_files/failed/tawoa_automata.lus
1

  
2
node tawoa_automata(input : int) returns (ok: bool);
3
var x1,  x2 : int;
4
    y1, y2:int; 
5
let
6
  automaton aut1
7
  state A :
8
  let
9
     x1 = input;
10
     y1 = x2;
11
  tel
12
  until true restart B
13
  state B :
14
  let
15
    x1 = 1; --    x1 = x2;
16
    y1 = 1;
17
  tel
18
  until true restart A
19
  automaton aut2
20
  state C :
21
  let
22
    x2 = x1;
23
    y2 = 2;
24
  tel
25
  until true restart D
26
  state D :
27
  let
28
    x2 = input;
29
y2 = x2;   -- y2 = x1;
30
  tel
31
  until true restart C
32

  
33
  ok = y1 = input || y2 = input;
34
tel
regression_tests/lustre_files/failed/tawoa_automata.lusi
1
(* Generated Lustre Interface file from tawoa_automata.lus *)
2
(* by Lustre-C compiler version 1.3-458, 2016/10/21, 12:58:32 *)
3
(* Feel free to mask some of the definitions by removing them from this file. *)
4

  
5
type aut2__type = enum {C, D }; 
6

  
7
type aut1__type = enum {A, B }; 
8

  
9
function aut1__A_handler_until (aut1__restart_act: bool; input: int; x2: int) returns (aut1__restart_in: bool; aut1__state_in: aut1__type; x1_out: int; y1_out: int);
10

  
11
function aut1__A_unless (aut1__restart_in: bool) returns (aut1__restart_act: bool; aut1__state_act: aut1__type);
12

  
13
function aut1__B_handler_until (aut1__restart_act: bool) returns (aut1__restart_in: bool; aut1__state_in: aut1__type; x1_out: int; y1_out: int);
14

  
15
function aut1__B_unless (aut1__restart_in: bool) returns (aut1__restart_act: bool; aut1__state_act: aut1__type);
16

  
17
function aut2__C_handler_until (aut2__restart_act: bool; x1: int) returns (aut2__restart_in: bool; aut2__state_in: aut2__type; x2_out: int; y2_out: int);
18

  
19
function aut2__C_unless (aut2__restart_in: bool) returns (aut2__restart_act: bool; aut2__state_act: aut2__type);
20

  
21
function aut2__D_handler_until (aut2__restart_act: bool; input: int) returns (aut2__restart_in: bool; aut2__state_in: aut2__type; x2_out: int; y2_out: int);
22

  
23
function aut2__D_unless (aut2__restart_in: bool) returns (aut2__restart_act: bool; aut2__state_act: aut2__type);
24

  
25
node tawoa_automata (input: int) returns (ok: bool);
26

  
regression_tests/lustre_files/failed/tawoa_automata_tawoa_automata_input_values
1
74
2
96
3
92
4
12
5
72
6
57
7
66
8
8
9
6
10
58
11
16
12
5
13
1
14
60
15
81
16
9
17
15
18
92
19
97
20
57
21
8
22
93
23
7
24
39
25
37
26
27
27
4
28
71
29
58
30
98
31
26
32
94
33
91
34
49
35
41
36
61
37
78
38
86
39
33
40
87
41
21
42
66
43
9
44
29
45
84
46
67
47
44
48
23
49
99
50
58
51
95
52
53
53
7
54
95
55
55
56
0
57
50
58
16
59
89
60
72
61
95
62
82
63
8
64
5
65
59
66
83
67
89
68
35
69
46
70
46
71
10
72
62
73
96
74
13
75
74
76
88
77
89
78
96
79
62
80
54
81
68
82
3
83
26
84
73
85
0
86
81
87
54
88
67
89
60
90
29
91
55
92
97
93
29
94
14
95
86
96
70
97
93
98
96
99
92
100
81
regression_tests/lustre_files/failed/test_nok.lus
1
node top (x:bool) returns (ok: bool);
2
var bit: bool;
3
    coin: bool;
4
let
5
  automaton mini_states
6
  state Even : 
7
  let 
8
    bit = true;
9
  tel until true restart Odd
10
  state Odd : 
11
  let 
12
    bit = false;
13
  tel until true restart Even
14

  
15
  coin = true -> not pre coin;
16
  ok = bit = not coin;
17
tel
18

  
regression_tests/lustre_files/failed/test_nok.lusi
1
(* Generated Lustre Interface file from test_nok.lus *)
2
(* by Lustre-C compiler version 1.3-458, 2016/10/21, 12:58:27 *)
3
(* Feel free to mask some of the definitions by removing them from this file. *)
4

  
5
type mini_states__type = enum {Even, Odd }; 
6

  
7
function mini_states__Even_handler_until (mini_states__restart_act: bool) returns (mini_states__restart_in: bool; mini_states__state_in: mini_states__type; bit_out: bool);
8

  
9
function mini_states__Even_unless (mini_states__restart_in: bool) returns (mini_states__restart_act: bool; mini_states__state_act: mini_states__type);
10

  
11
function mini_states__Odd_handler_until (mini_states__restart_act: bool) returns (mini_states__restart_in: bool; mini_states__state_in: mini_states__type; bit_out: bool);
12

  
13
function mini_states__Odd_unless (mini_states__restart_in: bool) returns (mini_states__restart_act: bool; mini_states__state_act: mini_states__type);
14

  
15
node top (x: bool) returns (ok: bool);
16

  
regression_tests/lustre_files/failed/test_nok_top__output_values
1
'ok': '0' 
2
'ok': '0' 
3
'ok': '0' 
4
'ok': '0' 
5
'ok': '0' 
6
'ok': '0' 
7
'ok': '0' 
8
'ok': '0' 
9
'ok': '0' 
10
'ok': '0' 
11
'ok': '0' 
12
'ok': '0' 
13
'ok': '0' 
14
'ok': '0' 
15
'ok': '0' 
16
'ok': '0' 
17
'ok': '0' 
18
'ok': '0' 
19
'ok': '0' 
20
'ok': '0' 
21
'ok': '0' 
22
'ok': '0' 
23
'ok': '0' 
24
'ok': '0' 
25
'ok': '0' 
26
'ok': '0' 
27
'ok': '0' 
28
'ok': '0' 
29
'ok': '0' 
30
'ok': '0' 
31
'ok': '0' 
32
'ok': '0' 
33
'ok': '0' 
34
'ok': '0' 
35
'ok': '0' 
36
'ok': '0' 
37
'ok': '0' 
38
'ok': '0' 
39
'ok': '0' 
40
'ok': '0' 
41
'ok': '0' 
42
'ok': '0' 
43
'ok': '0' 
44
'ok': '0' 
45
'ok': '0' 
46
'ok': '0' 
47
'ok': '0' 
48
'ok': '0' 
49
'ok': '0' 
50
'ok': '0' 
51
'ok': '0' 
52
'ok': '0' 
53
'ok': '0' 
54
'ok': '0' 
55
'ok': '0' 
56
'ok': '0' 
57
'ok': '0' 
58
'ok': '0' 
59
'ok': '0' 
60
'ok': '0' 
61
'ok': '0' 
62
'ok': '0' 
63
'ok': '0' 
64
'ok': '0' 
65
'ok': '0' 
66
'ok': '0' 
67
'ok': '0' 
68
'ok': '0' 
69
'ok': '0' 
70
'ok': '0' 
71
'ok': '0' 
72
'ok': '0' 
73
'ok': '0' 
74
'ok': '0' 
75
'ok': '0' 
76
'ok': '0' 
77
'ok': '0' 
78
'ok': '0' 
79
'ok': '0' 
80
'ok': '0' 
81
'ok': '0' 
82
'ok': '0' 
83
'ok': '0' 
84
'ok': '0' 
85
'ok': '0' 
86
'ok': '0' 
87
'ok': '0' 
88
'ok': '0' 
89
'ok': '0' 
90
'ok': '0' 
91
'ok': '0' 
92
'ok': '0' 
93
'ok': '0' 
94
'ok': '0' 
95
'ok': '0' 
96
'ok': '0' 
97
'ok': '0' 
98
'ok': '0' 
99
'ok': '0' 
100
'ok': '0' 
regression_tests/lustre_files/failed/test_nok_top__timeout60_xml.xml
1
<?xml version="1.0"?>
2
   <Results xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance">
3
     <Property name="top">
4
      <Date>2016-11-30 00:18</Date>
5
      <Lustre2Horn unit="sec">0.00</Lustre2Horn>
6
      <Parse unit="sec">0.00</Parse>
7
      <Query unit="sec">0.05</Query>
8
      <Answer>CEX</Answer>
9
      <Counterexample>
10
         <Node name ="top">
11
            <Stream name="top.x" type="unk">
12
                <Value instant="0">1</Value>
13
           </Stream>
14
            <Stream name="top.__top_14_c" type="unk">
15
                <Value instant="0">Even</Value>
16
           </Stream>
17
            <Stream name="top.__top_2_x" type="unk">
18
                <Value instant="0">1</Value>
19
           </Stream>
20
            <Stream name="top.__top_13_x" type="unk">
21
                <Value instant="0">1</Value>
22
           </Stream>
23
            <Stream name="top.__top_14_x" type="unk">
24
                <Value instant="0">Odd</Value>
25
           </Stream>
26
            <Stream name="top.__top_2_c" type="unk">
27
                <Value instant="0">1</Value>
28
           </Stream>
29
            <Stream name="top.ok" type="unk">
30
                <Value instant="0">1</Value>
31
           </Stream>
32
            <Stream name="top.__top_13_c" type="unk">
33
                <Value instant="0">1</Value>
34
           </Stream>
35
         </Node>
36
 <Node name ="mini_states__Even_unless">
37
            <Stream name="mini_states__Even_unless.mini_states__restart_act" type="unk">
38
                <Value instant="0">1</Value>
39
           </Stream>
40
            <Stream name="mini_states__Even_unless.mini_states__state_act" type="unk">
41
                <Value instant="0">Even</Value>
42
           </Stream>
43
            <Stream name="mini_states__restart_in" type="bool">
44
                <Value instant="0">1</Value>
45
           </Stream>
46
         </Node>
47
 <Node name ="mini_states__Even_handler_until">
48
            <Stream name="mini_states__Even_handler_until.mini_states__restart_in" type="unk">
49
                <Value instant="0">1</Value>
50
           </Stream>
51
            <Stream name="mini_states__Even_handler_until.bit_out" type="unk">
52
                <Value instant="0">1</Value>
53
           </Stream>
54
            <Stream name="mini_states__Even_handler_until.mini_states__restart_act" type="unk">
55
                <Value instant="0">1</Value>
56
           </Stream>
57
            <Stream name="mini_states__Even_handler_until.mini_states__state_in" type="unk">
58
                <Value instant="0">Odd</Value>
59
           </Stream>
60
         </Node>
61

  
62
      </Counterexample>
63
     </Property>
64
   </Results>
65

  
... This diff was truncated because it exceeds the maximum size that can be displayed.

Also available in: Unified diff