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