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.

Try in Refinery

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

info

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.

info

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(*).