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

regarding preprocessing for MAs 

Former-commit-id: 7e67d60879
main
TimQu 9 years ago
parent
6010266e5b
commit
aae8fc8e87
9 changed files with 92 additions and 33 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. 2
      examples/multiobjective/ma/stream/stream2_pareto.csl
  2. 3
      src/logic/FragmentSpecification.cpp
  3. 7
      src/modelchecker/multiobjective/SparseMaMultiObjectiveModelChecker.cpp
  4. 2
      src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.cpp
  5. 15
      src/modelchecker/multiobjective/helper/SparseMultiObjectiveObjectiveInformation.h
  6. 54
      src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp
  7. 1
      src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.h
  8. 14
      src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorData.h
  9. 27
      src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.cpp

2
examples/multiobjective/ma/stream/stream2_pareto.csl
View File

@ -1 +1 @@
multi(R{"initialbuffering"}min=? [ F "done" ], R{numRestarts}min=? [ F "done" ])
multi(R{"initialbuffering"}min=? [ F "done" ], R{"numRestarts"}min=? [ F "done" ])

3
src/logic/FragmentSpecification.cpp
View File

@ -93,10 +93,9 @@ namespace storm {
multiObjective.setReachabilityProbabilityFormulasAllowed(true);
multiObjective.setRewardOperatorsAllowed(true);
multiObjective.setReachabilityRewardFormulasAllowed(true);
multiObjective.setCumulativeRewardFormulasAllowed(true);
multiObjective.setTotalRewardFormulasAllowed(true);
multiObjective.setBoundedUntilFormulasAllowed(true);
multiObjective.setStepBoundedUntilFormulasAllowed(true);
return multiObjective;
}

7
src/modelchecker/multiobjective/SparseMaMultiObjectiveModelChecker.cpp
View File

@ -15,7 +15,7 @@
#include "src/utility/Stopwatch.h"
#include "src/exceptions/NotImplementedException.h"
#include "src/exceptions/InvalidArgumentException.h"
namespace storm {
namespace modelchecker {
@ -31,12 +31,13 @@ namespace storm {
//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().setStepBoundedUntilFormulasAllowed(true));
return checkTask.getFormula().isInFragment(storm::logic::multiObjective().setTimeAllowed(true).setTimeBoundedUntilFormulasAllowed(true));
}
template<typename SparseMaModelType>
std::unique_ptr<CheckResult> SparseMaMultiObjectiveModelChecker<SparseMaModelType>::checkMultiObjectiveFormula(CheckTask<storm::logic::MultiObjectiveFormula> const& checkTask) {
STORM_LOG_ASSERT(this->getModel().getInitialStates().getNumberOfSetBits() == 1, "Multi Objective Model checking on model with multiple initial states is not supported.");
STORM_LOG_ASSERT(this->getModel().getInitialStates().getNumberOfSetBits() == 1, "Multi-objective Model checking on model with multiple initial states is not supported.");
STORM_LOG_THROW(this->getModel().isClosed(), storm::exceptions::InvalidArgumentException, "Unable to check multi-objective formula in non-closed Markov automaton.");
std::unique_ptr<CheckResult> result;
#ifdef STORM_HAVE_CARL

2
src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.cpp
View File

@ -31,7 +31,7 @@ namespace storm {
//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().setStepBoundedUntilFormulasAllowed(true));
return checkTask.getFormula().isInFragment(storm::logic::multiObjective().setCumulativeRewardFormulasAllowed(true));
}
template<typename SparseMdpModelType>

15
src/modelchecker/multiobjective/helper/SparseMultiObjectiveObjectiveInformation.h
View File

@ -31,8 +31,9 @@ namespace storm {
// 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;
// The time bound(s) for the formula (if given by the originalFormula)
// If only a discrete bound is given, it is interpreted as an upper bound
boost::optional<boost::variant<uint_fast64_t, std::pair<double, double>>> timeBounds;
// Stores whether reward finiteness has been checked for this objective.
bool rewardFinitenessChecked;
@ -50,9 +51,13 @@ namespace storm {
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);
out << "time bound:";
if(timeBounds) {
if(timeBounds->which() == 0 ) {
out << "<=" << std::setw(5) << (boost::get<uint_fast64_t>(timeBounds.get()));
} else {
out << "[" << boost::get<std::pair<double, double>>(timeBounds.get()).first << ", " << boost::get<std::pair<double, double>>(timeBounds.get()).second << "]";
}
} else {
out << " none";
}

54
src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp
View File

@ -122,6 +122,8 @@ namespace storm {
preprocessFormula(formula.asProbabilityOperatorFormula(), data, currentObjective);
} else if(formula.isRewardOperatorFormula()){
preprocessFormula(formula.asRewardOperatorFormula(), data, currentObjective);
} else if(formula.isTimeOperatorFormula()){
preprocessFormula(formula.asTimeOperatorFormula(), data, currentObjective);
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Could not preprocess the objective " << formula << " because it is not supported");
}
@ -173,6 +175,21 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The subformula of " << formula << " is not supported.");
}
}
template<typename SparseModelType>
void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessFormula(storm::logic::TimeOperatorFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective) {
// Time formulas are only supported for Markov automata
STORM_LOG_THROW(data.originalModel.isOfType(storm::models::ModelType::MarkovAutomaton), storm::exceptions::InvalidPropertyException, "Time operator formulas are only supported for Markov automata.");
// reward finiteness does not need to be checked if we want to minimize time
currentObjective.rewardFinitenessChecked = !currentObjective.rewardsArePositive;
if(formula.getSubformula().isEventuallyFormula()){
preprocessFormula(formula.getSubformula().asEventuallyFormula(), data, currentObjective, false, false);
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The subformula of " << formula << " is not supported.");
}
}
template<typename SparseModelType>
void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessFormula(storm::logic::UntilFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective, bool isProb0Formula, bool isProb1Formula) {
@ -242,10 +259,23 @@ namespace storm {
template<typename SparseModelType>
void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessFormula(storm::logic::BoundedUntilFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective) {
STORM_LOG_THROW(formula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Expected a boundedUntilFormula with a discrete time bound but got " << formula << ".");
currentObjective.stepBound = formula.getDiscreteTimeBound();
STORM_LOG_THROW(*currentObjective.stepBound > 0, storm::exceptions::InvalidPropertyException, "Got a boundedUntilFormula with time bound 0. This is not supported.");
preprocessFormula(storm::logic::UntilFormula(formula.getLeftSubformula().asSharedPointer(), formula.getRightSubformula().asSharedPointer()), data, currentObjective, false, false);
if(data.originalModel.isOfType(storm::models::ModelType::Mdp)) {
STORM_LOG_THROW(formula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Expected a boundedUntilFormula with a discrete time bound but got " << formula << ".");
STORM_LOG_THROW(formula.getDiscreteTimeBound() > 0, storm::exceptions::InvalidPropertyException, "Got a boundedUntilFormula with time bound 0. This is not supported.");
currentObjective.timeBounds = formula.getDiscreteTimeBound();
preprocessFormula(storm::logic::UntilFormula(formula.getLeftSubformula().asSharedPointer(), formula.getRightSubformula().asSharedPointer()), data, currentObjective, false, false);
} else if(data.originalModel.isOfType(storm::models::ModelType::MarkovAutomaton)) {
if(formula.hasDiscreteTimeBound()) {
STORM_LOG_THROW(formula.getDiscreteTimeBound() > 0, storm::exceptions::InvalidPropertyException, "Got a boundedUntilFormula with time bound 0. This is not supported.");
currentObjective.timeBounds = formula.getDiscreteTimeBound();
} else {
STORM_LOG_THROW(formula.getIntervalBounds().first==formula.getIntervalBounds().second, storm::exceptions::InvalidPropertyException, "Got a boundedUntilFormula where upper and lower time bounds are equal. This is not supported.");
currentObjective.timeBounds = formula.getIntervalBounds();
}
preprocessFormula(storm::logic::UntilFormula(formula.getLeftSubformula().asSharedPointer(), formula.getRightSubformula().asSharedPointer()), data, currentObjective, false, false);
}
}
template<typename SparseModelType>
@ -267,7 +297,6 @@ namespace storm {
preprocessFormula(storm::logic::UntilFormula(storm::logic::Formula::getTrueFormula(), formula.getSubformula().asSharedPointer()), data, currentObjective, isProb0Formula, isProb1Formula);
return;
}
STORM_LOG_THROW(formula.isReachabilityRewardFormula(), storm::exceptions::InvalidPropertyException, "The formula " << formula << " neither considers reachability Probabilities nor reachability rewards");
CheckTask<storm::logic::Formula> targetTask(formula.getSubformula());
storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> mc(data.preprocessedModel);
@ -277,7 +306,15 @@ namespace storm {
updatePreprocessedModel(data, *duplicatorResult.model, duplicatorResult.newToOldStateIndexMapping);
// Add a reward model that gives zero reward to the actions of states of the second copy.
std::vector<ValueType> objectiveRewards = data.preprocessedModel.getRewardModel(optionalRewardModelName ? optionalRewardModelName.get() : "").getTotalRewardVector(data.preprocessedModel.getTransitionMatrix());
std::vector<ValueType> objectiveRewards;
if(formula.isReachabilityRewardFormula()) {
objectiveRewards = data.preprocessedModel.getRewardModel(optionalRewardModelName ? optionalRewardModelName.get() : "").getTotalRewardVector(data.preprocessedModel.getTransitionMatrix());
} else if(formula.isReachabilityTimeFormula() && data.preprocessedModel.isOfType(storm::models::ModelType::MarkovAutomaton)) {
objectiveRewards = std::vector<ValueType>(data.preprocessedModel.getTransitionMatrix().getRowCount(), storm::utility::zero<ValueType>());
storm::utility::vector::setVectorValues(objectiveRewards, data.getMarkovianStatesOfPreprocessedModel(), storm::utility::one<ValueType>());
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The formula " << formula << " neither considers reachability probabilities nor reachability rewards " << (data.preprocessedModel.isOfType(storm::models::ModelType::MarkovAutomaton) ? "nor reachability time" : "") << ". This is not supported.");
}
for(auto secondCopyState : duplicatorResult.secondCopy) {
for(uint_fast64_t choice = data.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[secondCopyState]; choice < data.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[secondCopyState+1]; ++choice) {
objectiveRewards[choice] = storm::utility::zero<ValueType>();
@ -306,9 +343,10 @@ namespace storm {
template<typename SparseModelType>
void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessFormula(storm::logic::CumulativeRewardFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective, boost::optional<std::string> const& optionalRewardModelName) {
STORM_LOG_THROW(!data.originalModel.isOfType(storm::models::ModelType::MarkovAutomaton), storm::exceptions::InvalidPropertyException, "Cumulative reward formulas are not supported for Markov automata.");
STORM_LOG_THROW(formula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Expected a cumulativeRewardFormula with a discrete time bound but got " << formula << ".");
currentObjective.stepBound = formula.getDiscreteTimeBound();
STORM_LOG_THROW(*currentObjective.stepBound > 0, storm::exceptions::InvalidPropertyException, "Got a cumulativeRewardFormula with time bound 0. This is not supported.");
STORM_LOG_THROW(formula.getDiscreteTimeBound() > 0, storm::exceptions::InvalidPropertyException, "Got a cumulativeRewardFormula with time bound 0. This is not supported.");
currentObjective.timeBounds = formula.getDiscreteTimeBound();
std::vector<ValueType> objectiveRewards = data.preprocessedModel.getRewardModel(optionalRewardModelName ? optionalRewardModelName.get() : "").getTotalRewardVector(data.preprocessedModel.getTransitionMatrix());
if(!currentObjective.rewardsArePositive){

1
src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.h
View File

@ -43,6 +43,7 @@ namespace storm {
static void preprocessFormula(storm::logic::OperatorFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective);
static void preprocessFormula(storm::logic::ProbabilityOperatorFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective);
static void preprocessFormula(storm::logic::RewardOperatorFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective);
static void preprocessFormula(storm::logic::TimeOperatorFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective);
static void preprocessFormula(storm::logic::UntilFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective, bool isProb0Formula, bool isProb1Formula);
static void preprocessFormula(storm::logic::BoundedUntilFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective);
static void preprocessFormula(storm::logic::GloballyFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective, bool isProb0Formula, bool isProb1Formula);

14
src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorData.h
View File

@ -4,10 +4,12 @@
#include <vector>
#include <memory>
#include <iomanip>
#include <type_traits>
#include <boost/optional.hpp>
#include "src/logic/Formulas.h"
#include "src/modelchecker/multiobjective/helper/SparseMultiObjectiveObjectiveInformation.h"
#include "src/models/sparse/MarkovAutomaton.h"
#include "src/storage/BitVector.h"
#include "src/utility/macros.h"
@ -47,6 +49,18 @@ namespace storm {
this->preprocessedModel.getStateLabeling().addLabel(this->prob1StatesLabel, storm::storage::BitVector(this->preprocessedModel.getNumberOfStates(), true));
}
template<typename MT = SparseModelType>
typename std::enable_if<std::is_same<MT, storm::models::sparse::MarkovAutomaton<typename SparseModelType::ValueType>>::value, storm::storage::BitVector const&>::type
getMarkovianStatesOfPreprocessedModel() {
return preprocessedModel.getMarkovianStates();
}
template<typename MT = SparseModelType>
typename std::enable_if<!std::is_same<MT, storm::models::sparse::MarkovAutomaton<typename SparseModelType::ValueType>>::value, storm::storage::BitVector const&>::type
getMarkovianStatesOfPreprocessedModel() {
STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Tried to retrieve Markovian states but the considered model is not an MA.");
}
void printToStream(std::ostream& out) const {
out << std::endl;
out << "---------------------------------------------------------------------------------------------------------------------------------------" << std::endl;

27
src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.cpp
View File

@ -35,7 +35,7 @@ namespace storm {
storm::storage::BitVector unboundedObjectives(data.objectives.size(), false);
std::vector<ValueType> weightedRewardVector(data.preprocessedModel.getTransitionMatrix().getRowCount(), storm::utility::zero<ValueType>());
for(uint_fast64_t objIndex = 0; objIndex < data.objectives.size(); ++objIndex) {
if(!data.objectives[objIndex].stepBound) {
if(!data.objectives[objIndex].timeBounds) {
unboundedObjectives.set(objIndex, true);
storm::utility::vector::addScaledVector(weightedRewardVector, data.preprocessedModel.getRewardModel(data.objectives[objIndex].rewardModelName).getStateActionRewardVector(), weightVector[objIndex]);
}
@ -65,7 +65,7 @@ namespace storm {
storm::storage::TotalScheduler const& SparseMultiObjectiveWeightVectorChecker<SparseModelType>::getScheduler() const {
STORM_LOG_THROW(checkHasBeenCalled, storm::exceptions::IllegalFunctionCallException, "Tried to retrieve results but check(..) has not been called before.");
for(auto const& obj : data.objectives) {
STORM_LOG_THROW(!obj.stepBound, storm::exceptions::NotImplementedException, "Scheduler retrival is not implemented for stepbounded objectives.");
STORM_LOG_THROW(!obj.timeBounds, storm::exceptions::NotImplementedException, "Scheduler retrival is not implemented for timeBounded objectives.");
}
return scheduler;
}
@ -145,7 +145,7 @@ namespace storm {
//Also only compute values for objectives with weightVector != zero,
//one check can be omitted as the result can be computed back from the weighed result and the results from the remaining objectives
for(uint_fast64_t objIndex = 0; objIndex < data.objectives.size(); ++objIndex) {
if(data.objectives[objIndex].stepBound){
if(data.objectives[objIndex].timeBounds){
objectiveResults[objIndex] = std::vector<ValueType>(data.preprocessedModel.getNumberOfStates(), storm::utility::zero<ValueType>());
} else {
storm::utility::vector::selectVectorValues(deterministicStateRewards, this->scheduler.getChoices(), data.preprocessedModel.getTransitionMatrix().getRowGroupIndices(), data.preprocessedModel.getRewardModel(data.objectives[objIndex].rewardModelName).getStateActionRewardVector());
@ -173,21 +173,22 @@ namespace storm {
std::vector<uint_fast64_t> optimalChoicesInCurrentEpoch(data.preprocessedModel.getNumberOfStates());
std::vector<ValueType> choiceValues(weightedRewardVector.size());
std::vector<ValueType> temporaryResult(data.preprocessedModel.getNumberOfStates());
// Get for each occurring stepBound the indices of the objectives with that bound.
std::map<uint_fast64_t, storm::storage::BitVector, std::greater<uint_fast64_t>> stepBounds;
// Get for each occurring timeBound the indices of the objectives with that bound.
std::map<uint_fast64_t, storm::storage::BitVector, std::greater<uint_fast64_t>> timeBounds;
for(auto objIndex : boundedObjectives) {
auto stepBoundIt = stepBounds.insert(std::make_pair(*data.objectives[objIndex].stepBound, storm::storage::BitVector(data.objectives.size(), false))).first;
stepBoundIt->second.set(objIndex);
uint_fast64_t timeBound = boost::get<uint_fast64_t>(data.objectives[objIndex].timeBounds.get());
auto timeBoundIt = timeBounds.insert(std::make_pair(timeBound, storm::storage::BitVector(data.objectives.size(), false))).first;
timeBoundIt->second.set(objIndex);
}
storm::storage::BitVector objectivesAtCurrentEpoch = ~boundedObjectives;
auto stepBoundIt = stepBounds.begin();
for(uint_fast64_t currentEpoch = stepBoundIt->first; currentEpoch > 0; --currentEpoch) {
if(stepBoundIt != stepBounds.end() && currentEpoch == stepBoundIt->first) {
objectivesAtCurrentEpoch |= stepBoundIt->second;
for(auto objIndex : stepBoundIt->second) {
auto timeBoundIt = timeBounds.begin();
for(uint_fast64_t currentEpoch = timeBoundIt->first; currentEpoch > 0; --currentEpoch) {
if(timeBoundIt != timeBounds.end() && currentEpoch == timeBoundIt->first) {
objectivesAtCurrentEpoch |= timeBoundIt->second;
for(auto objIndex : timeBoundIt->second) {
storm::utility::vector::addScaledVector(weightedRewardVector, data.preprocessedModel.getRewardModel(data.objectives[objIndex].rewardModelName).getStateActionRewardVector(), weightVector[objIndex]);
}
++stepBoundIt;
++timeBoundIt;
}
// Get values and scheduler for weighted sum of objectives

Write Preview
Loading…
Cancel
Save