From aca21eaf184ce2c0902e675bd4aa457bec6b22a5 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Mon, 8 Aug 2016 22:34:18 +0200
Subject: [PATCH] commit to switch workplace (no, not now)
Former-commit-id: b725946b2888c29f76c77fb73a21d4646628a7ad
---
src/abstraction/prism/AbstractProgram.h | 2 ++
src/abstraction/prism/PrismMenuGameAbstractor.cpp | 2 +-
src/abstraction/prism/PrismMenuGameAbstractor.h | 2 +-
.../abstraction/GameBasedMdpModelChecker.cpp | 13 ++++++++++++-
.../abstraction/GameBasedMdpModelChecker.h | 5 ++++-
5 files changed, 20 insertions(+), 4 deletions(-)
diff --git a/src/abstraction/prism/AbstractProgram.h b/src/abstraction/prism/AbstractProgram.h
index 8b4eb9a82..435d905d8 100644
--- a/src/abstraction/prism/AbstractProgram.h
+++ b/src/abstraction/prism/AbstractProgram.h
@@ -7,6 +7,8 @@
#include "src/abstraction/MenuGame.h"
#include "src/abstraction/prism/AbstractModule.h"
+#include "src/storage/dd/Add.h"
+
#include "src/storage/expressions/Expression.h"
namespace storm {
diff --git a/src/abstraction/prism/PrismMenuGameAbstractor.cpp b/src/abstraction/prism/PrismMenuGameAbstractor.cpp
index 996d66db7..1d965f344 100644
--- a/src/abstraction/prism/PrismMenuGameAbstractor.cpp
+++ b/src/abstraction/prism/PrismMenuGameAbstractor.cpp
@@ -8,7 +8,7 @@ namespace storm {
namespace prism {
template <storm::dd::DdType DdType, typename ValueType>
- PrismMenuGameAbstractor<DdType, ValueType>::PrismMenuGameAbstractor(storm::expressions::ExpressionManager& expressionManager, storm::prism::Program const& program, std::vector<storm::expressions::Expression> const& initialPredicates, std::unique_ptr<storm::utility::solver::SmtSolverFactory>&& smtSolverFactory) : abstractProgram(expressionManager, program, initialPredicates, std::move(smtSolverFactory), storm::settings::getModule<storm::settings::modules::AbstractionSettings>().isAddAllGuardsSet()) {
+ PrismMenuGameAbstractor<DdType, ValueType>::PrismMenuGameAbstractor(storm::expressions::ExpressionManager& expressionManager, storm::prism::Program const& program, std::vector<storm::expressions::Expression> const& initialPredicates, storm::utility::solver::SmtSolverFactory const& smtSolverFactory) : abstractProgram(expressionManager, program, initialPredicates, std::move(smtSolverFactory), storm::settings::getModule<storm::settings::modules::AbstractionSettings>().isAddAllGuardsSet()) {
// Intentionally left empty.
}
diff --git a/src/abstraction/prism/PrismMenuGameAbstractor.h b/src/abstraction/prism/PrismMenuGameAbstractor.h
index b3f30bea7..44301bc7f 100644
--- a/src/abstraction/prism/PrismMenuGameAbstractor.h
+++ b/src/abstraction/prism/PrismMenuGameAbstractor.h
@@ -11,7 +11,7 @@ namespace storm {
template <storm::dd::DdType DdType, typename ValueType>
class PrismMenuGameAbstractor : public MenuGameAbstractor<DdType, ValueType> {
public:
- PrismMenuGameAbstractor(storm::expressions::ExpressionManager& expressionManager, storm::prism::Program const& program, std::vector<storm::expressions::Expression> const& initialPredicates, std::unique_ptr<storm::utility::solver::SmtSolverFactory>&& smtSolverFactory = std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>());
+ PrismMenuGameAbstractor(storm::expressions::ExpressionManager& expressionManager, storm::prism::Program const& program, std::vector<storm::expressions::Expression> const& initialPredicates, storm::utility::solver::SmtSolverFactory const& smtSolverFactory);
virtual storm::abstraction::MenuGame<DdType, ValueType> abstract() override;
virtual void refine(std::vector<storm::expressions::Expression> const& predicates) override;
diff --git a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
index bf946d58a..a24189152 100644
--- a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
+++ b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
@@ -1,7 +1,11 @@
#include "src/modelchecker/abstraction/GameBasedMdpModelChecker.h"
+#include "src/models/symbolic/StandardRewardModel.h"
+
#include "src/storage/expressions/ExpressionManager.h"
+#include "src/abstraction/prism/PrismMenuGameAbstractor.h"
+
#include "src/logic/FragmentSpecification.h"
#include "src/utility/macros.h"
@@ -14,7 +18,7 @@
namespace storm {
namespace modelchecker {
template<storm::dd::DdType Type, typename ValueType>
- GameBasedMdpModelChecker<Type, ValueType>::GameBasedMdpModelChecker(storm::prism::Program const& program, std::unique_ptr<storm::utility::solver::SmtSolverFactory>&& smtSolverFactory) : originalProgram(program), smtSolverFactory(std::move(smtSolverFactory)) {
+ GameBasedMdpModelChecker<Type, ValueType>::GameBasedMdpModelChecker(storm::expressions::ExpressionManager& expressionManager, storm::prism::Program const& program, std::unique_ptr<storm::utility::solver::SmtSolverFactory>&& smtSolverFactory) : originalProgram(program), expressionManager(expressionManager), smtSolverFactory(std::move(smtSolverFactory)) {
STORM_LOG_THROW(program.getModelType() == storm::prism::Program::ModelType::DTMC || program.getModelType() == storm::prism::Program::ModelType::MDP, storm::exceptions::NotSupportedException, "Currently only DTMCs/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.
@@ -52,6 +56,13 @@ namespace storm {
template<storm::dd::DdType Type, typename ValueType>
std::unique_ptr<CheckResult> GameBasedMdpModelChecker<Type, ValueType>::performGameBasedAbstractionRefinement(CheckTask<storm::logic::Formula> 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.");
+
+ std::vector<storm::expressions::Expression> initialPredicates;
+ initialPredicates.push_back(targetStateExpression);
+ if (!constraintExpression.isTrue() && !constraintExpression.isFalse()) {
+ initialPredicates.push_back(constraintExpression);
+ }
+ storm::abstraction::prism::PrismMenuGameAbstractor<Type, ValueType> abstractor(expressionManager, preprocessedProgram, initialPredicates, *smtSolverFactory);
// 1. build initial abstraction based on the the constraint expression (if not 'true') and the target state expression.
diff --git a/src/modelchecker/abstraction/GameBasedMdpModelChecker.h b/src/modelchecker/abstraction/GameBasedMdpModelChecker.h
index 6f289859b..0c6658fee 100644
--- a/src/modelchecker/abstraction/GameBasedMdpModelChecker.h
+++ b/src/modelchecker/abstraction/GameBasedMdpModelChecker.h
@@ -21,7 +21,7 @@ namespace storm {
* @param program The program that implicitly specifies the model to check.
* @param smtSolverFactory A factory used to create SMT solver when necessary.
*/
- explicit GameBasedMdpModelChecker(storm::prism::Program const& program, std::unique_ptr<storm::utility::solver::SmtSolverFactory>&& smtSolverFactory = std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>());
+ explicit GameBasedMdpModelChecker(storm::expressions::ExpressionManager& expressionManager, storm::prism::Program const& program, std::unique_ptr<storm::utility::solver::SmtSolverFactory>&& smtSolverFactory = std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>());
virtual ~GameBasedMdpModelChecker() override;
@@ -42,6 +42,9 @@ namespace storm {
// original program.
storm::prism::Program preprocessedProgram;
+ /// The expression manager over which to build expressions during the abstraction.
+ storm::expressions::ExpressionManager& expressionManager;
+
// A factory that is used for creating SMT solvers when needed.
std::unique_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory;
};