aboutsummaryrefslogtreecommitdiffstats
path: root/subprojects/docs/src/learn/language/predicates
diff options
context:
space:
mode:
Diffstat (limited to 'subprojects/docs/src/learn/language/predicates')
-rw-r--r--subprojects/docs/src/learn/language/predicates/DerivedFeature.svg76
-rw-r--r--subprojects/docs/src/learn/language/predicates/index.md284
2 files changed, 360 insertions, 0 deletions
diff --git a/subprojects/docs/src/learn/language/predicates/DerivedFeature.svg b/subprojects/docs/src/learn/language/predicates/DerivedFeature.svg
new file mode 100644
index 00000000..be9465b8
--- /dev/null
+++ b/subprojects/docs/src/learn/language/predicates/DerivedFeature.svg
@@ -0,0 +1,76 @@
1<?xml version="1.0" encoding="UTF-8" standalone="no"?>
2<svg width="216pt" height="226pt" viewBox="-6 -6 227.8699951171875 238.39999389648438" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink" class="refinery-9k5t5y1ScYnYvNXEZbWT4"><style>.refinery-9k5t5y1ScYnYvNXEZbWT4 .node text{font-family:"Open Sans Variable","Open Sans","Roboto","Helvetica","Arial",sans-serif;fill:#19202b;}.refinery-9k5t5y1ScYnYvNXEZbWT4 .node .node-outline{stroke:#19202b;}.refinery-9k5t5y1ScYnYvNXEZbWT4 .node .node-header{fill:rgb(53, 161, 173);}.refinery-9k5t5y1ScYnYvNXEZbWT4 .node .node-bg{fill:#fff;}.refinery-9k5t5y1ScYnYvNXEZbWT4 .node-INDIVIDUAL .node-outline{stroke-width:2;}.refinery-9k5t5y1ScYnYvNXEZbWT4 .node-shadow.node-bg{fill:#19202b;opacity:0.24;}.refinery-9k5t5y1ScYnYvNXEZbWT4 .node-exists-UNKNOWN .node-outline{stroke-dasharray:5 2;}.refinery-9k5t5y1ScYnYvNXEZbWT4 .node-typeHash-g .node-header{fill:#e5c07b;}.refinery-9k5t5y1ScYnYvNXEZbWT4 .node-typeHash-h .node-header{fill:#e06c75;}.refinery-9k5t5y1ScYnYvNXEZbWT4 .node-typeHash-i .node-header{fill:#98c379;}.refinery-9k5t5y1ScYnYvNXEZbWT4 .node-typeHash-j .node-header{fill:#c678dd;}.refinery-9k5t5y1ScYnYvNXEZbWT4 .node-typeHash-k .node-header{fill:#80a7f4;}.refinery-9k5t5y1ScYnYvNXEZbWT4 .node-typeHash-l .node-header{fill:#e3d1b2;}.refinery-9k5t5y1ScYnYvNXEZbWT4 .node-typeHash-m .node-header{fill:#e78b8f;}.refinery-9k5t5y1ScYnYvNXEZbWT4 .node-typeHash-n .node-header{fill:#abcc94;}.refinery-9k5t5y1ScYnYvNXEZbWT4 .node-typeHash-o .node-header{fill:#dbb2e8;}.refinery-9k5t5y1ScYnYvNXEZbWT4 .node-typeHash-p .node-header{fill:#92c0e9;}.refinery-9k5t5y1ScYnYvNXEZbWT4 .edge text{font-family:"Open Sans Variable","Open Sans","Roboto","Helvetica","Arial",sans-serif;fill:#19202b;}.refinery-9k5t5y1ScYnYvNXEZbWT4 .edge .edge-line{stroke:#19202b;}.refinery-9k5t5y1ScYnYvNXEZbWT4 .edge .edge-arrow{fill:#19202b;}.refinery-9k5t5y1ScYnYvNXEZbWT4 .edge-UNKNOWN text{fill:#696c77;}.refinery-9k5t5y1ScYnYvNXEZbWT4 .edge-UNKNOWN .edge-line{stroke:#696c77;}.refinery-9k5t5y1ScYnYvNXEZbWT4 .edge-UNKNOWN .edge-arrow{fill:none;}.refinery-9k5t5y1ScYnYvNXEZbWT4 .edge-ERROR text{fill:#ca1243;}.refinery-9k5t5y1ScYnYvNXEZbWT4 .edge-ERROR .edge-line{stroke:#ca1243;}.refinery-9k5t5y1ScYnYvNXEZbWT4 .edge-ERROR .edge-arrow{fill:#ca1243;}.refinery-9k5t5y1ScYnYvNXEZbWT4 .icon-TRUE{fill:#19202b;}.refinery-9k5t5y1ScYnYvNXEZbWT4 .icon-UNKNOWN{fill:#696c77;}.refinery-9k5t5y1ScYnYvNXEZbWT4 .icon-ERROR{fill:#ca1243;}.refinery-9k5t5y1ScYnYvNXEZbWT4 text.label-UNKNOWN{fill:#696c77;}.refinery-9k5t5y1ScYnYvNXEZbWT4 text.label-ERROR{fill:#ca1243;}[data-theme="dark"] .refinery-9k5t5y1ScYnYvNXEZbWT4 .node text{font-family:"Open Sans Variable","Open Sans","Roboto","Helvetica","Arial",sans-serif;fill:#ebebff;}[data-theme="dark"] .refinery-9k5t5y1ScYnYvNXEZbWT4 .node .node-outline{stroke:#ebebff;}[data-theme="dark"] .refinery-9k5t5y1ScYnYvNXEZbWT4 .node .node-header{fill:rgb(60, 127, 135);}[data-theme="dark"] .refinery-9k5t5y1ScYnYvNXEZbWT4 .node .node-bg{fill:#282c34;}[data-theme="dark"] .refinery-9k5t5y1ScYnYvNXEZbWT4 .node-INDIVIDUAL .node-outline{stroke-width:2;}[data-theme="dark"] .refinery-9k5t5y1ScYnYvNXEZbWT4 .node-shadow.node-bg{fill:#ebebff;opacity:0.32;}[data-theme="dark"] .refinery-9k5t5y1ScYnYvNXEZbWT4 .node-exists-UNKNOWN .node-outline{stroke-dasharray:5 2;}[data-theme="dark"] .refinery-9k5t5y1ScYnYvNXEZbWT4 .node-typeHash-g .node-header{fill:#ae8003;}[data-theme="dark"] .refinery-9k5t5y1ScYnYvNXEZbWT4 .node-typeHash-h .node-header{fill:#a23b47;}[data-theme="dark"] .refinery-9k5t5y1ScYnYvNXEZbWT4 .node-typeHash-i .node-header{fill:#428141;}[data-theme="dark"] .refinery-9k5t5y1ScYnYvNXEZbWT4 .node-typeHash-j .node-header{fill:#854797;}[data-theme="dark"] .refinery-9k5t5y1ScYnYvNXEZbWT4 .node-typeHash-k .node-header{fill:#3982bb;}[data-theme="dark"] .refinery-9k5t5y1ScYnYvNXEZbWT4 .node-typeHash-l .node-header{fill:#827662;}[data-theme="dark"] .refinery-9k5t5y1ScYnYvNXEZbWT4 .node-typeHash-m .node-header{fill:#904f53;}[data-theme="dark"] .refinery-9k5t5y1ScYnYvNXEZbWT4 .node-typeHash-n .node-header{fill:#647e63;}[data-theme="dark"] .refinery-9k5t5y1ScYnYvNXEZbWT4 .node-typeHash-o .node-header{fill:#805f89;}[data-theme="dark"] .refinery-9k5t5y1ScYnYvNXEZbWT4 .node-typeHash-p .node-header{fill:#4f7799;}[data-theme="dark"] .refinery-9k5t5y1ScYnYvNXEZbWT4 .edge text{font-family:"Open Sans Variable","Open Sans","Roboto","Helvetica","Arial",sans-serif;fill:#ebebff;}[data-theme="dark"] .refinery-9k5t5y1ScYnYvNXEZbWT4 .edge .edge-line{stroke:#ebebff;}[data-theme="dark"] .refinery-9k5t5y1ScYnYvNXEZbWT4 .edge .edge-arrow{fill:#ebebff;}[data-theme="dark"] .refinery-9k5t5y1ScYnYvNXEZbWT4 .edge-UNKNOWN text{fill:#abb2bf;}[data-theme="dark"] .refinery-9k5t5y1ScYnYvNXEZbWT4 .edge-UNKNOWN .edge-line{stroke:#abb2bf;}[data-theme="dark"] .refinery-9k5t5y1ScYnYvNXEZbWT4 .edge-UNKNOWN .edge-arrow{fill:none;}[data-theme="dark"] .refinery-9k5t5y1ScYnYvNXEZbWT4 .edge-ERROR text{fill:#e06c75;}[data-theme="dark"] .refinery-9k5t5y1ScYnYvNXEZbWT4 .edge-ERROR .edge-line{stroke:#e06c75;}[data-theme="dark"] .refinery-9k5t5y1ScYnYvNXEZbWT4 .edge-ERROR .edge-arrow{fill:#e06c75;}[data-theme="dark"] .refinery-9k5t5y1ScYnYvNXEZbWT4 .icon-TRUE{fill:#ebebff;}[data-theme="dark"] .refinery-9k5t5y1ScYnYvNXEZbWT4 .icon-UNKNOWN{fill:#abb2bf;}[data-theme="dark"] .refinery-9k5t5y1ScYnYvNXEZbWT4 .icon-ERROR{fill:#e06c75;}[data-theme="dark"] .refinery-9k5t5y1ScYnYvNXEZbWT4 text.label-UNKNOWN{fill:#abb2bf;}[data-theme="dark"] .refinery-9k5t5y1ScYnYvNXEZbWT4 text.label-ERROR{fill:#e06c75;}</style><defs><svg xmlns="http://www.w3.org/2000/svg" width="24" height="24" viewBox="0 0 24 24" id="refinery-9k5t5y1ScYnYvNXEZbWT4-icon-TRUE" class="icon-TRUE"><path d="M17.63 5.84C17.27 5.33 16.67 5 16 5L5 5.01C3.9 5.01 3 5.9 3 7v10c0 1.1.9 1.99 2 1.99L16 19c.67 0 1.27-.33 1.63-.84L22 12l-4.37-6.16z"/></svg><svg xmlns="http://www.w3.org/2000/svg" width="24" height="24" viewBox="0 0 24 24" id="refinery-9k5t5y1ScYnYvNXEZbWT4-icon-UNKNOWN" class="icon-UNKNOWN"><path d="M17.63 5.84C17.27 5.33 16.67 5 16 5L5 5.01C3.9 5.01 3 5.9 3 7v10c0 1.1.9 1.99 2 1.99L16 19c.67 0 1.27-.33 1.63-.84L22 12l-4.37-6.16zM16 17H5V7h11l3.55 5L16 17z"/></svg><svg xmlns="http://www.w3.org/2000/svg" width="24" height="24" viewBox="0 0 24 24" id="refinery-9k5t5y1ScYnYvNXEZbWT4-icon-ERROR" class="icon-ERROR"><path d="M12 2C6.47 2 2 6.47 2 12s4.47 10 10 10s10-4.47 10-10S17.53 2 12 2zm5 13.59L15.59 17L12 13.41L8.41 17L7 15.59L10.59 12L7 8.41L8.41 7L12 10.59L15.59 7L17 8.41L13.41 12L17 15.59z"/></svg></defs>
3<g class="graph" transform="translate(4, 222.39999389648438)">
4<!-- n2 -->
5<g class="node node-IMPLICIT node-exists-TRUE node-equalsSelf-TRUE node-typeHash-i">
6
7<rect stroke="none" x="64.75" y="-48.8" width="84.22" height="48.8" rx="12" ry="12" class="node-bg"/>
8<rect stroke="none" x="60" y="-52" width="92" height="27" clip-path="url(#refinery-9k5t5y1ScYnYvNXEZbWT4-clip-0)" class="node-header"/>
9<text text-anchor="start" x="76.52" y="-33" font-size="12.00">transition1</text>
10<use x="70.7485" y="-19.2" width="12" height="12" id="" class="icon icon-TRUE" href="#refinery-9k5t5y1ScYnYvNXEZbWT4-icon-TRUE"/>
11<g><text text-anchor="start" x="86.75" y="-9.6" font-size="12.00" class="label label-TRUE">Transition</text>
12</g>
13<polyline points="64.75,-25.4 148.97,-25.4" class="node-outline"/>
14<rect fill="none" x="64.75" y="-48.8" width="84.22" height="48.8" rx="12" ry="12" class="node-outline"/>
15<clipPath id="refinery-9k5t5y1ScYnYvNXEZbWT4-clip-0"><rect stroke="none" x="64.75" y="-48.8" width="84.22" height="48.8" rx="12" ry="12" class="node-bg"/></clipPath></g>
16<!-- n3 -->
17<g class="node node-IMPLICIT node-exists-TRUE node-equalsSelf-TRUE node-typeHash-h">
18
19<rect stroke="none" x="74.84" y="-218.4" width="64.03" height="48.80000000000001" rx="12" ry="12" class="node-bg"/>
20<rect stroke="none" x="70" y="-222" width="72" height="27" clip-path="url(#refinery-9k5t5y1ScYnYvNXEZbWT4-clip-1)" class="node-header"/>
21<text text-anchor="start" x="85.98" y="-202.6" font-size="12.00">vertex1</text>
22<use x="80.8442" y="-188.8" width="12" height="12" id="" class="icon icon-TRUE" href="#refinery-9k5t5y1ScYnYvNXEZbWT4-icon-TRUE"/>
23<g><text text-anchor="start" x="96.84" y="-179.2" font-size="12.00" class="label label-TRUE">Vertex</text>
24</g>
25<polyline points="74.84,-195 138.87,-195" class="node-outline"/>
26<rect fill="none" x="74.84" y="-218.4" width="64.03" height="48.80000000000001" rx="12" ry="12" class="node-outline"/>
27<clipPath id="refinery-9k5t5y1ScYnYvNXEZbWT4-clip-1"><rect stroke="none" x="74.84" y="-218.4" width="64.03" height="48.80000000000001" rx="12" ry="12" class="node-bg"/></clipPath></g>
28<!-- n2&#45;&gt;n3 -->
29<g class="edge edge-TRUE">
30
31<path fill="none" d="M111.71,-48.78C113.97,-77.25 114.21,-125.59 112.45,-158.38" class="edge-line"/>
32<polygon points="108.96,-157.98 111.8,-168.19 115.95,-158.44 108.96,-157.98" class="edge-line edge-arrow"/>
33<text text-anchor="middle" x="97.12" y="-99.47" font-size="10.50">source</text>
34</g>
35<!-- n4 -->
36<g class="node node-IMPLICIT node-exists-TRUE node-equalsSelf-TRUE node-typeHash-h">
37
38<rect stroke="none" x="143.84" y="-133.6" width="64.03" height="48.8" rx="12" ry="12" class="node-bg"/>
39<rect stroke="none" x="139" y="-137" width="72" height="27" clip-path="url(#refinery-9k5t5y1ScYnYvNXEZbWT4-clip-2)" class="node-header"/>
40<text text-anchor="start" x="154.98" y="-117.8" font-size="12.00">vertex2</text>
41<use x="149.844" y="-104" width="12" height="12" id="" class="icon icon-TRUE" href="#refinery-9k5t5y1ScYnYvNXEZbWT4-icon-TRUE"/>
42<g><text text-anchor="start" x="165.84" y="-94.4" font-size="12.00" class="label label-TRUE">Vertex</text>
43</g>
44<polyline points="143.84,-110.2 207.87,-110.2" class="node-outline"/>
45<rect fill="none" x="143.84" y="-133.6" width="64.03" height="48.8" rx="12" ry="12" class="node-outline"/>
46<clipPath id="refinery-9k5t5y1ScYnYvNXEZbWT4-clip-2"><rect stroke="none" x="143.84" y="-133.6" width="64.03" height="48.8" rx="12" ry="12" class="node-bg"/></clipPath></g>
47<!-- n2&#45;&gt;n4 -->
48<g class="edge edge-TRUE">
49
50<path fill="none" d="M132.35,-48.63C140.1,-57.19 148.46,-67.04 155.81,-76.23" class="edge-line"/>
51<polygon points="152.92,-78.21 161.83,-83.94 158.44,-73.91 152.92,-78.21" class="edge-line edge-arrow"/>
52<text text-anchor="middle" x="133.35" y="-57.15" font-size="10.50">target</text>
53</g>
54<!-- n3&#45;&gt;n2 -->
55<g class="edge edge-TRUE">
56
57<path fill="none" stroke-width="2" d="M102.01,-169.7C99.75,-141.26 99.5,-92.92 101.27,-60.1" class="edge-line"/>
58<polygon stroke-width="2" points="104.3,-60.73 101.81,-51.8 98.18,-60.33 104.3,-60.73" class="edge-line edge-arrow"/>
59<text text-anchor="start" x="0" y="-113.73" font-weight="bold" font-size="10.50">outgoingTransition</text>
60</g>
61<!-- n4&#45;&gt;n2 -->
62<!-- n4&#45;&gt;n2 -->
63<g class="edge edge-TRUE">
64
65<path fill="none" d="M150.52,-85.14C142.77,-76.59 134.41,-66.75 127.05,-57.54" class="edge-line"/>
66<polygon points="129.93,-55.54 121.01,-49.82 124.41,-59.86 129.93,-55.54" class="edge-line edge-arrow"/>
67<text text-anchor="middle" x="87.8" y="-70.33" font-size="10.50">incomingTransition</text>
68</g><g class="edge edge-TRUE">
69
70<path fill="none" d="M126.08,-169.94C133.27,-161.31 141.57,-151.34 149.31,-142.06" class="edge-line"/>
71<polygon points="151.82,-144.51 155.53,-134.59 146.44,-140.03 151.82,-144.51" class="edge-line edge-arrow"/>
72<text text-anchor="middle" x="116.57" y="-154.94" font-size="10.50">neighbors</text>
73</g>
74
75</g>
76</svg> \ No newline at end of file
diff --git a/subprojects/docs/src/learn/language/predicates/index.md b/subprojects/docs/src/learn/language/predicates/index.md
new file mode 100644
index 00000000..261054c1
--- /dev/null
+++ b/subprojects/docs/src/learn/language/predicates/index.md
@@ -0,0 +1,284 @@
1---
2SPDX-FileCopyrightText: 2024 The Refinery Authors
3SPDX-License-Identifier: EPL-2.0
4description: Model queries and model validation
5sidebar_position: 2
6---
7
8# Graph predicates
9
10Graph predicates are logic expressions that can be used to query for interesting model fragments, as well as for validating the consistency of models. They are evaluated on partial models according to [four-valued logic](../logic) semantics.
11
12Predicates in Refinery are written in [Disjunctive Normal Form](https://en.wikipedia.org/wiki/Disjunctive_normal_form) (DNF) as an _OR_ of _ANDs_, i.e., a _disjunction_ of _clauses_ formed as a _conjunction_ of positive or negated logic _literals._
13This matches the syntax and semantics of logical query languages, such as [Datalog](https://en.wikipedia.org/wiki/Datalog), and logical programming languages, such as [Prolog](https://en.wikipedia.org/wiki/Prolog).
14
15import Link from '@docusaurus/Link';
16
17<details>
18<summary>Example metamodel</summary>
19
20In the examples on this page, we will use the following metamodel as illustration:
21
22```refinery
23abstract class CompositeElement {
24 contains Region[] regions
25}
26
27class Region {
28 contains Vertex[] vertices opposite region
29}
30
31abstract class Vertex {
32 container Region region opposite vertices
33 contains Transition[] outgoingTransition opposite source
34 Transition[] incomingTransition opposite target
35}
36
37class Transition {
38 container Vertex source opposite outgoingTransition
39 Vertex[1] target opposite incomingTransition
40}
41
42abstract class Pseudostate extends Vertex.
43
44abstract class RegularState extends Vertex.
45
46class Entry extends Pseudostate.
47
48class Exit extends Pseudostate.
49
50class Choice extends Pseudostate.
51
52class FinalState extends RegularState.
53
54class State extends RegularState, CompositeElement.
55
56class Statechart extends CompositeElement.
57```
58
59<p>
60 <Link
61 href="https://refinery.services/#/1/KLUv_WAEAiUIAOIKIR5gadMGg1ajk9jLoipJ58vc0vAE5opt1YaDpyOCAAdaCjMohSdgl4rj1yTo8UCgpTDHCIAE-o3Jr28mGO9AEoDcR-tLGh4liE2Z3IOX50z-FksLaNWLpLXd1QiUII2vNjCMBWOVEgTzjhG0eHVMIyIyFOjoxcrBv83FkgftlmJ0K_0eVDQgEBSCrXYvD1Q2wlwGXecz2HjRADQOLMh6iIYIWBPuFBBCI2igVgiHAFH4uclAydd4TFayN-oOpjzxgd0FlTzkN6QZ8CQDXBN4EPjB5VJZCANQlJA3wDd_PVyUA5eA0gaeAcgENsm4YnCogWihMAMkA8-CoB-gm9HJC0AB"
62 className="button button--lg button--primary button--play"
63 >Try in Refinery</Link>
64</p>
65
66</details>
67
68[Assertions](../logic/#assertions) about graph predicates can prescribe where the predicate should (for positive assertions) or should not (for negative assertions) hold.
69When generating consistent models
70
71## Atoms
72
73An _atom_ is formed by a _symbol_ and _argument list_ of variables.
74Possible symbols include [classes](../classes/#classes), [references](../classes/#references), and [predicates](../predicates).
75We may write a basic graph query as a conjunction (AND) of atoms.
76
77The `pred` keyword defines a graph predicate. After the _predicate name_, a _parameter list_ of variables is provided. The atoms of the graph predicate are written after the `<->` operator, and a full stop `.` terminates the predicate definition.
78
79The following predicate `entryInRegion` will match pairs of `Region` instances `r` and `Entry` instances `e` such that `e` is a vertex in `r`.
80
81```refinery
82pred entryInRegion(r, e) <->
83 Region(r),
84 vertices(r, e),
85 Entry(e).
86```
87
88We may write unary symbols that act as _parameter types_ directly in the parameter list. The following definition is equivalent to the previous one:
89
90```refinery
91pred entryInRegion(Region r, Entry e) <->
92 vertices(r, e).
93```
94
95import TableIcon from '@material-icons/svg/svg/table_chart/baseline.svg';
96
97:::info
98
99You may display the result of graph predicate matching in the <TableIcon style={{ fill: 'currentColor', verticalAlign: 'text-top' }} title="Table view icon" />&nbsp;_table view_ of the Refinery web UI.
100
101:::
102
103## Quantification
104
105Variables not appearing in the parameter list are _existentially quantified._
106
107The following predicate matches `Region` instances with two entries:
108
109```refinery
110pred multipleEntriesInRegion(Region r) <->
111 entryInRegion(r, e1),
112 entryInRegion(r, e2),
113 e1 != e2.
114```
115
116Existentially quantified variables that appear only once in the predicate should be prefixed with `_`. This shows that the variable is intentionally used only once (as opposite to the second reference to the variable being omitted by mistake).
117
118```refinery
119pred regionWithEntry(Region r) <->
120 entryInRegion(r, _e).
121```
122
123Alternatively, you may use a single `_` whenever a variable occurring only once is desired. Different occurrences of `_` are considered distinct variables.
124
125```refinery
126pred regionWithEntry(Region r) <->
127 entryInRegion(r, _).
128```
129
130## Negation
131
132Negative literals are written by prefixing the corresponding atom with `!`.
133
134Inside negative literals, quantification is _universal:_ the literal matches if there is no assignment of the variables solely appearing in it that satisfies the corresponding atom.
135
136The following predicate matches `Region` instances that have no `Entry`:
137
138```refinery
139pred regionWithoutEntry(Region r) <->
140 !entryInRegion(r, _).
141```
142
143In a graph predicate, all parameter variables must be _positively bound,_ i.e., appear in at least one positive literal (atom).
144Negative literals may further constrain the predicate match one it has been established by the positive literals.
145
146## Object equality
147
148The operators `a == b` and `a != b` correspond to the literals `equals(a, b)` and `!equals(a, b)`, respectively.
149See the section about [multi-objects](../logic/#multi-objects) for more information about the `equals` symbol.
150
151## Transitive closure
152
153The `+` operator forms the [transitive closure](https://en.wikipedia.org/wiki/Transitive_closure) of symbols with exactly 2 parameters.
154The transitive closure `r+(a, b)` holds if either `r(a, b)` is `true`, or there is a sequence of objects `c1`, `c2`, &hellip;, `cn` such that `r(a, c1)`, `r(c1, c2)`, `r(c2, c3)`, &hellip;, `r(cn, b)`.
155In other words, there is a path labelled with `r` in the graph from `a` to `b`.
156
157Transitive closure may express queries about graph reachability:
158
159```refinery
160pred neighbors(Vertex v1, Vertex v2) <->
161 Transition(t),
162 source(t, v1),
163 target(t, v2).
164
165pred cycle(Vertex v) <->
166 neighbors+(v, v).
167```
168
169## Disjunction
170
171Disjunction (OR) of _clauses_ formed by a conjunction (AND) of literals is denoted by `;`.
172
173```refinery
174pred regionWithInvalidNumberOfEntries(Region r) <->
175 !entryInRegion(r, _)
176;
177 entryInRegion(r, e1),
178 entryInRegion(r, e2),
179 e1 != e2.
180```
181
182Every clause of a disjunction must bind every parameter variable of the graph predicate _positively._
183_Type annotations_ on parameter are applied in all clauses.
184Therefore, the previous graph pattern is equivalent to the following:
185
186```refinery
187pred regionWithInvalidNumberOfEntries(r) <->
188 Region(r),
189 !entryInRegion(r, _)
190;
191 Region(r),
192 entryInRegion(r, e1),
193 entryInRegion(r, e2),
194 e1 != e2.
195```
196
197## Derived features
198
199Graph predicates may act as _derived types_ and _references_ in metamodel.
200
201A graph predicate with exactly 1 parameters can be use as if it was a class: you may use it as a [_parameter type_](#atoms) in other graph patterns, as a _target type_ of a (non-containment) [reference](../classes/#references), or in a [_scope constraint_](../logic#type-scopes).
202
203_Derived references_ are graph predicates with exactly 2 parameters, which correspond the source and target node of the reference.
204
205import TuneIcon from '@material-icons/svg/svg/tune/baseline.svg';
206import LabelIcon from '@material-icons/svg/svg/label/baseline.svg';
207import LabelOutlineIcon from '@material-icons/svg/svg/label/outline.svg';
208
209:::info
210
211You may use the <TuneIcon style={{ fill: 'currentColor', verticalAlign: 'text-top' }} title="Filter panel icon" />&nbsp;_filter panel_ icon in Refinery to toggle the visibility of graph predicates with 1 or 2 parameters.
212You may either show <LabelOutlineIcon style={{ fill: 'currentColor', verticalAlign: 'text-top' }} title="Unknown value icon" />&nbsp;_both true and unknown_ values or <LabelIcon style={{ fill: 'currentColor', verticalAlign: 'text-top' }} title="True value icon" />&nbsp;_just true_ values.
213
214:::
215
216---
217
218For example, we may replace the reference `neighbors` in the class `Vertex`:
219
220```refinery
221class Vertex {
222 Vertex[] neighbors
223}
224```
225
226with the graph predicate `neighbors` as follows:
227
228
229```refinery
230class Vertex {
231 contains Transition[] outgoingTransition opposite source
232 Transition[] incomingTransition opposite target
233}
234
235class Transition {
236 container Vertex source opposite outgoingTransition
237 Vertex[1] target opposite incomingTransition
238}
239
240pred neighbors(Vertex v1, Vertex v2) <->
241 Transition(t),
242 source(t, v1),
243 target(t, v2).
244```
245
246Since `neighbors` is now computed based on the `Transition` instances and their `source` and `target` references present in the model, the assertion
247
248```refinery
249neighbors(vertex1, vertex2).
250```
251
252will only be satisfied if a corresponding node `transition1` is present in the generated model that also satisfies
253
254```refinery
255Transition(transition1).
256source(transition1, vertex1).
257target(transition1, vertex2).
258```
259
260import DerivedFeature from './DerivedFeature.svg';
261
262<DerivedFeature />
263
264## Error predicates
265
266A common use-case for graph predicates is _model validation_, where a predicate highlights _errors_ in the model.
267Such predicates are called _error predicates._
268In a consistent generated model, an error predicates should have no matches.
269
270You can declare error predicates with the `error` keyword:
271
272```refinery
273error regionWithoutEntry(Region r) <->
274 !entryInRegion(r, _).
275```
276
277This is equivalent to asserting that the error predicate is `false` everywhere:
278
279```refinery
280pred regionWithoutEntry(Region r) <->
281 !entryInRegion(r, _).
282
283!regionWithoutEntry(*).
284```
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-06-17 19:28:40 +0000