Build graph game and graph game strategy for bounded games.

src/uniolunisaar/adam/ds/synthesis/solver/symbolic/bddapproach/distrenv/DistrEnvBDDSolvingObject.java

@@ -4,22 +4,26 @@
 import java.util.List;
 import java.util.Map;
 import java.util.Set;
+import java.util.function.BinaryOperator;
 import java.util.stream.Collectors;
 import org.apache.commons.collections4.CollectionUtils;
 import uniol.apt.adt.pn.Marking;
 import uniol.apt.adt.pn.Place;
 import uniol.apt.adt.pn.Transition;
 import uniolunisaar.adam.ds.objectives.Condition;
+import uniolunisaar.adam.ds.petrinet.PetriNetExtensionHandler;
 import uniolunisaar.adam.ds.synthesis.pgwt.PetriGameWithTransits;
 import uniolunisaar.adam.ds.synthesis.solver.symbolic.bddapproach.BDDSolvingObject;
 import uniolunisaar.adam.exceptions.pnwt.NetNotSafeException;
 import uniolunisaar.adam.exceptions.synthesis.pgwt.InvalidPartitionException;
 import uniolunisaar.adam.exceptions.synthesis.pgwt.NoSuitableDistributionFoundException;
 import uniolunisaar.adam.exceptions.synthesis.pgwt.NotSupportedGameException;
+import uniolunisaar.adam.exceptions.synthesis.pgwt.UnboundedPGException;
 import uniolunisaar.adam.logic.synthesis.pgwt.calculators.CalculatorIDs;
 import uniolunisaar.adam.logic.synthesis.pgwt.partitioning.Partitioner;
 import uniolunisaar.adam.tools.Logger;
 import uniolunisaar.adam.util.PGTools;
+import uniolunisaar.adam.util.PNTools;
 
 /**
  * This class serves for storing the input of the solving algorithm, i.e., the
@@ -31,6 +35,7 @@
 public class DistrEnvBDDSolvingObject<W extends Condition<W>> extends BDDSolvingObject<W> {
 
     private List<Transition> systemTransitions, envTransitions;
+    private Map<Integer, Long> boundOfPartitions;
 
     public DistrEnvBDDSolvingObject(PetriGameWithTransits game, W winCon) throws NotSupportedGameException, NetNotSafeException, NoSuitableDistributionFoundException, InvalidPartitionException {
         this(game, winCon, false);
@@ -46,8 +51,9 @@ public DistrEnvBDDSolvingObject(DistrEnvBDDSolvingObject<W> obj) {
 
     @Override
     protected void checkPrecondition(PetriGameWithTransits game) throws NetNotSafeException, NotSupportedGameException {
-        if (!game.getBounded().isSafe()) {
-            throw new NetNotSafeException(game.getBounded().unboundedPlace.toString(), game.getBounded().sequence.toString());
+        PNTools.addsBoundedness2Places(game);
+        if (!game.getBounded().isBounded()) {
+            throw new UnboundedPGException(game, game.getBounded().unboundedPlace);
         }
         PGTools.checkAtMostOneSysToken(game);
     }
@@ -181,6 +187,14 @@ public Place getSystemPlaceOfTransition(Transition transition, boolean post) {
         return currentPlaceOfSystemPlayer.iterator().next();
     }
 
+    public long getBoundOfPartition(int partition) {
+        if (this.boundOfPartitions == null) {
+            this.boundOfPartitions = this.getGame().getPlaces().stream()
+                    .collect(Collectors.toMap(this.getGame()::getPartition, PetriNetExtensionHandler::getBoundedness, BinaryOperator.maxBy(Long::compareTo)));
+        }
+        return this.boundOfPartitions.get(partition);
+    }
+
     public Set<Marking> getBadMarkings() {
         return this.getGame().getFinalMarkings();
     }

src/uniolunisaar/adam/ds/synthesis/solver/symbolic/bddapproach/distrenv/Multiset.java

@@ -0,0 +1,72 @@
+package uniolunisaar.adam.ds.synthesis.solver.symbolic.bddapproach.distrenv;
+
+import java.util.Collections;
+import java.util.Map;
+import java.util.Set;
+import java.util.function.BiFunction;
+import java.util.function.Function;
+import java.util.stream.Collector;
+import java.util.stream.Collectors;
+import java.util.stream.IntStream;
+import java.util.stream.Stream;
+
+public class Multiset<K> {
+    private final Map<K, Integer> map;
+
+    private Multiset(Map<K, Integer> map) {
+        this.map = map;
+    }
+
+    public int count(K element) {
+        return this.map.getOrDefault(element, 0);
+    }
+
+    public boolean contains(K element, int minMultiplicity) {
+        return this.count(element) >= minMultiplicity;
+    }
+
+    public boolean contains(K element) {
+        return this.contains(element, 1);
+    }
+
+    public boolean containsAll(Set<K> set) {
+        return set.stream().allMatch(this::contains);
+    }
+
+    public static <K> Collector<K, ?, Multiset<K>> collect() {
+        return Collectors.collectingAndThen(Collectors.toMap(Function.identity(), place -> 1, Integer::sum), Multiset::new);
+    }
+
+    public Stream<K> stream() {
+        return this.map.entrySet().stream()
+                .flatMap(entry -> IntStream.rangeClosed(1, entry.getValue()).mapToObj(i -> entry.getKey()));
+    }
+
+    public boolean equals(Set<K> set) {
+        return this.map.keySet().equals(set) && Set.copyOf(this.map.values()).equals(Set.of(1));
+    }
+
+    public Set<K> elements() {
+        return Collections.unmodifiableSet(this.map.keySet());
+    }
+
+    public String toString(final BiFunction<? super K, ? super Integer, String> f,
+                           final CharSequence delimiter, final CharSequence prefix, final CharSequence suffix) {
+        return this.map.entrySet().stream()
+                .map(e -> f.apply(e.getKey(), e.getValue()))
+                .collect(Collectors.joining(delimiter, prefix, suffix));
+    }
+
+    public String toString(final BiFunction<? super K, ? super Integer, String> f) {
+        return toString(f, ", ", "{", "}");
+    }
+
+    public String toString(final Function<? super K, String> f) {
+        return toString((element, count) -> count + "x " + f.apply(element), ", ", "{", "}");
+    }
+
+    @Override
+    public String toString() {
+        return this.toString(Object::toString);
+    }
+}

src/uniolunisaar/adam/logic/synthesis/builder/symbolic/bddapproach/distrenv/DistrEnvBDDGlobalSafetyPetriGameStrategyBuilder.java

@@ -10,8 +10,11 @@
 import java.util.Optional;
 import java.util.Queue;
 import java.util.Set;
+import java.util.stream.Collector;
 import java.util.stream.Collectors;
-import uniol.apt.adt.Node;
+import java.util.stream.LongStream;
+import java.util.stream.Stream;
+import uniol.apt.adt.pn.Node;
 import uniol.apt.adt.pn.Flow;
 import uniol.apt.adt.pn.Marking;
 import uniol.apt.adt.pn.PetriNet;
@@ -22,7 +25,9 @@
 import uniolunisaar.adam.ds.graph.synthesis.twoplayergame.symbolic.bddapproach.BDDState;
 import uniolunisaar.adam.ds.petrinet.PetriNetExtensionHandler;
 import uniolunisaar.adam.ds.synthesis.pgwt.PetriGameWithTransits;
+import uniolunisaar.adam.ds.synthesis.solver.symbolic.bddapproach.distrenv.Multiset;
 import uniolunisaar.adam.logic.synthesis.solver.symbolic.bddapproach.distrenv.safety.DistrEnvBDDGlobalSafetySolver;
+import uniolunisaar.adam.tools.Logger;
 import uniolunisaar.adam.util.symbolic.bddapproach.BDDTools;
 
 /**
@@ -86,6 +91,10 @@ public DistrEnvBDDGlobalSafetyPetriGameStrategyBuilder(DistrEnvBDDGlobalSafetySo
         this.graphStrategy = graphStrategy;
         this.game = this.solver.getGame();
         this.petriStrategy = new PetriGameWithTransits("Winning strategy of the system players of the game '" + solver.getGame().getName() + "'.");
+
+        if (!solver.getGame().getBounded().isSafe()) {
+            Logger.getInstance().addWarning("The petri game strategy for a unsafe petri game may be incorrect!");
+        }
     }
 
     public PetriGameWithTransits build() {
@@ -201,7 +210,7 @@ private void onNewVertex(BDDState predecessor, BDDState successor) {
                                 .findAny()
                                 .orElseGet(() -> {
                                     Transition t = newStrategyTransition(transitionInGame);
-                                    //System.out.println(t.getId() + " was created for " + bddStateToString(predecessor) + " -> " + bddStateToString(successor) + ", " + transitionInGame + ", " + cut + ", " + subCut);
+                                    //System.out.println(t.getId() + " was created for " + bddStateToString(predecessor) + " -> " + bddStateToString(successor) + ", " + transitionInGame.getId() + ", " + nodesToString(cut) + ", " + nodesToString(subCut));
                                     for (Place prePlaceInStrategy : subCut) {
                                         this.petriStrategy.createFlow(prePlaceInStrategy, t);
                                     }
@@ -210,7 +219,7 @@ private void onNewVertex(BDDState predecessor, BDDState successor) {
                                     }
                                     return t;
                                 });
-                        Set<Place> successorCut = markingToSet(setToMarking(this.petriStrategy, cut).fireTransitions(transitionInStrategy));
+                        Set<Place> successorCut = fire(cut, transitionInStrategy);
                         this.cuts.computeIfAbsent(successor, state -> new HashSet<>()).add(successorCut);
                     }
                     /*
@@ -227,23 +236,25 @@ public Place lambda(Place placeInStrategy) {
         return this.lambdaPlaces.get(placeInStrategy);
     }
 
-    public Set<Place> lambda(Collection<Place> placesInStrategy) {
+    public Multiset<Place> lambda(Collection<Place> placesInStrategy) {
         return placesInStrategy.stream()
                 .map(this::lambda)
-                .collect(Collectors.toSet());
+                .collect(Multiset.collect());
     }
 
     public Transition lambda(Transition placeInStrategy) {
         return this.lambdaTransitions.get(placeInStrategy);
     }
 
     public Marking lambda(Marking marking) {
-        return setToMarking(this.game, lambda(markingToSet(marking)));
+        return streamMarking(marking)
+                .map(this::lambda)
+                .collect(collectMarking(this.game));
     }
 
     private Set<Place> initialCut() {
         Marking initialMarking = this.game.getInitialMarking();
-        return markingToSet(initialMarking).stream()
+        return streamMarking(initialMarking)
                 .map(this::newStrategyPlace)
                 .peek(placeInStrategy -> placeInStrategy.setInitialToken(1))
                 .collect(Collectors.toSet());
@@ -280,14 +291,24 @@ private Transition newStrategyTransition(Transition transitionInGame) {
         return newTransitionInStrategy;
     }
 
-    public Set<Place> markingToSet(Marking marking) {
+    private Set<Place> fire(Set<Place> preCutInStrategy, Transition transitionInStrategy) {
+        Marking preMarking = preCutInStrategy.stream().collect(collectMarking(this.petriStrategy));
+        Marking postMarking = preMarking.fireTransitions(transitionInStrategy);
+        return streamMarking(postMarking).collect(Collectors.toSet());
+    }
+
+    private static Stream<Place> streamMarking(Marking marking) {
         return marking.getNet().getPlaces().stream()
-                .filter(place -> marking.getToken(place).getValue() >= 1)
-                .collect(Collectors.toSet());
+                .peek(place -> {
+                    assert !marking.getToken(place).isOmega();
+                })
+                .flatMap(place -> LongStream.rangeClosed(1, marking.getToken(place).getValue()).mapToObj(i -> place));
     }
 
-    public Marking setToMarking(PetriNet net, Set<Place> places) {
-        return new Marking(net, places.stream().collect(Collectors.toMap(Node::getId, place -> 1)));
+    private static Collector<Place, ?, Marking> collectMarking(PetriNet net) {
+        return Collectors.collectingAndThen(
+                Collectors.toMap(Node::getId, (Place place) -> 1, Integer::sum),
+                (Map<String, Integer> map) -> new Marking(net, map));
     }
 
     private String cutsToString() {
@@ -299,6 +320,10 @@ private String bddStateToString(BDDState state) {
         return BDDTools.getDecodedDecisionSets(state.getState(), this.solver).replace("-> (successor not defined)", "").replace("\n", "");
     }
 
+    private String nodesToString(Collection<? extends Node> nodes) {
+        return nodes.stream().map(Node::getId).collect(Collectors.joining(", ", "{", "}"));
+    }
+
     private class Edge {
 
         private final BDDState predecessor;