The keys and settings of the exploration configuration vocabulary, and the legacy strategy and acceptor keywords

This page is generated from the GROOVE 7.6.0 source code by manual/make-refs.sh; do not edit it by hand.

The keys and settings below constitute the vocabulary of the Generator’s -x option, of the exploration dialog in the Simulator and of the exploration grammar property (see the Exploration and verification chapter). The textual form of a configuration is a space-separated list of key=setting entries; a key that is absent takes its default.

Keys

Key Default Description
next oldest Selection of the next state to be explored
successor all Selection of the successor states to be generated
frontier complete Size restriction on the exploration frontier
heuristic none Quality function guiding the selection of the next state
cost none Cost of a single transition
goal final Condition determining when a result has been found
outcome satisfy Whether the goal condition is to be satisfied or violated
shape state Shape of the results the exploration yields
count all Number of results after which exploration halts
bound none Bound on the states to be explored
persistence all Degree to which discovered states are stored in the GTS
collapse grammar Condition under which a fresh state is considered equal to a known state
algebra grammar Interpretation of data values
seed auto Master random seed governing the randomised features

Settings

The settings per key; the default is marked with an asterisk. In the setting forms, n stands for a number, max[+inc] for a maximum with an optional increment for iterative deepening, and text for a name or formula as explained in the description.

Key Setting Description
next oldest* The oldest state in the frontier is explored next (breadth-first search)
  newest The newest state in the frontier is explored next (depth-first search)
  random A random state in the frontier is explored next
successor all* All unexplored successor states are generated, in their natural order
  all-random All unexplored successor states are generated, in random order
  single Only the first unexplored successor state is generated
  single-random Only a single, randomly chosen unexplored successor state is generated
frontier complete* No states are dropped from the frontier
  single The frontier holds a single state, giving rise to a linear search
  n or beam:n The frontier is restricted to a given maximum size (beam search)
heuristic none* No heuristic is used; all states have the same quality
  nen Count of node/edge/node tuples missing with respect to the goal (requires the goal to be a complete graph or unnested, NAC-free rule)
cost none* Transitions have no cost; the cost of a path is ignored
  uniform Every transition has cost 1, so the cost of a path equals its length
  rule Each rule application has a cost, fixed per rule or exposed as a rule parameter
goal none There is no goal; exploration continues until the frontier is empty
  any Every state is a result
  final* A state without outgoing transitions
  graph:text A state whose graph is isomorphic to the named graph
  condition:text A state whose graph satisfies a propositional condition over rule names (regardless of whether the rules are scheduled)
  fires:text A state in which the named action (a rule or recipe) fires, as scheduled
  ltl:text A trace satisfying an LTL formula
  ctl:text A state space satisfying a CTL formula
outcome satisfy* A result satisfies the goal condition
  violate A result violates the goal condition
shape state* A result is a state
  trace A result is a trace from the start state to a goal state
count all* Exploration continues until the entire state space has been explored
  first Exploration stops as soon as a single result has been found
  n or value:n Exploration stops as soon as the given number of results has been found
bound none* There is no bound; the state space is explored up to arbitrary depth
  initial Only the initial state is explored, and no further states are
  cost:max[+inc] States are bounded by the cost of the path leading to them
  size:max[+inc] States are bounded by the total number of their graph elements
  nodes:max[+inc] States are bounded by their number of nodes
  edges:text States are bounded by their number of edges of given types (a comma-separated list of label>bound pairs; labels may carry a type: or flag: prefix)
  upto:text States satisfying the named rule condition (negated if prefixed with ‘!’) are not explored
  include:text States satisfying the named rule condition (negated if prefixed with ‘!’) are the last to be explored
persistence all* All discovered states are stored in the GTS
  none No states are stored in the GTS
collapse grammar* As determined by the grammar property ‘checkIsomorphism’
  equality Graphs are compared for equality (the strongest condition)
  isomorphism Graphs are compared up to isomorphism
  hash Graphs are considered equivalent if their isomorphism hash codes coincide (may collapse non-isomorphic states)
algebra grammar* As determined by the grammar property ‘algebraFamily’
  default Java-based representation of data values
  big Arbitrary-precision representation of data values
  point All data values are collapsed to a single point
  term Data values are represented symbolically, as terms
seed auto* The master seed is left as it is: the -seed option or the groove.randomSeed system property if given, a freshly generated (and reported) seed otherwise
  n or value:n The given value becomes the master seed for the rest of the session, making the randomised features of this and subsequent explorations reproducible

Legacy strategies and acceptors

Up to release 7.5.3, an exploration was given by a named strategy and acceptor: the keywords of the Generator’s -s and -a options (still accepted as legacy shorthand) and of the explorationStrategy grammar property. Each combination maps onto a configuration, except for the LTL model checking strategies, which are not configuration-based. The table lists every keyword with an example of a legacy strategy acceptor pair and the configuration it translates to.

Legacy keyword Example Equivalent configuration
bfs bfs final (the default configuration)
bfs:n bfs:5 final cost=uniform bound=cost:5
dfs dfs final next=newest
dfs:n dfs:5 final next=newest cost=uniform bound=cost:5
linear linear final successor=single frontier=single
random random final successor=single-random frontier=single
state state final bound=initial
crule:[!]rule crule:done final bound=upto:done
cnbound:n cnbound:20 final bound=nodes:20
cebound:label>n,… cebound:item>3,flag:busy>1 final bound=edges:item>3,flag:busy>1
uptorule:(bfs|dfs)->[!]rule uptorule:dfs->done final next=newest bound=upto:done
uptorule:(bfs|dfs)=>[!]rule uptorule:bfs=>!done final bound=include:!done
ltl:formula ltl:G(!error) cycle ltl:G(!error) (not configuration-based: Nested Depth-First Search for a given LTL formula.)
ltlbounded:bound;formula ltlbounded:10,5;G(!error) cycle ltlbounded:10,5;G(!error) (not configuration-based: Nested Depth-First Search for a given LTL formula, using incremental bounds based on graph size or rule applications)
ltlpocket:bound;formula ltlpocket:grow;G(!error) cycle ltlpocket:grow;G(!error) (not configuration-based: Nested Depth-First Search for a given LTL formula, using incremental bounds based on graph size or rule applications and optimised to avoid reexploring connected components (‘pockets’))
final bfs final (the default configuration)
any bfs any goal=any
none bfs none goal=none
cycle ltl:G(!error) cycle ltl:G(!error) (not configuration-based: Nested Depth-First Search for a given LTL formula.)
ruleapp:rule bfs ruleapp:done goal=fires:done
inv:rule bfs inv:error goal=condition:error
inv:!rule bfs inv:!safe goal=condition:!safe
formula:formula bfs formula:done&&!error goal=condition:done&&!error