advanced.tex

\clearpage
\section{Advanced Concepts}
\seclabel{advanced}


\subsection{Wildcards and Label Variables}
\seclabel{wildcard}

Wildcards are special edge labels that can be used in rules to stand for
\emph{arbitrary} labels. The basic wildcard is just a question mark
``\lab?'': it is matched by any edge of which the source and target node
also match. Wildcards can be used as readers, embargoes and erasers;
\emph{named} wildcards can also be used as creators, see below.

\paragraph{Type or flag wildcards.}

Ordinary wildcards, of the form ``\lab?'' introduced above, can only
capture edges. Node types and flags can also be matched by wildcards, by using
``\lab{\typeP?}'' or ``\lab{\flagP?}'' instead.

\paragraph{Guarded wildcards.}

Wildcards can be \emph{guarded} either by a list of allowed labels or by a list
of forbidden labels:
\begin{itemize}\noitemsep
\item \lab{?[a,b,c]} stands for a wildcard that can only be matched by
  labels \lab{a}, \lab{b} or \lab{c} (this is therefore the same as
  the regular expression ``\lab{a$|$b$|$c}''; however, in contrast to
  regular expressions, wildcards (when used on their own) may occur on eraser
  edges, and (when named) also on creator edges.

\item \lab{?[\^{}a,b,c]} stands for a wildcard that can be matched by any
  label \emph{except} \lab{a}, \lab{b} or \lab{c}.
\end{itemize}
%
The labels \blab{a}, \blab{b}, \blab{c} above stand for edge labels, node types
or flags, depending on the kind of wildcard (\lab?, \typeP\lab? or
\flagP\lab?).

\paragraph{Named wildcards.}

Finally, wildcards can have a \emph{name}, in which case they act as
\emph{label variables}. The name directly follows the question mark, hence
``\lab{?x}'' is a wildcard with name \lab{x}. When such a wildcard is
matched by a certain edge label, that label is considered to be the
\emph{value} of the variable for the duration of the rule application. The same
label variable can occur multiple times within a single rule; the effect is
that each of these occurrences must be matched by the same label.

Variable names can be freely chosen (except that they must adhere to the syntax
rules of an identifier, i.e., start with a letter and consist only of letters,
digits and underscores); they may in fact coincide with actual labels, though
this must be considered bad practice. Variable names can also be combined with
guards; for instance, ``\lab{?x[\^{}a,b,c]}'' is matched by any label except
\lab{a}, \lab{b} or \lab{c}; the matching label is then bound to
\lab{x}.

In contrast to ordinary wildcards, named wildcards can be used on creator
edges, providing that a binding instance occurs in the LHS. This enables the
\emph{copying} of types, flags or edge labels.

For instance, the following rule specifies that if the same flag occurs on two
different \tlab{Person}s, and this flag is not \flab{John}, then it should be
added on a collector node labelled \tlab{Duplicates}, provided it is not
already there. The type label \tlab{Person} is automatically exempted from this
treatment.

\views{wildcard}
%
When using type graphs, the use of wildcards as creators is forbidden.

\paragraph{Example usage.}

The use of the above features is demonstrated by the following \GROOVE samples:
%
\begin{itemize}\noitemsep
\item \textsf{wildcards}, showing the general use of wildcards;
\item \textsf{counting}, demonstrating the use of variables in wildcards.
\end{itemize}

\subsection{Regular Expressions}
\seclabel{regular}

Rule edges can specify regular expressions over graph labels. Such a regular
expression is matched by any chain of edges in the host graph of which the
labels form a word recognised by the regular expression. Regular expressions
may only be used on reader and embargo edges, never on erasers or creators
(except in the special case of wildcards, discussed above).

Regular expressions are distinguished by surrounding curly braces. Thus,
``\lab{\{a.b\}}'' specifies a regular expression (matched by two consecutive
graph edges labelled ``\lab{a}'' and ``\lab{b}'') whereas ``\lab{a.b}''
specifies a single edge with exactly that label. Regular expressions are built
up from the following operators (for an overview see \tabcite{regular}):
%
\begin{table}
\begin{center}
\begin{tabular}{|c|l|}
\hline\hline
\bf Expression & \bf Meaning \\
\hline
\lab{\itshape label} & Simple label; matched literally \\
\lab{=} & Empty path/equality of nodes (see \seccite{equality}) \\
\lab? & Wildcard, possibly named and/or guarded (see
\seccite{wildcard}) \\
\lab{$R_1$.$R_2$} & Sequential composition of $R_1$ and $R_2$ \\
\lab{$R_1|R_2$} & Choice between $R_1$ and $R_2$ \\
\lab{$R$*} & Zero or more repetitions of $R$ \\
\lab{$R$+} & One or more repetitions of $R$ \\
\lab{-$R$} & Inversion of $R$ (matches $R$ when followed backwards) \\
\lab{!$R$} & Negation of $R$ (absence of a match for $R$) \\
\hline\hline
\end{tabular}
\end{center}
\vspace*{-\medskipamount}
\caption{Regular expressions}
\vspace*{-\medskipamount}
\tablabel{regular}
\end{table}
%
\begin{description}
\item[Atoms] These are simple labels, to be matched precisely. Note that the
  syntax rules discussed in \seccite{rules} must be followed whenever the label
  to be matched contains special characters.

\item[Sequencing] This is a binary infix operator, denoted ``\textsf{.}'',
  specifying that its left hand operator should match, followed by its right
  hand operator. Thus, a label sequence matches the regular expression
  \textsf{$R_1$.$R_2$} if it can be split into two sequences, the first of
  which matches $R_1$ and the second $R_2$.

\item[Choice] This is a binary infix operator, denoted ``\textsf{$|$}'',
  specifying that one of its operands should match. Thus, a label sequence
  matches the regular expression \textsf{$R_1|R_2$} if it matches either
  $R_1$ or $R_2$.

\item[Star] The star (or \emph{Kleene} star) (``\textsf{*}'') is a postfix
  operator that specifies that the preceding regular expression occurs zero or
  more times. Thus, a label sequence matches \textsf{$R$*} if it can be split
  into zero or more subsequences, each of which matches $R$.

\item[Plus] The plus (``\textsf{+}'') is a postfix operator that specifies that
  the preceding regular expression occurs one or more times. Thus, a label
  sequence matches \lab{$R$+} if it can be split into one or more
  subsequences, each of which matches $R$.

\item[Inversion] This is a prefix operator, denoted by the minus sign
  (``\lab{-}''), specifying that its operand should be interpreted in
  reverse, \emph{including the direction of the edges}. Thus, a sequence of
  edges matches \textsf{-$R$} if it matches $R$ when followed backwards.

\item[Equality] An equality sign (``\lab{=}'') may be used as an atomic
  entity in a regular expression, in which case it stands for the empty word,
  or in other words, it is matched by an emtpy sequence of edges in the host
  graph. For instance, the regular expression ``\lab{a$|$=}'' specifies that
  between two nodes there is an \textsf{a}-edge or the nodes coincide. Also,
  \textsf{$R$*} has the same meaning as \lab{$R$+$|$=} (for any regular
  expressions $R$).

\item[Wildcard] This is exactly as discussed in \seccite{wildcard} above.  Note
  that a named wildcard can only be used within a regular expression if the
  name is \emph{bound} by another occurrence, not inside a regular expression.

\item[Negation] This is the same as discussed in \seccite{negation}. Negations
  are specified by a single exclamation mark (``\lab{!}'') preceding the
  entire regular expression. Thus, they cannot be used \emph{inside} a
  regular expression. In fact, a negation is not properly part of the regular
  expression itself, since it is in itself not matched by anything; rather, it
  expresses the absence of a match for the actual regular expression.
\end{description}

For instance, the following rule specifies that a son should receive the name
of one of his forefathers.

\views{regular}

\paragraph{Example usage.}

The use of the above features is demonstrated by the \GROOVE \textsf{wildcards}
sample.

\subsection{Data Attributes}
\seclabel{attributes}

\emph{Attribute syntax has been much improved.}\marginpar{TODO}

\medskip\noindent
So far we have not discussed how to specify and manipulate data values, such as
integers, booleans and strings. In \GROOVE, as in other graph transformation
tools, data is included in the form of \emph{attributes}, which are essentially
edges to special data nodes. The data nodes represent the actual data values.

\paragraph{Data values.}

Typically, graph nodes are abstractions of objects from the model space which
somehow have an identity. That is, a graph can have multiple nodes that are
indistinguishable when only their connecting edges are taken into account. This
is not directly suitable for data nodes, however: for instance, every natural
number exists only \emph{once}, and it makes no sense to include multiple nodes
all of which represent this single value. Thus, it is necessary to make a
strict distinction between data nodes and ordinary graph nodes. In \GROOVE,
this is done in either of the following ways:

\begin{itemize}
\item If the concrete data value is known, then it is specified using a node
  label of the form ``\textsf{{\itshape type}:{\itshape const}}'', where
  \textsf{\itshape type} is the data type and \textsf{\itshape const} a
  denotation of its value. The available data types are \textsf{int},
  \textsf{bool}, \textsf{string} and \textsf{real}. The denotation of the
  constants is the usual one; e.g., \textsf{-1}, \textsf{0}, \textsf{1} etc.\
  for \textsf{int}, \textsf{true} and \textsf{false} of \textsf{bool} and
  \textsf{``text''} for \textsf{string}.

\item If the value is not known, for instance because the node occurs in the
  LHS and the value will only be established when matching the rule, then it
  should be labelled ``\textsf{attr:}''.
\end{itemize}
%
Data nodes can never be created or deleted and are always present (at least
virtually); hence, they can only occur as readers.

\paragraph{Operations.}

In addition to specifying data values, we also need to manipulate them; that
is, carry out calculations. This, too, is specified graphically, through
the following special types of nodes and edges:
%
\begin{description}
\item[Product nodes,] which essentially stand for \emph{tuples} of data
  values. Product nodes are distinguished by the special label
  ``\textsf{prod:}''.

\item[Argument edges,] which lead from a product node to the data nodes that
  constitute the individual values of the tuple. Argument edges are labelled
  ``\textsf{arg:{\itshape num}}'', where \textsf{\itshape num} is the argument
  number, ranging from \textsf{0} to (but not including) the size of the tuple.

\item[Operator edges,] which lead from a product node to a data node
  representing the result of an operation performed on the elements of the
  tuple. Operator edges are labelled ``\textsf{{\itshape type}:{\itshape
  op}}'', where \textsf{\itshape type} is a data type (which are the same as
  for the data nodes) and \textsf{\itshape op} is an operation performed on the
  source node tuple; for instance, \textsf{add} (for a pair of \textsf{int}
  values), \textsf{and} (for a pair of \textsf{bool} values), or
  \textsf{concat} (for a pair of \textsf{string} values). \tabcite{data} gives an
  overview of the available operations.
\end{description}

\begin{table}
\begin{center}
\begin{tabular}{|c|c|l|}
\hline\hline
\bf Type & \bf Op & \bf Meaning \\
\hline
\sf bool
  & \sf and & Conjunction of two boolean values \\
  & \sf or  & Disjunction of two boolean values \\
  & \sf not & Negation of a boolean value \\
  & \sf eq & Comparison of two boolean values \\
\cline{2-3}
  & \sf true & Boolean constant \\
  & \sf false & Boolean constant \\
\hline
\textsf{int}/\textsf{real}
  & \sf add & Addition of two integer or real values  \\
  & \sf sub & Subtraction of the second argument from the first \\
  & \sf mul & Multiplication of two integer or real values \\
  & \sf div & Integer (for \textsf{int}) or real (for \textsf{real}) division of the first argument by the second \\
  & \sf mod & Remainder after integer division (only for \textsf{int}) \\
  & \sf min & Minimum of two integer or real values \\
  & \sf max & Maximum of two integer or real values \\
  & \sf lt & Test if the first argument is
  smaller than the second \\
  & \sf le & Test if the first argument is
  smaller than or equal to the second \\
  & \sf gt & Test if the first argument is
  greater than the second \\
  & \sf ge & Test if the first argument is
  greater than or equal to the second \\
  & \sf eq & Comparison of two integer or real values \\
  & \sf neg & The negation of an integer or real value \\
  & \sf toString & Conversion of an integer or real value to a string \\
\hline
\sf string
  & \sf concat & Concatenation of two string values \\
  & \sf lt & Test if the first argument is
  lexicographically smaller than the second \\
  & \sf le & Test if the first argument is
  lexicographically smaller than or equal to the second \\
  & \sf gt & Test if the first argument is
  lexicographically greater than the second \\
  & \sf ge &Test if the first argument is
  lexicographically greater than or equal to the second \\
  & \sf eq & Comparison of two string values \\
\hline\hline
\end{tabular}
\end{center}
\vspace*{-\medskipamount}
\caption{Data types and operations}
\vspace*{-\medskipamount}
\tablabel{data}
\end{table}

In the Display view of rules, data nodes are depicted by ellipses and product
nodes by diamonds. In the Display view of graphs, the attribute edges leading
to data nodes as well as the data nodes themselves are not depcited as edges
and nodes at all, but rather in the more familiar sttribute notation, as
equations within the source nodes. (There is, however, an option in the
Simulator to switch off the attribute notation and show data values as
ellipsoid nodes.) For instance, the following rule
specifies the withdrawal from a bank account, provided the balance does not
become negative.

\views{attribute-rule}

The following shows an attributed graph:

\views{attribute-graph}

\paragraph{Algebras.}

Formally speaking, the operations listed in \tabcite{data}, as well as the data
values discussed above, are actually operators and constant symbols out of a
data \emph{signature}. This signature is then interpreted by an \emph{algebra},
which defines concrete values and functions for these symbols. There is a
default or natural algebra for our signature, which is the one that we all know
from mathematics; in a context where this is the only possible interpretation,
the distinction between signature and algebra is actually irrelevant. However,
\GROOVE{} offers the possibility of slotting in another algebra instead:
through the grammar properties (see \seccite{system-properties}) you can
specify under which algebra the rules should be interpreted.

Currently, three choices are supported:
\begin{itemize}\noitemsep
\item The default algebra, which is actually
implemented using the standard Java types \textsf{int}, \textsf{double},
\textsf{boolean} and \textsf{String};
\item The \emph{point algebra}, in which each data type has exactly one
  value. Every constant and operation returns this value.
\item The \emph{big algebra}, in which integers have arbitrary precision and
  reals have 34 digits of mantissa (which is twice the precision of Java
  \textsf{double}s).
\end{itemize}
%
In the default algebra, comparison of reals (using \textsf{eq}, \textsf{geq}
etc.) has a \emph{tolerance} of $10^{-15}$. In other words, if the difference
between two values is less than $10^{-15}$ times any of these values, then the
values are considered to be equal. This is so as to avoid the phenomenon that
rounding errors result in an artificial difference between values that would
otherwise be equal. In the case of the big algebra, the tolerance is
$10^{-30}$.

\paragraph{Example usage.}

The use of attributes is demonstrated by the \GROOVE \textsf{attributed-graphs}
sample.

\subsection{Rule Parameters}
\seclabel{parameters}

Rule parameters provide a way to make information about a match visible in the
transition system. A rule parameter is a node of LHS (on the implicit
existential level, see \seccite{nested}) that is marked with the special prefix
``\textsf{par=\${\itshape num}}'', where \textsf{\itshape num} is a parameter
number. Parameter numbers should form a consecutive sequence from 1 upwards; no
parameter number may occur more than once in a given rule. The following shows
a rule and a potential start graph.

\begin{equation}\eqlabel{parameters}
\tikzboxview{Rule edit view}{parameters-edit} \qquad
\tikzboxview{Rule display view}{parameters-display} \qquad
\tikzboxview{Start graph}{parameter-start-display}
\end{equation}

\paragraph{Node identities as arguments}

When a rule is eveluated, this results in a transition labelled by the rule
name (see \seccite{trans}). However, if a rule has parameters, and if the
\textsf{transitionParameters} property is set (see \seccite{system-properties})
then the transition labels are appended by lists of parameter values, being the
node identities of the host graph nodes matching the parameter nodes.

Note that a node identity is normally not visible in a graph. The node
identities appearing as transition parameters are denoted ``\lab{n{\itshape
id}}'', where \lab{\itshape id} is the \emph{node number} of the concrete graph
node. \emph{There is no guarantee that node identities are preserved among
graphs!} This means that before and after a transition, the same node identity
may refer to a completely different node. On the other hand, if a node identity
appears on different parameterised transitions starting in the \emph{same}
graph, then it is certain that this refers each time to the same node of that
graph.

\paragraph{Data values as arguments}

The situation is slightly different if the parameter node is an attribute node,
for as discussed above, the identity of a data node is taken to be the data
value itself. So, in that case, the data value is shown in the parameter list.

For instance, the applying the rule in \eqcite{parameters} to the graph also
shown there, there will be two transitions labelled
\textsf{parameters(n38152,``a'')} and \textsf{parameters(n38153,``a'')},
respectively.

\paragraph{Anonymous parameters}

Declaring a node to be a rule parameter has another effect, besides putting the
node identity on the transition label. Namely, those rule matches that map a
parameter node to a different host graph node will \emph{always} give rise to
distinct rule applications, even if the rule effect is the same. 

This is most noticeable in rules that do not modify the graph, i.e., in which
the LHS and RHS coincide (no erasers and no creators). Such rules essentially
encode \emph{conditions} on the graph, i.e., they measure the existence of a
match. Normally such an unmodifying rule is considered to have at most one
application in any host graph, even if the LHS matches at different subgraphs of
the host graph. However, if the rule has parameters, then matches that map the
parameter nodes to distinct host graph nodes will give rise to distinct
applications, with distrinct transition labels.

For the case that one needs distinct rule applications \emph{without} having
the node identity on the transition label, \GROOVE{} offers the concept of an
\emph{anonymous parameter}. This is essentially a parameter without number, in
the editor specified by just the prefix ``\textsf{par:}''. An example is the
following:

\views{anonymousParameter}

This rule, applied to the graph of \eqcite{parameters}, will give rise to two
distinct transitions, both labelled \textsf{anonymousParameter(``a'')}, which
are self-loops on the state since neither rule application changes the graph.

Note that the display view does not show the anonymous parameter at all.

\paragraph{Example usage.}

The use of parameters is demonstrated by the \GROOVE \textsf{parameters}
sample.

\subsection{Nested Rules}
\seclabel{nested}

Nested rules are used to make changes to sets of sub-graphs at the same time,
rather than just at the image of an existentially matched LHS. This is a quite
powerful concept, which has its roots in predicate logic.

\paragraph{Nesting levels}

The specification of nested rules relies on the use of special, auxiliary nodes
that stand for universal or existential quantification. These nodes are part of
the rule and are connected using ``\textsf{in}''-labelled edges. The quantifier
nodes and \textsf{in}-edges must form a \emph{forest}, i.e., a set of trees,
within a rule; in other words, it is not allowed that a quantifier node is
``\textsf{in}'' two distinct other quantifier nodes, or that there is a cycle
of quantifier nodes. Moreover, existential and universal nodes must alternate,
and the root nodes must be universal. In addition, there is always an
\emph{implicit} top-level existential node, with implicit \textsf{in}-edges
from all the explicit (universal) root nodes.

In the Editor view, the quantifier nodes are specified once more using special
prefixes:
\begin{itemize}\noitemsep
\item \textsf{forall:} specificies a universal level: in a match of the entire
  rule, the sub-rule at such a level can be matched arbitrarily often
  (including zero times).
\item \textsf{forallx:} specificies a \emph{non-vacuous} universal level: in a
  match of the entire rule, the sub-rule at such a level must be matched at
  least once.
\item \textsf{exists:} specificies an existential level: in every match of the
  entire rule, the sub-rule at such a level is matched exactly once.
\end{itemize}

The following is an example of a nesting structure (leaving out the actual
rule). 

\views{nesting}
%
The hierarchical structure of nesting levels corresponds to the quantifier
structure of a predicate formula, where the branching stands either for
conjunction (in case of universal levels), or for disjunction (in case of
existentials). In other words, the structure in \eqcite{nesting} roughly
reflects the predicate structure
%
\[ \exists (\forall(\exists\forall^{>0} \vee \exists) \wedge \forall^{>0}) \]
%
Every nesting level, represented by a quantifier node, \emph{contains} a
sub-rule. The containment relation is encoded by ``\textsf{at}''-labelled edges
from \emph{every} node in the sub-rule to the corresponding quantifier node.

As a simple example, Rule~$(a)$ in \eqcite{pick-flower} will result in the
removal of all \textsf{Flower}-labelled nodes of all \textsf{Plant}s of a given
(implicitly existentiall quantified) \textsf{Field}.  Rule~$(b)$ is a slightly
more complicated variant, which picks \emph{exactly one} \textsf{Flower} of
every \textsf{Plant} that \emph{has at least one} \textsf{Flower}.

\begin{equation}\eqlabel{pick-flower}
\begin{array}{ccc}
\tikzbox{pick-all-flowers-display} &
\tikzbox{pick-flower-display} &
\tikzbox{pick-at-least-one-flower-display} \\[\smallskipamount]
(a) & (b) & (c) 
\end{array}
\end{equation}

Yet another variant is given in Rule~$(c)$. Where Rule~$(b)$ is \emph{always}
applicable (as long as there is any \textsf{Field}-node) even if there are no
flowers to be picked, Rule~$(c)$ specifies that there should be \emph{at least
one} \textsf{Plant}-node that can be matched --- meaning that that
\textsf{Plant}-node should have at least one \textsf{Flower}. This means that
if a \textsf{Field} has \textsf{Plant}s but none of them have \textsf{Flower}s,
then Rule~$(b)$ matches, though its application does not change the graph,
whereas Rule~$(c)$ does not match.

Another example is given below. This specifies the rule for firing a transition
in a Place-Transition net. This rule has two independent universal nodes, one
to take care of the removal of tokens from every input place of the transition
to be fired, and one to take care of the addition of tokens to the output
places.

\begin{equation}
\tikzboxview{Petri net firing rule}{petri-net-firing-display}
\end{equation}

Another example of a rule system with nested rules can be found in the
\textsf{copy\_graph} grammar in the \GROOVE{} samples.

\paragraph{Named nesting levels}

Unfortunately, the specification of the sub-rule belonging to a given
quantifier node through special \lab{at}-edges fails if the sub-rule has
isolated edges, since we do not support edges that start at edges. Such an
isolated edge may occur if the end nodes belong to a higher nesting level.

For instance, suppose we want to specify that a girl that all boys like becomes
queen. This rule should be enabled if the following condition holds:

\[ \exists x:\tlab{Girl}(x) \wedge (\forall
y:\tlab{Boy}(y) \Rightarrow \lab{likes}(y,x)) \enspace.
\]
%
This cannot be specified using only \lab{at}-edges. An incorrect solution is
given as (\eqref{crowning}.$a$).

\begin{equation}\eqlabel{crowning}
\begin{array}{ccc}
\tikzboxview{Crowning (incorrect)}{crowning-wrong-display} &
\tikzboxview{Crowning (correct, edit view)}{crowning-right-edit} &
\tikzboxview{Crowning (correct)}{crowning-right-display} \\[\smallskipamount]
(a) & (b) & (c)
\end{array}
\end{equation}
%
The applicability condition in that rule instead corresponds to

\[ \exists x:\tlab{Girl}(x) \wedge (\forall
y:\tlab{Boy}(y) \wedge \lab{likes}(y,x) \Rightarrow \textit{true})
\]
%
meaning that the universally quantified sub-graph is trivially fulfilled.
Instead, the \lab{likes}-edge should be at an existential level \emph{below}
the universal, but there cannot be an \lab{at}-edge starting at the
\lab{likes}-edge.

The solution is to use \emph{named} nesting levels. The name of a nesting level
is given as a kind of parameter in the \lab{exists}- or \lab{forall}-prefix:
namely, the prefix becomes \lab{exists={\itshape name}:} (respectively
\lab{forall={\itshape name}:}), where \textsf{\itshape name} is the
(arbitrarily chosen) name of the nesting level. The edge to be associated with
this label then also needs to specify the name; this is done by adding it to
the prefix that specifies the edge role --- i.e., whether it is a reader
(\useP), eraser (\delP), creator (\newP) or embargo (\notP). The correct
version of the ``crowning'' rule is shown in (\eqref{crowning}.$b$) (edit
view) and (\eqref{crowning}.$c$) (display view).

\paragraph{Counting}


\marginpar{TODO}

\subsection{System Properties}
\seclabel{system-properties}

Apart from the rules, start graph and (optional) control, there are some global
properties of a graph grammar. These are called the system properties. They can
be set in the Simulator or by directly editing
the properties file (see \seccite{io-system-properties}). We discuss the
properties here; an overview is provided in \tabcite{system-properties}.

\begin{table}
\begin{center}
\begin{tabular}{@{}|l|c|l|@{}}
\hline\hline
\bf Property & \bf Default & \bf Meaning \\
\hline
\sf grammarVersion
  & \it version
  & Version under which this grammar was created (non-editable) \\
\sf remark
  & \it empty
  & One-line documentation of the rule system as a whole \\
\sf algebraFamily 
  & \sf default
  & Determines which algebras are used for attributes \\
\sf matchInjective 
  & \sf false
  & Enforces injectivity of matches \\
\sf checkDangling
  & \sf false
  & Makes rules inapplicable in case eraser nodes have dangling edges \\
\sf checkCreatorEdges
  & \sf false
  & Adds implicit edge embargoes for all simple edge creators \\
\sf rhsIsNAC
  & \sf false
  & Adds an implicit NAC for the entire RHS to every rule \\
\sf checkIsomorphism
  & \sf true
  & Ensures states are collapsed modulo isomorphism \\
\sf enableControl 
  & \sf false
  & Indicates that a control program is used to determine rule ordering \\
\sf controlProgram 
  & \sf control
  & Name of the control program (if \lab{enableControl} is set) \\
\sf typeGraph
  & \it empty
  & possible empty list of enabled type graph names \\
\sf controlLabels 
  & \it empty
  & List of graph labels that occur rarely (to speed up matching) \\
\sf commonLabels
  & \it empty
  & List of graph labels that occur frequently (to speed up matching) \\
\sf transitionBrackets
  & \sf false
  & Adds angular brackets around transition labels
  \\
\sf loopsAsLabels
  & \sf false
  & Specifies that self-loop labels are to be displayed on the nodes \\
\sf abstractionLabels
  & \it empty
  & List of node labels considered in abstraction \\
\hline\hline
\end{tabular}
\end{center}
\caption{System properties overview}
\vspace*{-\bigskipamount}
\tablabel{system-properties}
\vspace*{-\medskipamount}
\end{table}

\paragraph{Algebra family.}

This property specifies the algebra to be used when interpreting data
attributes --- see \seccite{attributes}. The currently supported values are:
%
\begin{description}\noitemsep
\item[\textsf{default}] The default algebra, consisting of the Java types
  \textsf{int}, \textsf{double}, \textsf{boolean} and \textsf{String}.
\item[\textsf{point}] A single-point algebra, where each data type has only a
  single value; all constants and operations evaluate to this one value.
\item[\textsf{big}] An algebra where integers have arbitrary precision, and
  real values have a mantissa of 34 digits (to be precise, they follow the
  IEEE 754R Decimal128 format, as implemented by the Java type
  \textsf{BigDecimal}).
\item[\textsf{term}] Term representation.\marginpar{TODO}
\end{description}

\paragraph{Match injectivity.}

As discussed in \seccite{equality}, matches are in general non-injective. By
setting the \textsf{matchInjective} property to \textsf{true}, however,
injectivity is enforced for all rules. In this way, \GROOVE{} can simulate rule
systems originally designed for tools that do impose injectivity always.

\paragraph{Dangling edge check.}

In general, when \GROOVE{} deletes a node, all incoming and outgoing edges are
also deleted, whether or not they were explicitly specified in the rule. This
is in conformance with the so-called \emph{SPO} (\emph{S}ingle
\emph{P}ush\emph{O}ut) approach. In the \emph{DPO} (\emph{D}ouble
\emph{P}ush\emph{O}ut) approach, on the other hand, if a node to be deleted has
an incident edge that is not explicitly deleted as well, then the rule is
considered to be non-applicable. To mimic this behaviour in \GROOVE, the
\textsf{checkDangling} property should be set to \textsf{true}.

\paragraph{Creator edge check.}

In \GROOVE, edges do not have their own identity: if an edge is added to a
graph that alsready has an edge between the same nodes and with the same label,
the graph actually does not change. This can be undesirable in some
circumstances. By setting \textsf{checkCreatorEdges} to \textsf{true}, an
implicit edge embargo is added for all creator edges; now, if an attempt is
made to add an edge that is already there, the rule is inapplicable.

\paragraph{Treating the RHSs as NACs.}

There exist graph transformation applications where a graph is slowly built up
but 
nothing is ever deleted. For instance, this holds in the important area of
\emph{model transformation}. In such circumstances, rules should always only
be applied one single time at every match; however, since nothing is deleted,
the re-application of a rule can only be prevented by adding a NAC. By setting
\textsf{rhsIsNAC} to \textsf{true}, such NACs are implicitly added to all
rules, improving readability and maintainability of the rules.

\paragraph{Isomorphism check.}

One of the strong points of \GROOVE{} is the fact that the graphs that it
generates are compared and collapsed modulo isomorphism --- meaning that there
will be at most graph in the resulting state space for every isomorphism
class. Though this is very effective in many modelling domains, nevertheless
the isomorphism check is expensive. In case a problem being modelled is known
to have little or no symmetries, so that the isomorphism check will always
fail, one can set \textsf{checkIsomorphism} to \textsf{false}, thereby gaining
efficiency.

\paragraph{Control labels and common labels.}

The final pair of properties can be used to optimise the matching process,
thereby improving efficiency.
%
\begin{description}
\item[\textsf{controlLabels}] is a space-separated list of labels that do
  \emph{not} occur frequently in the graph, and whose presence is a good
  indicator for a match at that place. When set, the matching process will
  start at these labels.
\item[\textsf{commonLabels}] is exactly the opposite: it is a space-separated
  list of labels that \emph{do} occur frequently in the graph. When set, the
  matching process will consider these labels last.
\end{description}

\paragraph{Transition parameters.}

The LTS view of the Simulator contains edges for all rule applications that
have been explored. The label display is affected by
\textsf{transitionParameters}, which controls whether transition labels show
the value of rule parameters, if any (see \seccite{parameters}). When set to
\textsf{true}, all labels will show a (possibly empty) list of parameters.

Values: \textsf{false}, \textsf{some} (default), \textsf{true}.\marginpar{TODO}

\paragraph{Displaying loops as node labels.}

The appropriate way to specify a true node label, i.e., a label that can only
occur on a node and not on a binary edge, is by declaring it to be a
\emph{flag} (see above). However, in previous versions of \GROOVE this
distinction was not made and ordinary labels were used as node labels; and
still, for novice users it makes sense to ignore the distinction. The old
behaviour can be set explicitly through the \textsf{loopsAsLabels} property:
when set to \textsf{true}, all self-edge labels will be displayed as node
labels. (Even so, such labels are distinguishable from flags by the fact that
the latter are italic.)

\paragraph{Abstraction.}

The final system property, \textsf{abstractionLabels}, is used to specify the
node labels that are used to parmeterise the abstraction. Since abstraction is
still an experimantal feature, we do not go into this issue here.

\subsection{Beautification}
\seclabel{beauty}
\marginpar{TODO}

\paragraph{Node colouring}

\paragraph{Nodes-as-edges}