CPN-AMI

Overview

Tool homepage: http://www.lip6.fr/cpn-ami

Tool availability: Free of charge

Tool Features

• High-level Petri Nets
• Place/Transition Nets

• Graphical Editor
• Fast Simulation
• State Spaces
• Condensed State Spaces
• Place Invariants
• Transition Invariants
• Structural Analysis
• Interchange File Format
• Services for Moduar Modeling

Environments

• PC, Linux
• Macintosh, Mac OS

Tool Description

CPN-AMI 3.5 is the Petri net based Software engineering environment designed at the "Laboratoire d'Informatique de Paris 6" (LIP6), Université Pierre & Marie Curie, France. CPN-AMI is built on top of FrameKit: a generic platform for the implementation of software engineering environments.

The last version runs on PC/Linux (Mandrake or Redhat) and now also on Mac/MacOS (version 10.5.x or later). It requires a Macintosh for the user interface. The Petri net dialect in CPN-AMI is AMI-Net (Well Formed Colored Petri nets with syntactic constraints). CPN-AMI proposes about 60 services dedicated to the modeling and verification of systems by means of Petri nets:

• new-> IDDMC, a new model checker based on Interval Decision Diagram (from the IDD-MC tool),
• new-> ZBDDMC, a new model checker based on Zero-suppressed Binary Decision Diagram (from the IDD-MC tool),
• new-> Definition of different strategies of Static Variable Ordering (and in a Hierarchical way for PNSDD and PNITS). These are to be use in our Decision Diagram based model checkers (PNSDD, PNITS, ZBDDMC, IDDMC). These strategies were developed i n the context of the Neoppod project:
1. PaToH : Variable ordering using hyper-graph partionning. Each partition is then used as a hierarchy module,
2. NOA99 + PaToH : Pre-variable ordering with NOA99 and then we create hierarchy by using PaToH
3. PF1 + N-Cut-Naive : Pre-variable ordering with Pre-Firing P/T Net (flatten order) and then we create hierarchy by using N-Cut-Naive
4. PF2 + N-Cut-Naive : Pre-variable ordering with Pre-Firing P/T Net (flatten order) and then we create hierarchy by using N-Cut-Naive
5. FORCE + N-Cut-Naive : Using FORCE Heuristics (flat order) and then we create hierarchy by using N-Cut-Naive
6. PISH : Partially Identical Sequence Heuristic
7. NOA99 + N-Cut-Naive : Pre-variable ordering with NOA99 and then we create hierarchy by using N-Cut-Naive Hierarchy
PF1 and PF2 are two pre-firing strategies that help us to find "good" ordering to elaborate our Petri Net encoding into decision diagrams.
PaToH is a ordering strategy based on hypergraphs (use of the PaToH tool).
• updated-> Coloane User interface as an Eclipse plug-in enabling the use of CPN-AMI on Linux (both user interface and tool server) and Windows (user interface with access on a remote tool server),
• updated-> support of the PNML format (standard ISO/IEC 15909) with both export and import function for P/T nets,
• The Graphical User Interface : Macao
• assembling of modular nets
• integration of LoLA facilities
• The AMI-Net syntax checker
• Colored Petri Net flow analysis,
• P/T logic formulae over marking,
• Structural invariants with GreatSPN, (developed by the Universities of Torino and Genova, Italy),
• Petri net Beautifier (rely on dot, from AT&T Bell Labs),
• BDD based analysis,
• Linear Characterization,
• Prefix (Computation of a Branching Process according to the algorithm of Esparza, Vogler and Römer). This service is also available in PEP, a Petri net based modelling environment,
• Analysis of the reachability graph with PROD (version 3.3.08 from the University of Helsinki),
• Computation of bounds for places in a P/T net,
• Computation of invariants on colored Petri nets using the coresponding unfoleded P/T net,
• Computation of bounds for places in a colored net by unfolding,
• services for basic assembling of Petri net modules (place fusion or transition fusion),
• suppression of 0-bounded places and transitions having such places in input (P/T nets).

To get CPN-AMI, please click here. CPN-AMI is free of charges for university and non profit organizations. For more administrative information on CPN-AMI, please contact cpn-ami[at]lip6.fr.

Contact Information

Fabrice Kordon
Laboratoire d'Informatique de Paris 6 (LIP6)
4 place Jussieu
75252 Paris Cedex 05
France

Phone:  +33 1 44 27 61 89
Fax:    +33 1 44 27 74 05
E-mail: cpn-ami@lip6.fr

Other Remarks