From 7b2bfa592cecd4d3f4124a811c8db2acaf5120e6 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 24 Jul 2015 17:37:51 -0700 Subject: [PATCH] started working on integration of games-based abstraction refinement in production code quality Former-commit-id: 123de72725b710c6e4476a6fd4921e726c03d0af --- .../reachability/MenuGameMdpModelChecker.cpp | 57 ++++++++++++++++++ .../reachability/MenuGameMdpModelChecker.h | 59 +++++++++++++++++++ 2 files changed, 116 insertions(+) create mode 100644 src/modelchecker/reachability/MenuGameMdpModelChecker.cpp create mode 100644 src/modelchecker/reachability/MenuGameMdpModelChecker.h diff --git a/src/modelchecker/reachability/MenuGameMdpModelChecker.cpp b/src/modelchecker/reachability/MenuGameMdpModelChecker.cpp new file mode 100644 index 000000000..1504a589b --- /dev/null +++ b/src/modelchecker/reachability/MenuGameMdpModelChecker.cpp @@ -0,0 +1,57 @@ +#include "src/modelchecker/reachability/MenuGameMdpModelChecker.h" + +#include "src/exceptions/NotSupportedException.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 new file mode 100644 index 000000000..9bb680a5d --- /dev/null +++ b/src/modelchecker/reachability/MenuGameMdpModelChecker.h @@ -0,0 +1,59 @@ +#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