Revision ca7ff3f7
Added by Lélio Brun over 1 year ago
src/tools/stateflow/models/model_simple.ml | ||
---|---|---|
4 | 4 |
|
5 | 5 |
let name = "simple" |
6 | 6 |
|
7 |
let condition _ = condition { |
|
8 |
expr = Corelang.mkexpr Location.dummy_loc (Lustre_types.Expr_const (Corelang.const_of_bool true)); |
|
9 |
cinputs = []; |
|
10 |
coutputs = []; |
|
11 |
cvariables = []; |
|
12 |
} |
|
13 |
|
|
14 |
let action _ = no_action |
|
7 |
let condition _ = |
|
8 |
condition |
|
9 |
{ |
|
10 |
expr = |
|
11 |
Corelang.mkexpr Location.dummy_loc |
|
12 |
(Lustre_types.Expr_const (Corelang.const_of_bool true)); |
|
13 |
cinputs = []; |
|
14 |
coutputs = []; |
|
15 |
cvariables = []; |
|
16 |
} |
|
17 |
|
|
18 |
let action _ = no_action |
|
15 | 19 |
|
16 | 20 |
let model : prog_t = |
17 |
let state_main = "main" in
|
|
18 |
let state_a = "a" in
|
|
19 |
let state_a1 = "a1" in
|
|
20 |
let state_b = "b" in
|
|
21 |
let state_main = "main" in |
|
22 |
let state_a = "a" in |
|
23 |
let state_a1 = "a1" in |
|
24 |
let state_b = "b" in |
|
21 | 25 |
|
22 |
let actions_main = state_action (action "emain") (action "dmain") (action "xmain") in |
|
23 |
let actions_a = state_action (action "eA") (action "dA") (action "xA") in |
|
24 |
let actions_a1 = state_action (action "eA1") (action "dA1") (action "xA1") in |
|
25 |
let actions_b = state_action (action "eB") (action "dB") (action "xB") in |
|
26 |
let actions_main = |
|
27 |
state_action (action "emain") (action "dmain") (action "xmain") |
|
28 |
in |
|
29 |
let actions_a = state_action (action "eA") (action "dA") (action "xA") in |
|
30 |
let actions_a1 = state_action (action "eA1") (action "dA1") (action "xA1") in |
|
31 |
let actions_b = state_action (action "eB") (action "dB") (action "xB") in |
|
26 | 32 |
|
27 |
let tA = { |
|
33 |
let tA = |
|
34 |
{ |
|
28 | 35 |
event = no_event; |
29 | 36 |
condition = condition "cond_tA"; |
30 | 37 |
condition_act = action "condact_tA"; |
31 | 38 |
transition_act = action "transact_tA"; |
32 |
dest = DPath [state_main;state_a];
|
|
39 |
dest = DPath [ state_main; state_a ];
|
|
33 | 40 |
} |
34 |
in |
|
35 |
let tB = { |
|
41 |
in |
|
42 |
let tB = |
|
43 |
{ |
|
36 | 44 |
event = no_event; |
37 | 45 |
condition = condition "cond_tB"; |
38 | 46 |
condition_act = action "condact_tB"; |
39 | 47 |
transition_act = action "transact_tB"; |
40 |
dest = DPath [state_main;state_b];
|
|
48 |
dest = DPath [ state_main; state_b ];
|
|
41 | 49 |
} |
42 |
in |
|
43 |
let tA1 = { |
|
50 |
in |
|
51 |
let tA1 = |
|
52 |
{ |
|
44 | 53 |
event = no_event; |
45 | 54 |
condition = condition "cond_tA1"; |
46 | 55 |
condition_act = action "condact_tA1"; |
47 | 56 |
transition_act = action "transact_tA1"; |
48 |
dest = DPath [state_main;state_a;state_a1];
|
|
57 |
dest = DPath [ state_main; state_a; state_a1 ];
|
|
49 | 58 |
} |
50 |
in |
|
51 |
|
|
59 |
in |
|
52 | 60 |
|
53 |
let def_a = { |
|
61 |
let def_a = |
|
62 |
{ |
|
54 | 63 |
state_actions = actions_a; |
55 |
outer_trans = [tB];
|
|
64 |
outer_trans = [ tB ];
|
|
56 | 65 |
inner_trans = []; |
57 |
internal_composition = Or ([tA1], [state_a1])
|
|
66 |
internal_composition = Or ([ tA1 ], [ state_a1 ]);
|
|
58 | 67 |
} |
59 |
in |
|
60 |
let def_a1 = { |
|
68 |
in |
|
69 |
let def_a1 = |
|
70 |
{ |
|
61 | 71 |
state_actions = actions_a1; |
62 |
outer_trans = [tB];
|
|
72 |
outer_trans = [ tB ];
|
|
63 | 73 |
inner_trans = []; |
64 |
internal_composition = Or ([], []) |
|
74 |
internal_composition = Or ([], []);
|
|
65 | 75 |
} |
66 |
in |
|
67 |
let def_b = { |
|
76 |
in |
|
77 |
let def_b = |
|
78 |
{ |
|
68 | 79 |
state_actions = actions_b; |
69 |
outer_trans = [tA1];
|
|
80 |
outer_trans = [ tA1 ];
|
|
70 | 81 |
inner_trans = []; |
71 |
internal_composition = Or ([], []) |
|
82 |
internal_composition = Or ([], []);
|
|
72 | 83 |
} |
73 |
in |
|
74 |
let def_main = { |
|
84 |
in |
|
85 |
let def_main = |
|
86 |
{ |
|
75 | 87 |
state_actions = actions_main; |
76 | 88 |
outer_trans = []; |
77 | 89 |
inner_trans = []; |
78 |
internal_composition = Or ([tA], [state_a; state_b])
|
|
90 |
internal_composition = Or ([ tA ], [ state_a; state_b ]);
|
|
79 | 91 |
} |
80 |
in |
|
81 |
let src = [State([state_main;state_a], def_a); |
|
82 |
State([state_main;state_a;state_a1], def_a1); |
|
83 |
State([state_main;state_b], def_b); |
|
84 |
State([state_main], def_main); |
|
85 |
] |
|
86 |
in |
|
87 |
Program (state_main, src, []) |
|
92 |
in |
|
93 |
let src = |
|
94 |
[ |
|
95 |
State ([ state_main; state_a ], def_a); |
|
96 |
State ([ state_main; state_a; state_a1 ], def_a1); |
|
97 |
State ([ state_main; state_b ], def_b); |
|
98 |
State ([ state_main ], def_main); |
|
99 |
] |
|
100 |
in |
|
101 |
Program (state_main, src, []) |
|
88 | 102 |
|
89 |
let traces : trace_t list = [[None; None]] |
|
103 |
let traces : trace_t list = [ [ None; None ] ] |
Also available in: Unified diff
reformatting