1
|
(* this file is no longer used. It contains the code that enable the use of the
|
2
|
CPS to build an evaluator.
|
3
|
|
4
|
Three pieces of code: - excerpt from the main that instanciate the functor to
|
5
|
the evaluator and run the provided trace - run_trace function - Evaluator
|
6
|
module *)
|
7
|
|
8
|
let _main_ _ = function
|
9
|
| Eval ->
|
10
|
let module Model = (val model) in
|
11
|
let module T = CPS_transformer.Evaluator in
|
12
|
let module Sem = CPS.Semantics (T) (Model) in
|
13
|
let nb_traces = List.length Model.traces in
|
14
|
if nb_traces = 0 then
|
15
|
failwith ("no available traces for model " ^ Model.name);
|
16
|
if !trace_id >= 0 && !trace_id < nb_traces then
|
17
|
let eval_func =
|
18
|
match !eval_mode with
|
19
|
| CPSEval ->
|
20
|
fun (evt, env) ->
|
21
|
let _, env', actions_performed =
|
22
|
Sem.compute modularmode (evt, env, [])
|
23
|
in
|
24
|
env', actions_performed
|
25
|
in
|
26
|
run_trace Model.model eval_func (List.nth Model.traces !trace_id)
|
27
|
else
|
28
|
failwith
|
29
|
(string_of_int !trace_id ^ " is not a valid trace index in [0.."
|
30
|
^ string_of_int nb_traces ^ "]")
|
31
|
|
32
|
let run_trace model func t =
|
33
|
let init_env = Datatype.SF.init_env model in
|
34
|
let _ =
|
35
|
Format.printf "Model definitions@.%a@.Initial state: %s @.####"
|
36
|
Datatype.SF.pp_src (snd model) (fst model)
|
37
|
in
|
38
|
|
39
|
let final_env, cpt =
|
40
|
List.fold_left
|
41
|
(fun (env, cpt) event ->
|
42
|
Format.printf "#### %i@.%a@." cpt ActiveStates.Env.pp_env env;
|
43
|
Format.printf "-- Event %a --@." Basetypes.pp_event event;
|
44
|
let env', actions_performed = func (event, env) in
|
45
|
let _ =
|
46
|
match actions_performed with
|
47
|
| [] ->
|
48
|
Format.printf "-- no action performed --@."
|
49
|
| _ ->
|
50
|
Format.printf "@[<v 2>-- action performed --@ ";
|
51
|
List.iter (fun a -> Format.printf "%s@ " a) actions_performed;
|
52
|
Format.printf "@]@."
|
53
|
in
|
54
|
(* we do not consider produced events *)
|
55
|
env', cpt + 1)
|
56
|
(init_env, 1) t
|
57
|
in
|
58
|
Format.printf "#### %i@.%a@." cpt ActiveStates.Env.pp_env final_env;
|
59
|
()
|
60
|
|
61
|
type truc = A of base_action_t | C of base_condition_t
|
62
|
|
63
|
module Evaluator :
|
64
|
TransformerType
|
65
|
with type t =
|
66
|
event_t * bool ActiveStates.Env.t * truc list ->
|
67
|
event_t * bool ActiveStates.Env.t * truc list = struct
|
68
|
include TransformerStub
|
69
|
|
70
|
type env_t = event_t * bool ActiveStates.Env.t * truc list
|
71
|
(* Don't care for values yet *)
|
72
|
|
73
|
type t = env_t -> env_t
|
74
|
|
75
|
let null rho = rho
|
76
|
|
77
|
let add_action a (evt, rho, al) = evt, rho, al @ [ A a ]
|
78
|
(* not very efficient but avoid to keep track of action order *)
|
79
|
|
80
|
let add_condition c (evt, rho, al) = evt, rho, al @ [ C c ]
|
81
|
(* not very efficient but avoid to keep track of action order *)
|
82
|
|
83
|
let bot _ = assert false
|
84
|
|
85
|
let ( >> ) tr1 tr2 rho = rho |> tr1 |> tr2
|
86
|
|
87
|
let ( ?? ) b tr = if b then tr else null
|
88
|
|
89
|
let eval_open p (evt, rho, al) = evt, ActiveStates.Env.add p true rho, al
|
90
|
|
91
|
let eval_close p (evt, rho, al) = evt, ActiveStates.Env.add p false rho, al
|
92
|
|
93
|
let eval_call :
|
94
|
type c. (module ThetaType with type t = t) -> c call_t -> c -> t =
|
95
|
fun kenv ->
|
96
|
let module Theta = (val kenv : ThetaType with type t = t) in
|
97
|
fun call ->
|
98
|
match call with
|
99
|
| Ecall ->
|
100
|
fun (p, p', f) -> Theta.theta E p p' f
|
101
|
| Dcall ->
|
102
|
fun p -> Theta.theta D p
|
103
|
| Xcall ->
|
104
|
fun (p, f) -> Theta.theta X p f
|
105
|
|
106
|
let eval_act kenv action =
|
107
|
(* Format.printf "----- action = %a@." Action.pp_act action; *)
|
108
|
match action with
|
109
|
| Action.Call (c, a) ->
|
110
|
eval_call kenv c a
|
111
|
| Action.Quote a ->
|
112
|
add_action a
|
113
|
| Action.Open p ->
|
114
|
eval_open p
|
115
|
| Action.Close p ->
|
116
|
eval_close p
|
117
|
| Action.Nil ->
|
118
|
null
|
119
|
|
120
|
(*if (match trans.event with None -> true | _ -> e = trans.event) &&
|
121
|
trans.condition rho*)
|
122
|
let rec eval_cond condition ok ko : t =
|
123
|
(* Format.printf "----- cond = %a@." Condition.pp_cond condition; *)
|
124
|
match condition with
|
125
|
| Condition.True ->
|
126
|
ok
|
127
|
| Condition.Active p ->
|
128
|
fun ((evt, env, al) as rho) ->
|
129
|
if ActiveStates.Env.find p env then ok rho else ko rho
|
130
|
| Condition.Event e -> (
|
131
|
fun ((evt, env, al) as rho) ->
|
132
|
match evt with
|
133
|
| None ->
|
134
|
ko rho
|
135
|
| Some e' ->
|
136
|
if e = e' then ok rho else ko rho)
|
137
|
| Condition.Neg cond ->
|
138
|
eval_cond cond ko ok
|
139
|
| Condition.And (cond1, cond2) ->
|
140
|
eval_cond cond1 (eval_cond cond2 ok ko) ko
|
141
|
| Condition.Quote c ->
|
142
|
add_condition c >> ok
|
143
|
(* invalid behavior but similar to the other: should evaluate condition *)
|
144
|
|
145
|
let pp_transformer fmt tr = Format.fprintf fmt "<transformer>"
|
146
|
|
147
|
let pp_principal fmt tr =
|
148
|
Format.fprintf fmt "principal =@.%a" pp_transformer tr
|
149
|
|
150
|
let pp_component : type c. Format.formatter -> c call_t -> c -> t -> unit =
|
151
|
fun fmt call ->
|
152
|
match call with
|
153
|
| Ecall ->
|
154
|
fun (p, p', f) tr ->
|
155
|
Format.fprintf fmt "component %a(%a, %a, %a) =@.%a" pp_call call pp_path
|
156
|
p pp_path p' pp_frontier f pp_transformer tr
|
157
|
| Dcall ->
|
158
|
fun p tr ->
|
159
|
Format.fprintf fmt "component %a(%a) =@.%a" pp_call call pp_path p
|
160
|
pp_transformer tr
|
161
|
| Xcall ->
|
162
|
fun (p, f) tr ->
|
163
|
Format.fprintf fmt "component %a(%a, %a) =@.%a" pp_call call pp_path p
|
164
|
pp_frontier f pp_transformer tr
|
165
|
end
|