Today I got a question about simulating a sequence of named transitions in CPN Tools. While this is not immediately possible, it can be done using Access/CPN, which has a Java component (featured here ) and a SML component, which is leading a much more secret life as the underpinning of ASAP.
Access/CPN is described in the papers [bibtex file=workshops.bib,tools.bib key=accesscpn,siminterface]
The idea is to use Access/CPN to execute the transitions and then force the GUI to update itself after the fact. The SML component of Access/CPN is instantiated using the Enter State-space tool of CPN Tools. Starting with version 3.2, CPN Tools has an extra option which loads the ASAP tool instead of the old one in CPN Tools. See more about ASAP in CPN Tools here.
Now, we have access to the structures Bind and ASAP.CPNToolsModel (and a couple others as well, but let’s not worry about those here).
Let us consider the model below:
Let’s assume that we want to perform some setup, so we need to execute first a with n = 1 and then b (also with n = 1). To do that, we can use the executeSequernce function of ASAP.CPNToolsModel. The function has interface:
executeSequence: state * event list -> (state * event list) list
Thus, we need to give a source state and a list of events to execute. The result is a set (list) of states and enabled events, namely the result of executing the event sequence (which we ignore). We can use the function
getInitialStates: unit -> (state * event list) list
to get the initial state (the interface allows multiple initial states to handle non-deterministic models, but the function always returns exactly one for CPN models).
The Bind structure contains a type event which is a union of a value for all transitions in the model. Transitions are described using two values, an integer indicating the instance number (the number shown next to the page name or 1 if none is shown) and the binding of all variables.
We thus devise the code:
[raw] letopen Bind ASAP.CPNToolsModel
val [(s, _)] = getInitialStates()
val r = executeSequence (s, [Top’a (1, { n = 1 }), Top’b (1, { n = 1 })])
in
CPN’Sim.reset_scheduler()
end
[/raw]
We first open the structures we need (l. 2) and obtain the initial state using pattern matching to only get the actual state descriptor (l. 3). We then execute the desired sequence of events. Here, we execute transition a on instance 1 of the page Top in the binding n = 1, then the transition b on the same page in the same binding. In line 6 we reset the scheduler. We need to do this as we are executing transitions without using the scheduler. Read more about the scheduler in a separate post.
Now we are nearly done: CPN Tools has actually executed the events, but the GUI does not reflect this. To reset the GUI, we need to fast forward (at least) one step. This may execute any transition, however, so we use a trick to ensure that a particular transition without importance is executed. The construction is shown below:
The idea is that the low-priority transition will never be executed until no other transitions are enabled and the high-priority transition will be executed before all others. The trick is that using Access/CPN to execute transitions allows us to execute the low-priority transition even though it is not enabled (it is only pre-enabled). See more about priorities in [bibtex file=workshops.bib key=priority]
Combining it all yields this model:
You can also get the model as a model for CPN Tools here. Note that we have added the low-priority transition at the end of the list of transitions to execute. The model is used by loading it in CPN Tools. Then the ASAP option is switched on for the Enter State Space tool and the tool is used on the model. Entering the ASAP tool instead of the old one normally used in CPN Tools is significantly faster. Now, the auxiliary text is executed using Evaluate ML. Finally, we Fast Forward, making sure to set the number of steps to skip ahead to 1 beforehand if it isn’t already set to that. The model is now in a state, where A contains 12 and C contains 11 and the other places are empty.
The constructions used are completely generic, which is why they may seem a bit complicated. The priority construction does not introduce new behavior (as long as we ensure that the priorities are indeed lower than/higher than all other used priorities). Dead-locks are preserved and (I’m fairly certain but haven’t bothered to prove) so are LTL properties.
