1
|
type state_name_t = string
|
2
|
|
3
|
type junction_name_t = string
|
4
|
|
5
|
type path_t = state_name_t list
|
6
|
|
7
|
type event_base_t = string
|
8
|
|
9
|
type event_t = event_base_t option
|
10
|
|
11
|
type user_variable_name_t = string
|
12
|
|
13
|
(* Connected to lustrec types *)
|
14
|
type base_action_t = {
|
15
|
defs : Lustre_types.statement list;
|
16
|
ainputs : Lustre_types.var_decl list;
|
17
|
aoutputs : Lustre_types.var_decl list;
|
18
|
avariables : Lustre_types.var_decl list; (* ident: string; *)
|
19
|
}
|
20
|
|
21
|
type base_condition_t = {
|
22
|
expr : Lustre_types.expr;
|
23
|
cinputs : Lustre_types.var_decl list;
|
24
|
coutputs : Lustre_types.var_decl list;
|
25
|
cvariables : Lustre_types.var_decl list;
|
26
|
}
|
27
|
|
28
|
val pp_state_name: Format.formatter -> state_name_t -> unit
|
29
|
val pp_junction_name: Format.formatter -> junction_name_t -> unit
|
30
|
val pp_path: Format.formatter -> path_t -> unit
|
31
|
|
32
|
type frontier_t = Loose | Strict
|
33
|
|
34
|
type _ call_t =
|
35
|
| Ecall : (path_t * path_t * frontier_t) call_t
|
36
|
| Dcall : path_t call_t
|
37
|
| Xcall : (path_t * frontier_t) call_t
|
38
|
|
39
|
(* Conditions are either (1) simple strings, (2) the active status of a state or
|
40
|
(3) occurence of an event. They can be combined (conjunction, negation) *)
|
41
|
module type ConditionType = sig
|
42
|
type t
|
43
|
|
44
|
val cquote : base_condition_t -> t
|
45
|
|
46
|
val tru : t
|
47
|
|
48
|
val active : path_t -> t
|
49
|
|
50
|
val event : event_t -> t
|
51
|
|
52
|
val ( && ) : t -> t -> t
|
53
|
|
54
|
val neg : t -> t
|
55
|
|
56
|
val pp_cond : Format.formatter -> t -> unit
|
57
|
end
|
58
|
|
59
|
module Condition: ConditionType
|
60
|
|
61
|
module type ActionType = sig
|
62
|
type t
|
63
|
|
64
|
val nil : t
|
65
|
|
66
|
val aquote : base_action_t -> t
|
67
|
|
68
|
val open_path : path_t -> t
|
69
|
|
70
|
val close_path : path_t -> t
|
71
|
|
72
|
val call : 'c call_t -> 'c -> t
|
73
|
|
74
|
val pp_act : Format.formatter -> t -> unit
|
75
|
end
|
76
|
|
77
|
module Action: ActionType
|