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 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.
The full state space report for the Dining Philosophers example CPN looks like this:
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 Markings: All
Dead Markings: None
Dead Transitions Instances: None
Live Transitions Instances: All
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.