Browse Source
introduced post processor plus a little renaiming of things
introduced post processor plus a little renaiming of things
Former-commit-id: f73f8eb2ff
main
TimQu
9 years ago
13 changed files with 400 additions and 256 deletions
-
17src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.cpp
-
173src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.cpp
-
32src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.h
-
63src/modelchecker/multiobjective/helper/SparseMultiObjectiveObjectiveInformation.h
-
57src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.cpp
-
48src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.h
-
39src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp
-
24src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.h
-
62src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorData.h
-
105src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorReturnType.h
-
16src/modelchecker/multiobjective/helper/SparseMultiObjectiveRefinementStep.h
-
16src/modelchecker/multiobjective/helper/SparseMultiObjectiveResultData.h
-
4src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.h
@ -0,0 +1,63 @@ |
|||
#ifndef STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEOBJECTIVEINFORMATION_H_ |
|||
#define STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEOBJECTIVEINFORMATION_H_ |
|||
|
|||
#include <iomanip> |
|||
#include <boost/optional.hpp> |
|||
|
|||
#include "src/logic/Formulas.h" |
|||
|
|||
namespace storm { |
|||
namespace modelchecker { |
|||
namespace helper { |
|||
template <typename ValueType> |
|||
struct SparseMultiObjectiveObjectiveInformation { |
|||
// the original input formula |
|||
std::shared_ptr<storm::logic::Formula const> originalFormula; |
|||
|
|||
// the name of the considered reward model in the preprocessedModel |
|||
std::string rewardModelName; |
|||
|
|||
// true if all rewards for this objective are positive, false if all rewards are negative. |
|||
bool rewardsArePositive; |
|||
|
|||
// transformation from the values of the preprocessed model to the ones for the actual input model, i.e., |
|||
// x is achievable in the preprocessed model iff factor*x + offset is achievable in the original model |
|||
ValueType toOriginalValueTransformationFactor; |
|||
ValueType toOriginalValueTransformationOffset; |
|||
|
|||
// The probability/reward threshold for the preprocessed model (if originalFormula specifies one). |
|||
// This is always a lower bound. |
|||
boost::optional<ValueType> threshold; |
|||
// True iff the specified threshold is strict, i.e., > |
|||
bool thresholdIsStrict = false; |
|||
|
|||
// The (discrete) stepBound for the formula (if given by the originalFormula) |
|||
boost::optional<uint_fast64_t> stepBound; |
|||
|
|||
void printToStream(std::ostream& out) const { |
|||
out << std::setw(30) << originalFormula->toString(); |
|||
out << " \t(toOrigVal:" << std::setw(3) << toOriginalValueTransformationFactor << "*x +" << std::setw(3) << toOriginalValueTransformationOffset << ", \t"; |
|||
out << "intern threshold:"; |
|||
if(threshold){ |
|||
out << (thresholdIsStrict ? " >" : ">="); |
|||
out << std::setw(5) << (*threshold) << ","; |
|||
} else { |
|||
out << " none,"; |
|||
} |
|||
out << " \t"; |
|||
out << "intern reward model: " << std::setw(10) << rewardModelName; |
|||
out << (rewardsArePositive ? " (positive)" : " (negative)") << ", \t"; |
|||
out << "step bound:"; |
|||
if(stepBound) { |
|||
out << std::setw(5) << (*stepBound); |
|||
} else { |
|||
out << " none"; |
|||
} |
|||
out << ")" << std::endl; |
|||
} |
|||
}; |
|||
} |
|||
} |
|||
} |
|||
|
|||
#endif /* STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEOBJECTIVEINFORMATION_H_ */ |
|||
@ -0,0 +1,57 @@ |
|||
#include "src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.h"
|
|||
|
|||
#include "src/adapters/CarlAdapter.h"
|
|||
#include "src/models/sparse/Mdp.h"
|
|||
#include "src/models/sparse/StandardRewardModel.h"
|
|||
#include "src/modelchecker/results/ExplicitQualitativeCheckResult.h"
|
|||
#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
|
|||
#include "src/storage/geometry/Polytope.h"
|
|||
#include "src/utility/macros.h"
|
|||
#include "src/utility/vector.h"
|
|||
|
|||
#include "src/exceptions/UnexpectedException.h"
|
|||
|
|||
namespace storm { |
|||
namespace modelchecker { |
|||
namespace helper { |
|||
|
|||
template<typename SparseModelType, typename RationalNumberType> |
|||
typename std::unique_ptr<CheckResult> SparseMultiObjectivePostprocessor<SparseModelType, RationalNumberType>::postprocess(PreprocessorData const& preprocessorData, ResultData const& resultData) { |
|||
STORM_LOG_ASSERT(preprocessor. |
|||
switch(preprocessorData.queryType) { |
|||
case PreprocessorData::QueryType::Achievability: |
|||
return postprocessAchievabilityQuery(preprocessorData, resultData); |
|||
case PreprocessorData::QueryType::Numerical: |
|||
return postprocessNumericalQuery(preprocessorData, resultData); |
|||
case PreprocessorData::QueryType::Pareto: |
|||
return postprocessParetoQuery(preprocessorData, resultData); |
|||
default: |
|||
STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Unknown Query Type"); |
|||
} |
|||
|
|||
return std::unique_ptr<CheckResult>(new ExplicitQualitativeCheckResult());; |
|||
} |
|||
|
|||
template<typename SparseModelType, typename RationalNumberType> |
|||
typename std::unique_ptr<CheckResult> SparseMultiObjectivePostprocessor<SparseModelType, RationalNumberType>::postprocessAchievabilityQuery(PreprocessorData const& preprocessorData, ResultData const& resultData) { |
|||
|
|||
} |
|||
|
|||
template<typename SparseModelType, typename RationalNumberType> |
|||
typename std::unique_ptr<CheckResult> SparseMultiObjectivePostprocessor<SparseModelType, RationalNumberType>::postprocessNumericalQuery(PreprocessorData const& preprocessorData, ResultData const& resultData) { |
|||
|
|||
} |
|||
|
|||
template<typename SparseModelType, typename RationalNumberType> |
|||
typename std::unique_ptr<CheckResult> SparseMultiObjectivePostprocessor<SparseModelType, RationalNumberType>::postprocessParetoQuery(PreprocessorData const& preprocessorData, ResultData const& resultData) { |
|||
|
|||
std::cout << "Postprocessing pareto queries not yet implemented"; |
|||
} |
|||
|
|||
#ifdef STORM_HAVE_CARL
|
|||
template class SparseMultiObjectivePostprocessor<storm::models::sparse::Mdp<double>, storm::RationalNumber>; |
|||
#endif
|
|||
|
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,48 @@ |
|||
#ifndef STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEPOSTPROCESSOR_H_ |
|||
#define STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEPOSTPROCESSOR_H_ |
|||
|
|||
|
|||
#include <memory> |
|||
|
|||
#include "src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorData.h" |
|||
#include "src/modelchecker/multiobjective/helper/SparseMultiObjectiveResultData.h" |
|||
#include "src/modelchecker/results/CheckResult.h" |
|||
|
|||
namespace storm { |
|||
namespace modelchecker { |
|||
namespace helper { |
|||
|
|||
/* |
|||
* Helper Class to invoke the necessary preprocessing for multi objective model checking |
|||
*/ |
|||
template <class SparseModelType, typename RationalNumberType> |
|||
class SparseMultiObjectivePostprocessor { |
|||
public: |
|||
typedef typename SparseModelType::ValueType ValueType; |
|||
typedef typename SparseModelType::RewardModelType RewardModelType; |
|||
|
|||
typedef SparseMultiObjectiveObjectiveInformation<ValueType> ObjectiveInformation; |
|||
typedef SparseMultiObjectivePreprocessorData<SparseModelType> PreprocessorData; |
|||
typedef SparseMultiObjectiveResultData<RationalNumberType> ResultData; |
|||
|
|||
/*! |
|||
* Postprocesses the multi objective model checking result. |
|||
* |
|||
* @param preprocessorData the data of the preprocessing |
|||
* @param resultData the data of the model checking |
|||
*/ |
|||
static std::unique_ptr<CheckResult> postprocess(PreprocessorData const& preprocessorData, ResultData const& resultData); |
|||
|
|||
private: |
|||
static std::unique_ptr<CheckResult> postprocessAchievabilityQuery(PreprocessorData const& preprocessorData, ResultData const& resultData); |
|||
static std::unique_ptr<CheckResult> postprocessNumericalQuery(PreprocessorData const& preprocessorData, ResultData const& resultData); |
|||
static std::unique_ptr<CheckResult> postprocessParetoQuery(PreprocessorData const& preprocessorData, ResultData const& resultData); |
|||
|
|||
|
|||
}; |
|||
|
|||
} |
|||
} |
|||
} |
|||
|
|||
#endif /* STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEPOSTPROCESSOR_H_ */ |
|||
@ -0,0 +1,62 @@ |
|||
#ifndef STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEPREPROCESSORDATA_H_ |
|||
#define STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEPREPROCESSORDATA_H_ |
|||
|
|||
#include <vector> |
|||
#include <memory> |
|||
#include <iomanip> |
|||
#include <boost/optional.hpp> |
|||
|
|||
#include "src/modelchecker/multiobjective/helper/SparseMultiObjectiveObjectiveInformation.h" |
|||
|
|||
namespace storm { |
|||
namespace modelchecker { |
|||
|
|||
|
|||
namespace helper { |
|||
|
|||
template <class SparseModelType> |
|||
struct SparseMultiObjectivePreprocessorData { |
|||
|
|||
enum class QueryType { Achievability, Numerical, Pareto }; |
|||
|
|||
SparseModelType preprocessedModel; |
|||
SparseModelType const& originalModel; |
|||
std::vector<uint_fast64_t> newToOldStateIndexMapping; |
|||
|
|||
QueryType queryType; |
|||
std::vector<SparseMultiObjectiveObjectiveInformation<typename SparseModelType::ValueType>> objectives; |
|||
boost::optional<uint_fast64_t> indexOfOptimizingObjective; |
|||
|
|||
bool produceSchedulers; |
|||
|
|||
SparseMultiObjectivePreprocessorData(SparseModelType const& model) : preprocessedModel(model), originalModel(model), produceSchedulers(false) { |
|||
//Intentionally left empty |
|||
} |
|||
|
|||
void printToStream(std::ostream& out) { |
|||
out << "---------------------------------------------------------------------------------------------------------------------------------------" << std::endl; |
|||
out << " Multi-objective Preprocessor Data " << std::endl; |
|||
out << "---------------------------------------------------------------------------------------------------------------------------------------" << std::endl; |
|||
out << std::endl; |
|||
out << "Objectives:" << std::endl; |
|||
out << "--------------------------------------------------------------" << std::endl; |
|||
for (auto const& obj : objectives) { |
|||
obj.printToStream(out); |
|||
} |
|||
out << "--------------------------------------------------------------" << std::endl; |
|||
out << std::endl; |
|||
out << "Original Model Information:" << std::endl; |
|||
originalModel.printModelInformationToStream(out); |
|||
out << std::endl; |
|||
out << "Preprocessed Model Information:" << std::endl; |
|||
preprocessedModel.printModelInformationToStream(out); |
|||
out << std::endl; |
|||
out << "---------------------------------------------------------------------------------------------------------------------------------------" << std::endl; |
|||
} |
|||
|
|||
}; |
|||
} |
|||
} |
|||
} |
|||
|
|||
#endif /* STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEPREPROCESSORDATA_H_ */ |
|||
@ -1,105 +0,0 @@ |
|||
#ifndef STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEPREPROCESSORRETURNTYPE_H_ |
|||
#define STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEPREPROCESSORRETURNTYPE_H_ |
|||
|
|||
#include <vector> |
|||
#include <memory> |
|||
#include <iomanip> |
|||
#include <boost/optional.hpp> |
|||
|
|||
#include "src/logic/Formulas.h" |
|||
|
|||
namespace storm { |
|||
namespace modelchecker { |
|||
|
|||
|
|||
namespace helper { |
|||
|
|||
template <class SparseModelType> |
|||
struct SparseMultiObjectivePreprocessorReturnType { |
|||
|
|||
typedef typename SparseModelType::ValueType ValueType; |
|||
typedef typename SparseModelType::RewardModelType RewardModelType; |
|||
|
|||
struct ObjectiveInformation { |
|||
// the original input formula |
|||
std::shared_ptr<storm::logic::Formula const> originalFormula; |
|||
|
|||
// the name of the considered reward model in the preprocessedModel |
|||
std::string rewardModelName; |
|||
|
|||
// true if all rewards for this objective are positive, false if all rewards are negative. |
|||
bool rewardsArePositive; |
|||
|
|||
// transformation from the values of the preprocessed model to the ones for the actual input model, i.e., |
|||
// x is achievable in the preprocessed model iff factor*x + offset is achievable in the original model |
|||
ValueType toOriginalValueTransformationFactor; |
|||
ValueType toOriginalValueTransformationOffset; |
|||
|
|||
// The probability/reward threshold for the preprocessed model (if originalFormula specifies one). |
|||
// This is always a lower bound. |
|||
boost::optional<ValueType> threshold; |
|||
// True iff the specified threshold is strict, i.e., > |
|||
bool thresholdIsStrict = false; |
|||
|
|||
// The (discrete) stepBound for the formula (if given by the originalFormula) |
|||
boost::optional<uint_fast64_t> stepBound; |
|||
|
|||
void printToStream(std::ostream& out) const { |
|||
out << std::setw(30) << originalFormula->toString(); |
|||
out << " \t(toOrigVal:" << std::setw(3) << toOriginalValueTransformationFactor << "*x +" << std::setw(3) << toOriginalValueTransformationOffset << ", \t"; |
|||
out << "intern threshold:"; |
|||
if(threshold){ |
|||
out << (thresholdIsStrict ? " >" : ">="); |
|||
out << std::setw(5) << (*threshold) << ","; |
|||
} else { |
|||
out << " none,"; |
|||
} |
|||
out << " \t"; |
|||
out << "intern reward model: " << std::setw(10) << rewardModelName; |
|||
out << (rewardsArePositive ? " (positive)" : " (negative)") << ", \t"; |
|||
out << "step bound:"; |
|||
if(stepBound) { |
|||
out << std::setw(5) << (*stepBound); |
|||
} else { |
|||
out << " none"; |
|||
} |
|||
out << ")" << std::endl; |
|||
} |
|||
}; |
|||
|
|||
SparseMultiObjectivePreprocessorReturnType(SparseModelType const& model) : preprocessedModel(model), originalModel(model) , produceSchedulers(false) { |
|||
//Intentionally left empty |
|||
} |
|||
|
|||
void printToStream(std::ostream& out) { |
|||
out << "---------------------------------------------------------------------------------------------------------------------------------------" << std::endl; |
|||
out << " Multi-objective Preprocessor Result " << std::endl; |
|||
out << "---------------------------------------------------------------------------------------------------------------------------------------" << std::endl; |
|||
out << std::endl; |
|||
out << "Objectives:" << std::endl; |
|||
out << "--------------------------------------------------------------" << std::endl; |
|||
for (auto const& obj : objectives) { |
|||
obj.printToStream(out); |
|||
} |
|||
out << "--------------------------------------------------------------" << std::endl; |
|||
out << std::endl; |
|||
out << "Original Model Information:" << std::endl; |
|||
originalModel.printModelInformationToStream(out); |
|||
out << std::endl; |
|||
out << "Preprocessed Model Information:" << std::endl; |
|||
preprocessedModel.printModelInformationToStream(out); |
|||
out << std::endl; |
|||
out << "---------------------------------------------------------------------------------------------------------------------------------------" << std::endl; |
|||
} |
|||
|
|||
SparseModelType preprocessedModel; |
|||
SparseModelType const& originalModel; |
|||
std::vector<uint_fast64_t> newToOldStateIndexMapping; |
|||
std::vector<ObjectiveInformation> objectives; |
|||
bool produceSchedulers; |
|||
}; |
|||
} |
|||
} |
|||
} |
|||
|
|||
#endif /* STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEPREPROCESSORRETURNTYPE_H_ */ |
|||
Write
Preview
Loading…
Cancel
Save
Reference in new issue