1
|
|
2
|
let sf_level = 2
|
3
|
|
4
|
(* Basic datatype for model elements: state and junction name, events ... *)
|
5
|
type state_name_t = string
|
6
|
type junction_name_t = string
|
7
|
type path_t = state_name_t list
|
8
|
type event_base_t = string
|
9
|
type event_t = event_base_t option
|
10
|
type user_variable_name_t = string
|
11
|
|
12
|
(* Connected to lustrec types *)
|
13
|
type base_action_t = { defs : LustreSpec.statement list;
|
14
|
ainputs: LustreSpec.var_decl list;
|
15
|
aoutputs: LustreSpec.var_decl list;
|
16
|
avariables: LustreSpec.var_decl list;
|
17
|
(* ident: string; *)
|
18
|
}
|
19
|
type base_condition_t = { expr: LustreSpec.expr;
|
20
|
cinputs: LustreSpec.var_decl list;
|
21
|
coutputs: LustreSpec.var_decl list;
|
22
|
cvariables: LustreSpec.var_decl list }
|
23
|
|
24
|
(* P(r)etty printers *)
|
25
|
let pp_state_name = Format.pp_print_string
|
26
|
let pp_junction_name = Format.pp_print_string
|
27
|
let pp_path fmt p = Utils.fprintf_list ~sep:"." pp_state_name fmt p
|
28
|
let pp_event fmt e = match e with None -> Format.fprintf fmt "none" | Some s -> Format.fprintf fmt "%s" s
|
29
|
let pp_base_act fmt a = Printers.pp_node_stmts fmt a.defs
|
30
|
let pp_base_cond fmt c= Printers.pp_expr fmt c.expr
|
31
|
|
32
|
(* Action and Condition types and functions. *)
|
33
|
|
34
|
(* Actions are defined by string + the opening and closing of states *)
|
35
|
|
36
|
(* This version is slightly more complex than the one of EMSOFT'05 to enable the
|
37
|
use of function calls in action.
|
38
|
|
39
|
TODO: these rich call type could be externalized and a functor introduced. *)
|
40
|
|
41
|
type frontier_t =
|
42
|
| Loose
|
43
|
| Strict
|
44
|
|
45
|
let pp_frontier fmt frontier =
|
46
|
match frontier with
|
47
|
| Loose -> Format.fprintf fmt "Loose"
|
48
|
| Strict -> Format.fprintf fmt "Strict"
|
49
|
|
50
|
type _ call_t =
|
51
|
| Ecall : (path_t * path_t * frontier_t) call_t
|
52
|
| Dcall : path_t call_t
|
53
|
| Xcall : (path_t * frontier_t) call_t
|
54
|
|
55
|
let pp_call :
|
56
|
type a. Format.formatter -> a call_t -> unit =
|
57
|
fun fmt call ->
|
58
|
match call with
|
59
|
| Ecall -> Format.fprintf fmt "CallE"
|
60
|
| Dcall -> Format.fprintf fmt "CallD"
|
61
|
| Xcall -> Format.fprintf fmt "CallX"
|
62
|
|
63
|
module type ActionType =
|
64
|
sig
|
65
|
type t
|
66
|
val nil : t
|
67
|
val aquote : base_action_t -> t
|
68
|
val open_path : path_t -> t
|
69
|
val close_path : path_t -> t
|
70
|
val call : 'c call_t -> 'c -> t
|
71
|
|
72
|
val pp_act : Format.formatter -> t -> unit
|
73
|
end
|
74
|
|
75
|
|
76
|
module Action =
|
77
|
struct
|
78
|
type t =
|
79
|
| Quote : base_action_t -> t
|
80
|
| Close : path_t -> t
|
81
|
| Open : path_t -> t
|
82
|
| Call : 'c call_t * 'c -> t
|
83
|
| Nil : t
|
84
|
|
85
|
|
86
|
let nil = Nil
|
87
|
let aquote act = Quote act
|
88
|
let open_path p = Open p
|
89
|
let close_path p = Close p
|
90
|
let call c a = Call (c, a)
|
91
|
|
92
|
let pp_call : type c. Format.formatter -> c call_t -> c -> unit =
|
93
|
fun fmt call ->
|
94
|
match call with
|
95
|
| Ecall -> (fun (p, p', f) -> Format.fprintf fmt "%a(%a, %a, %a)" pp_call call pp_path p pp_path p' pp_frontier f)
|
96
|
| Dcall -> (fun p -> Format.fprintf fmt "%a(%a)" pp_call call pp_path p)
|
97
|
| Xcall -> (fun (p, f) -> Format.fprintf fmt "%a(%a, %a)" pp_call call pp_path p pp_frontier f)
|
98
|
|
99
|
let pp_act fmt act =
|
100
|
match act with
|
101
|
| Call (c, a) -> pp_call fmt c a
|
102
|
| Quote a -> Format.fprintf fmt "%a" pp_base_act a
|
103
|
| Close p -> Format.fprintf fmt "Close(%a)" pp_path p
|
104
|
| Open p -> Format.fprintf fmt "Open(%a)" pp_path p
|
105
|
| Nil -> Format.fprintf fmt "Nil"
|
106
|
end
|
107
|
|
108
|
let _ = (module Action : ActionType)
|
109
|
|
110
|
|
111
|
(* Conditions are either (1) simple strings, (2) the active status of a state or
|
112
|
(3) occurence of an event. They can be combined (conjunction, negation) *)
|
113
|
module type ConditionType =
|
114
|
sig
|
115
|
type t
|
116
|
val cquote : base_condition_t -> t
|
117
|
val tru : t
|
118
|
val active : path_t -> t
|
119
|
val event : event_t -> t
|
120
|
val ( && ) : t -> t -> t
|
121
|
val neg : t -> t
|
122
|
|
123
|
val pp_cond : Format.formatter -> t -> unit
|
124
|
end
|
125
|
|
126
|
module Condition =
|
127
|
struct
|
128
|
type t =
|
129
|
| Quote of base_condition_t
|
130
|
| Active of path_t
|
131
|
| Event of event_base_t
|
132
|
| And of t * t
|
133
|
| Neg of t
|
134
|
| True
|
135
|
|
136
|
let cquote cond = Quote cond
|
137
|
let tru = True
|
138
|
let neg cond = Neg cond
|
139
|
let ( && ) cond1 cond2 = And (cond1, cond2)
|
140
|
let active path = Active path
|
141
|
let event evt =
|
142
|
match evt with
|
143
|
| None -> True
|
144
|
| Some e -> Event e
|
145
|
|
146
|
let rec pp_cond fmt cond =
|
147
|
match cond with
|
148
|
| True -> Format.fprintf fmt "true"
|
149
|
| Active p -> Format.fprintf fmt "Active(%a)" pp_path p
|
150
|
| Event e -> Format.fprintf fmt "Event(%s)" e
|
151
|
| Neg cond -> Format.fprintf fmt "(neg %a)" pp_cond cond
|
152
|
| And (cond1, cond2) -> Format.fprintf fmt "%a /\\ %a" pp_cond cond1 pp_cond cond2
|
153
|
| Quote c -> Format.fprintf fmt "%a" pp_base_cond c
|
154
|
|
155
|
end
|
156
|
|
157
|
let _ = (module Condition : ConditionType)
|