CristalCaveGem » LustreC » Lustrec-Tests

node top (x :int) returns (y:bool) 

var l:int;

let

 automaton parity

 state Even :

 unless (x mod 2 = 1) restart Odd

 let

   l = x -> pre (l/2);

 tel

 state Odd  :

 unless (x mod 2 = 0) restart Even

 let

  l = x -> pre (3*l + 1);

 tel

 y = (l = 1);

tel

(* Generated Lustre Interface file from aut1.lus *)

(* by Lustre-C compiler version 1.3-458, 2016/10/21, 12:58:29 *)

(* Feel free to mask some of the definitions by removing them from this file. *)

type parity__type = enum {Even, Odd }; 

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

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

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

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

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

'y': '0' 

'y': '0' 

'y': '0' 

'y': '1' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '1' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '1' 

'y': '0' 

'y': '0' 

'y': '1' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '1' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

'y': '0' 

<?xml version="1.0"?>

   <Results xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance">

     <Property name="top">

      <Date>2016-11-30 00:18</Date>

      <Lustre2Horn unit="sec">0.00</Lustre2Horn>

      <Parse unit="sec">0.00</Parse>

      <Query unit="sec">0.09</Query>

      <Answer>CEX</Answer>

      <Counterexample>

         <Node name ="parity__Even_unless">

            <Stream name="parity__Even_unless.parity__restart_act" type="unk">

                <Value instant="0">1</Value>

           </Stream>

            <Stream name="parity__Even_unless.parity__state_act" type="unk">

                <Value instant="0">Even</Value>

           </Stream>

            <Stream name="parity__Even_unless.parity__restart_in" type="unk">

                <Value instant="0">1</Value>

           </Stream>

            <Stream name="parity__Even_unless.x" type="unk">

                <Value instant="0">0</Value>

           </Stream>

         </Node>

 <Node name ="top">

            <Stream name="top.__top_13_x" type="unk">

                <Value instant="0">Even</Value>

           </Stream>

            <Stream name="top.__top_13_x" type="unk">

                <Value instant="0">Even</Value>

           </Stream>

            <Stream name="top.__top_12_x" type="unk">

                <Value instant="0">1</Value>

           </Stream>

            <Stream name="top.ni_1.parity__Odd_handler_until.__parity__Odd_handler_until_2_c" type="unk">

                <Value instant="0">5</Value>

           </Stream>

            <Stream name="top.ni_0.parity__Even_handler_until.__parity__Even_handler_until_2_x" type="unk">

                <Value instant="0">0</Value>

           </Stream>

            <Stream name="top.ni_1.parity__Odd_handler_until.__parity__Odd_handler_until_2_x" type="unk">

                <Value instant="0">0</Value>

           </Stream>

            <Stream name="top.__top_12_c" type="unk">

                <Value instant="0">1</Value>

           </Stream>

            <Stream name="y" type="bool">

                <Value instant="0">1</Value>

           </Stream>

            <Stream name="x" type="int">

                <Value instant="0">0</Value>

           </Stream>

            <Stream name="top.__top_13_c" type="unk">

                <Value instant="0">Even</Value>

           </Stream>

         </Node>

 <Node name ="parity__Even_handler_until">

            <Stream name="parity__Even_handler_until.l_out" type="unk">

                <Value instant="0">0</Value>

           </Stream>

            <Stream name="parity__Even_handler_until.parity__restart_in" type="unk">

                <Value instant="0">1</Value>

           </Stream>

            <Stream name="parity__Even_handler_until.__parity__Even_handler_until_2_x" type="unk">

                <Value instant="0">0</Value>

           </Stream>

            <Stream name="parity__Even_handler_until.parity__state_in" type="unk">

                <Value instant="0">Even</Value>

           </Stream>

            <Stream name="parity__Even_handler_until.x" type="unk">

                <Value instant="0">0</Value>

           </Stream>

            <Stream name="parity__Even_handler_until.__parity__Even_handler_until_2_c" type="unk">

                <Value instant="0">6</Value>

           </Stream>

            <Stream name="parity__Even_handler_until.parity__restart_act" type="unk">

                <Value instant="0">1</Value>

           </Stream>

         </Node>

      </Counterexample>

     </Property>

   </Results>

49

6

58

44

98

41

15

89

79

51

70

29

29

49

17

94

37

86

1

84

67

62

87

67

49

70

67

25

32

5

84

52

98

8

69

40

11

34

10

46

29

18

67

78

40

65

30

19

40

67

45

5

22

2

95

18

6

12

96

41

14

91

52

81

28

2

53

79

49

62

1

4

6

94

37

63

57

13

17

94

6

95

74

86

93

15

90

0

87

24

56

80

48

94

23

43

54

24

33

17

  type parity__type = enum {Even, Odd };

  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)

var __parity__Odd_unless_1: bool;

let

    parity__restart_act, parity__state_act = (if __parity__Odd_unless_1 then (true,Even) else (parity__restart_in,parity__state_in));

    __parity__Odd_unless_1 = ((l mod 2) = 0);

tel

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)

var __parity__Odd_handler_until_2: int;

    __parity__Odd_handler_until_1: bool;

    l: int;

let

    parity__restart_in, parity__state_in = (parity__restart_act,parity__state_act);

    l_out = l;

    l = (if __parity__Odd_handler_until_1 then x else __parity__Odd_handler_until_2);

    __parity__Odd_handler_until_2 = pre ((3 * l) + 1);

    __parity__Odd_handler_until_1 = (true -> false);

tel

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)

var __parity__Even_unless_1: bool;

let

    parity__restart_act, parity__state_act = (if __parity__Even_unless_1 then (true,Odd) else (parity__restart_in,parity__state_in));

    __parity__Even_unless_1 = ((l mod 2) = 1);

tel

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)

var __parity__Even_handler_until_2: int;

    __parity__Even_handler_until_1: bool;

    l: int;

let

    parity__restart_in, parity__state_in = (parity__restart_act,parity__state_act);

    l_out = l;

    l = (if __parity__Even_handler_until_1 then x else __parity__Even_handler_until_2);

    __parity__Even_handler_until_2 = pre (l / 2);

    __parity__Even_handler_until_1 = (true -> false);

tel

node top (x: int) returns (y: bool)

var __test1_12: bool;

    __test1_13: parity__type;

    __test1_11: bool;

    __test1_8: bool;

    __test1_9: parity__type;

    __test1_10: int;

    __test1_5: bool;

    __test1_6: parity__type;

    __test1_7: int;

    __test1_3: bool;

    __test1_4: parity__type;

    __test1_1: bool;

    __test1_2: parity__type;

    parity__next_restart_in: bool;

    parity__restart_in: bool;

    parity__restart_act: bool;

    parity__next_state_in: parity__type;

    parity__state_in: parity__type clock;

    parity__state_act: parity__type clock;

    l: int;

let

    parity__restart_in, parity__state_in = (if __test1_11 then (false,Even) else (__test1_12,__test1_13));

    __test1_12, __test1_13 = pre (parity__next_restart_in,parity__next_state_in);

    __test1_11 = (true -> false);

    parity__next_restart_in, parity__next_state_in, l = merge parity__state_act (Even -> (__test1_8,__test1_9,__test1_10))

                                                                                (Odd -> (__test1_5,__test1_6,__test1_7));

    __test1_8, __test1_9, __test1_10 = parity__Even_handler_until (parity__restart_act when Even(parity__state_act),

                                                                   parity__state_act when Even(parity__state_act),

                                                                   x when Even(parity__state_act))

                                       every (parity__restart_act);

    __test1_5, __test1_6, __test1_7 = parity__Odd_handler_until (parity__restart_act when Odd(parity__state_act),

                                                                 parity__state_act when Odd(parity__state_act),

                                                                 x when Odd(parity__state_act))

                                      every (parity__restart_act);

    parity__restart_act, parity__state_act = merge parity__state_in (Even -> (__test1_3,__test1_4))

                                                                    (Odd -> (__test1_1,__test1_2));

    __test1_3, __test1_4 = parity__Even_unless (parity__restart_in when Even(parity__state_in),

                                                parity__state_in when Even(parity__state_in),

                                                l when Even(parity__state_in))

                           every (parity__restart_in);

    __test1_1, __test1_2 = parity__Odd_unless (parity__restart_in when Odd(parity__state_in),

                                               parity__state_in when Odd(parity__state_in),

                                               l when Odd(parity__state_in))

                           every (parity__restart_in);

    y = (l = 1);

tel

(* Generated Lustre Interface file from aut2.lus *)

(* by Lustre-C compiler version 1.3-458, 2016/10/21, 12:58:30 *)

(* Feel free to mask some of the definitions by removing them from this file. *)

type parity__type = enum {Even, Odd }; 

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

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

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

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

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

91

45

85

83

27

22

75

8

76

70

44

55

9

63

74

15

62

21

57

86

89

94

97

21

19

19

52

5

57

88

77

62

66

59

8

87

27

74

82

23

54

53

46

63

42

14

66

60

95

34

88

51

14

54

92

40

67

40

15

64

10

90

86

43

30

39

33

86

57

74

31

55

54

41

91

43

8

13

45

33

22

31

83

29

33

33

88

66

82

19

50

29

35

77

72

12

10

63

75

56

const low = 5;

const high = 5;

const delay_on = 200;

const delay_off = 500;

node edge(c : bool) returns (edge_c : bool)

let

  edge_c = false -> c && not (pre c);

tel

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

var cpt:int;

let

  ok = (cpt = 0);

  cpt = 0 -> (if t then pre cpt + 1 else pre cpt) mod d;

tel

(* controling the heat *)

(* returns [true] when [expected_temp] does not agree with [actual_temp] *)

node heat(expected_temp, actual_temp : int) returns (ok : bool)

let

  automaton heat_control

    state Stop :

          unless (actual_temp <= expected_temp - low) resume Start

          let

            ok = false; 

          tel

    state Start :

          unless (actual_temp >= expected_temp + high) resume Stop

          let

            ok = true;

          tel

tel

(* a cyclic two mode automaton with an internal timer *)

(* [open_light = true] and [open_gas = true] for [delay_on millisecond] *)

(* then [open_light = false] and [open_gas = false] for *)

(* [delay_off millisecond] *)

node command(millisecond : bool) returns (open_light, open_gas : bool)

let

  automaton command_control

    state Open :

          let

            open_light = true;

            open_gas = true;

          tel

          until count(delay_on, millisecond) restart Silent

    state Silent :

          let

            open_light = false;

            open_gas = false;

          tel

          until count(delay_off, millisecond) restart Open

tel

(* the main command which control the opening of the light and gas *)

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

let

  automaton light_control

    state Light_off :

          let

            nok = false;

            open_light = false;

            open_gas = false;

          tel

          until on_heat restart Try

    state Light_on :

          let

            nok = false;

            open_light = false;

            open_gas = true;

          tel

          until not on_heat restart Light_off

    state Try :

          let

            nok = false;

            (open_light, open_gas) = command(millisecond);

          tel

          until on_light restart Light_on

          until count(3, edge(not open_light)) restart Failure

    state Failure :

          let

            nok = true; 

            open_light = false;

            open_gas = false;

          tel

tel

(* the main function *)

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

var on_heat, nok , open_light, open_gas: bool;

let

  on_heat = heat(expected_temp,actual_temp) every reset;

  (open_light, open_gas, nok) = light(millisecond, on_heat, on_light) every reset;

  ok = not nok;

tel

(* Generated Lustre Interface file from heater.lus *)

(* by Lustre-C compiler version 1.3-458, 2016/10/21, 12:58:29 *)

(* Feel free to mask some of the definitions by removing them from this file. *)

const low = 5;

const high = 5;

const delay_on = 200;

const delay_off = 500;

type heat_control__type = enum {Stop, Start }; 

type command_control__type = enum {Open, Silent }; 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

var steps_remaining: int;

let

  automaton microwave_basic_automaton

  state BSETUP :

  let

    mode = 1;

    steps_remaining = steps_to_cook;

  tel until start && steps_remaining > 0 restart BRUNNING

  state BRUNNING :

--  unless clear && pre mode = 3 restart BSETUP

  let

    automaton microwave_basic_running

    state BRUNNING_ENTRY :

    unless door_closed restart BCOOKING

    unless not door_closed restart BSUSPENDED

    let

      -- nothing is computed

      mode = 1; -- but this assign is transient and invisible

      steps_remaining = pre steps_remaining;

    tel

    state BCOOKING :

    unless clear || not door_closed restart BSUSPENDED

    let

      mode = 2;

      steps_remaining = pre steps_remaining - 1;

    tel

    state BSUSPENDED :

    unless start && door_closed restart BCOOKING

    let

      mode = 3;

      steps_remaining = pre steps_remaining;

    tel

  tel

  until steps_remaining <= 0 restart BSETUP

  until clear && mode = 3 restart BSETUP

tel

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

var only_one_pushed,  none_pushed:  bool;

let

  only_one_pushed = 

    (kp_0 && not (kp_1 || kp_2 || kp_3 || kp_4 || kp_5 || kp_6 || kp_7 || kp_8 || kp_9)) ||

    (kp_1 && not (kp_0 || kp_2 || kp_3 || kp_4 || kp_5 || kp_6 || kp_7 || kp_8 || kp_9)) ||

    (kp_2 && not (kp_0 || kp_1 || kp_3 || kp_4 || kp_5 || kp_6 || kp_7 || kp_8 || kp_9)) ||

    (kp_3 && not (kp_0 || kp_1 || kp_2 || kp_4 || kp_5 || kp_6 || kp_7 || kp_8 || kp_9)) ||

    (kp_4 && not (kp_0 || kp_1 || kp_2 || kp_3 || kp_5 || kp_6 || kp_7 || kp_8 || kp_9)) ||

    (kp_5 && not (kp_0 || kp_1 || kp_2 || kp_3 || kp_4 || kp_6 || kp_7 || kp_8 || kp_9)) ||

    (kp_6 && not (kp_0 || kp_1 || kp_2 || kp_3 || kp_4 || kp_5 || kp_7 || kp_8 || kp_9)) ||

    (kp_7 && not (kp_0 || kp_1 || kp_2 || kp_3 || kp_4 || kp_5 || kp_6 || kp_8 || kp_9)) ||

    (kp_8 && not (kp_0 || kp_1 || kp_2 || kp_3 || kp_4 || kp_5 || kp_6 || kp_7 || kp_9)) ||

    (kp_9 && not (kp_0 || kp_1 || kp_2 || kp_3 || kp_4 || kp_5 || kp_6 || kp_7 || kp_8 ));

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

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

  value = if kp_0 then 0 else if kp_1 then 1 else if kp_2 then 2 else if kp_3

          then 3 else if kp_4 then 4 else if kp_5 then 5 else if kp_6 then 6 else

          if kp_7 then 7 else if kp_8 then 8 else if kp_9 then 9 else 10;

tel

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

var ok: bool; value: int;

let

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

  left,  middle,  right = (0, 0, 0) ->

    if ok then

      (pre middle,  pre right,  value)

    else

      (pre left,  pre middle,  pre right);

tel

node microwave (kp_start, kp_clear: bool;

                kp_0, kp_1, kp_2, kp_3, kp_4, kp_5, kp_6, kp_7, kp_8, kp_9:  bool;

                door_closed:  bool) returns (light_on:  bool);

var 

  CLEAR_PRESSED, START_PRESSED:  bool; 

  steps_remaining, steps_to_cook: int;

  left, middle, right: int;

mode : int;

let

  CLEAR_PRESSED = kp_clear -> (kp_clear and (not (pre kp_clear)));

  START_PRESSED = kp_start -> (kp_start and (not (pre kp_start)));

  light_on = not door_closed || mode = 2;

  automaton microwave_automaton

  state SETUP :

  let

    mode = 1;

    -- used to setup setps_to_cook

    left, middle, right = 

      if kp_clear then 

        (0, 0, 0) 

      else 

        keypad (kp_0, kp_1, kp_2, kp_3, kp_4, kp_5, kp_6, kp_7, kp_8, kp_9);

    steps_to_cook = right + middle * 10  + left * 60;

    steps_remaining = steps_to_cook;

  tel until START_PRESSED && steps_remaining > 0 restart RUNNING

  state RUNNING :

 -- unless CLEAR_PRESSED && mode = 3 restart SETUP

  let

    -- we print current remaining steps

    left = steps_remaining div 60;

    middle = (steps_remaining - (left * 60)) div 10;

    right = steps_remaining - (left * 60) - (middle * 10);

    steps_to_cook = pre steps_to_cook;

    -- running automaton

    automaton microwave_running

    state RUNNING_ENTRY :

    unless door_closed restart COOKING

    unless not door_closed restart SUSPENDED

    let

      -- nothing is computed

      mode = 1; -- but this assign is transient and invisible

      steps_remaining = pre steps_remaining;

    tel

    state COOKING :

    unless CLEAR_PRESSED || not door_closed restart SUSPENDED

    let

      mode = 2;

      steps_remaining = pre steps_remaining - 1;

    tel

    state SUSPENDED :			

    unless START_PRESSED && door_closed restart COOKING

    let

      mode = 3;

      steps_remaining = pre steps_remaining;

    tel

  tel

  until steps_remaining <= 0 restart SETUP

  until CLEAR_PRESSED && mode = 3 restart SETUP

tel

(* Generated Lustre Interface file from microwave.lus *)

(* by Lustre-C compiler version 1.3-458, 2016/10/21, 12:58:32 *)

(* Feel free to mask some of the definitions by removing them from this file. *)

type microwave_basic_automaton__type = enum {BSETUP, BRUNNING }; 

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

type microwave_automaton__type = enum {SETUP, RUNNING }; 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1

0

0

0

0

1

0

0

1

0

1

0

0

0

1

0

1

0

1

0

0

0

0

1

0

1

1

1

0

0

0

1

0

0

0

0

1

1

0

0

0

0

0

0

0

0

0

0

0

1

1

1

0

0

1

1

0

1

1

0

1

1

1

1

1

0

0

0

1

1

0

0

1

0

1

0

1

1

1

1

1

1

0

0

0

1

0

1

1

1

1

1

0

0

1

1

0

0

1

0

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

var x1,  x2 : int;

    y1, y2:int; 

let

  automaton aut1

  state A :

  let

     x1 = input;

     y1 = x2;

  tel

  until true restart B

  state B :

  let

    x1 = 1; --    x1 = x2;

    y1 = 1;

  tel

  until true restart A

  automaton aut2

  state C :

  let

    x2 = x1;

    y2 = 2;

  tel

  until true restart D

  state D :

  let

    x2 = input;

y2 = x2;   -- y2 = x1;

  tel

  until true restart C

  ok = y1 = input || y2 = input;

tel

(* Generated Lustre Interface file from tawoa_automata.lus *)

(* by Lustre-C compiler version 1.3-458, 2016/10/21, 12:58:32 *)

(* Feel free to mask some of the definitions by removing them from this file. *)

type aut2__type = enum {C, D }; 

type aut1__type = enum {A, B }; 

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

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

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

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

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

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

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

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

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

74

96

92

12

72

57

66

8

6

58

16

5

1

60

81

9

15

92

97

57

8

93

7

39

37

27

4

71

58

98

26

94

91

49

41

61

78

86

33

87

21

66

9

29

84

67

44

23

99

58

95

53

7

95

55

0

50

16

89

72

95

82

8

5

59

83

89

35

46

46

10

62

96

13

74

88

89

96

62

54

68

3

26

73

0

81

54

67

60

29

55

97

29

14

86

70

93

96

92

81

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

var bit: bool;

    coin: bool;

let

  automaton mini_states

  state Even : 

  let 

    bit = true;

  tel until true restart Odd

  state Odd : 

  let 

    bit = false;

  tel until true restart Even

  coin = true -> not pre coin;

  ok = bit = not coin;

tel

(* Generated Lustre Interface file from test_nok.lus *)

(* by Lustre-C compiler version 1.3-458, 2016/10/21, 12:58:27 *)

(* Feel free to mask some of the definitions by removing them from this file. *)

type mini_states__type = enum {Even, Odd }; 

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

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

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

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

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

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

'ok': '0' 

<?xml version="1.0"?>

   <Results xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance">

     <Property name="top">

      <Date>2016-11-30 00:18</Date>

      <Lustre2Horn unit="sec">0.00</Lustre2Horn>

      <Parse unit="sec">0.00</Parse>

      <Query unit="sec">0.05</Query>

      <Answer>CEX</Answer>

      <Counterexample>

         <Node name ="top">

            <Stream name="top.x" type="unk">

                <Value instant="0">1</Value>

           </Stream>

            <Stream name="top.__top_14_c" type="unk">

                <Value instant="0">Even</Value>

           </Stream>

            <Stream name="top.__top_2_x" type="unk">

                <Value instant="0">1</Value>

           </Stream>

            <Stream name="top.__top_13_x" type="unk">

                <Value instant="0">1</Value>

           </Stream>

            <Stream name="top.__top_14_x" type="unk">

                <Value instant="0">Odd</Value>

           </Stream>

            <Stream name="top.__top_2_c" type="unk">

                <Value instant="0">1</Value>

           </Stream>

            <Stream name="top.ok" type="unk">

                <Value instant="0">1</Value>

           </Stream>

            <Stream name="top.__top_13_c" type="unk">

                <Value instant="0">1</Value>

           </Stream>

         </Node>

 <Node name ="mini_states__Even_unless">

            <Stream name="mini_states__Even_unless.mini_states__restart_act" type="unk">

                <Value instant="0">1</Value>

           </Stream>

            <Stream name="mini_states__Even_unless.mini_states__state_act" type="unk">

                <Value instant="0">Even</Value>

           </Stream>

            <Stream name="mini_states__restart_in" type="bool">

                <Value instant="0">1</Value>

           </Stream>

         </Node>

 <Node name ="mini_states__Even_handler_until">

            <Stream name="mini_states__Even_handler_until.mini_states__restart_in" type="unk">

                <Value instant="0">1</Value>

           </Stream>

            <Stream name="mini_states__Even_handler_until.bit_out" type="unk">

                <Value instant="0">1</Value>

           </Stream>

            <Stream name="mini_states__Even_handler_until.mini_states__restart_act" type="unk">

                <Value instant="0">1</Value>

           </Stream>

            <Stream name="mini_states__Even_handler_until.mini_states__state_in" type="unk">

                <Value instant="0">Odd</Value>

           </Stream>

         </Node>

      </Counterexample>

     </Property>

   </Results>