From a44a3554c8053f288350b99eed73959ced3bc856 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 16 Mar 2015 22:47:09 +0100 Subject: [PATCH] Fixed minimal command counterexample generation. Former-commit-id: 6e7e6208daacd31321d29ec3eec25cee56bc62e6 --- .../MILPMinimalLabelSetGenerator.h | 9 +++--- .../SMTMinimalCommandSetGenerator.h | 5 ++- src/modelchecker/AbstractModelChecker.cpp | 32 ++++++++++++++++--- .../prctl/SparseMdpPrctlModelChecker.cpp | 12 +++---- .../prctl/SparseMdpPrctlModelChecker.h | 6 +++- src/utility/cli.h | 5 +++ 6 files changed, 51 insertions(+), 18 deletions(-) diff --git a/src/counterexamples/MILPMinimalLabelSetGenerator.h b/src/counterexamples/MILPMinimalLabelSetGenerator.h index 4e09ae838..4c9b5b566 100644 --- a/src/counterexamples/MILPMinimalLabelSetGenerator.h +++ b/src/counterexamples/MILPMinimalLabelSetGenerator.h @@ -629,7 +629,7 @@ namespace storm { uint_fast64_t numberOfConstraintsCreated = 0; for (auto label : choiceInformation.knownLabels) { - storm::expressions::Expression constraint = variableInformation.labelToVariableMap.at(label) == solver.getConstant(0); + storm::expressions::Expression constraint = variableInformation.labelToVariableMap.at(label) == solver.getConstant(1); solver.addConstraint("KnownLabels" + std::to_string(numberOfConstraintsCreated), constraint); ++numberOfConstraintsCreated; } @@ -929,10 +929,9 @@ namespace storm { double maximalReachabilityProbability = 0; if (checkThresholdFeasible) { storm::modelchecker::SparseMdpPrctlModelChecker modelchecker(labeledMdp); - std::unique_ptr result = modelchecker.check(pathFormula); - storm::modelchecker::ExplicitQuantitativeCheckResult const& quantitativeResult = result->asExplicitQuantitativeCheckResult(); + std::vector result = modelchecker.computeUntilProbabilitiesHelper(false, phiStates, psiStates, false); for (auto state : labeledMdp.getInitialStates()) { - maximalReachabilityProbability = std::max(maximalReachabilityProbability, quantitativeResult[state]); + maximalReachabilityProbability = std::max(maximalReachabilityProbability, result[state]); } STORM_LOG_THROW((strictBound && maximalReachabilityProbability >= probabilityThreshold) || (!strictBound && maximalReachabilityProbability > probabilityThreshold), storm::exceptions::InvalidArgumentException, "Given probability threshold " << probabilityThreshold << " can not be " << (strictBound ? "achieved" : "exceeded") << " in model with maximal reachability probability of " << maximalReachabilityProbability << "."); std::cout << std::endl << "Maximal reachability in model is " << maximalReachabilityProbability << "." << std::endl << std::endl; @@ -953,6 +952,8 @@ namespace storm { // (4.2) Construct constraint system. buildConstraintSystem(*solver, labeledMdp, psiStates, stateInformation, choiceInformation, variableInformation, probabilityThreshold, strictBound, includeSchedulerCuts); + solver->writeModelToFile("model.lp"); + // (4.3) Optimize the model. solver->optimize(); diff --git a/src/counterexamples/SMTMinimalCommandSetGenerator.h b/src/counterexamples/SMTMinimalCommandSetGenerator.h index bde97a841..e79d76dda 100644 --- a/src/counterexamples/SMTMinimalCommandSetGenerator.h +++ b/src/counterexamples/SMTMinimalCommandSetGenerator.h @@ -1627,10 +1627,9 @@ namespace storm { double maximalReachabilityProbability = 0; if (checkThresholdFeasible) { storm::modelchecker::SparseMdpPrctlModelChecker modelchecker(labeledMdp); - std::unique_ptr result = modelchecker.check(pathFormula); - storm::modelchecker::ExplicitQuantitativeCheckResult const& quantitativeResult = result->asExplicitQuantitativeCheckResult(); + std::vector result = modelchecker.computeUntilProbabilitiesHelper(false, phiStates, psiStates, false); for (auto state : labeledMdp.getInitialStates()) { - maximalReachabilityProbability = std::max(maximalReachabilityProbability, quantitativeResult[state]); + maximalReachabilityProbability = std::max(maximalReachabilityProbability, result[state]); } STORM_LOG_THROW((strictBound && maximalReachabilityProbability >= probabilityThreshold) || (!strictBound && maximalReachabilityProbability > probabilityThreshold), storm::exceptions::InvalidArgumentException, "Given probability threshold " << probabilityThreshold << " can not be " << (strictBound ? "achieved" : "exceeded") << " in model with maximal reachability probability of " << maximalReachabilityProbability << "."); std::cout << std::endl << "Maximal reachability in model is " << maximalReachabilityProbability << "." << std::endl << std::endl; diff --git a/src/modelchecker/AbstractModelChecker.cpp b/src/modelchecker/AbstractModelChecker.cpp index eb9d539a9..6b4ab55ab 100644 --- a/src/modelchecker/AbstractModelChecker.cpp +++ b/src/modelchecker/AbstractModelChecker.cpp @@ -85,7 +85,7 @@ namespace storm { std::unique_ptr AbstractModelChecker::computeLongRunAverage(storm::logic::StateFormula const& eventuallyFormula, bool qualitative, boost::optional const& optimalityType) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the computation of long-run averages."); } - + std::unique_ptr AbstractModelChecker::computeExpectedTimes(storm::logic::EventuallyFormula const& eventuallyFormula, bool qualitative, boost::optional const& optimalityType) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the computation of expected times."); } @@ -160,6 +160,12 @@ namespace storm { std::unique_ptr result; if (stateFormula.hasOptimalityType()) { result = this->computeProbabilities(stateFormula.getSubformula().asPathFormula(), qualitative, stateFormula.getOptimalityType()); + } else if (stateFormula.hasBound()) { + if (stateFormula.getComparisonType() == storm::logic::ComparisonType::Less || storm::logic::ComparisonType::LessEqual) { + result = this->computeProbabilities(stateFormula.getSubformula().asPathFormula(), storm::logic::OptimalityType::Maximize); + } else { + result = this->computeProbabilities(stateFormula.getSubformula().asPathFormula(), storm::logic::OptimalityType::Minimize); + } } else { result = this->computeProbabilities(stateFormula.getSubformula().asPathFormula(), qualitative); } @@ -186,6 +192,12 @@ namespace storm { std::unique_ptr result; if (stateFormula.hasOptimalityType()) { result = this->computeRewards(stateFormula.getSubformula().asRewardPathFormula(), qualitative, stateFormula.getOptimalityType()); + } else if (stateFormula.hasBound()) { + if (stateFormula.getComparisonType() == storm::logic::ComparisonType::Less || storm::logic::ComparisonType::LessEqual) { + result = this->computeRewards(stateFormula.getSubformula().asRewardPathFormula(), storm::logic::OptimalityType::Maximize); + } else { + result = this->computeRewards(stateFormula.getSubformula().asRewardPathFormula(), storm::logic::OptimalityType::Minimize); + } } else { result = this->computeRewards(stateFormula.getSubformula().asRewardPathFormula(), qualitative); } @@ -212,6 +224,12 @@ namespace storm { std::unique_ptr result; if (stateFormula.hasOptimalityType()) { result = this->computeExpectedTimes(stateFormula.getSubformula().asEventuallyFormula(), qualitative, stateFormula.getOptimalityType()); + } else if (stateFormula.hasBound()) { + if (stateFormula.getComparisonType() == storm::logic::ComparisonType::Less || storm::logic::ComparisonType::LessEqual) { + result = this->computeExpectedTimes(stateFormula.getSubformula().asEventuallyFormula(), storm::logic::OptimalityType::Maximize); + } else { + result = this->computeExpectedTimes(stateFormula.getSubformula().asEventuallyFormula(), storm::logic::OptimalityType::Minimize); + } } else { result = this->computeExpectedTimes(stateFormula.getSubformula().asEventuallyFormula(), qualitative); } @@ -227,13 +245,19 @@ namespace storm { std::unique_ptr AbstractModelChecker::checkLongRunAverageOperatorFormula(storm::logic::LongRunAverageOperatorFormula const& stateFormula) { STORM_LOG_THROW(stateFormula.getSubformula().isEventuallyFormula(), storm::exceptions::InvalidArgumentException, "The given formula is invalid."); + std::unique_ptr result; if (stateFormula.hasOptimalityType()) { - return this->computeLongRunAverage(stateFormula.getSubformula().asStateFormula(), false, stateFormula.getOptimalityType()); + result = this->computeLongRunAverage(stateFormula.getSubformula().asStateFormula(), false, stateFormula.getOptimalityType()); + } else if (stateFormula.hasBound()) { + if (stateFormula.getComparisonType() == storm::logic::ComparisonType::Less || storm::logic::ComparisonType::LessEqual) { + result = this->computeLongRunAverage(stateFormula.getSubformula().asStateFormula(), storm::logic::OptimalityType::Maximize); + } else { + result = this->computeLongRunAverage(stateFormula.getSubformula().asStateFormula(), storm::logic::OptimalityType::Minimize); + } } else { - return this->computeLongRunAverage(stateFormula.getSubformula().asStateFormula(), false); + result = this->computeLongRunAverage(stateFormula.getSubformula().asStateFormula(), false); } - std::unique_ptr result; if (stateFormula.hasBound()) { return result->compareAgainstBound(stateFormula.getComparisonType(), stateFormula.getBound()); } else { diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index 3aec3ef8d..ced5463a6 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -69,7 +69,7 @@ namespace storm { template std::unique_ptr SparseMdpPrctlModelChecker::computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic this->getModel()."); + STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic."); std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); @@ -92,7 +92,7 @@ namespace storm { template std::unique_ptr SparseMdpPrctlModelChecker::computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic this->getModel()."); + STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic."); std::unique_ptr subResultPointer = this->check(pathFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); return std::unique_ptr(new ExplicitQuantitativeCheckResult(this->computeNextProbabilitiesHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, subResult.getTruthValuesVector()))); @@ -161,7 +161,7 @@ namespace storm { template std::unique_ptr SparseMdpPrctlModelChecker::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic this->getModel()."); + STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic."); std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); @@ -200,7 +200,7 @@ namespace storm { template std::unique_ptr SparseMdpPrctlModelChecker::computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, bool qualitative, boost::optional const& optimalityType) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic this->getModel()."); + STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic."); return std::unique_ptr(new ExplicitQuantitativeCheckResult(this->computeCumulativeRewardsHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, rewardPathFormula.getStepBound()))); } @@ -220,7 +220,7 @@ namespace storm { template std::unique_ptr SparseMdpPrctlModelChecker::computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, bool qualitative, boost::optional const& optimalityType) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic this->getModel()."); + STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic."); return std::unique_ptr(new ExplicitQuantitativeCheckResult(this->computeInstantaneousRewardsHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, rewardPathFormula.getStepCount()))); } @@ -307,7 +307,7 @@ namespace storm { template std::unique_ptr SparseMdpPrctlModelChecker::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, bool qualitative, boost::optional const& optimalityType) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic this->getModel()."); + STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic."); std::unique_ptr subResultPointer = this->check(rewardPathFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); return std::unique_ptr(new ExplicitQuantitativeCheckResult(this->computeReachabilityRewardsHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, subResult.getTruthValuesVector(), qualitative))); diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h index 848abc452..630ce0bb2 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h +++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h @@ -10,6 +10,9 @@ namespace storm { namespace counterexamples { template class SMTMinimalCommandSetGenerator; + + template + class MILPMinimalLabelSetGenerator; } namespace modelchecker { @@ -22,7 +25,8 @@ namespace storm { class SparseMdpPrctlModelChecker : public SparsePropositionalModelChecker { public: friend class SparseMarkovAutomatonCslModelChecker; - friend class counterexamples::SMTMinimalCommandSetGenerator; + friend class storm::counterexamples::SMTMinimalCommandSetGenerator; + friend class storm::counterexamples::MILPMinimalLabelSetGenerator; explicit SparseMdpPrctlModelChecker(storm::models::Mdp const& model); explicit SparseMdpPrctlModelChecker(storm::models::Mdp const& model, std::shared_ptr> nondeterministicLinearEquationSolver); diff --git a/src/utility/cli.h b/src/utility/cli.h index e00c4f612..3e0c31b5a 100644 --- a/src/utility/cli.h +++ b/src/utility/cli.h @@ -321,6 +321,11 @@ namespace storm { } options.addConstantDefinitionsFromString(program, settings.getConstantDefinitionString()); + // Generate command labels if we are going to build a counterexample later. + if (storm::settings::counterexampleGeneratorSettings().isMinimalCommandSetGenerationSet()) { + options.buildCommandLabels = true; + } + // Then, build the model from the symbolic description. result = storm::builder::ExplicitPrismModelBuilder::translateProgram(program, options); return result;