Revision ca7ff3f7
Added by Lélio Brun over 1 year ago
src/tools/stateflow/semantics/theta.ml | ||
---|---|---|
1 |
open Basetypes |
|
1 |
open Basetypes |
|
2 |
|
|
2 | 3 |
(* open ActiveEnv *) |
3 |
open CPS_transformer |
|
4 |
open CPS_transformer |
|
5 |
|
|
4 | 6 |
(* open Datatype *) |
5 | 7 |
(* open Simulink *) |
6 | 8 |
|
7 |
(* Theta functions interfaces including memoization when using modular calls |
|
8 |
|
|
9 |
parametrized by the transformer specifying the type of the |
|
10 |
continuation. Evaluation of actions is also continuation dependent. |
|
11 |
*) |
|
9 |
(* Theta functions interfaces including memoization when using modular calls |
|
12 | 10 |
|
13 |
module KenvTheta (T : TransformerType) =
|
|
14 |
struct
|
|
11 |
parametrized by the transformer specifying the type of the continuation.
|
|
12 |
Evaluation of actions is also continuation dependent. *)
|
|
15 | 13 |
|
14 |
module KenvTheta (T : TransformerType) = struct |
|
16 | 15 |
type kenv_t = { |
17 |
cont_node : ( |
|
18 |
path_t * ( |
|
19 |
(kenv_t -> path_t -> frontier_t -> T.t) * |
|
20 |
(kenv_t -> T.t) * |
|
21 |
(kenv_t -> frontier_t -> T.t) |
|
22 |
) |
|
23 |
) list; |
|
24 |
cont_junc : ( |
|
25 |
junction_name_t * ( |
|
26 |
kenv_t -> T.t wrapper_t -> T.t success_t -> T.t fail_t -> T.t) |
|
27 |
) list |
|
16 |
cont_node : |
|
17 |
(path_t |
|
18 |
* ((kenv_t -> path_t -> frontier_t -> T.t) |
|
19 |
* (kenv_t -> T.t) |
|
20 |
* (kenv_t -> frontier_t -> T.t))) |
|
21 |
list; |
|
22 |
cont_junc : |
|
23 |
(junction_name_t |
|
24 |
* (kenv_t -> T.t wrapper_t -> T.t success_t -> T.t fail_t -> T.t)) |
|
25 |
list; |
|
28 | 26 |
} |
29 | 27 |
|
30 |
|
|
31 | 28 |
let init_env src = |
32 |
List.fold_left (fun accu d -> |
|
33 |
match d with |
|
34 |
| Datatype.State (p, _) -> ActiveStates.Env.add p false accu |
|
35 |
| _ -> accu) |
|
36 |
ActiveStates.Env.empty |
|
37 |
src |
|
38 |
|
|
39 |
module type KenvType = |
|
40 |
sig |
|
29 |
List.fold_left |
|
30 |
(fun accu d -> |
|
31 |
match d with |
|
32 |
| Datatype.State (p, _) -> |
|
33 |
ActiveStates.Env.add p false accu |
|
34 |
| _ -> |
|
35 |
accu) |
|
36 |
ActiveStates.Env.empty src |
|
37 |
|
|
38 |
module type KenvType = sig |
|
41 | 39 |
val kenv : kenv_t |
42 | 40 |
end |
43 | 41 |
|
44 |
module type MemoThetaTablesType = |
|
45 |
sig |
|
42 |
module type MemoThetaTablesType = sig |
|
46 | 43 |
val tables : 'c call_t -> ('c, T.t) Memo.t |
47 | 44 |
end |
48 | 45 |
|
49 |
module type MemoThetaType = |
|
50 |
sig |
|
46 |
module type MemoThetaType = sig |
|
51 | 47 |
include ThetaType with type t = T.t |
48 |
|
|
52 | 49 |
val components : 'c call_t -> ('c * t) list |
53 | 50 |
end |
54 | 51 |
|
55 |
module type ModularType = |
|
56 |
sig |
|
52 |
module type ModularType = sig |
|
57 | 53 |
val modular : (path_t, 'b, bool) tag_t -> path_t -> 'b |
58 | 54 |
end |
59 | 55 |
|
60 |
module MemoThetaTables : functor () -> MemoThetaTablesType = functor () -> |
|
61 |
struct |
|
62 |
let table_theta_e = (Memo.create () : (path_t * path_t * frontier_t, T.t) Memo.t) |
|
63 |
let table_theta_d = (Memo.create () : (path_t, T.t) Memo.t) |
|
64 |
let table_theta_x = (Memo.create () : (path_t * frontier_t, T.t) Memo.t) |
|
65 |
|
|
66 |
let tables : type c. c call_t -> (c, T.t) Memo.t = |
|
67 |
fun call -> |
|
68 |
match call with |
|
69 |
| Ecall -> table_theta_e |
|
70 |
| Dcall -> table_theta_d |
|
71 |
| Xcall -> table_theta_x |
|
72 |
end |
|
73 |
|
|
74 |
module Memoize (Tables : MemoThetaTablesType) (Theta : ThetaType with type t = T.t) : MemoThetaType = |
|
75 |
struct |
|
56 |
module MemoThetaTables : functor () -> MemoThetaTablesType = |
|
57 |
functor |
|
58 |
() |
|
59 |
-> |
|
60 |
struct |
|
61 |
let table_theta_e = |
|
62 |
(Memo.create () : (path_t * path_t * frontier_t, T.t) Memo.t) |
|
63 |
|
|
64 |
let table_theta_d = (Memo.create () : (path_t, T.t) Memo.t) |
|
65 |
|
|
66 |
let table_theta_x = (Memo.create () : (path_t * frontier_t, T.t) Memo.t) |
|
67 |
|
|
68 |
let tables : type c. c call_t -> (c, T.t) Memo.t = |
|
69 |
fun call -> |
|
70 |
match call with |
|
71 |
| Ecall -> |
|
72 |
table_theta_e |
|
73 |
| Dcall -> |
|
74 |
table_theta_d |
|
75 |
| Xcall -> |
|
76 |
table_theta_x |
|
77 |
end |
|
78 |
|
|
79 |
module Memoize |
|
80 |
(Tables : MemoThetaTablesType) |
|
81 |
(Theta : ThetaType with type t = T.t) : MemoThetaType = struct |
|
76 | 82 |
type t = Theta.t |
77 | 83 |
|
78 | 84 |
let components call = |
79 |
Memo.fold (Tables.tables call) (fun k v res -> (k, v)::res) []
|
|
85 |
Memo.fold (Tables.tables call) (fun k v res -> (k, v) :: res) []
|
|
80 | 86 |
|
81 | 87 |
let theta : type a b. (a, b, t) theta_t = |
82 |
fun tag ->
|
|
88 |
fun tag -> |
|
83 | 89 |
match tag with |
84 |
| J -> Theta.theta J |
|
85 |
| E -> Memo.apply3 (Tables.tables Ecall) (Theta.theta E) |
|
86 |
| D -> Memo.apply (Tables.tables Dcall) (Theta.theta D) |
|
87 |
| X -> Memo.apply2 (Tables.tables Xcall) (Theta.theta X) |
|
90 |
| J -> |
|
91 |
Theta.theta J |
|
92 |
| E -> |
|
93 |
Memo.apply3 (Tables.tables Ecall) (Theta.theta E) |
|
94 |
| D -> |
|
95 |
Memo.apply (Tables.tables Dcall) (Theta.theta D) |
|
96 |
| X -> |
|
97 |
Memo.apply2 (Tables.tables Xcall) (Theta.theta X) |
|
88 | 98 |
end |
89 |
|
|
90 |
module Modularize (Mod : ModularType) (Theta : MemoThetaType) : MemoThetaType =
|
|
91 |
struct |
|
99 |
|
|
100 |
module Modularize (Mod : ModularType) (Theta : MemoThetaType) : |
|
101 |
MemoThetaType = struct
|
|
92 | 102 |
type t = Theta.t |
93 | 103 |
|
94 | 104 |
let mod_theta = (module Theta : ThetaType with type t = T.t) |
95 | 105 |
|
96 | 106 |
let components : type c. c call_t -> (c * t) list = |
97 |
fun call ->
|
|
107 |
fun call -> |
|
98 | 108 |
match call with |
99 |
| Ecall -> List.filter (fun ((p, p', f), _) -> Mod.modular E p p' f) (Theta.components Ecall) |
|
100 |
| Dcall -> List.filter (fun (p , _) -> Mod.modular D p) (Theta.components Dcall) |
|
101 |
| Xcall -> List.filter (fun ((p, f) , _) -> Mod.modular X p f) (Theta.components Xcall) |
|
109 |
| Ecall -> |
|
110 |
List.filter |
|
111 |
(fun ((p, p', f), _) -> Mod.modular E p p' f) |
|
112 |
(Theta.components Ecall) |
|
113 |
| Dcall -> |
|
114 |
List.filter (fun (p, _) -> Mod.modular D p) (Theta.components Dcall) |
|
115 |
| Xcall -> |
|
116 |
List.filter |
|
117 |
(fun ((p, f), _) -> Mod.modular X p f) |
|
118 |
(Theta.components Xcall) |
|
102 | 119 |
|
103 | 120 |
let theta : type a b. (a, b, t) theta_t = |
104 |
fun tag ->
|
|
121 |
fun tag -> |
|
105 | 122 |
match tag with |
106 |
| J -> Theta.theta tag |
|
107 |
| E -> (fun p p' f -> let theta_e = Theta.theta tag p p' f in |
|
108 |
if Mod.modular E p p' f |
|
109 |
then T.(eval_act mod_theta (call Ecall (p, p', f))) |
|
110 |
else theta_e) |
|
111 |
| D -> (fun p -> let theta_d = Theta.theta tag p in |
|
112 |
if Mod.modular D p |
|
113 |
then T.(eval_act mod_theta (call Dcall p)) |
|
114 |
else theta_d) |
|
115 |
| X -> (fun p f -> let theta_x = Theta.theta tag p f in |
|
116 |
if Mod.modular X p f |
|
117 |
then T.(eval_act mod_theta (call Xcall (p, f))) |
|
118 |
else theta_x) |
|
123 |
| J -> |
|
124 |
Theta.theta tag |
|
125 |
| E -> |
|
126 |
fun p p' f -> |
|
127 |
let theta_e = Theta.theta tag p p' f in |
|
128 |
if Mod.modular E p p' f then |
|
129 |
T.(eval_act mod_theta (call Ecall (p, p', f))) |
|
130 |
else theta_e |
|
131 |
| D -> |
|
132 |
fun p -> |
|
133 |
let theta_d = Theta.theta tag p in |
|
134 |
if Mod.modular D p then T.(eval_act mod_theta (call Dcall p)) |
|
135 |
else theta_d |
|
136 |
| X -> |
|
137 |
fun p f -> |
|
138 |
let theta_x = Theta.theta tag p f in |
|
139 |
if Mod.modular X p f then T.(eval_act mod_theta (call Xcall (p, f))) |
|
140 |
else theta_x |
|
119 | 141 |
end |
120 | 142 |
|
121 | 143 |
module type ThetaifyType = functor (Kenv : KenvType) -> MemoThetaType |
122 | 144 |
|
123 |
module BasicThetaify : ThetaifyType = functor (Kenv : KenvType) -> |
|
124 |
struct |
|
125 |
type t = T.t |
|
126 |
|
|
127 |
let theta_ify : type a b. kenv_t -> (a, b, T.t) theta_t = |
|
128 |
fun kenv tag -> |
|
129 |
match tag with |
|
130 |
| J -> (fun j -> |
|
131 |
try List.assoc j kenv.cont_junc kenv |
|
132 |
with Not_found -> |
|
133 |
Format.eprintf "Lost junction %a@ " pp_junction_name j; |
|
134 |
assert false) |
|
135 |
| E -> (fun p -> |
|
136 |
try |
|
137 |
let (e, _, _) = List.assoc p kenv.cont_node in e kenv |
|
138 |
with Not_found -> |
|
139 |
Format.eprintf "Entering lost path [%a]@." pp_path p; assert false) |
|
140 |
| D -> (fun p -> |
|
141 |
try |
|
142 |
let (_, d, _) = List.assoc p kenv.cont_node in d kenv |
|
143 |
with Not_found -> |
|
144 |
Format.eprintf "During lost path [%a]@." pp_path p; assert false) |
|
145 |
| X -> (fun p -> |
|
146 |
try |
|
147 |
let (_, _, x) = List.assoc p kenv.cont_node in x kenv |
|
148 |
with Not_found -> |
|
149 |
Format.eprintf "Exiting lost path [%a]@." pp_path p; assert false) |
|
150 |
|
|
151 |
let theta tag = theta_ify Kenv.kenv tag |
|
152 |
|
|
153 |
let components _call = [] |
|
154 |
end |
|
155 |
|
|
156 |
module ModularThetaify : functor (Tables : MemoThetaTablesType) (Mod : ModularType) -> ThetaifyType = |
|
157 |
functor (Tables : MemoThetaTablesType) (Mod : ModularType) (Kenv : KenvType) -> |
|
158 |
Modularize (Mod) (Memoize (Tables) (BasicThetaify (Kenv))) |
|
159 |
|
|
145 |
module BasicThetaify : ThetaifyType = |
|
146 |
functor |
|
147 |
(Kenv : KenvType) |
|
148 |
-> |
|
149 |
struct |
|
150 |
type t = T.t |
|
151 |
|
|
152 |
let theta_ify : type a b. kenv_t -> (a, b, T.t) theta_t = |
|
153 |
fun kenv tag -> |
|
154 |
match tag with |
|
155 |
| J -> ( |
|
156 |
fun j -> |
|
157 |
try List.assoc j kenv.cont_junc kenv |
|
158 |
with Not_found -> |
|
159 |
Format.eprintf "Lost junction %a@ " pp_junction_name j; |
|
160 |
assert false) |
|
161 |
| E -> ( |
|
162 |
fun p -> |
|
163 |
try |
|
164 |
let e, _, _ = List.assoc p kenv.cont_node in |
|
165 |
e kenv |
|
166 |
with Not_found -> |
|
167 |
Format.eprintf "Entering lost path [%a]@." pp_path p; |
|
168 |
assert false) |
|
169 |
| D -> ( |
|
170 |
fun p -> |
|
171 |
try |
|
172 |
let _, d, _ = List.assoc p kenv.cont_node in |
|
173 |
d kenv |
|
174 |
with Not_found -> |
|
175 |
Format.eprintf "During lost path [%a]@." pp_path p; |
|
176 |
assert false) |
|
177 |
| X -> ( |
|
178 |
fun p -> |
|
179 |
try |
|
180 |
let _, _, x = List.assoc p kenv.cont_node in |
|
181 |
x kenv |
|
182 |
with Not_found -> |
|
183 |
Format.eprintf "Exiting lost path [%a]@." pp_path p; |
|
184 |
assert false) |
|
185 |
|
|
186 |
let theta tag = theta_ify Kenv.kenv tag |
|
187 |
|
|
188 |
let components _call = [] |
|
189 |
end |
|
190 |
|
|
191 |
module ModularThetaify : functor |
|
192 |
(Tables : MemoThetaTablesType) |
|
193 |
(Mod : ModularType) |
|
194 |
-> ThetaifyType = |
|
195 |
functor |
|
196 |
(Tables : MemoThetaTablesType) |
|
197 |
(Mod : ModularType) |
|
198 |
(Kenv : KenvType) |
|
199 |
-> |
|
200 |
Modularize (Mod) (Memoize (Tables) (BasicThetaify (Kenv))) |
|
160 | 201 |
end |
Also available in: Unified diff
reformatting