TimQu
9 years ago
17 changed files with 667 additions and 106 deletions
-
22src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.cpp
-
199src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.cpp
-
9src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.h
-
9src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorData.h
-
21src/modelchecker/results/CheckResult.cpp
-
10src/modelchecker/results/CheckResult.h
-
88src/modelchecker/results/ParetoCurveCheckResult.cpp
-
56src/modelchecker/results/ParetoCurveCheckResult.h
-
20src/settings/ArgumentValidators.h
-
39src/settings/modules/MultiObjectiveSettings.cpp
-
44src/settings/modules/MultiObjectiveSettings.h
-
23src/storage/geometry/Hyperrectangle.h
-
2src/storage/geometry/HyproPolytope.cpp
-
106src/storage/geometry/Polytope.cpp
-
14src/storage/geometry/Polytope.h
-
4src/utility/Stopwatch.h
-
43src/utility/export.h
@ -0,0 +1,88 @@ |
|||||
|
#include "src/modelchecker/results/ParetoCurveCheckResult.h"
|
||||
|
|
||||
|
#include "src/adapters/CarlAdapter.h"
|
||||
|
#include "src/modelchecker/results/ExplicitQualitativeCheckResult.h"
|
||||
|
#include "src/utility/macros.h"
|
||||
|
#include "src/utility/vector.h"
|
||||
|
|
||||
|
#include "src/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) { |
||||
|
// 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) { |
||||
|
// 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; |
||||
|
} |
||||
|
|
||||
|
template<typename ValueType> |
||||
|
typename ParetoCurveCheckResult<ValueType>::polytope_type const& ParetoCurveCheckResult<ValueType>::getUnderApproximation() const { |
||||
|
return underApproximation; |
||||
|
} |
||||
|
|
||||
|
template<typename ValueType> |
||||
|
typename ParetoCurveCheckResult<ValueType>::polytope_type const& ParetoCurveCheckResult<ValueType>::getOverApproximation() const { |
||||
|
return overApproximation; |
||||
|
} |
||||
|
|
||||
|
|
||||
|
template<typename ValueType> |
||||
|
std::ostream& ParetoCurveCheckResult<ValueType>::writeToStream(std::ostream& out) const { |
||||
|
out << std::endl; |
||||
|
out << "Underapproximation of achievable values: " << underApproximation->toString() << std::endl; |
||||
|
out << "Overapproximation of achievable values: " << overApproximation->toString() << std::endl; |
||||
|
out << points.size() << " pareto optimal points found:" << std::endl; |
||||
|
for(auto const& p : points) { |
||||
|
out << " ("; |
||||
|
for(auto it = p.begin(); it != p.end(); ++it){ |
||||
|
if(it != p.begin()){ |
||||
|
out << ", "; |
||||
|
} |
||||
|
out << std::setw(10) << *it; |
||||
|
} |
||||
|
out << " )" << std::endl; |
||||
|
} |
||||
|
return out; |
||||
|
} |
||||
|
|
||||
|
template class ParetoCurveCheckResult<double>; |
||||
|
|
||||
|
#ifdef STORM_HAVE_CARL
|
||||
|
template class ParetoCurveCheckResult<storm::RationalNumber>; |
||||
|
#endif
|
||||
|
} |
||||
|
} |
||||
@ -0,0 +1,56 @@ |
|||||
|
#ifndef STORM_MODELCHECKER_PARETOCURVECHECKRESULT_H_ |
||||
|
#define STORM_MODELCHECKER_PARETOCURVECHECKRESULT_H_ |
||||
|
|
||||
|
#include <vector> |
||||
|
|
||||
|
#include "src/modelchecker/results/CheckResult.h" |
||||
|
#include "src/utility/OsDetection.h" |
||||
|
#include "src/storage/sparse/StateType.h" |
||||
|
#include "src/storage/geometry/Polytope.h" |
||||
|
|
||||
|
namespace storm { |
||||
|
namespace modelchecker { |
||||
|
template<typename ValueType> |
||||
|
class ParetoCurveCheckResult : public CheckResult { |
||||
|
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; |
||||
|
|
||||
|
// The pareto optimal points that have been found. |
||||
|
std::vector<point_type> points; |
||||
|
|
||||
|
// An underapproximation of the set of achievable values |
||||
|
polytope_type underApproximation; |
||||
|
|
||||
|
// An overapproximation of the set of achievable values |
||||
|
polytope_type overApproximation; |
||||
|
}; |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
#endif /* STORM_MODELCHECKER_PARETOCURVECHECKRESULT_H_ */ |
||||
Write
Preview
Loading…
Cancel
Save
Reference in new issue