# Graph predicates

Graph 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 semantics.

Predicates in Refinery are written in 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.*
This matches the syntax and semantics of logical query languages, such as Datalog, and logical programming languages, such as Prolog.

## Example metamodel

In the examples on this page, we will use the following metamodel as illustration:

`abstract class CompositeElement {`

contains Region[] regions

}

class Region {

contains Vertex[] vertices opposite region

}

abstract 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

}

abstract class Pseudostate extends Vertex.

abstract class RegularState extends Vertex.

class Entry extends Pseudostate.

class Exit extends Pseudostate.

class Choice extends Pseudostate.

class FinalState extends RegularState.

class State extends RegularState, CompositeElement.

class Statechart extends CompositeElement.

Assertions about graph predicates can prescribe where the predicate should (for positive assertions) or should not (for negative assertions) hold. When generating consistent models

## Atoms

An *atom* is formed by a *symbol* and *argument list* of variables.
Possible symbols include classes, references, and predicates.
We may write a basic graph query as a conjunction (AND) of atoms.

The `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.

The following predicate `entryInRegion`

will match pairs of `Region`

instances `r`

and `Entry`

instances `e`

such that `e`

is a vertex in `r`

.

`pred entryInRegion(r, e) <->`

Region(r),

vertices(r, e),

Entry(e).

We may write unary symbols that act as *parameter types* directly in the parameter list. The following definition is equivalent to the previous one:

`pred entryInRegion(Region r, Entry e) <->`

vertices(r, e).

You may display the result of graph predicate matching in the *table view* of the Refinery web UI.

## Quantification

Variables not appearing in the parameter list are *existentially quantified.*

The following predicate matches `Region`

instances with two entries:

`pred multipleEntriesInRegion(Region r) <->`

entryInRegion(r, e1),

entryInRegion(r, e2),

e1 != e2.

Existentially 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).

`pred regionWithEntry(Region r) <->`

entryInRegion(r, _e).

Alternatively, you may use a single `_`

whenever a variable occurring only once is desired. Different occurrences of `_`

are considered distinct variables.

`pred regionWithEntry(Region r) <->`

entryInRegion(r, _).

## Negation

Negative literals are written by prefixing the corresponding atom with `!`

.

Inside 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.

The following predicate matches `Region`

instances that have no `Entry`

:

`pred regionWithoutEntry(Region r) <->`

!entryInRegion(r, _).

In a graph predicate, all parameter variables must be *positively bound,* i.e., appear in at least one positive literal (atom).
Negative literals may further constrain the predicate match one it has been established by the positive literals.

## Object equality

The operators `a == b`

and `a != b`

correspond to the literals `equals(a, b)`

and `!equals(a, b)`

, respectively.
See the section about multi-objects for more information about the `equals`

symbol.

## Transitive closure

The `+`

operator forms the transitive closure of symbols with exactly 2 parameters.
The transitive closure `r+(a, b)`

holds if either `r(a, b)`

is `true`

, or there is a sequence of objects `c1`

, `c2`

, …, `cn`

such that `r(a, c1)`

, `r(c1, c2)`

, `r(c2, c3)`

, …, `r(cn, b)`

.
In other words, there is a path labelled with `r`

in the graph from `a`

to `b`

.

Transitive closure may express queries about graph reachability:

`pred neighbors(Vertex v1, Vertex v2) <->`

Transition(t),

source(t, v1),

target(t, v2).

pred cycle(Vertex v) <->

neighbors+(v, v).

## Disjunction

Disjunction (OR) of *clauses* formed by a conjunction (AND) of literals is denoted by `;`

.

`pred regionWithInvalidNumberOfEntries(Region r) <->`

!entryInRegion(r, _)

;

entryInRegion(r, e1),

entryInRegion(r, e2),

e1 != e2.

Every clause of a disjunction must bind every parameter variable of the graph predicate *positively.*
*Type annotations* on parameter are applied in all clauses.
Therefore, the previous graph pattern is equivalent to the following:

`pred regionWithInvalidNumberOfEntries(r) <->`

Region(r),

!entryInRegion(r, _)

;

Region(r),

entryInRegion(r, e1),

entryInRegion(r, e2),

e1 != e2.

## Derived features

Graph predicates may act as *derived types* and *references* in metamodel.

A graph predicate with exactly 1 parameters can be use as if it was a class: you may use it as a *parameter type* in other graph patterns, as a *target type* of a (non-containment) reference, or in a *scope constraint*.

*Derived references* are graph predicates with exactly 2 parameters, which correspond the source and target node of the reference.

You may use the *filter panel* icon in Refinery to toggle the visibility of graph predicates with 1 or 2 parameters.
You may either show *both true and unknown* values or *just true* values.

For example, we may replace the reference `neighbors`

in the class `Vertex`

:

`class Vertex {`

Vertex[] neighbors

}

with the graph predicate `neighbors`

as follows:

`class Vertex {`

contains Transition[] outgoingTransition opposite source

Transition[] incomingTransition opposite target

}

class Transition {

container Vertex source opposite outgoingTransition

Vertex[1] target opposite incomingTransition

}

pred neighbors(Vertex v1, Vertex v2) <->

Transition(t),

source(t, v1),

target(t, v2).

Since `neighbors`

is now computed based on the `Transition`

instances and their `source`

and `target`

references present in the model, the assertion

`neighbors(vertex1, vertex2).`

will only be satisfied if a corresponding node `transition1`

is present in the generated model that also satisfies

`Transition(transition1).`

source(transition1, vertex1).

target(transition1, vertex2).

## Error predicates

A common use-case for graph predicates is *model validation*, where a predicate highlights *errors* in the model.
Such predicates are called *error predicates.*
In a consistent generated model, an error predicates should have no matches.

You can declare error predicates with the `error`

keyword:

`error regionWithoutEntry(Region r) <->`

!entryInRegion(r, _).

This is equivalent to asserting that the error predicate is `false`

everywhere:

`pred regionWithoutEntry(Region r) <->`

!entryInRegion(r, _).

!regionWithoutEntry(*).