| 1 |
2de7fa82
|
ploc
|
open Datatype
|
| 2 |
|
|
open SF
|
| 3 |
|
|
|
| 4 |
|
|
let name = "medium"
|
| 5 |
|
|
|
| 6 |
93119c3f
|
ploc
|
let condition x = condition (Corelang.mkexpr Location.dummy_loc (LustreSpec.Expr_const (Corelang.const_of_bool true)))
|
| 7 |
b06b7b77
|
Christophe Garion
|
|
| 8 |
2de7fa82
|
ploc
|
let model : prog_t =
|
| 9 |
|
|
let state_main = "main" in
|
| 10 |
|
|
let state_a = "a" in
|
| 11 |
|
|
let state_a1 = "a1" in
|
| 12 |
|
|
let state_b = "b" in
|
| 13 |
|
|
|
| 14 |
|
|
let actions_main = state_action (action "emain") (action "dmain") (action "xmain") in
|
| 15 |
|
|
let actions_a = state_action (action "eA") (action "dA") (action "xA") in
|
| 16 |
|
|
let actions_a1 = state_action (action "eA1") (action "dA1") (action "xA1") in
|
| 17 |
|
|
let actions_b = state_action (action "eB") (action "dB") (action "xB") in
|
| 18 |
|
|
|
| 19 |
|
|
let tA = {
|
| 20 |
|
|
event = no_event;
|
| 21 |
|
|
condition = condition "cond_tA";
|
| 22 |
|
|
condition_act = action "condact_tA";
|
| 23 |
|
|
transition_act = action "transact_tA";
|
| 24 |
|
|
dest = DPath [state_main;state_a];
|
| 25 |
|
|
}
|
| 26 |
|
|
in
|
| 27 |
|
|
let tJ = {
|
| 28 |
|
|
event = no_event;
|
| 29 |
|
|
condition = condition "cond_tJ";
|
| 30 |
|
|
condition_act = action "condact_tJ";
|
| 31 |
|
|
transition_act = action "transact_tJ";
|
| 32 |
|
|
dest = DJunction "jmid";
|
| 33 |
|
|
}
|
| 34 |
|
|
in
|
| 35 |
|
|
let tB = {
|
| 36 |
|
|
event = no_event;
|
| 37 |
|
|
condition = condition "cond_tB";
|
| 38 |
|
|
condition_act = action "condact_tB";
|
| 39 |
|
|
transition_act = action "transact_tB";
|
| 40 |
|
|
dest = DPath [state_main;state_b];
|
| 41 |
|
|
}
|
| 42 |
|
|
in
|
| 43 |
|
|
let tA1 = {
|
| 44 |
|
|
event = no_event;
|
| 45 |
|
|
condition = condition "cond_tA1";
|
| 46 |
|
|
condition_act = action "condact_tA1";
|
| 47 |
|
|
transition_act = action "transact_tA1";
|
| 48 |
|
|
dest = DPath [state_main;state_a;state_a1];
|
| 49 |
|
|
}
|
| 50 |
|
|
in
|
| 51 |
|
|
|
| 52 |
|
|
|
| 53 |
|
|
let def_a = {
|
| 54 |
|
|
state_actions = actions_a;
|
| 55 |
|
|
outer_trans = [tJ];
|
| 56 |
|
|
inner_trans = [];
|
| 57 |
|
|
internal_composition = Or ([tA1], [state_a1])
|
| 58 |
|
|
}
|
| 59 |
|
|
in
|
| 60 |
|
|
let def_a1 = {
|
| 61 |
|
|
state_actions = actions_a1;
|
| 62 |
|
|
outer_trans = [tB];
|
| 63 |
|
|
inner_trans = [];
|
| 64 |
|
|
internal_composition = Or ([], [])
|
| 65 |
|
|
}
|
| 66 |
|
|
in
|
| 67 |
|
|
let def_b = {
|
| 68 |
|
|
state_actions = actions_b;
|
| 69 |
|
|
outer_trans = [tA1];
|
| 70 |
|
|
inner_trans = [];
|
| 71 |
|
|
internal_composition = Or ([], [])
|
| 72 |
|
|
}
|
| 73 |
|
|
in
|
| 74 |
|
|
let def_main = {
|
| 75 |
|
|
state_actions = actions_main;
|
| 76 |
|
|
outer_trans = [];
|
| 77 |
|
|
inner_trans = [];
|
| 78 |
|
|
internal_composition = Or ([tA], [state_a; state_b])
|
| 79 |
|
|
}
|
| 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 |
|
|
Junction("jmid", [tB]);
|
| 86 |
|
|
]
|
| 87 |
|
|
in
|
| 88 |
b06b7b77
|
Christophe Garion
|
Program (state_main, src, [])
|
| 89 |
2de7fa82
|
ploc
|
|
| 90 |
|
|
let traces : trace_t list = [[None; None]]
|