data structures and software dependability

• home

• contact

• members

• teaching

• research

• publications

• software

• events

PetriNuts Software tools

latest update: August 27, 2021, at 10:00 AM

All tools of our platform are freely available for non-commercial use.

However, we assume the self-evident rule of scientific honesty that credits are explicitly given in any publication or research project to all our tools, which have been used while pursuing them.

We are happy to receive your information to update our bibliography.

• Snoopy - hierarchical Petri net editor, animator and simulator
• Patty - web-based Petri net animation, see sampler;
• Charlie - analysis of Petri net models by standard Petri net theory
• Marcie - model checker for generalized stochastic Petri nets (former IDDMC)
• Spike - command line tool for stochastic, continuous & hybrid simulation of (coloured) Petri nets
• MC2 - command line tool for simulative model checking using PLTLc

First steps using our PetriNuts platform

1. Download and install Snoopy, Charlie, Marcie, Spike, and MC2.
2. Start modelling your net with Snoopy.
3. Guidelines for using Snoopy can be found here.
4. Use Snoopy's built-in animation/simulation for first insights.
5. For further analysis of your net export it to ANDL or CANDL (if coloured).
6. Use Charlie for structural properties, invariant based analysis, STP and reachability graph based analysis.
7. Use Marcie for qualitative and quantitative analysis of Generalized Stochastic Petri nets with extended arcs.
8. Use MC2 to model checking stochastic, deterministic or hybrid simulation traces.
9. Use Spike to set up simulation experiments with varying model and/or simulation parameters.

Former projects (no further development)

• PED - our former hierarchical Petri net editor, inspired many Snoopy features
• PInA - a tool for computation and analysis of invariants in Petri nets, with some influence on Charlie
• BDD Model Checking Tools - our former BDD based model checking tools, now incorporated in Marcie

Snoopy & Charlie were used in the iGEM project , aiding in the process of formalising the original biologists' models.