diff options
Diffstat (limited to 'subprojects/docs/src/learn/language/logic/index.md')
-rw-r--r-- | subprojects/docs/src/learn/language/logic/index.md | 256 |
1 files changed, 256 insertions, 0 deletions
diff --git a/subprojects/docs/src/learn/language/logic/index.md b/subprojects/docs/src/learn/language/logic/index.md new file mode 100644 index 00000000..e366e9b8 --- /dev/null +++ b/subprojects/docs/src/learn/language/logic/index.md | |||
@@ -0,0 +1,256 @@ | |||
1 | --- | ||
2 | SPDX-FileCopyrightText: 2024 The Refinery Authors | ||
3 | SPDX-License-Identifier: EPL-2.0 | ||
4 | description: Four-valued logic abstraction | ||
5 | sidebar_position: 1 | ||
6 | --- | ||
7 | |||
8 | # Partial modeling | ||
9 | |||
10 | Refinery allow precisely expressing _unknown,_ _uncertain_ or even _contradictory_ information using [four-valued logic](https://en.wikipedia.org/wiki/Four-valued_logic#Belnap). | ||
11 | During model generation, unknown aspects of the partial model get _refined_ into concrete (true or false) facts until the generated model is completed, or a contradiction is reached. | ||
12 | |||
13 | The _Belnap--Dunn four-valued logic_ supports the following truth values: | ||
14 | |||
15 | * `true` values correspond to facts known about the model, e.g., that a node is the instance of a given class or there is a reference between two nodes. | ||
16 | * `false` values correspond to facts that are known not to hold, e.g., that a node is _not_ an instance of a given class or there is _no_ reference between two nodes. | ||
17 | * `unknown` values express uncertain properties and design decisions yet to be made. During model refinement, `unknown` values are gradually replaced with `true` and `false` values until a consistent and concrete model is derived. | ||
18 | * `error` values represent contradictions and validation failures in the model. One a model contains an error value, it can't be refined into a consistent model anymore. | ||
19 | |||
20 | ## Assertions | ||
21 | |||
22 | _Assertions_ express facts about a partial model. An assertion is formed by a _symbol_ and an _argument list_ of _nodes_ in parentheses. | ||
23 | Possible symbols include [classes](../classes/#classes), [references](../classes/#references), and [predicates](../predicates). | ||
24 | Nodes appearing in the argument list are automatically added to the model. | ||
25 | |||
26 | A _negative_ assertion with a `false` truth value is indicated by prefixing it with `!`. | ||
27 | |||
28 | --- | ||
29 | |||
30 | Consider the following metamodel: | ||
31 | |||
32 | ```refinery | ||
33 | class Region { | ||
34 | contains Vertex[] vertices | ||
35 | } | ||
36 | class Vertex. | ||
37 | class State extends Vertex. | ||
38 | ``` | ||
39 | |||
40 | Along with the following set of assertions: | ||
41 | |||
42 | ```refinery | ||
43 | Region(r1). | ||
44 | Vertex(v1). | ||
45 | Vertex(v2). | ||
46 | !State(v2). | ||
47 | vertices(r1, v1). | ||
48 | vertices(r1, v2). | ||
49 | !vertices(Region::new, v1). | ||
50 | !vertices(Region::new, v2). | ||
51 | ``` | ||
52 | |||
53 | import AssertionsExample from './AssertionsExample.svg'; | ||
54 | |||
55 | <AssertionsExample /> | ||
56 | |||
57 | It is `true` that `r1` is an instance of the class `Region`, while `v1` and `v2` are instances of the class `Vertex`. | ||
58 | We also assert that `v2` is _not_ an instance of the class `State`, but it is unknown whether `v1` is an instance of the class `State`. | ||
59 | Types that are `unknown` are shown in a lighter color and with an outlined icon. | ||
60 | |||
61 | It is `true` that there is a `vertices` reference between `r1` and `v1`, as well as `r1` and `v2`, but there is no such reference from `Region::new` to the same vertices. | ||
62 | As no information is provided, it is `unknown` whether `State::new` is a vertex of any `Region` instance. | ||
63 | References that are `unknown` are shown in a lighter color and with a dashed line. | ||
64 | |||
65 | ### Propagation | ||
66 | |||
67 | Refinery can automatically infer some facts about the partial model based on the provided assertions by information _propagation._ | ||
68 | The set of assertions in the [example above](#assertions) is equivalent to the following: | ||
69 | |||
70 | ```refinery | ||
71 | vertices(r1, v1). | ||
72 | vertices(r1, v2). | ||
73 | !State(v2). | ||
74 | ``` | ||
75 | |||
76 | By the type constraints of the `vertices` reference, Refinery can infer that `r1` is a `Region` instance and `v1` and `v2` are `Vertex` instances. | ||
77 | Since `State` is a subclass of `Vertex`, it is still unknown whether `v1` is a `State` instance, | ||
78 | but `v2` is explicitly forbidden from being such by the negative assertion `!State(v2)`. | ||
79 | We may omit `!vertices(Region::new, v1)` and `!vertices(Region::new, v2)`, since `v1` and `v2` may be a target of only one [containment](../classes/#containment-hierarchy) reference. | ||
80 | |||
81 | Contradictory assertions lead to `error` values in the partial model: | ||
82 | |||
83 | ```refinery | ||
84 | State(v1). | ||
85 | !Vertex(v1). | ||
86 | ``` | ||
87 | |||
88 | import AssertionsError from './AssertionsError.svg'; | ||
89 | |||
90 | <AssertionsError /> | ||
91 | |||
92 | ### Default assertions | ||
93 | |||
94 | Assertions marked with the `default` keyword have _lower priority_ that other assertions. | ||
95 | They may contain wildcard arguments `*` to specify information about _all_ nodes in the graph. | ||
96 | However, they can be overridden by more specific assertions that are not marked with the `default` keyword. | ||
97 | |||
98 | --- | ||
99 | |||
100 | To make sure that the reference `vertices` is `false` everywhere except where explicitly asserted, we may add a `default` assertion: | ||
101 | |||
102 | ```refinery | ||
103 | default !vertices(*, *). | ||
104 | vertices(r1, v1). | ||
105 | vertices(r2, v2). | ||
106 | vertices(r3, v3). | ||
107 | ?vertices(r1, State::new). | ||
108 | ``` | ||
109 | |||
110 | import DefaultAssertions from './DefaultAssertions.svg'; | ||
111 | |||
112 | <DefaultAssertions /> | ||
113 | |||
114 | We can prefix an assertion with `?` to explicitly assert that some fact about the partial model is `unknown`. | ||
115 | This is useful for overriding negative `default` assertions. | ||
116 | |||
117 | ## Multi-objects | ||
118 | |||
119 | The special symbols `exists` and `equals` control the _number of graph nodes_ represented by an object in a partial model. | ||
120 | |||
121 | By default, `exists` is `true` for all objects. | ||
122 | An object `o` with `?exists(o)` (i.e., `exists(o)` explicitly set to `unknown`) may be _removed_ from the partial model. | ||
123 | Therefore, it represents _at least 0_ graph nodes. | ||
124 | |||
125 | By default, `equals` is `true` for its _diagonal_, i.e., we have `equals(o, o)` for all object `o`. | ||
126 | For off-diagonal pairs, i.e., `(p, q)` with `p` not equal to `q`, we always have `!equals(p, q)`: distinct objects can never be _merged._ | ||
127 | If we set a _diagonal_ entry to `unknown` by writing `?equals(o, o)`, the object `o` becomes a **multi-object:** it can be freely _split_ into multiple graph nodes. | ||
128 | Therefore, multi-objects represent _possibly more than 1_ graph nodes. | ||
129 | |||
130 | | `exists(o)` | `equals(o, o)` | Number of nodes | Description | | ||
131 | |:-:|:-:|-:|:-| | ||
132 | | `true` | `true` | `1` | graph node | | ||
133 | | `unknown` | `true` | `0..1` | removable graph node | | ||
134 | | `true` | `unknown` | `1..*` | multi-object | | ||
135 | | `unknown` | `unknown` | `0..*` | removable multi-object | | ||
136 | |||
137 | In the Refinery web UI, `?exists(o)` is represented with a _dashed_ border, while `?equals(o, o)` | ||
138 | |||
139 | ```refinery | ||
140 | node(node). | ||
141 | |||
142 | node(removable). | ||
143 | ?exists(removable). | ||
144 | |||
145 | node(multi). | ||
146 | ?equals(multi, multi). | ||
147 | |||
148 | node(removableMulti). | ||
149 | ?exists(removableMulti). | ||
150 | ?equals(removableMulti, removableMulti). | ||
151 | ``` | ||
152 | |||
153 | import MultiObjects from './MultiObjects.svg'; | ||
154 | |||
155 | <MultiObjects /> | ||
156 | |||
157 | import TuneIcon from '@material-icons/svg/svg/tune/baseline.svg'; | ||
158 | import LabelIcon from '@material-icons/svg/svg/label/baseline.svg'; | ||
159 | import LabelOutlineIcon from '@material-icons/svg/svg/label/outline.svg'; | ||
160 | |||
161 | :::info | ||
162 | |||
163 | You may use the <TuneIcon style={{ fill: 'currentColor', verticalAlign: 'text-top' }} title="Filter panel icon" /> _filter panel_ icon in Refinery to toggle the visibility of special symbols like `exists` and `equals`. | ||
164 | You may either show <LabelOutlineIcon style={{ fill: 'currentColor', verticalAlign: 'text-top' }} title="Unknown value icon" /> _both true and unknown_ values or <LabelIcon style={{ fill: 'currentColor', verticalAlign: 'text-top' }} title="True value icon" /> _just true_ values. | ||
165 | The _object scopes_ toggle will also show the number of graph nodes represented by an object in square brackets after its name, like in the figure above. | ||
166 | ::: | ||
167 | |||
168 | By default, a **new object** `C::new` is added for each non-`abstract` [class](../classes#classes) `C` with `?exists(C::new)` and `?equals(C::new, C::new)`. | ||
169 | This multi-object represents all potential instances of the class. | ||
170 | To assert that no new instances of `C` should be added to the generated model, you may write `!exists(C::new)`. | ||
171 | |||
172 | You may use the `multi` keyword to quickly defined a (removable) multi-object: | ||
173 | |||
174 | ```refinery | ||
175 | multi removableMulti. | ||
176 | % This is equivalent to: | ||
177 | % ?exists(removableMulti). | ||
178 | % ?equals(removableMulti, removableMulti). | ||
179 | ``` | ||
180 | |||
181 | ## Type scopes | ||
182 | |||
183 | _Type scopes_ offer finer-grained control over the number of graph nodes in the generated model (as represented by the multi-objects) that `exists` or `equals` assertions. | ||
184 | |||
185 | A _type scope constraint_ is formed by a unary symbol (a [class](../classes/#classes) or a [predicate](../predicates) with a single parameter) and _scope range._ | ||
186 | Ranges have a form similar to [multiplicity constraints](../classes#multiplicity): a range `n..m` indicates a lower bound of `n` and an upper bound of `m`. | ||
187 | While an upper bound of `*` indicates a possibly unbounded number of objects, generated models will always be finite. | ||
188 | Like for multiplicity constraints, the case `n..n` can be abbreviated as `n`. | ||
189 | |||
190 | The number of nodes in the generated model can be controlled using the `node` special symbol. | ||
191 | For example, we may write the following to generate a model with at least 100 at and most 120 nodes: | ||
192 | |||
193 | ```refinery | ||
194 | scope node = 100..200. | ||
195 | ``` | ||
196 | |||
197 | A `scope` declaration may prescribe type scope constraint for any number of symbols, separated by `,`. | ||
198 | Multiple `scope` declarations are also permitted. | ||
199 | Multiple ranges provided for the same symbol will be intersected, i.e., they influence the generated model simultaneously. | ||
200 | |||
201 | In other words, | ||
202 | ``` | ||
203 | scope Region = 10, State = 80..120. | ||
204 | scope State = 100..150. | ||
205 | % Equivalent to: | ||
206 | scope Region = 10, State = 100..120. | ||
207 | ``` | ||
208 | |||
209 | The _object scopes_ option in the <TuneIcon style={{ fill: 'currentColor', verticalAlign: 'text-top' }} title="Filter panel icon" /> _filter panel_ may help in exploring the effects of object scopes. | ||
210 | |||
211 | --- | ||
212 | |||
213 | Consider the example | ||
214 | |||
215 | ```refinery | ||
216 | class Region { | ||
217 | contains Vertex[] vertices | ||
218 | } | ||
219 | class Vertex. | ||
220 | class State extends Vertex. | ||
221 | scope node = 100..120, Vertex = 50..*. | ||
222 | ``` | ||
223 | |||
224 | import ObjectScopes from './ObjectScopes.svg'; | ||
225 | |||
226 | <ObjectScopes /> | ||
227 | |||
228 | Notice that Refinery could determine that there can be no more than 70 `Region` instances in the generated model, since at least 50 of the `100..120` nodes in the model must be `Vertex` instances. | ||
229 | However, since `State` is a subclass of `Vertex` (i.e., `State::new` is also an instance of `Vertex`), the range `50..*` is shared between both `Vertex::new` and `State::new`, resulting in both representing `0..120` nodes. | ||
230 | Nevertheless, every generated model will obey the scope constraint exactly, i.e., will have between 100 and 120 node, at least 50 of which are `Vertex` instances. | ||
231 | |||
232 | By providing more information, Refinery can determine more precise ranges for multi-objects. | ||
233 | For example, we may strengthen the scope constraints as follows: | ||
234 | |||
235 | ```refinery | ||
236 | scope node = 100..120, Vertex = 50..*, State = 20. | ||
237 | ``` | ||
238 | |||
239 | import StrongerObjectScopes from './StrongerObjectScopes.svg'; | ||
240 | |||
241 | <StrongerObjectScopes /> | ||
242 | |||
243 | ### Incremental scopes | ||
244 | |||
245 | We may specify an _incremental_ object scope with the `+=` operator to determine the number of new instances to be added to the model. | ||
246 | This is only allowed for symbol that are classes with no subclasses, as it directly influences the number of nodes represented by the corresponding `::new` object. | ||
247 | |||
248 | For example, to ensure that between 5 and 7 `State` instances are added to the model, we may write: | ||
249 | |||
250 | ```refinery | ||
251 | State(s1). | ||
252 | State(s2). | ||
253 | scope State += 5..7. | ||
254 | ``` | ||
255 | |||
256 | Since `s1` and `s2` are also instances of the `State` class, the generated concrete model will have between 7 and 9 `State` instances altogether. | ||