lustrec / src / tools / stateflow / models / model_simple.ml @ 9c654082
History | View | Annotate | Download (2.28 KB)
1 |
open Datatype |
---|---|
2 |
open SF |
3 |
|
4 |
let name = "simple" |
5 |
|
6 |
let condition x = condition { |
7 |
expr = Corelang.mkexpr Location.dummy_loc (LustreSpec.Expr_const (Corelang.const_of_bool true)); |
8 |
cinputs = []; |
9 |
coutputs = []; |
10 |
cvariables = []; |
11 |
} |
12 |
|
13 |
let action _ = no_action |
14 |
|
15 |
let model : prog_t = |
16 |
let state_main = "main" in |
17 |
let state_a = "a" in |
18 |
let state_a1 = "a1" in |
19 |
let state_b = "b" in |
20 |
|
21 |
let actions_main = state_action (action "emain") (action "dmain") (action "xmain") in |
22 |
let actions_a = state_action (action "eA") (action "dA") (action "xA") in |
23 |
let actions_a1 = state_action (action "eA1") (action "dA1") (action "xA1") in |
24 |
let actions_b = state_action (action "eB") (action "dB") (action "xB") in |
25 |
|
26 |
let tA = { |
27 |
event = no_event; |
28 |
condition = condition "cond_tA"; |
29 |
condition_act = action "condact_tA"; |
30 |
transition_act = action "transact_tA"; |
31 |
dest = DPath [state_main;state_a]; |
32 |
} |
33 |
in |
34 |
let tB = { |
35 |
event = no_event; |
36 |
condition = condition "cond_tB"; |
37 |
condition_act = action "condact_tB"; |
38 |
transition_act = action "transact_tB"; |
39 |
dest = DPath [state_main;state_b]; |
40 |
} |
41 |
in |
42 |
let tA1 = { |
43 |
event = no_event; |
44 |
condition = condition "cond_tA1"; |
45 |
condition_act = action "condact_tA1"; |
46 |
transition_act = action "transact_tA1"; |
47 |
dest = DPath [state_main;state_a;state_a1]; |
48 |
} |
49 |
in |
50 |
|
51 |
|
52 |
let def_a = { |
53 |
state_actions = actions_a; |
54 |
outer_trans = [tB]; |
55 |
inner_trans = []; |
56 |
internal_composition = Or ([tA1], [state_a1]) |
57 |
} |
58 |
in |
59 |
let def_a1 = { |
60 |
state_actions = actions_a1; |
61 |
outer_trans = [tB]; |
62 |
inner_trans = []; |
63 |
internal_composition = Or ([], []) |
64 |
} |
65 |
in |
66 |
let def_b = { |
67 |
state_actions = actions_b; |
68 |
outer_trans = [tA1]; |
69 |
inner_trans = []; |
70 |
internal_composition = Or ([], []) |
71 |
} |
72 |
in |
73 |
let def_main = { |
74 |
state_actions = actions_main; |
75 |
outer_trans = []; |
76 |
inner_trans = []; |
77 |
internal_composition = Or ([tA], [state_a; state_b]) |
78 |
} |
79 |
in |
80 |
let src = [State([state_main;state_a], def_a); |
81 |
State([state_main;state_a;state_a1], def_a1); |
82 |
State([state_main;state_b], def_b); |
83 |
State([state_main], def_main); |
84 |
] |
85 |
in |
86 |
Program (state_main, src, []) |
87 |
|
88 |
let traces : trace_t list = [[None; None]] |