From 0c0e347b8cced6146f7203e89e2024525f989407 Mon Sep 17 00:00:00 2001
From: Johannes Mey <johannes.mey@tu-dresden.de>
Date: Tue, 23 Jun 2020 15:45:55 +0200
Subject: [PATCH] add p/t net execution (both in-place and by creating new
markings)
---
src/main/jastadd/Navigation.jrag | 41 +++++++++++++++++++
src/main/jastadd/marking/Execution.jadd | 41 +++++++++++++++++++
src/main/jastadd/marking/Marking.jrag | 21 ++++++++++
src/main/jastadd/marking/Printing.jrag | 11 ++++-
.../java/de/tudresden/inf/st/pnml/Main.java | 25 ++++++++++-
5 files changed, 136 insertions(+), 3 deletions(-)
create mode 100644 src/main/jastadd/marking/Execution.jadd
diff --git a/src/main/jastadd/Navigation.jrag b/src/main/jastadd/Navigation.jrag
index 116505e..e84c14f 100644
--- a/src/main/jastadd/Navigation.jrag
+++ b/src/main/jastadd/Navigation.jrag
@@ -2,6 +2,42 @@ aspect Navigation {
inh PetriNet PnObject.petriNet();
eq PetriNet.getChild().petriNet() = this;
+ java.util.Collection<Place> Transition.incomingPlaces() {
+ java.util.Set<Place> incomingPlaces = new java.util.HashSet<>();
+ for (Arc incomingArc : getInArcList()) {
+ incomingPlaces.add(incomingArc.getSource().asPlaceNode().place());
+ }
+ return incomingPlaces;
+ }
+
+ java.util.Collection<Place> Transition.outgoingPlaces() {
+ java.util.Set<Place> outgoingPlaces = new java.util.HashSet<>();
+ for (Arc outgoingArc : getOutArcList()) {
+ outgoingPlaces.add(outgoingArc.getTarget().asPlaceNode().place());
+ }
+ return outgoingPlaces;
+ }
+
+ syn boolean Node.isPlaceNode() = false;
+ eq PlaceNode.isPlaceNode() = true;
+
+ syn PlaceNode Node.asPlaceNode() = null;
+ eq PlaceNode.asPlaceNode() = this;
+
+ syn boolean Node.isTransitionNode() = false;
+ eq TransitionNode.isTransitionNode() = true;
+
+ syn TransitionNode Node.asTransitionNode() = null;
+ eq TransitionNode.asTransitionNode() = this;
+
+ syn Place PlaceNode.place();
+ eq Place.place() = this;
+ eq RefPlace.place() = getRef().place();
+
+ syn Transition TransitionNode.transition();
+ eq Transition.transition() = this;
+ eq RefTransition.transition() = getRef().transition();
+
coll java.util.Set<PnObject> PetriNet.allObjects() [new java.util.HashSet()] root PetriNet;
PnObject contributes this
to PetriNet.allObjects()
@@ -11,4 +47,9 @@ aspect Navigation {
Place contributes this
to PetriNet.allPlaces()
for petriNet();
+
+ coll java.util.Set<Transition> PetriNet.allTransitions() [new java.util.HashSet()] root PetriNet;
+ Transition contributes this
+ to PetriNet.allTransitions()
+ for petriNet();
}
diff --git a/src/main/jastadd/marking/Execution.jadd b/src/main/jastadd/marking/Execution.jadd
new file mode 100644
index 0000000..a1b6684
--- /dev/null
+++ b/src/main/jastadd/marking/Execution.jadd
@@ -0,0 +1,41 @@
+aspect Execution {
+
+ public boolean Marking.fireInPlace() {
+ return fireInPlace(new Random());
+ }
+
+ public boolean Marking.fireInPlace(java.util.Random random) {
+ return fireInPlace(random, true).isPresent();
+ }
+
+ private Optional<Marking> Marking.fireInPlace(java.util.Random random, boolean requireFlush) {
+ if(enabledTransitions().isEmpty()) return Optional.empty();
+
+ // select a random transition
+ Transition transition = enabledTransitions().stream()
+ .sorted((t1, t2) -> t1.getId().compareTo(t2.getId()))
+ .skip(random.nextInt(enabledTransitions().size()))
+ .findFirst().get();
+
+ // take a token from each incoming place
+ transition.incomingPlaces().forEach(place -> this.resolvePlace(place).setMarking(this.resolvePlace(place).getMarking()-1));
+
+ // place a token in each outgoing place
+ transition.outgoingPlaces().forEach(place -> this.resolvePlace(place).setMarking(this.resolvePlace(place).getMarking()+1));
+
+ if (requireFlush) {
+ // flush the entire marking tree
+ this.flushTreeCache();
+ }
+
+ return Optional.of(this);
+ }
+
+ public Optional<Marking> Marking.fire() {
+ return fire(new Random());
+ }
+
+ public Optional<Marking> Marking.fire(java.util.Random random) {
+ return treeCopyNoTransform().fireInPlace(random, false);
+ }
+}
diff --git a/src/main/jastadd/marking/Marking.jrag b/src/main/jastadd/marking/Marking.jrag
index 93a7ec3..c5a365f 100644
--- a/src/main/jastadd/marking/Marking.jrag
+++ b/src/main/jastadd/marking/Marking.jrag
@@ -24,4 +24,25 @@ aspect Marking {
}
return map;
}
+
+ syn int Marking.marking(Place place) = resolvePlace(place).getMarking();
+
+ syn boolean Marking.isEnabled(Transition t) {
+ for (Place place : t.incomingPlaces()) {
+ if (marking(place) == 0) return false;
+ }
+ return true;
+ }
+
+ syn boolean Marking.isDead() {
+ for (Transition transition : getPetriNet().allTransitions()) {
+ if (isEnabled(transition)) return false;
+ }
+ return true;
+ }
+
+ syn java.util.Set<Transition> Marking.enabledTransitions()
+ = getPetriNet().allTransitions().stream()
+ .filter(t -> isEnabled(t))
+ .collect(Collectors.toSet());
}
diff --git a/src/main/jastadd/marking/Printing.jrag b/src/main/jastadd/marking/Printing.jrag
index 66bd662..e89c16e 100644
--- a/src/main/jastadd/marking/Printing.jrag
+++ b/src/main/jastadd/marking/Printing.jrag
@@ -1,10 +1,17 @@
aspect Printing {
syn String Marking.print() {
StringBuilder b = new StringBuilder();
- b.append("Marking for Petri net '").append(getPetriNet().getId()).append("':\n");
+ b.append("Marking for Petri net '").append(getPetriNet().name()).append("':\n");
for (MarkedPlace place : getPlaceList()) {
- b.append(" ").append(place.getPlace().getId()).append(": ").append(place.getMarking()).append("\n");
+ b.append(" ").append(place.getPlace().name()).append(": ").append(place.getMarking()).append("\n");
+ }
+ b.append("Transitions for Petri net '").append(getPetriNet().name()).append("':\n");
+ for (Transition trans : getPetriNet().allTransitions()) {
+ b.append(" ").append(trans.name()).append(": ").append(isEnabled(trans)?"true":"false").append("\n");
}
return b.toString();
}
+
+ syn String PetriNet.name() = hasName()?getName().getText():getId();
+ syn String PnObject.name() = hasName()?getName().getText():getId();
}
diff --git a/src/main/java/de/tudresden/inf/st/pnml/Main.java b/src/main/java/de/tudresden/inf/st/pnml/Main.java
index 25690ef..f1ec059 100644
--- a/src/main/java/de/tudresden/inf/st/pnml/Main.java
+++ b/src/main/java/de/tudresden/inf/st/pnml/Main.java
@@ -1,5 +1,6 @@
package de.tudresden.inf.st.pnml;
+import de.tudresden.inf.st.pnml.jastadd.model.Marking;
import de.tudresden.inf.st.pnml.jastadd.model.PetriNet;
import fr.lip6.move.pnml.framework.general.PNType;
import fr.lip6.move.pnml.framework.hlapi.HLAPIRootClass;
@@ -15,6 +16,8 @@ import java.nio.file.Path;
import java.nio.file.Paths;
import java.util.ArrayList;
import java.util.List;
+import java.util.Optional;
+import java.util.Random;
public class Main {
@@ -23,11 +26,31 @@ public class Main {
public static void main(String[] args) {
String fileName = "src/main/resources/minimal.pnml";
+// String fileName = "src/main/resources/philo.pnml";
List<PetriNet> petriNets = parsePnml(fileName);
for (PetriNet petriNet : petriNets) {
- logger.info(petriNet.initialMarking().print());
+ Marking originalMarking = petriNet.initialMarking();
+ Marking currentMarking = originalMarking;
+ logger.info("initial marking:\n{}", originalMarking.print());
+
+ // always use seed 0, it is the best seed!
+ Random random1 = new Random(0);
+ Random random2 = new Random(0);
+
+ for (int i = 1; i <= 5 && !originalMarking.isDead() && !currentMarking.isDead(); i++) {
+
+ Optional<Marking> optionalCurrentMarking = currentMarking.fire(random1);
+ if (optionalCurrentMarking.isPresent()) {
+ currentMarking = optionalCurrentMarking.get();
+ } else {
+ throw new RuntimeException("Unable to get successor marking, even though the marking is not dead!");
+ }
+ originalMarking.fireInPlace(random2);
+ logger.info("Original marking after {} firings: {}", i, originalMarking.print());
+ logger.info("Current marking after {} firings: {}", i, currentMarking.print());
+ }
}
}
--
GitLab