From c83db93c557eacf9e355d67cb80b700a9cd69494 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Fri, 5 Feb 2016 13:33:36 +0100
Subject: [PATCH] made everything compile again after latest changes
(CheckTasks)
Former-commit-id: 57fce885f65ce3aa9355c9591f36345542c8a3ac
---
src/cli/entrypoints.h | 2 +-
.../abstraction/GameBasedMdpModelChecker.cpp | 30 +++++++++++++++----
.../abstraction/GameBasedMdpModelChecker.h | 10 ++++---
src/utility/storm.h | 5 ++--
4 files changed, 34 insertions(+), 13 deletions(-)
diff --git a/src/cli/entrypoints.h b/src/cli/entrypoints.h
index 479c599db..36db3dcf4 100644
--- a/src/cli/entrypoints.h
+++ b/src/cli/entrypoints.h
@@ -48,7 +48,7 @@ namespace storm {
#endif
template<typename ValueType, storm::dd::DdType DdType>
- void verifySymbolicModelWithAbstractionRefinementEngine(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas, bool onlyInitialStatesRelevant = false) {
+ void verifySymbolicModelWithAbstractionRefinementEngine(storm::prism::Program const& program, std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas, bool onlyInitialStatesRelevant = false) {
for (auto const& formula : formulas) {
std::cout << std::endl << "Model checking property: " << *formula << " ...";
std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifyProgramWithAbstractionRefinementEngine<DdType, ValueType>(program, formula, onlyInitialStatesRelevant));
diff --git a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
index 1e603b6e8..56770de22 100644
--- a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
+++ b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
@@ -3,6 +3,7 @@
#include "src/utility/macros.h"
#include "src/exceptions/NotSupportedException.h"
+#include "src/exceptions/InvalidPropertyException.h"
#include "src/modelchecker/results/CheckResult.h"
@@ -26,10 +27,11 @@ namespace storm {
}
template<storm::dd::DdType Type, typename ValueType>
- bool GameBasedMdpModelChecker<Type, ValueType>::canHandle(storm::logic::Formula const& formula) const {
+ bool GameBasedMdpModelChecker<Type, ValueType>::canHandle(CheckTask<storm::logic::Formula> const& checkTask) const {
+ storm::logic::Formula const& formula = checkTask.getFormula();
if (formula.isProbabilityOperatorFormula()) {
storm::logic::ProbabilityOperatorFormula const& probabilityOperatorFormula = formula.asProbabilityOperatorFormula();
- return this->canHandle(probabilityOperatorFormula.getSubformula());
+ return this->canHandle(checkTask.replaceFormula(probabilityOperatorFormula.getSubformula()));
} else if (formula.isUntilFormula() || formula.isEventuallyFormula()) {
if (formula.isUntilFormula()) {
storm::logic::UntilFormula const& untilFormula = formula.asUntilFormula();
@@ -47,23 +49,39 @@ namespace storm {
}
template<storm::dd::DdType Type, typename ValueType>
- std::unique_ptr<CheckResult> GameBasedMdpModelChecker<Type, ValueType>::checkProbabilityOperatorFormula(storm::logic::ProbabilityOperatorFormula const& stateFormula) {
+ std::unique_ptr<CheckResult> GameBasedMdpModelChecker<Type, ValueType>::checkProbabilityOperatorFormula(CheckTask<storm::logic::ProbabilityOperatorFormula> const& checkTask) {
// Depending on whether or not there is a bound, we do something slightly different here.
return nullptr;
}
template<storm::dd::DdType Type, typename ValueType>
- std::unique_ptr<CheckResult> GameBasedMdpModelChecker<Type, ValueType>::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional<OptimizationDirection> const& optimalityType) {
+ std::unique_ptr<CheckResult> GameBasedMdpModelChecker<Type, ValueType>::computeUntilProbabilities(CheckTask<storm::logic::UntilFormula> const& checkTask) {
// TODO
return nullptr;
}
template<storm::dd::DdType Type, typename ValueType>
- std::unique_ptr<CheckResult> GameBasedMdpModelChecker<Type, ValueType>::computeEventuallyProbabilities(storm::logic::EventuallyFormula const& pathFormula, bool qualitative, boost::optional<OptimizationDirection> const& optimalityType) {
- // TODO
+ std::unique_ptr<CheckResult> GameBasedMdpModelChecker<Type, ValueType>::computeEventuallyProbabilities(CheckTask<storm::logic::EventuallyFormula> 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<storm::logic::Formula>(pathFormula), targetStateExpression);
+
return nullptr;
}
+ template<storm::dd::DdType Type, typename ValueType>
+ void GameBasedMdpModelChecker<Type, ValueType>::performGameBasedAbstractionRefinement(CheckTask<storm::logic::Formula> const& checkTask, storm::expressions::Expression const& targetStateExpression) {
+ std::cout << "hello world" << std::endl;
+ }
+
template class GameBasedMdpModelChecker<storm::dd::DdType::CUDD, double>;
}
}
\ No newline at end of file
diff --git a/src/modelchecker/abstraction/GameBasedMdpModelChecker.h b/src/modelchecker/abstraction/GameBasedMdpModelChecker.h
index 3edae3d71..cb3f5ebb2 100644
--- a/src/modelchecker/abstraction/GameBasedMdpModelChecker.h
+++ b/src/modelchecker/abstraction/GameBasedMdpModelChecker.h
@@ -25,14 +25,16 @@ namespace storm {
virtual ~GameBasedMdpModelChecker() override;
- virtual bool canHandle(storm::logic::Formula const& formula) const override;
+ virtual bool canHandle(CheckTask<storm::logic::Formula> const& checkTask) const override;
- virtual std::unique_ptr<CheckResult> checkProbabilityOperatorFormula(storm::logic::ProbabilityOperatorFormula const& stateFormula) override;
+ virtual std::unique_ptr<CheckResult> checkProbabilityOperatorFormula(CheckTask<storm::logic::ProbabilityOperatorFormula> const& stateFormula) override;
- virtual std::unique_ptr<CheckResult> computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional<OptimizationDirection> const& optimalityType = boost::optional<OptimizationDirection>()) override;
- virtual std::unique_ptr<CheckResult> computeEventuallyProbabilities(storm::logic::EventuallyFormula const& pathFormula, bool qualitative = false, boost::optional<OptimizationDirection> const& optimalityType = boost::optional<OptimizationDirection>()) override;
+ virtual std::unique_ptr<CheckResult> computeUntilProbabilities(CheckTask<storm::logic::UntilFormula> const& checkTask) override;
+ virtual std::unique_ptr<CheckResult> computeEventuallyProbabilities(CheckTask<storm::logic::EventuallyFormula> const& checkTask) override;
private:
+ void performGameBasedAbstractionRefinement(CheckTask<storm::logic::Formula> const& checkTask, storm::expressions::Expression const& targetStateExpression);
+
// The original program that was used to create this model checker.
storm::prism::Program originalProgram;
diff --git a/src/utility/storm.h b/src/utility/storm.h
index 2d0be5461..c74617283 100644
--- a/src/utility/storm.h
+++ b/src/utility/storm.h
@@ -386,12 +386,13 @@ namespace storm {
}
template<storm::dd::DdType DdType, typename ValueType>
- std::unique_ptr<storm::modelchecker::CheckResult> verifyProgramWithAbstractionRefinementEngine(storm::prism::Program const& program, std::shared_ptr<storm::logic::Formula> const& formula) {
+ std::unique_ptr<storm::modelchecker::CheckResult> verifyProgramWithAbstractionRefinementEngine(storm::prism::Program const& program, std::shared_ptr<const storm::logic::Formula> const& formula, bool onlyInitialStatesRelevant = false) {
STORM_LOG_THROW(program.getModelType() == storm::prism::Program::ModelType::MDP, storm::exceptions::InvalidSettingsException, "Cannot treat non-MDP model using the abstraction refinement engine.");
// FIXME: Cudd -> ValueType, double -> ValueType
storm::modelchecker::GameBasedMdpModelChecker<storm::dd::DdType::CUDD, double> modelchecker(program);
- return modelchecker.check(*formula);
+ storm::modelchecker::CheckTask<storm::logic::Formula> task(*formula, onlyInitialStatesRelevant);
+ return modelchecker.check(task);
}
template<typename ValueType>