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:
- PaToH : Variable ordering using hyper-graph partionning. Each partition is then used as a hierarchy module,
- NOA99 + PaToH : Pre-variable ordering with NOA99 and then we create hierarchy by using PaToH
- 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
- 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
- FORCE + N-Cut-Naive : Using FORCE Heuristics (flat order) and then we create hierarchy by using N-Cut-Naive
- PISH : Partially Identical Sequence Heuristic
- 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:
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
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
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
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
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
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
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.
|