The Azimuth Project
Blog - Petri net software

This page is a blog article in progress, written by John Baez. To see discussions of this article while it is being written, go to the Azimuth Forum.

CPN Tools

CPN Tools is probably the most popular tool for editing, simulating, and analyzing Coloured Petri nets.

It has been developed over the past 25 years.

The tool features incremental syntax checking and code generation, which take place while a net is being constructed. A fast simulator efficiently handles untimed and timed nets. Full and partial state spaces can be generated and analyzed, and a standard state space report contains information, such as boundedness properties and liveness properties.

Dependencies
  • Milton

Snoopy

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. biochemical 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
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
Availability
  • Windows
  • OS X
  • Debian varieties of Linux.
Dependencies
  • Javascript
  • C++
  • wxWidgets
  • Xerces

Helena

Dependencies
References

Abstract

In this paper we advocate a unifying technique for description of Petri net semantics. Semantics, i.e. a possible behaviour, is basically a set of node-labelled and arc-labelled directed acyclic graphs, called token flows, where the graphs are distinguished up to isomorphism. The nodes of a token flow represent occurrences of transitions of the underlying net, so they are labelled by transitions. Arcs are labelled by multisets of places.

Namely, an arc between an occurrence x of a transition a and an occurrence y of a transition b is labelled by a multiset of places, saying how many tokens produced by the occurrence x of the transition a is consumed by the occurrence y of the transition b. The variants of Petri net behaviour are given by different interpretation of arcs and different structure of token flows, resulting in different sets of labelled directed acyclic graphs accepted by the net.

We show that the most prominent semantics of Petri nets, namely processes of Goltz and Reisig, partial languages of Petri nets introduced by Grabowski, rewriting terms of Meseguer and Montanari, step sequences as well as classical occurrence (firing) sequences correspond to different subsets of token flows.

Finally, we discuss several results achieved using token flows during the last four years, including polynomial test for the acceptance of a partial word by a Petri net, synthesis of Petri nets from partial languages and token flow unfolding.

Abstract

Reaction systems are a formal model for processes inspired by the functioning of the living cell.The underlying idea of this model is that the functioning of the living cell is determined by the interactions of biochemical reactions, and these interactions are based on the mechanisms of facilitation and inhibition. In this paper we first review the main notions of the basic model of reaction systems which is a qualitative model.Then we discuss various ways of taking into account quantitative properties.

Abstract

Communication structured occurrence nets (CSON) are an extension of occurrence nets. They can be used to represent the execution behaviours of complex evolving systems. Communication structured place transition nets (CSPT-nets) provide a system-level model for describing the interaction between different systems, and CSONs can model individual runs of CSPT-nets. I

n this paper, we investigate branching processes of CSPT-nets which provide a complete information about their behaviours. We also outline an algorithm for the construction of unfoldings of CSPT-nets.

CSONs are acyclic and conflict-free.

GreatSPN

“GreatSPN is a suite of tools for the design and analysis (qualitative and quantitative) of Generalized Stochastic Petri Nets and Stochastic Well-formed nets. First released by the University of Torino in the late 1980’s, GreatSPN has been a widely used tool in the research community since it provides a breadth of solvers for computing net structural properties, the set of Reachable States (RS), the Reachability Graph (RG) with and without symmetry exploitation, and performance evaluation indices using both simulation and numerical solution for steady state and transient measures.

Over the years, GreatSPN functionality has been extended, also thanks to the collaboration with University of Paris 6 and the Universit`a del Piemonte Orientale, by improving and enhancing its solution algorithms, and by providing new solution methods for new formalisms and property languages defined over the years.

The latest enhancements include:

  • Model checking. A Computational Tree Logic (CTL) model checker for Petri nets with priorities and a CSL-TA stochastic model checker for SPN. The CTL model checker implementation is based on the Meedly library from University of Iowa
  • Optimization problem analyzer. Integration of the Markov Decision Well-formed Net formalism and associated solution algorithms, which allow the study of optimization problems based on Discrete Time Markov Decision Process.
  • Fluidification analysis. The addition of the PN2ODE module, which allows to automatically derive from an SPN model a corresponding set of ODEs (in Matlab format), whose solution provides the expected values of the performance indices, as a function of time.
  • Dynamic SRG and Extended SRG. The algorithms for the construction of the Symbolic RG have been extended to include Dynamic SRG and Extended SRG construction, two non trivial extensions of the SRG construction which can provide a reduction of the state space size in case of partially symmetrical SWN models.“
References
  • S. Baarir, M. Beccuti, D. Cerotti, M. D. Pierro, S. Donatelli, and G. Franceschinis. The greatspn tool: recent enhancements. SIGMETRICS Performance Evaluation Review, 36(4):4-9, 2009.
  • J. Babar, M. Beccuti, S. Donatelli, and A. S. Miner. Greatspn enhanced with decision diagram data structures. In Proc. of 31st International Conference, volume 6128 of Lecture Notes in Computer Science. Springer, pages 308-317, 2010.

ITS-Tools

  • Univ. Pierre & Marie Curie, France

ITS-tools is a suite of model-checking tools, developed in the team MoVe at LIP6. Written in C++, it is available under the terms of the GNU General Public Licence.

It features state-space generation, reachability analysis, LTL and CTL checking. ITS-tools accept a wide range of inputs: (Time) Petri Nets, ETF (produced by the tool LTSmin), DVE (input format to the tool DiVinE, used in the BEEM database), and a dedicated C-like format known as GAL. The input models can also be given as compiled object files. This allows for large possibilities of interaction with other tools.

Models, even in different formats, can also be easily composed, through the formalism of Instantiable Transition Systems (ITS) [Itstools3]. This ease the modeling process. ITS-tools also features a graphical interface, as an Eclipse plug-in, to further help the modeler, especially with compositions.

As for the back-end, ITS-tools rely on decision diagrams [Itstools1] to handle efficiently the combinatorial explosion of the state space. The decision diagrams manipulation is performed by the libDDD library, that features several mechanisms for the efficient manipulation of decision diagrams [Itstools2,Itstools4]. References

  • Hierarchical decision diagrams to exploit model structure, J. M. Couvreur and Y. Thierry-Mieg, Formal Techniques for Networked and Distributed Systems-FORTE 2005 443-457 (2005)
  • Hierarchical set decision diagrams and automatic saturation, A. Hamez and Y. Thierry-Mieg and F. Kordon, Applications and Theory of Petri Nets 211-230 (2008)
  • Hierarchical set decision diagrams and regular models, Y. Thierry-Mieg and D. Poitrenaud and A. Hamez and F. Kordon, Tools and Algorithms for the Construction and Analysis of Systems 5505 1-15 (2009)
  • Towards Distributed Software Model-Checking using Decision Diagrams, M. Colange and S. Baarir and F. Kordon and Y. Thierry-Mieg, Computer Aided Verification, to appear (2013)

LoLA

  • Univ. Rostock, Germany

“LoLA [Lola1] provides explicit state space verification for place/transition nets. It supports various simple properties. For the contest, mainly the reachability verification features are used.

LoLA offers several techniques for alleviating state explosion, including various stubborn set methods, symmetries (which it can determine fully automated), the sweep-line method (where it computes its own progress measure), bloom filters, and linear algebraic compressions. To our best knowledge, LoLA is the only tool worldwide that provides this large number of explicit state space techniques in this high degree of automaton, and with these possibilities for joint application.

In the MCC, we neither use symmetries nor the sweep-line method. For these methods, performance is too volatile for the black box scenario implemented in the MCC.

NOTE: associated to he main version, three variants (described below) were provided.“

References
  • K. Wolf. Generating Petri net state spaces. In J. Kleijn and A. Yakovlev, editors, 28th International Conference on Applications and Theory of Petri Nets and Other Models of Concurrency (ICATPN), June 25-29, 2007, Proceedings, volume 4546 of Lecture Notes in Computer Science, pages 29-42. Springer-Verlag, June 2007. Invited lecture

Variant: lola_optimistic

This variant uses a goal oriented stubborn set method and linear algebraic state compression. Goal oriented stubborn sets perform best on reachability queries that are ultimately satisfied in the net under investigation. A heuristics takes care that a satisfying state is reached with high probability already in very early stages of state space exploration. This way, only a tiny portion of the state space is actually explored. If the satisfying states are missed, however, or no satisfying state is reachable, a significantly larger state space is produced than the one produced by lola-pessimistic. Witness paths tend to be very small. Variant: lola_optimistic_incomplete

In addition to lola-optimistic, we use a bloom filter for internal representation of states. That is, only the hash value of a state is marked in several hash tables, each belonging to an independent hash function. The state itself is not stored at all. This way, we can handle a larger number of states within a given amount of memory. In the rare case of a hash collision, the colliding state is not explored, so parts of the state space may be missed and false negative results are possible.

The user can specify the number of hash tables to be used and thus control the probability of hash collisions. Variant: lola_pessimistic

This variant computes stubborn sets using a standard deletion algorithm. Deletion algorithms are much slower than goal-oriented stubborn sets (quadratic instead of linear) but yield better reduction. This better reduction pays off when the whole state space needs to be explored (i.e. there are no reachable satisfying states). If reachable states exist, this variant is outperformed by the optimistic variant since it has no goal-orienting heuristics and tends to miss reachable states in early phases of state space exploration.

Witness paths are often much longer than in the optimistic variant.

MARCIE

  • Univ. Cottbus, Germany

MARCIE [Marcie1] is a tool for the analysis of Generalized Stochastic Petri Nets, supporting qualitative and quantitative analyses including model checking facilities. Particular features are symbolic state space analysis including efficient saturation-based state space generation, evaluation of standard Petri net properties as well as CTL model checking.

Most of MARCIE’s features are realized on top of an Interval Decision Diagram (IDD) implementation [Marcie4]. IDDs are used to efficiently encode interval logic functions representing marking sets of bounded Petri nets. This allows to efficiently support qualitative state space based analysis techniques [Marcie3]. Further, MARCIE applies heuristics for the computation of static variable orders to achieve small DD representations.

For quantitative analysis MARCIE implements a multi-threaded on-the-fly computation of the underlying CTMC [Marcie2]. It is thus less sensitive to the number of distinct rate values than approaches based on, e.g., Multi-Terminal Decision Diagrams. Further it offers symbolic CSRL model checking and permits to compute reward expectations. Additionally MARCIE provides simulative and explicit approximative numerical analysis techniques. References

  • M. Heiner, C. Rohr, and M. Schwarick. MARCIE - Model checking And Reachability analysis done effiCIEntly. In J. Colom and J. Desel, editors, Proc. PETRI NETS 2013, volume 7927 of LNCS, pages 389-399. Springer, June 2013.
  • M. Schwarick, C. Rohr, and M. Heiner. MARCIE - Model checking And Reachability analysis done effiCIEntly. In Proc. 8th International Conference on Quantitative Evaluation of SysTems (QEST 2011), pages 91 - 100. IEEE CS Press, September 2011.
  • M. Schwarick and A. Tovchigrechko. IDD-based model validation of biochemical networks. TCS 412, pages 2884-2908, 2010.
  • A. Tovchigrechko. Model Checking Using Interval Decision Diagrams. PhD thesis, BTU Cottbus, Dep. of CS, 2008.

Neco

  • Univ. Evry-Val-d’Essone, France

“Neco is a suite of Unix tools to compile high-level Petri nets into libraries for explicit model-checking. These libraries can be used to build state spaces. It is a command-line tool suite available under the GNU Lesser GPL.

Neco compiler is based on SNAKES [Neco1] toolkit and handles high-level Petri nets annotated with arbitrary Python objects. This allows for big degree of expressivity. Extracting information form models, Neco can identify object types and produce optimized Python or C++ exploration code. The later is done using the Cython language. Moreover, if a part of the model cannot be compiled efficiently a Python fallback is used to handle this part of the model.

The compiler also performs model based optimizations using place bounds [Neco3] and control flow places for more efficient firing functions. However, these optimizations are closely related to a modelling language we use which allows them to be assumed by construction. Because the models from the contest were not provided with such properties, these optimizations could not be used.

The tool suite provides tools to compile high-level Petri nets and build state spaces but this year we also provide a LTL model-checker: Neco-spot. It builds upon Neco and upon Spot [Neco2, Neco4], a C++ library of model-checking algorithms.“

References
  • F. Pommereau. SNAKES is the net algebra kit for editors and simulators. http://www.ibisc.univ- evry.fr/ fpommereau/snakes.htm
  • A. Duret-Lutz and D. Poitrenaud. SPOT: an Extensible Model Checking Library using Transition-based Generalized Buchi Automata. In Proceedings of the 12th IEEE/ACM International Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunication Systems (MASCOTS), pages 76-83, 2004. IEEE Computer Society Press.
  • L. Fronc and F. Pommereau. Optimizing the compilation of Petri nets models. In Proceedings of the second International Workshop on Scalable and Usable Model Checking for Petri Net and other models of Concurrency (SUMO), volume 726. CEUR, 2011.
  • L. Fronc and A. Duret-Lutz. LTL Model Checking with Neco. In Proceedings of the 11th International Symposium on Automated Technology for Verification and Analysis (ATVA), to appear in Lecture Notes in Computer Science, Hanoi, Vietnam, 2013. Springer.

PNXDD

  • Univ. Pierre & Marie Curie, France

“PNXDD is CTL model-checker based on Set Decision Diagrams (SDD) [PNXDD1] for PT-nets, a variant of the decision diagrams (DD) family with hierarchy. Symmetric Petri Nets are handled via an optimized unfolding PNXDD2laces structurally detected as always empty and the associated transitions).

Hierarchy paradigm, used together with DDs offers greater sharing possibilities compared to traditional DDs. The ordering of variables in the diagram, a crucial parameter to obtain good performances in DDs, becomes a new challenge since portions of the model offering similar comportments must be statically identified to obtain a good hierarchical order. PNXDD relies on heuristics that are described in [PNXDD3].“

References
  • Y. Thierry-Mieg, D. Poitrenaud, A. Hamez and F. Kordon. Hierarchical Set Decision Diagrams and Regular Models. Proc. of TACAS 2009, volume 5505 of LNCS, pages 1-15, Springer.
  • F. Kordon, A. Linard and E. Paviot-Adet. Optimized Colored Nets Unfolding. Proc. of FORTE 2006, volume 4229 of LNCS, pages 339-355, Springer.
  • S. Hong, F. Kordon, E. Paviot-Adet and S. Evangelista. Computing a Hierarchical Static order for Decision Diagram-Based Representation from P/T Nets. Transactions on Petri Nets and Other Models of Concurrency (ToPNoC), volume V, pages 121-140, Springer Verlag 2012.

Sara

  • Univ. Rostock, Germany

“Sara [Sara1] answers reachability queries using the Petri net state equation. From this equation and inequations derived from the query, a linear programming problem is generated and solved using a standard package. If the system does not have solutions, we conclude that there are no reachable states satisfying the query. Other wise, we obtain a firing count vector which describes candidate firing sequences.

We check whether there is an executable firing sequence for the given vector. If so, we have a reachable satisfying state and a witness path. If not, we add inequalities that are not satisfied by the spurious solution. We result in one or more new linear programming problems which enable less serious solutions but still cover all feasible solutions. We proceed recursively with the new problems.

Sara has excellent performance if the state equation as such rules out reachability, or if an early solution reveals reachability. It may be used for unbounded Petri nets. since it does not try to represent or to explore the state space.

In worst case, Sara will not terminate (otherwise, our approach would contradict the known EXPSPACE hardness of the general reachability problem).“

References
  • H. Wimmel and K. Wolf. Applying CEGAR to the Petri net state equation. In Tools and Algorithms for the Construction and Analysis of Systems, 17th International Conference, TACAS, volume 6605 of Lecture Notes in Computer Science, pages 224-238. Springer-Verlag, 2011.

Maria

Maria is a reachability analyzer for concurrent systems that uses Algebraic System Nets (a high-level variant of Petri nets) as its modelling formalism. It has been written in C++, and its is freely available under the terms of the GNU General Public License.

References

PInA

References
  • Implementation of Joint Commitment Theory through Petri Net Plans. P. F. Palamara, V.A. Ziparo, L. Iocchi, D. Nardi, P. Lima. In Proc. of RoboCup Symposium, 2008.

  • Petri net plans: a formal model for representation and execution of multi-robot plans. V. A. Ziparo, L. Iocchi, D. Nardi, P. F. Palamara , H. Costelha. In Proc. of the 7th international joint conference on Autonomous Agents and MultiAgent Systems (AAMAS 2008). Volume 1. pp 79-86

  • A Robotic Soccer Passing Task Using Petri Net Plans (Demo Paper). P.F. Palamara, V. A. Ziparo, L. Iocchi, D. Nardi, P. Lima, H. Costelha. In Proc. of 7th Int. Conf. on Autonomous Agents and Multiagent Systems (AAMAS 2008), pp.1711-1712. Best Robotic Demo Award.

PROD

  • univ. hamburg

  • PROD

The Pr/T-net reachability analysis tool PROD implements several methods for efficient reachability analysis.

PROD is a text-based tool that can be used in UNIX (any system of that kind) and in Windows (3.1, 3.11, ‘95, NT, ‘98, 2000, XP). Currently no graphical user-interface exists. PROD supports the following reduced reachability graph generation methods that may also be combined:

The stubborn set method.
The sleep set method.
Priority definitions.
The use of symmetries.

PROD supports verification of CTL formulas from the reachability graph, and on-the-fly verification of LTL formulas using e.g. the stubborn set method.

  • Last updated 2007.

Haskell Coloured Petri Net Editor

Haskell-Coloured Petri Net is a graphical editor and simulator for Coloured Petri Nets, using Haskell as inscription and implementation language.“

“Dormant (great potential, but needs funding for intensive development, and to go beyond coloured Petri nets). Last updated to build with GHC/WxHaskell 0.8 (I do have a version that builds with GHC 6.10.3 and WxHaskell 0.11, but the binary releases of WxHaskell for Windows were missing a critical component, last I checked). More recently, I’ve started on a simple browser-based GUI alternative (Javascript+SVG), but that hasn’t been hooked up to code-generator and simulator yet.”

Availability
Dependencies
  • wxWidgets-2.9.

CosyVerif

Dependencies:
  • Coloane
  • Virtual Box (Oracle) or other VM
  • BenchKit
References

AlPINA

AlPINA stands for Algebraic Petri Nets Analyzer and is a model checker for Algebraic Petri Nets created by the SMV Group at the University of Geneva. It is 100% written in Java and it is available under the terms of the GNU general public license. Our goal is to provide a user friendly suite of tools for checking models based of the Algebraic Petri Net formalism. AlPiNA provides a user-friendly user interface that was built with the latest metamodeling techniques on the eclipse platform.

Usually, the number of states of concurrent systems grows exponentially in relation to the size of the system. This is called the State Space Explosion. Symbolic Model Checking (SMC) and particularly SMC based on Decision Diagrams is a proven technique to handle the State Space Explosion for simple formalisms such as P/T Petri nets./p>

Algebraic Petri Nets (APN : Petri Nets + Abstract Algebraic Data Types) are a powerful formalism to model concurrent systems. The State Space Explosion is even worse in the case of the APNs than in the P/T nets, mainly because their high expressive power allows end users to model more complex systems. To tackle this problem, AlPiNA uses evolutions of the well known Binary Decision Diagrams (BDDs), such as Data Decision Diagrams, Set Decision Diagrams and Sigma-DDs. It also includes some optimizations specific to the APN formalism, such as algebraic clustering and partial algebraic unfolding, to reduce the memory footprint. With these optimisations, AlPiNA provides a good balance between user-friendliness, modeling expressivity and computational performances.

References
  • D. Buchs, S. Hostettler, A. Marechal, and M. Risoldi. AlPiNA: A symbolic model checker. In J. Lilius and W. Penczek, editors, Applications and Theory of Petri Nets, volume 6128 of Lecture Notes in Computer Science, pages 287-296. Springer, 2010.
  • D. Buchs, S. Hostettler, A. Marechal, and M. Risoldi. Alpina: An algebraic petri net analyzer. In J. Esparza and R. Majumdar, editors, Tools and Algorithms for the Construction and Analysis of Systems, volume 6015 of Lecture Notes in Computer Science, pages 349-352. Springer, 2010.
  • S. Hostettler, A. Marechal, A. Linard, M. Risoldi, and D. Buchs. High-level petri net model checking with alpina. Fundamenta Informaticae, 113(3-4):229-264, Aug. 2011.

Cunf

  • École Normale Supérieure de Cachan, France.

Cunf is a set of programs for carrying out unfolding-based verification of Petri nets extended with read arcs, also known as contextual nets, or c-nets. The package specifically contains the following tools:

  • Cunf: constructs the unfolding of a c-net,
  • Cna: performs reachability and deadlock analysis using unfoldings constructed by Cunf,
  • Scripts such as pep2dot or grml2pep to do format conversion between various Petri net formats, unfolding formats, etc.

The unfolding of a c-net is another well-defined c-net of acyclic structure that fully represents the reachable markings of the first. Because unfolding represent behavior by partial orders rather than by interleaving, for highly concurrent c-nets, unfolding are often much (exponentially) smaller, which makes for natural interest in them for the verification of concurrent systems.

Cunf requires that the input c-net is 1-safe (i.e., no reachable marking puts more than one token on every place), and for the time being the tool will blindly assume this. It implements the c-net unfolding procedure proposed by Baldan et al.

Cna (Contextual Net Analyzer), checks for place coverability or deadlock-freedom of a c-net by examining its unfolding. The tool reduces these problems to the satisfiability of a propositional formula that it generates out of the unfolding, and uses Minisat as a back-end to solve the formula.

You may download the tool’s manual from the tool’s webpage, where you will find detailed instructions for installation. The tool is integrated in the Cosyverif environment, whose graphical editor you may want to use to analyze nets constructed by hand. Cunf also comes with Python libraries for producing c-nets programmatically, see Sec. 7 of the manual. References

  • Paolo Baldan, Andrea Corradini, Barbara Konig, and Stefan Schwoon. McMillan’s complete prefix for contextual nets. ToPNoC, 1:199-220, 2008. LNCS 5100.
  • P. Baldan, A. Bruni, A. Corradini, B. Konig, C. Rodriguez, and S. Schwoon. Efficient unfolding of contextual Petri nets. Theoretical Computer Science., 449:2-22, 2012.

libits

libITS is C++ library for model-checking of various formalisms using libDDD.

Main features include:

  • Instantiable Transition System as a framework, allow hierarchical composition of components specified in diverse formalisms.
  • User friendly GUI is provided as Eclipse plugins for modeling ITS compositions, (time) Petri nets, and rich-text editing of GAL models.
  • Optimized implementation taking full advantage of the features of libDDD, notably automatic saturation and hierarchy.
  • Support for Petri nets and some of their extensions
  • Support for discrete time in models such as Time Petri nets and their compositions
  • Support for GAL format input which offers rich data manipulation.
  • Support for ETF format input which is produced by the tool LTSmin from diverse formalisms.
  • Support for Divine format input which is native to the tool Divine and used in BEEM models.
  • Support for CTL model checking using saturation and forward transition relation.
  • Support for LTL model checking using some classic and some original algorithms that exploit saturation.

The ITS tools are distributed under the terms of the GNU Public License GPL. We have integrated modified versions of sources taken from other open-source projects such as Divine, VIS or LTSmin. See Acknowledgements section.

They are built using libDDD for model-checking of (labeled) Petri nets with some extensions (Time Petri nets, Queues, inhibitor arcs, rest arcs, self-modifying nets…), as well as their composition using a formalism called Instantiable Transition Systems. Composite ITS types offer a great flexibility in the definition of synchronized products of transitions systems. Scalar and Circular compositions express common symmetric synchronization patterns (a pool of processes, a ring topology), and are exploited by the tool to provide superior performance. The GAL language complements ITS by providing a model for high-level data manipulation. It offers a rich C-like syntax and direct support for arithmetic and arrays. Systems can be provided using mixed formalisms, such as TPN for the control part and GAL for the data part synchronized using Composite ITS types. ITS-tools also support Divine models natively, thanks to an internal translation to GAL. Last but not least, ETF files produced by LTSmin from several high-level formalisms can be used as input for symbolic model-checking.

Discrete Event Simulation (DES) Software

There is, or was, a visual formalism called DEVS—Discrete Event System Specification—which has developed a host of visual tools for modelling and maybe code/stub generation.

Wikipedia carries a list of open source and commercial DES software:

aDevs

aDevs (a discrete event simulator) is a C++ library for constructing discrete event simulations based on the Parallel DEVS and Dynamic DEVS (dynDEVS) formalisms.

DEVS has been applied to the study of social systems, ecological systems, computer networks and computer architecture, military systems at the tactical and theater levels, and in many other areas.

Recent advances in quantized approximations of continuous systems suggest promising computational techniques for high performance scientific computing (e.g. in the field of computational fluid dynamics).“

Dependencies
  • C++ compiler

CD++

“An open source tool based on the DEVS and Cell-DEVS formalisms (a discrete-event specification of cellular automata models). Hundreds of model samples are available. Varied 2D and 3D visualization engines can be used to improve the analysis of the simulation results.”

PowerDEVS

An integrated tool for hybrid systems modeling and simulation based on the DEVS formalism.

Dependencies
  • Java

Facsimile

A free, open-source discrete-event simulation/emulation library.

Galatea

An Agent-based simulation platform.

Chemical reaction software

Cain

Cain performs stochastic and deterministic simulations of chemical reactions. It can spawn multiple simulation processes to utilize multi-core computers. It stores models, simulation parameters, and simulation results in an XML format. In addition, SBML models can be imported and exported. The models and simulation parameters can be read from input files or edited within the program.

Cain offers a variety of solvers:

  • Gillespie’s direct method.
  • Gillespie’s first reaction method.
  • Gibson and Bruck’s next reaction method.
  • Tau-leaping.
  • Hybrid direct/tau-leaping.
  • ODE integration.“
Dependencies
  • Python

Computer animations

JointJS

  • [JointJS(http://jointjs.org)]

Flexible tool with Petri net demo animation.

Dependencies
  • backbone.js
  • jquery.hs

Computer Animations, U. Waterloo is a browser applet to simulate properties of gases.

“A user can choose one of several gases to investigate at a time. The temperature and volume are two independent variables that can be altered, and the pressures calculated by the two models are presented. This is a deterministic simulation, but the calculated pressures may be misleading.”

One of the suggested application is to ask students to formulate a general statement regarding the conditions, under which the model is valid. Gases such as He, H2, N2, H2O, CO2, etc are included in the applet.

Dependencies
  • Java

Molecular dynamics

PyMol

Molecular modelling tool.

Dependencies
  • Python

Chemsuite

Chemsuite is a set of programs designed for the processing of chemical information on Linux/X11.

Availability

Free software released under the GPL license.

Dependencies
  • QT GUI library version 2.3.1 from Trolltech Inc. .
  • Linux

CHIMP

CHIMP is a generic tool for the modeling of chemical phenomena. Eventually, chemical reaction modeling, molecular mechanics, and quantum mechanic modules will be implemented, along with an easy to use graphical-user interface (GUI). At present, CHIMP has the ability to perform dynamic Monte Carlo simulations on chemical reactions, in particular heterogeneous catalytic reactions.”

VASP

“This is a scientific visualization package for examining output files generated by the Vienna Ab-initio Simulation Package, a package for performing ab-initio quantum-mechanical molecular dynamics using pseudopotentials and a plane wave basis set. The project was initiated when a chemical engineering professor requested assitance in visualizing output files produced by the above package. It displays iso-surfaces and slices of a three-dimensional data set, along with the atoms that make up the molecule the calculations were performed for, and allows symbolic bonds to be inserted between them.”

BIGMAC

“Configurational Bias Monte Carlo (CBMC) is a recent technique to compute thermodynamic properties of flexible molecules. It has been used by several academic groups to study the adsorption behavior of linear and branched alkanes in zeolites and the vapor-liquid equilibrium of linear and branched alkanes. In Cerius2 version 4.0 there is a CBMC utility for calculating adsorption properties of linear and brached molecules. However, Cerius2 is platform dependent and quite expensive.

The group of Prof. Berend Smit has developped BIGMAC, which is a general-purpose CBMC code. You can download a version of this code for grand-canonical and gibbs ensemble simulations of simple linear alkanes (approximately 7.6 MB).“

References

Abinit

“ABINIT is a package whose main program allows one to find the total energy, charge density and electronic structure of systems made of electrons and nuclei (molecules and periodic solids) within Density Functional Theory (DFT), using pseudopotentials and a planewave or wavelet basis.

ABINIT also includes options to optimize the geometry according to the DFT forces and stresses, or to perform molecular dynamics simulations using these forces, or to generate dynamical matrices, Born effective charges, and dielectric tensors, based on Density-Functional Perturbation Theory, and many more properties.

Excited states can be computed within the Many-Body Perturbation Theory (the GW approximation and the Bethe-Salpeter equation), and Time-Dependent Density Functional Theory (for molecules). In addition to the main ABINIT code, different utility programs are provided.

ABINIT is a project that favours development and collaboration (short presentation of the ABINIT project - 10 pages in pdf).“

GROMACS

GROMACS is a versatile package to perform molecular dynamics, i.e. simulate the Newtonian equations of motion for systems with hundreds to millions of particles.

It is primarily designed for biochemical molecules like proteins, lipids and nucleic acids that have a lot of complicated bonded interactions, but since GROMACS is extremely fast at calculating the nonbonded interactions (that usually dominate simulations) many groups are also using it for research on non-biological systems, e.g. polymers.

GROMACS supports all the usual algorithms you expect from a modern molecular dynamics implementation, (check the online reference or manual for details), but there are also quite a few features that make it stand out from the competition:

  • Supports CUDA-based GPU access.
  • No scripting language, all programs use a simple interface.“

AlChemy

Fontana et al. represent molecules as λ-calculus expressions. Reactions are defined by the operations of “application” of one λ-term to its reaction partner. The result is a new λ-term.

It is worth noting in this context that chemical reactions can in turn be regarded as a model of computation, a possibility that is realized for example in the Chemical Abstract Machine.

  • Walter Fontana and Leo W. Buss, Towards a theory of biological organisation, A programmatic statement
  • W. Fontana. Algorithmic chemistry. In C. G. Langton, C. Taylor, J. D. Farmer, and S. Rasmussen, editors, Artificial Life II, pages 159–210, Redwood City, CA, 1992. Addison-Wesley.
  • [20] W. Fontana and L. W. Buss. What would be conserved if ‘the tape were played twice’? Proc. Natl. Acad. Sci. USA, 91:757–761, 1994.

Chemical Abstract Machine

[6] G. Berry and G. Boudol. The chemical abstract machine. Theor. Comp. Sci., 96:217–248, 1992.

Electric circuit emulation

LTSpice

Uses net list data file input.

Availability
  • open source
  • Windows
  • OS X

Synthetic biology

VANTED

  • Leibniz Institute of Plant Genetics and Crop Plant Research (IPK).

VANTED (2006) is a framework for systems biology applications, which comprises a comprehensive set of seven main tasks. These range from network reconstruction, data visualization, integration of various data types, network simulation to data exploration combined with a manifold support of systems biology standards for visualization and data exchange. The offered set of functionalities is instantiated by combining several tasks in order to enable users to view and explore a comprehensive dataset from different perspectives. We describe the system as well as an exemplary workflow.”

References
Dependencies
  • Java VM

Tortuga

Hybrid modelling tools

Hybrid modelling tools support Petri nets and other formalisms.

Hybrid Petri nets refer to Petri nets which support both discrete and continuous transitions.

OpenModelica

ExtendedPetriNet
Features
  • transitions allowing for deterministic or stochastic time delays before their firing (using builit-in random number generators BIRNG or custom made ones),
  • and places capable of containing more than one token such that timed, stochastic Petri nets can be modeled.
  • supports uniform, exponential, normal and Weibull distributions for random time delays.
  • multiple tokens per place as needed for flow and store nets..
Dependencies

InsightMaker

Availability
  • open source
Dependencies
  • any modern browser
  • javascript

Hydra

Hydra is a high level, declarative language for modelling and simulation of physical systems. Systems in Hydra are being modelled using implicitly formulated (undirected) Differential Algebraic Equations (DAEs). While, physical modelling is our main focus any domain is fine where problems can be formulated using DAEs.

The language provides constructs for definition and composition of model fragments that enable modelling and simulation of large, complex, hybrid and highly structurally dynamic systems.

The first outline of Hydra was given by Nilsson et al. in the framework called Functional Hybrid Modelling (FHM). Subsequently, a number of papers have been published about the design and implementation of Hydra that can be accessed on the following web pages:

Dependencies

Haskell compiler (ghc).

category: blog