Project

General

Profile

Download (4.69 KB) Statistics
| Branch: | Tag: | Revision:
1
open Basetypes
2
(* open ActiveEnv *)
3

    
4
(* Type definitions of a model *)
5

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

    
8
type trans_t = {
9
  event : event_t;
10
  condition : Condition.t;
11
  condition_act : Action.t;
12
  transition_act : Action.t;
13
  dest : destination_t;
14
}
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
  entry_act : Action.t;
24
  during_act : Action.t;
25
  exit_act : Action.t;
26
}
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
type 'prog_t src_components_t =
36
  | State of path_t * state_def_t
37
  | Junction of junction_name_t * transitions_t
38
  | SFFunction of 'prog_t
39

    
40
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

    
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

    
52
type trace_t = event_t list
53

    
54
module type MODEL_T = sig
55
  val name : string
56

    
57
  val model : prog_t
58

    
59
  val traces : trace_t list
60
end
61

    
62
(* Module (S)tate(F)low provides basic constructors for action, condition,
63
   events, as well as printer functions *)
64
module SF = struct
65
  (* Basic constructors *)
66

    
67
  let no_action = Action.nil
68

    
69
  let no_condition = Condition.tru
70

    
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

    
84
  let states (Program (_, defs, _)) =
85
    List.fold_left
86
      (fun res c ->
87
        match c with
88
        | State (p, _) ->
89
          ActiveStates.Vars.add p res
90
        | Junction _ ->
91
          res
92
        | SFFunction _ ->
93
          res)
94
      ActiveStates.Vars.empty defs
95

    
96
  let init_env model = ActiveStates.Env.from_set (states model) false
97

    
98
  let global_vars (Program (_, _, env)) = env
99

    
100
  (* Printers *)
101

    
102
  let pp_event fmt e =
103
    match e with
104
    | 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

    
116
  let pp_trans fmt t =
117
    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

    
121
  let pp_transitions fmt l =
122
    Format.fprintf fmt "@[<hov 0>[@[<hov 0>%a@]@ ]@]"
123
      (Utils.fprintf_list ~sep:";@ " pp_trans)
124
      l
125

    
126
  let pp_comp fmt c =
127
    match c with
128
    | Or (_T, _S) ->
129
      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

    
137
  let pp_state_actions fmt sa =
138
    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

    
141
  let pp_state fmt s =
142
    Format.fprintf fmt "@[<v 0>(@[<v 0>%a,@ %a,@ %a,@ %a@]@ @])"
143
      pp_state_actions s.state_actions pp_transitions s.outer_trans
144
      pp_transitions s.inner_trans pp_comp s.internal_composition
145

    
146
  let pp_src pp_sffunction fmt src =
147
    Format.fprintf fmt "@[<v>%a@ @]"
148
      (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
      src
157

    
158
  let rec pp_sffunction fmt (Program (name, component_list, _)) =
159
    Format.fprintf fmt "SFFunction name: %s@ %a@ " name (pp_src pp_sffunction)
160
      component_list
161

    
162
  let pp_vars fmt src =
163
    Format.fprintf fmt "@[<v>%a@ @]"
164
      (Utils.fprintf_list ~sep:"@ " Printers.pp_var)
165
      src
166

    
167
  let pp_prog fmt (Program (name, component_list, vars)) =
168
    Format.fprintf fmt "Main node name: %s@ %a@ %a@" name (pp_src pp_sffunction)
169
      component_list pp_vars (List.map fst vars)
170

    
171
  let pp_scope fmt src =
172
    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
end
(3-3/3)