sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

improved asserted constraints for high-level cex

tempestpy_adaptions
dehnert 7 years ago
parent
24d9b8dfc6
commit
d45eead440
3 changed files with 248 additions and 349 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 2
      src/storm/builder/DdJaniModelBuilder.cpp
  2. 2
      src/storm/builder/ExplicitModelBuilder.cpp
  3. 593
      src/storm/counterexamples/SMTMinimalLabelSetGenerator.h

2
src/storm/builder/DdJaniModelBuilder.cpp
View File

@ -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.

2
src/storm/builder/ExplicitModelBuilder.cpp
View File

@ -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()));

593
src/storm/counterexamples/SMTMinimalLabelSetGenerator.h
View File

@ -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.");

Write Preview
Loading…
Cancel
Save