sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

made everything compile again after latest changes (CheckTasks) 

Former-commit-id: 57fce885f6
tempestpy_adaptions
dehnert 9 years ago
parent
11489a53f3
commit
c83db93c55
4 changed files with 34 additions and 13 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 2
      src/cli/entrypoints.h
  2. 30
      src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
  3. 10
      src/modelchecker/abstraction/GameBasedMdpModelChecker.h
  4. 5
      src/utility/storm.h

2
src/cli/entrypoints.h
View File

@ -48,7 +48,7 @@ namespace storm {
#endif #endif
template<typename ValueType, storm::dd::DdType DdType> 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) { for (auto const& formula : formulas) {
std::cout << std::endl << "Model checking property: " << *formula << " ..."; std::cout << std::endl << "Model checking property: " << *formula << " ...";
std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifyProgramWithAbstractionRefinementEngine<DdType, ValueType>(program, formula, onlyInitialStatesRelevant)); std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifyProgramWithAbstractionRefinementEngine<DdType, ValueType>(program, formula, onlyInitialStatesRelevant));

30
src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
View File

@ -3,6 +3,7 @@
#include "src/utility/macros.h" #include "src/utility/macros.h"
#include "src/exceptions/NotSupportedException.h" #include "src/exceptions/NotSupportedException.h"
#include "src/exceptions/InvalidPropertyException.h"
#include "src/modelchecker/results/CheckResult.h" #include "src/modelchecker/results/CheckResult.h"
@ -26,10 +27,11 @@ namespace storm {
} }
template<storm::dd::DdType Type, typename ValueType> 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()) { if (formula.isProbabilityOperatorFormula()) {
storm::logic::ProbabilityOperatorFormula const& probabilityOperatorFormula = formula.asProbabilityOperatorFormula(); 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()) { } else if (formula.isUntilFormula() || formula.isEventuallyFormula()) {
if (formula.isUntilFormula()) { if (formula.isUntilFormula()) {
storm::logic::UntilFormula const& untilFormula = formula.asUntilFormula(); storm::logic::UntilFormula const& untilFormula = formula.asUntilFormula();
@ -47,23 +49,39 @@ namespace storm {
} }
template<storm::dd::DdType Type, typename ValueType> 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. // Depending on whether or not there is a bound, we do something slightly different here.
return nullptr; return nullptr;
} }
template<storm::dd::DdType Type, typename ValueType> 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 // TODO
return nullptr; return nullptr;
} }
template<storm::dd::DdType Type, typename ValueType> 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; 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>; template class GameBasedMdpModelChecker<storm::dd::DdType::CUDD, double>;
} }
} }

10
src/modelchecker/abstraction/GameBasedMdpModelChecker.h
View File

@ -25,14 +25,16 @@ namespace storm {
virtual ~GameBasedMdpModelChecker() override; 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: 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. // The original program that was used to create this model checker.
storm::prism::Program originalProgram; storm::prism::Program originalProgram;

5
src/utility/storm.h
View File

@ -386,12 +386,13 @@ namespace storm {
} }
template<storm::dd::DdType DdType, typename ValueType> 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."); 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 // FIXME: Cudd -> ValueType, double -> ValueType
storm::modelchecker::GameBasedMdpModelChecker<storm::dd::DdType::CUDD, double> modelchecker(program); 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> template<typename ValueType>

Write Preview
Loading…
Cancel
Save