Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / tools / stateflow / semantics / cPS_evaluator.ml @ 3769b712

History | View | Annotate | Download (5.14 KB)

1
  (* this file is no longer used. It contains the code that enable the use of
2
     the CPS to build an evaluator.
3
     
4
     Three pieces of code:
5
     - excerpt from the main that instanciate the functor to the evaluator and run the provided trace 
6
     - run_trace function
7
     - Evaluator module
8
 *)
9

    
10
 open Lustrec
11

    
12
  let _main_ _ = function 
13
    | Eval ->
14
     let module Model = (val model) in
15
     let module T = CPS_transformer.Evaluator in
16
     let module Sem = CPS.Semantics (T) (Model) in
17
     let nb_traces = List.length Model.traces in
18
     if nb_traces = 0 then
19
       failwith ("no available traces for model " ^ Model.name);
20
     if !trace_id >= 0 && !trace_id < nb_traces then
21
       let eval_func = 
22
	 match !eval_mode with
23
	 | CPSEval -> 
24
	    fun (evt, env) ->
25
	      let _, env', actions_performed = Sem.compute modularmode (evt, env, []) in
26
	      env', actions_performed
27
       in
28
       run_trace Model.model eval_func (List.nth Model.traces !trace_id)
29
	 
30
     else
31
       failwith (string_of_int !trace_id ^
32
		   " is not a valid trace index in [0.." ^ string_of_int nb_traces ^ "]")
33

    
34

    
35

    
36
let run_trace model func t =
37
  let init_env = Datatype.SF.init_env model in
38
  let _ = Format.printf "Model definitions@.%a@.Initial state: %s @.####" Datatype.SF.pp_src (snd model) (fst model) in 
39
  
40
  let final_env, cpt =
41
    List.fold_left (fun (env, cpt) event ->
42
      Format.printf "#### %i@.%a@." cpt ActiveStates.Lustrec.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
      | [] -> Format.printf "-- no action performed --@."
48
      | _ -> (
49
	Format.printf "@[<v 2>-- action performed --@ ";
50
	List.iter (fun a -> Format.printf "%s@ " a) actions_performed;
51
	Format.printf "@]@."
52
      ) in
53
      (* we do not consider produced events *)
54
      env', cpt+1
55
    ) (init_env, 1) t
56
  in
57
  Format.printf "#### %i@.%a@." cpt ActiveStates.Lustrec.Env.pp_env final_env;
58
  ()
59

    
60

    
61
    type truc = A of base_action_t | C of base_condition_t
62
module Evaluator : TransformerType with type t = (event_t * bool ActiveStates.Lustrec.Env.t * truc list) -> (event_t * bool ActiveStates.Lustrec.Env.t * truc list ) =
63
struct
64
  include TransformerStub
65
  type env_t = event_t * bool ActiveStates.Lustrec.Env.t * truc list (* Don't care for values yet *)
66
  type t = env_t -> env_t
67
 
68
  let null rho = rho
69
  let add_action a (evt, rho, al) = (evt, rho, al@[A a]) (* not very efficient but
70
							  avoid to keep track of
71
							  action order *)
72
  let add_condition c (evt, rho, al) = (evt, rho, al@[C c]) (* not very efficient but
73
							  avoid to keep track of
74
							  action order *)
75

    
76
  let bot _ = assert false
77
 
78
  let ( >> ) tr1 tr2 = fun rho -> rho |> tr1 |> tr2
79

    
80
  let ( ?? ) b tr = if b then tr else null
81

    
82
  let eval_open p (evt, rho, al)  = (evt, ActiveStates.Lustrec.Env.add p true rho, al)
83
  let eval_close p (evt, rho, al) = (evt, ActiveStates.Lustrec.Env.add p false rho, al)
84
  let eval_call : type c. (module ThetaType with type t = t) -> c call_t -> c -> t =
85
    fun kenv ->
86
    let module Theta = (val kenv : ThetaType with type t = t) in	      
87
    fun call -> match call with
88
    | Ecall -> (fun (p, p', f) -> Theta.theta E p p' f)
89
    | Dcall -> (fun p          -> Theta.theta D p)
90
    | Xcall -> (fun (p, f)     -> Theta.theta X p f)
91

    
92
  let eval_act kenv action =
93
    (* Format.printf "----- action = %a@." Action.pp_act action; *)
94
    match action with
95
    | Action.Call (c, a)      -> eval_call kenv c a
96
    | Action.Quote a          -> add_action a
97
    | Action.Open p           -> eval_open p
98
    | Action.Close p          -> eval_close p
99
    | Action.Nil              -> null
100

    
101
  (*if (match trans.event with None -> true | _ -> e = trans.event) && trans.condition rho*)
102
  let rec eval_cond condition ok ko : t =
103
    (* Format.printf "----- cond = %a@." Condition.pp_cond condition; *)
104
    match condition with
105
    | Condition.True               -> ok
106
    | Condition.Active p           -> (fun ((evt, env, al) as rho) -> if ActiveStates.Lustrec.Env.find p env then ok rho else ko rho)
107
    | Condition.Event e            -> (fun ((evt, env, al) as rho) -> match evt with None -> ko rho | Some e' -> if e=e' then ok rho else ko rho)
108
    | Condition.Neg cond           -> eval_cond cond ko ok
109
    | Condition.And (cond1, cond2) -> eval_cond cond1 (eval_cond cond2 ok ko) ko
110
    | Condition.Quote c            -> add_condition c >> ok (* invalid behavior but similar to the other: should evaluate condition *)
111

    
112
  let pp_transformer fmt tr =
113
    Format.fprintf fmt "<transformer>"
114

    
115
  let pp_principal fmt tr =
116
    Format.fprintf fmt "principal =@.%a" pp_transformer tr
117

    
118
  let pp_component : type c. Format.formatter -> c call_t -> c -> t -> unit =
119
    fun fmt call -> match call with
120
    | Ecall -> (fun (p, p', f) tr ->
121
      Format.fprintf fmt "component %a(%a, %a, %a) =@.%a" pp_call call pp_path p pp_path p' pp_frontier f pp_transformer tr)
122
    | Dcall -> (fun p tr ->
123
      Format.fprintf fmt "component %a(%a) =@.%a" pp_call call pp_path p pp_transformer tr)
124
    | Xcall -> (fun (p, f) tr ->
125
      Format.fprintf fmt "component %a(%a, %a) =@.%a" pp_call call pp_path p pp_frontier f pp_transformer tr)
126
end
127