Features of the current version (3.5, October 18, 2010)

CPN-AMI 3.5 provides the services already defined in CPN-AMI 3.4.1 plus the following features:

• IDDMC, a new model checker based on Interval Decision Diagram (from the IDD-MC tool),
• ZBDDMC, a new model checker based on Zero-suppressed Binary Decision Diagram (from the IDD-MC tool),
• 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 in 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).

To get more information, please refer to the user manual of CPN-AMI services.

Features of previous versions

Version (3.4.1, November 23, 2009)

CPN-AMI 3.4.1 provides the services already defined in CPN-AMI 3.4 plus the following features:

• It corrects several minor bugs in the distribution system (problems with some Linux distributions such as Ubuntu),
• PNITS, a new variant of PNSDD based on the new ITS (Intantiable Transisition Systems) library.

To get more information, please refer to the user manual of CPN-AMI services.

Version (3.4, October 21, 2009)

CPN-AMI 3.4 provides the services already defined in CPN-AMI 3.3 plus the following features:

• It is based on FrameKit 2.2 that fixes minor bugs, especially when handling very large nets,
• PNSDD, new CTL our new model checker developed within the context of the NEOPPOD project. It uses a new technology that enforces better support for large models.

Version 3.3 (November 4, 2008)

CPN-AMI 3.3 provides the services already defined in CPN-AMI 3.2 plus the following features:

• modsog and mcsog tools developed in cooperation with the LIPN laboratory.

Version 3.2 (October 25, 2007)

CPN-AMI 3.2 provides the services already defined in CPN-AMI 3.1 plus the following features:

• It is based on FrameKit 2.1.1,
• of the PetriScript interpreter (several minor bugs fixed),
• of the GreatSPN export (Model checking on the Symbolic reachability graph)
• New version of the PNML export (better integration of EMF technology and use of PNML-Framework)
• Connection with the Coloane User interface that enables the drawing of Petri Nets ad well as access to CPN-AMI services from any platform running Eclipse

Version 3.1 (October 25, 2006)

CPN-AMI 3.1 provides the services already defined in CPN-AMI 3.0.1 plus the following features:

• It is based on FrameKit 2.1 that behaves much faster in some cases,
• of the PetriScript interpreter (several minor bugs fixed),
• of the optimized unfolder (several bug fixed + possibility to disable optimizations on the resulted net + support of inhibitor arcs),
• New version of the PNML export (better integration of EMF technology and use of PNML-Framework),
• Model checking on the Symbolic reachability graph using LTL or for safety properties.

IMPORTANT: this new version of CPN-AMI is not compatible with Macao version 2.9.23 and lower. Please, download the last version of Macao here.

Version 3.0.1 (November 30, 2005)

CPN-AMI 3.0.1 provides the services already defined in CPN-AMI 3.0 but corrects some minor bugs:

• A configuration mismatch in prod that disabled access to standard CTL operators in the "expert mode",
• Some permission access management (particularly under MacOS X)
• a better version of the optimized unfolding.

Some problems in Macao 2.9.23 that appeared at version 10.4.2 of MacOS are also corrected (upload Macao or get it in the MacOS distribution).

Version 3.0 (October 10, 2005)

CPN-AMI 3.0 provides the services already defined in CPN-AMI 2.5.2 plus the following ones:

• Tool server platform relies on FrameKit 2.0 (click here for more information)
• AMI-Nets tools :
  • Modeling facilities completely redesigned, introduction of the PetriScript language to automate generation of Petri net pattern models (e.g. FIFO of size N) as well as the assembling of modular Petri nets,
  • PROD, the driver nows allocates prod with 512 Mbyte of memory if possible,
  • Symbolic reachability graph: automatic computation of simmetries + export of the symbolic reachability graph (model checking to come in a later version;-).
  • New optimized Colored Petri net to P/T nets unfolder (beta version). Now, very large models can be processed
  • Partial support of the PNML format (standard ISO/IEC 15909) with an export function (import should come soon)

Version 2.5.2 (October 25, 2004)

CPN-AMI 2.5.2 provides the services already defined in CPN-AMI 1.5 plus the following ones:

• Tool server platform relies on FrameKit 2.0 (click here for more information)
• AMI-Nets tools : many minor changes and minor bug fixed
• Some internal element (not yet available in the public version) to support model checking on the symbolic reachability graph.

This version was used internally only (for research and teaching in UPMC's CS master program).

Version 2.5.1 (June 15, 2002)

CPN-AMI 2.5 provides the services already defined in CPN-AMI 2.4.2 plus the following ones:

• Tool server platform relies on FrameKit 1.4.5 (click here for more information)
• AMI-Nets tools :
  • structured menus changed for better coherence,
  • modular services, better handling of arc attributes,
  • PROD, the driver nows remind the query in Macao historic window and allocates prod with 128 Mbyte of memory if possible,
  • Petri net syntax checker now handles expressions like <C.all>-<x> when using PROD for model checking. It also correct some minor bugs in the translation into PROD format of operator --.

Version 2.5 (January 4, 2001)

CPN-AMI 2.5 provides the services already defined in CPN-AMI 2.4.2 plus the following ones:

• Tool server platform relies on FrameKit 1.4.4 (click here for more information)
• AMI-Nets tools :
  • structured menus for an easier use of CPN-AMI
  • Integration of services provided by LoLA (model checking, search for a home state, search for net reversibility, check boundness of a place/net, check dead transitions...),
  • Petri net syntax checker (new tests on free variables in guards to prevent a limitation for some tools, now supports the LoLA format),
  • Colored Petri Net unfolder (bug fixed in the management of free variables in guards),
  • Computation of colored bounds by means of the unfolded P/T net (when unfolding the P/T net, deletion of structurally useless places and transition can be enabled)
  • Prefix (this service is also available in PEP) (the layout computation may be disabled for the generated prefix net),
  • Generation and analysis of the reachability graph with PROD 3.3.08 (from the Helsinki university of Technology) (new service to compute a path between two states in the reachability graph).

Version 2.4.2 (July 27, 1999)

Version 2.4.2 contains components of CPN-AMI 2.4 plus the following elements :

• AMI-Net formalism: colored Petri nets in CPN-AMI
• AMI-Nets tools :
  • Petri net syntax checker,
  • Debug and simulation for Coloured Petri Nets : CPN/DESIR,
  • Colored Petri Net unfolder,
  • Generation and analysis of the reachability graph with PROD 3.3.04 (from the Helsinki university of Technology),
  • Computation of bounds for places in a P/T net,
  • Computation of colored invariants by means of the unfolded P/T net.
  • Computation of colored bounds by means of the unfolded P/T net
  • Services for modular modelling using Petri nets
  • Supression of structurally 0-bounded places and transition having such place sin input

Diffusion

• Available on the Web.

Version 2.4 (June 25, 1999)

Version 2.4 contains components of CPN-AMI 2.3 plus the following elements :

• FameKit version 1.4.3 (click here for more information)
• Petri net verifier version 2.0, major checks enhancement. It also disable tools when some minor constraints are not verified (for example, places and transition names have to be named as C-identifiers for PROD),
• PROD in AMI-Nets version 1.2 interfaced with PROD version 3.3.
• Bounds version 1.1 it proposes some enhanced packaged services.
• Petri net unfolder version 1.3, it can eliminates 0-bounded places and transitions having such places in input during Petri net unfolding.
• CPN simulator 2.1, it fixes some minor problems introduced with FrameKit 1.4.2 and is more secure.
• new -> Colored bounds (with unfolding) version 1.0 that computes lower and upper places'bounds of the unfolded P/T net from a Colored net,
• new -> Services for modular modelling version 1.0 that proposes basic mechanisms to link Petri net modules.
• new -> suppression of structurally useless places and transitions 1.0 that deletes 0-bounded placaes as well as transition having such places in input in a P/T net.

Diffusion

• Available on the Web.

Version 2.3 (October 27, 1998)

Version 2.3 contains components of CPN-AMI 2.2.1 plus the following elements :

• Petri net syntax checker 1.5 (problems fixed for some subnets classes and major improovements in the execution speed),
• PROD in AMI-Nets version 1.1.1 still integrates version 3.2 but contains some users interface improvements and optimizations. It also supports a standard CTL interface.
• PetriBDD 1.1.1 (correct a bug that was disabling computation on models for which name contains a space),
• Graphic Display 2.0, it still relies on dot (AT&T Bell Labs) but work better (less crashing configurations).
• Linear Characterization 1.3.3, some display problem are fixed.
• new -> Bounds version 1.0 that computes lower and upper places'bounds in a P/T net,
• new -> invcpnunfold version 1.0 that computes colored invariant using the unfolded net.

Diffusion

• Available on the Web.
• preversion used for the Petri Net summer school in Jaca (September 1998)

Version 2.2.1 (April 16, 1998)

Version 2.2.1 contains components of CPN-AMI 2.2 plus the following elements :

• Petri net syntax checker version 1.4.1 (problem fixed in the generation of information into GreatSPN format),
• CPNunfolder version 1.2 (memory allocation problem fixed),
• BooleanCondition version 1.0 (bug fixed).

Diffusion

• Available on the Web.

Version 2.2 (march 19, 1998)

Version 2.2 contains components of CPN-AMI 2.1 plus the following elements :

• FrameKit version 1.4.1 (wich now runs on ultrasparcs under Solaris 2.5.1 or later, click here for more information),
• Petri net syntax checker version 1.4 (better handling of supported formats, smoother integration),
• CPNunfolder 1.1 with full support of transition predicates (integrates corrections made by the patch fixes_bug_1),
• Prefix version 1.0.1 (integrates corrections made by the patch fixes_bug_1),
• PetriBDD 1.1 (includes computation of minimal deadlocks),
• PROD in AMI-Nets version 1.1 still integrates version 3.2 but fixes some bugs (like the correction of an error in the generation of the PROD description) and integrates new features like the cleaning of prod files (usefull when the reachability graph is large).
• Linear Characterization version 1.3.2 which may be slower but provides more precise results,
• new -> "GreatSPN2" (SunOS version only) , the integration of reachability graphs construction modules from GreatSPN2 (generation of both coloured reachability graph and symbolic reachability graph).

Diffusion

• Available on the Web.

Version 2.1 (December 19, 1997)

Version 2.1 contains :

• the FrameKit platform (version 1.4) new -> click here for more details
• the AMI-Net formalism (colored Petri Nets)
• new -> the Branching-Process formalism (for results),
• new -> the ReachabilityGraph formalism (for results),
• the folloving set of tools:
  • "AMI-Net verifier" that verifies model syntax and detects if it corresponds to a P/T net or to a Coloured Net. new -> the verification speed has been enforced, especially for large Petri net models.
  • "Boolean condition" that computes a boolean formula verified by any marking in the reachability graph.
  • "GreatSPN in AMI" (GreatSPN is developed at the university of Torino, Italy) that computes P/T structural properties (place or transition invariants, deadlocks and traps). new -> optimized integration. Now results are computed once and the transfert of results to the User Interface is much faster.
  • "CPN unfolder" that unfold a colored Petri net into a P/T net. new -> a pretty layout can be computed if the kit "Graphic display is installed and a bug that was causing crashes when a color domain had only one colour has been corrected.
  • "CPN invariants" that computes colored place invariants
  • "CPN Desir" that simulates colored Petri nets
  • new -> "Linear Characterization", a service that computes linear constrainst that are respected all over the reachability graph.
  • new -> "Graphic Display", a service that rely on dot (AT&T Bell Labs) that arrange objects in order to minimise arc crossing (usefull when designing large nets). This tool is invoked by the Reachability Graph builder and the CPN unfolder.
  • new -> "Reachability Graph analysis", a set of services to build and analyse reachability graphs. They rely on PROD (University of Helsinki)
  • new -> "Prefix", a service that unfold a P/T net according to the algorithm of Esparza, Vogler and Römer (presented at the TACAS'96 conference [esparza 96]). The underlying tool has been extracted from PEP, another nice Petri Net based environment.

Diffusion

• Available on the Web.

Version 2.0 (March 7, 1997)

Version 2.0 contains:

• the FrameKit platform (version 1.3)
• the AMI-Net formalism (colored Petri Nets)
• the folloving set of tools:
  • "AMI-Net verifier" that verifies model syntax and detects if it corresponds to a P/T net or to a Coloured Net
  • "Boolean condition" that computes a boolean formula verified by any marking in the reachability graph
  • "GreatSPN in AMI" (GreatSPN is developed at the univversity of Torino, Italy) that computes P/T structural properties (place or transition invariants, deadlocks and traps)
  • "CPN unfolder" that unfold a colored Petri net into a P/T net
  • "CPN invariants" that computes colored place invariants
• "CPN Desir" that simulates colored Petri nets

Diffusion

• Available on the Web.

Version 1.1 to 1.3 (December 1994 to December 1995)

These first versions of CPN-AMI were based on AMI, a prototype of integration platform.The experience acquired with AMI and remarks from researchers who downloaded CPN-AMI brought us to work on a new framework generation. FrameKit focuses on the definition of simple procedures for customized installation, maintenance and integration of formalisms or tools. FrameKit do respect the architecture principle depicted in [ECMA 91].

Diffusion

• Fisrt versions were available via ftp on the Web.