Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / tools / stateflow / common / datatype.ml @ 3769b712

History | View | Annotate | Download (4.76 KB)

1
open Lustrec
2
open Basetypes
3
(* open ActiveEnv *)
4

    
5
(* Type definitions of a model *)
6

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

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

    
19
type transitions_t = trans_t list
20

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

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

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

    
38
type 'prog_t src_components_t =
39
  | State of path_t * state_def_t
40
  | Junction of junction_name_t * transitions_t
41
  | SFFunction of 'prog_t
42

    
43
type prog_t = Program of state_name_t * prog_t src_components_t list * (Lustrec.Lustre_types.var_decl * Lustrec.Lustre_types.expr) list
44

    
45
type scope_t = Constant | Input | Local | Output | Parameter
46

    
47
type datatype_var_init_t = Bool of bool | Real of float | Int of int
48

    
49
type user_variable_t = user_variable_name_t * scope_t * datatype_var_init_t
50

    
51
type trace_t = event_t list
52

    
53
module type MODEL_T = sig
54
  val name : string
55
  val model : prog_t
56
  val traces: trace_t list
57
end
58

    
59
(* Module (S)tate(F)low provides basic constructors for action, condition,
60
   events, as well as printer functions *)
61
module SF =
62
struct
63

    
64
  (* Basic constructors *)
65

    
66
  let no_action    = Action.nil
67
  let no_condition = Condition.tru
68
  let no_event     = None
69
  let event s      = Some s
70
  let action s     = Action.aquote s
71
  let condition s  = Condition.cquote s
72
  let no_state_action    = {entry_act = no_action; during_act = no_action; exit_act = no_action; }
73
  let state_action a b c = {entry_act = a; during_act = b; exit_act = c; }
74

    
75
  let states (Program (_, defs, _)) =
76
    List.fold_left
77
      (fun res c ->
78
	match c with
79
	| State (p, _) -> ActiveStates.Vars.add p res
80
	| Junction _  -> res
81
        | SFFunction _ -> res
82
      )
83
      ActiveStates.Vars.empty defs
84

    
85
  let init_env model = ActiveStates.Env.from_set (states model) false
86

    
87
  let global_vars (Program (_, _, env)) = env
88

    
89
  (* Lustrec.Printers *)
90

    
91
  let pp_event fmt e =
92
    match e with
93
    | Some e -> Format.fprintf fmt "%s" e
94
    | None -> Format.fprintf fmt "noevent"
95

    
96
  let pp_dest fmt d = match d with
97
    | DPath p -> Format.fprintf fmt "Path %a" pp_path p
98
    | DJunction j -> Format.fprintf fmt "Junction %a" pp_junction_name j
99

    
100
  let pp_trans fmt t =
101
    Format.fprintf fmt
102
      "@[<hov 0>(@[<hov 0>%a,@ %a,@ %a,@ %a,@ %a@]@ )@]"
103
      pp_event t.event
104
      Condition.pp_cond t.condition
105
      Action.pp_act t.condition_act
106
      Action.pp_act t.transition_act
107
      pp_dest t.dest
108

    
109
  let pp_transitions fmt l =
110
    Format.fprintf fmt
111
      "@[<hov 0>[@[<hov 0>%a@]@ ]@]"
112
      (Lustrec.Utils.fprintf_list ~sep:";@ " pp_trans) l
113

    
114
  let pp_comp fmt c = match c with
115
    | Or (_T, _S) ->
116
       Format.fprintf fmt "Or(%a, {%a})"
117
	 pp_transitions _T
118
	 (Lustrec.Utils.fprintf_list ~sep:"; " pp_state_name) _S
119
    | And (_S) ->
120
       Format.fprintf fmt "And({%a})"
121
	 (Lustrec.Utils.fprintf_list ~sep:"; " pp_state_name) _S
122

    
123
  let pp_state_actions fmt sa =
124
    Format.fprintf fmt "@[<hov 0>(%a,@ %a,@ %a)@]"
125
      Action.pp_act sa.entry_act
126
      Action.pp_act sa.during_act
127
      Action.pp_act sa.exit_act
128

    
129
  let pp_state fmt s =
130
    Format.fprintf fmt "@[<v 0>(@[<v 0>%a,@ %a,@ %a,@ %a@]@ @])"
131
      pp_state_actions s.state_actions
132
      pp_transitions s.outer_trans
133
      pp_transitions s.inner_trans
134
      pp_comp s.internal_composition
135

    
136
  let pp_src pp_sffunction fmt src =
137
    Format.fprintf fmt "@[<v>%a@ @]"
138
      (Lustrec.Utils.fprintf_list ~sep:"@ @ "
139
         (fun fmt src -> match src with
140
	    | State (p, def)   -> Format.fprintf fmt "%a: %a"
141
                                  pp_path p pp_state def
142
            | Junction (s, tl) -> Format.fprintf fmt "%a: %a"
143
	                            pp_state_name s
144
	                            pp_transitions tl
145
            | SFFunction p     -> pp_sffunction fmt p
146
         ))
147
      src
148

    
149
  let rec pp_sffunction fmt (Program (name, component_list, _)) =
150
    Format.fprintf fmt "SFFunction name: %s@ %a@ "
151
      name
152
      (pp_src pp_sffunction) component_list
153

    
154
  let pp_vars fmt src =
155
    Format.fprintf fmt "@[<v>%a@ @]"
156
      (Lustrec.Utils.fprintf_list ~sep:"@ " Lustrec.Printers.pp_var)
157
    src
158

    
159
  let pp_prog fmt (Program (name, component_list, vars)) =
160
    Format.fprintf fmt "Main node name: %s@ %a@ %a@"
161
      name
162
      (pp_src pp_sffunction) component_list
163
      pp_vars (List.map fst vars)
164

    
165
  let pp_scope fmt src =
166
    Format.fprintf fmt (match src with
167
        | Constant  -> "Constant"
168
        | Input     -> "Input"
169
        | Local     -> "Local"
170
        | Output    -> "Output"
171
        | Parameter -> "Parameter")
172
end