Project

General

Profile

Download (4.69 KB) Statistics
| Branch: | Tag: | Revision:
1 2de7fa82 ploc
open Basetypes
2
(* open ActiveEnv *)
3
4
(* Type definitions of a model *)
5
6 ca7ff3f7 Lélio Brun
type destination_t = DPath of path_t | DJunction of junction_name_t
7 2de7fa82 ploc
8
type trans_t = {
9 ca7ff3f7 Lélio Brun
  event : event_t;
10
  condition : Condition.t;
11
  condition_act : Action.t;
12
  transition_act : Action.t;
13
  dest : destination_t;
14 2de7fa82 ploc
}
15
16
type transitions_t = trans_t list
17
18
type composition_t =
19
  | Or of transitions_t * state_name_t list
20
  | And of state_name_t list
21
22
type state_actions_t = {
23 ca7ff3f7 Lélio Brun
  entry_act : Action.t;
24
  during_act : Action.t;
25
  exit_act : Action.t;
26 2de7fa82 ploc
}
27
28
type state_def_t = {
29
  state_actions : state_actions_t;
30
  outer_trans : transitions_t;
31
  inner_trans : transitions_t;
32
  internal_composition : composition_t;
33
}
34
35 eb70bae5 Christophe Garion
type 'prog_t src_components_t =
36 2de7fa82 ploc
  | State of path_t * state_def_t
37
  | Junction of junction_name_t * transitions_t
38 eb70bae5 Christophe Garion
  | SFFunction of 'prog_t
39
40 ca7ff3f7 Lélio Brun
type prog_t =
41
  | Program of
42
      state_name_t
43
      * prog_t src_components_t list
44
      * (Lustre_types.var_decl * Lustre_types.expr) list
45 eb70bae5 Christophe Garion
46
type scope_t = Constant | Input | Local | Output | Parameter
47
48
type datatype_var_init_t = Bool of bool | Real of float | Int of int
49
50
type user_variable_t = user_variable_name_t * scope_t * datatype_var_init_t
51 2de7fa82 ploc
52
type trace_t = event_t list
53 eb70bae5 Christophe Garion
54 2de7fa82 ploc
module type MODEL_T = sig
55
  val name : string
56 ca7ff3f7 Lélio Brun
57 2de7fa82 ploc
  val model : prog_t
58 ca7ff3f7 Lélio Brun
59
  val traces : trace_t list
60 2de7fa82 ploc
end
61 eb70bae5 Christophe Garion
62 2de7fa82 ploc
(* Module (S)tate(F)low provides basic constructors for action, condition,
63
   events, as well as printer functions *)
64 ca7ff3f7 Lélio Brun
module SF = struct
65 2de7fa82 ploc
  (* Basic constructors *)
66 eb70bae5 Christophe Garion
67 ca7ff3f7 Lélio Brun
  let no_action = Action.nil
68
69 2de7fa82 ploc
  let no_condition = Condition.tru
70 ca7ff3f7 Lélio Brun
71
  let no_event = None
72
73
  let event s = Some s
74
75
  let action s = Action.aquote s
76
77
  let condition s = Condition.cquote s
78
79
  let no_state_action =
80
    { entry_act = no_action; during_act = no_action; exit_act = no_action }
81
82
  let state_action a b c = { entry_act = a; during_act = b; exit_act = c }
83 2de7fa82 ploc
84 eb70bae5 Christophe Garion
  let states (Program (_, defs, _)) =
85 93119c3f ploc
    List.fold_left
86
      (fun res c ->
87 ca7ff3f7 Lélio Brun
        match c with
88
        | State (p, _) ->
89
          ActiveStates.Vars.add p res
90
        | Junction _ ->
91
          res
92
        | SFFunction _ ->
93
          res)
94 93119c3f ploc
      ActiveStates.Vars.empty defs
95 2de7fa82 ploc
96
  let init_env model = ActiveStates.Env.from_set (states model) false
97 93119c3f ploc
98 b06b7b77 Christophe Garion
  let global_vars (Program (_, _, env)) = env
99 eb70bae5 Christophe Garion
100 2de7fa82 ploc
  (* Printers *)
101 eb70bae5 Christophe Garion
102 2de7fa82 ploc
  let pp_event fmt e =
103
    match e with
104 ca7ff3f7 Lélio Brun
    | Some e ->
105
      Format.fprintf fmt "%s" e
106
    | None ->
107
      Format.fprintf fmt "noevent"
108
109
  let pp_dest fmt d =
110
    match d with
111
    | DPath p ->
112
      Format.fprintf fmt "Path %a" pp_path p
113
    | DJunction j ->
114
      Format.fprintf fmt "Junction %a" pp_junction_name j
115 2de7fa82 ploc
116
  let pp_trans fmt t =
117 ca7ff3f7 Lélio Brun
    Format.fprintf fmt "@[<hov 0>(@[<hov 0>%a,@ %a,@ %a,@ %a,@ %a@]@ )@]"
118
      pp_event t.event Condition.pp_cond t.condition Action.pp_act
119
      t.condition_act Action.pp_act t.transition_act pp_dest t.dest
120 eb70bae5 Christophe Garion
121 2de7fa82 ploc
  let pp_transitions fmt l =
122 ca7ff3f7 Lélio Brun
    Format.fprintf fmt "@[<hov 0>[@[<hov 0>%a@]@ ]@]"
123
      (Utils.fprintf_list ~sep:";@ " pp_trans)
124
      l
125 2de7fa82 ploc
126 ca7ff3f7 Lélio Brun
  let pp_comp fmt c =
127
    match c with
128 2de7fa82 ploc
    | Or (_T, _S) ->
129 ca7ff3f7 Lélio Brun
      Format.fprintf fmt "Or(%a, {%a})" pp_transitions _T
130
        (Utils.fprintf_list ~sep:"; " pp_state_name)
131
        _S
132
    | And _S ->
133
      Format.fprintf fmt "And({%a})"
134
        (Utils.fprintf_list ~sep:"; " pp_state_name)
135
        _S
136 2de7fa82 ploc
137
  let pp_state_actions fmt sa =
138 ca7ff3f7 Lélio Brun
    Format.fprintf fmt "@[<hov 0>(%a,@ %a,@ %a)@]" Action.pp_act sa.entry_act
139
      Action.pp_act sa.during_act Action.pp_act sa.exit_act
140 eb70bae5 Christophe Garion
141 2de7fa82 ploc
  let pp_state fmt s =
142
    Format.fprintf fmt "@[<v 0>(@[<v 0>%a,@ %a,@ %a,@ %a@]@ @])"
143 ca7ff3f7 Lélio Brun
      pp_state_actions s.state_actions pp_transitions s.outer_trans
144
      pp_transitions s.inner_trans pp_comp s.internal_composition
145 eb70bae5 Christophe Garion
146
  let pp_src pp_sffunction fmt src =
147 2de7fa82 ploc
    Format.fprintf fmt "@[<v>%a@ @]"
148 ca7ff3f7 Lélio Brun
      (Utils.fprintf_list ~sep:"@ @ " (fun fmt src ->
149
           match src with
150
           | State (p, def) ->
151
             Format.fprintf fmt "%a: %a" pp_path p pp_state def
152
           | Junction (s, tl) ->
153
             Format.fprintf fmt "%a: %a" pp_state_name s pp_transitions tl
154
           | SFFunction p ->
155
             pp_sffunction fmt p))
156 2de7fa82 ploc
      src
157 eb70bae5 Christophe Garion
158
  let rec pp_sffunction fmt (Program (name, component_list, _)) =
159 ca7ff3f7 Lélio Brun
    Format.fprintf fmt "SFFunction name: %s@ %a@ " name (pp_src pp_sffunction)
160
      component_list
161 eb70bae5 Christophe Garion
162 57ecad58 Christophe Garion
  let pp_vars fmt src =
163
    Format.fprintf fmt "@[<v>%a@ @]"
164
      (Utils.fprintf_list ~sep:"@ " Printers.pp_var)
165 ca7ff3f7 Lélio Brun
      src
166 57ecad58 Christophe Garion
167
  let pp_prog fmt (Program (name, component_list, vars)) =
168 ca7ff3f7 Lélio Brun
    Format.fprintf fmt "Main node name: %s@ %a@ %a@" name (pp_src pp_sffunction)
169
      component_list pp_vars (List.map fst vars)
170 eb70bae5 Christophe Garion
171
  let pp_scope fmt src =
172 ca7ff3f7 Lélio Brun
    Format.fprintf fmt
173
      (match src with
174
      | Constant ->
175
        "Constant"
176
      | Input ->
177
        "Input"
178
      | Local ->
179
        "Local"
180
      | Output ->
181
        "Output"
182
      | Parameter ->
183
        "Parameter")
184 2de7fa82 ploc
end