From aae8fc8e879d4bd8f9e2b63663349d9896f299d2 Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 29 Jun 2016 21:33:32 +0200 Subject: [PATCH] regarding preprocessing for MAs Former-commit-id: 7e67d608790bce3a3a7165bad9901ed5ac7c842d --- .../ma/stream/stream2_pareto.csl | 2 +- src/logic/FragmentSpecification.cpp | 3 +- .../SparseMaMultiObjectiveModelChecker.cpp | 7 +-- .../SparseMdpMultiObjectiveModelChecker.cpp | 2 +- ...SparseMultiObjectiveObjectiveInformation.h | 15 ++++-- .../SparseMultiObjectivePreprocessor.cpp | 54 ++++++++++++++++--- .../helper/SparseMultiObjectivePreprocessor.h | 1 + .../SparseMultiObjectivePreprocessorData.h | 14 +++++ ...parseMultiObjectiveWeightVectorChecker.cpp | 27 +++++----- 9 files changed, 92 insertions(+), 33 deletions(-) diff --git a/examples/multiobjective/ma/stream/stream2_pareto.csl b/examples/multiobjective/ma/stream/stream2_pareto.csl index 443415858..12e469030 100644 --- a/examples/multiobjective/ma/stream/stream2_pareto.csl +++ b/examples/multiobjective/ma/stream/stream2_pareto.csl @@ -1 +1 @@ -multi(R{"initialbuffering"}min=? [ F "done" ], R{numRestarts}min=? [ F "done" ]) +multi(R{"initialbuffering"}min=? [ F "done" ], R{"numRestarts"}min=? [ F "done" ]) diff --git a/src/logic/FragmentSpecification.cpp b/src/logic/FragmentSpecification.cpp index 851cc8741..0235e5ddf 100644 --- a/src/logic/FragmentSpecification.cpp +++ b/src/logic/FragmentSpecification.cpp @@ -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; } diff --git a/src/modelchecker/multiobjective/SparseMaMultiObjectiveModelChecker.cpp b/src/modelchecker/multiobjective/SparseMaMultiObjectiveModelChecker.cpp index edfafdcab..529f141c2 100644 --- a/src/modelchecker/multiobjective/SparseMaMultiObjectiveModelChecker.cpp +++ b/src/modelchecker/multiobjective/SparseMaMultiObjectiveModelChecker.cpp @@ -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 std::unique_ptr SparseMaMultiObjectiveModelChecker::checkMultiObjectiveFormula(CheckTask 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 result; #ifdef STORM_HAVE_CARL diff --git a/src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.cpp b/src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.cpp index c191f0b63..820172d5a 100644 --- a/src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.cpp +++ b/src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.cpp @@ -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 diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveObjectiveInformation.h b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveObjectiveInformation.h index 4c5709939..5814bca3c 100644 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveObjectiveInformation.h +++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveObjectiveInformation.h @@ -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 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>> 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(timeBounds.get())); + } else { + out << "[" << boost::get>(timeBounds.get()).first << ", " << boost::get>(timeBounds.get()).second << "]"; + } } else { out << " none"; } diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp index 4ccca84cb..5d1661412 100644 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp +++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp @@ -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 + void SparseMultiObjectivePreprocessor::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 void SparseMultiObjectivePreprocessor::preprocessFormula(storm::logic::UntilFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective, bool isProb0Formula, bool isProb1Formula) { @@ -242,10 +259,23 @@ namespace storm { template void SparseMultiObjectivePreprocessor::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 @@ -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 targetTask(formula.getSubformula()); storm::modelchecker::SparsePropositionalModelChecker 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 objectiveRewards = data.preprocessedModel.getRewardModel(optionalRewardModelName ? optionalRewardModelName.get() : "").getTotalRewardVector(data.preprocessedModel.getTransitionMatrix()); + std::vector 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(data.preprocessedModel.getTransitionMatrix().getRowCount(), storm::utility::zero()); + storm::utility::vector::setVectorValues(objectiveRewards, data.getMarkovianStatesOfPreprocessedModel(), storm::utility::one()); + } 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(); @@ -306,9 +343,10 @@ namespace storm { template void SparseMultiObjectivePreprocessor::preprocessFormula(storm::logic::CumulativeRewardFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective, boost::optional 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 objectiveRewards = data.preprocessedModel.getRewardModel(optionalRewardModelName ? optionalRewardModelName.get() : "").getTotalRewardVector(data.preprocessedModel.getTransitionMatrix()); if(!currentObjective.rewardsArePositive){ diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.h b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.h index 141bd7338..248a2c4fd 100644 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.h +++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.h @@ -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); diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorData.h b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorData.h index 373a086fc..6077758b4 100644 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorData.h +++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorData.h @@ -4,10 +4,12 @@ #include #include #include +#include #include #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 std::enable_if>::value, storm::storage::BitVector const&>::type + getMarkovianStatesOfPreprocessedModel() { + return preprocessedModel.getMarkovianStates(); + } + + template + typename std::enable_if>::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; diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.cpp b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.cpp index e5d343bd1..c631baa2d 100644 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.cpp +++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.cpp @@ -35,7 +35,7 @@ namespace storm { storm::storage::BitVector unboundedObjectives(data.objectives.size(), false); std::vector weightedRewardVector(data.preprocessedModel.getTransitionMatrix().getRowCount(), storm::utility::zero()); 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::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(data.preprocessedModel.getNumberOfStates(), storm::utility::zero()); } 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 optimalChoicesInCurrentEpoch(data.preprocessedModel.getNumberOfStates()); std::vector choiceValues(weightedRewardVector.size()); std::vector temporaryResult(data.preprocessedModel.getNumberOfStates()); - // Get for each occurring stepBound the indices of the objectives with that bound. - std::map> stepBounds; + // Get for each occurring timeBound the indices of the objectives with that bound. + std::map> 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(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