From 9e9e23a37099ea5e47d57c2bbaa8893f827874c5 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 5 Feb 2016 15:14:53 +0100 Subject: [PATCH] more preparation for game-based abstraction Former-commit-id: 0607d79be616603f7f5226530bdff4f614b4cecc --- .../abstraction/GameBasedMdpModelChecker.cpp | 44 +++++++++---------- .../abstraction/GameBasedMdpModelChecker.h | 6 +-- 2 files changed, 23 insertions(+), 27 deletions(-) diff --git a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index 56770de22..da27f0d82 100644 --- a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -1,5 +1,7 @@ #include "src/modelchecker/abstraction/GameBasedMdpModelChecker.h" +#include "src/storage/expressions/ExpressionManager.h" + #include "src/utility/macros.h" #include "src/exceptions/NotSupportedException.h" @@ -30,8 +32,7 @@ namespace storm { bool GameBasedMdpModelChecker::canHandle(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); if (formula.isProbabilityOperatorFormula()) { - storm::logic::ProbabilityOperatorFormula const& probabilityOperatorFormula = formula.asProbabilityOperatorFormula(); - return this->canHandle(checkTask.replaceFormula(probabilityOperatorFormula.getSubformula())); + return this->canHandle(checkTask.replaceFormula(formula.asProbabilityOperatorFormula().getSubformula())); } else if (formula.isUntilFormula() || formula.isEventuallyFormula()) { if (formula.isUntilFormula()) { storm::logic::UntilFormula const& untilFormula = formula.asUntilFormula(); @@ -47,39 +48,34 @@ namespace storm { } return false; } - - template - std::unique_ptr GameBasedMdpModelChecker::checkProbabilityOperatorFormula(CheckTask const& checkTask) { - // Depending on whether or not there is a bound, we do something slightly different here. - return nullptr; - } - + template std::unique_ptr GameBasedMdpModelChecker::computeUntilProbabilities(CheckTask const& checkTask) { - // TODO - return nullptr; + storm::logic::UntilFormula const& pathFormula = checkTask.getFormula(); + return performGameBasedAbstractionRefinement(CheckTask(pathFormula), getExpression(pathFormula.getLeftSubformula()), getExpression(pathFormula.getRightSubformula())); } template std::unique_ptr GameBasedMdpModelChecker::computeEventuallyProbabilities(CheckTask const& checkTask) { storm::logic::EventuallyFormula const& pathFormula = checkTask.getFormula(); - storm::logic::Formula const& subformula = pathFormula.getSubformula(); - STORM_LOG_THROW(subformula.isAtomicExpressionFormula() || subformula.isAtomicLabelFormula(), storm::exceptions::InvalidPropertyException, "The target states have to be given as label or an expression."); - storm::expressions::Expression targetStateExpression; - if (subformula.isAtomicLabelFormula()) { - targetStateExpression = preprocessedProgram.getLabelExpression(subformula.asAtomicLabelFormula().getLabel()); - } else { - targetStateExpression = subformula.asAtomicExpressionFormula().getExpression(); - } - - performGameBasedAbstractionRefinement(CheckTask(pathFormula), targetStateExpression); - + return performGameBasedAbstractionRefinement(CheckTask(pathFormula), originalProgram.getManager().boolean(true), getExpression(pathFormula.getSubformula())); + } + + template + std::unique_ptr GameBasedMdpModelChecker::performGameBasedAbstractionRefinement(CheckTask const& checkTask, storm::expressions::Expression const& constraintExpression, storm::expressions::Expression const& targetStateExpression) { return nullptr; } template - void GameBasedMdpModelChecker::performGameBasedAbstractionRefinement(CheckTask const& checkTask, storm::expressions::Expression const& targetStateExpression) { - std::cout << "hello world" << std::endl; + storm::expressions::Expression GameBasedMdpModelChecker::getExpression(storm::logic::Formula const& formula) { + STORM_LOG_THROW(formula.isAtomicExpressionFormula() || formula.isAtomicLabelFormula(), storm::exceptions::InvalidPropertyException, "The target states have to be given as label or an expression."); + storm::expressions::Expression result; + if (formula.isAtomicLabelFormula()) { + result = preprocessedProgram.getLabelExpression(formula.asAtomicLabelFormula().getLabel()); + } else { + result = formula.asAtomicExpressionFormula().getExpression(); + } + return result; } template class GameBasedMdpModelChecker; diff --git a/src/modelchecker/abstraction/GameBasedMdpModelChecker.h b/src/modelchecker/abstraction/GameBasedMdpModelChecker.h index cb3f5ebb2..c10510ec0 100644 --- a/src/modelchecker/abstraction/GameBasedMdpModelChecker.h +++ b/src/modelchecker/abstraction/GameBasedMdpModelChecker.h @@ -27,13 +27,13 @@ namespace storm { virtual bool canHandle(CheckTask const& checkTask) const override; - virtual std::unique_ptr checkProbabilityOperatorFormula(CheckTask const& stateFormula) override; - virtual std::unique_ptr computeUntilProbabilities(CheckTask const& checkTask) override; virtual std::unique_ptr computeEventuallyProbabilities(CheckTask const& checkTask) override; private: - void performGameBasedAbstractionRefinement(CheckTask const& checkTask, storm::expressions::Expression const& targetStateExpression); + std::unique_ptr performGameBasedAbstractionRefinement(CheckTask const& checkTask, storm::expressions::Expression const& constraintExpression, storm::expressions::Expression const& targetStateExpression); + + storm::expressions::Expression getExpression(storm::logic::Formula const& formula); // The original program that was used to create this model checker. storm::prism::Program originalProgram;