Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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

History | View | Annotate | Download (4.09 KB)

1

    
2
(* Basic datatype for model elements: state and junction name, events ... *)
3
type state_name_t    = string
4
type junction_name_t = string
5
type path_t = state_name_t list
6
type event_base_t = string
7
type event_t      = event_base_t option
8
type base_action_t = string
9
type base_condition_t = string
10
  
11
(* P(r)etty printers *)
12
let pp_state_name = Format.pp_print_string
13
let pp_junction_name = Format.pp_print_string
14
let pp_path fmt p = Utils.fprintf_list ~sep:"." pp_state_name fmt p
15
let pp_event fmt e = match e with None -> Format.fprintf fmt "none" | Some s -> Format.fprintf fmt "%s" s
16
let pp_base_act = Format.pp_print_string
17
let pp_base_cond = Format.pp_print_string
18
  
19
(* Action and Condition types and functions. *)
20

    
21
(* Actions are defined by string + the opening and closing of states *)
22

    
23
(* This version is slightly more complex than the one of EMSOFT'05 to enable the
24
   use of function calls in action.
25

    
26
   TODO: these rich call type could be externalized and a functor introduced. *)
27

    
28
type frontier_t =
29
  | Loose
30
  | Strict
31

    
32
let pp_frontier fmt frontier =
33
  match frontier with
34
  | Loose  -> Format.fprintf fmt "Loose"
35
  | Strict -> Format.fprintf fmt "Strict"
36

    
37
type _ call_t =
38
  | Ecall : (path_t * path_t * frontier_t) call_t
39
  | Dcall : path_t call_t
40
  | Xcall : (path_t * frontier_t) call_t
41

    
42
let pp_call :
43
type a. Format.formatter -> a call_t -> unit = 
44
  fun fmt call ->
45
    match call with
46
    | Ecall -> Format.fprintf fmt "CallE"
47
    | Dcall -> Format.fprintf fmt "CallD"
48
    | Xcall -> Format.fprintf fmt "CallX"
49
  
50
module type ActionType =
51
sig
52
  type t
53
  val nil : t
54
  val aquote : base_action_t -> t
55
  val open_path : path_t -> t
56
  val close_path : path_t -> t
57
  val call : 'c call_t -> 'c -> t
58
    
59
  val pp_act : Format.formatter -> t -> unit
60
end
61

    
62

    
63
module Action =
64
struct
65
  type t =
66
    | Quote : base_action_t -> t
67
    | Close : path_t -> t
68
    | Open  : path_t -> t
69
    | Call  : 'c call_t * 'c -> t
70
    | Nil   : t
71

    
72
    
73
  let nil = Nil
74
  let aquote act = Quote act
75
  let open_path p = Open p
76
  let close_path p = Close p
77
  let call c a = Call (c, a)
78

    
79
  let pp_call : type c. Format.formatter -> c call_t -> c -> unit =
80
    fun fmt call ->
81
    match call with
82
    | Ecall -> (fun (p, p', f) -> Format.fprintf fmt "%a(%a, %a, %a)" pp_call call pp_path p pp_path p' pp_frontier f)
83
    | Dcall -> (fun p          -> Format.fprintf fmt "%a(%a)" pp_call call pp_path p)
84
    | Xcall -> (fun (p, f)     -> Format.fprintf fmt "%a(%a, %a)" pp_call call pp_path p pp_frontier f)
85

    
86
  let pp_act fmt act =
87
    match act with
88
    | Call (c, a)      -> pp_call fmt c a
89
    | Quote a          -> Format.fprintf fmt "%a" pp_base_act a
90
    | Close p          -> Format.fprintf fmt "Close(%a)" pp_path p
91
    | Open p           -> Format.fprintf fmt "Open(%a)" pp_path p
92
    | Nil              -> Format.fprintf fmt "Nil"
93
end
94

    
95
let _ = (module Action : ActionType) 
96

    
97

    
98
(* Conditions are either (1) simple strings, (2) the active status of a state or
99
   (3) occurence of an event. They can be combined (conjunction, negation) *)
100
module type ConditionType =
101
sig
102
  type t
103
  val cquote : base_condition_t -> t
104
  val tru : t
105
  val active : path_t -> t
106
  val event : event_t -> t
107
  val ( && ) : t -> t -> t
108
  val neg : t -> t
109

    
110
  val pp_cond : Format.formatter -> t -> unit
111
end
112

    
113
  module Condition =
114
struct
115
  type t =
116
    | Quote of base_condition_t
117
    | Active of path_t
118
    | Event of event_base_t
119
    | And of t * t
120
    | Neg of t
121
    | True
122

    
123
  let cquote cond = Quote cond
124
  let tru = True
125
  let neg cond = Neg cond
126
  let ( && ) cond1 cond2 = And (cond1, cond2)
127
  let active path = Active path
128
  let event evt =
129
    match evt with
130
    | None   -> True
131
    | Some e -> Event e
132

    
133
  let rec pp_cond fmt cond =
134
    match cond with
135
    | True               -> Format.fprintf fmt "true"
136
    | Active p           -> Format.fprintf fmt "Active(%a)" pp_path p
137
    | Event e            -> Format.fprintf fmt "Event(%s)" e
138
    | Neg cond           -> Format.fprintf fmt "(neg %a)" pp_cond cond
139
    | And (cond1, cond2) -> Format.fprintf fmt "%a /\\ %a" pp_cond cond1 pp_cond cond2
140
    | Quote c            -> Format.fprintf fmt "%a" pp_base_cond c
141

    
142
end
143

    
144
let _ = (module Condition : ConditionType)