migrate SLE PetriNet project

parents
# Petrinets4Analysis
### Introduction
This tool can be used for supporting development and use of petrinet
models. It allows the description of models and the verification of
essential properties such as safeness and transition liveness.
Furthermore, subclasses of petrinets can be recognised and certain
simplifying transformations are applied upon request. _[[not yet completed]]_
### The Petrinets4Analysis Language
##### Example
The basic structure of a model in the domain-specific language
is as follows:
```
petrinet ExamplePetrinet {
/* C-style block comments
* may be used anywhere
* and span multiple lines.
*/
place P1 initial 1;
transition t1: // this is a transition followed by a line-comment
1 <- P1
1 -> P2
place P2; // places may also come after transitions referencing them
}
```
##### Description
A petrinet must have an (arbitrarily chosen) name following the keyword
`petrinet`. Within braces, it can contain any number of _places_ and
_transitions_ (in any order).
A place is introduced with the keyword `place`, has a unique name and
can---optionally---contain tokens in the initial marking (default: 0).
A transition also has a name (distinct from all other transitions and
places) following the keyword `transition`. It is described by a set of
incoming and outgoing edges specified below; each edge has a _weight_
indicating the number of tokens moved (usually 1, but any positive integer
can be used), and references a place that must be defined somewhere
in the petrinet. `n <- P` (read: _n from P_) is an incoming edge,
i.e. the tokens are taken from P upon firing the transition. Conversely,
`n -> P` (read: _n to P_) is an outgoing edge, and n tokens are added to
P once the transition is fired.
##### Assertions
Additionally, the petrinet may include _assertions_ of the form
```
petrinet Assertions {
assert safe;
assert l1live(*);
assert extended_free_choice;
assert l0live(t);
place P;
transition t:
1 <- P
}
```
If the assertion is not satisfied, the petrinet will not be processed
and an error will be reported. This is useful for modeling where certain
domain requirements should hold at all times and not need to be verified
manually.
The following is a list of currently supported assertions and their meaning.
| Assertion | Meaning |
|-----------|---------|
| `assert safe;` | The petrinet is _safe_, i.e. no transition sequence results in more than one token per place. |
| `assert bounded;` | The petrinet is _bounded_, i.e. it is not possible to produce arbitrarily many tokens. |
| `assert l0live;`<br>`assert l0live(*);`<br>`assert l0live(t1,t2);` | The specified transitions are _l0-live_, i.e. can never be fired in any sequence. If `*` or no argument, applies to all transitions. |
| `assert l1live;`<br>`assert l1live(*);`<br>`assert l1live(t1,t2);` | The specified transitions are _l1-live_, i.e. there is a transition sequence where they are fired. If `*` or no argument, applies to all transitions. |
| `assert state_machine;` | The petrinet is a _state machine_, i.e. each transition has a unique in- and out-place. |
| `assert marked_graph;` | The petrinet is a _marked graph_, i.e. each place has a unique incoming and outgoing transition. |
| `assert free_choice;` | The petrinet is _free-choice_, i.e. if a place has multiple outgoing edges, each of these must be the only from-edge of their transition. |
| `assert extended_free_choice;` | The petrinet is an _extended free-choice net_, i.e. for any two places the sets of outgoing transitions are either the same, or disjoint. |
| `assert asymmetric_choice;` | The petrinet is _asymmetric-choice_ (_simple_), i.e. for any two places the sets of outgoing transitions are either disjoint or one is contained within the other. |
### The Petrinets4Analysis Application
#### Building
Have maven installed and run `mvn install`.
Tested with JDK 12; compiled for JDK 8.
#### Running the Tool
The maven configuration produces a compiled jar, including all
dependencies, at `[project]/target/petrinets-[version]-jar-with-dependencies.jar`,
which can be run as a normal command-line tool with the Java interpreter
(JRE required), i.e. `java -jar /path/to/petrinets.jar inputfile.pn`.
In normal use, the program will attempt to parse and verify a given
petrinet model file. Additionally, certain arguments can modify the
behaviour:
| Flag | Behaviour |
|------|-----------|
| `--debug` | Enables debug output, if it has been disabled (`--pretty`, `--dot`). |
| `--no-debug` | Disables debug output, e.g. if the output should be fed into another program or a file. |
| `--safe` or `--unsafe` | Checks whether `assert safe;` would be successful, including a (counter-)example. |
| `--bounded` or `--unbounded` | Checks whether `assert bounded;` would be successful, including a (counter-)example. |
| `--l0-live *` or `--l1-live *` | For each transition, checks whether it is l0-live or l1-live. |
| `--l0-live t1,t2` | Checks whether `assert l0live(t1,t2);` would be successful, including a counterexample. |
| `--l1-live t1,t2` | Checks whether `assert l1live(t1,t2);` would be successful, including an example. |
| `--type` | Checks which of the subclasses the net belongs to, i.e. which `assert subclass;` would be successful. |
| `--pretty` | Pretty-prints the given petrinet in a more readable format. Implies `--no-debug`. |
| `--dot` | Prints the petrinet in [dot-format](https://www.graphviz.org/doc/info/lang.html) that can be visualised, e.g. with [graphviz](https://www.graphviz.org/) using <code>java -jar petrinets.jar model.pn --dot &#124; dot -Tpng > graph.png</code> |
| `--simplify` | Applies simple transformations to reduce petrinet complexity. |
Arguments are order-sensitive: `petrinets.jar input.pn --pretty --simplify` will give the *original* petrinet and *then*
simplify. `petrinets.jar input.pn --simplify --pretty` will *first* simplify and *then* output the result.
Similarly, `petrinet.jar input.pn --bounded --simplify --bounded` could be used to verify that the transformation
preserves boundedness: duplicate arguments will be evaluated multiple times in order.
\ No newline at end of file
This diff is collapsed.
<?xml version="1.0" encoding="UTF-8"?>
<Diagram>
<ID>JAVA</ID>
<OriginalElement />
<nodes>
<node x="203.0" y="142.0">petrinet.analyses.transformations.Transformation</node>
<node x="0.0" y="71.0">petrinet.prettyprint.PetrinetPrettyPrinter</node>
<node x="0.0" y="284.0">petrinet.cocos</node>
<node x="0.0" y="213.0">petrinet.PetrinetsTool</node>
<node x="0.0" y="142.0">petrinet.analyses.CoverabilityTree</node>
<node x="0.0" y="0.0">petrinet.analyses.transformations.SimpleTransformations</node>
<node x="0.0" y="355.0">petrinet.analyses.Subclass</node>
<node x="147.0" y="355.0">petrinet.analyses.Liveness</node>
<node x="182.0" y="213.0">petrinet.analyses.Boundedness</node>
<node x="294.0" y="355.0">petrinet.analyses.Marking</node>
<node x="166.0" y="284.0">petrinet.analyses.TokenCount</node>
<node x="238.0" y="71.0">petrinet.prettyprint.PetrinetDotPrinter</node>
</nodes>
<notes />
<edges />
<settings layout="Hierarchic Group" zoom="1.0" x="401.0" y="181.0" />
<SelectedNodes />
<Categories />
<SCOPE>All</SCOPE>
<VISIBILITY>private</VISIBILITY>
</Diagram>
<project xmlns="http://maven.apache.org/POM/4.0.0" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
<modelVersion>4.0.0</modelVersion>
<!-- == PROJECT COORDINATES ============================================= -->
<groupId>de.monticore.lang</groupId>
<artifactId>petrinets</artifactId>
<version>0.0.1</version>
<properties>
<!-- .. Libraries ..................................................... -->
<monticore.version>5.0.2</monticore.version>
<guava.version>28.0-jre</guava.version>
<jsr305.version>3.0.2</jsr305.version>
<junit.version>4.11</junit.version>
<antlr.version>4.7.2</antlr.version>
<logback.version>1.2.3</logback.version>
<junit.jupiter.version>5.4.2</junit.jupiter.version>
<!-- .. Plugins ....................................................... -->
<assembly.plugin>3.1.1</assembly.plugin>
<compiler.plugin>3.8.1</compiler.plugin>
<release.plugin>2.5.3</release.plugin>
<source.plugin>3.1.0</source.plugin>
<surefire.plugin>2.22.2</surefire.plugin>
<!-- Classifiers -->
<grammars.classifier>grammars</grammars.classifier>
<!-- .. Misc .......................................................... -->
<java.version>1.8</java.version>
<wagon.provider.version>3.3.2</wagon.provider.version>
<project.build.sourceEncoding>UTF-8</project.build.sourceEncoding>
<project.reporting.outputEncoding>UTF-8</project.reporting.outputEncoding>
</properties>
<!-- == PROJECT METAINFORMATION ==
======================================= -->
<name>Petrinets</name>
<url />
<inceptionYear>2019</inceptionYear>
<organization>
<name>SE RWTH Aachen</name>
<url>http://www.se-rwth.de/</url>
</organization>
<mailingLists>
<mailingList>
<name>Developer</name>
<post>monticore-dev@se-rwth.de</post>
</mailingList>
</mailingLists>
<issueManagement>
<system>Trac</system>
<url>https://sselab.de/lab2/private/trac/MontiCore/</url>
</issueManagement>
<!-- == DEFAULT BUILD SETTINGS =========================================== -->
<build>
<extensions>
<extension>
<groupId>org.apache.maven.wagon</groupId>
<artifactId>wagon-webdav-jackrabbit</artifactId>
<version>${wagon.provider.version}</version>
</extension>
</extensions>
<plugins>
<!-- MontiCore Generation -->
<plugin>
<groupId>de.monticore.mojo</groupId>
<artifactId>monticore-maven-plugin</artifactId>
<version>${monticore.version}</version>
<executions>
<execution>
<configuration>
<script>de/monticore/monticore_noemf.groovy</script>
</configuration>
<goals>
<goal>generate</goal>
</goals>
</execution>
</executions>
</plugin>
<!-- Other Configuration -->
<plugin>
<groupId>org.apache.maven.plugins</groupId>
<artifactId>maven-compiler-plugin</artifactId>
<version>${compiler.plugin}</version>
<configuration>
<source>${java.version}</source>
<target>${java.version}</target>
</configuration>
</plugin>
<plugin>
<artifactId>maven-surefire-plugin</artifactId>
<version>${surefire.plugin}</version>
<configuration>
<classpathDependencyExcludes>
<classpathDependencyExclude>de.monticore:monticore-cli</classpathDependencyExclude>
</classpathDependencyExcludes>
</configuration>
</plugin>
<plugin>
<groupId>org.apache.maven.plugins</groupId>
<artifactId>maven-release-plugin</artifactId>
<version>${release.plugin}</version>
<configuration>
<tagNameFormat>petrinets-@{project.version}</tagNameFormat>
</configuration>
</plugin>
<plugin>
<artifactId>maven-source-plugin</artifactId>
<version>${source.plugin}</version>
<executions>
<execution>
<phase>package</phase>
<goals>
<goal>jar-no-fork</goal>
</goals>
</execution>
</executions>
</plugin>
<plugin>
<groupId>org.apache.maven.plugins</groupId>
<artifactId>maven-assembly-plugin</artifactId>
<version>${assembly.plugin}</version>
<configuration>
<archive>
<manifest>
<mainClass>petrinet.PetrinetsTool</mainClass>
</manifest>
</archive>
<descriptorRefs>
<descriptorRef>jar-with-dependencies</descriptorRef>
</descriptorRefs>
</configuration>
<executions>
<execution>
<configuration>
<formats>
<format>jar</format>
</formats>
</configuration>
<id>petrinets-assembly</id>
<phase>package</phase>
<goals>
<goal>single</goal>
</goals>
</execution>
</executions>
</plugin>
</plugins>
</build>
<dependencies>
<dependency>
<groupId>com.google.guava</groupId>
<artifactId>guava</artifactId>
<version>${guava.version}</version>
</dependency>
<dependency>
<groupId>com.google.code.findbugs</groupId>
<artifactId>jsr305</artifactId>
<version>${jsr305.version}</version>
</dependency>
<dependency>
<groupId>org.antlr</groupId>
<artifactId>antlr4-runtime</artifactId>
<version>${antlr.version}</version>
</dependency>
<!-- MontiCore Dependencies -->
<dependency>
<groupId>de.monticore</groupId>
<artifactId>monticore-runtime</artifactId>
<version>${monticore.version}</version>
</dependency>
<dependency>
<groupId>de.monticore</groupId>
<artifactId>monticore-grammar</artifactId>
<version>${monticore.version}</version>
</dependency>
<dependency>
<groupId>de.monticore</groupId>
<artifactId>monticore-grammar</artifactId>
<version>${monticore.version}</version>
<classifier>${grammars.classifier}</classifier>
<scope>provided</scope>
</dependency>
<!-- .. Test Libraries ............................................... -->
<dependency>
<groupId>org.junit.jupiter</groupId>
<artifactId>junit-jupiter-api</artifactId>
<version>${junit.jupiter.version}</version>
<scope>test</scope>
</dependency>
<dependency>
<groupId>org.junit.jupiter</groupId>
<artifactId>junit-jupiter-engine</artifactId>
<version>${junit.jupiter.version}</version>
<scope>test</scope>
</dependency>
<dependency>
<groupId>org.junit.jupiter</groupId>
<artifactId>junit-jupiter-params</artifactId>
<version>${junit.jupiter.version}</version>
<scope>test</scope>
</dependency>
<dependency>
<groupId>de.monticore</groupId>
<artifactId>monticore-runtime</artifactId>
<version>${monticore.version}</version>
<type>test-jar</type>
<scope>test</scope>
</dependency>
<dependency>
<groupId>ch.qos.logback</groupId>
<artifactId>logback-classic</artifactId>
<version>${logback.version}</version>
</dependency>
</dependencies>
<reporting>
<plugins>
<plugin>
<groupId>de.monticore.mojo</groupId>
<artifactId>monticore-maven-plugin</artifactId>
<version>${monticore.version}</version>
<inherited>false</inherited>
<reportSets>
<reportSet>
<reports>
<report>reporting-report</report>
</reports>
</reportSet>
</reportSets>
</plugin>
</plugins>
</reporting>
<!-- == DISTRIBUTION ==================================================== -->
<distributionManagement>
<repository>
<id>se-nexus</id>
<url>http://nexus.se.rwth-aachen.de/content/repositories/monticore-releases/</url>
</repository>
<snapshotRepository>
<id>se-nexus</id>
<url>http://nexus.se.rwth-aachen.de/content/repositories/monticore-snapshots/</url>
</snapshotRepository>
</distributionManagement>
<repositories>
<repository>
<id>se-nexus</id>
<url>https://nexus.se.rwth-aachen.de/content/groups/public/</url>
</repository>
</repositories>
<pluginRepositories>
<pluginRepository>
<id>se-nexus</id>
<url>https://nexus.se.rwth-aachen.de/content/groups/public/</url>
</pluginRepository>
</pluginRepositories>
</project>
<assembly
xmlns="http://maven.apache.org/plugins/maven-assembly-plugin/assembly/1.1.2"
xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
xsi:schemaLocation="http://maven.apache.org/plugins/maven-assembly-plugin/assembly/1.1.2 http://maven.apache.org/xsd/assembly-1.1.2.xsd">
<id>petrinets</id>
<includeBaseDirectory>false</includeBaseDirectory>
<includeSiteDirectory>false</includeSiteDirectory>
<fileSets>
<fileSet>
<outputDirectory>src</outputDirectory>
<directory>src/main/java</directory>
<excludes>
<exclude>petrinets/_ast/</exclude>
<exclude>petrinets/_symboltable/</exclude>
</excludes>
</fileSet>
<fileSet>
<outputDirectory>hwc</outputDirectory>
<directory>src/main/java</directory>
<includes>
<include>petrinets/_ast/</include>
<include>petrinets/_symboltable/</include>
</includes>
</fileSet>
<fileSet>
<outputDirectory />
<directory>src/main/grammars</directory>
</fileSet>
<fileSet>
<outputDirectory />
<directory>src/main/resources</directory>
</fileSet>
</fileSets>
</assembly>
grammar Petrinet extends de.monticore.literals.Literals {
scope Petrinet = "petrinet" Name "{"
Assertion*
(Place | Transition)*
"}";
Assertion = "assert" Requirement ";";
// workarounds for features missing in MontiCore:
// - enum implements interface is not allowed
// - repetition of symbols is not allowed / does not compile
interface Requirement;
astrule Requirement = method Optional<Boolean> verify(ASTPetrinet petrinet) { };
GlobalRequirement implements Requirement = GlobalFeature;
enum GlobalFeature = "bounded" | "safe";
SubclassRequirement implements Requirement = Subclass;
enum Subclass = "state_machine" | "marked_graph" | "free_choice" | "extended_free_choice" | "asymmetric_choice";
Liveness implements Requirement =
LivenessLevel
("(" ("*" | (TransitionReference || ",")+) ")")?;
enum LivenessLevel = "l0live" | "l1live";
TransitionReference = transition:Name@Transition;
symbol Place = "place" Name ("initial" initial:IntLiteral)? ";";
astrule Place = outEdge:FromEdge* inEdge:ToEdge*;
symbol Transition = "transition" Name ":" (FromEdge | ToEdge)*;
abstract Edge = count:IntLiteral place:Name@Place;
FromEdge extends Edge = count:IntLiteral "<-" place:Name@Place;
ToEdge extends Edge = count:IntLiteral "->" place:Name@Place;
}
This diff is collapsed.
package petrinet._ast;
import petrinet._symboltable.PlaceSymbol;
import java.util.Optional;
public abstract class ASTEdge extends ASTEdgeTOP {
private ASTTransition transition;
/**
* A reference to the enclosing transition.
*
* @return The enclosing transition object.
*/
public ASTTransition getTransition() {
return transition;
}
/**
* Sets the enclosing transition.
*
* @param transition The enclosing transition object.
*/
public void setTransition(ASTTransition transition) {
this.transition = transition;
}
@Override
public Optional<ASTPlace> getPlaceDefinitionOpt() {
// Monticore 5.0.2 is broken, fix symbol resolution.
// Upgrade breaks other stuff, in particular:
// equalAttributes tries to access placeSymbol attribute of ASTEdgeTOP on an
// object casted to ASTEdge, but placeSymbol is private.
if (!placeDefinition.isPresent()) {
if ((place != null) && isPresentEnclosingScope()) {
Optional<petrinet._symboltable.PlaceSymbol> symbol = enclosingScope.flatMap(scope -> scope.resolve(place, PlaceSymbol.KIND));
// flatMap instead of get; symbol might be empty.
placeDefinition = symbol.flatMap(PlaceSymbol::getPlaceNode);
}
}
return placeDefinition;
}
/**
* Checks whether two edges are the same but potentially a from/to pair
* @param other The other edge to compare
* @return True if all attributes are the same
*/
public boolean equalExceptDirection(ASTEdge other) {
return place.equals(other.place) && count.getValue() == other.count.getValue() && transition.deepEquals(other.transition);
}
/**
* Check whether two edges are the same, with potentially different transitions.
* @param other The other edge to compare
* @return True if all attributes except the transition are the same.
*/
public boolean equalExceptTransition(ASTEdge other) {
return place.equals(other.place) && count.getValue() == other.count.getValue();
}
/**
* Check whether two edges are the same, with potentially different places.
* @param other The other edge to compare
* @return True if all attributes except the place are the same.
*/
public boolean equalExceptPlace(ASTEdge other) {
return transition.deepEquals(other.transition) && count.getValue() == other.count.getValue();
}
}
package petrinet._ast;
import petrinet.analyses.Boundedness;
import java.util.Optional;
public class ASTGlobalRequirement extends ASTGlobalRequirementTOP {<