Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / tools / stateflow / common / basetypes.ml @ 5c0d6e4e

History | View | Annotate | Download (4.3 KB)

1

    
2
let sf_level = 2
3

    
4
(* Basic datatype for model elements: state and junction name, events ... *)
5
type state_name_t         = string
6
type junction_name_t      = string
7
type path_t               = state_name_t list
8
type event_base_t         = string
9
type event_t              = event_base_t option
10
type user_variable_name_t = string
11

    
12
(* Connected to lustrec types *)
13
type base_action_t    = { defs : LustreSpec.eq list; ident : string }
14
type base_condition_t = LustreSpec.expr
15

    
16
(* P(r)etty printers *)
17
let pp_state_name     = Format.pp_print_string
18
let pp_junction_name  = Format.pp_print_string
19
let pp_path fmt p     = Utils.fprintf_list ~sep:"." pp_state_name fmt p
20
let pp_event fmt e    = match e with None -> Format.fprintf fmt "none" | Some s -> Format.fprintf fmt "%s" s
21
let pp_base_act fmt a = Utils.fprintf_list ~sep:",@ " Printers.pp_node_eq fmt a.defs
22
let pp_base_cond      = Printers.pp_expr
23

    
24
(* Action and Condition types and functions. *)
25

    
26
(* Actions are defined by string + the opening and closing of states *)
27

    
28
(* This version is slightly more complex than the one of EMSOFT'05 to enable the
29
   use of function calls in action.
30

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

    
33
type frontier_t =
34
  | Loose
35
  | Strict
36

    
37
let pp_frontier fmt frontier =
38
  match frontier with
39
  | Loose  -> Format.fprintf fmt "Loose"
40
  | Strict -> Format.fprintf fmt "Strict"
41

    
42
type _ call_t =
43
  | Ecall : (path_t * path_t * frontier_t) call_t
44
  | Dcall : path_t call_t
45
  | Xcall : (path_t * frontier_t) call_t
46

    
47
let pp_call :
48
type a. Format.formatter -> a call_t -> unit =
49
  fun fmt call ->
50
    match call with
51
    | Ecall -> Format.fprintf fmt "CallE"
52
    | Dcall -> Format.fprintf fmt "CallD"
53
    | Xcall -> Format.fprintf fmt "CallX"
54

    
55
module type ActionType =
56
sig
57
  type t
58
  val nil : t
59
  val aquote : base_action_t -> t
60
  val open_path : path_t -> t
61
  val close_path : path_t -> t
62
  val call : 'c call_t -> 'c -> t
63

    
64
  val pp_act : Format.formatter -> t -> unit
65
end
66

    
67

    
68
module Action =
69
struct
70
  type t =
71
    | Quote : base_action_t -> t
72
    | Close : path_t -> t
73
    | Open  : path_t -> t
74
    | Call  : 'c call_t * 'c -> t
75
    | Nil   : t
76

    
77

    
78
  let nil = Nil
79
  let aquote act = Quote act
80
  let open_path p = Open p
81
  let close_path p = Close p
82
  let call c a = Call (c, a)
83

    
84
  let pp_call : type c. Format.formatter -> c call_t -> c -> unit =
85
    fun fmt call ->
86
    match call with
87
    | Ecall -> (fun (p, p', f) -> Format.fprintf fmt "%a(%a, %a, %a)" pp_call call pp_path p pp_path p' pp_frontier f)
88
    | Dcall -> (fun p          -> Format.fprintf fmt "%a(%a)" pp_call call pp_path p)
89
    | Xcall -> (fun (p, f)     -> Format.fprintf fmt "%a(%a, %a)" pp_call call pp_path p pp_frontier f)
90

    
91
  let pp_act fmt act =
92
    match act with
93
    | Call (c, a)      -> pp_call fmt c a
94
    | Quote a          -> Format.fprintf fmt "%a" pp_base_act a
95
    | Close p          -> Format.fprintf fmt "Close(%a)" pp_path p
96
    | Open p           -> Format.fprintf fmt "Open(%a)" pp_path p
97
    | Nil              -> Format.fprintf fmt "Nil"
98
end
99

    
100
let _ = (module Action : ActionType)
101

    
102

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

    
115
  val pp_cond : Format.formatter -> t -> unit
116
end
117

    
118
  module Condition =
119
struct
120
  type t =
121
    | Quote of base_condition_t
122
    | Active of path_t
123
    | Event of event_base_t
124
    | And of t * t
125
    | Neg of t
126
    | True
127

    
128
  let cquote cond = Quote cond
129
  let tru = True
130
  let neg cond = Neg cond
131
  let ( && ) cond1 cond2 = And (cond1, cond2)
132
  let active path = Active path
133
  let event evt =
134
    match evt with
135
    | None   -> True
136
    | Some e -> Event e
137

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

    
147
end
148

    
149
let _ = (module Condition : ConditionType)