CPN-AMI Web site

2010-10-19

LIP6 > Software > MoVe Sofware > CPN-AMI > Manual

Below is the full set of services available in CPN-AMI. Please note that :

By default services are available for all supported target architectures (As for now, PC/Linux and MAc/MacOS X),
Services marked in red are not available for Darwin

Menu items that are not available for a given target architecture will not be displayed.

To access a specific user manual, please click on the corresponding item (note that CPN-AMI menus are also available in French and Spanish if you start FrameKit specifying these languages as default). You can also get the PDF version (easier to print;-) of these pages here.

AMI-Net
Petri net syntax checker
Modelling facilities
	Petri net assembling
		Assembling by transition fusion
		Assembling by place fusion
		Execute PetriScript program
		Execute PetriScript program (debug mode)
	Petri net Beautifier
		Oriented graph strategy
		Non oriented graph strategy
		Options
			90 degres rotation
			Reduction factor: 50%
			Expantion factor: 150%
			Expansion factor: 200%
	Suppress structuraly useless places and transitions
Structural properties
	Invariants
		Colored invariants
		P-invariants
		T-invariants
		P-invariants by unfolding
		Linear characterization (verbose)
		Linear characterization
	Structural bounds
		Compute structural bounds
		Is the net structuraly safe?
		Is the net structurally bounded?
		Compute structural bounds by unfolding
		Is the colored structurally net safe (by unfolding)?
		Is the colored net structurally bounded?
		Options
			Suppress structuraly useless places and transitions
	Syphoon and traps
		Minimal syphon
		Minimal traps
		BDD based Minimal syphon
		BDD based Minimal traps
		Minimal syphon by unfolding
		Minimal traps by unfolding
	Liveness for 1-bounded nets
		Liveness
		Liveness (verbose)
Behavioral Properties
	Symbolic reachability graph - GreatSPN and liP6 tools
		Does the system have deadlocks
		LTL model checking on the symbolic RG
		Show symmetric model
		Generation of symbolic RG
		Generation of RG
		Get the symbolic RG (pretty)
		Get the symbolic RG
		Get the RG (pretty)
		Get the RG
	Model Checking with PNITS
		DDD CTL Verification
		DDD CTL Verification (by unfolding)
	Model Checking with PNSDD - LIBDDD Activate
		DDD CTL Verification
		DDD CTL Verification (by unfolding)
	Model Checking with IDDMC
		SDD CTL Verification
		SDD CTL Verification (by unfolding)
	Model Checking with ZBDDMC
		SDD CTL Verification
		SDD CTL Verification (by unfolding)
	Model Checking with PNSDD - LIBSDD Activate
		SDD CTL Verification
		SDD CTL Verification (by unfolding)
	Model Checking with PNITS
		ITS CTL Verification
		ITS CTL Verification (by unfolding)
	Model Checking with PROD
		LTL verification "on the fly"...
		Start/Continue the Reachability Graph construction
		Set the reachability Graph (interrupted construction)
		Statistics about the reachability graph
		List of dead markings
		Extract a path between two nodes
		Extract a path between two nodes (verbose)
		Extract a path between two nodes (with animation)
		Test empty place
		List empty place
		Get the reachability graph - arc routing
		Get the reachability graph - no arc routing
		Expert mode - CTL model checking
			Build a query...
			Help...
		Clean files
		Options
			LTL verification
				Use Stubborn Sets
			RG Construction
				Compute Strongly Connected Components
				New graph
				Bound execution time...
				Bound number of nodes...
				Use Memory...
	LoLA
		Semi-decide reachability of a state
		Decide reachability of a state
		Evaluate a temporal logic query
		Is a transition dead?
		Is the net reversible?
		Is there a home marking?
		Is there a deadlock state?
		Is a place bounded?
		Is the net bounded?
	Modular symbolic observation graphs
	LTL with symbolic observation graphs
	Prefix (EVR unfolding, from PEP)
	Complete Prefix + lyaouts (EVR unfolding, from PEP)
	Boolean condition over place marking
Unfoldings
	CPN unfolder
		Unfold
		Options
			Suppress structuraly useless places and transitions
			Compute layout
		Optimized unfold
	Optimized CPN unfolder
		Execute Unfold
		Optimizations on the resulted PN
			Removal of "false" guarded transitions
			Removal of maximal unmarked syphon
			Removal of orphaned marked places
			Generate the P/T net after unfolding
ISO/IEC-15909
	Export to PNML format
	Import from PNML format