S N O O P Y ' s home page
latest update: July 20, 2010
Please use the following reference to give credits to Snoopy:
C Rohr, W Marwan, M Heiner:
Snoopy - a unifying Petri net framework to investigate biomolecular networks;
Bioinformatics 2010 26(7): 974-975.
Index:
general description
news
related papers
case studies
downloads
related software (import / export)
bug reports
mailing list
G e n e r a l D e s c
r i p t i o n
Snoopy is a software tool to design and animate hierarchical graphs,
among others Petri
nets. The tool has been developed - and is still under
development - at the
University of Technology in Cottbus, Dep. of Computer Science,
"Data Structures and Software Dependability".
The tool is in use for the verification of technical systems,
especially software-based systems, as well as for the validation of
natural systems, i.e. biochemcial networks as metabolic, signal
transduction, gene regulatory networks, compare [poster "overview
on the research activities of our working group"].
Basic Properties
- extensible
- generic design facilitates add on of new graph types
- adaptive
- simultaneous use of several graph types
- GUI adopts dynamically to graph type in active window
- platform independent
- implementation: C++, wxWidgets, Xerces
- supported for Windows, Mac OS X and Linux
Main Features
- hierarchies by subgraphs
- logical (fusion) nodes
- different shapes for net elements
- colouring of graph elements (e.g. paths or invariants)
- automated layout by Graphviz library
- digital signature by md5 hash function
- animation of place/transition Petri nets
- simulation of stochastic/continuous Petri nets
- printing support: eps, Xfig, FrameMaker
- import/export from/to analysis tools, see
related software
- SBML import/export (rules, events, functions not supported)
- support of web-based Petri net animation, see
sampler
Available Graph Classes
- place/transition Petri net
- extended Petri net (read / inhibitor / reset arcs)
- time(d) Petri net
- generalized stochastic Petri net
- continuous Petri net
- modulo Petri net
- "music" Petri net
- reachability graph
- MTBDD/MTIDD
- fault tree
- extended fault tree
- freestyle net
- EDL signature net
- < your favourite graph class ? >
Upcoming
- coloured Petri net
- PNML support
- import of biochemical network models in the KEGG data
formats
- managing and executing animation sequences (e.g. counter examples
produced by external analysis tools)
R e l a t e d P a p e r s
Some Technical and Academic Case Studies
- control software of a production cell:
M. Heiner, P. Deussen, and J. Spranger. A Case Study in Design and
Verification of Manufacturing Systems with Hierarchical Petri Nets.
Journal of Advanced Manufacturing Technology,
15:139-152, 1999.
- concurrent pusher:
M. Heiner. Verification and Optimization of Control Programs by Petri
Nets without State Explosion. In Proc. 2nd Int. Workshop on
Manufacturing and Petri Nets at Int. Conf. on Application and Theory of
Petri Nets (ICATPN �97 Toulouse), pages
69-84, 1997
- solitaire game:
P. H. Starke. Halma net. Petri Net Newsletter,
28:3-8, 1987.
Some Biological Case Studies
- qualitative models of signal transduction networks
- Apoptosis:
M. Heiner, I. Koch, and J. Will. Model Validation of Biological
Pathways Using Petri Nets - Demonstrated for Apoptosis. BioSystems,
75:15-28, 2004.
- Haemorrhage:
G. Neumann. Modeling of Biochemical Processes with Petri Nets;
Hemostasis vs. Fibrinolysis vs. Inhibitors (in German).
Master's thesis, Brandenburg University of
Technology Cottbus, Computer Science Dept., 2004.
- qualitative models of metabolic networks
- Glycolysis and Pentose Phosphate pathway (G/PPP):
I Koch, M Heiner: Petri Nets;
in BH Junker, F Schreiber (eds.): Biological
Network Analysis,
Wiley Book Series on Bioinformatics (Series
Eds. Yi Pan, Albert Y. Zomaya), Chapter 7, pp. 139 - 179, 2008.
- Potato tuber:
I. Koch, B. H. Junker, and M. Heiner. Application of Petri Net Theory
for Modeling and Validation of the Sucrose Breakdown Pathway in the
Potato Tuber. Bioinformatics, 21(7):1219-1226,
2005.
- Glycolysis and Pentose Phosphate pathway (G/PPP):
T. Runge. Model Engineering and Validation of Biochemical Networks with
Coloured Petri nets - Demonstrated for Glycolysis (in German).
Master's thesis, Brandenburg University of
Technology Cottbus, Computer Science Dept., 2004.
- stochastic models
- Phosphate regulation in enteric bacteria:
W Marwan, C Rohr, M Heiner:
Petri nets in Snoopy: A unifying framework for the graphical display,
computational modelling, and simulation
of bacterial regulatory networks;
in Jv Helden, A Toussaint, D Thieffry (eds):
Methods in Molecular Biology - Bacterial Molecular Networks,
Humana Press, book series "Methods in Molecular Biology", submitted.
- Lac operon:
M Heiner, S Lehrack, D Gilbert, W Marwan:
Extended Stochastic Petri Nets for Model-based Design of Wetlab Experiments;
Trans. on Computational Systems Biology XI, Springer LNCS/LNBI 5750, pp. 138-163, 2009.
- continuous models
- Hypoxia:
M Heiner, K Sriram.
Structural Analysis to Determine the Core of Hypoxia Response Network;
PLoS ONE 5(1): e8600, doi:10.1371/journal.pone.0008600, January 2010.
- RKIP:
D. Gilbert and M. Heiner. From Petri Nets to Differential Equations -
an Integrative Approach for Biochemical Network Analysis; In Proc.
27th ICATPN 2006, LNCS 4024, pages 181-200.
Springer, 2006.
- case studies discussed in three paradigms (qualitative, stochastic, continuous)
- RKIP:
M Heiner, R Donaldson, D Gilbert:
Petri Nets for Systems Biology;
in MS Iyengar (ed.):
Symbolic Systems Biology: Theory and Methods,
Jones & Bartlett Learning, LLC, Chapter 3, pp. 61-97, 2010.
- MAPK:
M Heiner, D Gilbert, R Donaldson:
Petri Nets for Systems and Synthetic Biology;
in M Bernardo, P Degano, and G Zavattaro (eds.): SFM 2008,
Springer
LNCS 5016, pp. 215-264, 2008.
- Biosensor:
D Gilbert, M Heiner, S Rosser, R Fulton, X Gu, M Trybilo:
A
Case
Study in Model-driven Synthetic Biology;
IFIP WCC 2008, 2nd IFIP
Conference on Biologically Inspired Collaborative Computing (BICC
2008), Milano, Sept. 2008, Springer Boston, IFIP, Vol . 268, pp.
163-175, 2008.
- MAPK:
D. Gilbert, M. Heiner, and S. Lehrack: A Unifying Framework for
Modelling and Analysing Biochemical Pathways Using Petri Nets. In Proc.
CMSB 2007, LNCS/LNBI 4695, pages 200-216.
Springer, 2007.
D o w n l o a d s
N e w s
- 2009-12-02 new netclass Freestyle net
- 2009-07-06 new export of stochastic attributes lists to csv
- 2009-06-10 some bugfixes in the stochastic simulation
- 2009-05-26 New stable version of snoopy
- 2009-03-27 New Export from stochastic Petri nets to PRISM
- 2009-03-06 New PRNG (Mersenne-Twister) for stochastic Simulation
- 2009-02-04 Many bugfixes and small changes regarding the stability of snoopy
- 2008-11-18 Snoopy is now Unicode capable, many bugfixes
- 2008-10-09 New netclass MusicNets available, again many bugfixes
- 2008-08-08 improvements and bugfixes for SBML import
- 2008-08-05 new beta version with SBML support and some minor bugfixes
- 2008-07-07 new beta version with some bugfixes and new zoom and scrolling features released
- 2008-06-30 New Snoopy-BETA version with many bugfixes and spline arcs released
- 2008-04-16 New fixed Snoopy-BETA windows version with new installer and Mac version released
Change log for Snoopy-BETA:
- Unicode support
- SBML Level 2 import/export
- experimental graph class for stochastic Petri nets added
- Update to latest library versions (wxwidgets 2.8, xerces 2.7,
graphviz 2.12)
- interaction manager
- new graph classes: extended fault tree, MTBDD, Time PT nets
- colouring of invariants
- several GUI improvements
Any comments are welcome.
Windows version
- download
- after download finished double click on the *.msi and the installation starts
- start snoopy, e.g. by double click on the icon on your desktop
Linux version
- Ubuntu 9.10:
- Debian 5.0:
- OpenSUSE 11.1:
- Fedora 12:
Mac OS X version
- download
- open the dmg and drag snoopy to your favorite location
- start snoopy, e.g. by double click on the name
For our faithful long-term friends, who want to transfer their
PED-files, we provide here a ped2snoopy converter, and some useful hints to use it.
Here are some examples to get used to the tool:
There is no manual available, but you will probably not miss it.
Anyway, here you find some useful
hints (tricks and tips, undocumented features, scheduled
extensions, etc) are not supposed to be exhaustive.
R e l a t e d S o f t w
a r e
Charlie
Charlie
is a software tool to analyse Place/Transition nets. The tool is in use
for the verification of technical systems, especially software-based
systems, as well as for the validation of natural systems, i.e.
biochemical networks as metabolic, signal transduction and gene
regulatory networks.
The tool has been developed - and is still under development - at our
research group.
Main Features
- structural properties (net classes, deadlocks/traps)
- invariant based analysis (p- and t-invariants, dependent node
sets)
- reachability graph based analysis
- behavioural properties (boundedness, liveness,
reversibility)
- explicit CTL model checking
- explicit LTL model checking
- shortest paths
- reachability/coverability graph visualization using the JUNG library
DSSZ-MC
DSSZ-MC
contains tools for the symbolic analysis of bounded Petri nets for standard properties and CTL model checking. They are based on an efficient implementation of Zero-suppressed
Binary Decision Diagrams (zbdd-mc) and Interval Decision Diagrams (idd-mc).
Main Features
- no previous knowledge of the boundedness degree required (idd-mc)
- efficient saturation-based reachability analysis
- dead state analysis with trace generation
- analysis of strongly connected components (liveness, reversibility)
- efficient CTL model checking based on limited backward reachability analysis
- support of Petri nets with extended arcs (read arcs, inhibitor arcs, reset arcs)
MC2(PLTLc)
MC2(PLTLc) is a Monte Carlo Model Checker for
Probabilistic Linear Time Logic with numerical constraints. I t
is a product of the Bioinformatics
Research Centre, University of Glasgow,
UK. It analyses
stochastic and deterministic simulation runs of stochastic or
continuous models, e.g.
stochastic or continuous Petri nets. It follows the off-line approach,
i.e.
MC2 takes as input any time series output, produced by simulations or
measured in wetlab experiments; it reads Snoopy's Gillespie traces. MC2(PLTLc) home page
Main features
- Logic: Probabilistic Linear Time Logic with numerical constraints
(PLTLc)
- model checking: Monte Carlo approximation by analysing a finite
number of finite traces
- off-line approach
- parallel evaluation of several traces
- model checking of parameter scan outputs
PInA
PInA is a software tool for computation and analysis of invariants of
place/transition nets:
PInA
home page
The tool is in use for the verification of technical systems,
especially software-based systems, as well as for the validation of
natural systems, i.e. biochemcial networks as metabolic, signal
transduction, gene regulatory networks.
Main Features
- computation of p- and t-invariants
- statistical analysis
- computation of dependent transition sets/MCT-sets
- cluster analysis
- imports/exports from/to other tools
INA
INA - the Integrated
Net Analyzer - may be used to to analyze Petri nets produced by
Snoopy. The tool has been developed at the Humboldt University in
Berlin, Dep. of Computer Science, "automata theory" over about 20
years. So it shouldn't be a big suprise that it comes along with a pure
ASCII user interface only.
Recommendations for Windows users:
- rename INAwin32.exe to ina.exe
- write the ina.exe to the same folder as snoopy.exe
or better: add the directory, where ina.exe is located, to
the PATH system variable
- start INA in the command line of the DOS window by
typing ina.exe
Snoopy provides an import from the following tools/languages:
- Petri net EDitor:PED
- Abstract Petri Net Notation:APNN
- TIme petri Net Analyzer:TINA
- Systems Biology Markup Language Level 2 Version 3: SBML
(rules, events and functions are not supported yet)
- disjunctive normal form of boolean expresion to fault tree
Furthermore Snoopy provides exports to several analysis tools, among
them:
B u g R e p o r t s
Submit your bug reports and comments about Snoopy to:
- Please check, if your problem still exists in the latest
available version of Snoopy
- Please include the information about your platform (Windows,
Linux) and Snoopy build details (available in the Help->About
window)
M a i l i n g L i s t
If you want to be close related to our Snoopy development you can join
our mailing list:
This mailing list is for discussion of new features, bug reports, and
for announcements of new Snoopy versions.
For joining our mailing list write an email to majordomo@informatik.tu-cottbus.de
with no subject and the following text inside:
subscribe snoopy-l
Then you get a email with a authentication code to ensure that nobody
can put others on the list.
Reply to this email and send back only the line with the authentication
code as described in the email.
. . . t h e e n d . . .