| Class | Description |
|---|---|
| AbstractLivenessAnalyzer | |
| BoundednessAnalyzer |
Class to analyze whether a given PetriNet is bounded Based on Murata, Tadao.
|
| CGGenerator |
This class represents a plugin to transform net into coverability graph
|
| DeadTransitionAnalyzer |
This class analyze dead transitions in a given net Based on coverability
graph written by Murata, Tadao.
|
| HomeMarkingAnalyzer |
Class to analyze all home marking Home marking is reachable from all of
available marking.
|
| LivenessAnalyzer |
Class to analyze whether a given net is live based on Murata, Tadao.
|
| LivenessAnalyzerWithSequence |
Class to analyze whether a given net is live based on Murata, Tadao.
|
| RelaxedSoundnessAnalyzer |
Relaxed soundness checker using LoLA Assuming that the Petri net has
interleaving semantics
|
| TSGenerator |