Saving a standard state space report

After you have calculated a state space, and optionally the SCC graph, it is possible to save a standard state space report with the calculations. To save a report, apply the

Save state space report

Save state space report tool to a sheet containing a page from the net.

A save dialog box will appear. Specify the location and name of the report file you want to create.

The contents of the report are determined by the options for the Save state space report tool.

The textual format of place and transition names in a report can be changed by setting the string representation options. To set these options, you must change attributes and options.

Example

The full state space report for the Dining Philosophers example CPN looks like this:

Statistics
————————————————————————
Occurrence Graph
Nodes: 11
Arcs: 30
Secs: 0
Status: Full

Scc Graph
Nodes: 1
Arcs: 0
Secs: 0

Boundedness Properties
————————————————————————
Best Integers Bounds Upper Lower
Page’Eat 1 2 0
Page’Think 1 5 3
Page’Unused 1 5 1

Best Upper Multi-set Bounds
Page’Eat 1 1`ph(1)++1`ph(2)++1`ph(3)++1`ph(4)++1`ph(5)
Page’Think 1 1`ph(1)++1`ph(2)++1`ph(3)++1`ph(4)++1`ph(5)
Page’Unused 1 1`cs(1)++1`cs(2)++1`cs(3)++1`cs(4)++1`cs(5)

Best Lower Multi-set Bounds
Page’Eat 1 empty
Page’Think 1 empty
Page’Unused 1 empty

Home Properties
————————————————————————
Home Markings: All

Liveness Properties
————————————————————————
Dead Markings: None
Dead Transitions Instances: None

Live Transitions Instances: All

Fairness Properties
————————————————————————
Page’Put 1 Impartial
Page’Take 1 Impartial

Error if SCC graph not calculated

Tool options for the Save state space report tool determine whether home, live transition instances, and fairness properties should be included in a state space report. These properties can be calculated only if the SCC graph has been calculated.

If these properties should be included in the state space report and the SCC graph has not been calculated, then an SccGraphNotCalculated exception will be raised after the Save state space report tool has been applied.

Error if SCC graph has not been calculated

To solve the problem, calculate the SCC graph, and then apply the Save state space report tool again.

Related pages

Verification, Attributes and options in state space tool