Project

General

Profile

Revision 2de7fa82

View differences:

tools/stateflow/src/Makefile
1
sf_sem:
2
	ocamlbuild sf_sem.native
3
	cp sf_sem.native sf_sem
4

  
5
clean:
6
	rm -rf _build
7
	rm sf_sem.native
8

  
9
.PHONY: sf_sem
tools/stateflow/src/_tags
1
"models": include
2
"common": include
3
"semantics/CPS": include
4
"semantics/emsoft05": include
tools/stateflow/src/common/activeStates.ml
1
open Basetypes 
2

  
3
(* Module to manipulate set of active states.
4

  
5
   It relies on sets of path to represent active ones.
6
*)
7

  
8
(*******************************)
9
module Vars =
10
struct
11
  include Set.Make (struct type t = path_t let compare = compare end)
12

  
13
  let pp_set fmt rho =
14
    Format.fprintf fmt "@[<v 0>%a@ @]"
15
      (Utils.fprintf_list ~sep:"@ "
16
	 (fun fmt p -> Format.fprintf fmt "%a" pp_path p))
17
      (elements rho)
18
end
19

  
20
module Env =
21
struct
22
  include Map.Make (struct type t = path_t let compare = compare end)
23

  
24
  let from_set s default =
25
    Vars.fold (fun e m -> add e default m ) s empty
26
      
27
  let find a b =
28
    try 
29
      find a b
30
    with Not_found -> (
31
      Format.printf "Looking for %a@." pp_path a ;
32
      raise Not_found
33
    )
34
  let keys a =
35
    fold (fun key _ -> Vars.add key) a Vars.empty
36

  
37
  let pp_env fmt rho =
38
    Format.fprintf fmt "@[<v 0>%a@ @]"
39
      (Utils.fprintf_list ~sep:"@ "
40
	 (fun fmt (p,b) -> Format.fprintf fmt "%a -> %b" pp_path p b))
41
      (bindings rho)
42
end
43

  
44

  
tools/stateflow/src/common/basetypes.ml
1

  
2
(* Basic datatype for model elements: state and junction name, events ... *)
3
type state_name_t    = string
4
type junction_name_t = string
5
type path_t = state_name_t list
6
type event_base_t = string
7
type event_t      = event_base_t option
8
type base_action_t = string
9
type base_condition_t = string
10
  
11
(* P(r)etty printers *)
12
let pp_state_name = Format.pp_print_string
13
let pp_junction_name = Format.pp_print_string
14
let pp_path fmt p = Utils.fprintf_list ~sep:"." pp_state_name fmt p
15
let pp_event fmt e = match e with None -> Format.fprintf fmt "none" | Some s -> Format.fprintf fmt "%s" s
16
let pp_base_act = Format.pp_print_string
17
let pp_base_cond = Format.pp_print_string
18
  
19
(* Action and Condition types and functions. *)
20

  
21
(* Actions are defined by string + the opening and closing of states *)
22

  
23
(* This version is slightly more complex than the one of EMSOFT'05 to enable the
24
   use of function calls in action.
25

  
26
   TODO: these rich call type could be externalized and a functor introduced. *)
27

  
28
type frontier_t =
29
  | Loose
30
  | Strict
31

  
32
let pp_frontier fmt frontier =
33
  match frontier with
34
  | Loose  -> Format.fprintf fmt "Loose"
35
  | Strict -> Format.fprintf fmt "Strict"
36

  
37
type _ call_t =
38
  | Ecall : (path_t * path_t * frontier_t) call_t
39
  | Dcall : path_t call_t
40
  | Xcall : (path_t * frontier_t) call_t
41

  
42
let pp_call :
43
type a. Format.formatter -> a call_t -> unit = 
44
  fun fmt call ->
45
    match call with
46
    | Ecall -> Format.fprintf fmt "CallE"
47
    | Dcall -> Format.fprintf fmt "CallD"
48
    | Xcall -> Format.fprintf fmt "CallX"
49
  
50
module type ActionType =
51
sig
52
  type t
53
  val nil : t
54
  val aquote : base_action_t -> t
55
  val open_path : path_t -> t
56
  val close_path : path_t -> t
57
  val call : 'c call_t -> 'c -> t
58
    
59
  val pp_act : Format.formatter -> t -> unit
60
end
61

  
62

  
63
module Action =
64
struct
65
  type t =
66
    | Quote : base_action_t -> t
67
    | Close : path_t -> t
68
    | Open  : path_t -> t
69
    | Call  : 'c call_t * 'c -> t
70
    | Nil   : t
71

  
72
    
73
  let nil = Nil
74
  let aquote act = Quote act
75
  let open_path p = Open p
76
  let close_path p = Close p
77
  let call c a = Call (c, a)
78

  
79
  let pp_call : type c. Format.formatter -> c call_t -> c -> unit =
80
    fun fmt call ->
81
    match call with
82
    | Ecall -> (fun (p, p', f) -> Format.fprintf fmt "%a(%a, %a, %a)" pp_call call pp_path p pp_path p' pp_frontier f)
83
    | Dcall -> (fun p          -> Format.fprintf fmt "%a(%a)" pp_call call pp_path p)
84
    | Xcall -> (fun (p, f)     -> Format.fprintf fmt "%a(%a, %a)" pp_call call pp_path p pp_frontier f)
85

  
86
  let pp_act fmt act =
87
    match act with
88
    | Call (c, a)      -> pp_call fmt c a
89
    | Quote a          -> Format.fprintf fmt "%a" pp_base_act a
90
    | Close p          -> Format.fprintf fmt "Close(%a)" pp_path p
91
    | Open p           -> Format.fprintf fmt "Open(%a)" pp_path p
92
    | Nil              -> Format.fprintf fmt "Nil"
93
end
94

  
95
let _ = (module Action : ActionType) 
96

  
97

  
98
(* Conditions are either (1) simple strings, (2) the active status of a state or
99
   (3) occurence of an event. They can be combined (conjunction, negation) *)
100
module type ConditionType =
101
sig
102
  type t
103
  val cquote : base_condition_t -> t
104
  val tru : t
105
  val active : path_t -> t
106
  val event : event_t -> t
107
  val ( && ) : t -> t -> t
108
  val neg : t -> t
109

  
110
  val pp_cond : Format.formatter -> t -> unit
111
end
112

  
113
  module Condition =
114
struct
115
  type t =
116
    | Quote of base_condition_t
117
    | Active of path_t
118
    | Event of event_base_t
119
    | And of t * t
120
    | Neg of t
121
    | True
122

  
123
  let cquote cond = Quote cond
124
  let tru = True
125
  let neg cond = Neg cond
126
  let ( && ) cond1 cond2 = And (cond1, cond2)
127
  let active path = Active path
128
  let event evt =
129
    match evt with
130
    | None   -> True
131
    | Some e -> Event e
132

  
133
  let rec pp_cond fmt cond =
134
    match cond with
135
    | True               -> Format.fprintf fmt "true"
136
    | Active p           -> Format.fprintf fmt "Active(%a)" pp_path p
137
    | Event e            -> Format.fprintf fmt "Event(%s)" e
138
    | Neg cond           -> Format.fprintf fmt "(neg %a)" pp_cond cond
139
    | And (cond1, cond2) -> Format.fprintf fmt "%a /\\ %a" pp_cond cond1 pp_cond cond2
140
    | Quote c            -> Format.fprintf fmt "%a" pp_base_cond c
141

  
142
end
143

  
144
let _ = (module Condition : ConditionType)
tools/stateflow/src/common/datatype.ml
1
open Basetypes
2
(* open ActiveEnv *)
3

  
4
(* Type definitions of a model *)
5

  
6
type destination_t =
7
  | DPath of path_t
8
  | DJunction of junction_name_t
9

  
10
type trans_t = {
11
  event: event_t;
12
  condition: Condition.t;
13
  condition_act: Action.t;
14
  transition_act: Action.t;
15
  dest: destination_t;
16
}
17

  
18
type transitions_t = trans_t list
19

  
20
type composition_t =
21
  | Or of transitions_t * state_name_t list
22
  | And of state_name_t list
23

  
24
type state_actions_t = {
25
  entry_act: Action.t;
26
  during_act: Action.t;
27
  exit_act: Action.t;
28
}
29

  
30
type state_def_t = {
31
  state_actions : state_actions_t;
32
  outer_trans : transitions_t;
33
  inner_trans : transitions_t;
34
  internal_composition : composition_t;
35
}
36

  
37
type src_components_t =
38
  | State of path_t * state_def_t
39
  | Junction of junction_name_t * transitions_t
40

  
41
type prog_t = state_name_t * src_components_t list
42
  
43
type trace_t = event_t list
44
    
45
module type MODEL_T = sig
46
  val name : string
47
  val model : prog_t
48
  val traces: trace_t list
49
end
50
  
51
(* Module (S)tate(F)low provides basic constructors for action, condition,
52
   events, as well as printer functions *)
53
module SF =
54
struct
55

  
56
  (* Basic constructors *)
57
  
58
  let no_action    = Action.nil
59
  let no_condition = Condition.tru
60
  let no_event     = None
61
  let event s      = Some s
62
  let action s     = Action.aquote s
63
  let condition s  = Condition.cquote s
64
  let no_state_action    = {entry_act = no_action; during_act = no_action; exit_act = no_action; }
65
  let state_action a b c = {entry_act = a; during_act = b; exit_act = c; }
66

  
67
  let states (_, defs) =
68
    List.fold_left (fun res c -> match c with State (p, _) -> ActiveStates.Vars.add p res | Junction _ -> res) ActiveStates.Vars.empty defs
69

  
70
  let init_env model = ActiveStates.Env.from_set (states model) false
71
    
72
  (* Printers *)
73
      
74
  let pp_event fmt e =
75
    match e with
76
    | Some e -> Format.fprintf fmt "%s" e
77
    | None -> Format.fprintf fmt "noevent"
78
    
79
  let pp_dest fmt d = match d with
80
    | DPath p -> Format.fprintf fmt "Path %a" pp_path p
81
    | DJunction j -> Format.fprintf fmt "Junction %a" pp_junction_name j
82

  
83
  let pp_trans fmt t =
84
    Format.fprintf fmt
85
      "@[<hov 0>(@[<hov 0>%a,@ %a,@ %a,@ %a,@ %a@]@ )@]"
86
      pp_event t.event
87
      Condition.pp_cond t.condition
88
      Action.pp_act t.condition_act
89
      Action.pp_act t.transition_act    
90
      pp_dest t.dest
91
      
92
  let pp_transitions fmt l =
93
    Format.fprintf fmt
94
      "@[<hov 0>[@[<hov 0>%a@]@ ]@]"
95
      (Utils.fprintf_list ~sep:";@ " pp_trans) l
96

  
97
  let pp_comp fmt c = match c with
98
    | Or (_T, _S) ->
99
       Format.fprintf fmt "Or(%a, {%a})"
100
	 pp_transitions _T
101
	 (Utils.fprintf_list ~sep:"; " pp_state_name) _S
102
    | And (_S) ->
103
       Format.fprintf fmt "And({%a})"
104
	 (Utils.fprintf_list ~sep:"; " pp_state_name) _S
105

  
106
  let pp_state_actions fmt sa =
107
    Format.fprintf fmt "@[<hov 0>(%a,@ %a,@ %a)@]"
108
      Action.pp_act sa.entry_act
109
      Action.pp_act sa.during_act
110
      Action.pp_act sa.exit_act
111
      
112
  let pp_state fmt s =
113
    Format.fprintf fmt "@[<v 0>(@[<v 0>%a,@ %a,@ %a,@ %a@]@ @])"
114
      pp_state_actions s.state_actions
115
      pp_transitions s.outer_trans
116
      pp_transitions s.inner_trans
117
      pp_comp s.internal_composition
118
      
119
  let pp_src fmt src =
120
    Format.fprintf fmt "@[<v>%a@ @]"
121
      (Utils.fprintf_list ~sep:"@ @ " (fun fmt src -> match src with
122
	State (p, def) ->
123
	  Format.fprintf fmt "%a: %a"
124
	    pp_path p
125
	    pp_state def
126
      | Junction (s, tl) ->
127
	 Format.fprintf fmt "%a: %a"
128
	   pp_state_name s
129
	   pp_transitions tl
130
       ))
131
      src
132
end
133
   
tools/stateflow/src/common/log.ml
1
let debug = false
2

  
3
let log ?debug:(dbg=false) f =
4
  if debug || dbg then
5
    Format.printf "%t" f
6
  else
7
    ()
tools/stateflow/src/common/utils.ml
1
let rec fprintf_list ~sep:sep f fmt = function
2
  | []   -> ()
3
  | [e]  -> f fmt e
4
  | x::r -> Format.fprintf fmt "%a%(%)%a" f x sep (fprintf_list ~sep f) r
5

  
6
let last l = List.hd (List.rev l)
tools/stateflow/src/models/model_medium.ml
1
open Datatype
2
open SF
3

  
4
let name = "medium"
5

  
6
 
7
let model : prog_t =
8
    let state_main = "main" in
9
    let state_a = "a" in
10
    let state_a1 = "a1" in
11
    let state_b = "b" in
12

  
13
    let actions_main = state_action (action "emain") (action "dmain") (action "xmain") in
14
    let actions_a = state_action (action "eA") (action "dA") (action "xA") in
15
    let actions_a1 = state_action (action "eA1") (action "dA1") (action "xA1") in
16
    let actions_b = state_action (action "eB") (action "dB") (action "xB") in
17

  
18
    let tA = {
19
      event = no_event;
20
      condition = condition "cond_tA";
21
      condition_act = action "condact_tA";
22
      transition_act = action "transact_tA";
23
      dest = DPath [state_main;state_a];
24
    }
25
    in
26
    let tJ = {
27
      event = no_event;
28
      condition = condition "cond_tJ";
29
      condition_act = action "condact_tJ";
30
      transition_act = action "transact_tJ";
31
      dest = DJunction "jmid";
32
    }
33
    in
34
    let tB = {
35
      event = no_event;
36
      condition = condition "cond_tB";
37
      condition_act = action "condact_tB";
38
      transition_act = action "transact_tB";
39
      dest = DPath [state_main;state_b];
40
    }
41
    in
42
    let tA1 = {
43
      event = no_event;
44
      condition = condition "cond_tA1";
45
      condition_act = action "condact_tA1";
46
      transition_act = action "transact_tA1";
47
      dest = DPath [state_main;state_a;state_a1];
48
    }
49
    in
50

  
51

  
52
    let def_a = {
53
      state_actions = actions_a;
54
      outer_trans = [tJ];
55
      inner_trans = [];
56
      internal_composition = Or ([tA1], [state_a1])
57
    }
58
    in
59
    let def_a1 = {
60
      state_actions = actions_a1;
61
      outer_trans = [tB];
62
      inner_trans = [];
63
      internal_composition = Or ([], [])
64
    }
65
    in
66
    let def_b = {
67
      state_actions = actions_b;
68
      outer_trans = [tA1];
69
      inner_trans = [];
70
      internal_composition = Or ([], [])
71
    }
72
    in
73
    let def_main = {
74
      state_actions = actions_main;
75
      outer_trans = [];
76
      inner_trans = [];
77
      internal_composition = Or ([tA], [state_a; state_b])
78
    }
79
    in
80
    let src = [State([state_main;state_a], def_a);
81
	       State([state_main;state_a;state_a1], def_a1);
82
	       State([state_main;state_b], def_b);
83
	       State([state_main], def_main);
84
	       Junction("jmid", [tB]);
85
	      ]
86
    in
87
    (state_main, src)
88

  
89
let traces : trace_t list = [[None; None]]
tools/stateflow/src/models/model_simple.ml
1
open Datatype
2
open SF
3

  
4
let name = "simple"
5

  
6
 
7
let model : prog_t =
8
    let state_main = "main" in
9
    let state_a = "a" in
10
    let state_a1 = "a1" in
11
    let state_b = "b" in
12

  
13
    let actions_main = state_action (action "emain") (action "dmain") (action "xmain") in
14
    let actions_a = state_action (action "eA") (action "dA") (action "xA") in
15
    let actions_a1 = state_action (action "eA1") (action "dA1") (action "xA1") in
16
    let actions_b = state_action (action "eB") (action "dB") (action "xB") in
17

  
18
    let tA = {
19
      event = no_event;
20
      condition = condition "cond_tA";
21
      condition_act = action "condact_tA";
22
      transition_act = action "transact_tA";
23
      dest = DPath [state_main;state_a];
24
    }
25
    in
26
    let tB = {
27
      event = no_event;
28
      condition = condition "cond_tB";
29
      condition_act = action "condact_tB";
30
      transition_act = action "transact_tB";
31
      dest = DPath [state_main;state_b];
32
    }
33
    in
34
    let tA1 = {
35
      event = no_event;
36
      condition = condition "cond_tA1";
37
      condition_act = action "condact_tA1";
38
      transition_act = action "transact_tA1";
39
      dest = DPath [state_main;state_a;state_a1];
40
    }
41
    in
42

  
43

  
44
    let def_a = {
45
      state_actions = actions_a;
46
      outer_trans = [tB];
47
      inner_trans = [];
48
      internal_composition = Or ([tA1], [state_a1])
49
    }
50
    in
51
    let def_a1 = {
52
      state_actions = actions_a1;
53
      outer_trans = [tB];
54
      inner_trans = [];
55
      internal_composition = Or ([], [])
56
    }
57
    in
58
    let def_b = {
59
      state_actions = actions_b;
60
      outer_trans = [tA1];
61
      inner_trans = [];
62
      internal_composition = Or ([], [])
63
    }
64
    in
65
    let def_main = {
66
      state_actions = actions_main;
67
      outer_trans = [];
68
      inner_trans = [];
69
      internal_composition = Or ([tA], [state_a; state_b])
70
    }
71
    in
72
    let src = [State([state_main;state_a], def_a);
73
	       State([state_main;state_a;state_a1], def_a1);
74
	       State([state_main;state_b], def_b);
75
	       State([state_main], def_main);
76
	      ]
77
    in
78
    (state_main, src)
79

  
80
let traces : trace_t list = [[None; None]]
tools/stateflow/src/models/model_stopwatch.ml
1
open Datatype
2
(* open Transformer2 *)
3
open SF
4

  
5
let verbose = false
6
let actionv x = if verbose then action x else no_action
7
    
8
let name = "stopwatch"
9
  
10
let model = 
11
  let smain    = "main" in
12
  let sstop    = "stop" in
13
  let sreset   = "reset" in
14
  let slapstop = "lap_stop" in
15
  let srun     = "run" in
16
  let srunning = "running" in
17
  let slap     = "lap" in
18

  
19
  let tinitstop = {
20
    event = no_event;
21
    condition = no_condition;
22
    condition_act  = actionv "ac_cond_init_stop";
23
    transition_act = actionv "ac_trans_init_stop";
24
    dest = DPath [smain;sstop];
25
  }
26
  in
27
  let tinitreset = {
28
    event = no_event;
29
    condition = no_condition;
30
    condition_act  = actionv "ac_cond_init_reset";
31
    transition_act = actionv "ac_cond_init_stop";
32
    dest = DPath [smain;sstop;sreset];
33
  }
34
  in
35
  let treset = {
36
    event = event "LAP";
37
    condition = no_condition;
38
    condition_act  = action "reset counter";
39
    transition_act = actionv "ac_trans_reset_junction";
40
    dest = DJunction "jreset" (* [smain;sstop;sreset]; ou bien mettre une junction.  Verifier
41
				 si il y a des effets de bords non
42
				 desirés de fermeture/ouverture de
43
				 noeud *)
44
  }
45
  in
46
  let treset_start  = {
47
    event = event "START";
48
    condition = no_condition;
49
    condition_act  = actionv "ac_cond_reset->running";
50
    transition_act = actionv "ac_trans_reset->running";
51
    dest = DPath [smain;srun;srunning];
52
  }
53
  in
54
  
55
  let tlapstop_lap  = {
56
    event = event "LAP";
57
    condition = no_condition;
58
    condition_act  = actionv "ac_cond_lap_stop->reset";
59
    transition_act = actionv "ac_trans_lap_stop->reset";
60
    dest = DPath [smain;sstop;sreset];
61
  }
62
  in
63

  
64
  let tlapstop_start  = {
65
    event = event "START";
66
    condition = no_condition;
67
    condition_act  = actionv "ac_cond_lap_stop->lap";
68
    transition_act = actionv "ac_trans_lap_stop->lap";
69
    dest = DPath [smain;srun;slap];
70
  }
71
  in
72
  let ttic   = {
73
    event = event "TIC";
74
    condition = no_condition;
75
    condition_act  = action "cent+=1";
76
    transition_act = actionv "ac_trans_->J1";
77
    dest = DJunction "j1";
78
  }
79
  in
80
  let trunning_start  = {
81
    event = event "START";
82
    condition = no_condition;
83
    condition_act  = actionv "ac_cond_running->reset";
84
    transition_act = actionv "ac_trans_running->reset";
85
    dest = DPath [smain;sstop;sreset];
86
  }
87
  in
88
  let tlap_start  = {
89
    event = event "START";
90
    condition = no_condition;
91
    condition_act  = actionv "ac_cond_lap->lap_stop";
92
    transition_act = actionv "ac_trans_lap->lap_stop";
93
    dest = DPath [smain;sstop;slapstop];
94
  }
95
  in
96
  let tlap_lap  = {
97
    event = event "LAP";
98
    condition = no_condition;
99
    condition_act  = actionv "ac_cond_lap->running";
100
    transition_act = actionv "ac_trans_lap->running";
101
    dest = DPath [smain;srun;srunning];
102
  }
103
  in
104
  let trunning_lap  = {
105
    event = event "LAP";
106
    condition = no_condition;
107
    condition_act  = actionv "ac_cond_running->lap";
108
    transition_act = actionv "ac_trans_running->lap";
109
    dest = DPath [smain;srun;slap];
110
  }
111
  in
112
  let tj1j2 = {
113
    event = no_event;
114
    condition = condition "cent==100";
115
    condition_act  = action "cont=0;sec+=1";
116
    transition_act = actionv "ac_trans_J1->J2";
117
    dest = DJunction "j2";
118
  }
119
  in
120
  let tj1j3 =    {
121
    event = no_event;
122
    condition = condition "cent!=100";
123
    condition_act  = actionv "ac_cond_J1->J3";
124
    transition_act = actionv "ac_trans_J1->J3";
125
    dest = DJunction "j3";
126
  }
127
  in
128
  let tj2j3gauche   = {
129
    event = no_event;
130
    condition = condition "sec!=60";
131
    condition_act  = actionv "ac_cond_J2->J3_left";
132
    transition_act = actionv "ac_trans_J2->J3_left";
133
    dest = DJunction "j3";
134
  }
135
  in
136
  let tj2j3droite    = {
137
    event = no_event;
138
    condition = condition "sec==60";
139
    condition_act  = action "sec=0; min+=1";
140
    transition_act = actionv "ac_trans_J2->J3_right";
141
    dest = (*DPath [smain;srun];*) DJunction "j3";
142
  }
143
  in
144
  let def_main = {
145
    state_actions = {
146
      entry_act  = actionv "ac_main_entry";
147
      during_act = actionv "ac_main_during";
148
      exit_act   = actionv "ac_main_exit";
149
    };
150
    outer_trans = [];
151
    inner_trans = [];
152
    internal_composition = Or ([tinitstop], [sstop; srun])
153
  }
154
  in
155

  
156
  let def_stop = {
157
    state_actions = {
158
      entry_act  = actionv "ac_stop_entry";
159
      during_act = actionv "ac_stop_during";
160
      exit_act   = actionv "ac_stop_exit";
161
    };
162
    outer_trans = [];
163
    inner_trans = [];
164
    internal_composition = Or ([tinitreset], [sreset; slapstop])
165
  }
166
  in
167

  
168
  let def_reset = {
169
    state_actions = {
170
      entry_act  = actionv "ac_reset_entry";
171
      during_act = actionv "ac_reset_during";
172
      exit_act   = actionv "ac_reset_exit";
173
    };
174
    outer_trans = [treset_start];
175
    inner_trans = [treset];
176
    internal_composition = Or ([treset_start], [])
177
  }
178
  in
179

  
180
  let def_lapstop = {
181
    state_actions = {
182
      entry_act  = actionv "ac_lapstop_entry";
183
      during_act = actionv "ac_lapstop_during";
184
      exit_act   = actionv "ac_lapstop_exit";
185
    };
186
    outer_trans = [tlapstop_lap; tlapstop_start];
187
    inner_trans = [];
188
    internal_composition = Or ([], [])
189
  }
190
  in
191

  
192
  let def_run = {
193
    state_actions = {
194
      entry_act  = actionv "ac_run_entry";
195
      during_act = actionv "ac_run_during";
196
      exit_act   = actionv "ac_run_exit";
197
    };
198
    outer_trans = [];
199
    inner_trans = [ttic];
200
    internal_composition = Or ([], [srunning; slap])
201
  }
202
  in
203

  
204
  let def_running = {
205
    state_actions = {
206
      entry_act  = actionv "ac_running_entry";
207
      during_act = action "disp=(cent,sec,min)";
208
      exit_act   = actionv "ac_running_exit";
209
    };
210
    outer_trans = [trunning_start; trunning_lap];
211
    inner_trans = [];
212
    internal_composition = Or ([], [])
213
  }
214
  in
215

  
216
  let def_lap = {
217
    state_actions = {
218
      entry_act  = actionv "ac_lap_entry";
219
      during_act = actionv "ac_lap_during";
220
      exit_act   = actionv "ac_lap_exit";
221
    };
222
    outer_trans = [tlap_start; tlap_lap];
223
    inner_trans = [];
224
    internal_composition = Or ([], [])
225
  }
226
  in
227

  
228
  let src = [
229
    State([smain;srun;srunning], def_running);
230
    State([smain;srun;slap], def_lap);
231
    State([smain;srun], def_run);
232
    State([smain;sstop;sreset], def_reset);
233
    State([smain;sstop;slapstop], def_lapstop);
234
    State([smain;sstop], def_stop);
235
    State([smain], def_main);
236
    Junction("jreset", []);
237
    Junction("j1", [tj1j2;tj1j3]);
238
    Junction("j2", [tj2j3droite; tj2j3gauche]);
239
    Junction("j3", []);
240
  ]
241
  in
242
  (smain, src)
243

  
244
let traces : trace_t list =
245
  [
246
    [None; Some "TIC"; Some "START"; Some "TIC"; Some "TIC"];
247
    [None; Some "START"; Some "START"; Some "START"];
248
    [None; Some "START"; Some "TIC"; Some "START"; Some "TIC"]
249
  ]
tools/stateflow/src/semantics/CPS/cPS.ml
1
open Basetypes 
2
open Datatype
3
open CPS_transformer
4
open Theta 
5

  
6
module Semantics = functor (T: TransformerType) (M: MODEL_T) ->
7
struct
8
  
9
module Prog =
10
struct
11
  let init = fst M.model
12
  let defs = snd M.model
13
  let vars = SF.states M.model
14
(*let _ = Format.printf "Model definitions@.%a@.####" Simulink.pp_src defs; () *)
15
end
16

  
17

  
18
module Interp = CPS_interpreter.Interpreter (T)
19
module KenvTheta = KenvTheta (T)
20
module Tables = KenvTheta.MemoThetaTables ()
21

  
22
let eval ((modular_entry:bool), (modular_during:bool), (modular_exit:bool)) =
23
  let module Modularity : KenvTheta.ModularType =
24
      struct
25
	let modular : type b. (path_t, b, bool) tag_t -> path_t -> b =
26
			fun tag ->
27
			  match tag with
28
			  | E -> (fun p p' f -> modular_entry)
29
			  | D -> (fun p      -> modular_during)
30
			  | X -> (fun p f    -> modular_exit)
31
      end
32
  in
33
  let module Thetaify = KenvTheta.ModularThetaify (Tables) (Modularity) in
34
  let module EvalProg = Interp.Evaluation (Thetaify) (Prog) in
35
  (module EvalProg: Interp.EvaluationType)
36
  
37
let compute modular  =
38
  let module Eval = (val (eval modular)) in
39
  Eval.eval_prog 
40
    
41
let code_gen fmt modular  =
42
  let module Eval = (val (eval modular)) in
43
  let principal, components =  Eval.eval_prog, Eval.eval_components in
44
  Format.fprintf fmt "%a@." T.pp_principal principal;
45

  
46
  List.iter
47
    (fun (c, tr) -> Format.fprintf fmt "@.%a@." (fun fmt -> T.pp_component fmt Ecall c) tr)
48
    (components Ecall);
49
  List.iter
50
    (fun (c, tr) -> Format.fprintf fmt "@.%a@." (fun fmt -> T.pp_component fmt Dcall c) tr)
51
    (components Dcall);
52
  List.iter
53
    (fun (c, tr) -> Format.fprintf fmt "@.%a@." (fun fmt -> T.pp_component fmt Xcall c) tr)
54
    (components Xcall);
55

  
56
  ()
57

  
58
end
tools/stateflow/src/semantics/CPS/cPS_interpreter.ml
1
open Basetypes 
2
open Datatype
3
(* open ActiveEnv *)
4
open CPS_transformer
5
(* open Simulink *)
6
open Theta 
7

  
8
module Interpreter (Transformer : TransformerType) =
9
struct
10
  module KT = KenvTheta (Transformer)
11
  open KT
12

  
13
  let ( >? ) cond tr =
14
    if cond then tr else Transformer.null
15

  
16
  module type DenotationType =
17
  sig
18
    module Theta : MemoThetaType
19

  
20
    val eval_dest : destination_t -> Transformer.t wrapper_t -> Transformer.t success_t -> Transformer.t fail_t -> Transformer.t
21
    val eval_tau : trans_t -> Transformer.t wrapper_t -> Transformer.t success_t -> Transformer.t fail_t -> Transformer.t
22
    val eval_T : transitions_t -> Transformer.t wrapper_t -> Transformer.t success_t -> Transformer.t fail_t -> Transformer.t
23
    val eval_C : (path_t, 'b, Transformer.t) tag_t -> path_t -> composition_t -> Transformer.t
24
    val eval_open_path : mode_t -> path_t -> path_t -> Transformer.t wrapper_t
25
    val eval_S : (path_t, 'b, Transformer.t) tag_t -> path_t -> state_def_t -> 'b
26
  end
27

  
28
  module type AbsDenotationType =
29
  sig
30
    val eval_dest : kenv_t -> destination_t -> Transformer.t wrapper_t -> Transformer.t success_t -> Transformer.t fail_t -> Transformer.t
31
    val eval_tau : kenv_t -> trans_t -> Transformer.t wrapper_t -> Transformer.t success_t -> Transformer.t fail_t -> Transformer.t
32
    val eval_T : kenv_t -> transitions_t -> Transformer.t wrapper_t -> Transformer.t success_t -> Transformer.t fail_t -> Transformer.t
33
    val eval_C : kenv_t -> (path_t, 'b, Transformer.t) tag_t -> path_t -> composition_t -> Transformer.t
34
    val eval_open_path : kenv_t -> mode_t -> path_t -> path_t -> Transformer.t wrapper_t
35
    val eval_S : kenv_t -> (path_t, 'b, Transformer.t) tag_t -> path_t -> state_def_t -> 'b
36
  end
37

  
38
  module AbstractKenv (Denot : functor (Kenv : KenvType) -> DenotationType) : AbsDenotationType =
39
  struct
40
    let eval_dest kenv =
41
      let module Kenv =
42
	  struct
43
	    let kenv = kenv
44
	  end in
45
      let module D = Denot (Kenv) in
46
      D.eval_dest
47

  
48
    let eval_tau kenv =
49
      let module Kenv =
50
	  struct
51
	    let kenv = kenv
52
	  end in
53
      let module D = Denot (Kenv) in
54
      D.eval_tau
55

  
56
    let eval_T kenv =
57
      let module Kenv =
58
	  struct
59
	    let kenv = kenv
60
	  end in
61
      let module D = Denot (Kenv) in
62
      D.eval_T
63

  
64
    let eval_C kenv =
65
      let module Kenv =
66
	  struct
67
	    let kenv = kenv
68
	  end in
69
      let module D = Denot (Kenv) in
70
      D.eval_C
71

  
72
    let eval_open_path kenv =
73
      let module Kenv =
74
	  struct
75
	    let kenv = kenv
76
	  end in
77
      let module D = Denot (Kenv) in
78
      D.eval_open_path
79

  
80
    let eval_S kenv =
81
      let module Kenv =
82
	  struct
83
	    let kenv = kenv
84
	  end in
85
      let module D = Denot (Kenv) in
86
      D.eval_S
87
  end
88

  
89
  module Denotation : functor (Thetaify : ThetaifyType) (Kenv : KenvType) -> DenotationType =
90
  functor (Thetaify : ThetaifyType) (Kenv : KenvType) ->
91
  struct
92
    module Theta = Thetaify (Kenv)
93

  
94
    let eval_dest dest wrapper success fail =
95
      Log.log (fun fmt -> Format.fprintf fmt "@[<v 2>D[[%a]]@ " SF.pp_dest dest);
96
      match dest with
97
      | DPath p -> wrapper p (success p)
98
      | DJunction j -> Theta.theta J j wrapper success fail
99

  
100
    let eval_tau trans wrapper success fail =
101
      Log.log (fun fmt -> Format.fprintf fmt "@[<v 2>tau[[%a]]@ " SF.pp_trans trans);
102
      let success' p =
103
	Transformer.(success p >> eval_act (module Theta) trans.transition_act)
104
      in
105
      let cond = Transformer.(event trans.event && trans.condition) in
106
      Transformer.(eval_cond cond
107
		     (eval_act (module Theta) trans.condition_act >> eval_dest trans.dest wrapper success' fail)
108
		     fail.local)
109

  
110
    let rec eval_T tl wrapper success fail =
111
      Log.log ~debug:false (fun fmt -> Format.fprintf fmt "@[<v 2>T[[%a]]@ " SF.pp_transitions tl);
112
      match tl with
113
      | [] -> fail.global
114
      | t::[] ->  eval_tau t wrapper success fail
115
      | t::tl ->
116
	 let fail' = { fail with local = eval_T tl wrapper success fail } in
117
	 eval_tau t wrapper success fail'
118

  
119
    let frontier path =
120
      match path with
121
      | []   -> [], []
122
      | t::q -> [t], q
123

  
124
    let rec eval_open_path mode p p1 p2 success_p2 =
125
      Log.log ~debug:false (fun fmt -> Format.fprintf fmt "@[<v 2>open_path_rec[[mode %a, prefix %a, src %a, dst %a]]@ " pp_mode mode pp_path p pp_path p1 pp_path p2);
126
      match frontier p1, frontier p2 with
127
      | ([x], ps), ([y], pd) when x = y -> eval_open_path mode (p@[x]) ps pd success_p2
128
      | (x  , _ ), (y  , pd)            ->
129
	 match mode with
130
	 | Outer -> (Transformer.(Theta.theta X (p@x) Loose  >> success_p2 >> Theta.theta E (p@y) pd Loose))
131
	 | Inner -> (assert (x = []);
132
		     Transformer.(Theta.theta X (p@x) Strict >> success_p2 >> Theta.theta E (p@y) pd Strict))
133
	 | Enter -> (assert (x = [] && y <> []);
134
		     Transformer.(                              success_p2 >> Theta.theta E (p@y) pd Loose))
135

  
136
    let rec eval_C : type a b. (a, b, Transformer.t) tag_t -> path_t -> composition_t -> Transformer.t =
137
      fun tag prefix comp ->
138
	match tag with
139
	| E -> Transformer.(
140
	  Log.log ~debug:false (fun fmt -> Format.fprintf fmt "@[<v 2>C_%a[[%a, %a]]@ " pp_tag tag pp_path prefix SF.pp_comp comp);
141
	  match comp with
142
	  | Or (_T, [])   -> null
143
	  | Or ([], [s0]) -> eval_open_path Enter prefix [] [s0] null
144
	  | Or (_T, _S)   -> let wrapper = eval_open_path Enter [] prefix in
145
			     let success p_d = null in
146
			     eval_T _T wrapper success { local = bot; global = bot }
147
	  | And (_S)    -> List.fold_right (fun p -> (>>) (Theta.theta E (prefix@[p]) [] Loose)) _S null
148
	)
149
	| D -> Transformer.(
150
	  match comp with
151
	  | Or (_T, [])    -> null
152
	  | Or (_T, p::_S) -> eval_cond (active (prefix@[p])) (Theta.theta D (prefix@[p])) (eval_C D prefix (Or (_T, _S)))
153
	  | And (_S)       -> List.fold_right (fun p -> (>>) (Theta.theta D (prefix@[p]))) _S null
154
	)
155
	| X -> Transformer.(
156
	  match comp with
157
	  | Or (_T, [])    -> null
158
	  | Or (_T, p::_S) -> eval_cond (active (prefix@[p])) (Theta.theta X (prefix@[p]) Loose) (eval_C X prefix (Or (_T, _S)))
159
	  | And (_S)       -> List.fold_right (fun p -> (>>) (Theta.theta X (prefix@[p]) Loose)) _S null
160
	)
161
	| J -> assert false
162

  
163
    let eval_S : type b. (path_t, b, Transformer.t) tag_t -> path_t -> state_def_t -> b =
164
      fun tag p p_def ->
165
	match tag with
166
	| E -> fun path frontier -> Transformer.(
167
	  Log.log ~debug:false (fun fmt -> Format.fprintf fmt "@[<v 2>S_%a[[node %a, dest %a, frontier %a]]@ " pp_tag tag pp_path p pp_path path pp_frontier frontier);
168
	  ((frontier = Loose) >? (eval_act (module Theta) p_def.state_actions.entry_act >> eval_act (module Theta) (open_path p))) >> 
169
	  match path with
170
	  | []         -> eval_C E p p_def.internal_composition
171
	  | s::path_tl -> Theta.theta E (p@[s]) path_tl Loose
172
	)
173
	| D -> Transformer.(
174
	  Log.log ~debug:false (fun fmt -> Format.fprintf fmt "@[<v 2>S_%a[[node %a]]@ " pp_tag tag pp_path p);
175
	  let wrapper_i = eval_open_path Inner [] p in
176
	  let wrapper_o = eval_open_path Outer [] p in
177
	  let success p_d = null in
178
	  let fail_o =
179
	    let fail_i =
180
	      let same_fail_C = eval_C D p p_def.internal_composition in
181
	      { local = same_fail_C; global = same_fail_C }
182
	    in
183
	    let same_fail_i = eval_act (module Theta) p_def.state_actions.during_act >> eval_T p_def.inner_trans wrapper_i success fail_i in
184
	    { local = same_fail_i; global = same_fail_i }
185
	  in
186
	  eval_T p_def.outer_trans wrapper_o success fail_o
187
	)
188
	| X -> fun frontier -> Transformer.(
189
	  Log.log ~debug:false (fun fmt -> Format.fprintf fmt "@[<v 2>S_%a[[node %a, frontier %a]]@ " pp_tag tag pp_path p pp_frontier frontier);
190
	  eval_C X p p_def.internal_composition >>
191
	  ((frontier = Loose) >? (eval_act (module Theta) p_def.state_actions.exit_act >> eval_act (module Theta) (close_path p)))
192
	)
193
  end
194

  
195
  module type ProgType =
196
  sig
197
    val init : state_name_t
198
    val defs : src_components_t list
199
  end
200

  
201
  module type EvaluationType =
202
  sig
203
    module Theta : ThetaType with type t = Transformer.t
204
    val eval_prog : Transformer.t
205
    val eval_components : 'c call_t -> ('c * Transformer.t) list
206
  end
207
    
208
  module Evaluation (Thetaify : ThetaifyType) (Prog : ProgType) : EvaluationType =
209
  struct
210
    module Denotation = Denotation (Thetaify)
211
    module AbsDenotation = AbstractKenv (Denotation)
212
    include AbsDenotation
213

  
214
    module Kenv : KenvType =
215
    struct
216
      let kenv =
217
	List.fold_left (
218
	  fun accu d -> match d with
219
   | State (p, defp) -> { accu with cont_node = (p, ((fun kenv -> eval_S kenv E p defp), (fun kenv -> eval_S kenv D p defp), (fun kenv -> eval_S kenv X p defp)))::accu.cont_node  }
220
	  | Junction (j, defj) -> { accu with cont_junc = (j, (fun kenv -> eval_T kenv defj))::accu.cont_junc  }
221
	) {cont_node = []; cont_junc = []} Prog.defs
222
    end
223

  
224
    module AppDenotation = Denotation (Kenv)
225
    module Theta = AppDenotation.Theta
226

  
227
    let eval_components = Theta.components
228

  
229
    let eval_prog =
230
      Transformer.(eval_cond (active [Prog.init]) (Theta.theta D [Prog.init]) (Theta.theta E [Prog.init] [] Loose))
231
  end
232
 (*
233
  module ThetaFix (Prog : ProgType) (Theta : ThetaType) : ThetaType =
234
  struct
235
    include Denotation (Theta)
236

  
237
    let theta =
238
      let kenv =
239
	List.fold_left (
240
	  fun accu d -> match d with
241
	  | State (p, defp) -> { accu with cont_node = (p, (eval_S E p defp, eval_S D p defp, eval_S X p defp))::accu.cont_node  }
242
	  | Junction (j, defj) -> { accu with cont_junc = (j, (eval_T defj))::accu.cont_junc  }
243
	) {cont_node = []; cont_junc = []} Prog.defs
244
      in Obj.magic (fun tag -> theta_ify kenv tag)
245
  end
246
  module Rec (Prog : ProgType) =
247
  struct
248
    module rec Theta : ThetaType = ThetaFix (Prog) (Theta)
249
  end
250

  
251
  module Eval (Prog : ProgType) : EvaluationType =
252
  struct
253
    module RecTheta = Rec (Prog)
254
    module Theta = RecTheta.Theta
255

  
256
    let eval_prog =
257
	Transformer.(eval_cond (active [Prog.init]) (Theta.theta D [Prog.init]) (Theta.theta E [Prog.init] []))
258
  end
259

  
260
  module Eval (Prog : ProgType) =
261
  struct
262
    module ThetaFunctor (Evaluation : EvaluationType) : ThetaType =
263
    struct
264
      let theta tag = (theta_ify Evaluation.kenv) tag
265
    end
266
    module EvaluationFunctor (Theta : ThetaType) : EvaluationType =
267
    struct
268
      include Denotation (Theta)
269

  
270
      let kenv =
271
	List.fold_left (
272
	  fun accu d -> match d with
273
	  | State (p, defp) -> { accu with cont_node = (p, (fun kenv -> eval_S E p defp, eval_S D p defp, eval_S X p defp))::accu.cont_node  }
274
	  | Junction (j, defj) -> { accu with cont_junc = (j, (eval_T defj))::accu.cont_junc  }
275
	) {cont_node = []; cont_junc = []} Prog.defs
276

  
277
      let eval_prog =
278
	Transformer.(eval_cond (active [Prog.init]) (Theta.theta D [Prog.init]) (Theta.theta E [Prog.init] []))
279
    end
280
    module rec Theta : ThetaType = ThetaFunctor (Evaluation)
281
    and Evaluation : EvaluationType = EvaluationFunctor (Theta)
282
end
283
  *)
284
end
tools/stateflow/src/semantics/CPS/cPS_transformer.ml
1
open Basetypes
2
open ActiveStates
3

  
4
type mode_t =
5
  | Outer
6
  | Inner
7
  | Enter
8

  
9

  
10
type 't success_t = path_t -> 't
11
type 't fail_t = { local: 't; global: 't }
12
type 't wrapper_t = path_t -> 't -> 't
13

  
14
type ('a, 'b, 't) tag_t =
15
  | E : (path_t, path_t -> frontier_t -> 't, 't) tag_t
16
  | D : (path_t, 't, 't) tag_t
17
  | X : (path_t, frontier_t -> 't, 't) tag_t
18
  | J : (junction_name_t, 't wrapper_t -> 't success_t -> 't fail_t -> 't, 't) tag_t
19

  
20

  
21
type ('a, 'b, 't) theta_t = ('a, 'b, 't) tag_t -> 'a -> 'b
22

  
23
module type ThetaType =
24
sig
25
  type t
26
  val theta : ('a, 'b, t) theta_t
27
end
28

  
29
let pp_mode fmt mode =
30
  match mode with
31
  | Outer -> Format.fprintf fmt "Outer"
32
  | Inner -> Format.fprintf fmt "Inner"
33
  | Enter -> Format.fprintf fmt "Enter"
34

  
35

  
36
let pp_tag : type a b t. Format.formatter -> (a, b, t) tag_t -> unit =
37
  fun fmt tag ->
38
    match tag with
39
    | E -> Format.fprintf fmt "e"
40
    | D -> Format.fprintf fmt "d"
41
    | X -> Format.fprintf fmt "x"
42
    | J -> Format.fprintf fmt "j"
43

  
44
(*
45
module Proj1Theta (T : sig type t1 val bot1 : t1 type t2 val bot2 : t2 end) (Theta : ThetaType with type t = T.t1 * T.t2) : ThetaType with type t = T.t1 =
46
struct
47
  type t = T.t1
48

  
49
  let f f1 = (f1, T.bot2)
50
  let s s1 p = (s1 p, T.bot2)
51
  let w w1 p (tr1, _) = (w1 p tr1, T.bot2)
52

  
53
  let theta : type a b. (a, b, t) theta_t =
54
    fun tag ->
55
    match tag with
56
    | E -> (fun p p' f     -> fst (Theta.theta E p p' f))
57
    | D -> (fun p          -> fst (Theta.theta D p))
58
    | X -> (fun p f        -> fst (Theta.theta X p f))
59
    | J -> (fun j w1 s1 f1 -> fst (Theta.theta J j (w w1) (s s1) (f f1)))
60
end
61

  
62
module Proj2Theta (T : sig type t1 val bot1 : t1 type t2 val bot2 : t2 end) (Theta : ThetaType with type t = T.t1 * T.t2) : ThetaType with type t = T.t2 =
63
struct
64
  type t = T.t2
65

  
66
  let f f2 = (T.bot1, f2)
67
  let s s2 p = (T.bot1, s2 p)
68
  let w w2 p (_, tr2) = (T.bot1, w2 p tr2)
69

  
70
  let theta : type a b. (a, b, t) theta_t =
71
    fun tag ->
72
    match tag with
73
    | E -> (fun p p' f     -> snd (Theta.theta E p p' f))
74
    | D -> (fun p          -> snd (Theta.theta D p))
75
    | X -> (fun p f        -> snd (Theta.theta X p f))
76
    | J -> (fun j w2 s2 f2 -> snd (Theta.theta J j (w w2) (s s2) (f f2)))
77
end
78
*)
79

  
80
module TransformerStub =
81
struct
82
  type act_t = Action.t
83
  type cond_t = Condition.t
84

  
85
  let nil = Action.nil
86
  let aquote = Action.aquote
87
  let open_path = Action.open_path
88
  let close_path = Action.close_path
89
  let call = Action.call
90
  let pp_act = Action.pp_act
91

  
92
  let cquote = Condition.cquote
93
  let tru = Condition.tru
94
  let event = Condition.event
95
  let active = Condition.active
96
  let ( && ) = Condition.( && )
97
  let neg = Condition.neg
98
  let pp_cond = Condition.pp_cond
99
end
100

  
101
module type TransformerType =
102
sig
103
  type act_t = Action.t
104
  type cond_t = Condition.t
105
  type t
106

  
107
  include ActionType with type t := act_t
108
  include ConditionType with type t := cond_t
109

  
110
  val null : t
111
  val bot : t
112
  val ( >> ) : t -> t -> t
113
  val eval_act : (module ThetaType with type t = t) -> act_t -> t
114
  val eval_cond : cond_t -> t -> t -> t
115
  val pp_transformer : Format.formatter -> t -> unit
116
  val pp_principal : Format.formatter -> t -> unit
117
  val pp_component : Format.formatter -> 'c call_t -> 'c -> t -> unit
118
end
119

  
120
module type ComparableTransformerType =
121
sig
122
  include TransformerType
123

  
124
  val ( == ) : t -> t -> bool
125
end
126
(*
127
module Pair (T1 : ComparableTransformerType) (T2 : TransformerType) : ComparableTransformerType with type t = T1.t * T2.t =
128
struct
129
  include TransformerStub
130

  
131
  type t = T1.t * T2.t
132

  
133
  module T =
134
  struct
135
    type t1 = T1.t
136
    type t2 = T2.t
137
    let bot1 = T1.bot
138
    let bot2 = T2.bot
139
  end
140

  
141
  let null = T1.null, T2.null
142

  
143
  let bot = T1.bot, T2.bot
144

  
145
  let ( >> ) (tr11, tr12) (tr21, tr22) =
146
    T1.(tr11 >> tr21), T2.(tr12 >> tr22)
147

  
148
  let eval_act theta action =
149
    let module Theta = (val theta : ThetaType with type t = T1.t * T2.t) in
150
    let theta1 = (module Proj1Theta (T) (Theta) : ThetaType with type t = T1.t) in
151
    let theta2 = (module Proj2Theta (T) (Theta) : ThetaType with type t = T2.t) in
152
    T1.eval_act theta1 action, T2.eval_act theta2 action
153

  
154
  let eval_cond cond (trt1, trt2) (tre1, tre2) =
155
    T1.eval_cond cond trt1 tre1, T2.eval_cond cond trt2 tre2
156

  
157
  let ( == ) (tr1, _) (tr2, _) = T1.(tr1 == tr2)
158

  
159
  let pp_transformer fmt (tr1, tr2) =
160
    Format.fprintf fmt "< %a , %a >" T1.pp_transformer tr1 T2.pp_transformer tr2
161

  
162
  let pp_principal fmt (tr1, tr2) =
163
    Format.fprintf fmt "< %a , %a >" T1.pp_principal tr1 T2.pp_principal tr2
164

  
165
  let pp_component : type c. Format.formatter -> c call_t -> c -> t -> unit =
166
    fun fmt call ->
167
    match call with
168
    | Ecall -> (fun c (tr1, tr2) ->
169
      Format.fprintf fmt "< %t , %t >"
170
	(fun fmt -> T1.pp_component fmt Ecall c tr1)
171
	(fun fmt -> T2.pp_component fmt Ecall c tr2))
172
    | Dcall -> (fun c (tr1, tr2) ->
173
      Format.fprintf fmt "< %t , %t >"
174
	(fun fmt -> T1.pp_component fmt Dcall c tr1)
175
	(fun fmt -> T2.pp_component fmt Dcall c tr2))
176
    | Xcall -> (fun c (tr1, tr2) ->
177
      Format.fprintf fmt "< %t , %t >"
178
	(fun fmt -> T1.pp_component fmt Xcall c tr1)
179
	(fun fmt -> T2.pp_component fmt Xcall c tr2))
180
end
181
*)
182
  
183
module Evaluator : TransformerType with type t = (event_t * bool ActiveStates.Env.t * base_action_t list -> event_t * bool ActiveStates.Env.t * base_action_t list ) =
184
struct
185
  include TransformerStub
186

  
187
  type env_t = event_t * bool ActiveStates.Env.t * base_action_t list (* Don't care for values yet *)
188
  type t = env_t -> env_t
189
 
190
  let null rho = rho
191
  let add_action a (evt, rho, al) = (evt, rho, al@[a]) (* not very efficient but
192
							  avoid to keep track of
193
							  action order *)
194
  let bot _ = assert false
195
 
196
  let ( >> ) tr1 tr2 = fun rho -> rho |> tr1 |> tr2
197

  
198
  let ( ?? ) b tr = if b then tr else null
199

  
200
  let eval_open p (evt, rho, al)  = (evt, ActiveStates.Env.add p true rho, al)
201
  let eval_close p (evt, rho, al) = (evt, ActiveStates.Env.add p false rho, al)
202
  let eval_call : type c. (module ThetaType with type t = t) -> c call_t -> c -> t =
203
    fun kenv ->
204
    let module Theta = (val kenv : ThetaType with type t = t) in	      
205
    fun call -> match call with
206
    | Ecall -> (fun (p, p', f) -> Theta.theta E p p' f)
207
    | Dcall -> (fun p          -> Theta.theta D p)
208
    | Xcall -> (fun (p, f)     -> Theta.theta X p f)
209

  
210
  let eval_act kenv action =
211
    (* Format.printf "----- action = %a@." Action.pp_act action; *)
212
    match action with
213
    | Action.Call (c, a)      -> eval_call kenv c a
214
    | Action.Quote a          -> add_action a
215
    | Action.Open p           -> eval_open p
216
    | Action.Close p          -> eval_close p
217
    | Action.Nil              -> null
218

  
219
  (*if (match trans.event with None -> true | _ -> e = trans.event) && trans.condition rho*)
220
  let rec eval_cond condition ok ko =
221
    (* Format.printf "----- cond = %a@." Condition.pp_cond condition; *)
222
    match condition with
223
    | Condition.True               -> ok
224
    | Condition.Active p           -> (fun ((evt, env, al) as rho) -> if ActiveStates.Env.find p env then ok rho else ko rho)
225
    | 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)
226
    | Condition.Neg cond           -> eval_cond cond ko ok
227
    | Condition.And (cond1, cond2) -> eval_cond cond1 (eval_cond cond2 ok ko) ko
228
    | Condition.Quote c            -> add_action c >> ok (* invalid behavior but similar to the other: should evaluate condition *)
229

  
230
  let pp_transformer fmt tr =
231
    Format.fprintf fmt "<transformer>"
232

  
233
  let pp_principal fmt tr =
234
    Format.fprintf fmt "principal =@.%a" pp_transformer tr
235

  
236
  let pp_component : type c. Format.formatter -> c call_t -> c -> t -> unit =
237
    fun fmt call -> match call with
238
    | Ecall -> (fun (p, p', f) tr ->
239
      Format.fprintf fmt "component %a(%a, %a, %a) =@.%a" pp_call call pp_path p pp_path p' pp_frontier f pp_transformer tr)
240
    | Dcall -> (fun p tr ->
241
      Format.fprintf fmt "component %a(%a) =@.%a" pp_call call pp_path p pp_transformer tr)
242
    | Xcall -> (fun (p, f) tr ->
243
      Format.fprintf fmt "component %a(%a, %a) =@.%a" pp_call call pp_path p pp_frontier f pp_transformer tr)
244
end
245

  
246
module CodeGenerator : ComparableTransformerType =
247
struct
248
  include TransformerStub
249

  
250
  type t =
251
  | Bot
252
  | Act of act_t
253
  | Seq of t list
254
  | Ite of cond_t * t * t
255

  
256
  let null = Seq []
257

  
258
  let bot = Bot
259
 
260
  let ( >> ) tr1 tr2 =
261
    match tr1, tr2 with
262
    | Seq trl1, Seq trl2 -> Seq (trl1@trl2)
263
    | Seq trl1, _        -> Seq (trl1@[tr2])
264
    | _       , Seq trl2 -> Seq (tr1::trl2)
265
    | _                  -> Seq ([tr1;tr2])
266

  
267
  let rec ( == ) tr1 tr2 = tr1 = tr2
268

  
269
  let eval_act kenv (action : act_t) =
270
    (*Format.printf "----- action = %a@." Action.pp_act action;*)
271
    Act action
272

  
273
  (*if (match trans.event with None -> true | _ -> e = trans.event) && trans.condition rho*)
274
  let rec eval_cond condition ok ko =
275
    (*Format.printf "----- cond = %a@." Condition.pp_cond condition;*)
276
    Ite (condition, ok, ko)
277
    
278
  let rec pp_transformer fmt tr =
279
    match tr with
280
    | Bot           -> Format.fprintf fmt "bot"
281
    | Act a         ->
282
       Format.fprintf fmt "<%a>" pp_act a
283
    | Seq trl       ->
284
       Format.fprintf fmt "@[<v 0>%a@]"
285
	 (Utils.fprintf_list ~sep:";@ " pp_transformer)
286
	 trl
287
    | Ite (c, t, e) ->
288
       Format.fprintf fmt "@[<v 0>if %a@ @[<v 2>then@ %a@]@ @[<v 2>else@ %a@]@ endif@]" pp_cond c pp_transformer t pp_transformer e
289

  
290
  let pp_principal fmt tr =
291
    Format.fprintf fmt "principal =@.%a" pp_transformer tr
292
      
293
  let pp_component : type c. Format.formatter -> c call_t -> c -> t -> unit =
294
    fun fmt call -> match call with
295
    | Ecall -> (fun (p, p', f) tr ->
296
      Format.fprintf fmt "component %a(%a, %a, %a) =@.@[<v 2>begin@ %a@]@.end" pp_call call pp_path p pp_path p' pp_frontier f pp_transformer tr)
297
    | Dcall -> (fun p tr ->
298
      Format.fprintf fmt "component %a(%a) =@.@[<v 2>begin@ %a@]@.end" pp_call call pp_path p pp_transformer tr)
299
    | Xcall -> (fun (p, f) tr ->
300
      Format.fprintf fmt "component %a(%a, %a) =@.@[<v 2>begin@ %a@]@.end" pp_call call pp_path p pp_frontier f pp_transformer tr)
301
end
302

  
303
module LustrePrinter (Vars : sig val vars : ActiveStates.Vars.t end) : TransformerType =
304
struct
305
  include TransformerStub
306

  
307
  type name_t = string
308
  type t = name_t -> name_t -> (ActiveStates.Vars.t * (Format.formatter -> unit))
309

  
310
  let new_loc, reset_loc =
... This diff was truncated because it exceeds the maximum size that can be displayed.

Also available in: Unified diff