From 2d44d4f822335ae67dab858931c58082d4cb18ba Mon Sep 17 00:00:00 2001 From: sjunges Date: Fri, 15 Jan 2016 19:10:52 +0100 Subject: [PATCH 1/4] getUndefinedConstantsAsString added to storm::prism::program Former-commit-id: 8dbfbf256614d635b3f2cec0511c17d0d66e4f86 --- src/storage/prism/Program.cpp | 15 +++++++++++++++ src/storage/prism/Program.h | 9 ++++++++- 2 files changed, 23 insertions(+), 1 deletion(-) diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp index fee721878..7947b4c78 100644 --- a/src/storage/prism/Program.cpp +++ b/src/storage/prism/Program.cpp @@ -171,6 +171,21 @@ namespace storm { } return result; } + + std::string Program::getUndefinedConstantsAsString() const { + std::stringstream stream; + bool printComma = false; + for (auto const& constant : getUndefinedConstants()) { + if (printComma) { + stream << ", "; + } else { + printComma = true; + } + stream << constant.get().getName() << " (" << constant.get().getType() << ")"; + } + stream << "."; + return stream.str(); + } bool Program::hasConstant(std::string const& constantName) const { return this->constantToIndexMap.find(constantName) != this->constantToIndexMap.end(); diff --git a/src/storage/prism/Program.h b/src/storage/prism/Program.h index b4e6d45b5..45ac16b62 100644 --- a/src/storage/prism/Program.h +++ b/src/storage/prism/Program.h @@ -89,7 +89,14 @@ namespace storm { * @return The undefined constants in the program. */ std::vector> getUndefinedConstants() const; - + + /*! + * Retrieves the undefined constants in the program as a comma-separated string. + * + * @return A string with the undefined constants in the program, separated by a comma + */ + std::string getUndefinedConstantsAsString() const; + /*! * Retrieves whether the given constant exists in the program. * From e4725aa4a18b26077e00a7abed822d5a73657e47 Mon Sep 17 00:00:00 2001 From: sjunges Date: Sat, 16 Jan 2016 14:16:03 +0100 Subject: [PATCH 2/4] Instead of returning the program, return the prepared formulas Former-commit-id: a06fbaad2b434f4772ba4aad5be690ced412a7ac --- src/cli/entrypoints.h | 39 ++++++++++----------------------- src/storage/ModelFormulasPair.h | 16 ++++++++++++++ src/storage/ModelProgramPair.h | 12 ---------- src/utility/storm.h | 27 ++++++++++++++++++----- 4 files changed, 50 insertions(+), 44 deletions(-) create mode 100644 src/storage/ModelFormulasPair.h delete mode 100644 src/storage/ModelProgramPair.h diff --git a/src/cli/entrypoints.h b/src/cli/entrypoints.h index 93f9e1777..b93e4e9ae 100644 --- a/src/cli/entrypoints.h +++ b/src/cli/entrypoints.h @@ -108,47 +108,32 @@ namespace storm { template void buildAndCheckSymbolicModel(storm::prism::Program const& program, std::vector> const& formulas) { - storm::storage::ModelProgramPair modelProgramPair = buildSymbolicModel(program, formulas); - STORM_LOG_THROW(modelProgramPair.model != nullptr, storm::exceptions::InvalidStateException, "Model could not be constructed for an unknown reason."); + storm::storage::ModelFormulasPair modelFormulasPair = buildSymbolicModel(program, formulas); + STORM_LOG_THROW(modelFormulasPair.model != nullptr, storm::exceptions::InvalidStateException, "Model could not be constructed for an unknown reason."); // Preprocess the model if needed. - BRANCH_ON_MODELTYPE(modelProgramPair.model, modelProgramPair.model, ValueType, LibraryType, preprocessModel, formulas); + BRANCH_ON_MODELTYPE(modelFormulasPair.model, modelFormulasPair.model, ValueType, LibraryType, preprocessModel, formulas); // Print some information about the model. - modelProgramPair.model->printModelInformationToStream(std::cout); + modelFormulasPair.model->printModelInformationToStream(std::cout); // Verify the model, if a formula was given. if (!formulas.empty()) { - // There may be constants of the model appearing in the formulas, so we replace all their occurrences - // by their definitions in the translated program. - - // Start by building a mapping from constants of the (translated) model to their defining expressions. - std::map constantSubstitution; - for (auto const& constant : modelProgramPair.program.getConstants()) { - if (constant.isDefined()) { - constantSubstitution.emplace(constant.getExpressionVariable(), constant.getExpression()); - } - } - - std::vector> preparedFormulas; - for (auto const& formula : formulas) { - preparedFormulas.emplace_back(formula->substitute(constantSubstitution)); - } - - if (modelProgramPair.model->isSparseModel()) { + + if (modelFormulasPair.model->isSparseModel()) { if(storm::settings::generalSettings().isCounterexampleSet()) { // If we were requested to generate a counterexample, we now do so for each formula. - for(auto const& formula : preparedFormulas) { - generateCounterexample(program, modelProgramPair.model->as>(), formula); + for(auto const& formula : modelFormulasPair.formulas) { + generateCounterexample(program, modelFormulasPair.model->as>(), formula); } } else { - verifySparseModel(modelProgramPair.model->as>(), preparedFormulas); + verifySparseModel(modelFormulasPair.model->as>(), modelFormulasPair.formulas); } - } else if (modelProgramPair.model->isSymbolicModel()) { + } else if (modelFormulasPair.model->isSymbolicModel()) { if (storm::settings::generalSettings().getEngine() == storm::settings::modules::GeneralSettings::Engine::Hybrid) { - verifySymbolicModelWithHybridEngine(modelProgramPair.model->as>(), preparedFormulas); + verifySymbolicModelWithHybridEngine(modelFormulasPair.model->as>(), modelFormulasPair.formulas); } else { - verifySymbolicModelWithSymbolicEngine(modelProgramPair.model->as>(), preparedFormulas); + verifySymbolicModelWithSymbolicEngine(modelFormulasPair.model->as>(), modelFormulasPair.formulas); } } else { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Invalid input model type."); diff --git a/src/storage/ModelFormulasPair.h b/src/storage/ModelFormulasPair.h new file mode 100644 index 000000000..57181a566 --- /dev/null +++ b/src/storage/ModelFormulasPair.h @@ -0,0 +1,16 @@ +#pragma once +#include "../models/ModelBase.h" + + +namespace storm { + namespace logic { + class Formula; + } + + namespace storage { + struct ModelFormulasPair { + std::shared_ptr model; + std::vector> formulas; + }; + } +} \ No newline at end of file diff --git a/src/storage/ModelProgramPair.h b/src/storage/ModelProgramPair.h deleted file mode 100644 index c50b6d306..000000000 --- a/src/storage/ModelProgramPair.h +++ /dev/null @@ -1,12 +0,0 @@ -#include "../models/ModelBase.h" -#include "prism/Program.h" - - -namespace storm { - namespace storage { - struct ModelProgramPair { - std::shared_ptr model; - storm::prism::Program program; - }; - } -} \ No newline at end of file diff --git a/src/utility/storm.h b/src/utility/storm.h index af70bb89c..0739b2612 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -8,6 +8,7 @@ #include #include #include +#include #include "initialize.h" @@ -46,7 +47,7 @@ // Headers for model processing. #include "src/storage/bisimulation/DeterministicModelBisimulationDecomposition.h" #include "src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.h" -#include "src/storage/ModelProgramPair.h" +#include "src/storage/ModelFormulasPair.h" // Headers for model checking. #include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" @@ -82,10 +83,13 @@ namespace storm { storm::prism::Program parseProgram(std::string const& path); std::vector> parseFormulasForExplicit(std::string const& inputString); std::vector> parseFormulasForProgram(std::string const& inputString, storm::prism::Program const& program); + + template - storm::storage::ModelProgramPair buildSymbolicModel(storm::prism::Program const& program, std::vector> const& formulas) { - storm::storage::ModelProgramPair result; + storm::storage::ModelFormulasPair buildSymbolicModel(storm::prism::Program const& program, std::vector> const& formulas) { + storm::storage::ModelFormulasPair result; + storm::prism::Program translatedProgram; storm::settings::modules::GeneralSettings settings = storm::settings::generalSettings(); @@ -105,7 +109,7 @@ namespace storm { storm::builder::ExplicitPrismModelBuilder builder; result.model = builder.translateProgram(program, options); - result.program = builder.getTranslatedProgram(); + translatedProgram = builder.getTranslatedProgram(); } else if (settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::Dd || settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::Hybrid) { typename storm::builder::DdPrismModelBuilder::Options options; options = typename storm::builder::DdPrismModelBuilder::Options(formulas); @@ -113,9 +117,22 @@ namespace storm { storm::builder::DdPrismModelBuilder builder; result.model = builder.translateProgram(program, options); - result.program = builder.getTranslatedProgram(); + translatedProgram = builder.getTranslatedProgram(); + } + // There may be constants of the model appearing in the formulas, so we replace all their occurrences + // by their definitions in the translated program. + + // Start by building a mapping from constants of the (translated) model to their defining expressions. + std::map constantSubstitution; + for (auto const& constant : translatedProgram.getConstants()) { + if (constant.isDefined()) { + constantSubstitution.emplace(constant.getExpressionVariable(), constant.getExpression()); + } } + for (auto const& formula : formulas) { + result.formulas.emplace_back(formula->substitute(constantSubstitution)); + } return result; } From bfe7354b22a439ab1a7bdc2e3a5a152cdbf99cc5 Mon Sep 17 00:00:00 2001 From: sjunges Date: Mon, 25 Jan 2016 12:02:11 +0100 Subject: [PATCH 3/4] fixed a double extern declaration Former-commit-id: 216058aae1b47c3a721c26f01456eb04a653422a --- src/utility/initialize.cpp | 1 + src/utility/initialize.h | 3 +-- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/utility/initialize.cpp b/src/utility/initialize.cpp index a499dcbfa..d5cbb58db 100644 --- a/src/utility/initialize.cpp +++ b/src/utility/initialize.cpp @@ -1,5 +1,6 @@ #include "initialize.h" +#include "macros.h" #include "src/settings/SettingsManager.h" #include "src/settings/modules/DebugSettings.h" diff --git a/src/utility/initialize.h b/src/utility/initialize.h index 173d52f7e..06fa8c2fa 100644 --- a/src/utility/initialize.h +++ b/src/utility/initialize.h @@ -8,8 +8,7 @@ #include "log4cplus/loggingmacros.h" #include "log4cplus/consoleappender.h" #include "log4cplus/fileappender.h" -extern log4cplus::Logger logger; -extern log4cplus::Logger printer; +#include "macros.h" #include "src/settings/SettingsManager.h" From 64e7cd63f540dd6c9fc9da9f616fdec7d9d05706 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 25 Jan 2016 12:14:11 +0100 Subject: [PATCH 4/4] removed obsolete menu-game model checker class Former-commit-id: 6354fe9895d8ad24737871311ffbe5ddef641861 --- .../reachability/MenuGameMdpModelChecker.cpp | 61 ------------------- .../reachability/MenuGameMdpModelChecker.h | 59 ------------------ 2 files changed, 120 deletions(-) delete mode 100644 src/modelchecker/reachability/MenuGameMdpModelChecker.cpp delete mode 100644 src/modelchecker/reachability/MenuGameMdpModelChecker.h diff --git a/src/modelchecker/reachability/MenuGameMdpModelChecker.cpp b/src/modelchecker/reachability/MenuGameMdpModelChecker.cpp deleted file mode 100644 index 09ad129d3..000000000 --- a/src/modelchecker/reachability/MenuGameMdpModelChecker.cpp +++ /dev/null @@ -1,61 +0,0 @@ -#include "src/modelchecker/reachability/MenuGameMdpModelChecker.h" - -#include "src/utility/macros.h" - -#include "src/exceptions/NotSupportedException.h" - -#include "src/modelchecker/results/CheckResult.h" - -namespace storm { - namespace modelchecker { - MenuGameMdpModelChecker::MenuGameMdpModelChecker(storm::prism::Program const& program, std::unique_ptr&& smtSolverFactory) : originalProgram(program), smtSolverFactory(std::move(smtSolverFactory)) { - STORM_LOG_THROW(program.getModelType() == storm::prism::Program::ModelType::MDP, storm::exceptions::NotSupportedException, "Currently only MDPs are supported by the game-based model checker."); - - // Start by preparing the program. That is, we flatten the modules if there is more than one. - if (originalProgram.getNumberOfModules() > 1) { - preprocessedProgram = originalProgram.flattenModules(smtSolverFactory); - } else { - preprocessedProgram = originalProgram; - } - } - - bool MenuGameMdpModelChecker::canHandle(storm::logic::Formula const& formula) const { - if (formula.isProbabilityOperatorFormula()) { - storm::logic::ProbabilityOperatorFormula const& probabilityOperatorFormula = formula.asProbabilityOperatorFormula(); - return this->canHandle(probabilityOperatorFormula.getSubformula()); - } else if (formula.isUntilFormula() || formula.isEventuallyFormula()) { - if (formula.isUntilFormula()) { - storm::logic::UntilFormula const& untilFormula = formula.asUntilFormula(); - if (untilFormula.getLeftSubformula().isPropositionalFormula() && untilFormula.getRightSubformula().isPropositionalFormula()) { - return true; - } - } else if (formula.isEventuallyFormula()) { - storm::logic::EventuallyFormula const& eventuallyFormula = formula.asEventuallyFormula(); - if (eventuallyFormula.getSubformula().isPropositionalFormula()) { - return true; - } - } - } - return false; - } - - std::unique_ptr MenuGameMdpModelChecker::checkProbabilityOperatorFormula(storm::logic::ProbabilityOperatorFormula const& stateFormula) { - // Depending on whether or not there is a bound, we do something slightly different here. - - return nullptr; - } - - std::unique_ptr computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { - // TODO - - return nullptr; - } - - std::unique_ptr computeEventuallyProbabilities(storm::logic::EventuallyFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { - // TODO - - return nullptr; - } - - } -} \ No newline at end of file diff --git a/src/modelchecker/reachability/MenuGameMdpModelChecker.h b/src/modelchecker/reachability/MenuGameMdpModelChecker.h deleted file mode 100644 index 7919d1bed..000000000 --- a/src/modelchecker/reachability/MenuGameMdpModelChecker.h +++ /dev/null @@ -1,59 +0,0 @@ -#ifndef STORM_MODELCHECKER_MENUGAMEMDPMODELCHECKER_H_ -#define STORM_MODELCHECKER_MENUGAMEMDPMODELCHECKER_H_ - -#include "src/modelchecker/AbstractModelChecker.h" - -#include "src/storage/prism/Program.h" - -#include "src/utility/solver.h" - -namespace storm { - namespace modelchecker { - class MenuGameMdpModelChecker : public AbstractModelChecker { - public: - /*! - * Constructs a model checker whose underlying model is implicitly given by the provided program. All - * verification calls will be answererd with respect to this model. - * - * @param program The program that implicitly specifies the model to check. - * @param smtSolverFactory A factory used to create SMT solver when necessary. - */ - explicit MenuGameMdpModelChecker(storm::prism::Program const& program, std::unique_ptr&& smtSolverFactory); - - virtual bool canHandle(storm::logic::Formula const& formula) const override; - - virtual std::unique_ptr checkProbabilityOperatorFormula(storm::logic::ProbabilityOperatorFormula const& stateFormula) override; - - virtual std::unique_ptr computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeEventuallyProbabilities(storm::logic::EventuallyFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - - private: - /*! - * Performs game-based abstraction refinement on the model until either the precision is met or the provided - * proof goal was successfully proven. - * - * @param filterPredicate A predicate that needs to hold until the target predicate holds. - * @param targetPredicate A predicate characterizing the target states. - * @param precision The precision to use. This governs what difference between lower and upper bounds is - * acceptable. - * @param proofGoal A proof goal that says the probability must only be established to be above/below a given - * threshold. If the proof goal is met before the precision is achieved, the refinement procedure will abort - * and return the current result. - * @return A pair of values, that are under- and over-approximations of the actual probability, respectively. - */ - std::pair performGameBasedRefinement(storm::expressions::Expression const& filterPredicate, storm::expressions::Expression const& targetPredicate, double precision, boost::optional> const& proofGoal); - - // The original program that was used to create this model checker. - storm::prism::Program originalProgram; - - // The preprocessed program that contains only one module and otherwhise corresponds to the semantics of the - // original program. - storm::prism::Program preprocessedProgram; - - // A factory that is used for creating SMT solvers when needed. - std::unique_ptr smtSolverFactory; - }; - } -} - -#endif /* STORM_MODELCHECKER_MENUGAMEMDPMODELCHECKER_H_ */ \ No newline at end of file