From 7da35af0bbf5fe77b04031f0167f941f844ccf72 Mon Sep 17 00:00:00 2001 From: David_Korzeniewski Date: Thu, 29 Jan 2015 12:35:41 +0100 Subject: [PATCH 1/4] Some compile errors on Windows fixed, some still persist. Former-commit-id: 1a9331371b57b1c11285d5dabbffd90fd40dbb1b --- src/modelchecker/ExplicitQualitativeCheckResult.cpp | 8 ++++++++ .../reachability/SparseDtmcEliminationModelChecker.cpp | 1 + src/solver/SmtSolver.h | 6 ++++++ src/solver/Z3SmtSolver.cpp | 5 +++-- src/solver/Z3SmtSolver.h | 2 ++ src/storage/expressions/LinearCoefficientVisitor.h | 2 ++ 6 files changed, 22 insertions(+), 2 deletions(-) diff --git a/src/modelchecker/ExplicitQualitativeCheckResult.cpp b/src/modelchecker/ExplicitQualitativeCheckResult.cpp index b688bb1d8..114819af6 100644 --- a/src/modelchecker/ExplicitQualitativeCheckResult.cpp +++ b/src/modelchecker/ExplicitQualitativeCheckResult.cpp @@ -111,10 +111,18 @@ namespace storm { out << std::boolalpha; map_type const& map = boost::get(truthValues); + +#ifndef WINDOWS typename map_type::const_iterator it = map.begin(); typename map_type::const_iterator itPlusOne = map.begin(); ++itPlusOne; typename map_type::const_iterator ite = map.end(); +#else + map_type::const_iterator it = map.begin(); + map_type::const_iterator itPlusOne = map.begin(); + ++itPlusOne; + map_type::const_iterator ite = map.end(); +#endif for (; it != ite; ++itPlusOne, ++it) { out << it->second; diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp index 4ac0cbd16..86ca64a6b 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp @@ -1,6 +1,7 @@ #include "src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h" #include +#include #ifdef PARAMETRIC_SYSTEMS #include "src/storage/parameters.h" diff --git a/src/solver/SmtSolver.h b/src/solver/SmtSolver.h index 7425e8187..d97481b09 100644 --- a/src/solver/SmtSolver.h +++ b/src/solver/SmtSolver.h @@ -70,9 +70,15 @@ namespace storm { virtual ~SmtSolver(); SmtSolver(SmtSolver const& other) = default; + +#ifndef WINDOWS SmtSolver(SmtSolver&& other) = default; +#endif SmtSolver& operator=(SmtSolver const& other) = default; + +#ifndef WINDOWS SmtSolver& operator=(SmtSolver&& other) = default; +#endif /*! * Pushes a backtracking point on the solver's stack. A following call to pop() deletes exactly those diff --git a/src/solver/Z3SmtSolver.cpp b/src/solver/Z3SmtSolver.cpp index 0e89d1d6c..b8b93431a 100644 --- a/src/solver/Z3SmtSolver.cpp +++ b/src/solver/Z3SmtSolver.cpp @@ -155,6 +155,7 @@ namespace storm { #endif } +#ifndef WINDOWS SmtSolver::CheckResult Z3SmtSolver::checkWithAssumptions(std::initializer_list const& assumptions) { #ifdef STORM_HAVE_Z3 @@ -181,7 +182,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support."); #endif } - +#endif storm::expressions::SimpleValuation Z3SmtSolver::getModelAsValuation() { #ifdef STORM_HAVE_Z3 @@ -229,7 +230,7 @@ namespace storm { { #ifdef STORM_HAVE_Z3 std::vector valuations; - this->allSat(important, [&valuations](storm::expressions::SimpleValuation const& valuation) -> bool { valuations.push_back(valuation); return true; }); + this->allSat(important, static_cast>([&valuations](storm::expressions::SimpleValuation const& valuation) -> bool { valuations.push_back(valuation); return true; })); return valuations; #else STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support."); diff --git a/src/solver/Z3SmtSolver.h b/src/solver/Z3SmtSolver.h index 1e0fd2a43..1873cb4df 100644 --- a/src/solver/Z3SmtSolver.h +++ b/src/solver/Z3SmtSolver.h @@ -51,7 +51,9 @@ namespace storm { virtual CheckResult checkWithAssumptions(std::set const& assumptions) override; +#ifndef WINDOWS virtual CheckResult checkWithAssumptions(std::initializer_list const& assumptions) override; +#endif virtual storm::expressions::SimpleValuation getModelAsValuation() override; diff --git a/src/storage/expressions/LinearCoefficientVisitor.h b/src/storage/expressions/LinearCoefficientVisitor.h index 3b675a60d..b48c53d09 100644 --- a/src/storage/expressions/LinearCoefficientVisitor.h +++ b/src/storage/expressions/LinearCoefficientVisitor.h @@ -18,8 +18,10 @@ namespace storm { VariableCoefficients(VariableCoefficients const& other) = default; VariableCoefficients& operator=(VariableCoefficients const& other) = default; +#ifndef WINDOWS VariableCoefficients(VariableCoefficients&& other) = default; VariableCoefficients& operator=(VariableCoefficients&& other) = default; +#endif VariableCoefficients& operator+=(VariableCoefficients&& other); VariableCoefficients& operator-=(VariableCoefficients&& other); From ab36c5fb0d61eb51821db8412c032233de746178 Mon Sep 17 00:00:00 2001 From: David_Korzeniewski Date: Thu, 29 Jan 2015 15:04:02 +0100 Subject: [PATCH 2/4] Workarounds for more Windows quirks. Compiles but tests crash. Former-commit-id: 0c47ae886d0fcd4577cf9752392993ff331ff812 --- src/solver/MathsatSmtSolver.cpp | 2 ++ src/solver/MathsatSmtSolver.h | 2 ++ src/solver/SmtSolver.h | 4 +++- src/storage/expressions/Expression.h | 10 ++++++++++ 4 files changed, 17 insertions(+), 1 deletion(-) diff --git a/src/solver/MathsatSmtSolver.cpp b/src/solver/MathsatSmtSolver.cpp index 9627c8dea..16610f4ad 100644 --- a/src/solver/MathsatSmtSolver.cpp +++ b/src/solver/MathsatSmtSolver.cpp @@ -191,6 +191,7 @@ namespace storm { #endif } +#ifndef WINDOWS SmtSolver::CheckResult MathsatSmtSolver::checkWithAssumptions(std::initializer_list const& assumptions) { #ifdef STORM_HAVE_MSAT @@ -218,6 +219,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support."); #endif } +#endif storm::expressions::SimpleValuation MathsatSmtSolver::getModelAsValuation() { diff --git a/src/solver/MathsatSmtSolver.h b/src/solver/MathsatSmtSolver.h index badca77a8..a1ec0810b 100644 --- a/src/solver/MathsatSmtSolver.h +++ b/src/solver/MathsatSmtSolver.h @@ -79,7 +79,9 @@ namespace storm { virtual CheckResult checkWithAssumptions(std::set const& assumptions) override; +#ifndef WINDOWS virtual CheckResult checkWithAssumptions(std::initializer_list const& assumptions) override; +#endif virtual storm::expressions::SimpleValuation getModelAsValuation() override; diff --git a/src/solver/SmtSolver.h b/src/solver/SmtSolver.h index d97481b09..475c3ee95 100644 --- a/src/solver/SmtSolver.h +++ b/src/solver/SmtSolver.h @@ -152,8 +152,10 @@ namespace storm { * @param assumptions The assumptions to add to the call. * @return Sat if the conjunction of the asserted expressions together with the provided assumptions is * satisfiable, Unsat if it is unsatisfiable and Unknown if the solver could not determine satisfiability. - */ + */ +#ifndef WINDOWS virtual CheckResult checkWithAssumptions(std::initializer_list const& assumptions) = 0; +#endif /*! * If the last call to check() or checkWithAssumptions() returned Sat, this method retrieves a model that diff --git a/src/storage/expressions/Expression.h b/src/storage/expressions/Expression.h index 2c7360b08..777bde9f9 100644 --- a/src/storage/expressions/Expression.h +++ b/src/storage/expressions/Expression.h @@ -324,4 +324,14 @@ namespace storm { } } +//specialize +namespace std { + template<> + struct less < storm::expressions::Expression > { + bool operator()(const storm::expressions::Expression& lhs, const storm::expressions::Expression& rhs) const { + return lhs.getBaseExpressionPointer() < rhs.getBaseExpressionPointer(); + } + }; +} + #endif /* STORM_STORAGE_EXPRESSIONS_EXPRESSION_H_ */ \ No newline at end of file From abc222fc31dcb74a37f238da9082dc381e0d385a Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 29 Jan 2015 15:56:39 +0100 Subject: [PATCH 3/4] Fixed some compilation errors. Former-commit-id: b344bee8d277e6cfb9616c9ecc01a8f61d508d79 --- src/counterexamples/SMTMinimalCommandSetGenerator.h | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/counterexamples/SMTMinimalCommandSetGenerator.h b/src/counterexamples/SMTMinimalCommandSetGenerator.h index 501fc097c..250083ea7 100644 --- a/src/counterexamples/SMTMinimalCommandSetGenerator.h +++ b/src/counterexamples/SMTMinimalCommandSetGenerator.h @@ -1691,7 +1691,7 @@ namespace storm { modelCheckingClock = std::chrono::high_resolution_clock::now(); commandSet.insert(relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end()); storm::models::Mdp subMdp = labeledMdp.restrictChoiceLabels(commandSet); - storm::modelchecker::prctl::SparseMdpPrctlModelChecker modelchecker(subMdp); + storm::modelchecker::SparseMdpPrctlModelChecker modelchecker(subMdp); LOG4CPLUS_DEBUG(logger, "Invoking model checker."); std::vector result = modelchecker.checkUntil(false, phiStates, psiStates, false).first; LOG4CPLUS_DEBUG(logger, "Computed model checking results."); @@ -1776,20 +1776,20 @@ namespace storm { std::unique_ptr leftResult = modelchecker.check(untilFormula.getLeftSubformula()); std::unique_ptr rightResult = modelchecker.check(untilFormula.getRightSubformula()); - storm::modelchecker::ExplicitQualitativeCheckResult const& leftQualitativeResult = leftResult.asExplicitQualitativeCheckResult(); - storm::modelchecker::ExplicitQualitativeCheckResult const& rightQualitativeResult = rightResult.asExplicitQualitativeCheckResult(); + storm::modelchecker::ExplicitQualitativeCheckResult const& leftQualitativeResult = leftResult->asExplicitQualitativeCheckResult(); + storm::modelchecker::ExplicitQualitativeCheckResult const& rightQualitativeResult = rightResult->asExplicitQualitativeCheckResult(); phiStates = leftQualitativeResult.getTruthValuesVector(); psiStates = rightQualitativeResult.getTruthValuesVector(); } else if (probabilityOperator.getSubformula().isEventuallyFormula()) { storm::logic::EventuallyFormula const& eventuallyFormula = probabilityOperator.getSubformula().asEventuallyFormula(); - std::unique_ptr subResult = modelchecker.check(untilFormula.getSubformula()); + std::unique_ptr subResult = modelchecker.check(eventuallyFormula.getSubformula()); storm::modelchecker::ExplicitQualitativeCheckResult const& subQualitativeResult = subResult.asExplicitQualitativeCheckResult(); phiStates = storm::storage::BitVector(labeledMdp.getNumberOfStates(), true); - psiStates = subResult.getTruthValuesVector(); + psiStates = subResult->getTruthValuesVector(); } // Delegate the actual computation work to the function of equal name. From 98efde80f774859262db0936350c8a6661c2298a Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 29 Jan 2015 17:44:43 +0100 Subject: [PATCH 4/4] Fixed some compile issues (and some other issues). Former-commit-id: e07861bd92fb8e8e1f5174aa3a804a29aad53b08 --- src/counterexamples/SMTMinimalCommandSetGenerator.h | 2 +- src/logic/BinaryPathFormula.cpp | 2 ++ src/logic/BinaryStateFormula.cpp | 2 ++ src/modelchecker/prctl/SparseMdpPrctlModelChecker.h | 6 ++++++ src/utility/cli.h | 3 +-- 5 files changed, 12 insertions(+), 3 deletions(-) diff --git a/src/counterexamples/SMTMinimalCommandSetGenerator.h b/src/counterexamples/SMTMinimalCommandSetGenerator.h index 250083ea7..fcb0aff94 100644 --- a/src/counterexamples/SMTMinimalCommandSetGenerator.h +++ b/src/counterexamples/SMTMinimalCommandSetGenerator.h @@ -1693,7 +1693,7 @@ namespace storm { storm::models::Mdp subMdp = labeledMdp.restrictChoiceLabels(commandSet); storm::modelchecker::SparseMdpPrctlModelChecker modelchecker(subMdp); LOG4CPLUS_DEBUG(logger, "Invoking model checker."); - std::vector result = modelchecker.checkUntil(false, phiStates, psiStates, false).first; + std::vector result = modelchecker.computeUntilProbabilitiesHelper(false, phiStates, psiStates, false) LOG4CPLUS_DEBUG(logger, "Computed model checking results."); totalModelCheckingTime += std::chrono::high_resolution_clock::now() - modelCheckingClock; diff --git a/src/logic/BinaryPathFormula.cpp b/src/logic/BinaryPathFormula.cpp index 046d53803..adfac9686 100644 --- a/src/logic/BinaryPathFormula.cpp +++ b/src/logic/BinaryPathFormula.cpp @@ -44,10 +44,12 @@ namespace storm { void BinaryPathFormula::gatherAtomicExpressionFormulas(std::vector>& atomicExpressionFormulas) const { this->getLeftSubformula().gatherAtomicExpressionFormulas(atomicExpressionFormulas); + this->getLeftSubformula().gatherAtomicExpressionFormulas(atomicExpressionFormulas); } void BinaryPathFormula::gatherAtomicLabelFormulas(std::vector>& atomicLabelFormulas) const { this->getLeftSubformula().gatherAtomicLabelFormulas(atomicLabelFormulas); + this->getRightSubformula().gatherAtomicLabelFormulas(atomicLabelFormulas); } } } \ No newline at end of file diff --git a/src/logic/BinaryStateFormula.cpp b/src/logic/BinaryStateFormula.cpp index e8557651b..fb9a7560e 100644 --- a/src/logic/BinaryStateFormula.cpp +++ b/src/logic/BinaryStateFormula.cpp @@ -44,10 +44,12 @@ namespace storm { void BinaryStateFormula::gatherAtomicExpressionFormulas(std::vector>& atomicExpressionFormulas) const { this->getLeftSubformula().gatherAtomicExpressionFormulas(atomicExpressionFormulas); + this->getRightSubformula().gatherAtomicExpressionFormulas(atomicExpressionFormulas); } void BinaryStateFormula::gatherAtomicLabelFormulas(std::vector>& atomicLabelFormulas) const { this->getLeftSubformula().gatherAtomicLabelFormulas(atomicLabelFormulas); + this->getRightSubformula().gatherAtomicLabelFormulas(atomicLabelFormulas); } } } \ No newline at end of file diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h index a24dfcc06..a3a7a9c08 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h +++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h @@ -7,6 +7,11 @@ #include "src/solver/NondeterministicLinearEquationSolver.h" namespace storm { + namespace counterexamples { + template + class SMTMinimalCommandSetGenerator; + } + namespace modelchecker { // Forward-declare other model checkers to make them friend classes. @@ -17,6 +22,7 @@ namespace storm { class SparseMdpPrctlModelChecker : public AbstractModelChecker { public: friend class SparseMarkovAutomatonCslModelChecker; + friend class counterexamples::SMTMinimalCommandSetGenerator; 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 73ff738ee..de987e365 100644 --- a/src/utility/cli.h +++ b/src/utility/cli.h @@ -274,9 +274,8 @@ namespace storm { typename storm::builder::ExplicitPrismModelBuilder::Options options; if (formula) { options = storm::builder::ExplicitPrismModelBuilder::Options(*formula.get()); - } else { - options.addConstantDefinitionsFromString(program, settings.getConstantDefinitionString()); } + options.addConstantDefinitionsFromString(program, settings.getConstantDefinitionString()); // Then, build the model from the symbolic description. result = storm::builder::ExplicitPrismModelBuilder::translateProgram(program, options);