Skip to content
Snippets Groups Projects
Commit 0c0e347b authored by Johannes Mey's avatar Johannes Mey
Browse files

add p/t net execution (both in-place and by creating new markings)

parent dbabcdba
No related branches found
No related tags found
No related merge requests found
......@@ -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();
}
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);
}
}
......@@ -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());
}
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();
}
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());
}
}
}
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment