The Occurrence Graph Tool

The Occurrence Graph tool allows the user to construct and analyse occurrence graphs of hierarchical CP-nets - with or without time. An occurrence graph is a directed graph with a node for each reachable marking and an arc for each occurring binding element. Occurrence graphs are also known as state spaces, reachability graphs or reachability trees. With the present version of the Occurrence Graph tool, we have constructed occurrence graphs with more than one hundred thousand nodes and more than one million arcs. Below you can find a presentation of some of the most important facilities in the Occurrence Graph tool. The description is taken from Chapter 3 of Overview of Design/CPN:

Integration with the CPN Simulator
Construction of Occurrence Graphs
Standard Report
Standard Queries
Customised Queries
Temporal Logic
Occurrence Graphs with Equivalence Classes
Strongly Connected Components
Graphical Display of Occurrence Graphs

Integration with the CPN Simulator

The Occurrence Graph tool is closely integrated with the CPN simulator. By a single command it is possible to "move" a marking from the Occurrence Graph tool to the simulator. This is very useful, since it allows the user to inspect the marking directly on the graphical representation of the CP-net. It is possible to see the enabled transition instances, investigate their bindings and make simulations. It is also possible to "move" a marking from the simulator to the Occurrence Graph tool - where it becomes a node.

It is possible to make an occurrence graph for part of a large model. This is done in exactly the same way as in the CPN simulator, i.e., in Mode Attributes (by means of Prime Page and Do Not Include in Simulation).

Occurrence graphs can be constructed with or without time and with or without code segments. Code segments should, however, be used with care. If they have side effects which must be executed in a particular order, it makes no sense to construct an occurrence graph (because this will execute the code segments in a wrong order).

Construction of Occurrence Graphs

The construction of the occurrence graphs is totally automatic, and the user can specify whether he wants the entire occurrence graph to be calculated or only a part of it. This is done by means of stop and branching criteria.

The stop criteria tell us how large the constructed graph should be. As an example, it is possible to specify that the construction should finish when a certain amount of real time has been used or when a certain number of nodes have been constructed. It is also possible to specify an Standard ML function with a more complex stop criteria, e.g., telling that the construction should stop if a dead marking is encountered.

The branching criteria imply that it is possible only to develop some of the immediate successors of a given marking. As an example, the user may specify that he wants the construction to investigate at most two binding elements (for each enabled transition instance).

When a partial graph has been constructed, by using a set of stop criteria or a set of branching criteria, it is later possible to continue the construction (with or without stop and branching criteria).

Standard Report

When an occurrence graph has been constructed it can be analysed in different ways. The easiest approach is to use the Save Report command to generate a standard report providing information about all standard CPN properties:
  • Statistics (size of occurrence graph and Scc-graph (see below)).
  • Boundedness Properties (integer and multi-set bounds for place instances).
  • Home Properties (home markings).
  • Liveness Properties (dead markings, dead/live transition instances).
  • Fairness Properties (impartial/fair/just transition instances).
The command invokes a dialogue box allowing the user to specify the kind of information which he wants to obtain. This is done by choosing one or more of the possibilities mentioned above.

Standard Queries

To investigate the CP-net in more detail, the Occurrence Graph tool has a large number of query functions, i.e., Standard ML functions providing information about the behavioural properties of specified place instances, transition instances and markings. Below we give some examples of query functions. Each of them is executed in a few seconds (even for large occurrence graph).
  • Reachable determines whether there exists an occurrence sequence between two specified markings.
  • AllReachable determines whether all the reachable markings are reachable from each other.
  • UpperInteger calculates the maximal number of tokens at a specified place instance.
  • UpperMultiSet calculates the upper multi-set bound of a specified place instance (i.e., the smallest multi-set which is larger than all the markings of the place instance).
  • LowerInteger calculates the minimal number of tokens at a specified place instance.
  • LowerMultiSet calculates the lower multi-set bound of a specified place instance (i.e., the largest multi-set which is smaller than all the markings of the place instance).
  • HomeMarkingExists determines whether the CP-net has any home markings.
  • HomeMarking determines whether a specified marking is a home marking, i.e., whether it can be reached from all reachable markings.
  • InitialHomeMarking determines whether the initial marking is a home marking.
  • ListHomeMarkings returns a list with all those markings that are home markings.
  • HomeSpace determines whether a specified set of markings is a home space, i.e., whether, from each reachable marking, it is possible to reach at least one of the specified markings.
  • MinimalHomeSpace returns the minimal number of markings which is needed to form a home space.
  • DeadMarking determines whether a specified marking is dead, i.e., has no enabled binding elements.
  • ListDeadMarkings returns a list with all those markings that are dead.
  • TIsDead determines whether a specified set of transition instances is dead in a specified marking.
  • BEsDead determines whether a specified set of binding elements is dead in a specified marking.
  • ListDeadTIs returns a list with all those transition instances that are dead.
  • TIsLive determines whether a specified set of transition instances is live.
  • BEsLive determines whether a specified set of binding elements is live.
  • ListLiveTIs returns a list with all those transition instances that are live.
  • TIsFairness determines whether a specified set of transition instances is impartial, fair or just.
  • BEsFairness determines whether a specified set of binding elements is impartial, fair or just.
  • ListImpartialTIs returns a list with all those transition instances that are impartial.
  • ListFairTIs returns a list with all those transition instances that are fair.
  • ListJustTIs returns a list with all those transition instances that are just.

Customised Queries

In addition to the standard queries, it is also possible to make special-purpose queries - testing properties that are particular to the CP-net in question. For this purpose the Occurrence Graph tool has a function called SearchNodes. It takes six arguments:
  • The first argument specifies the search area, i.e., the part of the graph which should be searched. This can, e.g., be the entire graph or a strongly connected component (see below).
  • The second argument specifies the predicate function. It maps each node into a boolean value. Those nodes which evaluate to false are ignored; the others take part in the further analysis.
  • The third argument specifies the search limit. It is an integer, and it tells us how many times the predicate function must be true before we terminate the search.
  • The fourth argument specifies the evaluation function. It maps each node into a value, of some type A. The evaluation function is used to identify those nodes (of the search area) for which the predicate function is true.
  • The fifth argument specifies the start value. It is a constant, of some type B.
  • The sixth argument specifies the combination function. It maps from A x B into B, and it describes how the individual results (obtained by the evaluation function) is combined to yield the final result.
It should be noticed that the predicate function, the evaluation function and the combination function are all written by the user. This means that they can be arbitrarily complex.

In addition to SearchNodes there is a function called SearchArcs. It takes the same six arguments, and it works in a similar way - except that it searches arcs, instead of nodes. The search functions may seem a bit complicated. However, they are also extremely general and powerful. This is illustrated by the fact that all the standard queries mentioned above are implemented by means of the search functions. This typically takes 2-5 lines of Standard ML code.

Temporal Logic

Queries can also be made by means of a CTL-like temporal logic. This is provided via a Standard ML library. It is possible to formulate queries about states, but also queries about state changes (e.g., the occurrence of certain transitions). For more details see the Design/CPN Libraries.

Occurrence Graphs with Equivalence Classes

It is possible to construct and analyse occurrence graphs with equivalence classes, i.e., graphs where each node represents a class of closely related system states while each arc represents a class of related state changes. Occurrence graphs with equivalence classes are often much smaller than the corresponding ordinary occurrence graphs. Nevertheless they contain the same information and can be used to answer the same kinds of queries. For more details see the Design/CPN Libraries.

Strongly Connected Components

A strongly connected component (of a directed graph) is a maximal subgraph in which all nodes are reachable from each other. The strongly connected components (SCCs) are pairwise disjoint. For each occurrence graph Design/CPN calculates an SCC graph, i.e., a graph with a node for each strongly component and an arc for each occurrence graph arc starting in one component and ending in another.

For cyclic CP-nets we usually have an SCC-graph which is much smaller than the occurrence graph. Often there is only one SCC or a few - while the occurrence graph may have many thousand nodes. By means of the SCC graph a number of behavioural properties can be investigated in a very efficient way - because the SCC graph is small. As an example we can determine whether there are home markings or not by counting the number of terminal SCCs. We can also determine whether a transition instance is live. This is done by checking whether it appears in each terminal SCC.

Graphical Display of Occurrence Graphs

The constructed occurrence graphs are usually large. Hence, it is useless to draw the entire graph. However, it often makes sense to display selected parts of it, e.g., the nearest surroundings of some interesting nodes/arcs - found via queries.

The user specifies the nodes and arcs which he wants the tool to display. This can be done by explicitly listing the desired nodes/arcs. It can also be done by asking for the successors or predecessors of some already displayed nodes. The new nodes are drawn with a default position and with default attributes. The objects of the occurrence graph are ordinary graphical objects, and this means that the user can change the attributes. Usually, he will modify the positions as he adds new nodes - to get a nice layout without too many crossing arcs.

The user determines the text strings to be displayed for the individual nodes and arcs. This is done by specifying two Standard ML functions. One of these maps from nodes into text strings, while the other maps from arcs into text strings. Usually, the first function gives a condensed representation of the marking (of the node), while the second gives a condensed representation of the binding element (of the arc). Each text string is displayed in a region of the corresponding node/arc, and the region can be made visible/invisible by double clicking the node/arc.

Last modified: Tue Jun 4 10:32:59 1996 -- Design/CPN Online admin
http://www.daimi.au.dk/designCPN/over/occ.html