From 459763c019b8eafb04c1576e56d63729d6b1840d Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 10 Jan 2018 16:42:06 +0100 Subject: [PATCH 01/10] investigating a cut-related issue in high-level cex --- .../counterexamples/SMTMinimalLabelSetGenerator.h | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h b/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h index 74203f65d..ddfcdaf6b 100644 --- a/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h +++ b/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h @@ -677,8 +677,7 @@ namespace storm { ++setIterator; } } else { - throw storm::exceptions::InvalidStateException() << "Choice label set is empty."; - STORM_LOG_DEBUG("Choice label set is empty."); + STORM_LOG_ASSERT(false, "Choice label set is empty."); } STORM_LOG_DEBUG("About to assert disjunction of negated guards."); @@ -780,7 +779,9 @@ namespace storm { for (auto const& labelSetImplicationsPair : backwardImplications) { for (auto const& set : labelSetImplicationsPair.second) { if (std::includes(relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), set.begin(), set.end())) { - hasKnownPredecessor.insert(set); + // Should this be labelSetImplicationsPair.first??? + // hasKnownPredecessor.insert(set); + hasKnownPredecessor.insert(labelSetImplicationsPair.first); break; } } @@ -801,12 +802,12 @@ namespace storm { formulae.push_back(!variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label))); } - for (auto const& precedingSet : labelSetImplicationsPair.second) { + for (auto const& preceedingSet : labelSetImplicationsPair.second) { boost::container::flat_set tmpSet; // Check which labels of the current following set are not known. This set must be non-empty, because // otherwise a predecessor combination would already be known and control cannot reach this point. - std::set_difference(precedingSet.begin(), precedingSet.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(tmpSet, tmpSet.end())); + std::set_difference(preceedingSet.begin(), preceedingSet.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); @@ -847,9 +848,9 @@ namespace storm { storm::expressions::Expression disjunctionOverPredecessors = variableInformation.manager->boolean(false); auto precedingLabelSetsIterator = precedingLabelSets.find(synchSet); if (precedingLabelSetsIterator != precedingLabelSets.end()) { - for (auto precedingSet : precedingLabelSetsIterator->second) { + for (auto preceedingSet : precedingLabelSetsIterator->second) { storm::expressions::Expression conjunctionOverLabels = variableInformation.manager->boolean(true); - for (auto label : precedingSet) { + for (auto label : preceedingSet) { if (relevancyInformation.knownLabels.find(label) == relevancyInformation.knownLabels.end()) { conjunctionOverLabels = conjunctionOverLabels && variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label)); } From 9dea83055b0906bd335bc08e1289ff16ec586ff8 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 11 Jan 2018 14:42:59 +0100 Subject: [PATCH 02/10] added cache to Z3 expression translator to speed up the translation of large constraints --- src/storm/adapters/Z3ExpressionAdapter.cpp | 162 ++++++++++++++---- src/storm/adapters/Z3ExpressionAdapter.h | 7 + .../SMTMinimalLabelSetGenerator.h | 26 ++- 3 files changed, 157 insertions(+), 38 deletions(-) diff --git a/src/storm/adapters/Z3ExpressionAdapter.cpp b/src/storm/adapters/Z3ExpressionAdapter.cpp index e55f5fe3c..c7e27756d 100644 --- a/src/storm/adapters/Z3ExpressionAdapter.cpp +++ b/src/storm/adapters/Z3ExpressionAdapter.cpp @@ -18,8 +18,10 @@ namespace storm { z3::expr Z3ExpressionAdapter::translateExpression(storm::expressions::Expression const& expression) { STORM_LOG_ASSERT(expression.getManager() == this->manager, "Invalid expression for solver."); + z3::expr result = boost::any_cast(expression.getBaseExpression().accept(*this, boost::none)); - + expressionCache.clear(); + for (z3::expr const& assertion : additionalAssertions) { result = result && assertion; } @@ -160,124 +162,220 @@ namespace storm { } boost::any Z3ExpressionAdapter::visit(storm::expressions::BinaryBooleanFunctionExpression const& expression, boost::any const& data) { + auto cacheIt = expressionCache.find(&expression); + if (cacheIt != expressionCache.end()) { + return cacheIt->second; + } + z3::expr leftResult = boost::any_cast(expression.getFirstOperand()->accept(*this, data)); z3::expr rightResult = boost::any_cast(expression.getSecondOperand()->accept(*this, data)); + z3::expr result(context); switch(expression.getOperatorType()) { case storm::expressions::BinaryBooleanFunctionExpression::OperatorType::And: - return leftResult && rightResult; + result = leftResult && rightResult; + break; case storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Or: - return leftResult || rightResult; + result = leftResult || rightResult; + break; case storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Xor: - return z3::expr(context, Z3_mk_xor(context, leftResult, rightResult)); + result = z3::expr(context, Z3_mk_xor(context, leftResult, rightResult)); + break; case storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Implies: - return z3::expr(context, Z3_mk_implies(context, leftResult, rightResult)); + result = z3::expr(context, Z3_mk_implies(context, leftResult, rightResult)); + break; case storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Iff: - return z3::expr(context, Z3_mk_iff(context, leftResult, rightResult)); + result = z3::expr(context, Z3_mk_iff(context, leftResult, rightResult)); + break; default: STORM_LOG_THROW(false, storm::exceptions::ExpressionEvaluationException, "Cannot evaluate expression: unknown boolean binary operator '" << static_cast(expression.getOperatorType()) << "' in expression " << expression << "."); } + expressionCache.emplace(&expression, result); + return result; } boost::any Z3ExpressionAdapter::visit(storm::expressions::BinaryNumericalFunctionExpression const& expression, boost::any const& data) { + auto cacheIt = expressionCache.find(&expression); + if (cacheIt != expressionCache.end()) { + return cacheIt->second; + } + z3::expr leftResult = boost::any_cast(expression.getFirstOperand()->accept(*this, data)); z3::expr rightResult = boost::any_cast(expression.getSecondOperand()->accept(*this, data)); + z3::expr result(context); switch(expression.getOperatorType()) { case storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Plus: - return leftResult + rightResult; + result = leftResult + rightResult; + break; case storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Minus: - return leftResult - rightResult; + result = leftResult - rightResult; + break; case storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Times: - return leftResult * rightResult; + result = leftResult * rightResult; + break; case storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Divide: - return leftResult / rightResult; + result = leftResult / rightResult; + break; case storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Min: - return ite(leftResult <= rightResult, leftResult, rightResult); + result = ite(leftResult <= rightResult, leftResult, rightResult); + break; case storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Max: - return ite(leftResult >= rightResult, leftResult, rightResult); + result = ite(leftResult >= rightResult, leftResult, rightResult); + break; case storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Power: - return pw(leftResult,rightResult); + result = pw(leftResult,rightResult); + break; default: STORM_LOG_THROW(false, storm::exceptions::ExpressionEvaluationException, "Cannot evaluate expression: unknown numerical binary operator '" << static_cast(expression.getOperatorType()) << "' in expression " << expression << "."); } + + expressionCache.emplace(&expression, result); + return result; } boost::any Z3ExpressionAdapter::visit(storm::expressions::BinaryRelationExpression const& expression, boost::any const& data) { + auto cacheIt = expressionCache.find(&expression); + if (cacheIt != expressionCache.end()) { + return cacheIt->second; + } + z3::expr leftResult = boost::any_cast(expression.getFirstOperand()->accept(*this, data)); z3::expr rightResult = boost::any_cast(expression.getSecondOperand()->accept(*this, data)); + z3::expr result(context); switch(expression.getRelationType()) { case storm::expressions::BinaryRelationExpression::RelationType::Equal: - return leftResult == rightResult; + result = leftResult == rightResult; + break; case storm::expressions::BinaryRelationExpression::RelationType::NotEqual: - return leftResult != rightResult; + result = leftResult != rightResult; + break; case storm::expressions::BinaryRelationExpression::RelationType::Less: - return leftResult < rightResult; + result = leftResult < rightResult; + break; case storm::expressions::BinaryRelationExpression::RelationType::LessOrEqual: - return leftResult <= rightResult; + result = leftResult <= rightResult; + break; case storm::expressions::BinaryRelationExpression::RelationType::Greater: - return leftResult > rightResult; + result = leftResult > rightResult; + break; case storm::expressions::BinaryRelationExpression::RelationType::GreaterOrEqual: - return leftResult >= rightResult; + result = leftResult >= rightResult; + break; default: STORM_LOG_THROW(false, storm::exceptions::ExpressionEvaluationException, "Cannot evaluate expression: unknown boolean binary operator '" << static_cast(expression.getRelationType()) << "' in expression " << expression << "."); } + + expressionCache.emplace(&expression, result); + return result; } boost::any Z3ExpressionAdapter::visit(storm::expressions::BooleanLiteralExpression const& expression, boost::any const&) { - return context.bool_val(expression.getValue()); + auto cacheIt = expressionCache.find(&expression); + if (cacheIt != expressionCache.end()) { + return cacheIt->second; + } + + z3::expr result = context.bool_val(expression.getValue()); + + expressionCache.emplace(&expression, result); + return result; } boost::any Z3ExpressionAdapter::visit(storm::expressions::RationalLiteralExpression const& expression, boost::any const&) { + auto cacheIt = expressionCache.find(&expression); + if (cacheIt != expressionCache.end()) { + return cacheIt->second; + } + std::stringstream fractionStream; fractionStream << expression.getValue(); - return context.real_val(fractionStream.str().c_str()); + z3::expr result = context.real_val(fractionStream.str().c_str()); + + expressionCache.emplace(&expression, result); + return result; } boost::any Z3ExpressionAdapter::visit(storm::expressions::IntegerLiteralExpression const& expression, boost::any const&) { - return context.int_val(static_cast(expression.getValue())); + auto cacheIt = expressionCache.find(&expression); + if (cacheIt != expressionCache.end()) { + return cacheIt->second; + } + + z3::expr result = context.int_val(static_cast(expression.getValue())); + + expressionCache.emplace(&expression, result); + return result; } boost::any Z3ExpressionAdapter::visit(storm::expressions::UnaryBooleanFunctionExpression const& expression, boost::any const& data) { - z3::expr childResult = boost::any_cast(expression.getOperand()->accept(*this, data)); + auto cacheIt = expressionCache.find(&expression); + if (cacheIt != expressionCache.end()) { + return cacheIt->second; + } + + z3::expr result = boost::any_cast(expression.getOperand()->accept(*this, data)); switch (expression.getOperatorType()) { case storm::expressions::UnaryBooleanFunctionExpression::OperatorType::Not: - return !childResult; + result = !result; + break; default: STORM_LOG_THROW(false, storm::exceptions::ExpressionEvaluationException, "Cannot evaluate expression: unknown boolean binary operator '" << static_cast(expression.getOperatorType()) << "' in expression " << expression << "."); - } + } + + expressionCache.emplace(&expression, result); + return result; } boost::any Z3ExpressionAdapter::visit(storm::expressions::UnaryNumericalFunctionExpression const& expression, boost::any const& data) { - z3::expr childResult = boost::any_cast(expression.getOperand()->accept(*this, data)); + auto cacheIt = expressionCache.find(&expression); + if (cacheIt != expressionCache.end()) { + return cacheIt->second; + } + + z3::expr result = boost::any_cast(expression.getOperand()->accept(*this, data)); switch(expression.getOperatorType()) { case storm::expressions::UnaryNumericalFunctionExpression::OperatorType::Minus: - return 0 - childResult; + result = 0 - result; + break; case storm::expressions::UnaryNumericalFunctionExpression::OperatorType::Floor: { storm::expressions::Variable freshAuxiliaryVariable = manager.declareFreshVariable(manager.getIntegerType(), true); z3::expr floorVariable = context.int_const(freshAuxiliaryVariable.getName().c_str()); - additionalAssertions.push_back(z3::expr(context, Z3_mk_int2real(context, floorVariable)) <= childResult && childResult < (z3::expr(context, Z3_mk_int2real(context, floorVariable)) + 1)); - return floorVariable; + additionalAssertions.push_back(z3::expr(context, Z3_mk_int2real(context, floorVariable)) <= result && result < (z3::expr(context, Z3_mk_int2real(context, floorVariable)) + 1)); + result = floorVariable; + break; } case storm::expressions::UnaryNumericalFunctionExpression::OperatorType::Ceil:{ storm::expressions::Variable freshAuxiliaryVariable = manager.declareFreshVariable(manager.getIntegerType(), true); z3::expr ceilVariable = context.int_const(freshAuxiliaryVariable.getName().c_str()); - additionalAssertions.push_back(z3::expr(context, Z3_mk_int2real(context, ceilVariable)) - 1 <= childResult && childResult < z3::expr(context, Z3_mk_int2real(context, ceilVariable))); - return ceilVariable; + additionalAssertions.push_back(z3::expr(context, Z3_mk_int2real(context, ceilVariable)) - 1 <= result && result < z3::expr(context, Z3_mk_int2real(context, ceilVariable))); + result = ceilVariable; + break; } default: STORM_LOG_THROW(false, storm::exceptions::ExpressionEvaluationException, "Cannot evaluate expression: unknown numerical unary operator '" << static_cast(expression.getOperatorType()) << "'."); } + + expressionCache.emplace(&expression, result); + return result; } boost::any Z3ExpressionAdapter::visit(storm::expressions::IfThenElseExpression const& expression, boost::any const& data) { + auto cacheIt = expressionCache.find(&expression); + if (cacheIt != expressionCache.end()) { + return cacheIt->second; + } + z3::expr conditionResult = boost::any_cast(expression.getCondition()->accept(*this, data)); z3::expr thenResult = boost::any_cast(expression.getThenExpression()->accept(*this, data)); z3::expr elseResult = boost::any_cast(expression.getElseExpression()->accept(*this, data)); - return z3::expr(context, Z3_mk_ite(context, conditionResult, thenResult, elseResult)); + z3::expr result = z3::expr(context, Z3_mk_ite(context, conditionResult, thenResult, elseResult)); + + expressionCache.emplace(&expression, result); + return result; } boost::any Z3ExpressionAdapter::visit(storm::expressions::VariableExpression const& expression, boost::any const&) { diff --git a/src/storm/adapters/Z3ExpressionAdapter.h b/src/storm/adapters/Z3ExpressionAdapter.h index ddc6e185c..11ed5fe8a 100644 --- a/src/storm/adapters/Z3ExpressionAdapter.h +++ b/src/storm/adapters/Z3ExpressionAdapter.h @@ -16,6 +16,10 @@ #include "storm/storage/expressions/ExpressionVisitor.h" namespace storm { + namespace expressions { + class BaseExpression; + } + namespace adapters { #ifdef STORM_HAVE_Z3 @@ -99,6 +103,9 @@ namespace storm { // A mapping from z3 declarations to the corresponding variables. std::unordered_map declarationToVariableMapping; + + // A cache of already translated constraints. Only valid during the translation of one expression. + std::unordered_map expressionCache; }; #endif } // namespace adapters diff --git a/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h b/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h index ddfcdaf6b..79bb2591f 100644 --- a/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h +++ b/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h @@ -1017,8 +1017,16 @@ namespace storm { * result bit. */ static std::pair createFullAdder(storm::expressions::Expression in1, storm::expressions::Expression in2, storm::expressions::Expression carryIn) { - storm::expressions::Expression resultBit = (in1 && !in2 && !carryIn) || (!in1 && in2 && !carryIn) || (!in1 && !in2 && carryIn) || (in1 && in2 && carryIn); - storm::expressions::Expression carryBit = in1 && in2 || in1 && carryIn || in2 && carryIn; + storm::expressions::Expression resultBit; + storm::expressions::Expression carryBit; + + if (carryIn.isFalse()) { + resultBit = (in1 && !in2) || (!in1 && in2); + carryBit = in1 && in2; + } else { + resultBit = (in1 && !in2 && !carryIn) || (!in1 && in2 && !carryIn) || (!in1 && !in2 && carryIn) || (in1 && in2 && carryIn); + carryBit = in1 && in2 || in1 && carryIn || in2 && carryIn; + } return std::make_pair(carryBit, resultBit); } @@ -1090,8 +1098,6 @@ namespace storm { * @return A bit vector representing the number of literals that are set to true. */ static std::vector createCounterCircuit(VariableInformation const& variableInformation, std::vector const& literals) { - STORM_LOG_DEBUG("Creating counter circuit for " << literals.size() << " literals."); - if (literals.empty()) { return std::vector(); } @@ -1106,7 +1112,9 @@ namespace storm { while (aux.size() > 1) { aux = createAdderPairs(variableInformation, aux); } - + + STORM_LOG_DEBUG("Created counter circuit for " << literals.size() << " literals."); + return aux.front(); } @@ -1307,6 +1315,7 @@ namespace storm { * @param variableInformation A structure with information about the variables of the solver. */ static std::vector assertAdder(storm::solver::SmtSolver& solver, VariableInformation const& variableInformation) { + auto start = std::chrono::high_resolution_clock::now(); std::stringstream variableName; std::vector result; @@ -1317,8 +1326,13 @@ namespace storm { variableName << "adder" << i; result.push_back(variableInformation.manager->declareBooleanVariable(variableName.str())); solver.add(storm::expressions::implies(adderVariables[i], result.back())); + STORM_LOG_TRACE("Added bit " << i << " of adder."); } - + + auto end = std::chrono::high_resolution_clock::now(); + uint64_t duration = std::chrono::duration_cast(end - start).count(); + STORM_LOG_DEBUG("Asserted adder in " << duration << "ms."); + return result; } From 24d9b8dfc6fbdcdfd806e7229ded1033196fee9f Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 15 Jan 2018 16:33:52 +0100 Subject: [PATCH 03/10] minor reformulation --- .../SMTMinimalLabelSetGenerator.h | 18 +++++------------- 1 file changed, 5 insertions(+), 13 deletions(-) diff --git a/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h b/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h index 79bb2591f..854d92500 100644 --- a/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h +++ b/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h @@ -1450,16 +1450,12 @@ namespace storm { isBorderChoice = true; } } - + if (isBorderChoice) { boost::container::flat_set currentLabelSet; - for (auto label : originalLabelSets.at(currentChoice)) { - if (commandSet.find(label) == commandSet.end()) { - currentLabelSet.insert(label); - } - } + std::set_difference(originalLabelSets[currentChoice].begin(), originalLabelSets[currentChoice].end(), commandSet.begin(), commandSet.end(), std::inserter(currentLabelSet, currentLabelSet.begin())); std::set_difference(guaranteedLabelSets[state].begin(), guaranteedLabelSets[state].end(), commandSet.begin(), commandSet.end(), std::inserter(currentLabelSet, currentLabelSet.end())); - + cutLabels.insert(currentLabelSet); } } @@ -1559,13 +1555,9 @@ namespace storm { for (auto currentChoice : relevancyInformation.relevantChoicesForRelevantStates.at(state)) { if (!std::includes(commandSet.begin(), commandSet.end(), originalLabelSets[currentChoice].begin(), originalLabelSets[currentChoice].end())) { boost::container::flat_set currentLabelSet; - for (auto label : originalLabelSets[currentChoice]) { - if (commandSet.find(label) == commandSet.end()) { - currentLabelSet.insert(label); - } - } + std::set_difference(originalLabelSets[currentChoice].begin(), originalLabelSets[currentChoice].end(), commandSet.begin(), commandSet.end(), std::inserter(currentLabelSet, currentLabelSet.begin())); std::set_difference(guaranteedLabelSets[state].begin(), guaranteedLabelSets[state].end(), commandSet.begin(), commandSet.end(), std::inserter(currentLabelSet, currentLabelSet.end())); - + cutLabels.insert(currentLabelSet); } } From 22d97332b0b2e958bb06b8c942191d6b2ef16e0f Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 19 Jan 2018 23:05:20 +0100 Subject: [PATCH 04/10] Temporarily disabled Mac builds in Travis --- .travis.yml | 117 ---------------------------------------------------- 1 file changed, 117 deletions(-) diff --git a/.travis.yml b/.travis.yml index 4995abe2d..7279e2999 100644 --- a/.travis.yml +++ b/.travis.yml @@ -39,31 +39,6 @@ jobs: # Stage: Build (1st run) ### - # osx - - stage: Build (1st run) - os: osx - osx_image: xcode9.1 - compiler: clang - env: CONFIG=DefaultDebug COMPILER=clang STL=libc++ - install: - - rm -rf build - - travis/install_osx.sh - script: - - travis/build.sh Build1 - after_failure: - - find build -iname '*err*.log' -type f -print -exec cat {} \; - - stage: Build (1st run) - os: osx - osx_image: xcode9.1 - compiler: clang - env: CONFIG=DefaultRelease COMPILER=clang STL=libc++ - install: - - rm -rf build - - travis/install_osx.sh - script: - - travis/build.sh Build1 - after_failure: - - find build -iname '*err*.log' -type f -print -exec cat {} \; # ubuntu-16.10 - stage: Build (1st run) os: linux @@ -96,29 +71,6 @@ jobs: # Stage: Build (2nd run) ### - # osx - - stage: Build (2nd run) - os: osx - osx_image: xcode9.1 - compiler: clang - env: CONFIG=DefaultDebug COMPILER=clang STL=libc++ - install: - - travis/install_osx.sh - script: - - travis/build.sh Build2 - after_failure: - - find build -iname '*err*.log' -type f -print -exec cat {} \; - - stage: Build (2nd run) - os: osx - osx_image: xcode9.1 - compiler: clang - env: CONFIG=DefaultRelease COMPILER=clang STL=libc++ - install: - - travis/install_osx.sh - script: - - travis/build.sh Build2 - after_failure: - - find build -iname '*err*.log' -type f -print -exec cat {} \; # ubuntu-16.10 - stage: Build (2nd run) os: linux @@ -149,29 +101,6 @@ jobs: # Stage: Build (3rd run) ### - # osx - - stage: Build (3rd run) - os: osx - osx_image: xcode9.1 - compiler: clang - env: CONFIG=DefaultDebug COMPILER=clang STL=libc++ - install: - - travis/install_osx.sh - script: - - travis/build.sh Build3 - after_failure: - - find build -iname '*err*.log' -type f -print -exec cat {} \; - - stage: Build (3rd run) - os: osx - osx_image: xcode9.1 - compiler: clang - env: CONFIG=DefaultRelease COMPILER=clang STL=libc++ - install: - - travis/install_osx.sh - script: - - travis/build.sh Build3 - after_failure: - - find build -iname '*err*.log' -type f -print -exec cat {} \; # ubuntu-16.10 - stage: Build (3rd run) os: linux @@ -202,29 +131,6 @@ jobs: # Stage: Build (4th run) ### - # osx - - stage: Build (4th run) - os: osx - osx_image: xcode9.1 - compiler: clang - env: CONFIG=DefaultDebug COMPILER=clang STL=libc++ - install: - - travis/install_osx.sh - script: - - travis/build.sh BuildLast - after_failure: - - find build -iname '*err*.log' -type f -print -exec cat {} \; - - stage: Build (4th run) - os: osx - osx_image: xcode9.1 - compiler: clang - env: CONFIG=DefaultRelease COMPILER=clang STL=libc++ - install: - - travis/install_osx.sh - script: - - travis/build.sh BuildLast - after_failure: - - find build -iname '*err*.log' -type f -print -exec cat {} \; # ubuntu-16.10 - stage: Build (4th run) os: linux @@ -255,29 +161,6 @@ jobs: # Stage: Test all ### - # osx - - stage: Test all - os: osx - osx_image: xcode9.1 - compiler: clang - env: CONFIG=DefaultDebug COMPILER=clang STL=libc++ - install: - - travis/install_osx.sh - script: - - travis/build.sh TestAll - after_failure: - - find build -iname '*err*.log' -type f -print -exec cat {} \; - - stage: Test all - os: osx - osx_image: xcode9.1 - compiler: clang - env: CONFIG=DefaultRelease COMPILER=clang STL=libc++ - install: - - travis/install_osx.sh - script: - - travis/build.sh TestAll - after_failure: - - find build -iname '*err*.log' -type f -print -exec cat {} \; # ubuntu-16.10 - stage: Test all os: linux From d45eead4402f2cdcd7a74bc56135c4cdaea816be Mon Sep 17 00:00:00 2001 From: dehnert Date: Sun, 21 Jan 2018 18:11:39 +0100 Subject: [PATCH 05/10] improved asserted constraints for high-level cex --- src/storm/builder/DdJaniModelBuilder.cpp | 2 +- src/storm/builder/ExplicitModelBuilder.cpp | 2 +- .../SMTMinimalLabelSetGenerator.h | 593 ++++++++---------- 3 files changed, 248 insertions(+), 349 deletions(-) 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() * transientAssignment.second * indicesEncodedWithLocalNondeterminismVariables[k].first.template toAdd()); + addToTransientAssignmentMap(transientAssignments, transientAssignment.first, remainingGuardChoicesIntersection.template toAdd() * 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 modelComponents(transitionMatrixBuilder.build(0, transitionMatrixBuilder.getCurrentRowGroupCount()), buildStateLabeling(), std::unordered_map(), !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 relevantLabels; + // The set of relevant label sets. + boost::container::flat_set> relevantLabelSets; + // The set of labels that matter in terms of minimality. boost::container::flat_set minimalityLabels; @@ -128,19 +131,17 @@ namespace storm { relevancyInformation.relevantChoicesForRelevantStates.emplace(state, std::list()); 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 const& labelSet, std::map>> const& synchronizingLabels, boost::container::flat_map, 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> 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 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 const& model, std::vector> 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 const& model, std::vector> 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 initialLabels; std::set> initialCombinations; - std::map> precedingLabels; boost::container::flat_set targetLabels; boost::container::flat_set> targetCombinations; + std::map, std::set>> precedingLabels; std::map, std::set>> followingLabels; std::map>> synchronizingLabels; // Get some data from the model for convenient access. storm::storage::SparseMatrix const& transitionMatrix = model.getTransitionMatrix(); - storm::storage::BitVector const& initialStates = model.getInitialStates(); storm::storage::SparseMatrix 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 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 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 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 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> 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 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 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 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> 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 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 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 const& model, std::vector> 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, std::set>> precedingLabelSets; - - // A container that maps labels to their reachable synchronization sets. - std::map>> synchronizingLabels; - - // Get some data from the model for convenient access. - storm::storage::SparseMatrix const& transitionMatrix = model.getTransitionMatrix(); - storm::storage::SparseMatrix 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 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, std::set>> 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> 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> 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> 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 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 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 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 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 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, 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 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 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 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> 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 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 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."); From 8a836a2bfdafee684de4378d438d7ba427a36080 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 25 Jan 2018 19:25:08 +0100 Subject: [PATCH 06/10] Try to avoid timeout in travis with travis_wait --- travis/build-helper.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/travis/build-helper.sh b/travis/build-helper.sh index 7d722dc99..4aed04eee 100755 --- a/travis/build-helper.sh +++ b/travis/build-helper.sh @@ -35,7 +35,7 @@ run() { # Make travis_fold start make cd build - make -j$N_JOBS + travis_wait make -j$N_JOBS travis_fold end make # Set skip-file if [[ "$1" != "BuildLast" ]] From 2a8e58284cc1d4a67a264accc882900ac41167cd Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 26 Jan 2018 17:45:43 +0100 Subject: [PATCH 07/10] Next try with travis_wait --- .travis.yml | 20 ++++++++++---------- travis/build-helper.sh | 2 +- travis/generate_travis.py | 6 +++--- 3 files changed, 14 insertions(+), 14 deletions(-) diff --git a/.travis.yml b/.travis.yml index 7279e2999..669f831c5 100644 --- a/.travis.yml +++ b/.travis.yml @@ -48,7 +48,7 @@ jobs: - rm -rf build - travis/install_linux.sh script: - - travis/build.sh Build1 + - travis_wait 40 travis/build.sh Build1 before_cache: - docker cp storm:/storm/. . after_failure: @@ -61,7 +61,7 @@ jobs: - rm -rf build - travis/install_linux.sh script: - - travis/build.sh Build1 + - travis_wait 40 travis/build.sh Build1 before_cache: - docker cp storm:/storm/. . after_failure: @@ -79,7 +79,7 @@ jobs: install: - travis/install_linux.sh script: - - travis/build.sh Build2 + - travis_wait 40 travis/build.sh Build2 before_cache: - docker cp storm:/storm/. . after_failure: @@ -91,7 +91,7 @@ jobs: install: - travis/install_linux.sh script: - - travis/build.sh Build2 + - travis_wait 40 travis/build.sh Build2 before_cache: - docker cp storm:/storm/. . after_failure: @@ -109,7 +109,7 @@ jobs: install: - travis/install_linux.sh script: - - travis/build.sh Build3 + - travis_wait 40 travis/build.sh Build3 before_cache: - docker cp storm:/storm/. . after_failure: @@ -121,7 +121,7 @@ jobs: install: - travis/install_linux.sh script: - - travis/build.sh Build3 + - travis_wait 40 travis/build.sh Build3 before_cache: - docker cp storm:/storm/. . after_failure: @@ -139,7 +139,7 @@ jobs: install: - travis/install_linux.sh script: - - travis/build.sh BuildLast + - travis_wait 40 travis/build.sh BuildLast before_cache: - docker cp storm:/storm/. . after_failure: @@ -151,7 +151,7 @@ jobs: install: - travis/install_linux.sh script: - - travis/build.sh BuildLast + - travis_wait 40 travis/build.sh BuildLast before_cache: - docker cp storm:/storm/. . after_failure: @@ -169,7 +169,7 @@ jobs: install: - travis/install_linux.sh script: - - travis/build.sh TestAll + - travis_wait 40 travis/build.sh TestAll before_cache: - docker cp storm:/storm/. . after_failure: @@ -185,7 +185,7 @@ jobs: install: - travis/install_linux.sh script: - - travis/build.sh TestAll + - travis_wait 40 travis/build.sh TestAll before_cache: - docker cp storm:/storm/. . after_failure: diff --git a/travis/build-helper.sh b/travis/build-helper.sh index 4aed04eee..7d722dc99 100755 --- a/travis/build-helper.sh +++ b/travis/build-helper.sh @@ -35,7 +35,7 @@ run() { # Make travis_fold start make cd build - travis_wait make -j$N_JOBS + make -j$N_JOBS travis_fold end make # Set skip-file if [[ "$1" != "BuildLast" ]] diff --git a/travis/generate_travis.py b/travis/generate_travis.py index b104661f1..71f719696 100644 --- a/travis/generate_travis.py +++ b/travis/generate_travis.py @@ -9,7 +9,7 @@ configs_linux = [ # Configurations for Mac configs_mac = [ # OS, compiler - ("osx", "clang", ""), +# ("osx", "clang", ""), ] # Build types @@ -93,7 +93,7 @@ if __name__ == "__main__": buildConfig += " - rm -rf build\n" buildConfig += " - travis/install_osx.sh\n" buildConfig += " script:\n" - buildConfig += " - travis/build.sh {}\n".format(stage[1]) + buildConfig += " - travis_wait 40 travis/build.sh {}\n".format(stage[1]) buildConfig += " after_failure:\n" buildConfig += " - find build -iname '*err*.log' -type f -print -exec cat {} \;\n" s += buildConfig @@ -114,7 +114,7 @@ if __name__ == "__main__": buildConfig += " - rm -rf build\n" buildConfig += " - travis/install_linux.sh\n" buildConfig += " script:\n" - buildConfig += " - travis/build.sh {}\n".format(stage[1]) + buildConfig += " - travis_wait 40 travis/build.sh {}\n".format(stage[1]) buildConfig += " before_cache:\n" buildConfig += " - docker cp storm:/storm/. .\n" buildConfig += " after_failure:\n" From 58990aea2750d03bf0d3588d1ae50ba90af2778e Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Sat, 27 Jan 2018 14:57:34 +0100 Subject: [PATCH 08/10] Another try with travis_wait --- .travis.yml | 20 ++++++++++---------- travis/generate_travis.py | 4 ++-- 2 files changed, 12 insertions(+), 12 deletions(-) diff --git a/.travis.yml b/.travis.yml index 669f831c5..7b8de9321 100644 --- a/.travis.yml +++ b/.travis.yml @@ -48,7 +48,7 @@ jobs: - rm -rf build - travis/install_linux.sh script: - - travis_wait 40 travis/build.sh Build1 + - travis_wait 60 travis/build.sh Build1 before_cache: - docker cp storm:/storm/. . after_failure: @@ -61,7 +61,7 @@ jobs: - rm -rf build - travis/install_linux.sh script: - - travis_wait 40 travis/build.sh Build1 + - travis_wait 60 travis/build.sh Build1 before_cache: - docker cp storm:/storm/. . after_failure: @@ -79,7 +79,7 @@ jobs: install: - travis/install_linux.sh script: - - travis_wait 40 travis/build.sh Build2 + - travis_wait 60 travis/build.sh Build2 before_cache: - docker cp storm:/storm/. . after_failure: @@ -91,7 +91,7 @@ jobs: install: - travis/install_linux.sh script: - - travis_wait 40 travis/build.sh Build2 + - travis_wait 60 travis/build.sh Build2 before_cache: - docker cp storm:/storm/. . after_failure: @@ -109,7 +109,7 @@ jobs: install: - travis/install_linux.sh script: - - travis_wait 40 travis/build.sh Build3 + - travis_wait 60 travis/build.sh Build3 before_cache: - docker cp storm:/storm/. . after_failure: @@ -121,7 +121,7 @@ jobs: install: - travis/install_linux.sh script: - - travis_wait 40 travis/build.sh Build3 + - travis_wait 60 travis/build.sh Build3 before_cache: - docker cp storm:/storm/. . after_failure: @@ -139,7 +139,7 @@ jobs: install: - travis/install_linux.sh script: - - travis_wait 40 travis/build.sh BuildLast + - travis_wait 60 travis/build.sh BuildLast before_cache: - docker cp storm:/storm/. . after_failure: @@ -151,7 +151,7 @@ jobs: install: - travis/install_linux.sh script: - - travis_wait 40 travis/build.sh BuildLast + - travis_wait 60 travis/build.sh BuildLast before_cache: - docker cp storm:/storm/. . after_failure: @@ -169,7 +169,7 @@ jobs: install: - travis/install_linux.sh script: - - travis_wait 40 travis/build.sh TestAll + - travis_wait 60 travis/build.sh TestAll before_cache: - docker cp storm:/storm/. . after_failure: @@ -185,7 +185,7 @@ jobs: install: - travis/install_linux.sh script: - - travis_wait 40 travis/build.sh TestAll + - travis_wait 60 travis/build.sh TestAll before_cache: - docker cp storm:/storm/. . after_failure: diff --git a/travis/generate_travis.py b/travis/generate_travis.py index 71f719696..87f622c57 100644 --- a/travis/generate_travis.py +++ b/travis/generate_travis.py @@ -93,7 +93,7 @@ if __name__ == "__main__": buildConfig += " - rm -rf build\n" buildConfig += " - travis/install_osx.sh\n" buildConfig += " script:\n" - buildConfig += " - travis_wait 40 travis/build.sh {}\n".format(stage[1]) + buildConfig += " - travis_wait 60 travis/build.sh {}\n".format(stage[1]) buildConfig += " after_failure:\n" buildConfig += " - find build -iname '*err*.log' -type f -print -exec cat {} \;\n" s += buildConfig @@ -114,7 +114,7 @@ if __name__ == "__main__": buildConfig += " - rm -rf build\n" buildConfig += " - travis/install_linux.sh\n" buildConfig += " script:\n" - buildConfig += " - travis_wait 40 travis/build.sh {}\n".format(stage[1]) + buildConfig += " - travis_wait 60 travis/build.sh {}\n".format(stage[1]) buildConfig += " before_cache:\n" buildConfig += " - docker cp storm:/storm/. .\n" buildConfig += " after_failure:\n" From 5a62a60e17bd1d4a1868bccd2bd8b93562c7e2e5 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Sat, 27 Jan 2018 19:13:50 +0100 Subject: [PATCH 09/10] fix in pla without simplifications allowed --- .../region/SparseMdpParameterLiftingModelChecker.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp index de1f47b24..0aa70d974 100644 --- a/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp +++ b/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp @@ -47,7 +47,7 @@ namespace storm { template void SparseMdpParameterLiftingModelChecker::specify(Environment const& env, std::shared_ptr parametricModel, CheckTask const& checkTask, bool generateRegionSplitEstimates, bool allowModelSimplifications) { auto mdp = parametricModel->template as(); - specify_internal(env, mdp, checkTask, generateRegionSplitEstimates, false); + specify_internal(env, mdp, checkTask, generateRegionSplitEstimates, !allowModelSimplifications); } template From b64b65f156f6e6382402d708046a064852e2d268 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Sat, 27 Jan 2018 19:14:21 +0100 Subject: [PATCH 10/10] qualitative model checking for pmdps enabled --- src/storm/api/verification.h | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/src/storm/api/verification.h b/src/storm/api/verification.h index 4f7c59dbc..5d07f9f51 100644 --- a/src/storm/api/verification.h +++ b/src/storm/api/verification.h @@ -152,8 +152,13 @@ namespace storm { } template - typename std::enable_if::value, std::unique_ptr>::type verifyWithSparseEngine(std::shared_ptr> const&, storm::modelchecker::CheckTask const&) { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Sparse engine cannot verify MDPs with this data type."); + typename std::enable_if::value, std::unique_ptr>::type verifyWithSparseEngine(std::shared_ptr> const& mdp, storm::modelchecker::CheckTask const& task) { + std::unique_ptr result; + storm::modelchecker::SparsePropositionalModelChecker> modelchecker(*mdp); + if (modelchecker.canHandle(task)) { + result = modelchecker.check(task); + } + return result; } template