diff --git a/src/storm/builder/DdJaniModelBuilder.cpp b/src/storm/builder/DdJaniModelBuilder.cpp
index f5ae8e13a..48496b352 100644
--- a/src/storm/builder/DdJaniModelBuilder.cpp
+++ b/src/storm/builder/DdJaniModelBuilder.cpp
@@ -1515,7 +1515,7 @@ namespace storm {
// Keep track of the fragment of transient assignments.
for (auto const& transientAssignment : currentEdge.transientEdgeAssignments) {
- addToTransientAssignmentMap(transientAssignments, transientAssignment.first, remainingGuardChoicesIntersection.template toAdd<ValueType>() * transientAssignment.second * indicesEncodedWithLocalNondeterminismVariables[k].first.template toAdd<ValueType>());
+ addToTransientAssignmentMap(transientAssignments, transientAssignment.first, remainingGuardChoicesIntersection.template toAdd<ValueType>() * transientAssignment.second * indicesEncodedWithLocalNondeterminismVariables[k].second);
}
// Keep track of the written global variables of the fragment.
diff --git a/src/storm/builder/ExplicitModelBuilder.cpp b/src/storm/builder/ExplicitModelBuilder.cpp
index 6467793c6..986e04ae7 100644
--- a/src/storm/builder/ExplicitModelBuilder.cpp
+++ b/src/storm/builder/ExplicitModelBuilder.cpp
@@ -310,7 +310,7 @@ namespace storm {
// Initialize the model components with the obtained information.
storm::storage::sparse::ModelComponents<ValueType, RewardModelType> modelComponents(transitionMatrixBuilder.build(0, transitionMatrixBuilder.getCurrentRowGroupCount()), buildStateLabeling(), std::unordered_map<std::string, RewardModelType>(), !generator->isDiscreteTimeModel(), std::move(markovianStates));
-
+
// Now finalize all reward models.
for (auto& rewardModelBuilder : rewardModelBuilders) {
modelComponents.rewardModels.emplace(rewardModelBuilder.getName(), rewardModelBuilder.build(modelComponents.transitionMatrix.getRowCount(), modelComponents.transitionMatrix.getColumnCount(), modelComponents.transitionMatrix.getRowGroupCount()));
diff --git a/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h b/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h
index 854d92500..7210d6e1b 100644
--- a/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h
+++ b/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h
@@ -44,6 +44,9 @@ namespace storm {
// The set of relevant labels.
boost::container::flat_set<uint_fast64_t> relevantLabels;
+ // The set of relevant label sets.
+ boost::container::flat_set<boost::container::flat_set<uint_fast64_t>> relevantLabelSets;
+
// The set of labels that matter in terms of minimality.
boost::container::flat_set<uint_fast64_t> minimalityLabels;
@@ -128,19 +131,17 @@ namespace storm {
relevancyInformation.relevantChoicesForRelevantStates.emplace(state, std::list<uint_fast64_t>());
for (uint_fast64_t row = nondeterministicChoiceIndices[state]; row < nondeterministicChoiceIndices[state + 1]; ++row) {
- bool currentChoiceRelevant = false;
-
for (auto const& entry : transitionMatrix.getRow(row)) {
// If there is a relevant successor, we need to add the labels of the current choice.
if (relevancyInformation.relevantStates.get(entry.getColumn()) || psiStates.get(entry.getColumn())) {
+ relevancyInformation.relevantChoicesForRelevantStates[state].push_back(row);
+
for (auto const& label : labelSets[row]) {
relevancyInformation.relevantLabels.insert(label);
}
-
- if (!currentChoiceRelevant) {
- currentChoiceRelevant = true;
- relevancyInformation.relevantChoicesForRelevantStates[state].push_back(row);
- }
+
+ relevancyInformation.relevantLabelSets.insert(labelSets[row]);
+ break;
}
}
}
@@ -277,6 +278,43 @@ namespace storm {
solver.add(formula);
}
+ static storm::expressions::Expression getOtherSynchronizationEnabledFormula(boost::container::flat_set<uint_fast64_t> const& labelSet, std::map<uint_fast64_t, std::set<boost::container::flat_set<uint_fast64_t>>> const& synchronizingLabels, boost::container::flat_map<boost::container::flat_set<uint_fast64_t>, storm::expressions::Expression> const& labelSetToFormula, VariableInformation const& variableInformation, RelevancyInformation const& relevancyInformation) {
+ // Taking all commands of a combination does not necessarily mean that a following label set needs to be taken.
+ // This is because it could be that the commands are taken to enable other synchronizations. Therefore, we need
+ // to add an additional clause that says that the right-hand side of the implication is also true if all commands
+ // of the current choice have enabled synchronization options.
+ if (labelSet.size() > 1) {
+ storm::expressions::Expression result = variableInformation.manager->boolean(true);
+ for (auto label : labelSet) {
+ storm::expressions::Expression alternativeExpressionForLabel = variableInformation.manager->boolean(false);
+ std::set<boost::container::flat_set<uint_fast64_t>> const& synchsForCommand = synchronizingLabels.at(label);
+
+ for (auto const& synchSet : synchsForCommand) {
+ storm::expressions::Expression alternativeExpression = variableInformation.manager->boolean(true);
+
+ // If the current synchSet is the same as left-hand side of the implication, we can to skip it.
+ if (synchSet == labelSet) continue;
+
+ // Build labels that are missing for this synchronization option.
+ std::set<uint_fast64_t> unknownSynchSetLabels;
+ std::set_difference(synchSet.begin(), synchSet.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(unknownSynchSetLabels, unknownSynchSetLabels.end()));
+
+ for (auto label : unknownSynchSetLabels) {
+ alternativeExpression = alternativeExpression && variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label));
+ }
+
+ alternativeExpressionForLabel = alternativeExpressionForLabel || (alternativeExpression && labelSetToFormula.at(synchSet));
+ }
+
+ result = result && alternativeExpressionForLabel;
+ }
+
+ return result;
+ } else {
+ return variableInformation.manager->boolean(false);
+ }
+ }
+
/*!
* Asserts cuts that are derived from the explicit representation of the model and rule out a lot of
* suboptimal solutions.
@@ -285,7 +323,7 @@ namespace storm {
* @param context The Z3 context in which to build the expressions.
* @param solver The solver to use for the satisfiability evaluation.
*/
- static void assertExplicitCuts(storm::models::sparse::Model<T> const& model, std::vector<boost::container::flat_set<uint_fast64_t>> const& labelSets, storm::storage::BitVector const& psiStates, VariableInformation const& variableInformation, RelevancyInformation const& relevancyInformation, storm::solver::SmtSolver& solver) {
+ static void assertCuts(storm::prism::Program& program, storm::models::sparse::Model<T> const& model, std::vector<boost::container::flat_set<uint_fast64_t>> const& labelSets, storm::storage::BitVector const& psiStates, VariableInformation const& variableInformation, RelevancyInformation const& relevancyInformation, storm::solver::SmtSolver& solver) {
// Walk through the model and
// * identify labels enabled in initial states
// * identify labels that can directly precede a given action
@@ -294,16 +332,16 @@ namespace storm {
boost::container::flat_set<uint_fast64_t> initialLabels;
std::set<boost::container::flat_set<uint_fast64_t>> initialCombinations;
- std::map<uint_fast64_t, boost::container::flat_set<uint_fast64_t>> precedingLabels;
boost::container::flat_set<uint_fast64_t> targetLabels;
boost::container::flat_set<boost::container::flat_set<uint_fast64_t>> targetCombinations;
+ std::map<boost::container::flat_set<uint_fast64_t>, std::set<boost::container::flat_set<uint_fast64_t>>> precedingLabels;
std::map<boost::container::flat_set<uint_fast64_t>, std::set<boost::container::flat_set<uint_fast64_t>>> followingLabels;
std::map<uint_fast64_t, std::set<boost::container::flat_set<uint_fast64_t>>> synchronizingLabels;
// Get some data from the model for convenient access.
storm::storage::SparseMatrix<T> const& transitionMatrix = model.getTransitionMatrix();
- storm::storage::BitVector const& initialStates = model.getInitialStates();
storm::storage::SparseMatrix<T> backwardTransitions = model.getBackwardTransitions();
+ storm::storage::BitVector const& initialStates = model.getInitialStates();
for (auto currentState : relevancyInformation.relevantStates) {
for (auto currentChoice : relevancyInformation.relevantChoicesForRelevantStates.at(currentState)) {
@@ -326,6 +364,8 @@ namespace storm {
for (auto const& entry : transitionMatrix.getRow(currentChoice)) {
if (relevancyInformation.relevantStates.get(entry.getColumn())) {
for (auto relevantChoice : relevancyInformation.relevantChoicesForRelevantStates.at(entry.getColumn())) {
+ if (labelSets[currentChoice] == labelSets[relevantChoice]) continue;
+
followingLabels[labelSets[currentChoice]].insert(labelSets[relevantChoice]);
}
} else if (psiStates.get(entry.getColumn())) {
@@ -338,250 +378,6 @@ namespace storm {
targetLabels.insert(labelSets[currentChoice].begin(), labelSets[currentChoice].end());
targetCombinations.insert(labelSets[currentChoice]);
}
- }
-
- // Iterate over predecessors and add all choices that target the current state to the preceding
- // label set of all labels of all relevant choices of the current state.
- for (auto const& predecessorEntry : backwardTransitions.getRow(currentState)) {
- if (relevancyInformation.relevantStates.get(predecessorEntry.getColumn())) {
- for (auto predecessorChoice : relevancyInformation.relevantChoicesForRelevantStates.at(predecessorEntry.getColumn())) {
- bool choiceTargetsCurrentState = false;
- for (auto const& successorEntry : transitionMatrix.getRow(predecessorChoice)) {
- if (successorEntry.getColumn() == currentState) {
- choiceTargetsCurrentState = true;
- }
- }
-
- if (choiceTargetsCurrentState) {
- for (auto currentChoice : relevancyInformation.relevantChoicesForRelevantStates.at(currentState)) {
- for (auto labelToAdd : labelSets[predecessorChoice]) {
- for (auto labelForWhichToAdd : labelSets[currentChoice]) {
- precedingLabels[labelForWhichToAdd].insert(labelToAdd);
- }
- }
- }
- }
- }
- }
- }
- }
-
- STORM_LOG_DEBUG("Successfully gathered data for explicit cuts.");
-
- STORM_LOG_DEBUG("Asserting initial combination is taken.");
- {
- std::vector<storm::expressions::Expression> formulae;
-
- // Start by asserting that we take at least one initial label. We may do so only if there is no initial
- // combination that is already known. Otherwise this condition would be too strong.
- bool initialCombinationKnown = false;
- for (auto const& combination : initialCombinations) {
- boost::container::flat_set<uint_fast64_t> tmpSet;
- std::set_difference(combination.begin(), combination.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(tmpSet, tmpSet.end()));
- if (tmpSet.size() == 0) {
- initialCombinationKnown = true;
- break;
- } else {
- storm::expressions::Expression conj = variableInformation.manager->boolean(true);
- for (auto label : tmpSet) {
- conj = conj && variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label));
- }
- formulae.push_back(conj);
- }
- }
- if (!initialCombinationKnown) {
- assertDisjunction(solver, formulae, *variableInformation.manager);
- }
- }
-
- STORM_LOG_DEBUG("Asserting target combination is taken.");
- {
- std::vector<storm::expressions::Expression> formulae;
-
- // Likewise, if no target combination is known, we may assert that there is at least one.
- bool targetCombinationKnown = false;
- for (auto const& combination : targetCombinations) {
- boost::container::flat_set<uint_fast64_t> tmpSet;
- std::set_difference(combination.begin(), combination.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(tmpSet, tmpSet.end()));
- if (tmpSet.size() == 0) {
- targetCombinationKnown = true;
- break;
- } else {
- storm::expressions::Expression conj = variableInformation.manager->boolean(true);
- for (auto label : tmpSet) {
- conj = conj && variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label));
- }
- formulae.push_back(conj);
- }
- }
- if (!targetCombinationKnown) {
- assertDisjunction(solver, formulae, *variableInformation.manager);
- }
- }
-
- // Compute the sets of labels such that the transitions labeled with this set possess at least one known successor.
- boost::container::flat_set<boost::container::flat_set<uint_fast64_t>> hasKnownSuccessor;
- for (auto const& labelSetFollowingSetsPair : followingLabels) {
- for (auto const& set : labelSetFollowingSetsPair.second) {
- if (std::includes(relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), set.begin(), set.end())) {
- hasKnownSuccessor.insert(set);
- break;
- }
- }
- }
-
- STORM_LOG_DEBUG("Asserting taken labels are followed by another label if they are not a target label.");
- // Now assert that for each non-target label, we take a following label.
- for (auto const& labelSetFollowingSetsPair : followingLabels) {
- std::vector<storm::expressions::Expression> formulae;
-
- // Only build a constraint if the combination does not lead to a target state and
- // no successor set is already known.
- if (targetCombinations.find(labelSetFollowingSetsPair.first) == targetCombinations.end() && hasKnownSuccessor.find(labelSetFollowingSetsPair.first) == hasKnownSuccessor.end()) {
-
- // Compute the set of unknown labels on the left-hand side of the implication.
- boost::container::flat_set<uint_fast64_t> unknownLhsLabels;
- std::set_difference(labelSetFollowingSetsPair.first.begin(), labelSetFollowingSetsPair.first.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(unknownLhsLabels, unknownLhsLabels.end()));
- for (auto label : unknownLhsLabels) {
- formulae.push_back(!variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label)));
- }
-
- for (auto const& followingSet : labelSetFollowingSetsPair.second) {
- boost::container::flat_set<uint_fast64_t> tmpSet;
-
- // Check which labels of the current following set are not known. This set must be non-empty, because
- // otherwise a successor combination would already be known and control cannot reach this point.
- std::set_difference(followingSet.begin(), followingSet.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(tmpSet, tmpSet.end()));
-
- // Construct an expression that enables all unknown labels of the current following set.
- storm::expressions::Expression conj = variableInformation.manager->boolean(true);
- for (auto label : tmpSet) {
- conj = conj && variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label));
- }
- formulae.push_back(conj);
- }
-
- if (labelSetFollowingSetsPair.first.size() > 1) {
- // Taking all commands of a combination does not necessarily mean that a following label set needs to be taken.
- // This is because it could be that the commands are taken to enable other synchronizations. Therefore, we need
- // to add an additional clause that says that the right-hand side of the implication is also true if all commands
- // of the current choice have enabled synchronization options.
- storm::expressions::Expression finalDisjunct = variableInformation.manager->boolean(true);
- for (auto label : labelSetFollowingSetsPair.first) {
- storm::expressions::Expression alternativeExpressionForLabel = variableInformation.manager->boolean(false);
- std::set<boost::container::flat_set<uint_fast64_t>> const& synchsForCommand = synchronizingLabels.at(label);
-
- for (auto const& synchSet : synchsForCommand) {
- storm::expressions::Expression alternativeExpression = variableInformation.manager->boolean(true);
-
- // If the current synchSet is the same as left-hand side of the implication, we need to skip it.
- if (synchSet == labelSetFollowingSetsPair.first) continue;
-
- // Now that we have the labels that are unknown and "missing", we still need to check whether this other
- // synchronizing set already has a known successor or leads directly to a target state.
- if (hasKnownSuccessor.find(synchSet) == hasKnownSuccessor.end() && targetCombinations.find(synchSet) == targetCombinations.end()) {
- // If not, we can assert that we take one of its possible successors.
- boost::container::flat_set<uint_fast64_t> unknownSynchs;
- std::set_difference(synchSet.begin(), synchSet.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(unknownSynchs, unknownSynchs.end()));
- unknownSynchs.erase(label);
-
- for (auto label : unknownSynchs) {
- alternativeExpression = alternativeExpression && variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label));
- }
-
- storm::expressions::Expression disjunctionOverSuccessors = variableInformation.manager->boolean(false);
- for (auto successorSet : followingLabels.at(synchSet)) {
- storm::expressions::Expression conjunctionOverLabels = variableInformation.manager->boolean(true);
- for (auto label : successorSet) {
- if (relevancyInformation.knownLabels.find(label) == relevancyInformation.knownLabels.end()) {
- conjunctionOverLabels = conjunctionOverLabels && variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label));
- }
- }
- disjunctionOverSuccessors = disjunctionOverSuccessors || conjunctionOverLabels;
- }
-
- alternativeExpression = alternativeExpression && disjunctionOverSuccessors;
- }
-
- alternativeExpressionForLabel = alternativeExpressionForLabel || alternativeExpression;
- }
-
- finalDisjunct = finalDisjunct && alternativeExpressionForLabel;
- }
-
- formulae.push_back(finalDisjunct);
- }
-
- if (formulae.size() > 0) {
- assertDisjunction(solver, formulae, *variableInformation.manager);
- }
- }
- }
-
- STORM_LOG_DEBUG("Asserting synchronization cuts.");
- // Finally, assert that if we take one of the synchronizing labels, we also take one of the combinations
- // the label appears in.
- for (auto const& labelSynchronizingSetsPair : synchronizingLabels) {
- std::vector<storm::expressions::Expression> formulae;
-
- if (relevancyInformation.knownLabels.find(labelSynchronizingSetsPair.first) == relevancyInformation.knownLabels.end()) {
- formulae.push_back(!variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(labelSynchronizingSetsPair.first)));
- }
-
- // We need to be careful, because there may be one synchronisation set out of which all labels are
- // known, which means we must not assert anything.
- bool allImplicantsKnownForOneSet = false;
- for (auto const& synchronizingSet : labelSynchronizingSetsPair.second) {
- storm::expressions::Expression currentCombination = variableInformation.manager->boolean(true);
- bool allImplicantsKnownForCurrentSet = true;
- for (auto label : synchronizingSet) {
- if (relevancyInformation.knownLabels.find(label) == relevancyInformation.knownLabels.end() && label != labelSynchronizingSetsPair.first) {
- currentCombination = currentCombination && variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label));
- }
- }
- formulae.push_back(currentCombination);
-
- // If all implicants of the current set are known, we do not need to further build the constraint.
- if (allImplicantsKnownForCurrentSet) {
- allImplicantsKnownForOneSet = true;
- break;
- }
- }
-
- if (!allImplicantsKnownForOneSet) {
- assertDisjunction(solver, formulae, *variableInformation.manager);
- }
- }
- }
-
- /*!
- * Asserts cuts that are derived from the symbolic representation of the model and rule out a lot of
- * suboptimal solutions.
- *
- * @param program The symbolic representation of the model in terms of a program.
- * @param solver The solver to use for the satisfiability evaluation.
- */
- static void assertSymbolicCuts(storm::prism::Program& program, storm::models::sparse::Model<T> const& model, std::vector<boost::container::flat_set<uint_fast64_t>> const& labelSets, VariableInformation const& variableInformation, RelevancyInformation const& relevancyInformation, storm::solver::SmtSolver& solver) {
- // A container storing the label sets that may precede a given label set.
- std::map<boost::container::flat_set<uint_fast64_t>, std::set<boost::container::flat_set<uint_fast64_t>>> precedingLabelSets;
-
- // A container that maps labels to their reachable synchronization sets.
- std::map<uint_fast64_t, std::set<boost::container::flat_set<uint_fast64_t>>> synchronizingLabels;
-
- // Get some data from the model for convenient access.
- storm::storage::SparseMatrix<T> const& transitionMatrix = model.getTransitionMatrix();
- storm::storage::SparseMatrix<T> backwardTransitions = model.getBackwardTransitions();
-
- // Compute the set of labels that may precede a given action.
- for (auto currentState : relevancyInformation.relevantStates) {
- for (auto currentChoice : relevancyInformation.relevantChoicesForRelevantStates.at(currentState)) {
-
- // If the choice is a synchronization choice, we need to record it.
- if (labelSets[currentChoice].size() > 1) {
- for (auto label : labelSets[currentChoice]) {
- synchronizingLabels[label].emplace(labelSets[currentChoice]);
- }
- }
// Iterate over predecessors and add all choices that target the current state to the preceding
// label set of all labels of all relevant choices of the current state.
@@ -596,7 +392,7 @@ namespace storm {
}
if (choiceTargetsCurrentState) {
- precedingLabelSets[labelSets.at(currentChoice)].insert(labelSets.at(predecessorChoice));
+ precedingLabels[labelSets.at(currentChoice)].insert(labelSets.at(predecessorChoice));
}
}
}
@@ -608,7 +404,7 @@ namespace storm {
// cuts.
std::unique_ptr<storm::solver::SmtSolver> localSolver(new storm::solver::Z3SmtSolver(program.getManager()));
storm::expressions::ExpressionManager const& localManager = program.getManager();
-
+
// Then add the constraints for bounds of the integer variables..
for (auto const& integerVariable : program.getGlobalIntegerVariables()) {
localSolver->add(integerVariable.getExpressionVariable() >= integerVariable.getLowerBoundExpression());
@@ -628,8 +424,7 @@ namespace storm {
std::map<boost::container::flat_set<uint_fast64_t>, std::set<boost::container::flat_set<uint_fast64_t>>> backwardImplications;
// Now check for possible backward cuts.
- for (auto const& labelSetAndPrecedingLabelSetsPair : precedingLabelSets) {
-
+ for (auto const& labelSetAndPrecedingLabelSetsPair : precedingLabels) {
// Find out the commands for the currently considered label set.
std::vector<std::reference_wrapper<storm::prism::Command const>> currentCommandVector;
for (uint_fast64_t moduleIndex = 0; moduleIndex < program.getNumberOfModules(); ++moduleIndex) {
@@ -637,7 +432,7 @@ namespace storm {
for (uint_fast64_t commandIndex = 0; commandIndex < module.getNumberOfCommands(); ++commandIndex) {
storm::prism::Command const& command = module.getCommand(commandIndex);
-
+
// If the current command is one of the commands we need to consider, store a reference to it in the container.
if (labelSetAndPrecedingLabelSetsPair.first.find(command.getGlobalIndex()) != labelSetAndPrecedingLabelSetsPair.first.end()) {
currentCommandVector.push_back(command);
@@ -657,7 +452,13 @@ namespace storm {
storm::solver::SmtSolver::CheckResult checkResult = localSolver->check();
localSolver->pop();
localSolver->push();
-
+
+// std::cout << "combi" << std::endl;
+// for (auto const& e : labelSetAndPrecedingLabelSetsPair.first) {
+// std::cout << e << ", ";
+// }
+// std::cout << std::endl;
+
// If the solver reports unsat, then we know that the current selection is not enabled in the initial state.
if (checkResult == storm::solver::SmtSolver::CheckResult::Unsat) {
STORM_LOG_DEBUG("Selection not enabled in initial state.");
@@ -680,21 +481,21 @@ namespace storm {
STORM_LOG_ASSERT(false, "Choice label set is empty.");
}
- STORM_LOG_DEBUG("About to assert disjunction of negated guards.");
- storm::expressions::Expression guardExpression = localManager.boolean(false);
- bool firstAssignment = true;
- for (auto const& command : currentCommandVector) {
- if (firstAssignment) {
- guardExpression = !command.get().getGuardExpression();
- } else {
- guardExpression = guardExpression || !command.get().getGuardExpression();
- }
- }
- localSolver->add(guardExpression);
+ STORM_LOG_DEBUG("About to assert that combination is not enabled in the current state.");
+// std::cout << "negated guard expr " << !guardConjunction << std::endl;
+ localSolver->add(!guardConjunction);
STORM_LOG_DEBUG("Asserted disjunction of negated guards.");
// Now check the possible preceding label sets for the essential ones.
for (auto const& precedingLabelSet : labelSetAndPrecedingLabelSetsPair.second) {
+ if (labelSetAndPrecedingLabelSetsPair.first == precedingLabelSet) continue;
+
+// std::cout << "new preceeding label set" << std::endl;
+// for (auto const& e : precedingLabelSet) {
+// std::cout << e << ", ";
+// }
+// std::cout << std::endl;
+
// Create a restore point so we can easily pop-off all weakest precondition expressions.
localSolver->push();
@@ -715,6 +516,7 @@ namespace storm {
// Assert all the guards of the preceding command set.
for (auto const& command : currentPrecedingCommandVector) {
+// std::cout << "command guard " << command.get().getGuardExpression() << std::endl;
localSolver->add(command.get().getGuardExpression());
}
@@ -736,6 +538,7 @@ namespace storm {
STORM_LOG_DEBUG("About to assert a weakest precondition.");
storm::expressions::Expression wp = guardConjunction.substitute(currentUpdateCombinationMap);
+// std::cout << "wp: " << wp << std::endl;
formulae.push_back(wp);
STORM_LOG_DEBUG("Asserted weakest precondition.");
@@ -756,53 +559,160 @@ namespace storm {
done = true;
}
}
-
+
// Now assert the disjunction of all weakest preconditions of all considered update combinations.
assertDisjunction(*localSolver, formulae, localManager);
STORM_LOG_DEBUG("Asserted disjunction of all weakest preconditions.");
if (localSolver->check() == storm::solver::SmtSolver::CheckResult::Sat) {
+// std::cout << "sat" << std::endl;
backwardImplications[labelSetAndPrecedingLabelSetsPair.first].insert(precedingLabelSet);
}
+// else {
+// std::cout << "unsat" << std::endl;
+// }
localSolver->pop();
}
// Popping the disjunction of negated guards from the solver stack.
localSolver->pop();
+ } else {
+ STORM_LOG_DEBUG("Selection is enabled in initial state.");
}
}
- // Compute the sets of labels such that the transitions labeled with this set possess at least one known successor.
+ // Compute the sets of labels such that the transitions labeled with this set possess at least one known label.
+ boost::container::flat_set<boost::container::flat_set<uint_fast64_t>> hasKnownSuccessor;
+ for (auto const& labelSetFollowingSetsPair : followingLabels) {
+ for (auto const& set : labelSetFollowingSetsPair.second) {
+ if (std::includes(relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), set.begin(), set.end())) {
+ hasKnownSuccessor.insert(set);
+ break;
+ }
+ }
+ }
+
+ // Compute the sets of labels such that the transitions labeled with this set possess at least one known predecessor.
boost::container::flat_set<boost::container::flat_set<uint_fast64_t>> hasKnownPredecessor;
for (auto const& labelSetImplicationsPair : backwardImplications) {
for (auto const& set : labelSetImplicationsPair.second) {
if (std::includes(relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), set.begin(), set.end())) {
- // Should this be labelSetImplicationsPair.first???
- // hasKnownPredecessor.insert(set);
hasKnownPredecessor.insert(labelSetImplicationsPair.first);
break;
}
}
}
+
- STORM_LOG_DEBUG("Asserting taken labels are preceded by another label if they are not an initial label.");
- // Now assert that for each non-target label, we take a following label.
- for (auto const& labelSetImplicationsPair : backwardImplications) {
+ STORM_LOG_DEBUG("Successfully gathered data for cuts.");
+
+ STORM_LOG_DEBUG("Asserting initial combination is taken.");
+ {
std::vector<storm::expressions::Expression> formulae;
- // Only build a constraint if the combination no predecessor set is already known.
- if (hasKnownPredecessor.find(labelSetImplicationsPair.first) == hasKnownPredecessor.end()) {
-
- // Compute the set of unknown labels on the left-hand side of the implication.
- boost::container::flat_set<uint_fast64_t> unknownLhsLabels;
- std::set_difference(labelSetImplicationsPair.first.begin(), labelSetImplicationsPair.first.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(unknownLhsLabels, unknownLhsLabels.end()));
- for (auto label : unknownLhsLabels) {
- formulae.push_back(!variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label)));
+ // Start by asserting that we take at least one initial label. We may do so only if there is no initial
+ // combination that is already known. Otherwise this condition would be too strong.
+ bool initialCombinationKnown = false;
+ for (auto const& combination : initialCombinations) {
+ boost::container::flat_set<uint_fast64_t> tmpSet;
+ std::set_difference(combination.begin(), combination.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(tmpSet, tmpSet.end()));
+ if (tmpSet.size() == 0) {
+ initialCombinationKnown = true;
+ break;
+ } else {
+ storm::expressions::Expression conj = variableInformation.manager->boolean(true);
+ for (auto label : tmpSet) {
+ conj = conj && variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label));
+ }
+ formulae.push_back(conj);
}
+ }
+ if (!initialCombinationKnown) {
+ assertDisjunction(solver, formulae, *variableInformation.manager);
+ }
+ }
+
+ STORM_LOG_DEBUG("Asserting target combination is taken.");
+ {
+ std::vector<storm::expressions::Expression> formulae;
+
+ // Likewise, if no target combination is known, we may assert that there is at least one.
+ bool targetCombinationKnown = false;
+ for (auto const& combination : targetCombinations) {
+ boost::container::flat_set<uint_fast64_t> tmpSet;
+ std::set_difference(combination.begin(), combination.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(tmpSet, tmpSet.end()));
+ if (tmpSet.size() == 0) {
+ targetCombinationKnown = true;
+ break;
+ } else {
+ storm::expressions::Expression conj = variableInformation.manager->boolean(true);
+ for (auto label : tmpSet) {
+ conj = conj && variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label));
+ }
+ formulae.push_back(conj);
+ }
+ }
+ if (!targetCombinationKnown) {
+ assertDisjunction(solver, formulae, *variableInformation.manager);
+ }
+ }
+
+ STORM_LOG_DEBUG("Asserting taken labels are followed and preceeded by another label if they are not a target label or an initial label, respectively.");
+ boost::container::flat_map<boost::container::flat_set<uint_fast64_t>, storm::expressions::Expression> labelSetToFormula;
+ for (auto const& labelSet : relevancyInformation.relevantLabelSets) {
+ storm::expressions::Expression labelSetFormula = variableInformation.manager->boolean(false);
+
+ // Compute the set of unknown labels on the left-hand side of the implication.
+ boost::container::flat_set<uint_fast64_t> unknownLhsLabels;
+ std::set_difference(labelSet.begin(), labelSet.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(unknownLhsLabels, unknownLhsLabels.end()));
+ for (auto label : unknownLhsLabels) {
+ labelSetFormula = labelSetFormula || !variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label));
+ }
+
+ // Only build a constraint if the combination does not lead to a target state and
+ // no successor set is already known.
+ storm::expressions::Expression successorExpression;
+ if (targetCombinations.find(labelSet) == targetCombinations.end() && hasKnownSuccessor.find(labelSet) == hasKnownSuccessor.end()) {
+ successorExpression = variableInformation.manager->boolean(false);
+
+ auto const& followingLabelSets = followingLabels.at(labelSet);
+
+ for (auto const& followingSet : followingLabelSets) {
+ boost::container::flat_set<uint_fast64_t> tmpSet;
+
+ // Check which labels of the current following set are not known. This set must be non-empty, because
+ // otherwise a successor combination would already be known and control cannot reach this point.
+ std::set_difference(followingSet.begin(), followingSet.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(tmpSet, tmpSet.end()));
+
+ // Construct an expression that enables all unknown labels of the current following set.
+ storm::expressions::Expression conj = variableInformation.manager->boolean(true);
+ for (auto label : tmpSet) {
+ conj = conj && variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label));
+ }
+ successorExpression = successorExpression || conj;
+ }
+ } else {
+ successorExpression = variableInformation.manager->boolean(true);
+ }
+ // Constructed following cuts at this point.
+
+ // Only build a constraint if the combination is no initial combination and no
+ // predecessor set is already known.
+ storm::expressions::Expression predecessorExpression;
+ if (initialCombinations.find(labelSet) == initialCombinations.end() && hasKnownPredecessor.find(labelSet) == hasKnownPredecessor.end()) {
+ predecessorExpression = variableInformation.manager->boolean(false);
- for (auto const& preceedingSet : labelSetImplicationsPair.second) {
+// std::cout << "labelSet" << std::endl;
+// for (auto const& e : labelSet) {
+// std::cout << e << ", ";
+// }
+// std::cout << std::endl;
+
+ auto const& preceedingLabelSets = backwardImplications.at(labelSet);
+
+ for (auto const& preceedingSet : preceedingLabelSets) {
boost::container::flat_set<uint_fast64_t> tmpSet;
// Check which labels of the current following set are not known. This set must be non-empty, because
@@ -814,67 +724,54 @@ namespace storm {
for (auto label : tmpSet) {
conj = conj && variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label));
}
- formulae.push_back(conj);
+ predecessorExpression = predecessorExpression || conj;
}
-
- if (labelSetImplicationsPair.first.size() > 1) {
- // Taking all commands of a combination does not necessarily mean that a predecessor label set needs to be taken.
- // This is because it could be that the commands are taken to enable other synchronizations. Therefore, we need
- // to add an additional clause that says that the right-hand side of the implication is also true if all commands
- // of the current choice have enabled synchronization options.
- storm::expressions::Expression finalDisjunct = variableInformation.manager->boolean(false);
- for (auto label : labelSetImplicationsPair.first) {
- storm::expressions::Expression alternativeExpressionForLabel = variableInformation.manager->boolean(false);
- std::set<boost::container::flat_set<uint_fast64_t>> const& synchsForCommand = synchronizingLabels.at(label);
-
- for (auto const& synchSet : synchsForCommand) {
- storm::expressions::Expression alternativeExpression = variableInformation.manager->boolean(true);
-
- // If the current synchSet is the same as left-hand side of the implication, we need to skip it.
- if (synchSet == labelSetImplicationsPair.first) continue;
-
- // Now that we have the labels that are unknown and "missing", we still need to check whether this other
- // synchronizing set already has a known predecessor.
- if (hasKnownPredecessor.find(synchSet) == hasKnownPredecessor.end()) {
- // If not, we can assert that we take one of its possible predecessors.
- boost::container::flat_set<uint_fast64_t> unknownSynchs;
- std::set_difference(synchSet.begin(), synchSet.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(unknownSynchs, unknownSynchs.end()));
- unknownSynchs.erase(label);
-
- for (auto label : unknownSynchs) {
- alternativeExpression = alternativeExpression && variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label));
- }
-
- storm::expressions::Expression disjunctionOverPredecessors = variableInformation.manager->boolean(false);
- auto precedingLabelSetsIterator = precedingLabelSets.find(synchSet);
- if (precedingLabelSetsIterator != precedingLabelSets.end()) {
- for (auto preceedingSet : precedingLabelSetsIterator->second) {
- storm::expressions::Expression conjunctionOverLabels = variableInformation.manager->boolean(true);
- for (auto label : preceedingSet) {
- if (relevancyInformation.knownLabels.find(label) == relevancyInformation.knownLabels.end()) {
- conjunctionOverLabels = conjunctionOverLabels && variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label));
- }
- }
- disjunctionOverPredecessors = disjunctionOverPredecessors || conjunctionOverLabels;
- }
- }
-
- alternativeExpression = alternativeExpression && disjunctionOverPredecessors;
- }
-
- alternativeExpressionForLabel = alternativeExpressionForLabel || alternativeExpression;
- }
-
- finalDisjunct = finalDisjunct && alternativeExpressionForLabel;
- }
+ } else {
+ predecessorExpression = variableInformation.manager->boolean(true);
+ }
+
+ labelSetFormula = labelSetFormula || (successorExpression && predecessorExpression);
+
+ labelSetToFormula[labelSet] = labelSetFormula;
+ }
+
+ for (auto const& labelSetFormula : labelSetToFormula) {
+ solver.add(labelSetFormula.second || getOtherSynchronizationEnabledFormula(labelSetFormula.first, synchronizingLabels, labelSetToFormula, variableInformation, relevancyInformation));
+ }
- formulae.push_back(finalDisjunct);
+ STORM_LOG_DEBUG("Asserting synchronization cuts.");
+ // Finally, assert that if we take one of the synchronizing labels, we also take one of the combinations
+ // the label appears in.
+ for (auto const& labelSynchronizingSetsPair : synchronizingLabels) {
+ std::vector<storm::expressions::Expression> formulae;
+
+ if (relevancyInformation.knownLabels.find(labelSynchronizingSetsPair.first) == relevancyInformation.knownLabels.end()) {
+ formulae.push_back(!variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(labelSynchronizingSetsPair.first)));
+ }
+
+ // We need to be careful, because there may be one synchronisation set out of which all labels are
+ // known, which means we must not assert anything.
+ bool allImplicantsKnownForOneSet = false;
+ for (auto const& synchronizingSet : labelSynchronizingSetsPair.second) {
+ storm::expressions::Expression currentCombination = variableInformation.manager->boolean(true);
+ bool allImplicantsKnownForCurrentSet = true;
+ for (auto label : synchronizingSet) {
+ if (relevancyInformation.knownLabels.find(label) == relevancyInformation.knownLabels.end() && label != labelSynchronizingSetsPair.first) {
+ currentCombination = currentCombination && variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label));
+ }
}
-
- if (formulae.size() > 0) {
- assertDisjunction(solver, formulae, *variableInformation.manager);
+ formulae.push_back(currentCombination);
+
+ // If all implicants of the current set are known, we do not need to further build the constraint.
+ if (allImplicantsKnownForCurrentSet) {
+ allImplicantsKnownForOneSet = true;
+ break;
}
}
+
+ if (!allImplicantsKnownForOneSet) {
+ assertDisjunction(solver, formulae, *variableInformation.manager);
+ }
}
}
@@ -1353,6 +1250,10 @@ namespace storm {
// try with an increased bound.
while (solver.checkWithAssumptions({assumption}) == storm::solver::SmtSolver::CheckResult::Unsat) {
STORM_LOG_DEBUG("Constraint system is unsatisfiable with at most " << currentBound << " taken commands; increasing bound.");
+#ifndef NDEBUG
+ STORM_LOG_DEBUG("Sanity check to see whether constraint system is still satisfiable.");
+ STORM_LOG_ASSERT(solver.check() == storm::solver::SmtSolver::CheckResult::Sat, "Constraint system is not satisfiable anymore.");
+#endif
solver.add(variableInformation.auxiliaryVariables.back());
variableInformation.auxiliaryVariables.push_back(assertLessOrEqualKRelaxed(solver, variableInformation, ++currentBound));
assumption = !variableInformation.auxiliaryVariables.back();
@@ -1729,10 +1630,8 @@ namespace storm {
// (6) Add constraints that cut off a lot of suboptimal solutions.
STORM_LOG_DEBUG("Asserting cuts.");
- assertExplicitCuts(model, labelSets, psiStates, variableInformation, relevancyInformation, *solver);
- STORM_LOG_DEBUG("Asserted explicit cuts.");
- assertSymbolicCuts(program, model, labelSets, variableInformation, relevancyInformation, *solver);
- STORM_LOG_DEBUG("Asserted symbolic cuts.");
+ assertCuts(program, model, labelSets, psiStates, variableInformation, relevancyInformation, *solver);
+ STORM_LOG_DEBUG("Asserted cuts.");
if (includeReachabilityEncoding) {
assertReachabilityCuts(model, labelSets, psiStates, variableInformation, relevancyInformation, *solver);
STORM_LOG_DEBUG("Asserted reachability cuts.");