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<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
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<typename SparseMdpModelType>
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<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";
}
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<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){
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 <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;
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<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