From 824d026860539dd8e26a3dcd6382ba129abe1fe5 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 5 Feb 2016 15:29:27 +0100 Subject: [PATCH] started to write outline of abstraction-refinement procedure Former-commit-id: f5847873468922831143b71b6e9008f6af528545 --- .../abstraction/GameBasedMdpModelChecker.cpp | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index da27f0d82..71e39cf67 100644 --- a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -63,6 +63,19 @@ namespace storm { template std::unique_ptr GameBasedMdpModelChecker::performGameBasedAbstractionRefinement(CheckTask const& checkTask, storm::expressions::Expression const& constraintExpression, storm::expressions::Expression const& targetStateExpression) { + + STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::InvalidPropertyException, "The game-based abstraction refinement model checker can only compute the result for the initial states."); + + // 1. build initial abstraction based on the the constraint expression (if not 'true') and the target state expression. + + // 2. solve the game wrt. to min/max as given by checkTask and min/max for the abstraction player to obtain two bounds. + // Note that we have to deal with bottom states if not all guards were added in the beginning. + // Also note that it might be the case that not both bounds need to be computed if there is a bound given in checkTask. + + // 3. if the bounds suffice to complete checkTask, return result now. + + // 4. if the bounds do not suffice + return nullptr; }