ASAP

Since version 3.0 of CPN Tools, the state space tool of ASAP has secretly been part of CPN Tools. It is not exposed in the GUI, however, and lacks support for some features of CPN Tools.

Limitations

Current limitations of ASAP in CPN Tools are

  1. No support for priorities
  2. No support for time
  3. Error reporting is very lacking

Using ASAP in CPN Tools

To use the ASAP tool from within CPN Tools starting from 3.2, simply open the options of the Enter state space tool and switch on ASAP. Then enter the state space tool for your model. ASAP is a bit stricter about naming than the old state space tool, so all places, transitions, pages, and substitution transitions should have unique names.

You now have a structure “ASAP” available. It contains a structure CPNToolsModel and two hash functions. You furthermore have structures “Mark” and “Event”. You can use these with the structures in ASAP. For example, to check a safety property using BFS and storing all states in a hash-table 

open ASAP

structure HashStorage = HashStorage (
structure Hash = CPNToolsHashFunction
structure Model = CPNToolsModel
)

structure HashExplorationBFS = WaitingSetExploration (
structure Model = CPNToolsModel
structure Storage = HashStorage
structure WaitingSet = FifoQueue
)

structure SafetyChecker = SafetyChecker(
structure Exploration = SimpleTraceExploration(
structure Exploration = HashExplorationBFS
)
)

SafetyChecker.explore true 10 (HashStorage.emptyStorage { init_size = 1000 } ())
(CPNToolsModel.getInitialStates()) (op::) (fn (_, []) => false | _ => true)