Project

General

Profile

« Previous | Next » 

Revision ca7ff3f7

Added by LĂ©lio Brun 7 months ago

reformatting

View differences:

src/tools/stateflow/semantics/cPS_evaluator.ml
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
  let _main_ _ = function
11
    | Eval ->
12
     let module Model = (val model) in
13
     let module T = CPS_transformer.Evaluator in
14
     let module Sem = CPS.Semantics (T) (Model) in
15
     let nb_traces = List.length Model.traces in
16
     if nb_traces = 0 then
17
       failwith ("no available traces for model " ^ Model.name);
18
     if !trace_id >= 0 && !trace_id < nb_traces then
19
       let eval_func = 
20
	 match !eval_mode with
21
	 | CPSEval -> 
22
	    fun (evt, env) ->
23
	      let _, env', actions_performed = Sem.compute modularmode (evt, env, []) in
24
	      env', actions_performed
25
       in
26
       run_trace Model.model eval_func (List.nth Model.traces !trace_id)
27
	 
28
     else
29
       failwith (string_of_int !trace_id ^
30
		   " is not a valid trace index in [0.." ^ string_of_int nb_traces ^ "]")
1
(* this file is no longer used. It contains the code that enable the use of the
2
   CPS to build an evaluator.
31 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 *)
32 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 ^ "]")
33 31

  
34 32
let run_trace model func t =
35 33
  let init_env = Datatype.SF.init_env model in
36
  let _ = Format.printf "Model definitions@.%a@.Initial state: %s @.####" Datatype.SF.pp_src (snd model) (fst model) in 
37
  
34
  let _ =
35
    Format.printf "Model definitions@.%a@.Initial state: %s @.####"
36
      Datatype.SF.pp_src (snd model) (fst model)
37
  in
38

  
38 39
  let final_env, cpt =
39
    List.fold_left (fun (env, cpt) event ->
40
      Format.printf "#### %i@.%a@." cpt ActiveStates.Env.pp_env env;
41
      Format.printf "-- Event %a --@." Basetypes.pp_event event;
42
      let env', actions_performed = func (event, env) in
43
      let _ =
44
	match actions_performed with
45
      | [] -> Format.printf "-- no action performed --@."
46
      | _ -> (
47
	Format.printf "@[<v 2>-- action performed --@ ";
48
	List.iter (fun a -> Format.printf "%s@ " a) actions_performed;
49
	Format.printf "@]@."
50
      ) in
51
      (* we do not consider produced events *)
52
      env', cpt+1
53
    ) (init_env, 1) t
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
54 57
  in
55 58
  Format.printf "#### %i@.%a@." cpt ActiveStates.Env.pp_env final_env;
56 59
  ()
57 60

  
61
type truc = A of base_action_t | C of base_condition_t
58 62

  
59
    type truc = A of base_action_t | C of base_condition_t
60
module Evaluator : TransformerType with type t = (event_t * bool ActiveStates.Env.t * truc list) -> (event_t * bool ActiveStates.Env.t * truc list ) =
61
struct
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
62 68
  include TransformerStub
63
  type env_t = event_t * bool ActiveStates.Env.t * truc list (* Don't care for values yet *)
69

  
70
  type env_t = event_t * bool ActiveStates.Env.t * truc list
71
  (* Don't care for values yet *)
72

  
64 73
  type t = env_t -> env_t
65
 
74

  
66 75
  let null rho = rho
67
  let add_action a (evt, rho, al) = (evt, rho, al@[A a]) (* not very efficient but
68
							  avoid to keep track of
69
							  action order *)
70
  let add_condition c (evt, rho, al) = (evt, rho, al@[C c]) (* not very efficient but
71
							  avoid to keep track of
72
							  action order *)
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 *)
73 82

  
74 83
  let bot _ = assert false
75
 
76
  let ( >> ) tr1 tr2 = fun rho -> rho |> tr1 |> tr2
84

  
85
  let ( >> ) tr1 tr2 rho = rho |> tr1 |> tr2
77 86

  
78 87
  let ( ?? ) b tr = if b then tr else null
79 88

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

  
90 106
  let eval_act kenv action =
91 107
    (* Format.printf "----- action = %a@." Action.pp_act action; *)
92 108
    match action with
93
    | Action.Call (c, a)      -> eval_call kenv c a
94
    | Action.Quote a          -> add_action a
95
    | Action.Open p           -> eval_open p
96
    | Action.Close p          -> eval_close p
97
    | Action.Nil              -> null
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
98 119

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

  
110
  let pp_transformer fmt tr =
111
    Format.fprintf fmt "<transformer>"
145
  let pp_transformer fmt tr = Format.fprintf fmt "<transformer>"
112 146

  
113 147
  let pp_principal fmt tr =
114 148
    Format.fprintf fmt "principal =@.%a" pp_transformer tr
115 149

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

  

Also available in: Unified diff