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 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 Attributes and options in state space tool.

The full state space report for the Dining philosophers example 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

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.

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

Verification, Attributes and options in state space tool