lustrec / src / tools / stateflow / common / basetypes.ml @ 9ae027f8
History | View | Annotate | Download (4.56 KB)
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) |