S N O O P Y - FAQ
latest update: August 03, 2020, at 11:37 AM
Questions
Answers
Q: Why is Snoopy called Snoopy? (^)
A: Snoopy was (is?) the favorite cartoon character of the guys who came up with the first Snoopy implementation around 2000 which is still the core of the code we use today.
Q: How to make Snoopy read a net given in SBML format? (^)
A: File → Import shows you all IMPORT options supported by Snoopy.
Likewise, you have to choose from File → Export if you want to generate SBML out of a Snoopy file.
Having generated the Petri net, you may want to try one of the automatic layout algorithms offered by Edit → Layout.
Q: How to draw a Petri net? (^)
A: To draw your first Petri net, repeat the following steps.
- Create a new net (File → New) and chose the appropriate net class. You get a new drawing window with the name “unnamed“.
- Select the graph element Place in the menu panel on the left-hand side, and make a left mouse click on the drawing window at those positions where you want to get a place. Each mouse click creates a new place.
- Likewise, select the graph element Transition in the menu panel, and create transitions.
- To connect two nodes, select Edge in the menu panel, click on the source node, and move the mouse pointer, while keeping the mouse button pressed, to the target node, where the mouse button is released.
- A double click on a graph element (place, transition, edge) opens an attribute window, which allows to edit the element-specific properties.
- Finally, do not forget to save your work under a new name (File → Save as).
Q: What are logical nodes or macro nodes, and what are they for? (^)
A: In addition to the basic toolkit for drawing Petri nets, Snoopy supports two distinguished features for the design and systematic construction of larger Petri nets.
Logical nodes (also called fusion nodes) with the same name are logically identical, i.e., graphical copies of a single node. They are automatically coloured in grey (or cross-hatched in the colour as assigned by the user). There are two types of logical nodes:
- Logical places - to connect remote net parts by places;
- Logical transitions - to connect remote net parts by transitions;
Logical nodes support the structured design of flat Petri nets, while macro nodes permit the hierarchical structuring of Petri nets. There are two types of macro nodes.
- Macro transitions - are drawn as two centric squares, and should stand for transition-bordered subnets, i.e. subnets having only transitions as interface to the super-net (not checked).
- Macro places - are drawn as two centric circles, and should stand for place-bordered subnets, i.e. subnets having only places as interface to the super-net (not checked).
Logical nodes and macro nodes help to deal with larger networks. They may contribute to a net’s readability and, therefore, are crucial for non-trivial net examples. However, they do not extend the expressiveness of Petri nets as a modelling language.
Q: How to draw a hierarchical Petri net? (^)
A: To hierarchically structure a Petri net, repeat the following steps.
- Draw your flat net (or portion of it) as you wish to have it.
- Select the sub-graph which you want to be abstracted by a macro node, and select Hierarchy → Coarse. Chose the appropriate coarse element and hit the OK button.
- A double click on the macro node opens its attribute window and allows to assign a suitable name, a click on the entry with this name in the hierarchy panel on the left-hand side opens the sub-graph in a separate window. The blue net parts have been automatically generated and represent the connection of the sub-graph (macro node) with the neighbouring nodes on the next higher hierarchy level.
- Finally, do not forget to save your work under a new name (File → Save as).
Q: How to connect nodes in a hierarchical Petri net? (^)
A: To connect a node with an existing node inside a macro node, repeat the following steps.
- Draw the node, if it does not already exist.
- Connect the node with the macro node via an arc. A new node is automatically created inside the macro node.
- Open the macro node and merge the new node with the one you wanted to connect the outside node with. This is done by moving the new node over the old node using the mouse.
- Finally, do not forget to save your work under a new name (File → Save as).
Q: How does a name in Snoopy look like? (^)
A: First of all, all names have to be unique in a net.
But empty names are possible too; if required a name is generated automatically out of the element class name and its ID.
A name can contain any of the following elements:
- letters a-z and A-Z
- digits 0-9
- underscore _
A name has to start with a letter or underscore, possibly followed by any combination of these elements.
In summary, Snoopy adopts the same naming convention as many programming languages.
The uniqueness is needed to correctly identify each entity during analysis and simulation.
Q: What keywords are reserved in Snoopy? (^)
A: There are a couple of keywords in Snoopy, which should never be used, except inside comments. Here is a list of the reserved keywords:
- pn, cpn, hpn, xpn, spn, gspn, xspn,
- bool, int, double, string, enum,
- atan, tan, asin, sin, acos, cos, abs, sqr, sqrt, floor, ceil, log, log10, exp, binomial, d, d2,
- function, DeterministicFiring, Deterministic, ImmediateFiring, Immediate, ScheduledFiring, Scheduled, BioLevelInterpretation, LevelInterpretation, BioMassAction, MassAction,
- max, min, pow, prod, sum.
in alphabetical order:
abs, acos, asin, atan, binomial, BioLevelInterpretation, BioMassAction, bool, ceil, cos, cpn, d, d2, Deterministic, DeterministicFiring, double, enum, exp, floor, function, gspn, hpn, Immediate, ImmediateFiring, int, LevelInterpretation, log, log10, MassAction, max, min, pn, pow, prod, Scheduled, ScheduledFiring, sin, spn, sqr, sqrt, string, sum, tan, xpn, xspn.
If the Petri net is meant to undergo a model checking analysis, then any names of temporal-logical operators (such as A, E, F, G, U) need to be avoided, too.
The keywords are prohibited in any spelling.
Q: How to get my Petri net neat and tidy? (^)
A: There are a couple of features to improve the layout of your net.
- Go to Global Preference, Canvas to set grid spacing and to switch the grid on/off.
- Use Shift + Arrows to move a node on the canvas. The step size of each move is controlled by the grid spacing in the Global Preference dialog.
- Hold down the Ctrl-key (on Linux and Windows) or the Cmd-key (on Mac OSX) and left click on the arc to add intermediate points to an arc.
- Move an intermediate point over another one and it will be deleted.
- Go to Global Preference, Elements to choose between lines and splines, which just changes the style an arc is drawn.
- Go to Edit → Layout to try one of the automatic layout algorithms.
Q: How to play the token game? (^)
A: Petri nets can be animated by playing the token game.
- Open the net, and then open the animate window (View → Animation Mode).
- The animation can be triggered manually by clicking on an enabled transition.
- It can also be done in automatic mode by clicking on the control panel. In each step of the automatic mode, the set of all enabled transitions is determined. There are three strategies to choose the transition(s) to be fired in the next execution step among all enabled transitions.
- Single step – one single transition is randomly chosen.
- Intermediate step – an arbitrary subset of concurrently enabled transitions is randomly chosen.
- Maximal step – a maximal set of concurrently enabled transitions is randomly chosen.
Steps just done can be played backwards up to a depth of 10; this default value can be changed in the Global Preferences dialogue. Each execution exemplifies some possible net behaviour.
Q: How to change the net class of a given Petri net? (^)
A: Snoopy supports various net classes. A Petri net of a given class can be converted into any other Petri net class, possibly requiring several export steps. For example, a qualitative Petri net can be converted into a stochastic Petri net, which allows to re-use the structure. Only the additional attributes have to be set.
- Open the qualitative Petri net, and go to the export Window (File → Export), chose the appropriate target(s) and hit the OK button.
- Open the stochastic Petri net, just generated. It looks exactly the same as the qualitative net.
- Now you are ready to specify the attributes specific for stochastic Petri nets.
Q: What are these special arcs which do exist for extended Petri nets (xPN) and extended stochastic Petri nets (xSPN)? (^)
A: Snoopy supports four types of special arcs (also called edges). They go always from a place p to a transition t and may carry an arc weight k.
- read arc - the transition t is enabled (with respect to p) if p has at least k tokens;
- inhibitory arc - the transition t is enabled (with respect to p) if p has less than k tokens;
- equal arc - the transition t is enabled (with respect to p) if p has exactly k tokens;
- reset arc - the token number on p doesn't matter; but if the transition t fires, any tokens on p are removed;
Read, inhibitory and equal arcs do influence the enabledness of the connected transition, but the token number on the connected place never changes upon firing. On the contrary, a reset arc does not influence the enabledness, but the token number generally changes upon firing (set to zero).
To change the type of an arc go to edit → convert to.
Q: What are modifiers (modifier arcs)? (^)
A: Modifiers are particular arcs, which only exist for stochastic, continuous or hybrid Petri nets. Graphically, they are represented by dashed lines. As special arcs, they go always from a place to a transition. Pre-places connected with a transition by a modifier arc may modify the transition’s firing rate, but do not have an influence on the transition’s enabledness (contrary to special arcs).
Modifiers are also known in SBML; they support the locality principle: only pre-places can be used in a transition's rate function.
Q: Modifiers vs read arcs - when to use which kind of arc? (^)
A: The decision between read arc and modifier should be guided by the fact whether the connected place is a pre-condition for the enabledness of the connected transition. If yes, then read arc is the correct way to model this situation. A modifier should only be used if the transition is allowed to fire even if the marking of the connected place is zero.
The syntax constraint: a transition's rate function can only deploy pre-places of this transition has been introduced to keep a strong relation between structure and behaviour and to prevent hidden dependencies.
To phrase it differently:
Changing read arcs to modifier arcs or vice versa may change the semantics, depending on the rate functions.
- A read arc makes the pre-place to a pre-condition for the enabledness, and thus firing.
- Using modifier arcs, we get the same behaviour only if the connected place is used in the rate function in such a way that its zero value sets the rate to zero (as it is the case, e.g., for mass action kinetics).
Q: What means this predefined function MassAction? (^)
A: MassAction is a macro that creates the rate function for a transition out of its pre-places and takes a parameter as argument.
For example, let's assume t1 has two pre-places p1 and p2, and the parameter k is defined.
Now you can specify the rate function of t1 to obey mass/action kinetics as follows:
- k*p1*p2, or
- MassAction(k).
They compute the same result. MassAction takes care of the structure. If you change the pre-places, the rate function is automatically adapted.
To learn which other functions are supported, open the function assistant when editing transition properties of a quantitative Petri net.
Q: What are these special transitions which exist for stochastic Petri nets? (^)
A: Snoopy supports extended stochastic Petri nets (xSPN). Besides the stochastic transitions, there are deterministically timed transitions, which come in three flavours.
- Deterministic transitions have - contrary to stochastic transitions – a deterministic firing delay which is specified by an integer constant. The delay is always relative to the time point where the transition gets enabled. The transition may lose its enabledness while waiting for the delay to expire. Then, the transition will not fire. This behaviour is also known as the so-called pre-emptive firing rule. As for stochastic transitions, the firing itself of a deterministic transition does not consume time and follows the standard firing rule of qualitative Petri nets.
Deterministic transitions may be useful to reduce networks, and thus speed-up simulations, e.g. by replacing a linear sequence of stochastic transitions by one deterministic transition with the delay set to the expectation value of the sum of the sequence.
- Immediate transitions are a popular special case of deterministic transitions. They have a zero delay and always highest priority. The latter creates a subtle difference between an immediate transition and a deterministic transition with zero firing delay: if there is a conflict between the two, .i.e. a situation, where two transitions compete for tokens, the immediate transition gets priority.
Immediate transitions may help to avoid stiff systems by using them for transitions with extremely high rates (non-significant delay), compared to the other transitions in the system.
- Scheduled transitions are another special case of deterministic transitions. The deterministic firing occurs according to a schedule specifying absolute points of the simulation time. A schedule can specify just a single time point, or equidistant time points within a given interval, triggering the firing once or periodically. However, transitions only fire at their scheduled time points if they are enabled at this time.
Scheduled transitions can dramatically restrict the (qualitative) net behaviour. The crucial point is that they allow to disturb the core model at well-defined time points as it is done experimentally with the actual biological system under investigation in the wet lab.
In most practical cases, extended stochastic Petri nets are the obvious choice. Therefore, Snoopy does not distinguish between stochastic Petri nets (SPN) and extended stochastic Petri nets (xSPN).
Q: How to open the animation or simulation dialogue? (^)
A: If animation is supported, you can open the animation dialog using either:
- select from the menu View → Start Anim-mode
- press function key F5
If simulation is supported, you can open the simulation dialog using either:
- select from the menu View → Start Simulation-mode
- press function key F6
Q: Can I simulate a stochastic Petri net as a continuous one? (^)
A: In Snoopy you can either export SPN into CPN and do the continuous simulation or export it into HPN where you can easily simulate the same net using different simulators
Q: How to choose among the various options for stochastic simulation? (^)
A: Before you start a stochastic simulation experiment, specify the following options.
- A model can be conveniently modified by a couple of sets. If you don't want to use the main sets, then select:
- marking set - used as initial marking,
- function set - by default: all functions are set to mass action kinetics,
- weight set - applies only, if there are immediate transitions.
- delay set - applies only, if there are deterministically delayed transitions.
- schedule set - applies only, if there are scheduled transitions.
- parameter set - applies only, if there are parameters.
- Specify the simulation time of interest:
- interval start - simulation always starts at time point zero; but the the recording of the simulation trace starts with the time point given as interval start.
- interval end - time point for the end of one simulation run, and thus of the recording. This time will not be reached if the simulation encounters a dead state, where the simulation immediately stops.
- Output step count - the number of time points in the specified simulation time interval to be recorded. They define together with the interval start and end values the output grid of the recorded simulation data.
- Number of runs (Simulator → properties → number of runs) - the number of simulation runs done within one experiment. The output shown in the tables or diagrams gives the average values over all runs.
- Number of threads (Simulator → properties → number of thread) - the individual stochastic runs can be done independently. Here one can specify how many threads (parallel processes) shall be used if local hardware (multicore machine) permits.
- Choose how to export the simulation trace(s), if required.
- Direct export - the averaged values of the selected places or transitions is exported according to the specified output grid.
- Single trace export - the result of every simulation run is separately exported according to the specified output grid.
- Exact trace export - like single trace export, but every event is reported; i.e. every change of the marking of the selected places or the transition rates at any time point.
- Hit the Start Simulation button.
Now you might have time for a cup of tea, or two. Note, there is a progress bar giving an estimate of the remaining runtime of the ongoing experiment, and a counter for the total simulation runtime used so far.
Q: How to choose among the various options for continuous simulation? (^)
A: There are many options which are important to set them appropriately in order to do accurate or fast continuous simulation. In general these properties are ODE-solver-dependent.
First to open the option box of the simulation dialog press the properties button in the front of the currently selected simulator type. The properties dialog will be opened. Between the properties that can be adjusted are:
- Visualize in between results: if set true, the simulation results will be redrawn at a regular duration. This might consume some time and in turn will slow down the simulator. However, it has been proved useful to get insight about the simulation results in early stages, particularly for coloured Petri nets.
- Refresh rate: set the elapsed time between redrawn the simulation dialog. If Visualize in between results option is set to be true, the simulation result is redrawn. In both cases simulation statistics (e.g., simulation run time) are updated. The default value is 5000 millisecond. Small values of this option will slow down the simulation.
- Initial step size For variable step size ODE solver, specifying the initial step size will save the ODE solver from approximating a suitable initial step to start with. This will have a big implications on problems with large number of places. If you have no idea about which initial step size to start with, then let the solver to determine it for you (see below).
- Automatically calculate initial step size If set true the solver will calculate the initial step size by itself. Otherwise you have to specify it. See Initial step size option.
- Check for negative values: If the model is not correctly set up, it might produce negative values. Setting this option to true will give you a warning when a negative value is occurred. This will consume extra computations.
- Output noise values: sometimes small negative (hence unphysical) values can occur during the integration of the ODEs. This option can control the output of such values.
- Reduce resulting ODEs: If a place has a transition which is a pre and post transition connected using the same weight, then this option will eliminate the corresponding transition rate from being repeated. Hence will improve the time and quality of the final solution.
- Relative tolerance: is used to control relative errors. The default value is 1.0e-5.
- Absolute tolerance: is used to control absolute errors. The default value is 1.0e-10.
Both of the relative and absolute tolerances are problem-dependent and should be appropriately chosen to get an accurate solution. One idea is to do a few experiments with the tolerances to see how the computed solution values vary as tolerances are reduced.
- Step size: fixed step-size solvers require the specification of the step size. The default value is 0.1.
Q: How to choose among the various options for hybrid simulation? (^)
A: Similar to the continuous and stochastic simulations, the hybrid simulator has some options to permit the adaptation of the general purpose simulation engine to specific needs. Some of these options are equivalence to the ones mentioned in the questions related to the continuous and stochastic simulations. Therefore, we only consider here properties related to the hybrid simulation.
Selecting the synchronization algorithm The synchronization algorithm determines how the stochastic and continuous regimes are interacting with each other. We have four methods to do that:
- static: the simulation engine keeps each transition type as it has been determined by the user.
- dynamic: the simulator decides on the fly which transition should be considered as stochastic and which one as continuous. The algorithm do such partitioning based on the current transition rate values. Note that other transition types (e.g., immediate and deterministic timed transitions are not partitioned).
- continuous: the net is simulated continuously. If there are any stochastic transitions, they are automatically converted to continuous ones
- stochastic: consider the overall network as a stochastic one. If there are some continuous transitions, they will be converted to stochastic ones.
Selecting the ODE solver if you decided to use one of the synchronization algorithms that requires the simulation of continuous transitions (i.e., static, dynamic, or continuous), then the synchronization algorithm requires the specification of an ODE solver. The currently available ODE solvers in the hybrid module are:
- BDF: a multi-step implicit solver
- ADAMS: a multi-step explicit solver
The options of the ODE solver can be adjusted in the same way as in the continuous simulation.
Option of the dynamic synchronization algorithms
- maximum cumulative rate: is the threshold value that the summation of the stochastic transition rates is not allowed to exceed it. If the summation of stochastic rates become above this value, the transitions are repartitioned.
- minimum cumulative rate: is the value that the summation of the stochastic transition rates is not allowed to be below it. If the summation of stochastic rates becomes below this value, the transitions are repartitioned.
- rate and marking thresholds: during the partitioning, each transition rate is checked against the rate threshold and the transition pre and post places are checked against the marking threshold. If the transition rate is below the rate threshold or one of its connected places current marking is below the marking threshold, it will be simulated as a stochastic transition otherwise; it will be simulated as a continuous transition.
- show partitioning information: if this flag is set true, then the partitioning information is displayed in the log each time the partitioning is repeated. This option is useful to debug or understand how the partitioning process progresses. However, it is very time consuming.
Q: What are views and how to manipulate them? (^)
A: What are views for:
views let you to quickly view the simulation results from different perspectives. You can for example create a view to monitor the values of some places, create another view to monitor the values of transition rates, and so on.
There is always one default view. This default view has the name 'main view' and it has default setting for its properties (see below).
For each model, one can define several views. To create a new view do:
- left click the "options..." button
- select new from the pop up menu
- type a name and press OK
Options of the current view:
- Edit: Modify existing view To change the subset of nodes which are currently listed in the selected list, you might need to edit the view. To edit the view do:
- Select edit from "options..."
- a dialog will appear
- add (remove) nodes to (from) the selected list
- press OK
- select the view which you need to remove
- left click the "options..." button
- select remove from the pop up menu
- confirm the warning message
- CSV export: exports the current view to a comma separated value format. To do CSV export do:
- select CSV export from "options..."
- select the separator type (comma, semicolon, or tab)
- select the file name
- press OK
- Image export: exports the current view to an image format. The currently supported formats are: bitmap, gif, png, and jpg. To do this type of export:
- select image export from "options.."
- type the file name
- select the image type
- press OK
- Change X axis: the variable bounded to the x-axis can be change to either the time, a place marking, or a transition rate. To change the x-axis variable do:
- selected change X axis from "the options..."
- select the variable type (time, place, or transition)
- select the variable name (place or a transition name)
- press OK
- Open separately: you can view the simulation result in a separate window. To do that:
- select Open separately from the "option..."
- the current view will be opened in a separate window.
- to disconnect this window from the simulator (i.e., it will not receives update of the result) press disconnect
- to manually refresh the window press refersh
- Open all separately: you also have the chance to open all of the views individually in a separate windows. To do that:
- select "Open all separately" from the "option..."
- all of the currently defined views will be opened in parallel.
Each view is assigned one viewer. which can be changed any time. There are three viewer types:
- tabular viewer:
- xy plot viewer:
- histogram viewer:
See question "How to manipulate a viewer? " for more details.
Q: How to manipulate a viewer? (^)
A: What you can do with a viewer, depends on its type.
tabular viewer: shows the simulation result in a table.
xy plot viewer: shows the simulation result as an xy plot where the x-axis might be the time, a place, or a transition.
histogram viewer: shows the simulation result in a histogram view where the frequencies of node values are shown.
To change the curve color of an xy-plot:
- go to the item list where you check and unchecked the nodes to appear in the view
- double click the item you want to change its color
- a small dialog will appear
- select the curve color, curve width, and/or line style
- press OK
To change a viewer setting:
- select the view that you want to change the setting of its viewer
- in the front of the viewer type select setting
- depending on the viewer type you find a set of attributes organized in tabs
- change the required attribute values
- press OK
To change the view title:
- select setting
- from the general tab change the title field
- press OK
To show hide the legend
- select setting in the front of the viewer
- go to the tab legend
- check (uncheck) the check box "show legend" to show (hide) the legend
To change the legend position
- select setting in the front of the viewer
- go to the tab legend
- select the horizontal and vertical positions from the drop list (left, center, or right)
To show/hide the X-axis label:
- select setting
- in the axis tab check/uncheck "show X axis"
- press OK
To show/hide the Y-axis label:
- select setting
- in the axis tab check/uncheck "show Y axis"
- press OK
To change the X axis label:
- select setting
- in the axis tab change the text in the front of the X-axis title
- press OK
To change the Y axis label:
- select setting
- in the axis tab change the text in the front of the Y-axis title
- press OK
Q: How to connect Snoopy with MC2? (^)
A: Start with exporting simulation traces from Snoopy, which can then be read by MC2.
- For deterministic models, select direct export.
- For stochastic models, select single trace export or exact trace export.
Note, both exports may produce different model checking results. Exact traces contain all events ( but are usually much longer), while single trace export yields traces containing only the states according to the set output grid (and are therefore usually much smaller).
- Then select destination, file name and file type under Properties.
Note you must give the extension to the file (i.e. '.csv').
- Select the separator to be a semicolon.
- Perform the simulation.
- Perform model checking with mc2, using the 'stoch' option and the '-snoopy' final flag, for both deterministic as well as stochastic models, e.g.
java -jar MC2.jar stoch deterministic_trace.csv my_deterministic_properties.queries -snoopy
java -jar MC2.jar stoch stochastic_trace.csv my_stochastic_properties.queries -snoopy
Q: Unfolding or simulation takes ages or causes a Snoopy crash. I get the error message Simulation could not be initialised. What to do? (^)
A: Snoopy seems to have reached its computational limits enforced by the finite resources of your computer.
Memory consumption peaks, caused by
- unfolding
- size of result table (rough estimate: number of variables x output step counter x 8 byte (ie, double value))
may require a 64bit Snoopy/Snoopy steering server. For several reasons, a 64bit Snoopy version is supported so far for linux only.
One can observe the progress of the simulation time in the lower left part of the simulation window. As long as the simulation run time increases, the system didn't run into a loop. But with increasing rates (caused, e.g., by increasing token numbers), the progress will substantially slow down.
Generally, it is a good idea to run expensive simulations on a separate powerful machine (so far at best on a native linux installation, ie, no VM), at best exploiting Snoopy's steering server and having nothing else to do than doing the simulations. So far, there is no official release of the steering server, but it is available on request.
Q: Does Snoopy support the Systems Biology Markup Language (SBML)? (^)
A: Snoopy supports SBML Level 2 Version 4 by incorporating LibSBML.
It imports any SBML document which is compatible to Level 2 Version 4. If a conversion is needed, it is done by LibSBML automatically, if possible.
Snoopy is able to export SBML Level 2 Version 4 as well as Level 1 Version 2. The user can choose this in the export dialog (Level 2 is the default).
Q: Snoopy doesn't like my colored expressions anymore? (^)
A: There is a new feature in Mac OSX 10.9+ called "smart quotes and dashes". It's enabled by default and replaces double quotes and single quotes with fancier looking characters. But this behavior contradicts with some parts of Snoopy.
Our advice for you: Disable "smart quotes and dashes"!
You find an how-to here.
Q: When using coloured Petri nets, what is the difference between the different unfolding algorithms one can chose from? (^)
A: Right now, Snoopy provides four different ways to perform the unfolding, which are given in inverse chronological order.
(1) 'Generic (intern)' is kind of hand-made, but applies some patterns described in [LHY12]; the software code is built-in (intern).
Gecode is a constraint solver package (see http://www.gecode.org), and the following two unfoldings convert the unfolding problem into a constraint problem in the syntax of the Gecode package, which is then called. (2) 'Gecode (intern)' does the convertion by built-in code, while (3) 'Gecode (dssz_util)' uses the library 'dssz_util' (a bundle of algorithms repeatedly used in our toolsuite).
Finally, (4) 'IDD (dssz_util)' uses interval decision diagrams (IDD) (instead of Gecode) to solve the unfolding problem.
Theoretically, all four algorithms should yield the same results, but in practice there are differences, caused by the development history, which we were not able to resolve so far due to limited working power. If you encounter reproducible problems, please report them to us (provide the Petri net in Snoopy syntax and a description of the steps to reproduce the bug.)