From 64e7cd63f540dd6c9fc9da9f616fdec7d9d05706 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 25 Jan 2016 12:14:11 +0100 Subject: [PATCH] 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