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

Fixed check results of hybrid multi objective model checking

tempestpy_adaptions
TimQu 8 years ago
parent
01d3e1f5c7
commit
1f4552c046
11 changed files with 306 additions and 79 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 4
      src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp
  2. 30
      src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp
  3. 63
      src/storm/modelchecker/results/CheckResult.cpp
  4. 35
      src/storm/modelchecker/results/CheckResult.h
  5. 58
      src/storm/modelchecker/results/ExplicitParetoCurveCheckResult.cpp
  6. 39
      src/storm/modelchecker/results/ExplicitParetoCurveCheckResult.h
  7. 30
      src/storm/modelchecker/results/ParetoCurveCheckResult.cpp
  8. 26
      src/storm/modelchecker/results/ParetoCurveCheckResult.h
  9. 57
      src/storm/modelchecker/results/SymbolicParetoCurveCheckResult.cpp
  10. 41
      src/storm/modelchecker/results/SymbolicParetoCurveCheckResult.h
  11. 2
      src/storm/solver/SolverSelectionOptions.cpp

4
src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp
View File

@ -4,7 +4,7 @@
#include "storm/models/sparse/Mdp.h"
#include "storm/models/sparse/MarkovAutomaton.h"
#include "storm/models/sparse/StandardRewardModel.h"
#include "storm/modelchecker/results/ParetoCurveCheckResult.h"
#include "storm/modelchecker/results/ExplicitParetoCurveCheckResult.h"
#include "storm/utility/constants.h"
#include "storm/utility/vector.h"
#include "storm/settings/SettingsManager.h"
@ -43,7 +43,7 @@ namespace storm {
for(auto const& vertex : vertices) {
paretoOptimalPoints.push_back(storm::utility::vector::convertNumericVector<typename SparseModelType::ValueType>(this->transformPointToOriginalModel(vertex)));
}
return std::unique_ptr<CheckResult>(new ParetoCurveCheckResult<typename SparseModelType::ValueType>(this->originalModel.getInitialStates().getNextSetIndex(0),
return std::unique_ptr<CheckResult>(new ExplicitParetoCurveCheckResult<typename SparseModelType::ValueType>(this->originalModel.getInitialStates().getNextSetIndex(0),
std::move(paretoOptimalPoints),
this->transformPolytopeToOriginalModel(this->underApproximation)->template convertNumberRepresentation<typename SparseModelType::ValueType>(),
this->transformPolytopeToOriginalModel(this->overApproximation)->template convertNumberRepresentation<typename SparseModelType::ValueType>()));

30
src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp
View File

@ -5,8 +5,14 @@
#include "storm/models/symbolic/Mdp.h"
#include "storm/models/symbolic/StandardRewardModel.h"
#include "storm/storage/dd/DdManager.h"
#include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h"
#include "storm/modelchecker/results/SymbolicQuantitativeCheckResult.h"
#include "storm/modelchecker/results/SymbolicParetoCurveCheckResult.h"
#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "storm/modelchecker/results/ExplicitParetoCurveCheckResult.h"
#include "storm/logic/FragmentSpecification.h"
@ -21,6 +27,7 @@
#include "storm/exceptions/InvalidStateException.h"
#include "storm/exceptions/InvalidPropertyException.h"
#include "storm/exceptions/UnexpectedException.h"
namespace storm {
namespace modelchecker {
@ -41,7 +48,8 @@ namespace storm {
return true;
} else {
// Check whether we consider a multi-objective formula
// For multi-objective model checking, each state requires an individual scheduler (in contrast to single-objective model checking). Let's exclude that all states are considered.
// For multi-objective model checking, each state requires an individual scheduler (in contrast to single-objective model checking). Let's exclude that multiple states are relevant
if(this->getModel().getInitialStates().getNonZeroCount() > 1) return false;
if(!checkTask.isOnlyInitialStatesRelevantSet()) return false;
return formula.isInFragment(storm::logic::multiObjective().setCumulativeRewardFormulasAllowed(true));
}
@ -118,7 +126,25 @@ namespace storm {
template<typename ModelType>
std::unique_ptr<CheckResult> HybridMdpPrctlModelChecker<ModelType>::checkMultiObjectiveFormula(CheckTask<storm::logic::MultiObjectiveFormula, ValueType> const& checkTask) {
auto sparseModel = storm::transformer::SymbolicMdpToSparseMdpTransformer<DdType, ValueType>::translate(this->getModel());
return multiobjective::performPcaa(*sparseModel, checkTask.getFormula());
std::unique_ptr<CheckResult> explicitResult = multiobjective::performPcaa(*sparseModel, checkTask.getFormula());
// Convert the explicit result
if(explicitResult->isExplicitQualitativeCheckResult()) {
if(explicitResult->asExplicitQualitativeCheckResult()[*sparseModel->getInitialStates().begin()]) {
return std::unique_ptr<CheckResult>(new storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(this->getModel().getReachableStates(), this->getModel().getInitialStates(), this->getModel().getManager().getBddOne()));
} else {
return std::unique_ptr<CheckResult>(new storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(this->getModel().getReachableStates(), this->getModel().getInitialStates(), this->getModel().getManager().getBddZero()));
}
} else if(explicitResult->isExplicitQuantitativeCheckResult()) {
ValueType const& res = explicitResult->template asExplicitQuantitativeCheckResult<ValueType>()[*sparseModel->getInitialStates().begin()];
return std::unique_ptr<CheckResult>(new storm::modelchecker::SymbolicQuantitativeCheckResult<DdType, ValueType>(this->getModel().getReachableStates(), this->getModel().getInitialStates(), this->getModel().getManager().template getConstant<ValueType>(res)));
} else if(explicitResult->isExplicitParetoCurveCheckResult()) {
ExplicitParetoCurveCheckResult<ValueType> const& paretoResult = explicitResult->template asExplicitParetoCurveCheckResult<ValueType>();
return std::unique_ptr<CheckResult>(new storm::modelchecker::SymbolicParetoCurveCheckResult<DdType, ValueType>(this->getModel().getInitialStates(), paretoResult.getPoints(), paretoResult.getUnderApproximation(), paretoResult.getOverApproximation()));
} else {
STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "The obtained checkresult has an unexpected type.");
return nullptr;
}
}
template class HybridMdpPrctlModelChecker<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD, double>>;

63
src/storm/modelchecker/results/CheckResult.cpp
View File

@ -5,10 +5,11 @@
#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "storm/modelchecker/results/ExplicitParetoCurveCheckResult.h"
#include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h"
#include "storm/modelchecker/results/SymbolicQuantitativeCheckResult.h"
#include "storm/modelchecker/results/SymbolicParetoCurveCheckResult.h"
#include "storm/modelchecker/results/HybridQuantitativeCheckResult.h"
#include "storm/modelchecker/results/ParetoCurveCheckResult.h"
#include "storm/utility/macros.h"
#include "storm/exceptions/InvalidOperationException.h"
@ -34,7 +35,11 @@ namespace storm {
bool CheckResult::isQualitative() const {
return false;
}
bool CheckResult::isParetoCurveCheckResult() const {
return false;
}
bool CheckResult::isResultForAllStates() const {
return false;
}
@ -51,7 +56,11 @@ namespace storm {
bool CheckResult::isExplicitQuantitativeCheckResult() const {
return false;
}
bool CheckResult::isExplicitParetoCurveCheckResult() const {
return false;
}
bool CheckResult::isSymbolicQualitativeCheckResult() const {
return false;
}
@ -59,12 +68,12 @@ namespace storm {
bool CheckResult::isSymbolicQuantitativeCheckResult() const {
return false;
}
bool CheckResult::isHybridQuantitativeCheckResult() const {
bool CheckResult::isSymbolicParetoCurveCheckResult() const {
return false;
}
bool CheckResult::isParetoCurveCheckResult() const {
bool CheckResult::isHybridQuantitativeCheckResult() const {
return false;
}
@ -85,6 +94,16 @@ namespace storm {
ExplicitQuantitativeCheckResult<ValueType> const& CheckResult::asExplicitQuantitativeCheckResult() const {
return dynamic_cast<ExplicitQuantitativeCheckResult<ValueType> const&>(*this);
}
template<typename ValueType>
ExplicitParetoCurveCheckResult<ValueType>& CheckResult::asExplicitParetoCurveCheckResult() {
return dynamic_cast<ExplicitParetoCurveCheckResult<ValueType>&>(*this);
}
template<typename ValueType>
ExplicitParetoCurveCheckResult<ValueType> const& CheckResult::asExplicitParetoCurveCheckResult() const {
return dynamic_cast<ExplicitParetoCurveCheckResult<ValueType> const&>(*this);
}
QualitativeCheckResult& CheckResult::asQualitativeCheckResult() {
return dynamic_cast<QualitativeCheckResult&>(*this);
@ -124,25 +143,29 @@ namespace storm {
HybridQuantitativeCheckResult<Type, ValueType> const& CheckResult::asHybridQuantitativeCheckResult() const {
return dynamic_cast<HybridQuantitativeCheckResult<Type, ValueType> const&>(*this);
}
template<typename ValueType>
ParetoCurveCheckResult<ValueType>& CheckResult::asParetoCurveCheckResult() {
return dynamic_cast<ParetoCurveCheckResult<ValueType>&>(*this);
template <storm::dd::DdType Type, typename ValueType>
SymbolicParetoCurveCheckResult<Type, ValueType>& CheckResult::asSymbolicParetoCurveCheckResult() {
return dynamic_cast<SymbolicParetoCurveCheckResult<Type, ValueType>&>(*this);
}
template<typename ValueType>
ParetoCurveCheckResult<ValueType> const& CheckResult::asParetoCurveCheckResult() const {
return dynamic_cast<ParetoCurveCheckResult<ValueType> const&>(*this);
template <storm::dd::DdType Type, typename ValueType>
SymbolicParetoCurveCheckResult<Type, ValueType> const& CheckResult::asSymbolicParetoCurveCheckResult() const {
return dynamic_cast<SymbolicParetoCurveCheckResult<Type, ValueType> const&>(*this);
}
// Explicitly instantiate the template functions.
template ExplicitQuantitativeCheckResult<double>& CheckResult::asExplicitQuantitativeCheckResult();
template ExplicitQuantitativeCheckResult<double> const& CheckResult::asExplicitQuantitativeCheckResult() const;
template ExplicitParetoCurveCheckResult<double>& CheckResult::asExplicitParetoCurveCheckResult();
template ExplicitParetoCurveCheckResult<double> const& CheckResult::asExplicitParetoCurveCheckResult() const;
template SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>& CheckResult::asSymbolicQualitativeCheckResult();
template SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD> const& CheckResult::asSymbolicQualitativeCheckResult() const;
template SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD, double>& CheckResult::asSymbolicQuantitativeCheckResult();
template SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD, double> const& CheckResult::asSymbolicQuantitativeCheckResult() const;
template SymbolicParetoCurveCheckResult<storm::dd::DdType::CUDD, double>& CheckResult::asSymbolicParetoCurveCheckResult();
template SymbolicParetoCurveCheckResult<storm::dd::DdType::CUDD, double> const& CheckResult::asSymbolicParetoCurveCheckResult() const;
template HybridQuantitativeCheckResult<storm::dd::DdType::CUDD, double>& CheckResult::asHybridQuantitativeCheckResult();
template HybridQuantitativeCheckResult<storm::dd::DdType::CUDD, double> const& CheckResult::asHybridQuantitativeCheckResult() const;
@ -150,11 +173,11 @@ namespace storm {
template SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan> const& CheckResult::asSymbolicQualitativeCheckResult() const;
template SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>& CheckResult::asSymbolicQuantitativeCheckResult();
template SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double> const& CheckResult::asSymbolicQuantitativeCheckResult() const;
template SymbolicParetoCurveCheckResult<storm::dd::DdType::Sylvan, double>& CheckResult::asSymbolicParetoCurveCheckResult();
template SymbolicParetoCurveCheckResult<storm::dd::DdType::Sylvan, double> const& CheckResult::asSymbolicParetoCurveCheckResult() const;
template HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>& CheckResult::asHybridQuantitativeCheckResult();
template HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan, double> const& CheckResult::asHybridQuantitativeCheckResult() const;
template ParetoCurveCheckResult<double>& CheckResult::asParetoCurveCheckResult();
template ParetoCurveCheckResult<double> const& CheckResult::asParetoCurveCheckResult() const;
#ifdef STORM_HAVE_CARL
template ExplicitQuantitativeCheckResult<storm::RationalNumber>& CheckResult::asExplicitQuantitativeCheckResult();
@ -163,8 +186,8 @@ namespace storm {
template ExplicitQuantitativeCheckResult<storm::RationalFunction>& CheckResult::asExplicitQuantitativeCheckResult();
template ExplicitQuantitativeCheckResult<storm::RationalFunction> const& CheckResult::asExplicitQuantitativeCheckResult() const;
template ParetoCurveCheckResult<storm::RationalNumber>& CheckResult::asParetoCurveCheckResult();
template ParetoCurveCheckResult<storm::RationalNumber> const& CheckResult::asParetoCurveCheckResult() const;
template ExplicitParetoCurveCheckResult<storm::RationalNumber>& CheckResult::asExplicitParetoCurveCheckResult();
template ExplicitParetoCurveCheckResult<storm::RationalNumber> const& CheckResult::asExplicitParetoCurveCheckResult() const;
#endif
}
}

35
src/storm/modelchecker/results/CheckResult.h
View File

@ -18,18 +18,21 @@ namespace storm {
template <typename ValueType>
class ExplicitQuantitativeCheckResult;
template <typename ValueType>
class ExplicitParetoCurveCheckResult;
template <storm::dd::DdType Type>
class SymbolicQualitativeCheckResult;
template <storm::dd::DdType Type, typename ValueType>
class SymbolicQuantitativeCheckResult;
template <storm::dd::DdType Type, typename ValueType>
class HybridQuantitativeCheckResult;
template <typename ValueType>
class ParetoCurveCheckResult;
template <storm::dd::DdType Type, typename ValueType>
class SymbolicParetoCurveCheckResult;
// The base class of all check results.
class CheckResult {
public:
@ -49,12 +52,14 @@ namespace storm {
virtual bool isHybrid() const;
virtual bool isQuantitative() const;
virtual bool isQualitative() const;
virtual bool isParetoCurveCheckResult() const;
virtual bool isExplicitQualitativeCheckResult() const;
virtual bool isExplicitQuantitativeCheckResult() const;
virtual bool isExplicitParetoCurveCheckResult() const;
virtual bool isSymbolicQualitativeCheckResult() const;
virtual bool isSymbolicQuantitativeCheckResult() const;
virtual bool isSymbolicParetoCurveCheckResult() const;
virtual bool isHybridQuantitativeCheckResult() const;
virtual bool isParetoCurveCheckResult() const;
virtual bool isResultForAllStates() const;
QualitativeCheckResult& asQualitativeCheckResult();
@ -78,6 +83,12 @@ namespace storm {
template<typename ValueType>
ExplicitQuantitativeCheckResult<ValueType> const& asExplicitQuantitativeCheckResult() const;
template <typename ValueType>
ExplicitParetoCurveCheckResult<ValueType>& asExplicitParetoCurveCheckResult();
template <typename ValueType>
ExplicitParetoCurveCheckResult<ValueType> const& asExplicitParetoCurveCheckResult() const;
template <storm::dd::DdType Type>
SymbolicQualitativeCheckResult<Type>& asSymbolicQualitativeCheckResult();
@ -97,11 +108,11 @@ namespace storm {
template <storm::dd::DdType Type, typename ValueType>
HybridQuantitativeCheckResult<Type, ValueType> const& asHybridQuantitativeCheckResult() const;
template <typename ValueType>
ParetoCurveCheckResult<ValueType>& asParetoCurveCheckResult();
template <typename ValueType>
ParetoCurveCheckResult<ValueType> const& asParetoCurveCheckResult() const;
template <storm::dd::DdType Type, typename ValueType>
SymbolicParetoCurveCheckResult<Type, ValueType>& asSymbolicParetoCurveCheckResult();
template <storm::dd::DdType Type, typename ValueType>
SymbolicParetoCurveCheckResult<Type, ValueType> const& asSymbolicParetoCurveCheckResult() const;
virtual std::ostream& writeToStream(std::ostream& out) const = 0;
};

58
src/storm/modelchecker/results/ExplicitParetoCurveCheckResult.cpp
View File

@ -0,0 +1,58 @@
#include "storm/modelchecker/results/ExplicitParetoCurveCheckResult.h"
#include "storm/adapters/CarlAdapter.h"
#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
#include "storm/utility/macros.h"
#include "storm/utility/vector.h"
#include "storm/exceptions/InvalidOperationException.h"
namespace storm {
namespace modelchecker {
template<typename ValueType>
ExplicitParetoCurveCheckResult<ValueType>::ExplicitParetoCurveCheckResult() {
// Intentionally left empty.
}
template<typename ValueType>
ExplicitParetoCurveCheckResult<ValueType>::ExplicitParetoCurveCheckResult(storm::storage::sparse::state_type const& state, std::vector<typename ParetoCurveCheckResult<ValueType>::point_type> const& points, typename ParetoCurveCheckResult<ValueType>::polytope_type const& underApproximation, typename ParetoCurveCheckResult<ValueType>::polytope_type const& overApproximation) : ParetoCurveCheckResult<ValueType>(points, underApproximation, overApproximation), state(state) {
// Intentionally left empty.
}
template<typename ValueType>
ExplicitParetoCurveCheckResult<ValueType>::ExplicitParetoCurveCheckResult(storm::storage::sparse::state_type const& state, std::vector<typename ParetoCurveCheckResult<ValueType>::point_type>&& points, typename ParetoCurveCheckResult<ValueType>::polytope_type&& underApproximation, typename ParetoCurveCheckResult<ValueType>::polytope_type&& overApproximation) : ParetoCurveCheckResult<ValueType>(points, underApproximation, overApproximation), state(state) {
// Intentionally left empty.
}
template<typename ValueType>
bool ExplicitParetoCurveCheckResult<ValueType>::isExplicitParetoCurveCheckResult() const {
return true;
}
template<typename ValueType>
bool ExplicitParetoCurveCheckResult<ValueType>::isExplicit() const {
return true;
}
template<typename ValueType>
void ExplicitParetoCurveCheckResult<ValueType>::filter(QualitativeCheckResult const& filter) {
STORM_LOG_THROW(filter.isExplicitQualitativeCheckResult(), storm::exceptions::InvalidOperationException, "Cannot filter explicit check result with non-explicit filter.");
STORM_LOG_THROW(filter.isResultForAllStates(), storm::exceptions::InvalidOperationException, "Cannot filter check result with non-complete filter.");
ExplicitQualitativeCheckResult const& explicitFilter = filter.asExplicitQualitativeCheckResult();
ExplicitQualitativeCheckResult::vector_type const& filterTruthValues = explicitFilter.getTruthValuesVector();
STORM_LOG_THROW(filterTruthValues.getNumberOfSetBits() == 1 && filterTruthValues.get(state), storm::exceptions::InvalidOperationException, "The check result fails to contain some results referred to by the filter.");
}
template<typename ValueType>
storm::storage::sparse::state_type const& ExplicitParetoCurveCheckResult<ValueType>:: getState() const {
return state;
}
template class ExplicitParetoCurveCheckResult<double>;
#ifdef STORM_HAVE_CARL
template class ExplicitParetoCurveCheckResult<storm::RationalNumber>;
#endif
}
}

39
src/storm/modelchecker/results/ExplicitParetoCurveCheckResult.h
View File

@ -0,0 +1,39 @@
#ifndef STORM_MODELCHECKER_EXPLICITPARETOCURVECHECKRESULT_H_
#define STORM_MODELCHECKER_EXPLICITPARETOCURVECHECKRESULT_H_
#include <vector>
#include "storm/modelchecker/results/ParetoCurveCheckResult.h"
#include "storm/storage/sparse/StateType.h"
namespace storm {
namespace modelchecker {
template<typename ValueType>
class ExplicitParetoCurveCheckResult : public ParetoCurveCheckResult<ValueType> {
public:
ExplicitParetoCurveCheckResult();
ExplicitParetoCurveCheckResult(storm::storage::sparse::state_type const& state, std::vector<typename ParetoCurveCheckResult<ValueType>::point_type> const& points, typename ParetoCurveCheckResult<ValueType>::polytope_type const& underApproximation, typename ParetoCurveCheckResult<ValueType>::polytope_type const& overApproximation);
ExplicitParetoCurveCheckResult(storm::storage::sparse::state_type const& state, std::vector<typename ParetoCurveCheckResult<ValueType>::point_type>&& points, typename ParetoCurveCheckResult<ValueType>::polytope_type&& underApproximation, typename ParetoCurveCheckResult<ValueType>::polytope_type&& overApproximation);
ExplicitParetoCurveCheckResult(ExplicitParetoCurveCheckResult const& other) = default;
ExplicitParetoCurveCheckResult& operator=(ExplicitParetoCurveCheckResult const& other) = default;
ExplicitParetoCurveCheckResult(ExplicitParetoCurveCheckResult&& other) = default;
ExplicitParetoCurveCheckResult& operator=(ExplicitParetoCurveCheckResult&& other) = default;
virtual ~ExplicitParetoCurveCheckResult() = default;
virtual bool isExplicitParetoCurveCheckResult() const override;
virtual bool isExplicit() const override;
virtual void filter(QualitativeCheckResult const& filter) override;
storm::storage::sparse::state_type const& getState() const;
private:
// The state of the checked model to which the result applies
storm::storage::sparse::state_type state;
};
}
}
#endif /* STORM_MODELCHECKER_EXPLICITPARETOCURVECHECKRESULT_H_ */

30
src/storm/modelchecker/results/ParetoCurveCheckResult.cpp
View File

@ -1,49 +1,31 @@
#include "storm/modelchecker/results/ParetoCurveCheckResult.h"
#include "storm/adapters/CarlAdapter.h"
#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
#include "storm/utility/macros.h"
#include "storm/utility/vector.h"
#include "storm/exceptions/InvalidOperationException.h"
namespace storm {
namespace modelchecker {
template<typename ValueType>
ParetoCurveCheckResult<ValueType>::ParetoCurveCheckResult() {
// Intentionally left empty.
}
template<typename ValueType>
ParetoCurveCheckResult<ValueType>::ParetoCurveCheckResult(storm::storage::sparse::state_type const& state, std::vector<point_type> const& points, polytope_type const& underApproximation, polytope_type const& overApproximation) : state(state), points(points), underApproximation(underApproximation), overApproximation(overApproximation) {
ParetoCurveCheckResult<ValueType>::ParetoCurveCheckResult(std::vector<point_type> const& points, polytope_type const& underApproximation, polytope_type const& overApproximation) : points(points), underApproximation(underApproximation), overApproximation(overApproximation) {
// Intentionally left empty.
}
template<typename ValueType>
ParetoCurveCheckResult<ValueType>::ParetoCurveCheckResult(storm::storage::sparse::state_type const& state, std::vector<point_type>&& points, polytope_type&& underApproximation, polytope_type&& overApproximation) : state(state), points(points), underApproximation(underApproximation), overApproximation(overApproximation) {
ParetoCurveCheckResult<ValueType>::ParetoCurveCheckResult(std::vector<point_type>&& points, polytope_type&& underApproximation, polytope_type&& overApproximation) : points(points), underApproximation(underApproximation), overApproximation(overApproximation) {
// Intentionally left empty.
}
template<typename ValueType>
bool ParetoCurveCheckResult<ValueType>::isParetoCurveCheckResult() const {
return true;
}
template<typename ValueType>
void ParetoCurveCheckResult<ValueType>::filter(QualitativeCheckResult const& filter) {
STORM_LOG_THROW(filter.isExplicitQualitativeCheckResult(), storm::exceptions::InvalidOperationException, "Cannot filter explicit check result with non-explicit filter.");
STORM_LOG_THROW(filter.isResultForAllStates(), storm::exceptions::InvalidOperationException, "Cannot filter check result with non-complete filter.");
ExplicitQualitativeCheckResult const& explicitFilter = filter.asExplicitQualitativeCheckResult();
ExplicitQualitativeCheckResult::vector_type const& filterTruthValues = explicitFilter.getTruthValuesVector();
STORM_LOG_THROW(filterTruthValues.getNumberOfSetBits() == 1 && filterTruthValues.get(state), storm::exceptions::InvalidOperationException, "The check result fails to contain some results referred to by the filter.");
}
template<typename ValueType>
storm::storage::sparse::state_type const& ParetoCurveCheckResult<ValueType>:: getState() const {
return state;
}
template<typename ValueType>
std::vector<typename ParetoCurveCheckResult<ValueType>::point_type> const& ParetoCurveCheckResult<ValueType>::getPoints() const {
return points;

26
src/storm/modelchecker/results/ParetoCurveCheckResult.h
View File

@ -4,8 +4,6 @@
#include <vector>
#include "storm/modelchecker/results/CheckResult.h"
#include "storm/utility/OsDetection.h"
#include "storm/storage/sparse/StateType.h"
#include "storm/storage/geometry/Polytope.h"
namespace storm {
@ -15,32 +13,22 @@ namespace storm {
public:
typedef std::vector<ValueType> point_type;
typedef std::shared_ptr<storm::storage::geometry::Polytope<ValueType>> polytope_type;
ParetoCurveCheckResult();
ParetoCurveCheckResult(storm::storage::sparse::state_type const& state, std::vector<point_type> const& points, polytope_type const& underApproximation, polytope_type const& overApproximation);
ParetoCurveCheckResult(storm::storage::sparse::state_type const& state, std::vector<point_type>&& points, polytope_type&& underApproximation, polytope_type&& overApproximation);
ParetoCurveCheckResult(ParetoCurveCheckResult const& other) = default;
ParetoCurveCheckResult& operator=(ParetoCurveCheckResult const& other) = default;
ParetoCurveCheckResult(ParetoCurveCheckResult&& other) = default;
ParetoCurveCheckResult& operator=(ParetoCurveCheckResult&& other) = default;
virtual ~ParetoCurveCheckResult() = default;
virtual bool isParetoCurveCheckResult() const override;
virtual void filter(QualitativeCheckResult const& filter) override;
storm::storage::sparse::state_type const& getState() const;
std::vector<point_type> const& getPoints() const;
polytope_type const& getUnderApproximation() const;
polytope_type const& getOverApproximation() const;
virtual std::ostream& writeToStream(std::ostream& out) const override;
private:
// The state of the checked model to which the result applies
storm::storage::sparse::state_type state;
protected:
ParetoCurveCheckResult(std::vector<point_type> const& points, polytope_type const& underApproximation, polytope_type const& overApproximation);
ParetoCurveCheckResult(std::vector<point_type>&& points, polytope_type&& underApproximation, polytope_type&& overApproximation);
// The pareto optimal points that have been found.
std::vector<point_type> points;

57
src/storm/modelchecker/results/SymbolicParetoCurveCheckResult.cpp
View File

@ -0,0 +1,57 @@
#include "storm/modelchecker/results/SymbolicParetoCurveCheckResult.h"
#include "storm/adapters/CarlAdapter.h"
#include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h"
#include "storm/utility/macros.h"
#include "storm/storage/dd/DdManager.h"
#include "storm/exceptions/InvalidOperationException.h"
namespace storm {
namespace modelchecker {
template<storm::dd::DdType Type, typename ValueType>
SymbolicParetoCurveCheckResult<Type, ValueType>::SymbolicParetoCurveCheckResult() {
// Intentionally left empty.
}
template<storm::dd::DdType Type, typename ValueType>
SymbolicParetoCurveCheckResult<Type, ValueType>::SymbolicParetoCurveCheckResult(storm::dd::Bdd<Type> const& state, std::vector<typename ParetoCurveCheckResult<ValueType>::point_type> const& points, typename ParetoCurveCheckResult<ValueType>::polytope_type const& underApproximation, typename ParetoCurveCheckResult<ValueType>::polytope_type const& overApproximation) : ParetoCurveCheckResult<ValueType>(points, underApproximation, overApproximation), state(state) {
STORM_LOG_THROW(this->state.getNonZeroCount() == 1, storm::exceptions::InvalidOperationException, "ParetoCheckResults are only relevant for a single state.");
}
template<storm::dd::DdType Type, typename ValueType>
SymbolicParetoCurveCheckResult<Type, ValueType>::SymbolicParetoCurveCheckResult(storm::dd::Bdd<Type> const& state, std::vector<typename ParetoCurveCheckResult<ValueType>::point_type>&& points, typename ParetoCurveCheckResult<ValueType>::polytope_type&& underApproximation, typename ParetoCurveCheckResult<ValueType>::polytope_type&& overApproximation) : ParetoCurveCheckResult<ValueType>(points, underApproximation, overApproximation), state(state) {
STORM_LOG_THROW(this->state.getNonZeroCount() == 1, storm::exceptions::InvalidOperationException, "ParetoCheckResults are only relevant for a single state.");
}
template<storm::dd::DdType Type, typename ValueType>
bool SymbolicParetoCurveCheckResult<Type, ValueType>::isSymbolicParetoCurveCheckResult() const {
return true;
}
template<storm::dd::DdType Type, typename ValueType>
bool SymbolicParetoCurveCheckResult<Type, ValueType>::isSymbolic() const {
return true;
}
template<storm::dd::DdType Type, typename ValueType>
void SymbolicParetoCurveCheckResult<Type, ValueType>::filter(QualitativeCheckResult const& filter) {
STORM_LOG_THROW(filter.isSymbolicQualitativeCheckResult(), storm::exceptions::InvalidOperationException, "Cannot filter Symbolic check result with non-Symbolic filter.");
STORM_LOG_THROW(filter.isResultForAllStates(), storm::exceptions::InvalidOperationException, "Cannot filter check result with non-complete filter.");
SymbolicQualitativeCheckResult<Type> const& symbolicFilter = filter.template asSymbolicQualitativeCheckResult<Type>();
storm::dd::Bdd<Type> const& filterTruthValues = symbolicFilter.getTruthValuesVector();
STORM_LOG_THROW(filterTruthValues.getNonZeroCount() == 1 && !(filterTruthValues && state).isZero(), storm::exceptions::InvalidOperationException, "The check result fails to contain some results referred to by the filter.");
}
template<storm::dd::DdType Type, typename ValueType>
storm::dd::Bdd<Type> const& SymbolicParetoCurveCheckResult<Type, ValueType>::getState() const {
return state;
}
template class SymbolicParetoCurveCheckResult<storm::dd::DdType::CUDD, double>;
template class SymbolicParetoCurveCheckResult<storm::dd::DdType::Sylvan, double>;
}
}

41
src/storm/modelchecker/results/SymbolicParetoCurveCheckResult.h
View File

@ -0,0 +1,41 @@
#ifndef STORM_MODELCHECKER_SYMBOLICPARETOCURVECHECKRESULT_H_
#define STORM_MODELCHECKER_SYMBOLICPARETOCURVECHECKRESULT_H_
#include <vector>
#include "storm/modelchecker/results/ParetoCurveCheckResult.h"
#include "storm/storage/dd/DdType.h"
#include "storm/storage/dd/Bdd.h"
namespace storm {
namespace modelchecker {
template<storm::dd::DdType Type, typename ValueType = double>
class SymbolicParetoCurveCheckResult : public ParetoCurveCheckResult<ValueType> {
public:
SymbolicParetoCurveCheckResult();
SymbolicParetoCurveCheckResult(storm::dd::Bdd<Type> const& state, std::vector<typename ParetoCurveCheckResult<ValueType>::point_type> const& points, typename ParetoCurveCheckResult<ValueType>::polytope_type const& underApproximation, typename ParetoCurveCheckResult<ValueType>::polytope_type const& overApproximation);
SymbolicParetoCurveCheckResult(storm::dd::Bdd<Type> const& state, std::vector<typename ParetoCurveCheckResult<ValueType>::point_type>&& points, typename ParetoCurveCheckResult<ValueType>::polytope_type&& underApproximation, typename ParetoCurveCheckResult<ValueType>::polytope_type&& overApproximation);
SymbolicParetoCurveCheckResult(SymbolicParetoCurveCheckResult const& other) = default;
SymbolicParetoCurveCheckResult& operator=(SymbolicParetoCurveCheckResult const& other) = default;
SymbolicParetoCurveCheckResult(SymbolicParetoCurveCheckResult&& other) = default;
SymbolicParetoCurveCheckResult& operator=(SymbolicParetoCurveCheckResult&& other) = default;
virtual ~SymbolicParetoCurveCheckResult() = default;
virtual bool isSymbolicParetoCurveCheckResult() const override;
virtual bool isSymbolic() const override;
virtual void filter(QualitativeCheckResult const& filter) override;
storm::dd::Bdd<Type> const& getState() const;
private:
// The state of the checked model to which the result applies
storm::dd::Bdd<Type> state;
};
}
}
#endif /* STORM_MODELCHECKER_SYMBOLICPARETOCURVECHECKRESULT_H_ */

2
src/storm/solver/SolverSelectionOptions.cpp
View File

@ -21,6 +21,8 @@ namespace storm {
return "Gurobi";
case LpSolverType::Glpk:
return "Glpk";
case LpSolverType::Z3:
return "Z3";
}
return "invalid";
}

Write Preview
Loading…
Cancel
Save