Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / tools / stateflow / common / datatype.ml @ 9c654082

History | View | Annotate | Download (4.67 KB)

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 'prog_t src_components_t =
38
  | State of path_t * state_def_t
39
  | Junction of junction_name_t * transitions_t
40
  | SFFunction of 'prog_t
41

    
42
type prog_t = Program of state_name_t * prog_t src_components_t list * (LustreSpec.var_decl * LustreSpec.expr) list
43

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

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

    
48
type user_variable_t = user_variable_name_t * scope_t * datatype_var_init_t
49

    
50
type trace_t = event_t list
51

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

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

    
63
  (* Basic constructors *)
64

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

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

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

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

    
88
  (* Printers *)
89

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

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

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

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

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

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

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

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

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

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

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

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