Project

General

Profile

Revision 93119c3f

View differences:

Makefile.in
21 21
	@echo Compiling binary lustret
22 22
	@make -C src lustret
23 23

  
24
lustresf:
25
	@echo Compiling binary lustresf
26
	@make -C src lustresf
27

  
24 28
configure: configure.ac
25 29
	@echo configure.ac has changed relaunching autoconf
26 30
	@autoconf
src/Makefile.in
24 24
	@mkdir -p $(LOCAL_BINDIR)
25 25
	@mv _build/main_lustre_testgen.native $(LOCAL_BINDIR)/lustret
26 26

  
27
lustresf:
28
	@echo Compiling binary lustret
29
	@$(OCAMLBUILD) tools/stateflow/sf_sem.native
30
	@mkdir -p $(LOCAL_BINDIR)
31
	@mv _build/tools/stateflow/sf_sem.native $(LOCAL_BINDIR)/lustresf
32

  
27 33
doc:
28 34
	@echo Generating doc
29 35
	@$(OCAMLBUILD) lustrec.docdir/index.html
src/_tags.in
5 5
"plugins/salsa": include
6 6
"plugins/scopes": include
7 7
"plugins/mpfr": include
8
"tools/stateflow": include
9
"tools/stateflow/common": include
10
"tools/stateflow/semantics": include
11
"tools/stateflow/models": include
12

  
8 13
<**/.svn>: -traverse
9 14
<**/.svn>: not_hygienic
10 15

  
src/tools/stateflow/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
src/tools/stateflow/README.md
1
# stateflow_CPS_semantics
2
A continuation passing style semantics for Stateflow in Ocaml
3

  
4
Software implements:
5
- our generic CPS semantics, instanciated as
6
  - an evaluator (aka simulator)
7
  - an imperative code generator
8
  - a lustre automaton generator compatible with lustrec (github/coco-team/lustrec)
9
- the reference denotational semantics of Stateflow by Hamon as presented in his EMSOFT'05 paper.
10

  
11
Options:
12
sf_sem takes as input a model name and a backend. Traces are hard coded in the source files.
13

  
14
Backends are interpretor, imperative code generator, lustre code generator.
15
  -model model in {simple, stopwatch} (default: simple)
16
  -eval execute the model on trace <int>
17
  -eval-mode select evaluator: cps, emsoft05 or compare
18
  -gen_imp generate imperative code
19
  -gen_lustre generate lustre model
20
  -modular generate modular code (either for imperative or lustre backend) 0 is not modular, 1 modularize nodes, 2 modularize entry, during and exit actions (default 0)
21

  
22
Example:
23
./sf_sem -model stopwatch -eval-mode compare -eval 1
24

  
src/tools/stateflow/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

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

  
2
let sf_level = 2
3
  
4
(* Basic datatype for model elements: state and junction name, events ... *)
5
type state_name_t    = string
6
type junction_name_t = string
7
type path_t = state_name_t list
8
type event_base_t = string
9
type event_t      = event_base_t option
10

  
11
(* Connected to lustrec types *)
12
type base_action_t = { defs : LustreSpec.eq list; ident : string }
13
type base_condition_t = LustreSpec.expr
14
  
15
(* P(r)etty printers *)
16
let pp_state_name = Format.pp_print_string
17
let pp_junction_name = Format.pp_print_string
18
let pp_path fmt p = Utils.fprintf_list ~sep:"." pp_state_name fmt p
19
let pp_event fmt e = match e with None -> Format.fprintf fmt "none" | Some s -> Format.fprintf fmt "%s" s
20
let pp_base_act fmt a = Utils.fprintf_list ~sep:",@ " Printers.pp_node_eq fmt a.defs
21
let pp_base_cond = Printers.pp_expr
22
  
23
(* Action and Condition types and functions. *)
24

  
25
(* Actions are defined by string + the opening and closing of states *)
26

  
27
(* This version is slightly more complex than the one of EMSOFT'05 to enable the
28
   use of function calls in action.
29

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

  
32
type frontier_t =
33
  | Loose
34
  | Strict
35

  
36
let pp_frontier fmt frontier =
37
  match frontier with
38
  | Loose  -> Format.fprintf fmt "Loose"
39
  | Strict -> Format.fprintf fmt "Strict"
40

  
41
type _ call_t =
42
  | Ecall : (path_t * path_t * frontier_t) call_t
43
  | Dcall : path_t call_t
44
  | Xcall : (path_t * frontier_t) call_t
45

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

  
66

  
67
module Action =
68
struct
69
  type t =
70
    | Quote : base_action_t -> t
71
    | Close : path_t -> t
72
    | Open  : path_t -> t
73
    | Call  : 'c call_t * 'c -> t
74
    | Nil   : t
75

  
76
    
77
  let nil = Nil
78
  let aquote act = Quote act
79
  let open_path p = Open p
80
  let close_path p = Close p
81
  let call c a = Call (c, a)
82

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

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

  
99
let _ = (module Action : ActionType) 
100

  
101

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

  
114
  val pp_cond : Format.formatter -> t -> unit
115
end
116

  
117
  module Condition =
118
struct
119
  type t =
120
    | Quote of base_condition_t
121
    | Active of path_t
122
    | Event of event_base_t
123
    | And of t * t
124
    | Neg of t
125
    | True
126

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

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

  
146
end
147

  
148
let _ = (module Condition : ConditionType)
src/tools/stateflow/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 * LustreSpec.var_decl 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
69
      (fun res c ->
70
	match c with
71
	| State (p, _) -> ActiveStates.Vars.add p res
72
	| Junction _ -> res
73
      )
74
      ActiveStates.Vars.empty defs
75

  
76
  let init_env model = ActiveStates.Env.from_set (states model) false
77

  
78
  let global_vars (_, _, env) = env
79
    
80
  (* Printers *)
81
      
82
  let pp_event fmt e =
83
    match e with
84
    | Some e -> Format.fprintf fmt "%s" e
85
    | None -> Format.fprintf fmt "noevent"
86
    
87
  let pp_dest fmt d = match d with
88
    | DPath p -> Format.fprintf fmt "Path %a" pp_path p
89
    | DJunction j -> Format.fprintf fmt "Junction %a" pp_junction_name j
90

  
91
  let pp_trans fmt t =
92
    Format.fprintf fmt
93
      "@[<hov 0>(@[<hov 0>%a,@ %a,@ %a,@ %a,@ %a@]@ )@]"
94
      pp_event t.event
95
      Condition.pp_cond t.condition
96
      Action.pp_act t.condition_act
97
      Action.pp_act t.transition_act    
98
      pp_dest t.dest
99
      
100
  let pp_transitions fmt l =
101
    Format.fprintf fmt
102
      "@[<hov 0>[@[<hov 0>%a@]@ ]@]"
103
      (Utils.fprintf_list ~sep:";@ " pp_trans) l
104

  
105
  let pp_comp fmt c = match c with
106
    | Or (_T, _S) ->
107
       Format.fprintf fmt "Or(%a, {%a})"
108
	 pp_transitions _T
109
	 (Utils.fprintf_list ~sep:"; " pp_state_name) _S
110
    | And (_S) ->
111
       Format.fprintf fmt "And({%a})"
112
	 (Utils.fprintf_list ~sep:"; " pp_state_name) _S
113

  
114
  let pp_state_actions fmt sa =
115
    Format.fprintf fmt "@[<hov 0>(%a,@ %a,@ %a)@]"
116
      Action.pp_act sa.entry_act
117
      Action.pp_act sa.during_act
118
      Action.pp_act sa.exit_act
119
      
120
  let pp_state fmt s =
121
    Format.fprintf fmt "@[<v 0>(@[<v 0>%a,@ %a,@ %a,@ %a@]@ @])"
122
      pp_state_actions s.state_actions
123
      pp_transitions s.outer_trans
124
      pp_transitions s.inner_trans
125
      pp_comp s.internal_composition
126
      
127
  let pp_src fmt src =
128
    Format.fprintf fmt "@[<v>%a@ @]"
129
      (Utils.fprintf_list ~sep:"@ @ " (fun fmt src -> match src with
130
	State (p, def) ->
131
	  Format.fprintf fmt "%a: %a"
132
	    pp_path p
133
	    pp_state def
134
      | Junction (s, tl) ->
135
	 Format.fprintf fmt "%a: %a"
136
	   pp_state_name s
137
	   pp_transitions tl
138
       ))
139
      src
140
end
141
   
src/tools/stateflow/models/model_medium.ml
1
open Datatype
2
open SF
3

  
4
let name = "medium"
5

  
6
let condition x = condition (Corelang.mkexpr Location.dummy_loc (LustreSpec.Expr_const (Corelang.const_of_bool true)))
7
 
8
let model : prog_t =
9
    let state_main = "main" in
10
    let state_a = "a" in
11
    let state_a1 = "a1" in
12
    let state_b = "b" in
13

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

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

  
52

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

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

  
4
let name = "simple"
5

  
6
  let condition x = condition (Corelang.mkexpr Location.dummy_loc (LustreSpec.Expr_const (Corelang.const_of_bool true)))
7

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

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

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

  
45

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

  
82
let traces : trace_t list = [[None; None]]
src/tools/stateflow/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
let condition x = condition (Corelang.mkexpr Location.dummy_loc (LustreSpec.Expr_const (Corelang.const_of_bool true)))
8
    
9
let name = "stopwatch"
10
  
11
let model = 
12
  let smain    = "main" in
13
  let sstop    = "stop" in
14
  let sreset   = "reset" in
15
  let slapstop = "lap_stop" in
16
  let srun     = "run" in
17
  let srunning = "running" in
18
  let slap     = "lap" in
19

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

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

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

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

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

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

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

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

  
229
  let src = [
230
    State([smain;srun;srunning], def_running);
231
    State([smain;srun;slap], def_lap);
232
    State([smain;srun], def_run);
233
    State([smain;sstop;sreset], def_reset);
234
    State([smain;sstop;slapstop], def_lapstop);
235
    State([smain;sstop], def_stop);
236
    State([smain], def_main);
237
    Junction("jreset", []);
238
    Junction("j1", [tj1j2;tj1j3]);
239
    Junction("j2", [tj2j3droite; tj2j3gauche]);
240
    Junction("j3", []);
241
  ]
242
  in
243
  let globals =
244
    let int_typ = Corelang.mktyp Location.dummy_loc LustreSpec.Tydec_int in
245
    List.map (fun k ->
246
      Corelang.mkvar_decl
247
	Location.dummy_loc
248
	(k, (* name *)
249
	 int_typ, (* type *)
250
	 Corelang.dummy_clock_dec, (* clock *)
251
	 false, (* not a constant *)
252
	 None (* no default value *)
253
	)
254
    )
255
      ["cent";
256
       "sec";
257
       "min";
258
       "cont"
259
      ]
260
  in
261
  (smain, src, globals)
262

  
263
let traces : trace_t list =
264
  [
265
    [None; Some "TIC"; Some "START"; Some "TIC"; Some "TIC"];
266
    [None; Some "START"; Some "START"; Some "START"];
267
    [None; Some "START"; Some "TIC"; Some "START"; Some "TIC"]
268
  ]
src/tools/stateflow/semantics/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, defs, state_vars = 
12
    let (init, defs, globals) = M.model in
13
    let state_vars = SF.states M.model in
14
    init, defs, state_vars
15
    
16
(*let _ = Format.printf "Model definitions@.%a@.####" Simulink.pp_src defs; () *)
17
end
18

  
19

  
20
module Interp = CPS_interpreter.Interpreter (T)
21
module KenvTheta = KenvTheta (T)
22
module Tables = KenvTheta.MemoThetaTables ()
23

  
24
let eval ((modular_entry:bool), (modular_during:bool), (modular_exit:bool)) =
25
  let module Modularity : KenvTheta.ModularType =
26
      struct
27
	let modular : type b. (path_t, b, bool) tag_t -> path_t -> b =
28
			fun tag ->
29
			  match tag with
30
			  | E -> (fun p p' f -> modular_entry)
31
			  | D -> (fun p      -> modular_during)
32
			  | X -> (fun p f    -> modular_exit)
33
      end
34
  in
35
  let module Thetaify = KenvTheta.ModularThetaify (Tables) (Modularity) in
36
  let module EvalProg = Interp.Evaluation (Thetaify) (Prog) in
37
  (module EvalProg: Interp.EvaluationType)
38
  
39
let compute modular  =
40
  let module Eval = (val (eval modular)) in
41
  Eval.eval_prog 
42
    
43
let code_gen fmt modular  =
44
  let module Eval = (val (eval modular)) in
45
  let principal, components =  Eval.eval_prog, Eval.eval_components in
46
  [
47
    List.map (fun (c, tr) -> T.mkcomponent Ecall c tr) (components Ecall);
48
    List.map (fun (c, tr) -> T.mkcomponent Dcall c tr) (components Dcall);
49
    List.map (fun (c, tr) -> T.mkcomponent Xcall c tr) (components Xcall);
50
    T.mkprincipal principal;
51
  ]
52
end
src/tools/stateflow/semantics/cPS_ccode_generator.ml
1
open Basetypes
2
open ActiveStates
3
open CPS_transformer
4

  
5
module CodeGenerator : ComparableTransformerType =
6
struct
7
  include TransformerStub
8

  
9
  type t =
10
  | Bot
11
  | Act of act_t
12
  | Seq of t list
13
  | Ite of cond_t * t * t
14

  
15
  let null = Seq []
16

  
17
  let bot = Bot
18
 
19
  let ( >> ) tr1 tr2 =
20
    match tr1, tr2 with
21
    | Seq trl1, Seq trl2 -> Seq (trl1@trl2)
22
    | Seq trl1, _        -> Seq (trl1@[tr2])
23
    | _       , Seq trl2 -> Seq (tr1::trl2)
24
    | _                  -> Seq ([tr1;tr2])
25

  
26
  let rec ( == ) tr1 tr2 = tr1 = tr2
27

  
28
  let eval_act kenv (action : act_t) =
29
    (*Format.printf "----- action = %a@." Action.pp_act action;*)
30
    Act action
31

  
32
  (*if (match trans.event with None -> true | _ -> e = trans.event) && trans.condition rho*)
33
  let rec eval_cond condition ok ko =
34
    (*Format.printf "----- cond = %a@." Condition.pp_cond condition;*)
35
    Ite (condition, ok, ko)
36
    
37
  let rec pp_transformer fmt tr =
38
    match tr with
39
    | Bot           -> Format.fprintf fmt "bot"
40
    | Act a         ->
41
       Format.fprintf fmt "<%a>" pp_act a
42
    | Seq trl       ->
43
       Format.fprintf fmt "@[<v 0>%a@]"
44
	 (Utils.fprintf_list ~sep:";@ " pp_transformer)
45
	 trl
46
    | Ite (c, t, e) ->
47
       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
48

  
49
  let pp_principal fmt tr =
50
    Format.fprintf fmt "principal =@.%a" pp_transformer tr
51
      
52
  let pp_component : type c. Format.formatter -> c call_t -> c -> t -> unit =
53
    fun fmt call -> match call with
54
    | Ecall -> (fun (p, p', f) tr ->
55
      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)
56
    | Dcall -> (fun p tr ->
57
      Format.fprintf fmt "component %a(%a) =@.@[<v 2>begin@ %a@]@.end" pp_call call pp_path p pp_transformer tr)
58
    | Xcall -> (fun (p, f) tr ->
59
      Format.fprintf fmt "component %a(%a, %a) =@.@[<v 2>begin@ %a@]@.end" pp_call call pp_path p pp_frontier f pp_transformer tr)
60
end
61

  
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_ _ = 
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 ^ "]")
31

  
32

  
33

  
34
let run_trace model func t =
35
  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
  
38
  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
54
  in
55
  Format.printf "#### %i@.%a@." cpt ActiveStates.Env.pp_env final_env;
56
  ()
57

  
58

  
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
62
  include TransformerStub
63
  type env_t = event_t * bool ActiveStates.Env.t * truc list (* Don't care for values yet *)
64
  type t = env_t -> env_t
65
 
66
  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 *)
73

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

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

  
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

  
90
  let eval_act kenv action =
91
    (* Format.printf "----- action = %a@." Action.pp_act action; *)
92
    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
98

  
99
  (*if (match trans.event with None -> true | _ -> e = trans.event) && trans.condition rho*)
100
  let rec eval_cond condition ok ko : t =
101
    (* Format.printf "----- cond = %a@." Condition.pp_cond condition; *)
102
    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 *)
109

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

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

  
116
  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)
124
end
125

  
src/tools/stateflow/semantics/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.report ~level:sf_level (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.report ~level:sf_level (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.report ~level:sf_level (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.report ~level:sf_level (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.report ~level:sf_level (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.report ~level:sf_level (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.report ~level:sf_level (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.report ~level:sf_level (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
src/tools/stateflow/semantics/cPS_lustre_generator.ml
1
open Basetypes
2
open ActiveStates
3
open CPS_transformer
4

  
5
let ff = Format.fprintf 
6
       
7
module LustrePrinter (
8
  Vars : sig
9
    val state_vars : ActiveStates.Vars.t
10
    val global_vars : LustreSpec.var_decl list
11
  end) : TransformerType =
12
struct
13
  include TransformerStub
14

  
15
  type name_t = string
16
  type t_base = { statements : LustreSpec.statement list; assert_false: bool }
17
  type t = name_t -> name_t -> (ActiveStates.Vars.t * t_base)
18

  
19
  let new_loc, reset_loc =
20
    let cpt = ref 0 in
21
    ((fun () -> incr cpt; Format.sprintf "loc_%i" !cpt),
22
     (fun () -> cpt := 0))
23

  
24
  let new_aut, reset_aut =
25
    let cpt = ref 0 in
26
    ((fun () -> incr cpt; Format.sprintf "aut_%i" !cpt),
27
     (fun () -> cpt := 0))
28
      
29
  let pp_path prefix fmt path =
30
    Format.fprintf fmt "%s%t"
31
      prefix
32
      (fun fmt -> Utils.fprintf_list ~sep:"_" Format.pp_print_string fmt path)
33

  
34
  let pp_typed_path sin fmt path =
35
    Format.fprintf fmt "%a : bool" (pp_path sin) path
36

  
37
  let pp_vars sin fmt vars =
38
    Format.fprintf fmt "%t" (fun fmt -> Utils.fprintf_list ~sep:", " (pp_path sin) fmt (ActiveStates.Vars.elements vars))
39
  let pp_vars_decl sin fmt vars =
... This diff was truncated because it exceeds the maximum size that can be displayed.

Also available in: Unified diff