|
1
|
open Datatype
|
|
2
|
open Basetypes
|
|
3
|
open SF
|
|
4
|
|
|
5
|
let name = "simple"
|
|
6
|
|
|
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
|
|
19
|
|
|
20
|
let model : prog_t =
|
|
21
|
let state_main = "main" in
|
|
22
|
let state_a = "a" in
|
|
23
|
let state_a1 = "a1" in
|
|
24
|
let state_b = "b" in
|
|
25
|
|
|
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
|
|
32
|
|
|
33
|
let tA =
|
|
34
|
{
|
|
35
|
event = no_event;
|
|
36
|
condition = condition "cond_tA";
|
|
37
|
condition_act = action "condact_tA";
|
|
38
|
transition_act = action "transact_tA";
|
|
39
|
dest = DPath [ state_main; state_a ];
|
|
40
|
}
|
|
41
|
in
|
|
42
|
let tB =
|
|
43
|
{
|
|
44
|
event = no_event;
|
|
45
|
condition = condition "cond_tB";
|
|
46
|
condition_act = action "condact_tB";
|
|
47
|
transition_act = action "transact_tB";
|
|
48
|
dest = DPath [ state_main; state_b ];
|
|
49
|
}
|
|
50
|
in
|
|
51
|
let tA1 =
|
|
52
|
{
|
|
53
|
event = no_event;
|
|
54
|
condition = condition "cond_tA1";
|
|
55
|
condition_act = action "condact_tA1";
|
|
56
|
transition_act = action "transact_tA1";
|
|
57
|
dest = DPath [ state_main; state_a; state_a1 ];
|
|
58
|
}
|
|
59
|
in
|
|
60
|
|
|
61
|
let def_a =
|
|
62
|
{
|
|
63
|
state_actions = actions_a;
|
|
64
|
outer_trans = [ tB ];
|
|
65
|
inner_trans = [];
|
|
66
|
internal_composition = Or ([ tA1 ], [ state_a1 ]);
|
|
67
|
}
|
|
68
|
in
|
|
69
|
let def_a1 =
|
|
70
|
{
|
|
71
|
state_actions = actions_a1;
|
|
72
|
outer_trans = [ tB ];
|
|
73
|
inner_trans = [];
|
|
74
|
internal_composition = Or ([], []);
|
|
75
|
}
|
|
76
|
in
|
|
77
|
let def_b =
|
|
78
|
{
|
|
79
|
state_actions = actions_b;
|
|
80
|
outer_trans = [ tA1 ];
|
|
81
|
inner_trans = [];
|
|
82
|
internal_composition = Or ([], []);
|
|
83
|
}
|
|
84
|
in
|
|
85
|
let def_main =
|
|
86
|
{
|
|
87
|
state_actions = actions_main;
|
|
88
|
outer_trans = [];
|
|
89
|
inner_trans = [];
|
|
90
|
internal_composition = Or ([ tA ], [ state_a; state_b ]);
|
|
91
|
}
|
|
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, [])
|
|
102
|
|
|
103
|
let traces : trace_t list = [ [ None; None ] ]
|