Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / tools / stateflow / common / datatype.ml @ 93119c3f

History | View | Annotate | Download (3.53 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 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