|
1
|
open Datatype
|
|
2
|
open SF
|
|
3
|
|
|
4
|
let name = "medium"
|
|
5
|
|
|
6
|
let condition x = condition (Corelang.mkexpr Location.dummy_loc (LustreSpec.Expr_const (Corelang.const_of_bool true)))
|
|
7
|
|
|
8
|
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
|
Program (state_main, src, [])
|
|
89
|
|
|
90
|
let traces : trace_t list = [[None; None]]
|