From 96cd95fc8fbf79b12586f10ccc46a01860837f74 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Krist=C3=B3f=20Marussy?= Date: Tue, 23 Apr 2024 21:22:48 +0200 Subject: [PATCH] docs: metamodeling and partial modeling --- .../docs/src/learn/language/classes.md | 14 - .../language/classes/ContainmentInstance.svg | 227 ++++++++++++++++ .../language/classes/InvalidInstance.svg | 20 ++ .../MultiplicityConstraintsInstance.svg | 229 ++++++++++++++++ .../language/classes/NewObjectsSimple.svg | 29 ++ .../classes/NewObjectsWithInheritance.svg | 38 +++ .../classes/ReferencesOppositeInstance.svg | 69 +++++ .../classes/ReferencesOppositeSelf.svg | 24 ++ .../language/classes/ReferencesSimple.svg | 43 +++ .../docs/src/learn/language/classes/index.md | 212 +++++++++++++++ .../learn/language/logic/AssertionsError.svg | 20 ++ .../language/logic/AssertionsExample.svg | 99 +++++++ .../language/logic/DefaultAssertions.svg | 129 +++++++++ .../src/learn/language/logic/MultiObjects.svg | 81 ++++++ .../src/learn/language/logic/ObjectScopes.svg | 58 ++++ .../language/logic/StrongerObjectScopes.svg | 58 ++++ .../docs/src/learn/language/logic/index.md | 256 ++++++++++++++++++ 17 files changed, 1592 insertions(+), 14 deletions(-) delete mode 100644 subprojects/docs/src/learn/language/classes.md create mode 100644 subprojects/docs/src/learn/language/classes/ContainmentInstance.svg create mode 100644 subprojects/docs/src/learn/language/classes/InvalidInstance.svg create mode 100644 subprojects/docs/src/learn/language/classes/MultiplicityConstraintsInstance.svg create mode 100644 subprojects/docs/src/learn/language/classes/NewObjectsSimple.svg create mode 100644 subprojects/docs/src/learn/language/classes/NewObjectsWithInheritance.svg create mode 100644 subprojects/docs/src/learn/language/classes/ReferencesOppositeInstance.svg create mode 100644 subprojects/docs/src/learn/language/classes/ReferencesOppositeSelf.svg create mode 100644 subprojects/docs/src/learn/language/classes/ReferencesSimple.svg create mode 100644 subprojects/docs/src/learn/language/classes/index.md create mode 100644 subprojects/docs/src/learn/language/logic/AssertionsError.svg create mode 100644 subprojects/docs/src/learn/language/logic/AssertionsExample.svg create mode 100644 subprojects/docs/src/learn/language/logic/DefaultAssertions.svg create mode 100644 subprojects/docs/src/learn/language/logic/MultiObjects.svg create mode 100644 subprojects/docs/src/learn/language/logic/ObjectScopes.svg create mode 100644 subprojects/docs/src/learn/language/logic/StrongerObjectScopes.svg create mode 100644 subprojects/docs/src/learn/language/logic/index.md diff --git a/subprojects/docs/src/learn/language/classes.md b/subprojects/docs/src/learn/language/classes.md deleted file mode 100644 index 7278dc352..000000000 --- a/subprojects/docs/src/learn/language/classes.md +++ /dev/null @@ -1,14 +0,0 @@ ---- -SPDX-FileCopyrightText: 2024 The Refinery Authors -SPDX-License-Identifier: EPL-2.0 -description: Metamodeling in Refinery -sidebar_position: 0 ---- - -# Classes and references - -:::warning - -Under construction - -::: diff --git a/subprojects/docs/src/learn/language/classes/ContainmentInstance.svg b/subprojects/docs/src/learn/language/classes/ContainmentInstance.svg new file mode 100644 index 000000000..197f4b48c --- /dev/null +++ b/subprojects/docs/src/learn/language/classes/ContainmentInstance.svg @@ -0,0 +1,227 @@ + + + + + + + + +v1 + +Vertex + + + + + + + + + +r1 + +Region + + + + + + + + + +region + + + + + + +t1 + +Transition + + + + + + + + + +outgoingTransition + + + + + + + + +t2 + +Transition + + + + + + + + + +outgoingTransition + + + + +incomingTransition + + + + + + + + +t3 + +Transition + + + + + + + + + + + +vertices + + + + + + +v2 + +Vertex + + + + + + + + + +vertices + + + + + + +region + + + + + + +incomingTransition + + + + + + + + + + +v3 + +Vertex + + + + + + + +incomingTransition + + + + + + +r2 + +Region + + + + + + + + + +region + + + + + + + + + + +target + + + + + + + + +vertices + + + + +outgoingTransition + + + + +target + + + + + +source + + + + +target + + + + +source + + + + +source + + \ No newline at end of file diff --git a/subprojects/docs/src/learn/language/classes/InvalidInstance.svg b/subprojects/docs/src/learn/language/classes/InvalidInstance.svg new file mode 100644 index 000000000..fb9dd37de --- /dev/null +++ b/subprojects/docs/src/learn/language/classes/InvalidInstance.svg @@ -0,0 +1,20 @@ + + + + + + + + + +invalid + +Region + + +State + + + + + \ No newline at end of file diff --git a/subprojects/docs/src/learn/language/classes/MultiplicityConstraintsInstance.svg b/subprojects/docs/src/learn/language/classes/MultiplicityConstraintsInstance.svg new file mode 100644 index 000000000..b28c295a7 --- /dev/null +++ b/subprojects/docs/src/learn/language/classes/MultiplicityConstraintsInstance.svg @@ -0,0 +1,229 @@ + + + + + + + + + + + + + + + + +v1 + +Vertex + + + + + + + + + +outgoingTransition + + + + + + +source + + + + + +t1 + +Transition + + + + + + + +source + + + + +outgoingTransition + + + + +t2 + +Transition + + + + + + + + +v2 + +Vertex + + +outgoingTransition::invalidMultiplicity + + + + + + + +t3 + +Transition + + + + + + + + + + + +source + + + + + + +outgoingTransition + + + + + + +t4 + +Transition + + + + + + + + + +v3 + +Vertex + + + +outgoingTransition::invalidMultiplicity + + + + + + + + +source + + + + + + +outgoingTransition + + + + + + +t5 + +Transition + + + + + + + + + +outgoingTransition + + + + + + +t6 + +Transition + + + + + + + + + +outgoingTransition + + + + + + +t7 + +Transition + + + + + + + + + +outgoingTransition + + + + + + +source + + + + + + +source + + + + + + +source + + + \ No newline at end of file diff --git a/subprojects/docs/src/learn/language/classes/NewObjectsSimple.svg b/subprojects/docs/src/learn/language/classes/NewObjectsSimple.svg new file mode 100644 index 000000000..95ba8def7 --- /dev/null +++ b/subprojects/docs/src/learn/language/classes/NewObjectsSimple.svg @@ -0,0 +1,29 @@ + + + + + + + + +Region::new + +Region + + + + + + + + + + +State::new + + + + +State + + \ No newline at end of file diff --git a/subprojects/docs/src/learn/language/classes/NewObjectsWithInheritance.svg b/subprojects/docs/src/learn/language/classes/NewObjectsWithInheritance.svg new file mode 100644 index 000000000..cdf365f0b --- /dev/null +++ b/subprojects/docs/src/learn/language/classes/NewObjectsWithInheritance.svg @@ -0,0 +1,38 @@ + + + + + + + + +Region::new + +Region + + + + + + + + + +State::new + +CompositeElement + + +Vertex + + +RegularState + + +State + + + + + + \ No newline at end of file diff --git a/subprojects/docs/src/learn/language/classes/ReferencesOppositeInstance.svg b/subprojects/docs/src/learn/language/classes/ReferencesOppositeInstance.svg new file mode 100644 index 000000000..56a4d956c --- /dev/null +++ b/subprojects/docs/src/learn/language/classes/ReferencesOppositeInstance.svg @@ -0,0 +1,69 @@ + + + + + + + + + + + + + + + + + + + + +v1 + +Vertex + + + + + + + + +source + + + + +v2 + +Vertex + + + + + + + +t1 + +Transition + + + + + + + +outgoingTransition + + + + +target + + + + +incomingTransition + + \ No newline at end of file diff --git a/subprojects/docs/src/learn/language/classes/ReferencesOppositeSelf.svg b/subprojects/docs/src/learn/language/classes/ReferencesOppositeSelf.svg new file mode 100644 index 000000000..81ab4a0cb --- /dev/null +++ b/subprojects/docs/src/learn/language/classes/ReferencesOppositeSelf.svg @@ -0,0 +1,24 @@ + + + + + + + + +Person::new + +Person + + + + + + + + + +friend + + + \ No newline at end of file diff --git a/subprojects/docs/src/learn/language/classes/ReferencesSimple.svg b/subprojects/docs/src/learn/language/classes/ReferencesSimple.svg new file mode 100644 index 000000000..fac748159 --- /dev/null +++ b/subprojects/docs/src/learn/language/classes/ReferencesSimple.svg @@ -0,0 +1,43 @@ + + + + + + + + +Vertex::new + +Vertex + + + + + + + + + +Transition::new + +Transition + + + + + + + + + +source + + + + + + +target + + + \ No newline at end of file diff --git a/subprojects/docs/src/learn/language/classes/index.md b/subprojects/docs/src/learn/language/classes/index.md new file mode 100644 index 000000000..73108039c --- /dev/null +++ b/subprojects/docs/src/learn/language/classes/index.md @@ -0,0 +1,212 @@ +--- +SPDX-FileCopyrightText: 2024 The Refinery Authors +SPDX-License-Identifier: EPL-2.0 +description: Metamodeling in Refinery +sidebar_position: 0 +--- + +# Classes and references + +Refinery supports _metamodeling_ to describe the desired structure of generated models. + +The metamodeling facilities are inspired by object-oriented software and the [Eclipse Modeling Foundation](https://eclipse.dev/modeling/emf/) (EMF) Core, a lightweight framework for data models. +The textual syntax in Refinery for defining metamodels is largely compatible with [Xcore](https://wiki.eclipse.org/Xcore), a textual syntax for EMF metamodels. + +## Classes + +Classes are declared with the `class` keyword. + +Like in many programming languages, class members are specified between curly braces `{}`. +If a class has no members, the declaration may be terminated with a `.` instead. + +```refinery +% Class with no members. +class Region {} + +% Alternative syntax without curly braces. +class State. +``` + +By default, a _new object_ is added to the partial model to represent the instances of a class. +For example, the new objects `Region::new` and `State::new` represent potential instances of the classes `Region` and `State`, respectively: + +import NewObjectsSimple from './NewObjectsSimple.svg'; + + + +As you can see, no new objects represent potential nodes that are instanceof of both `Region` and `State`. +In fact, such instances are not permitted at all. +Each node must the instance of a _single most-specific class:_ + +import InvalidInstance from './InvalidInstance.svg'; + + + +### Inheritance + +Like in object-oriented programming languages, classes may declare _superclasses_ with the `extends` keyword. +The inheritance hierarchy may not contain any cycles (a class cannot be a superclass of itself), but _multiple inheritance_ is allowed. + +Classes that can't be instantiated directly (i.e., a subclass must be instantiated instead) can be marked with the `abstract` keyword. +Such classes do not have a _new object,_ since there are no direct instances to represent. + +```refinery +abstract class CompositeElement. +class Region. +abstract class Vertex. +abstract class RegularState extends Vertex. +class State extends RegularState, CompositeElement. +``` + +Notice that the new object `State::new` is an instance of `CompositeElement`, `Vertex`, `RegularState`, and `State` as well. + +import NewObjectsWithInheritance from './NewObjectsWithInheritance.svg'; + + + +## References + +The graph structure of model generated by Refinery is determined by the _references_ of the metamodel, which will appear as labeled edges between nodes (class instances). + +References are declared as class members by providing the _target type,_ and optional _multiplicity,_ and the name of the reference: + +```refinery +class Vertex. +class Transition { + Vertex[1] source + Vertex[1] target +} +``` + +import ReferencesSimple from './ReferencesSimple.svg'; + + + +You may add the `refers` keyword for compatibility with [Xcore](https://wiki.eclipse.org/Xcore). The following specification is equivalent: + +```refinery +class Vertex. +class Transition { + refers Vertex[1] source + refers Vertex[1] target +} +``` + +### Opposite constraints + +The `opposite` keywords specifies that two references are in an _opposite_ relationship, i.e., if one reference is present in a direction, the other must be present between the same nodes in the opposite direction. + +``` +class Vertex { + Transition[] outgoingTransition opposite source + Transition[] incomingTransition opposite target +} +class Transition { + Vertex[1] source opposite outgoingTransition + Vertex[1] target opposite incomingTransition +} +``` + +import ReferencesOppositeInstance from './ReferencesOppositeInstance.svg'; + + + +Opposites must be declared in pairs: it is a specification error to declare the `opposite` for one direction but not the other. + +Unlike in EMF, references that are the `opposite` of themselves are also supported. +These must always be present in both directions between two nodes. +Thus, they correspond to undirected graph edges. + +```refinery +class Person { + Person[] friend opposite friend +} +``` + +import ReferencesOppositeSelf from './ReferencesOppositeSelf.svg'; + + + +### Multiplicity + +_Multiplicity constrains_ can be provided after the reference type in square braces. +They specify how many _outgoing_ references should exist for any given instance of the class. + +:::info + +To control the number of _incoming_ references, add an `opposite` reference with multiplicity constraint. + +::: + +A multiplicity constraint is of the form `[n..m]`, where the non-negative integer `n` is the _lower_ bound of outgoing references, +and `m` is a positive integer or `*` corresponding to the _upper_ bound of outgoing references. +The value of `*` represent a reference with _unbounded_ upper multiplicity. + +If `n` = `m`, the shorter form `[n]` may be used. +The bound `[0..*]` may be abbreviated as `[]`. +If the multiplicity constraint is omitted, the bound `[0..1]` is assumed. + +--- + +In the following model, the node `v1` satisfies all multiplicity constraints of `outgoingTransition`. +The node `v2` violates the lower bound constraint, while `v3` violates the upper bound constraint. +All `Transition` instances satisfy the multiplicity constrains associated with `source`. + +```refinery +class Vertex { + Transition[2..3] outgoingTransition opposite source +} +class Transition { + Vertex[1] source opposite outgoingTransition +} +``` + +import MultiplicityConstraintsInstance from './MultiplicityConstraintsInstance.svg'; + + + +### Containment hierarchy + +To structure models and ensure their connectedness, Refinery supports _containment_ constraints. + +References may be marked as _containment_ references with the `contains` keyword. + +Classes that are the _target type_ of at least one _containment_ reference are considered `contained`. +An instance of a `contained` class must have exactly 1 incoming containment reference. +Instances of classes that are not `contained` must _not_ have any incoming containment references. + +Containment references have to form a _forest_, i.e., they must not contain any cycles. +The _roots_ of the forest are instances of classes that are not `contained`, while `contained` classes for the internal nodes and leaves of the trees. + +Opposites of _containment_ references have to be marked with the `container` keyword. +They must not specify any multiplicity constraint, since the multiplicity is already implied by the containment hierarchy. + +--- + +In the following model, the instances of `Region` are the roots of the containment hierarchy. +The classes `Vertex` are `Transition` are both considered `contained`. + +```refinery +class Region { + contains Vertex[] vertices opposite region +} + +class Vertex { + container Region region opposite vertices + contains Transition[] outgoingTransition opposite source + Transition[] incomingTransition opposite target +} + +class Transition { + container Vertex source opposite outgoingTransition + Vertex[1] target opposite incomingTransition +} +``` + +Containment edges are show with **thick** lines: + +import ContainmentInstance from './ContainmentInstance.svg'; + + + +Containment edges form trees, while non-containment references, such as `target`, may point across the containment hierarchy. diff --git a/subprojects/docs/src/learn/language/logic/AssertionsError.svg b/subprojects/docs/src/learn/language/logic/AssertionsError.svg new file mode 100644 index 000000000..8ddc65f30 --- /dev/null +++ b/subprojects/docs/src/learn/language/logic/AssertionsError.svg @@ -0,0 +1,20 @@ + + + + + + + + +v1 + + + +Vertex + + +State + + + + \ No newline at end of file diff --git a/subprojects/docs/src/learn/language/logic/AssertionsExample.svg b/subprojects/docs/src/learn/language/logic/AssertionsExample.svg new file mode 100644 index 000000000..26b3d1fff --- /dev/null +++ b/subprojects/docs/src/learn/language/logic/AssertionsExample.svg @@ -0,0 +1,99 @@ + + + + + + + + +Region::new + +Region + + + + + + + + + +State::new + +Vertex + + +State + + + + + + + + + +vertices + + + + + + + +v1 + +Vertex + + +State + + + + + + + + +r1 + +Region + + + + + + + +v2 + +Vertex + + + + + + + + +vertices + + + + + + + + + + + +vertices + + + + + +vertices + + \ No newline at end of file diff --git a/subprojects/docs/src/learn/language/logic/DefaultAssertions.svg b/subprojects/docs/src/learn/language/logic/DefaultAssertions.svg new file mode 100644 index 000000000..2ab002bf5 --- /dev/null +++ b/subprojects/docs/src/learn/language/logic/DefaultAssertions.svg @@ -0,0 +1,129 @@ + + + + + + + + + + +State::new + +Vertex + + +State + + + + + + + + + + + +r1 + +Region + + + + + + + + + +vertices + + + + + + +v1 + +Vertex + + +State + + + + + + + + + +vertices + + + + + + +r2 + +Region + + + + + + + + + +v2 + +Vertex + + +State + + + + + + + + + +vertices + + + + +v3 + +Vertex + + +State + + + + + + + + +r3 + +Region + + + + + + + + +vertices + + + \ No newline at end of file diff --git a/subprojects/docs/src/learn/language/logic/MultiObjects.svg b/subprojects/docs/src/learn/language/logic/MultiObjects.svg new file mode 100644 index 000000000..a52325755 --- /dev/null +++ b/subprojects/docs/src/learn/language/logic/MultiObjects.svg @@ -0,0 +1,81 @@ + + + + + + + + +node [1] + + + +exists + + + + + + + +equals + + + + + + +removable [0..1] + + + +exists + + + + + + + +equals + + + + + + +multi [1..*] + +exists + + + + + + + + + +equals + + + + + + +removableMulti [0..*] + +exists + + + + + + + + + +equals + + + \ No newline at end of file diff --git a/subprojects/docs/src/learn/language/logic/ObjectScopes.svg b/subprojects/docs/src/learn/language/logic/ObjectScopes.svg new file mode 100644 index 000000000..440dfb192 --- /dev/null +++ b/subprojects/docs/src/learn/language/logic/ObjectScopes.svg @@ -0,0 +1,58 @@ + + + + + + + + +Region::new [0..70] + +Region + + + + + + + + + +State::new [0..120] + +Vertex + + +State + + + + + + + +Vertex::new [0..120] + +Vertex + + + + + + + + + +vertices + + + + + + + + +vertices + + + \ No newline at end of file diff --git a/subprojects/docs/src/learn/language/logic/StrongerObjectScopes.svg b/subprojects/docs/src/learn/language/logic/StrongerObjectScopes.svg new file mode 100644 index 000000000..6f9880652 --- /dev/null +++ b/subprojects/docs/src/learn/language/logic/StrongerObjectScopes.svg @@ -0,0 +1,58 @@ + + + + + + + + +Region::new [0..70] + +Region + + + + + + + + + +State::new [20] + +Vertex + + +State + + + + + + + +Vertex::new [30..100] + +Vertex + + + + + + + + + +vertices + + + + + + + + +vertices + + + \ No newline at end of file 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 000000000..21107d6b5 --- /dev/null +++ b/subprojects/docs/src/learn/language/logic/index.md @@ -0,0 +1,256 @@ +--- +SPDX-FileCopyrightText: 2024 The Refinery Authors +SPDX-License-Identifier: EPL-2.0 +description: Four-valued logic abstraction +sidebar_position: 1 +--- + +# Partial modeling + +Refinery allow precisely expressing _unknown,_ _uncertain_ or even _contradictory_ information using [four-valued logic](https://en.wikipedia.org/wiki/Four-valued_logic#Belnap). +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. + +The _Belnap--Dunn four-valued logic_ supports the following truth values: + +* `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. +* `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. +* `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. +* `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. + +## Assertions + +_Assertions_ express facts about a partial model. An assertion is formed by a _symbol_ and an _argument list_ of _nodes_ in parentheses. +Possible symbols include [classes](../classes/#classes), [references](../classes/#references), and [predicates](../predicates). +Nodes appearing in the argument list are automatically added to the model. + +A _negative_ assertion with a `false` truth value is indicated by prefixing it with `!`. + +--- + +Consider the following metamodel: + +```refinery +class Region { + contains Vertex[] vertices +} +class Vertex. +class State extends Vertex. +``` + +Along with the following set of assertions: + +```refinery +Region(r1). +Vertex(v1). +Vertex(v2). +!State(v2). +vertices(r1, v1). +vertices(r1, v2). +!vertices(Region::new, v1). +!vertices(Region::new, v2). +``` + +import AssertionsExample from './AssertionsExample.svg'; + + + +It is `true` that `r1` is an instance of the class `Region`, while `v1` and `v2` are instances of the class `Vertex`. +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`. +Types that are `unknown` are shown in a lighter color and with an outlined icon. + +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. +As no information is provided, it is `unknown` whether `State::new` is a vertex of any `Region` instance. +References that are `unknown` are shown in a lighter color and with a dashed line. + +### Propagation + +Refinery can automatically infer some facts about the partial model based on the provided assertions by information _propagation._ +The set of assertions in the [example above](#assertions) is equivalent to the following: + +```refinery +vertices(r1, v1). +vertices(r1, v2). +!State(v2). +``` + +By the type constraints of the `vertices` reference, Refinery can infer that `r1` is a `Region` instance and `v1` and `v2` are `Vertex` instances. +Since `State` is a subclass of `Vertex`, it is still unknown whether `v1` is a `State` instance, +but `v2` is explicitly forbidden from being such by the negative assertion `!State(v2)`. +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. + +Contradictory assertions lead to `error` values in the partial model: + +```refinery +State(v1). +!Vertex(v1). +``` + +import AssertionsError from './AssertionsError.svg'; + + + +### Default assertions + +Assertions marked with the `default` keyword have _lower priority_ that other assertions. +They may contain wildcard arguments `*` to specify information about _all_ nodes in the graph. +However, they can be overridden by more specific assertions that are not marked with the `default` keyword. + +--- + +To make sure that the reference `vertices` is `false` everywhere except where explicitly asserted, we may add a `default` assertion: + +```refinery +default !vertices(*, *). +vertices(r1, v1). +vertices(r2, v2). +vertices(r3, v3). +?vertices(r1, State::new). +``` + +import DefaultAssertions from './DefaultAssertions.svg'; + + + +We can prefix an assertion with `?` to explicitly assert that some fact about the partial model is `unknown`. +This is useful for overriding negative `default` assertions. + +## Multi-objects + +The special symbols `exists` and `equals` control the _number of graph nodes_ represented by an object in a partial model. + +By default, `exists` is `true` for all objects. +An object `o` with `?exists(o)` (i.e., `exists(o)` explicitly set to `unknown`) may be _removed_ from the partial model. +Therefore, it represents _at least 0_ graph nodes. + +By default, `equals` is `true` for its _diagonal_, i.e., we have `equals(o, o)` for all object `o`. +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._ +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. +Therefore, multi-objects represent _possibly more than 1_ graph nodes. + +| `exists(o)` | `equals(o, o)` | Number of nodes | Description | +|:-:|:-:|-:|:-| +| `true` | `true` | `1` | graph node | +| `unknown` | `true` | `0..1` | removable graph node | +| `true` | `unknown` | `1..*` | multi-object | +| `unknown` | `unknown` | `0..*` | removable multi-object | + +In the Refinery web UI, `?exists(o)` is represented with a _dashed_ border, while `?equals(o, o)` + +```refinery +node(node). + +node(removable). +?exists(removable). + +node(multi). +?equals(multi, multi). + +node(removableMulti). +?exists(removableMulti). +?equals(removableMulti, removableMulti). +``` + +import MultiObjects from './MultiObjects.svg'; + + + +import TuneIcon from '@material-icons/svg/svg/tune/baseline.svg'; +import LabelIcon from '@material-icons/svg/svg/label/baseline.svg'; +import LabelOutlineIcon from '@material-icons/svg/svg/label/outline.svg'; + +:::info + +You may use the  _filter panel_ icon in refinery to toggle the visibility of special symbols like `exists` and `equals`. +You may either show  _both true and unknown_ values or  _just true_ values. +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. +::: + +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)`. +This multi-object represents all potential instances of the class. +To assert that no new instances of `C` should be added to the generated model, you may write `!exists(C::new)`. + +You may use the `multi` keyword to quickly defined a (removable) multi-object: + +``` +mutlti removableMulti. +% This is equivalent to: +% ?exists(removableMulti). +% ?equals(removableMulti, removableMulti). +``` + +## Type scopes + +_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. + +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._ +Ranges have a form similar to [multiplicity constraints](../classes#multiplciity): a range `n..m` indicates a lower bound of `n` and an upper bound of `m`. +While an upper bound of `*` indicates a possibly unbounded number of objects, generated models will always be finite. +Like for multiplicity constraints, the case `n..n` can be abbreviated as `n`. + +The number of nodes in the generated model can be controlled using the `node` special symbol. +For example, we may write the following to generate a model with at least 100 at and most 120 nodes: + +```refinery +scope node = 100..200. +``` + +A `scope` declaration may prescribe type scope constraint for any number of symbols, separated by `,`. +Multiple `scope` declarations are also permitted. +Multiple ranges provided for the same symbol will be intersected, i.e., they influence the generated model simultaneously. + +In other words, +``` +scope Region = 10, State = 80..120. +scope State = 100..150. +% Equivalent to: +scope Region = 10, State = 100..120. +``` + +The _object scopes_ option in the  _filter panel_ may help in exploring the effects of object scopes. + +--- + +Consider the example + +```refinery +class Region { + contains Vertex[] vertices +} +class Vertex. +class State extends Vertex. +scope node = 100..120, Vertex = 50..*. +``` + +import ObjectScopes from './ObjectScopes.svg'; + + + +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. +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. +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. + +By providing more information, Refinery can determine more precise ranges for multi-objects. +For example, we may strengthen the scope constraints as follows: + +```refinery +scope node = 100..120, Vertex = 50..*, State = 20. +``` + +import StrongerObjectScopes from './StrongerObjectScopes.svg'; + + + +### Incremental scopes + +We may specify an _incremental_ object scope with the `+=` operator to determine the number of new instances to be added to the model. +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. + +For example, to ensure that between 5 and 7 `State` instances are added to the model, we may write: + +```refinery +State(s1). +State(s2). +scope State += 5..7. +``` + +Since `s1` and `s2` are also instances of the `State` class, the generated concrete model will have between 7 and 9 `State` instances altogether.