TimQu
9 years ago
15 changed files with 590 additions and 17 deletions
-
5src/CMakeLists.txt
-
3src/logic/FragmentChecker.cpp
-
18src/logic/FragmentSpecification.cpp
-
4src/logic/FragmentSpecification.h
-
25src/logic/MultiObjectiveFormula.cpp
-
10src/logic/MultiObjectiveFormula.h
-
7src/modelchecker/AbstractModelChecker.cpp
-
6src/modelchecker/AbstractModelChecker.h
-
46src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.cpp
-
27src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.h
-
254src/modelchecker/multiobjective/helper/SparseMdpMultiObjectivePreprocessingHelper.cpp
-
62src/modelchecker/multiobjective/helper/SparseMdpMultiObjectivePreprocessingHelper.h
-
83src/modelchecker/multiobjective/helper/SparseMultiObjectiveModelCheckerInformation.h
-
17src/utility/storm.h
-
40test/functional/logic/FragmentCheckerTest.cpp
@ -0,0 +1,46 @@ |
|||||
|
#include "src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.h"
|
||||
|
|
||||
|
#include "src/utility/macros.h"
|
||||
|
#include "src/logic/Formulas.h"
|
||||
|
#include "src/logic/FragmentSpecification.h"
|
||||
|
|
||||
|
#include "src/models/sparse/StandardRewardModel.h"
|
||||
|
|
||||
|
#include "src/modelchecker/results/ExplicitQualitativeCheckResult.h"
|
||||
|
#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
|
||||
|
|
||||
|
#include "src/modelchecker/multiobjective/helper/SparseMdpMultiObjectivePreprocessingHelper.h"
|
||||
|
#include "src/modelchecker/multiobjective/helper/SparseMultiObjectiveModelCheckerInformation.h"
|
||||
|
|
||||
|
#include "src/exceptions/NotImplementedException.h"
|
||||
|
|
||||
|
namespace storm { |
||||
|
namespace modelchecker { |
||||
|
template<typename SparseMdpModelType> |
||||
|
SparseMdpMultiObjectiveModelChecker<SparseMdpModelType>::SparseMdpMultiObjectiveModelChecker(SparseMdpModelType const& model) : SparseMdpPrctlModelChecker<SparseMdpModelType>(model) { |
||||
|
// Intentionally left empty.
|
||||
|
} |
||||
|
|
||||
|
template<typename SparseMdpModelType> |
||||
|
bool SparseMdpMultiObjectiveModelChecker<SparseMdpModelType>::canHandle(CheckTask<storm::logic::Formula> const& checkTask) const { |
||||
|
// A formula without multi objective (sub)formulas can be handled by the base class
|
||||
|
if(SparseMdpPrctlModelChecker<SparseMdpModelType>::canHandle(checkTask)) return true; |
||||
|
//In general, each initial state requires an individual scheduler (in contrast to single objective model checking). Let's exclude this.
|
||||
|
if(this->getModel().getInitialStates().getNumberOfSetBits() > 1) return false; |
||||
|
if(!checkTask.isOnlyInitialStatesRelevantSet()) return false; |
||||
|
return checkTask.getFormula().isInFragment(storm::logic::multiObjective()); |
||||
|
} |
||||
|
|
||||
|
template<typename SparseMdpModelType> |
||||
|
std::unique_ptr<CheckResult> SparseMdpMultiObjectiveModelChecker<SparseMdpModelType>::checkMultiObjectiveFormula(CheckTask<storm::logic::MultiObjectiveFormula> const& checkTask) { |
||||
|
|
||||
|
helper::SparseMultiObjectiveModelCheckerInformation<SparseMdpModelType> info = helper::SparseMdpMultiObjectivePreprocessingHelper<SparseMdpModelType>::preprocess(checkTask.getFormula(), this->getModel()); |
||||
|
|
||||
|
return std::unique_ptr<CheckResult>(new ExplicitQualitativeCheckResult()); |
||||
|
} |
||||
|
|
||||
|
|
||||
|
|
||||
|
template class SparseMdpMultiObjectiveModelChecker<storm::models::sparse::Mdp<double>>; |
||||
|
} |
||||
|
} |
||||
@ -0,0 +1,27 @@ |
|||||
|
#ifndef STORM_MODELCHECKER_MULTIOBJECTIVE_SPARSEMDPMULTIOBJECTIVEMODELCHECKER_H_ |
||||
|
#define STORM_MODELCHECKER_MULTIOBJECTIVE_SPARSEMDPMULTIOBJECTIVEMODELCHECKER_H_ |
||||
|
|
||||
|
#include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h" |
||||
|
|
||||
|
namespace storm { |
||||
|
namespace modelchecker { |
||||
|
template<class SparseMdpModelType> |
||||
|
class SparseMdpMultiObjectiveModelChecker : public SparseMdpPrctlModelChecker<SparseMdpModelType> { |
||||
|
public: |
||||
|
typedef typename SparseMdpModelType::ValueType ValueType; |
||||
|
typedef typename SparseMdpModelType::RewardModelType RewardModelType; |
||||
|
|
||||
|
explicit SparseMdpMultiObjectiveModelChecker(SparseMdpModelType const& model); |
||||
|
|
||||
|
virtual bool canHandle(CheckTask<storm::logic::Formula> const& checkTask) const override; |
||||
|
|
||||
|
virtual std::unique_ptr<CheckResult> checkMultiObjectiveFormula(CheckTask<storm::logic::MultiObjectiveFormula> const& checkTask) override; |
||||
|
|
||||
|
private: |
||||
|
|
||||
|
|
||||
|
}; |
||||
|
} // namespace modelchecker |
||||
|
} // namespace storm |
||||
|
|
||||
|
#endif /* STORM_MODELCHECKER_MULTIOBJECTIVE_SPARSEMDPMULTIOBJECTIVEMODELCHECKER_H_ */ |
||||
@ -0,0 +1,254 @@ |
|||||
|
#include "src/modelchecker/multiobjective/helper/SparseMdpMultiObjectivePreprocessingHelper.h"
|
||||
|
|
||||
|
#include "src/models/sparse/Mdp.h"
|
||||
|
#include "src/models/sparse/StandardRewardModel.h"
|
||||
|
|
||||
|
#include "src/modelchecker/propositional/SparsePropositionalModelChecker.h"
|
||||
|
#include "src/modelchecker/results/ExplicitQualitativeCheckResult.h"
|
||||
|
|
||||
|
#include "src/storage/BitVector.h"
|
||||
|
|
||||
|
#include "src/utility/macros.h"
|
||||
|
#include "src/utility/vector.h"
|
||||
|
#include "src/utility/graph.h"
|
||||
|
|
||||
|
#include "src/exceptions/InvalidPropertyException.h"
|
||||
|
#include "src/exceptions/UnexpectedException.h"
|
||||
|
|
||||
|
namespace storm { |
||||
|
namespace modelchecker { |
||||
|
namespace helper { |
||||
|
|
||||
|
template<typename SparseMdpModelType> |
||||
|
SparseMultiObjectiveModelCheckerInformation<SparseMdpModelType> SparseMdpMultiObjectivePreprocessingHelper<SparseMdpModelType>::preprocess(storm::logic::MultiObjectiveFormula const& originalFormula, SparseMdpModelType originalModel) { |
||||
|
Information info(std::move(originalModel)); |
||||
|
|
||||
|
//Initialize the state mapping.
|
||||
|
info.getNewToOldStateMapping().reserve(info.getModel().getNumberOfStates()); |
||||
|
for(uint_fast64_t state = 0; state < info.getModel().getNumberOfStates(); ++state){ |
||||
|
info.getNewToOldStateMapping().push_back(state); |
||||
|
} |
||||
|
|
||||
|
//Gather information regarding the individual objectives
|
||||
|
if(!gatherObjectiveInformation(originalFormula, info)){ |
||||
|
STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Could not gather information for objectives " << originalFormula << "."); |
||||
|
} |
||||
|
|
||||
|
// Find out whether negative rewards should be considered.
|
||||
|
if(!setWhetherNegativeRewardsAreConsidered(info)){ |
||||
|
STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Could not find out whether to consider negative rewards " << originalFormula << "."); |
||||
|
} |
||||
|
|
||||
|
//Invoke preprocessing on objectives
|
||||
|
bool success = false; |
||||
|
for (auto& obj : info.getObjectives()){ |
||||
|
STORM_LOG_DEBUG("Preprocessing objective " << *obj.originalFormula << "."); |
||||
|
if(obj.originalFormula->isProbabilityOperatorFormula()){ |
||||
|
success = preprocess(obj.originalFormula->asProbabilityOperatorFormula(), info, obj); |
||||
|
} else if(obj.originalFormula->isRewardOperatorFormula()){ |
||||
|
success = preprocess(obj.originalFormula->asRewardOperatorFormula(), info, obj); |
||||
|
} |
||||
|
} |
||||
|
STORM_LOG_THROW(success, storm::exceptions::InvalidPropertyException, "Could not preprocess for the formula " << originalFormula << "."); |
||||
|
return info; |
||||
|
} |
||||
|
|
||||
|
template<typename SparseMdpModelType> |
||||
|
bool SparseMdpMultiObjectivePreprocessingHelper<SparseMdpModelType>::gatherObjectiveInformation(storm::logic::MultiObjectiveFormula const& formula, Information& info) { |
||||
|
for(auto const& subF : formula.getSubFormulas()){ |
||||
|
if(!subF->isOperatorFormula()){ |
||||
|
STORM_LOG_ERROR("Expected an OperatorFormula as subformula of " << formula << " but got " << *subF); |
||||
|
return false; |
||||
|
} |
||||
|
storm::logic::OperatorFormula const& f = subF->asOperatorFormula(); |
||||
|
typename Information::ObjectiveInformation objective; |
||||
|
|
||||
|
objective.originalFormula = subF; |
||||
|
|
||||
|
if(f.hasBound()){ |
||||
|
objective.threshold = f.getBound().threshold; |
||||
|
// Note that we minimize if the comparison type is an upper bound since we are interested in the EXISTENCE of a scheduler...
|
||||
|
objective.originalFormulaMinimizes = !storm::logic::isLowerBound(f.getBound().comparisonType); |
||||
|
} else if (f.hasOptimalityType()){ |
||||
|
objective.originalFormulaMinimizes = storm::solver::minimize(f.getOptimalityType()); |
||||
|
} else { |
||||
|
STORM_LOG_ERROR("Current objective" << f << "does not specify whether to minimize or maximize"); |
||||
|
} |
||||
|
|
||||
|
objective.rewardModelName = "objective" + std::to_string(info.getObjectives().size()); |
||||
|
// Make sure the new reward model gets a unique name
|
||||
|
while(info.getModel().hasRewardModel(objective.rewardModelName)){ |
||||
|
objective.rewardModelName = "_" + objective.rewardModelName; |
||||
|
} |
||||
|
|
||||
|
if(!setStepBoundOfObjective(objective)) { |
||||
|
return false; |
||||
|
} |
||||
|
|
||||
|
info.getObjectives().push_back(std::move(objective)); |
||||
|
} |
||||
|
return true; |
||||
|
} |
||||
|
|
||||
|
template<typename SparseMdpModelType> |
||||
|
bool SparseMdpMultiObjectivePreprocessingHelper<SparseMdpModelType>::setStepBoundOfObjective(typename Information::ObjectiveInformation& objective){ |
||||
|
if(objective.originalFormula->isProbabilityOperatorFormula()){ |
||||
|
storm::logic::Formula const& f = objective.originalFormula->asProbabilityOperatorFormula().getSubformula(); |
||||
|
if(f.isBoundedUntilFormula()){ |
||||
|
if(f.asBoundedUntilFormula().hasDiscreteTimeBound()){ |
||||
|
objective.stepBound = f.asBoundedUntilFormula().getDiscreteTimeBound(); |
||||
|
} else { |
||||
|
STORM_LOG_ERROR("Expected a discrete time bound at boundedUntilFormula but got" << f << "."); |
||||
|
return false; |
||||
|
} |
||||
|
} |
||||
|
} else if(objective.originalFormula->isRewardOperatorFormula()){ |
||||
|
storm::logic::Formula const& f = objective.originalFormula->asRewardOperatorFormula(); |
||||
|
if(f.isCumulativeRewardFormula()){ |
||||
|
if(f.asCumulativeRewardFormula().hasDiscreteTimeBound()){ |
||||
|
objective.stepBound = f.asCumulativeRewardFormula().getDiscreteTimeBound(); |
||||
|
} else { |
||||
|
STORM_LOG_ERROR("Expected a discrete time bound at cumulativeRewardFormula but got" << f << "."); |
||||
|
return false; |
||||
|
} |
||||
|
} |
||||
|
} else { |
||||
|
STORM_LOG_ERROR("Expected a Probability or Reward OperatorFormula but got " << *objective.originalFormula << "."); |
||||
|
return false; |
||||
|
} |
||||
|
return true; |
||||
|
} |
||||
|
|
||||
|
template<typename SparseMdpModelType> |
||||
|
bool SparseMdpMultiObjectivePreprocessingHelper<SparseMdpModelType>::setWhetherNegativeRewardsAreConsidered(Information& info) { |
||||
|
// Negative Rewards are considered whenever there is an unbounded reward objective that requires to minimize.
|
||||
|
// If there is no unbounded reward objective, we make a majority vote.
|
||||
|
uint_fast64_t numOfMinimizingObjectives = 0; |
||||
|
for(auto const& obj : info.getObjectives()){ |
||||
|
if(obj.originalFormula->isRewardOperatorFormula() && !obj.stepBound){ |
||||
|
info.setNegativeRewardsConsidered(obj.originalFormulaMinimizes); |
||||
|
return true; |
||||
|
} |
||||
|
numOfMinimizingObjectives += obj.originalFormulaMinimizes ? 1 : 0; |
||||
|
} |
||||
|
// Reaching this point means that we make a majority vote
|
||||
|
info.setNegativeRewardsConsidered(numOfMinimizingObjectives*2 > info.getObjectives().size()); |
||||
|
return true; |
||||
|
} |
||||
|
|
||||
|
template<typename SparseMdpModelType> |
||||
|
bool SparseMdpMultiObjectivePreprocessingHelper<SparseMdpModelType>::preprocess(storm::logic::ProbabilityOperatorFormula const& formula, Information& info, typename Information::ObjectiveInformation& currentObjective) { |
||||
|
// Check if we need to complement the property, e.g., P<0.3 [ F "a" ] ---> P >=0.7 [ G !"a" ]
|
||||
|
// This is the case if the formula requires to minimize and positive rewards are considered or vice versa
|
||||
|
if(info.areNegativeRewardsConsidered() != currentObjective.originalFormulaMinimizes){ |
||||
|
STORM_LOG_ERROR("Inverting of properties not yet supported"); |
||||
|
//TODO
|
||||
|
return false; |
||||
|
} |
||||
|
|
||||
|
bool success = false; |
||||
|
// Invoke preprocessing for subformula
|
||||
|
if(formula.getSubformula().isUntilFormula()){ |
||||
|
success = preprocess(formula.getSubformula().asUntilFormula(), info, currentObjective); |
||||
|
} else if(formula.getSubformula().isBoundedUntilFormula()){ |
||||
|
success = preprocess(formula.getSubformula().asBoundedUntilFormula(), info, currentObjective); |
||||
|
} else if(formula.getSubformula().isGloballyFormula()){ |
||||
|
success = preprocess(formula.getSubformula().asGloballyFormula(), info, currentObjective); |
||||
|
} else if(formula.getSubformula().isEventuallyFormula()){ |
||||
|
success = preprocess(formula.getSubformula().asEventuallyFormula(), info, currentObjective); |
||||
|
} |
||||
|
STORM_LOG_ERROR_COND(success, "No implementation for the subformula of " << formula << "."); |
||||
|
|
||||
|
return success; |
||||
|
} |
||||
|
|
||||
|
template<typename SparseMdpModelType> |
||||
|
bool SparseMdpMultiObjectivePreprocessingHelper<SparseMdpModelType>::preprocess(storm::logic::RewardOperatorFormula const& formula, Information& info, typename Information::ObjectiveInformation& currentObjective) { |
||||
|
// Make sure that our decision for negative rewards is consistent with the formula
|
||||
|
if(info.areNegativeRewardsConsidered() != currentObjective.originalFormulaMinimizes){ |
||||
|
STORM_LOG_ERROR("Decided to consider " << (info.areNegativeRewardsConsidered() ? "negative" : "non-negative") << "rewards, but the formula " << formula << (currentObjective.originalFormulaMinimizes ? " minimizes" : "maximizes") << ". Reward objectives should either all minimize or all maximize."); |
||||
|
return false; |
||||
|
} |
||||
|
|
||||
|
// Check if the reward model is uniquely specified
|
||||
|
if((formula.hasRewardModelName() && info.getModel().hasRewardModel(formula.getRewardModelName())) |
||||
|
|| info.getModel().hasUniqueRewardModel()){ |
||||
|
STORM_LOG_ERROR("The reward model is not unique and the formula " << formula << " does not specify a reward model."); |
||||
|
return false; |
||||
|
} |
||||
|
|
||||
|
bool success = false; |
||||
|
// Invoke preprocessing for subformula
|
||||
|
if(formula.getSubformula().isEventuallyFormula()){ |
||||
|
success = preprocess(formula.getSubformula().asEventuallyFormula(), info, currentObjective, formula.getOptionalRewardModelName()); |
||||
|
} else if(formula.getSubformula().isCumulativeRewardFormula()) { |
||||
|
success = preprocess(formula.getSubformula().asCumulativeRewardFormula(), info, currentObjective, formula.getOptionalRewardModelName()); |
||||
|
} |
||||
|
STORM_LOG_ERROR_COND(success, "No implementation for the subformula of " << formula << "."); |
||||
|
|
||||
|
return success; |
||||
|
|
||||
|
} |
||||
|
|
||||
|
template<typename SparseMdpModelType> |
||||
|
bool SparseMdpMultiObjectivePreprocessingHelper<SparseMdpModelType>::preprocess(storm::logic::UntilFormula const& formula, Information& info, typename Information::ObjectiveInformation& currentObjective) { |
||||
|
bool success = false; |
||||
|
CheckTask<storm::logic::Formula> phiTask(formula.getLeftSubformula()); |
||||
|
CheckTask<storm::logic::Formula> psiTask(formula.getRightSubformula()); |
||||
|
storm::modelchecker::SparsePropositionalModelChecker<SparseMdpModelType> mc(info.getModel()); |
||||
|
success = mc.canHandle(phiTask) && mc.canHandle(psiTask); |
||||
|
STORM_LOG_ERROR_COND(success, "The subformulas of " << formula << " should be propositional."); |
||||
|
storm::storage::BitVector phiStates = mc.check(phiTask)->asExplicitQualitativeCheckResult().getTruthValuesVector(); |
||||
|
storm::storage::BitVector psiStates = mc.check(psiTask)->asExplicitQualitativeCheckResult().getTruthValuesVector(); |
||||
|
|
||||
|
// modelUnfolder(info.model, (~phiStates) | psiStates)
|
||||
|
// info.model = modelUnfolder.info()
|
||||
|
// build info.stateMapping from modelUnfolder.stateMapping
|
||||
|
// build stateaction reward vector
|
||||
|
// insert it in the model information
|
||||
|
|
||||
|
// TODO
|
||||
|
|
||||
|
return success; |
||||
|
} |
||||
|
|
||||
|
template<typename SparseMdpModelType> |
||||
|
bool SparseMdpMultiObjectivePreprocessingHelper<SparseMdpModelType>::preprocess(storm::logic::BoundedUntilFormula const& formula, Information& info, typename Information::ObjectiveInformation& currentObjective) { |
||||
|
return preprocess(storm::logic::UntilFormula(formula.getLeftSubformula().asSharedPointer(), formula.getRightSubformula().asSharedPointer()), info, currentObjective); |
||||
|
} |
||||
|
|
||||
|
template<typename SparseMdpModelType> |
||||
|
bool SparseMdpMultiObjectivePreprocessingHelper<SparseMdpModelType>::preprocess(storm::logic::GloballyFormula const& formula, Information& info, typename Information::ObjectiveInformation& currentObjective) { |
||||
|
//TODO
|
||||
|
STORM_LOG_ERROR("Globally not yet implemented"); |
||||
|
return false; |
||||
|
} |
||||
|
|
||||
|
template<typename SparseMdpModelType> |
||||
|
bool SparseMdpMultiObjectivePreprocessingHelper<SparseMdpModelType>::preprocess(storm::logic::EventuallyFormula const& formula, Information& info, typename Information::ObjectiveInformation& currentObjective, boost::optional<std::string> const& optionalRewardModelName) { |
||||
|
if(formula.isReachabilityProbabilityFormula()){ |
||||
|
return preprocess(storm::logic::UntilFormula(storm::logic::Formula::getTrueFormula(), formula.getSubformula().asSharedPointer()), info, currentObjective); |
||||
|
} |
||||
|
if (!formula.isReachabilityRewardFormula()){ |
||||
|
STORM_LOG_ERROR("The formula " << formula << " neither considers reachability Probabilities nor reachability rewards"); |
||||
|
return false; |
||||
|
} |
||||
|
//TODO
|
||||
|
STORM_LOG_ERROR("Rewards not yet implemented"); |
||||
|
return false; |
||||
|
} |
||||
|
|
||||
|
template<typename SparseMdpModelType> |
||||
|
bool SparseMdpMultiObjectivePreprocessingHelper<SparseMdpModelType>::preprocess(storm::logic::CumulativeRewardFormula const& formula, Information& info, typename Information::ObjectiveInformation& currentObjective, boost::optional<std::string> const& optionalRewardModelName) { |
||||
|
//TODO
|
||||
|
STORM_LOG_ERROR("Rewards not yet implemented"); |
||||
|
return false; |
||||
|
} |
||||
|
|
||||
|
|
||||
|
template class SparseMdpMultiObjectivePreprocessingHelper<storm::models::sparse::Mdp<double>>; |
||||
|
|
||||
|
|
||||
|
} |
||||
|
} |
||||
|
} |
||||
@ -0,0 +1,62 @@ |
|||||
|
#ifndef STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMDPMULTIOBJECTIVEPREPROCESSINGHELPER_H_ |
||||
|
#define STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMDPMULTIOBJECTIVEPREPROCESSINGHELPER_H_ |
||||
|
|
||||
|
#include "src/logic/Formulas.h" |
||||
|
#include "src/modelchecker/multiobjective/helper/SparseMultiObjectiveModelCheckerInformation.h" |
||||
|
#include "src/storage/BitVector.h" |
||||
|
|
||||
|
namespace storm { |
||||
|
namespace modelchecker { |
||||
|
|
||||
|
|
||||
|
namespace helper { |
||||
|
|
||||
|
/* |
||||
|
* Helper Class to invoke the necessary preprocessing for multi objective model checking |
||||
|
*/ |
||||
|
template <class SparseMdpModelType> |
||||
|
class SparseMdpMultiObjectivePreprocessingHelper { |
||||
|
public: |
||||
|
typedef typename SparseMdpModelType::ValueType ValueType; |
||||
|
typedef typename SparseMdpModelType::RewardModelType RewardModelType; |
||||
|
typedef SparseMultiObjectiveModelCheckerInformation<SparseMdpModelType> Information; |
||||
|
|
||||
|
/*! |
||||
|
* Preprocesses the given model w.r.t. the given formulas. |
||||
|
* @param originalModel The considered model |
||||
|
* @param originalFormula the considered formula. The subformulas should only contain one OperatorFormula at top level, i.e., the formula is simple. |
||||
|
*/ |
||||
|
static Information preprocess(storm::logic::MultiObjectiveFormula const& originalFormula, SparseMdpModelType originalModel); |
||||
|
|
||||
|
private: |
||||
|
|
||||
|
static bool gatherObjectiveInformation(storm::logic::MultiObjectiveFormula const& formula, Information& info); |
||||
|
static bool setStepBoundOfObjective(typename Information::ObjectiveInformation& currentObjective); |
||||
|
static bool setWhetherNegativeRewardsAreConsidered(Information& info); |
||||
|
|
||||
|
/*! |
||||
|
* Apply the neccessary preprocessing for the given formula. |
||||
|
* @param formula the current (sub)formula |
||||
|
* @param info the current state of the preprocessing. |
||||
|
* @return true iff there was no error |
||||
|
*/ |
||||
|
// State formulas (will transform the formula and the reward model) |
||||
|
static bool preprocess(storm::logic::ProbabilityOperatorFormula const& formula, Information& info, typename Information::ObjectiveInformation& currentObjective); |
||||
|
static bool preprocess(storm::logic::RewardOperatorFormula const& formula, Information& info, typename Information::ObjectiveInformation& currentObjective); |
||||
|
|
||||
|
// Path formulas (will transform the model) |
||||
|
static bool preprocess(storm::logic::UntilFormula const& formula, Information& info, typename Information::ObjectiveInformation& currentObjective); |
||||
|
static bool preprocess(storm::logic::BoundedUntilFormula const& formula, Information& info, typename Information::ObjectiveInformation& currentObjective); |
||||
|
static bool preprocess(storm::logic::GloballyFormula const& formula, Information& info, typename Information::ObjectiveInformation& currentObjective); |
||||
|
static bool preprocess(storm::logic::EventuallyFormula const& formula, Information& info, typename Information::ObjectiveInformation& currentObjective, boost::optional<std::string> const& optionalRewardModelName = boost::none); |
||||
|
static bool preprocess(storm::logic::CumulativeRewardFormula const& formula, Information& info, typename Information::ObjectiveInformation& currentObjective, boost::optional<std::string> const& optionalRewardModelName = boost::none); |
||||
|
|
||||
|
static storm::storage::BitVector checkPropositionalFormula(storm::logic::Formula propFormula, SparseMdpModelType const& model); |
||||
|
|
||||
|
}; |
||||
|
|
||||
|
} |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
#endif /* STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMDPMULTIOBJECTIVEPREPROCESSINGHELPER_H_ */ |
||||
@ -0,0 +1,83 @@ |
|||||
|
#ifndef STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEMODELCHECKERINFORMATION_H_ |
||||
|
#define STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEMODELCHECKERINFORMATION_H_ |
||||
|
|
||||
|
#include <vector> |
||||
|
#include <memory> |
||||
|
|
||||
|
#include "src/logic/Formulas.h" |
||||
|
|
||||
|
namespace storm { |
||||
|
namespace modelchecker { |
||||
|
|
||||
|
|
||||
|
namespace helper { |
||||
|
|
||||
|
template <class SparseModelType> |
||||
|
class SparseMultiObjectiveModelCheckerInformation { |
||||
|
public : |
||||
|
|
||||
|
typedef typename SparseModelType::ValueType ValueType; |
||||
|
typedef typename SparseModelType::RewardModelType RewardModelType; |
||||
|
|
||||
|
struct ObjectiveInformation { |
||||
|
std::shared_ptr<storm::logic::Formula const> originalFormula; |
||||
|
bool originalFormulaMinimizes; |
||||
|
boost::optional<double> threshold; |
||||
|
std::string rewardModelName; |
||||
|
boost::optional<uint_fast64_t> stepBound; |
||||
|
}; |
||||
|
|
||||
|
|
||||
|
SparseMultiObjectiveModelCheckerInformation(SparseModelType const& model) : model(model) { |
||||
|
//Intentionally left empty |
||||
|
} |
||||
|
|
||||
|
SparseMultiObjectiveModelCheckerInformation(SparseModelType && model) : model(model) { |
||||
|
//Intentionally left empty |
||||
|
} |
||||
|
|
||||
|
SparseModelType& getModel(){ |
||||
|
return model; |
||||
|
} |
||||
|
SparseModelType const& getModel() const { |
||||
|
return model; |
||||
|
} |
||||
|
|
||||
|
std::vector<uint_fast64_t>& getNewToOldStateMapping(){ |
||||
|
return newToOldStateMapping; |
||||
|
} |
||||
|
std::vector<uint_fast64_t>const& getNewToOldStateMapping() const{ |
||||
|
return newToOldStateMapping; |
||||
|
} |
||||
|
|
||||
|
bool areNegativeRewardsConsidered() { |
||||
|
return negativeRewardsConsidered; |
||||
|
} |
||||
|
|
||||
|
void setNegativeRewardsConsidered(bool value){ |
||||
|
negativeRewardsConsidered = value; |
||||
|
} |
||||
|
|
||||
|
std::vector<ObjectiveInformation>& getObjectives() { |
||||
|
return objectives; |
||||
|
} |
||||
|
std::vector<ObjectiveInformation>const& getObjectives() const { |
||||
|
return objectives; |
||||
|
} |
||||
|
|
||||
|
|
||||
|
private: |
||||
|
SparseModelType model; |
||||
|
std::vector<uint_fast64_t> newToOldStateMapping; |
||||
|
bool negativeRewardsConsidered; |
||||
|
|
||||
|
std::vector<ObjectiveInformation> objectives; |
||||
|
|
||||
|
|
||||
|
|
||||
|
}; |
||||
|
} |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
#endif /* STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEMODELCHECKERINFORMATION_H_ */ |
||||
Reference in new issue
xxxxxxxxxx