From e76effefb88a8dcc13f79d9ff840b3b3af464adf Mon Sep 17 00:00:00 2001 From: Lukas Panneke Date: Sat, 27 Mar 2021 23:53:31 +0100 Subject: [PATCH 1/4] Build the graph game with multisets This allows solving k-bounded games. --- .../distrenv/DistrEnvBDDSolvingObject.java | 18 +- .../safety/DistrEnvBDDGlobalSafetySolver.java | 338 ++++++++++++------ 2 files changed, 248 insertions(+), 108 deletions(-) diff --git a/src/uniolunisaar/adam/ds/synthesis/solver/symbolic/bddapproach/distrenv/DistrEnvBDDSolvingObject.java b/src/uniolunisaar/adam/ds/synthesis/solver/symbolic/bddapproach/distrenv/DistrEnvBDDSolvingObject.java index c546f30..4b0201e 100644 --- a/src/uniolunisaar/adam/ds/synthesis/solver/symbolic/bddapproach/distrenv/DistrEnvBDDSolvingObject.java +++ b/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> extends BDDSolvingObject { private List systemTransitions, envTransitions; + private Map boundOfPartitions; public DistrEnvBDDSolvingObject(PetriGameWithTransits game, W winCon) throws NotSupportedGameException, NetNotSafeException, NoSuitableDistributionFoundException, InvalidPartitionException { this(game, winCon, false); @@ -46,8 +51,9 @@ public DistrEnvBDDSolvingObject(DistrEnvBDDSolvingObject 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 getBadMarkings() { return this.getGame().getFinalMarkings(); } diff --git a/src/uniolunisaar/adam/logic/synthesis/solver/symbolic/bddapproach/distrenv/safety/DistrEnvBDDGlobalSafetySolver.java b/src/uniolunisaar/adam/logic/synthesis/solver/symbolic/bddapproach/distrenv/safety/DistrEnvBDDGlobalSafetySolver.java index 6ba5f7c..a5d7acc 100644 --- a/src/uniolunisaar/adam/logic/synthesis/solver/symbolic/bddapproach/distrenv/safety/DistrEnvBDDGlobalSafetySolver.java +++ b/src/uniolunisaar/adam/logic/synthesis/solver/symbolic/bddapproach/distrenv/safety/DistrEnvBDDGlobalSafetySolver.java @@ -4,6 +4,7 @@ import java.util.Arrays; import java.util.Collection; import java.util.Collections; +import java.util.LinkedHashMap; import java.util.LinkedList; import java.util.List; import java.util.Map; @@ -11,16 +12,21 @@ import java.util.Set; import java.util.StringJoiner; import java.util.function.Function; +import java.util.function.LongUnaryOperator; import java.util.stream.Collector; import java.util.stream.Collectors; import java.util.stream.IntStream; +import java.util.stream.LongStream; +import java.util.stream.Stream; import net.sf.javabdd.BDD; import net.sf.javabdd.BDDDomain; import org.apache.commons.collections4.CollectionUtils; import uniol.apt.adt.pn.Marking; import uniol.apt.adt.pn.Place; +import uniol.apt.adt.pn.Token; import uniol.apt.adt.pn.Transition; import uniolunisaar.adam.ds.objectives.global.GlobalSafety; +import uniolunisaar.adam.ds.petrinet.PetriNetExtensionHandler; import uniolunisaar.adam.ds.synthesis.pgwt.PetriGameWithTransits; import uniolunisaar.adam.ds.synthesis.solver.symbolic.bddapproach.distrenv.DistrEnvBDDSolverOptions; import uniolunisaar.adam.ds.synthesis.solver.symbolic.bddapproach.distrenv.DistrEnvBDDSolvingObject; @@ -28,9 +34,13 @@ import uniolunisaar.adam.exceptions.synthesis.pgwt.NoStrategyExistentException; import uniolunisaar.adam.logic.synthesis.builder.symbolic.bddapproach.distrenv.DistrEnvBDDGlobalSafetyPetriGameStrategyBuilder; import uniolunisaar.adam.logic.synthesis.builder.twoplayergame.symbolic.bddapproach.BDDGraphAndGStrategyBuilder; +import uniolunisaar.adam.logic.synthesis.pgwt.calculators.CalculatorIDs; +import uniolunisaar.adam.logic.synthesis.pgwt.calculators.ConcurrencyPreservingGamesCalculator; import uniolunisaar.adam.logic.synthesis.solver.symbolic.bddapproach.BDDSolver; import uniolunisaar.adam.logic.synthesis.solver.symbolic.bddapproach.distrenv.DistrEnvBDDSolver; +import uniolunisaar.adam.logic.synthesis.solver.symbolic.bddapproach.distrenv.DistrEnvBDDSolverFactory; import uniolunisaar.adam.tools.Logger; +import uniolunisaar.adam.util.PGTools; import uniolunisaar.adam.util.benchmarks.synthesis.Benchmarks; import uniolunisaar.adam.util.symbolic.bddapproach.BDDTools; @@ -133,12 +143,14 @@ public class DistrEnvBDDGlobalSafetySolver extends DistrEnvBDDSolver and() { protected void createVariables() { int numberOfPartitions = this.getSolvingObject().getMaxTokenCountInt(); PLACES = new BDDDomain[2][numberOfPartitions]; + PLACE_MULTIPLICITY = new BDDDomain[2][numberOfPartitions]; TRANSITIONS = new BDDDomain[2]; TOP = new BDDDomain[2]; - RESPONSIBILITY = new BDDDomain[2]; + RESPONSIBILITY_MULTIPLICITY = new BDDDomain[2][numberOfPartitions]; + for (int pos : List.of(PREDECESSOR, SUCCESSOR)) { for (int partition = 0; partition < numberOfPartitions; partition++) { PLACES[pos][partition] = this.getFactory().extDomain( this.getSolvingObject().getDevidedPlaces()[partition].size() + (this.getSolvingObject().isConcurrencyPreserving() ? 0 : 1)); - - /* for every system transition the system player must choose whether or not to allow that transition. */ - TRANSITIONS[pos] = this.getFactory().extDomain(BigInteger.TWO.pow(this.getSolvingObject().getSystemTransitions().size())); - TOP[pos] = this.getFactory().extDomain(2); - RESPONSIBILITY[pos] = this.getFactory().extDomain(BigInteger.TWO.pow(numberOfPartitions)); + PLACE_MULTIPLICITY[pos][partition] = this.getFactory().extDomain(this.getSolvingObject().getBoundOfPartition(partition) + 1); + RESPONSIBILITY_MULTIPLICITY[pos][partition] = this.getFactory().extDomain(this.getSolvingObject().getBoundOfPartition(partition) + 1); } + /* for every system transition the system player must choose whether or not to allow that transition. */ + TRANSITIONS[pos] = this.getFactory().extDomain(BigInteger.TWO.pow(this.getSolvingObject().getSystemTransitions().size())); + TOP[pos] = this.getFactory().extDomain(2); } setDCSLength(getFactory().varNum() / 2); // TODO what is this? } @@ -204,9 +218,14 @@ protected void createVariables() { @Override protected BDD getVariables(int pos) { return TOP[pos].set() - .and(TRANSITIONS[pos].set()) - .and(RESPONSIBILITY[pos].set()) - .and(Arrays.stream(PLACES[pos]) + .andWith(TRANSITIONS[pos].set()) + .andWith(Arrays.stream(PLACES[pos]) + .map(BDDDomain::set) + .collect(and())) + .andWith(Arrays.stream(PLACE_MULTIPLICITY[pos]) + .map(BDDDomain::set) + .collect(and())) + .andWith(Arrays.stream(RESPONSIBILITY_MULTIPLICITY[pos]) .map(BDDDomain::set) .collect(and())); } @@ -214,10 +233,15 @@ protected BDD getVariables(int pos) { @Override protected BDD preBimpSucc() { return TOP[PREDECESSOR].buildEquals(TOP[SUCCESSOR]) - .and(TRANSITIONS[PREDECESSOR].buildEquals(TRANSITIONS[SUCCESSOR])) - .and(RESPONSIBILITY[PREDECESSOR].buildEquals(RESPONSIBILITY[SUCCESSOR])) - .and(this.streamPartitions() + .andWith(TRANSITIONS[PREDECESSOR].buildEquals(TRANSITIONS[SUCCESSOR])) + .andWith(this.streamPartitions() .mapToObj(partition -> PLACES[PREDECESSOR][partition].buildEquals(PLACES[SUCCESSOR][partition])) + .collect(and())) + .andWith(this.streamPartitions() + .mapToObj(partition -> PLACE_MULTIPLICITY[PREDECESSOR][partition].buildEquals(PLACE_MULTIPLICITY[SUCCESSOR][partition])) + .collect(and())) + .andWith(this.streamPartitions() + .mapToObj(partition -> RESPONSIBILITY_MULTIPLICITY[PREDECESSOR][partition].buildEquals(RESPONSIBILITY_MULTIPLICITY[SUCCESSOR][partition])) .collect(and())); } @@ -228,10 +252,6 @@ private BDD codeSystemTransition(Transition transition, int pos) { return this.getFactory().ithVar(TRANSITIONS[pos].vars()[transitionIndex]); } - protected BDD codeResponsibility(int partition, int pos) { - return this.getFactory().ithVar(RESPONSIBILITY[pos].vars()[partition]); - } - protected IntStream streamPartitions() { return streamPartitions(true); } @@ -248,7 +268,8 @@ protected BDD graphGame_initialVertex(int pos) { */ .andWith(top(pos).biimpWith(tokenExists(PARTITION_OF_SYSTEM_PLAYER, pos))) .andWith(nothingChosen(pos)) - .andWith(onlySystemInResponsibilitySet(PREDECESSOR)); + .andWith(onlySystemInResponsibilitySet(PREDECESSOR)) + .andWith(responsibilityContainsSystem(PREDECESSOR)); } /** @@ -320,34 +341,57 @@ protected BDD graphGame_player1Edge_purelyEnvironmentalTransition(Transition tra ret.andWith(commitmentsEqual()); } - BDD add, remove = transition.getPreset().stream() - .map(this.getGame()::getPartition) - .map(partition -> codeResponsibility(partition, SUCCESSOR)) - .collect(and()); - if (createsNewSystemToken) { - /* - * if this transition creates a new system token, - * choose that as the new entry to the responsibility set. - * otherwise there is no way for the system token to add the system in the future, - * meaning that no system transition can ever fire. - */ - add = codeResponsibility(PARTITION_OF_SYSTEM_PLAYER, SUCCESSOR); - } else { - /* - * if no system token is created, choose a random token. - */ - add = transition.getPostset().stream() - .map(this.getGame()::getPartition) - .map(partition -> codeResponsibility(partition, SUCCESSOR)) - .collect(xor()); - } - ret.andWith(responsibilitiesEqual().exist(remove).andWith(remove.not()).exist(add).andWith(add)); + ret.andWith(updateResponsibilityOnPurelyEnvironmentalEdge(transition, createsNewSystemToken)); ret.andWith(responsibilitySubsetMarking(SUCCESSOR)); ret.andWith(fire(transition)); return ret; } + private BDD updateResponsibilityOnPurelyEnvironmentalEdge(Transition transition, boolean createsNewSystemToken) { + PetriGameWithTransits game = this.getSolvingObject().getGame(); + + Set pre = transition.getPreset(); + Set post = transition.getPostset(); + + Map prePartitionToPlace = pre.stream() + .collect(Collectors.toMap(game::getPartition, Function.identity())); + Map postPartitionToPlace = post.stream() + .collect(Collectors.toMap(game::getPartition, Function.identity())); + + Set prePartitions = pre.stream() + .map(game::getPartition) + .collect(Collectors.toSet()); + Set postPartitions = post.stream() + .map(game::getPartition) + .collect(Collectors.toSet()); + /* + * if this transition creates a new system token, + * choose that as the new entry to the responsibility set. + * otherwise there is no way for the system token to add the system in the future, + * meaning that no system transition can ever fire. + * if no system token is created, choose a random token nondeterministically. + */ + return (createsNewSystemToken ? Stream.of(PARTITION_OF_SYSTEM_PLAYER) : postPartitions.stream()) + .map(chosenPartition -> this.streamPartitions(true) + .mapToObj(partition -> { + if (prePartitions.contains(partition)) { + Place prePlace = prePartitionToPlace.get(partition); + int consumeWeight = this.getGame().getFlow(prePlace, transition).getWeight(); + return updateResponsibility(partition, 0, bound(prePlace), + r -> Math.max(0, r - consumeWeight) + (partition == chosenPartition ? 1 : 0)); + } else { + if (partition == chosenPartition) { + return updateResponsibility(partition, 0, bound(postPartitionToPlace.get(partition)) - 1, r -> r + 1); + } else { + return responsibilitiesEqual(partition); + } + } + }) + .collect(and())) + .collect(xor()); + } + /** * In the paper these are the edges of type E3. */ @@ -369,13 +413,17 @@ protected BDD graphGame_player1Edge_systemTransition(Transition transition) { ret.andWith(nothingChosen(SUCCESSOR)); ret.andWith(fire(transition)); - Set prePartitions = transition.getPreset().stream() - .map(this.getGame()::getPartition) - .collect(Collectors.toSet()); - BDD responsibilitySubsetPreset = this.streamPartitions(false) - .filter(partition -> !prePartitions.contains(partition)) - .mapToObj(partition -> codeResponsibility(partition, PREDECESSOR).not()) + Map prePartitionToPlace = transition.getPreset().stream() + .collect(Collectors.toMap(this.getGame()::getPartition, Function.identity())); + BDD responsibilitySubsetPreset = this.streamPartitions(true) + .mapToObj(partition -> { + int weight = Optional.ofNullable(prePartitionToPlace.get(partition)) + .map(place -> this.getGame().getFlow(place, transition).getWeight()) + .orElse(0); + return codeResponsibilityAtMost(partition, PREDECESSOR, weight); + }) .collect(and()); + ret.andWith(responsibilitySubsetPreset); ret.andWith(onlySystemInResponsibilitySet(SUCCESSOR)); @@ -501,6 +549,10 @@ protected BDD graphGame_winningVertices() throws CalculationInterruptedException return reachableVertices.and(poisonedVertices.not().andWith(wellformed())); } + protected long bound(Place place) { + return PetriNetExtensionHandler.getBoundedness(place); + } + protected BDD fire(Transition transition) { PetriGameWithTransits game = this.getSolvingObject().getGame(); @@ -519,49 +571,47 @@ protected BDD fire(Transition transition) { .map(game::getPartition) .collect(Collectors.toSet()); - /* partitions that had a token before the transition has fired, but don't have one afterwards */ - /* CP => nothing consumed */ - assert !getSolvingObject().isConcurrencyPreserving() || CollectionUtils.subtract(prePartitions, postPartitions).isEmpty(); - BDD consumed = CollectionUtils.subtract(prePartitions, postPartitions).stream() - .map(partition -> codePlace(prePartitionToPlace.get(partition), PREDECESSOR, partition).andWith(notUsedToken(SUCCESSOR, partition))) - .collect(and()); - /* - * notUsedToken(SUCCESSOR, partition) is equal to codePlace(0, SUCCESSOR, partition). - * This could be problematic, because in the concurrency preserving case - * the place id 0 does refer to an actual place. - * But in the concurrency preserving case - * no token can ever be taken out of a partition, - * but only be moved within the partition. - * Thus there can never ba a partition without a token - * and this code is never executed when it could be problematic. - */ - - /* partitions that had no token before the transition has fired, but have one afterwards */ - /* CP => nothing produced */ - assert !getSolvingObject().isConcurrencyPreserving() || CollectionUtils.subtract(postPartitions, prePartitions).isEmpty(); - BDD produced = CollectionUtils.subtract(postPartitions, prePartitions).stream() - .map(partition -> notUsedToken(PREDECESSOR, partition).andWith(codePlace(postPartitionToPlace.get(partition), SUCCESSOR, partition))) - .collect(and()); - - /* partitions that have a token before and after the transition fires */ - BDD moved = CollectionUtils.intersection(postPartitions, prePartitions).stream() - .map(partition -> codePlace(prePartitionToPlace.get(partition), PREDECESSOR, partition).andWith(codePlace(postPartitionToPlace.get(partition), SUCCESSOR, partition))) + BDD flows = this.streamPartitions(true) + .mapToObj(partition -> { + if (prePartitions.contains(partition) && postPartitions.contains(partition)) { + /* moves the token within a partition. That means between two different places, or on the same place */ + Place prePlace = prePartitionToPlace.get(partition); + Place postPlace = postPartitionToPlace.get(partition); + int consumeWeight = this.getGame().getFlow(prePlace, transition).getWeight(); + int produceWeight = this.getGame().getFlow(transition, postPlace).getWeight(); + BDD ret = codePlace(prePlace, PREDECESSOR, partition) + .andWith(codePlace(postPlace, SUCCESSOR, partition)); + if (prePlace.equals(postPlace)) { + /* can still change the number of tokens, but not to 0. */ + return ret.andWith(updatePlaceMultiplicity(partition, consumeWeight, Math.min(bound(prePlace), bound(postPlace) + produceWeight), + r -> r - consumeWeight + produceWeight)); + } else { + /* prePlace looses all tokens, postPlace had none and now gains some tokens. */ + return ret.andWith(codePlaceMultiplicity(partition, PREDECESSOR, consumeWeight)) + .andWith(codePlaceMultiplicity(partition, SUCCESSOR, produceWeight)); + } + } else if (prePartitions.contains(partition)) { + /* up to all tokens are removed from this partition */ + Place prePlace = prePartitionToPlace.get(partition); + int consumeWeight = this.getGame().getFlow(prePlace, transition).getWeight(); + return codePlace(prePlace, PREDECESSOR, partition, consumeWeight) + .andWith(notUsedToken(SUCCESSOR, partition)) + .andWith(codePlaceMultiplicity(partition, SUCCESSOR, 0)) + .orWith(updatePlace(prePlace, prePlace, partition, consumeWeight + 1, bound(prePlace), m -> m - consumeWeight)); + } else if (postPartitions.contains(partition)) { + /* previously this partition had at least 0 tokens, now there is at least 1. */ + Place postPlace = postPartitionToPlace.get(partition); + int produceWeight = this.getGame().getFlow(transition, postPlace).getWeight(); + return notUsedToken(PREDECESSOR, partition) + .andWith(codePlaceMultiplicity(partition, PREDECESSOR, 0)) + .andWith(codePlace(postPlace, SUCCESSOR, partition, produceWeight)) + .orWith(updatePlace(postPlace, postPlace, partition, 1, bound(postPlace) - produceWeight, m -> m + produceWeight)); + } else { + /* this partition is not attached to the transition, everything stays the same */ + return markingEqual(partition).andWith(onlyExistingPlacesInMarking(PREDECESSOR)); + } + }) .collect(and()); - - /* partitions that have no contact with the transition */ - BDD unaffected = this.streamPartitions() - .filter(o -> !prePartitions.contains(o)) - .filter(o -> !postPartitions.contains(o)) - .mapToObj(this::markingEqual) - .collect(and()) - .andWith(onlyExistingPlacesInMarking(PREDECESSOR)) - .andWith(onlyExistingPlacesInMarking(SUCCESSOR)); - - BDD flows = consumed - .andWith(produced) - .andWith(moved) - .andWith(unaffected); - return enabled(transition, PREDECESSOR).andWith(flows); } @@ -641,6 +691,12 @@ protected BDD onlyExistingPlacesInMarking(int pos) { .collect(and()); } + protected BDD unmarkedPlaceIffMultiplicityZero(int pos) { + return this.streamPartitions(true) + .mapToObj(partition -> tokenExists(partition, pos).biimpWith(codePlaceMultiplicity(partition, pos, 0).not())) + .collect(and()); + } + protected BDD tokenExists(int partition, int pos) { if (this.getSolvingObject().isConcurrencyPreserving()) { return getOne(); @@ -650,12 +706,13 @@ protected BDD tokenExists(int partition, int pos) { } protected BDD markingEqual(int partition) { - return PLACES[PREDECESSOR][partition].buildEquals(PLACES[SUCCESSOR][partition]); + return PLACES[PREDECESSOR][partition].buildEquals(PLACES[SUCCESSOR][partition]) + .andWith(PLACE_MULTIPLICITY[PREDECESSOR][partition].buildEquals(PLACE_MULTIPLICITY[SUCCESSOR][partition])); } protected BDD markingsEqual() { return this.streamPartitions() - .mapToObj(partition -> markingEqual(partition)) + .mapToObj(this::markingEqual) .collect(and()); } @@ -673,24 +730,32 @@ protected BDD somethingChosen(int pos) { .collect(or()); } + protected BDD responsibilitiesEqual(int partition) { + return RESPONSIBILITY_MULTIPLICITY[PREDECESSOR][partition].buildEquals(RESPONSIBILITY_MULTIPLICITY[SUCCESSOR][partition]); + } + protected BDD responsibilitiesEqual() { - return RESPONSIBILITY[PREDECESSOR].buildEquals(RESPONSIBILITY[SUCCESSOR]); + return this.streamPartitions(true) + .mapToObj(this::responsibilitiesEqual) + .collect(and()); } protected BDD onlySystemInResponsibilitySet(int pos) { - return codeResponsibility(PARTITION_OF_SYSTEM_PLAYER, pos).biimpWith(tokenExists(PARTITION_OF_SYSTEM_PLAYER, pos)) - .andWith(this.streamPartitions(false) - .mapToObj(partition -> codeResponsibility(partition, pos).not()) - .collect(and())); + return responsibilityContainsSystem(pos).andWith(this.streamPartitions(false) + .mapToObj(partition -> codeResponsibility(partition, pos, 0)) + .collect(and())); } protected BDD responsibilityContainsSystem(int pos) { - return codeResponsibility(PARTITION_OF_SYSTEM_PLAYER, pos).biimpWith(tokenExists(PARTITION_OF_SYSTEM_PLAYER, pos)); + return tokenExists(PARTITION_OF_SYSTEM_PLAYER, pos).biimpWith(codeResponsibility(PARTITION_OF_SYSTEM_PLAYER, pos, 1)); } protected BDD responsibilitySubsetMarking(int pos) { - return this.streamPartitions() - .mapToObj(partition -> codeResponsibility(partition, pos).impWith(tokenExists(partition, pos))) + return this.streamPartitions(true) + .mapToObj(partition -> LongStream.rangeClosed(0, this.getSolvingObject().getBoundOfPartition(partition)) + .mapToObj(multiplicityOfPlace -> PLACE_MULTIPLICITY[pos][partition].ithVar(multiplicityOfPlace) + .impWith(codeResponsibilityAtMost(partition, pos, multiplicityOfPlace))) + .collect(and())) .collect(and()); } @@ -729,6 +794,7 @@ protected BDD wellformed(int pos) { /* only places that exist may be encoded */ BDD ret = getOne(); ret.andWith(onlyExistingPlacesInMarking(pos)); + ret.andWith(unmarkedPlaceIffMultiplicityZero(pos)); /* * only transitions in the postset of the system player may be in the commitment. * in top states there is no commitment set, thus there are no constraints on it. @@ -765,10 +831,10 @@ protected BDD codeMarking(Marking marking, int pos, boolean encodeMissingToken) .mapToObj(partition -> { Optional place = getPlaceOfPartitionInMarking(marking, partition); if (place.isPresent()) { - return codePlace(place.get(), pos, partition); + return codePlace(place.get(), pos, partition, marking.getToken(place.get())); } else if (encodeMissingToken) { assert !this.getSolvingObject().isConcurrencyPreserving(); - return notUsedToken(pos, partition); + return notUsedToken(pos, partition).andWith(codePlaceMultiplicity(partition, pos, 0)); } else { return getOne(); } @@ -814,6 +880,58 @@ protected BDD enabled(Transition transition, int pos) { .collect(and()); } + protected BDD codePlace(Place place, int pos, int partition, long multiplicity) { + return super.codePlace(place, pos, partition).andWith(codePlaceMultiplicity(partition, pos, multiplicity)); + } + + protected BDD codePlace(Place place, int pos, int partition, int multiplicity) { + return super.codePlace(place, pos, partition).andWith(codePlaceMultiplicity(partition, pos, multiplicity)); + } + + protected BDD codePlace(Place place, int pos, int partition, Token multiplicity) { + assert !multiplicity.isOmega(); + return super.codePlace(place, pos, partition).andWith(codePlaceMultiplicity(partition, pos, multiplicity.getValue())); + } + + protected BDD codePlaceMultiplicity(int partition, int pos, long multiplicity) { + return PLACE_MULTIPLICITY[pos][partition].ithVar(multiplicity); + } + + protected BDD codeResponsibility(int partition, int pos, long multiplicity) { + return RESPONSIBILITY_MULTIPLICITY[pos][partition].ithVar(multiplicity); + } + + protected BDD codeResponsibilityAtMost(int partition, int pos, long maxMultiplicity) { + return range(RESPONSIBILITY_MULTIPLICITY[pos][partition], 0, maxMultiplicity); + } + + private BDD range(BDDDomain domain, long startInclusive, long endInclusive) { + return LongStream.rangeClosed(startInclusive, endInclusive) + .mapToObj(domain::ithVar) + .collect(or()); + } + + private BDD updateResponsibility(int partition, long preMin, long preMax, LongUnaryOperator post) { + return LongStream.rangeClosed(preMin, preMax) + .mapToObj(pre -> codeResponsibility(partition, PREDECESSOR, pre) + .andWith(codeResponsibility(partition, SUCCESSOR, post.applyAsLong(pre)))) + .collect(or()); + } + + private BDD updatePlaceMultiplicity(int partition, long preMin, long preMax, LongUnaryOperator post) { + return LongStream.rangeClosed(preMin, preMax) + .mapToObj(pre -> codePlaceMultiplicity(partition, PREDECESSOR, pre) + .andWith(codePlaceMultiplicity(partition, SUCCESSOR, post.applyAsLong(pre)))) + .collect(or()); + } + + private BDD updatePlace(Place prePlace, Place postPlace, int partition, long preMin, long preMax, LongUnaryOperator post) { + return LongStream.rangeClosed(preMin, preMax) + .mapToObj(pre -> codePlace(prePlace, PREDECESSOR, partition, pre) + .andWith(codePlace(postPlace, SUCCESSOR, partition, post.applyAsLong(pre)))) + .collect(or()); + } + /* */ @Override @@ -984,21 +1102,25 @@ private static String commitmentToConciseString(Map> c return sj.toString(); } - private Map decodeResponsibility(byte[] dcs, int pos) { + private Map decodeResponsibility(byte[] dcs, int pos) { return this.streamPartitions() .boxed() - .collect(Collectors.toMap(Function.identity(), partition -> dcs[RESPONSIBILITY[pos].vars()[partition]])); + .collect(Collectors.toMap(Function.identity(), partition -> decodeInteger(dcs, RESPONSIBILITY_MULTIPLICITY[pos][partition]))); } protected String decodeVertex(byte[] dcs, int pos) { boolean verbose = false; - Map responsibility = decodeResponsibility(dcs, pos); + Map responsibility = decodeResponsibility(dcs, pos); String systemPlayer = decodePlayer(dcs, pos, PARTITION_OF_SYSTEM_PLAYER); - assert responsibility.get(PARTITION_OF_SYSTEM_PLAYER) == 1 ^ systemPlayer.equals("-") : "System player " + systemPlayer + " is not in responsibility set " + responsibility; + //assert responsibility.get(PARTITION_OF_SYSTEM_PLAYER) == 1 ^ systemPlayer.equals("-") : "System player " + systemPlayer + " is not in responsibility set " + responsibility; String stringifiedEnvPlayerPlaces = IntStream.range(1, this.getSolvingObject().getMaxTokenCountInt()) .mapToObj(partition -> { StringBuilder sb = new StringBuilder(); String player = decodePlayer(dcs, pos, partition); + int multiplicity = decodeInteger(dcs, PLACE_MULTIPLICITY[pos][partition]); + if (verbose || !player.equals("-")) { + sb.append(multiplicity).append("x "); + } sb.append(player); if (verbose || !player.equals("-")) { sb.append(":").append(responsibility.get(partition)); @@ -1007,7 +1129,11 @@ protected String decodeVertex(byte[] dcs, int pos) { }) .collect(Collectors.joining(", ")); StringBuilder ret = new StringBuilder(); - ret.append("(s: ").append(systemPlayer); + ret.append("(s: "); + if (verbose) { + ret.append(decodeInteger(dcs, PLACE_MULTIPLICITY[pos][PARTITION_OF_SYSTEM_PLAYER])).append("x "); + } + ret.append(systemPlayer); if (verbose) { ret.append(":").append(responsibility.get(PARTITION_OF_SYSTEM_PLAYER)); } From 7e87867567c7c460804ddd5da5381323addd9e94 Mon Sep 17 00:00:00 2001 From: Lukas Panneke Date: Mon, 29 Mar 2021 20:38:03 +0200 Subject: [PATCH 2/4] Build the petri game strategy with multisets --- .../bddapproach/distrenv/Multiset.java | 72 +++++++++++++++++++ ...DGlobalSafetyPetriGameStrategyBuilder.java | 44 ++++++++---- 2 files changed, 104 insertions(+), 12 deletions(-) create mode 100644 src/uniolunisaar/adam/ds/synthesis/solver/symbolic/bddapproach/distrenv/Multiset.java diff --git a/src/uniolunisaar/adam/ds/synthesis/solver/symbolic/bddapproach/distrenv/Multiset.java b/src/uniolunisaar/adam/ds/synthesis/solver/symbolic/bddapproach/distrenv/Multiset.java new file mode 100644 index 0000000..964ad9a --- /dev/null +++ b/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 { + private final Map map; + + private Multiset(Map 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 set) { + return set.stream().allMatch(this::contains); + } + + public static Collector> collect() { + return Collectors.collectingAndThen(Collectors.toMap(Function.identity(), place -> 1, Integer::sum), Multiset::new); + } + + public Stream stream() { + return this.map.entrySet().stream() + .flatMap(entry -> IntStream.rangeClosed(1, entry.getValue()).mapToObj(i -> entry.getKey())); + } + + public boolean equals(Set set) { + return this.map.keySet().equals(set) && Set.copyOf(this.map.values()).equals(Set.of(1)); + } + + public Set elements() { + return Collections.unmodifiableSet(this.map.keySet()); + } + + public String toString(final BiFunction 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 f) { + return toString(f, ", ", "{", "}"); + } + + public String toString(final Function f) { + return toString((element, count) -> count + "x " + f.apply(element), ", ", "{", "}"); + } + + @Override + public String toString() { + return this.toString(Object::toString); + } +} diff --git a/src/uniolunisaar/adam/logic/synthesis/builder/symbolic/bddapproach/distrenv/DistrEnvBDDGlobalSafetyPetriGameStrategyBuilder.java b/src/uniolunisaar/adam/logic/synthesis/builder/symbolic/bddapproach/distrenv/DistrEnvBDDGlobalSafetyPetriGameStrategyBuilder.java index 8e7150e..2b742c3 100644 --- a/src/uniolunisaar/adam/logic/synthesis/builder/symbolic/bddapproach/distrenv/DistrEnvBDDGlobalSafetyPetriGameStrategyBuilder.java +++ b/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,6 +25,7 @@ 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.util.symbolic.bddapproach.BDDTools; @@ -201,7 +205,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 +214,7 @@ private void onNewVertex(BDDState predecessor, BDDState successor) { } return t; }); - Set successorCut = markingToSet(setToMarking(this.petriStrategy, cut).fireTransitions(transitionInStrategy)); + Set successorCut = fire(cut, transitionInStrategy); this.cuts.computeIfAbsent(successor, state -> new HashSet<>()).add(successorCut); } /* @@ -227,10 +231,10 @@ public Place lambda(Place placeInStrategy) { return this.lambdaPlaces.get(placeInStrategy); } - public Set lambda(Collection placesInStrategy) { + public Multiset lambda(Collection placesInStrategy) { return placesInStrategy.stream() .map(this::lambda) - .collect(Collectors.toSet()); + .collect(Multiset.collect()); } public Transition lambda(Transition placeInStrategy) { @@ -238,12 +242,14 @@ public Transition lambda(Transition 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 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 +286,24 @@ private Transition newStrategyTransition(Transition transitionInGame) { return newTransitionInStrategy; } - public Set markingToSet(Marking marking) { + private Set fire(Set 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 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 places) { - return new Marking(net, places.stream().collect(Collectors.toMap(Node::getId, place -> 1))); + private static Collector collectMarking(PetriNet net) { + return Collectors.collectingAndThen( + Collectors.toMap(Node::getId, (Place place) -> 1, Integer::sum), + (Map map) -> new Marking(net, map)); } private String cutsToString() { @@ -299,6 +315,10 @@ private String bddStateToString(BDDState state) { return BDDTools.getDecodedDecisionSets(state.getState(), this.solver).replace("-> (successor not defined)", "").replace("\n", ""); } + private String nodesToString(Collection nodes) { + return nodes.stream().map(Node::getId).collect(Collectors.joining(", ", "{", "}")); + } + private class Edge { private final BDDState predecessor; From 7ff264c08a3a63aca76e75ce4298c1e33980b40e Mon Sep 17 00:00:00 2001 From: Lukas Panneke Date: Wed, 7 Apr 2021 18:30:13 +0200 Subject: [PATCH 3/4] Add todo for unnecessary variables --- .../safety/DistrEnvBDDGlobalSafetySolver.java | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/uniolunisaar/adam/logic/synthesis/solver/symbolic/bddapproach/distrenv/safety/DistrEnvBDDGlobalSafetySolver.java b/src/uniolunisaar/adam/logic/synthesis/solver/symbolic/bddapproach/distrenv/safety/DistrEnvBDDGlobalSafetySolver.java index a5d7acc..388c1d2 100644 --- a/src/uniolunisaar/adam/logic/synthesis/solver/symbolic/bddapproach/distrenv/safety/DistrEnvBDDGlobalSafetySolver.java +++ b/src/uniolunisaar/adam/logic/synthesis/solver/symbolic/bddapproach/distrenv/safety/DistrEnvBDDGlobalSafetySolver.java @@ -4,7 +4,6 @@ import java.util.Arrays; import java.util.Collection; import java.util.Collections; -import java.util.LinkedHashMap; import java.util.LinkedList; import java.util.List; import java.util.Map; @@ -34,13 +33,9 @@ import uniolunisaar.adam.exceptions.synthesis.pgwt.NoStrategyExistentException; import uniolunisaar.adam.logic.synthesis.builder.symbolic.bddapproach.distrenv.DistrEnvBDDGlobalSafetyPetriGameStrategyBuilder; import uniolunisaar.adam.logic.synthesis.builder.twoplayergame.symbolic.bddapproach.BDDGraphAndGStrategyBuilder; -import uniolunisaar.adam.logic.synthesis.pgwt.calculators.CalculatorIDs; -import uniolunisaar.adam.logic.synthesis.pgwt.calculators.ConcurrencyPreservingGamesCalculator; import uniolunisaar.adam.logic.synthesis.solver.symbolic.bddapproach.BDDSolver; import uniolunisaar.adam.logic.synthesis.solver.symbolic.bddapproach.distrenv.DistrEnvBDDSolver; -import uniolunisaar.adam.logic.synthesis.solver.symbolic.bddapproach.distrenv.DistrEnvBDDSolverFactory; import uniolunisaar.adam.tools.Logger; -import uniolunisaar.adam.util.PGTools; import uniolunisaar.adam.util.benchmarks.synthesis.Benchmarks; import uniolunisaar.adam.util.symbolic.bddapproach.BDDTools; @@ -205,6 +200,11 @@ protected void createVariables() { PLACES[pos][partition] = this.getFactory().extDomain( this.getSolvingObject().getDevidedPlaces()[partition].size() + (this.getSolvingObject().isConcurrencyPreserving() ? 0 : 1)); + /* + * TODO don't create these variables if the game is safe, + * because then the multiplicity is 0 iff the partition is unmarked + * and 1 iff the partition is marked. + */ PLACE_MULTIPLICITY[pos][partition] = this.getFactory().extDomain(this.getSolvingObject().getBoundOfPartition(partition) + 1); RESPONSIBILITY_MULTIPLICITY[pos][partition] = this.getFactory().extDomain(this.getSolvingObject().getBoundOfPartition(partition) + 1); } @@ -212,7 +212,7 @@ protected void createVariables() { TRANSITIONS[pos] = this.getFactory().extDomain(BigInteger.TWO.pow(this.getSolvingObject().getSystemTransitions().size())); TOP[pos] = this.getFactory().extDomain(2); } - setDCSLength(getFactory().varNum() / 2); // TODO what is this? + setDCSLength(getFactory().varNum() / 2); } @Override From 460693bf0aff6064463966b9b3ac2e51fabda773 Mon Sep 17 00:00:00 2001 From: Lukas Panneke Date: Wed, 7 Apr 2021 18:34:46 +0200 Subject: [PATCH 4/4] Warn about incorrect petri game strategy fpr unbounded petri games --- .../DistrEnvBDDGlobalSafetyPetriGameStrategyBuilder.java | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/uniolunisaar/adam/logic/synthesis/builder/symbolic/bddapproach/distrenv/DistrEnvBDDGlobalSafetyPetriGameStrategyBuilder.java b/src/uniolunisaar/adam/logic/synthesis/builder/symbolic/bddapproach/distrenv/DistrEnvBDDGlobalSafetyPetriGameStrategyBuilder.java index 2b742c3..aed0a6f 100644 --- a/src/uniolunisaar/adam/logic/synthesis/builder/symbolic/bddapproach/distrenv/DistrEnvBDDGlobalSafetyPetriGameStrategyBuilder.java +++ b/src/uniolunisaar/adam/logic/synthesis/builder/symbolic/bddapproach/distrenv/DistrEnvBDDGlobalSafetyPetriGameStrategyBuilder.java @@ -27,6 +27,7 @@ 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; /** @@ -90,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() {