|
1
|
open Basetypes
|
|
2
|
|
|
3
|
(* Type definitions of a model *)
|
|
4
|
|
|
5
|
type destination_t = DPath of path_t | DJunction of junction_name_t
|
|
6
|
|
|
7
|
type trans_t = {
|
|
8
|
event : event_t;
|
|
9
|
condition : Condition.t;
|
|
10
|
condition_act : Action.t;
|
|
11
|
transition_act : Action.t;
|
|
12
|
dest : destination_t;
|
|
13
|
}
|
|
14
|
|
|
15
|
type transitions_t = trans_t list
|
|
16
|
|
|
17
|
type composition_t =
|
|
18
|
| Or of transitions_t * state_name_t list
|
|
19
|
| And of state_name_t list
|
|
20
|
|
|
21
|
type state_actions_t = {
|
|
22
|
entry_act : Action.t;
|
|
23
|
during_act : Action.t;
|
|
24
|
exit_act : Action.t;
|
|
25
|
}
|
|
26
|
|
|
27
|
type state_def_t = {
|
|
28
|
state_actions : state_actions_t;
|
|
29
|
outer_trans : transitions_t;
|
|
30
|
inner_trans : transitions_t;
|
|
31
|
internal_composition : composition_t;
|
|
32
|
}
|
|
33
|
|
|
34
|
type 'prog_t src_components_t =
|
|
35
|
| State of path_t * state_def_t
|
|
36
|
| Junction of junction_name_t * transitions_t
|
|
37
|
| SFFunction of 'prog_t
|
|
38
|
|
|
39
|
type prog_t =
|
|
40
|
| Program of
|
|
41
|
state_name_t
|
|
42
|
* prog_t src_components_t list
|
|
43
|
* (Lustre_types.var_decl * Lustre_types.expr) list
|
|
44
|
|
|
45
|
type trace_t = event_t list
|
|
46
|
|
|
47
|
module type MODEL_T = sig
|
|
48
|
val name : string
|
|
49
|
|
|
50
|
val model : prog_t
|
|
51
|
|
|
52
|
val traces : trace_t list
|
|
53
|
end
|