Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / automata / with_properties / aut2.lus @ 02d89bbb

History | View | Annotate | Download (4.63 KB)

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