Petruchio

Overview

Entry last updated: 2010/9/3
Entry last validated: 2010/9/3

Tool homepage: http://petruchio.informatik.uni-oldenburg.de/

Tool availability: Free of charge

Tool Features

Petri Nets Supported (see also help on terminology)

High-level Petri Nets
Place/Transition Nets
Stochastic Petri Nets
Petri Nets with Time
Transfer Petri Nets

Components (see also help on terminology)

Graphical Editor
Token Game Animation
Fast Simulation
State Spaces
Place Invariants
Net Reductions
Simple Performance Analysis
Interchange File Format

Environments

Sun, SunOS
HP, HP-UX
PC, Linux
PC, MS Windows 95
PC, MS Windows 98
PC, MS Windows NT
PC, MS Windows 2000
PC, MS Windows XP
Macintosh, Mac OS
Macintosh, Mac OS X
Java

Tool Description

Petruchio is a tool for computing Petri net translations of dynamic networks modeled in terms of Pi-calculus processes. It provides means to further analyse (the resulting) nets.

It consists of a rich (graphical) frontend with model-checker integration and several command-line backend tools which allow for fast simulation of (high-level) GSPN, checking coverability for low-level (transfer) Petri nets, and application of reduction techniques for low-level Petri nets.

Several (low-level) Petri net formats are supported.

See Other Remarks for further details.

Contact Information

Tim Strazny
Carl von Ossietzky University Oldenburg
Ammerlaender Heerstrasse 114-118
D-26129 Oldenburg
Germany

Phone:  +49-441-798-2362
Fax:    +49-441-798-2965
E-mail: tim.strazny@informatik.uni-oldenburg.de

Other Remarks

Petruchio Backend

Command-line tools
Fast computation of (structural) Petri net semantics of Pi-calculus processes
Fast (backward) coverability checker for low-level (transfer) Petri nets
Several reduction techniques implemented (pre-/post-agglomeration, ...)
Reads and writes many low-level Petri net formats (pnml, ll_net, spec, lola, ina, ...)
Fast (non-visual) simulation of (high-level) generalized stochastic Petri nets
Simulation based statistical analysis

Petruchio IDE

Rich Eclipse based GUI
Integrates Petruchio Backend
Low-level Petri net editor with simulation capabilities
Model-checker integration (MCKit, ...)
Counter-example visualization
Interpretation of Petri net markings as Pi-calculus processes
Editor for Pi-calculus processes with syntax highlighting
Display connection structure of Pi-calculus processes

The maintainers of this page