Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / tools / stateflow / src / common / datatype.ml @ 2de7fa82

History | View | Annotate | Download (3.44 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
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 (fun res c -> match c with State (p, _) -> ActiveStates.Vars.add p res | Junction _ -> res) ActiveStates.Vars.empty defs
69

    
70
  let init_env model = ActiveStates.Env.from_set (states model) false
71
    
72
  (* Printers *)
73
      
74
  let pp_event fmt e =
75
    match e with
76
    | Some e -> Format.fprintf fmt "%s" e
77
    | None -> Format.fprintf fmt "noevent"
78
    
79
  let pp_dest fmt d = match d with
80
    | DPath p -> Format.fprintf fmt "Path %a" pp_path p
81
    | DJunction j -> Format.fprintf fmt "Junction %a" pp_junction_name j
82

    
83
  let pp_trans fmt t =
84
    Format.fprintf fmt
85
      "@[<hov 0>(@[<hov 0>%a,@ %a,@ %a,@ %a,@ %a@]@ )@]"
86
      pp_event t.event
87
      Condition.pp_cond t.condition
88
      Action.pp_act t.condition_act
89
      Action.pp_act t.transition_act    
90
      pp_dest t.dest
91
      
92
  let pp_transitions fmt l =
93
    Format.fprintf fmt
94
      "@[<hov 0>[@[<hov 0>%a@]@ ]@]"
95
      (Utils.fprintf_list ~sep:";@ " pp_trans) l
96

    
97
  let pp_comp fmt c = match c with
98
    | Or (_T, _S) ->
99
       Format.fprintf fmt "Or(%a, {%a})"
100
	 pp_transitions _T
101
	 (Utils.fprintf_list ~sep:"; " pp_state_name) _S
102
    | And (_S) ->
103
       Format.fprintf fmt "And({%a})"
104
	 (Utils.fprintf_list ~sep:"; " pp_state_name) _S
105

    
106
  let pp_state_actions fmt sa =
107
    Format.fprintf fmt "@[<hov 0>(%a,@ %a,@ %a)@]"
108
      Action.pp_act sa.entry_act
109
      Action.pp_act sa.during_act
110
      Action.pp_act sa.exit_act
111
      
112
  let pp_state fmt s =
113
    Format.fprintf fmt "@[<v 0>(@[<v 0>%a,@ %a,@ %a,@ %a@]@ @])"
114
      pp_state_actions s.state_actions
115
      pp_transitions s.outer_trans
116
      pp_transitions s.inner_trans
117
      pp_comp s.internal_composition
118
      
119
  let pp_src fmt src =
120
    Format.fprintf fmt "@[<v>%a@ @]"
121
      (Utils.fprintf_list ~sep:"@ @ " (fun fmt src -> match src with
122
	State (p, def) ->
123
	  Format.fprintf fmt "%a: %a"
124
	    pp_path p
125
	    pp_state def
126
      | Junction (s, tl) ->
127
	 Format.fprintf fmt "%a: %a"
128
	   pp_state_name s
129
	   pp_transitions tl
130
       ))
131
      src
132
end
133