-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathmodel.atd
195 lines (150 loc) · 7 KB
/
model.atd
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
(****************************************************************************)
(* *)
(* This file is part of Zephyrus. *)
(* *)
(* Zephyrus is free software: you can redistribute it and/or modify *)
(* it under the terms of the GNU General Public License as published by *)
(* the Free Software Foundation, either version 3 of the License, or *)
(* (at your option) any later version. *)
(* *)
(* Zephyrus is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
(* GNU General Public License for more details. *)
(* *)
(* You should have received a copy of the GNU General Public License *)
(* along with Zephyrus. If not, see <http://www.gnu.org/licenses/>. *)
(* *)
(****************************************************************************)
<doc text="Type definitions for naming.">
type component_type_name = string
type port_name = string
type component_name = string
type package_name = string
type repository_name = string
type location_name = string
type resource_name = string
<doc text="Type definitions for Component Type.">
type provide_arity = [ InfiniteProvide | FiniteProvide of int ]
type require_arity = int
type resource_consumption = int
type resource_provide_arity = int (* Better name? *)
type component_type = {
name : component_type_name;
~provide <ocaml default="[]"> : (port_name * provide_arity) list;
~require <ocaml default="[]"> : (port_name * require_arity) list;
~conflict <ocaml default="[]"> : port_name list;
~consume <ocaml default="[]"> : (resource_name * resource_consumption) list
} <ocaml field_prefix="component_type_">
type component_types = component_type list
<doc text="Type definitions for Universe.">
type package = {
name : package_name;
~depend <ocaml default="[]"> : (package_name list) list;
~conflict <ocaml default="[]"> : package_name list;
~consume <ocaml default="[]"> : (resource_name * resource_consumption) list
} <ocaml field_prefix="package_">
type packages = package list
type repository = {
name : repository_name;
~packages <ocaml default="[]"> : package list;
} <ocaml field_prefix="repository_">
type repositories = repository list
type package_names = package_name list (* This definition is useless, but ATD won't swallow the next one with a type which has nested lists and tuples in the same type. WHY? *)
type universe = {
~component_types <ocaml default="[]"> : component_type list;
~implementation <ocaml default="[]"> : (component_type_name * package_names) list; (* mapping from component type name to sets of package names *)
~repositories <ocaml default="[]"> : repository list
} <ocaml field_prefix="universe_">
<doc text="Type definitions for Configuration.">
type resources_provided = (resource_name * resource_provide_arity) list
type location = {
name : location_name;
~provide_resources <ocaml default="[]"> : resources_provided;
repository : repository_name;
~packages_installed <ocaml default="[]"> : package_name list
} <ocaml field_prefix="location_">
type component = {
component_name : component_name;
component_type : component_type_name;
component_location : location_name;
} (* A little inconsistency: no "field_prefix" parameter here!
* If we try to do it with a "component_" field prefix, we cannot name a field named "component_type",
* because "type" is a keyword... So instead we add the "component_" prefix manually to each field. *)
type binding = {
port : port_name;
requirer : component_name;
provider : component_name;
} <ocaml field_prefix="binding_">
type configuration = {
~locations <ocaml default="[]"> : location list;
~components <ocaml default="[]"> : component list;
~bindings <ocaml default="[]"> : binding list;
} <ocaml field_prefix="configuration_">
(*
* Correctness:
*
* 1. the validity of components (ports: requires / provides, conflicts)
* 2. the validity of implementation (all components are implemented by packages)
* 3. the validity of package dependencies (all package dependencies are satisfied, no package conflicts are violated)
* 4. the validity of resource consumption (all consumed resources are provided)
*
*)
<doc text="Type definitions for Specification.">
type spec_variable_name = string
type spec_const = int
type specification =
[ SpecTrue
| SpecOp of (spec_expr * spec_op * spec_expr)
| SpecAnd of (specification * specification)
| SpecOr of (specification * specification)
| SpecImpl of (specification * specification)
| SpecNot of specification
]
type spec_expr =
[ SpecExprVar of spec_variable_name
| SpecExprConst of spec_const
| SpecExprArity of spec_element
| SpecExprAdd of (spec_expr * spec_expr)
| SpecExprSub of (spec_expr * spec_expr)
| SpecExprMul of (spec_const * spec_expr)
]
type spec_element =
[ SpecElementPackage of package_name
| SpecElementComponentType of component_type_name
| SpecElementPort of port_name
| SpecElementLocalisation of (spec_resource_constraints * spec_repository_constraints * local_specification)
]
type local_specification =
[ SpecLocalTrue
| SpecLocalOp of (spec_local_expr * spec_op * spec_local_expr)
| SpecLocalAnd of (local_specification * local_specification)
| SpecLocalOr of (local_specification * local_specification)
| SpecLocalImpl of (local_specification * local_specification)
| SpecLocalNot of local_specification
]
type spec_local_expr =
[ SpecLocalExprVar of spec_variable_name
| SpecLocalExprConst of spec_const
| SpecLocalExprArity of spec_local_element
| SpecLocalExprAdd of (spec_local_expr * spec_local_expr)
| SpecLocalExprSub of (spec_local_expr * spec_local_expr)
| SpecLocalExprMul of (spec_const * spec_local_expr)
]
type spec_local_element =
[ SpecLocalElementPackage of package_name
| SpecLocalElementComponentType of component_type_name
| SpecLocalElementPort of port_name
]
type spec_resource_constraint = (resource_name * spec_op * spec_const)
type spec_resource_constraints = spec_resource_constraint list
type spec_repository_constraint = repository_name
type spec_repository_constraints = spec_repository_constraint list
type spec_op =
[ Lt
| LEq
| Eq
| GEq
| Gt
| NEq
]