diff --git a/src/storm/cli/cli.cpp b/src/storm/cli/cli.cpp index 7310f56c6..181a67480 100644 --- a/src/storm/cli/cli.cpp +++ b/src/storm/cli/cli.cpp @@ -322,6 +322,12 @@ namespace storm { buildAndCheckExplicitModel(properties, true); #else STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "No parameters are supported in this build."); +#endif + } else if (generalSettings.isExactSet()) { +#ifdef STORM_HAVE_CARL + buildAndCheckExplicitModel(properties, true); +#else + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "No exact numbers are supported in this build."); #endif } else { buildAndCheckExplicitModel(properties, true); diff --git a/src/storm/cli/entrypoints.h b/src/storm/cli/entrypoints.h index 028d6b466..25be46969 100644 --- a/src/storm/cli/entrypoints.h +++ b/src/storm/cli/entrypoints.h @@ -441,35 +441,15 @@ namespace storm { STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::InvalidStateException, "Expected sparse model."); verifySparseModel(model->as>(), properties, onlyInitialStatesRelevant); } - } - -#ifdef STORM_HAVE_CARL - template<> - void buildAndCheckExplicitModel(std::vector const& properties, bool onlyInitialStatesRelevant) { - storm::settings::modules::IOSettings const& settings = storm::settings::getModule(); - - STORM_LOG_THROW(settings.isExplicitSet() || settings.isExplicitDRNSet(), storm::exceptions::InvalidStateException, "Unable to build explicit model without model files."); - - storm::utility::Stopwatch modelBuildingWatch(true); - std::shared_ptr model; - STORM_LOG_THROW(!settings.isExplicitSet(), storm::exceptions::NotSupportedException, "Parametric explicit model files are not supported."); - model = buildExplicitDRNModel(settings.getExplicitDRNFilename()); - modelBuildingWatch.stop(); - STORM_PRINT_AND_LOG("Time for model construction: " << modelBuildingWatch << "." << std::endl); - - // Preprocess the model if needed. - BRANCH_ON_MODELTYPE(model, model, storm::RationalFunction, storm::dd::DdType::CUDD, preprocessModel, extractFormulasFromProperties(properties)); - - // Print some information about the model. - model->printModelInformationToStream(std::cout); - - // Verify the model, if a formula was given. - if (!properties.empty()) { - STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::InvalidStateException, "Expected sparse model."); - verifySparseModel(model->as>(), properties, onlyInitialStatesRelevant); + + // Export DOT if required. + if(storm::settings::getModule().isExportDotSet()) { + std::ofstream stream; + storm::utility::openFile(storm::settings::getModule().getExportDotFilename(), stream); + model->as>()->writeDotToStream(stream); + storm::utility::closeFile(stream); } - } -#endif + } } } diff --git a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp index 8f2fd22ce..7f555e6d2 100644 --- a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp @@ -2,7 +2,7 @@ #include "storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h" -#include "storm/modelchecker/multiobjective/pcaa.h" +#include "storm/modelchecker/multiobjective/multiObjectiveModelChecking.h" #include "storm/models/sparse/StandardRewardModel.h" @@ -121,7 +121,7 @@ namespace storm { template std::unique_ptr SparseMarkovAutomatonCslModelChecker::checkMultiObjectiveFormula(CheckTask const& checkTask) { - return multiobjective::performPcaa(this->getModel(), checkTask.getFormula()); + return multiobjective::performMultiObjectiveModelChecking(this->getModel(), checkTask.getFormula()); } template class SparseMarkovAutomatonCslModelChecker>; diff --git a/src/storm/modelchecker/multiobjective/MultiObjectiveModelCheckingMethod.cpp b/src/storm/modelchecker/multiobjective/MultiObjectiveModelCheckingMethod.cpp new file mode 100644 index 000000000..6842c3ea7 --- /dev/null +++ b/src/storm/modelchecker/multiobjective/MultiObjectiveModelCheckingMethod.cpp @@ -0,0 +1,19 @@ +#include "storm/modelchecker/multiobjective/MultiObjectiveModelCheckingMethod.h" + + +namespace storm { + namespace modelchecker { + namespace multiobjective { + + std::string toString(MultiObjectiveMethod m) { + switch (m) { + case MultiObjectiveMethod::Pcaa: + return "Pareto Curve Approximation Algorithm"; + case MultiObjectiveMethod::ConstraintBased: + return "Constraint Based Algorithm"; + } + return "invalid"; + } + } + } +} diff --git a/src/storm/modelchecker/multiobjective/MultiObjectiveModelCheckingMethod.h b/src/storm/modelchecker/multiobjective/MultiObjectiveModelCheckingMethod.h new file mode 100644 index 000000000..3bef420cc --- /dev/null +++ b/src/storm/modelchecker/multiobjective/MultiObjectiveModelCheckingMethod.h @@ -0,0 +1,13 @@ +#pragma once + +#include "storm/utility/ExtendSettingEnumWithSelectionField.h" + +namespace storm { + namespace modelchecker { + namespace multiobjective { + ExtendEnumsWithSelectionField(MultiObjectiveMethod, Pcaa, ConstraintBased) + } + } +} + + diff --git a/src/storm/modelchecker/multiobjective/Objective.h b/src/storm/modelchecker/multiobjective/Objective.h new file mode 100644 index 000000000..09faaf075 --- /dev/null +++ b/src/storm/modelchecker/multiobjective/Objective.h @@ -0,0 +1,82 @@ +#pragma once + +#include + +#include "storm/logic/Formula.h" +#include "storm/logic/Bound.h" +#include "storm/logic/TimeBound.h" +#include "storm/solver/OptimizationDirection.h" + +namespace storm { + namespace modelchecker { + namespace multiobjective { + template + struct Objective { + // the original input formula + std::shared_ptr originalFormula; + + // the name of the considered reward model in the preprocessedModel + boost::optional rewardModelName; + + // True iff the complementary event is considered. + // E.g. if we consider P<1-t [F !"safe"] instead of P>=t [ G "safe"] + bool considersComplementaryEvent; + + // The probability/reward threshold for the preprocessed model (if originalFormula specifies one). + boost::optional bound; + // The optimization direction for the preprocessed model + // if originalFormula does ot specifies one, the direction is derived from the bound. + storm::solver::OptimizationDirection optimizationDirection; + + // Lower and upper time/step bouds + boost::optional lowerTimeBound, upperTimeBound; + + boost::optional lowerResultBound, upperResultBound; + + void printToStream(std::ostream& out) const { + out << originalFormula->toString(); + out << " \t"; + out << "direction: "; + out << optimizationDirection; + out << " \t"; + out << "intern bound: "; + if (bound){ + out << *bound; + } else { + out << " -none- "; + } + out << " \t"; + out << "time bounds: "; + if (lowerTimeBound && upperTimeBound) { + out << (lowerTimeBound->isStrict() ? "(" : "[") << lowerTimeBound->getBound() << "," << upperTimeBound->getBound() << (upperTimeBound->isStrict() ? ")" : "]"); + } else if (lowerTimeBound) { + out << (lowerTimeBound->isStrict() ? ">" : ">=") << lowerTimeBound->getBound(); + } else if (upperTimeBound) { + out << (upperTimeBound->isStrict() ? "<" : "<=") << upperTimeBound->getBound(); + } else { + out << " -none- "; + } + out << " \t"; + out << "intern reward model: "; + if (rewardModelName) { + out << *rewardModelName; + } else { + out << " -none- "; + } + out << " \t"; + out << "result bounds: "; + if (lowerResultBound && upperResultBound) { + out << "[" << *lowerResultBound << ", " << *upperResultBound << "]"; + } else if (lowerResultBound) { + out << ">=" << *lowerResultBound; + } else if (upperResultBound) { + out << "<=" << *upperResultBound; + } else { + out << " -none- "; + } + } + }; + } + } +} + diff --git a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp new file mode 100644 index 000000000..252af5a7a --- /dev/null +++ b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp @@ -0,0 +1,504 @@ +#include "storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.h" + +#include +#include + +#include "storm/models/sparse/Mdp.h" +#include "storm/models/sparse/MarkovAutomaton.h" +#include "storm/models/sparse/StandardRewardModel.h" +#include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h" +#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" +#include "storm/storage/MaximalEndComponentDecomposition.h" +#include "storm/storage/memorystructure/MemoryStructureBuilder.h" +#include "storm/storage/memorystructure/SparseModelMemoryProduct.h" +#include "storm/storage/expressions/ExpressionManager.h" +#include "storm/transformer/SubsystemBuilder.h" +#include "storm/utility/macros.h" +#include "storm/utility/vector.h" +#include "storm/utility/graph.h" + +#include "storm/exceptions/InvalidPropertyException.h" +#include "storm/exceptions/UnexpectedException.h" +#include "storm/exceptions/NotImplementedException.h" + +namespace storm { + namespace modelchecker { + namespace multiobjective { + + template + typename SparseMultiObjectivePreprocessor::ReturnType SparseMultiObjectivePreprocessor::preprocess(SparseModelType const& originalModel, storm::logic::MultiObjectiveFormula const& originalFormula) { + + PreprocessorData data(originalModel); + + //Invoke preprocessing on the individual objectives + for (auto const& subFormula : originalFormula.getSubformulas()) { + STORM_LOG_INFO("Preprocessing objective " << *subFormula<< "."); + data.objectives.push_back(std::make_shared>()); + data.objectives.back()->originalFormula = subFormula; + data.finiteRewardCheckObjectives.resize(data.objectives.size(), false); + if (data.objectives.back()->originalFormula->isOperatorFormula()) { + preprocessOperatorFormula(data.objectives.back()->originalFormula->asOperatorFormula(), data); + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Could not preprocess the subformula " << *subFormula << " of " << originalFormula << " because it is not supported"); + } + } + + // Incorporate the required memory into the state space + storm::storage::SparseModelMemoryProduct product = data.memory->product(originalModel); + std::shared_ptr preprocessedModel = std::dynamic_pointer_cast(product.build()); + + auto backwardTransitions = preprocessedModel->getBackwardTransitions(); + + // compute the end components of the model (if required) + bool endComponentAnalysisRequired = false; + for (auto& task : data.tasks) { + endComponentAnalysisRequired = endComponentAnalysisRequired || task->requiresEndComponentAnalysis(); + } + if (endComponentAnalysisRequired) { + // TODO + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "End component analysis required but currently not implemented."); + } + + for (auto& task : data.tasks) { + task->perform(*preprocessedModel); + } + + // Build the actual result + return buildResult(originalModel, originalFormula, data, preprocessedModel, backwardTransitions); + } + + template + SparseMultiObjectivePreprocessor::PreprocessorData::PreprocessorData(SparseModelType const& model) : originalModel(model) { + storm::storage::MemoryStructureBuilder memoryBuilder(1); + memoryBuilder.setTransition(0,0, storm::logic::Formula::getTrueFormula()); + memory = std::make_shared(memoryBuilder.build()); + + // The memoryLabelPrefix should not be a prefix of a state label of the given model to ensure uniqueness of label names + memoryLabelPrefix = "mem"; + while (true) { + bool prefixIsUnique = true; + for (auto const& label : originalModel.getStateLabeling().getLabels()) { + if (memoryLabelPrefix.size() <= label.size()) { + if (std::mismatch(memoryLabelPrefix.begin(), memoryLabelPrefix.end(), label.begin()).first == memoryLabelPrefix.end()) { + prefixIsUnique = false; + memoryLabelPrefix = "_" + memoryLabelPrefix; + break; + } + } + } + if (prefixIsUnique) { + break; + } + } + + // The rewardModelNamePrefix should not be a prefix of a reward model name of the given model to ensure uniqueness of reward model names + rewardModelNamePrefix = "obj"; + while (true) { + bool prefixIsUnique = true; + for (auto const& label : originalModel.getStateLabeling().getLabels()) { + if (memoryLabelPrefix.size() <= label.size()) { + if (std::mismatch(memoryLabelPrefix.begin(), memoryLabelPrefix.end(), label.begin()).first == memoryLabelPrefix.end()) { + prefixIsUnique = false; + memoryLabelPrefix = "_" + memoryLabelPrefix; + break; + } + } + } + if (prefixIsUnique) { + break; + } + } + } + + template + void SparseMultiObjectivePreprocessor::preprocessOperatorFormula(storm::logic::OperatorFormula const& formula, PreprocessorData& data) { + + Objective& objective = *data.objectives.back(); + + objective.considersComplementaryEvent = false; + + if (formula.hasBound()) { + STORM_LOG_THROW(!formula.getBound().threshold.containsVariables(), storm::exceptions::InvalidPropertyException, "The formula " << formula << "considers a non-constant threshold"); + objective.bound = formula.getBound(); + if (storm::logic::isLowerBound(formula.getBound().comparisonType)) { + objective.optimizationDirection = storm::solver::OptimizationDirection::Maximize; + } else { + objective.optimizationDirection = storm::solver::OptimizationDirection::Minimize; + } + STORM_LOG_WARN_COND(!formula.hasOptimalityType() || formula.getOptimalityType() == objective.optimizationDirection, "Optimization direction of formula " << formula << " ignored as the formula also specifies a threshold."); + } else if (formula.hasOptimalityType()){ + objective.optimizationDirection = formula.getOptimalityType(); + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Current objective " << formula << " does not specify whether to minimize or maximize"); + } + + if (formula.isProbabilityOperatorFormula()){ + preprocessProbabilityOperatorFormula(formula.asProbabilityOperatorFormula(), data); + } else if (formula.isRewardOperatorFormula()){ + preprocessRewardOperatorFormula(formula.asRewardOperatorFormula(), data); + } else if (formula.isTimeOperatorFormula()){ + preprocessTimeOperatorFormula(formula.asTimeOperatorFormula(), data); + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Could not preprocess the objective " << formula << " because it is not supported"); + } + + // Invert the bound and optimization direction (if necessary) + if (objective.considersComplementaryEvent) { + if (objective.bound) { + objective.bound->threshold = objective.bound->threshold.getManager().rational(storm::utility::one()) - objective.bound->threshold; + switch (objective.bound->comparisonType) { + case storm::logic::ComparisonType::Greater: + objective.bound->comparisonType = storm::logic::ComparisonType::Less; + break; + case storm::logic::ComparisonType::GreaterEqual: + objective.bound->comparisonType = storm::logic::ComparisonType::LessEqual; + break; + case storm::logic::ComparisonType::Less: + objective.bound->comparisonType = storm::logic::ComparisonType::Greater; + break; + case storm::logic::ComparisonType::LessEqual: + objective.bound->comparisonType = storm::logic::ComparisonType::GreaterEqual; + break; + default: + STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Current objective " << formula << " has unexpected comparison type"); + } + } + objective.optimizationDirection = storm::solver::invert(objective.optimizationDirection); + } + } + + template + void SparseMultiObjectivePreprocessor::preprocessProbabilityOperatorFormula(storm::logic::ProbabilityOperatorFormula const& formula, PreprocessorData& data) { + + // Probabilities are between zero and one + data.objectives.back()->lowerResultBound = storm::utility::zero(); + data.objectives.back()->upperResultBound = storm::utility::one(); + + if (formula.getSubformula().isUntilFormula()){ + preprocessUntilFormula(formula.getSubformula().asUntilFormula(), data); + } else if (formula.getSubformula().isBoundedUntilFormula()){ + preprocessBoundedUntilFormula(formula.getSubformula().asBoundedUntilFormula(), data); + } else if (formula.getSubformula().isGloballyFormula()){ + preprocessGloballyFormula(formula.getSubformula().asGloballyFormula(), data); + } else if (formula.getSubformula().isEventuallyFormula()){ + preprocessEventuallyFormula(formula.getSubformula().asEventuallyFormula(), data); + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The subformula of " << formula << " is not supported."); + } + } + + template + void SparseMultiObjectivePreprocessor::preprocessRewardOperatorFormula(storm::logic::RewardOperatorFormula const& formula, PreprocessorData& data) { + + STORM_LOG_THROW((formula.hasRewardModelName() && data.originalModel.hasRewardModel(formula.getRewardModelName())) + || (!formula.hasRewardModelName() && data.originalModel.hasUniqueRewardModel()), storm::exceptions::InvalidPropertyException, "The reward model is not unique or the formula " << formula << " does not specify an existing reward model."); + + std::string rewardModelName; + if (formula.hasRewardModelName()) { + rewardModelName = formula.getRewardModelName(); + STORM_LOG_THROW(data.originalModel.hasRewardModel(rewardModelName), storm::exceptions::InvalidPropertyException, "The reward model specified by formula " << formula << " does not exist in the model"); + } else { + STORM_LOG_THROW(data.originalModel.hasUniqueRewardModel(), storm::exceptions::InvalidOperationException, "The formula " << formula << " does not specify a reward model name and the reward model is not unique."); + rewardModelName = data.originalModel.getRewardModels().begin()->first; + } + + data.objectives.back()->lowerResultBound = storm::utility::zero(); + + if (formula.getSubformula().isEventuallyFormula()){ + preprocessEventuallyFormula(formula.getSubformula().asEventuallyFormula(), data, rewardModelName); + } else if (formula.getSubformula().isCumulativeRewardFormula()) { + preprocessCumulativeRewardFormula(formula.getSubformula().asCumulativeRewardFormula(), data, rewardModelName); + } else if (formula.getSubformula().isTotalRewardFormula()) { + preprocessTotalRewardFormula(data, rewardModelName); + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The subformula of " << formula << " is not supported."); + } + } + + template + void SparseMultiObjectivePreprocessor::preprocessTimeOperatorFormula(storm::logic::TimeOperatorFormula const& formula, PreprocessorData& data) { + // 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."); + + data.objectives.back()->lowerResultBound = storm::utility::zero(); + + if (formula.getSubformula().isEventuallyFormula()){ + preprocessEventuallyFormula(formula.getSubformula().asEventuallyFormula(), data); + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The subformula of " << formula << " is not supported."); + } + } + + template + void SparseMultiObjectivePreprocessor::preprocessUntilFormula(storm::logic::UntilFormula const& formula, PreprocessorData& data) { + + // Check if the formula is already satisfied in the initial state because then the transformation to expected rewards will fail. + if (!data.objectives.back()->lowerTimeBound) { + storm::modelchecker::SparsePropositionalModelChecker mc(data.originalModel); + if (!(data.originalModel.getInitialStates() & mc.check(formula.getRightSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector()).empty()) { + // TODO: Handle this case more properly + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "The Probability for the objective " << *data.objectives.back()->originalFormula << " is always one as the rhs of the until formula is true in the initial state. This (trivial) case is currently not implemented."); + } + } + + // Create a memory structure that stores whether a non-PhiState or a PsiState has already been reached + storm::storage::MemoryStructureBuilder builder(2); + std::string relevantStatesLabel = data.memoryLabelPrefix + "_obj" + std::to_string(data.objectives.size()) + "_relevant"; + builder.setLabel(0, relevantStatesLabel); + auto negatedLeftSubFormula = std::make_shared(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, formula.getLeftSubformula().asSharedPointer()); + auto targetFormula = std::make_shared(storm::logic::BinaryBooleanStateFormula::OperatorType::Or, negatedLeftSubFormula, formula.getRightSubformula().asSharedPointer()); + builder.setTransition(0, 0, std::make_shared(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, targetFormula)); + builder.setTransition(0, 1, targetFormula); + builder.setTransition(1, 1, storm::logic::Formula::getTrueFormula()); + storm::storage::MemoryStructure objectiveMemory = builder.build(); + data.memory = std::make_shared(data.memory->product(objectiveMemory)); + + data.objectives.back()->rewardModelName = data.rewardModelNamePrefix + std::to_string(data.objectives.size()); + + auto relevantStatesFormula = std::make_shared(relevantStatesLabel); + data.tasks.push_back(std::make_shared>(data.objectives.back(), relevantStatesFormula, formula.getRightSubformula().asSharedPointer())); + + } + + template + void SparseMultiObjectivePreprocessor::preprocessBoundedUntilFormula(storm::logic::BoundedUntilFormula const& formula, PreprocessorData& data) { + STORM_LOG_THROW(!data.originalModel.isOfType(storm::models::ModelType::MarkovAutomaton) || !formula.isStepBounded(), storm::exceptions::InvalidPropertyException, "Multi-objective model checking currently does not support STEP-bounded properties for Markov automata."); + + if (formula.hasLowerBound()) { + STORM_LOG_THROW(!formula.getLowerBound().containsVariables(), storm::exceptions::InvalidPropertyException, "The lower time bound for the formula " << formula << " still contains variables"); + if (!storm::utility::isZero(formula.getLowerBound()) || formula.isLowerBoundStrict()) { + data.objectives.back()->lowerTimeBound = storm::logic::TimeBound(formula.isLowerBoundStrict(), formula.getLowerBound()); + } + } + if (formula.hasUpperBound()) { + STORM_LOG_THROW(!formula.getUpperBound().containsVariables(), storm::exceptions::InvalidPropertyException, "The Upper time bound for the formula " << formula << " still contains variables"); + if (!storm::utility::isInfinity(formula.getUpperBound())) { + data.objectives.back()->upperTimeBound = storm::logic::TimeBound(formula.isUpperBoundStrict(), formula.getUpperBound()); + } + } + preprocessUntilFormula(storm::logic::UntilFormula(formula.getLeftSubformula().asSharedPointer(), formula.getRightSubformula().asSharedPointer()), data); + } + + template + void SparseMultiObjectivePreprocessor::preprocessGloballyFormula(storm::logic::GloballyFormula const& formula, PreprocessorData& data) { + // The formula will be transformed to an until formula for the complementary event. + data.objectives.back()->considersComplementaryEvent = true; + + auto negatedSubformula = std::make_shared(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, formula.getSubformula().asSharedPointer()); + + preprocessUntilFormula(storm::logic::UntilFormula(storm::logic::Formula::getTrueFormula(), negatedSubformula), data); + } + + template + void SparseMultiObjectivePreprocessor::preprocessEventuallyFormula(storm::logic::EventuallyFormula const& formula, PreprocessorData& data, boost::optional const& optionalRewardModelName) { + if (formula.isReachabilityProbabilityFormula()){ + preprocessUntilFormula(storm::logic::UntilFormula(storm::logic::Formula::getTrueFormula(), formula.getSubformula().asSharedPointer()), data); + return; + } + + // Create a memory structure that stores whether a target state has already been reached + storm::storage::MemoryStructureBuilder builder(2); + // Get a unique label that is not already present in the model + std::string relevantStatesLabel = data.memoryLabelPrefix + "_obj" + std::to_string(data.objectives.size()) + "_relevant"; + builder.setLabel(0, relevantStatesLabel); + builder.setTransition(0, 0, std::make_shared(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, formula.getSubformula().asSharedPointer())); + builder.setTransition(0, 1, formula.getSubformula().asSharedPointer()); + builder.setTransition(1, 1, std::make_shared(true)); + storm::storage::MemoryStructure objectiveMemory = builder.build(); + data.memory = std::make_shared(data.memory->product(objectiveMemory)); + + auto relevantStatesFormula = std::make_shared(relevantStatesLabel); + + data.objectives.back()->rewardModelName = data.rewardModelNamePrefix + std::to_string(data.objectives.size()); + data.finiteRewardCheckObjectives.set(data.objectives.size() - 1, true); + + if (formula.isReachabilityRewardFormula()) { + assert(optionalRewardModelName.is_initialized()); + data.tasks.push_back(std::make_shared>(data.objectives.back(), relevantStatesFormula, optionalRewardModelName.get())); + data.finiteRewardCheckObjectives.set(data.objectives.size() - 1); + } else if (formula.isReachabilityTimeFormula() && data.originalModel.isOfType(storm::models::ModelType::MarkovAutomaton)) { + data.finiteRewardCheckObjectives.set(data.objectives.size() - 1); + data.tasks.push_back(std::make_shared>(data.objectives.back(), relevantStatesFormula)); + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The formula " << formula << " neither considers reachability probabilities nor reachability rewards " << (data.originalModel.isOfType(storm::models::ModelType::MarkovAutomaton) ? "nor reachability time" : "") << ". This is not supported."); + } + } + + template + void SparseMultiObjectivePreprocessor::preprocessCumulativeRewardFormula(storm::logic::CumulativeRewardFormula const& formula, PreprocessorData& data, boost::optional const& optionalRewardModelName) { + STORM_LOG_THROW(data.originalModel.isOfType(storm::models::ModelType::Mdp), storm::exceptions::InvalidPropertyException, "Cumulative reward formulas are not supported for the given model type."); + + STORM_LOG_THROW(!formula.getBound().containsVariables(), storm::exceptions::InvalidPropertyException, "The time bound for the formula " << formula << " still contains variables"); + if (!storm::utility::isInfinity(formula.getBound())) { + data.objectives.back()->upperTimeBound = storm::logic::TimeBound(formula.isBoundStrict(), formula.getBound()); + } + + assert(optionalRewardModelName.is_initialized()); + data.objectives.back()->rewardModelName = *optionalRewardModelName; + + } + + template + void SparseMultiObjectivePreprocessor::preprocessTotalRewardFormula(PreprocessorData& data, boost::optional const& optionalRewardModelName) { + assert(optionalRewardModelName.is_initialized()); + data.objectives.back()->rewardModelName = *optionalRewardModelName; + data.finiteRewardCheckObjectives.set(data.objectives.size() - 1, true); + } + + template + typename SparseMultiObjectivePreprocessor::ReturnType SparseMultiObjectivePreprocessor::buildResult(SparseModelType const& originalModel, storm::logic::MultiObjectiveFormula const& originalFormula, PreprocessorData& data, std::shared_ptr const& preprocessedModel, storm::storage::SparseMatrix const& backwardTransitions) { + + ReturnType result(originalFormula, originalModel); + + result.preprocessedModel = preprocessedModel; + + for (auto& obj : data.objectives) { + result.objectives.push_back(std::move(*obj)); + } + + result.queryType = getQueryType(result.objectives); + + auto minMaxNonZeroRewardStates = getStatesWithNonZeroRewardMinMax(result, backwardTransitions); + auto finiteRewardStates = ensureRewardFiniteness(result, data.finiteRewardCheckObjectives, minMaxNonZeroRewardStates.first, backwardTransitions); + + std::set relevantRewardModels; + for (auto const& obj : result.objectives) { + relevantRewardModels.insert(*obj.rewardModelName); + } + + // Build a subsystem that discards states that yield infinite reward for all schedulers. + // We can also merge the states that will have reward zero anyway. + storm::storage::BitVector zeroRewardStates = ~minMaxNonZeroRewardStates.second; + storm::storage::BitVector maybeStates = finiteRewardStates & ~zeroRewardStates; + storm::transformer::GoalStateMerger merger(*result.preprocessedModel); + typename storm::transformer::GoalStateMerger::ReturnType mergerResult = merger.mergeTargetAndSinkStates(maybeStates, zeroRewardStates, storm::storage::BitVector(maybeStates.size(), false), std::vector(relevantRewardModels.begin(), relevantRewardModels.end())); + + result.preprocessedModel = mergerResult.model; + result.possibleBottomStates = (~minMaxNonZeroRewardStates.first) % maybeStates; + if (mergerResult.targetState) { + storm::storage::BitVector targetStateAsVector(result.preprocessedModel->getNumberOfStates(), false); + targetStateAsVector.set(*mergerResult.targetState, true); + // The overapproximation for the possible ec choices consists of the states that can reach the target states with prob. 0 and the target state itself. + result.possibleECChoices = result.preprocessedModel->getTransitionMatrix().getRowFilter(storm::utility::graph::performProb0E(*result.preprocessedModel, result.preprocessedModel->getBackwardTransitions(), storm::storage::BitVector(targetStateAsVector.size(), true), targetStateAsVector)); + result.possibleECChoices.set(result.preprocessedModel->getTransitionMatrix().getRowGroupIndices()[*mergerResult.targetState], true); + // There is an additional state in the result + result.possibleBottomStates.resize(result.possibleBottomStates.size() + 1, true); + } else { + result.possibleECChoices = storm::storage::BitVector(result.preprocessedModel->getNumberOfChoices(), true); + } + assert(result.possibleBottomStates.size() == result.preprocessedModel->getNumberOfStates()); + + return result; + } + + template + typename SparseMultiObjectivePreprocessor::ReturnType::QueryType SparseMultiObjectivePreprocessor::getQueryType(std::vector> const& objectives) { + uint_fast64_t numOfObjectivesWithThreshold = 0; + for (auto& obj : objectives) { + if (obj.bound) { + ++numOfObjectivesWithThreshold; + } + } + if (numOfObjectivesWithThreshold == objectives.size()) { + return ReturnType::QueryType::Achievability; + } else if (numOfObjectivesWithThreshold + 1 == objectives.size()) { + // Note: We do not want to consider a Pareto query when the total number of objectives is one. + return ReturnType::QueryType::Quantitative; + } else if (numOfObjectivesWithThreshold == 0) { + return ReturnType::QueryType::Pareto; + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Invalid Multi-objective query: The numer of qualitative objectives should be either 0 (Pareto query), 1 (quantitative query), or #objectives (achievability query)."); + } + } + + template + std::pair SparseMultiObjectivePreprocessor::getStatesWithNonZeroRewardMinMax(ReturnType& result, storm::storage::SparseMatrix const& backwardTransitions) { + + uint_fast64_t stateCount = result.preprocessedModel->getNumberOfStates(); + auto const& transitions = result.preprocessedModel->getTransitionMatrix(); + std::vector const& groupIndices = transitions.getRowGroupIndices(); + storm::storage::BitVector allStates(stateCount, true); + + // Get the choices that yield non-zero reward + storm::storage::BitVector zeroRewardChoices(result.preprocessedModel->getNumberOfChoices(), true); + for (auto const& obj : result.objectives) { + auto const& rewModel = result.preprocessedModel->getRewardModel(*obj.rewardModelName); + zeroRewardChoices &= rewModel.getChoicesWithZeroReward(transitions); + } + + // Get the states that have reward for at least one (or for all) choices assigned to it. + storm::storage::BitVector statesWithRewardForOneChoice = storm::storage::BitVector(stateCount, false); + storm::storage::BitVector statesWithRewardForAllChoices = storm::storage::BitVector(stateCount, true); + for (uint_fast64_t state = 0; state < stateCount; ++state) { + bool stateHasChoiceWithReward = false; + bool stateHasChoiceWithoutReward = false; + uint_fast64_t const& groupEnd = groupIndices[state + 1]; + for (uint_fast64_t choice = groupIndices[state]; choice < groupEnd; ++choice) { + if (zeroRewardChoices.get(choice)) { + stateHasChoiceWithoutReward = true; + } else { + stateHasChoiceWithReward = true; + } + } + if (stateHasChoiceWithReward) { + statesWithRewardForOneChoice.set(state, true); + } + if (stateHasChoiceWithoutReward) { + statesWithRewardForAllChoices.set(state, false); + } + } + + // get the states from which the minimal/maximal expected reward is always non-zero + storm::storage::BitVector minStates = storm::utility::graph::performProbGreater0A(transitions, groupIndices, backwardTransitions, allStates, statesWithRewardForAllChoices, false, 0, zeroRewardChoices); + storm::storage::BitVector maxStates = storm::utility::graph::performProbGreater0E(backwardTransitions, allStates, statesWithRewardForOneChoice); + STORM_LOG_ASSERT(minStates.isSubsetOf(maxStates), "The computed set of states with minimal non-zero expected rewards is not a subset of the states with maximal non-zero rewards."); + return std::make_pair(std::move(minStates), std::move(maxStates)); + } + + template + storm::storage::BitVector SparseMultiObjectivePreprocessor::ensureRewardFiniteness(ReturnType& result, storm::storage::BitVector const& finiteRewardCheckObjectives, storm::storage::BitVector const& nonZeroRewardMin, storm::storage::SparseMatrix const& backwardTransitions) { + + auto const& transitions = result.preprocessedModel->getTransitionMatrix(); + std::vector const& groupIndices = transitions.getRowGroupIndices(); + + storm::storage::BitVector maxRewardsToCheck(result.preprocessedModel->getNumberOfChoices(), true); + bool hasMinRewardToCheck = false; + for (auto const& objIndex : finiteRewardCheckObjectives) { + auto const& rewModel = result.preprocessedModel->getRewardModel(result.objectives[objIndex].rewardModelName.get()); + if (storm::solver::minimize(result.objectives[objIndex].optimizationDirection)) { + hasMinRewardToCheck = true; + } else { + maxRewardsToCheck &= rewModel.getChoicesWithZeroReward(transitions); + } + } + maxRewardsToCheck.complement(); + + // Assert reward finitiness for maximizing objectives under all schedulers + storm::storage::BitVector allStates(result.preprocessedModel->getNumberOfStates(), true); + if (storm::utility::graph::checkIfECWithChoiceExists(transitions, backwardTransitions, allStates, maxRewardsToCheck)) { + STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "At least one of the maximizing objectives induces infinite expected reward (or time). This is not supported"); + } + + // Assert that there is one scheduler under which all rewards are finite. + // This only has to be done if there are minimizing expected rewards that potentially can be infinite + storm::storage::BitVector finiteRewardStates; + if (hasMinRewardToCheck) { + finiteRewardStates = storm::utility::graph::performProb1E(transitions, groupIndices, backwardTransitions, allStates, ~nonZeroRewardMin); + if ((finiteRewardStates & result.preprocessedModel->getInitialStates()).empty()) { + // There is no scheduler that induces finite reward for the initial state + STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "For every scheduler, at least one objective gets infinite reward."); + } + } else { + finiteRewardStates = allStates; + } + return finiteRewardStates; + } + + template class SparseMultiObjectivePreprocessor>; + template class SparseMultiObjectivePreprocessor>; + + template class SparseMultiObjectivePreprocessor>; + template class SparseMultiObjectivePreprocessor>; + } + } +} diff --git a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.h b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.h new file mode 100644 index 000000000..318433575 --- /dev/null +++ b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.h @@ -0,0 +1,95 @@ +#pragma once + +#include +#include + +#include "storm/logic/Formulas.h" +#include "storm/storage/BitVector.h" +#include "storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorReturnType.h" +#include "storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorTask.h" +#include "storm/storage/memorystructure/MemoryStructure.h" + +namespace storm { + namespace modelchecker { + namespace multiobjective { + + /* + * This class invokes the necessary preprocessing for the constraint based multi-objective model checking algorithm + */ + template + class SparseMultiObjectivePreprocessor { + public: + typedef typename SparseModelType::ValueType ValueType; + typedef typename SparseModelType::RewardModelType RewardModelType; + typedef SparseMultiObjectivePreprocessorReturnType ReturnType; + + /*! + * 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. + */ + static ReturnType preprocess(SparseModelType const& originalModel, storm::logic::MultiObjectiveFormula const& originalFormula); + + private: + + struct PreprocessorData { + SparseModelType const& originalModel; + std::vector>> objectives; + std::vector>> tasks; + std::shared_ptr memory; + + // Indices of the objectives that require a check for finite reward + storm::storage::BitVector finiteRewardCheckObjectives; + + std::string memoryLabelPrefix; + std::string rewardModelNamePrefix; + + PreprocessorData(SparseModelType const& model); + }; + + /*! + * Apply the neccessary preprocessing for the given formula. + * @param formula the current (sub)formula + * @param data the current data. The currently processed objective is located at data.objectives.back() + * @param optionalRewardModelName the reward model name that is considered for the formula (if available) + */ + static void preprocessOperatorFormula(storm::logic::OperatorFormula const& formula, PreprocessorData& data); + static void preprocessProbabilityOperatorFormula(storm::logic::ProbabilityOperatorFormula const& formula, PreprocessorData& data); + static void preprocessRewardOperatorFormula(storm::logic::RewardOperatorFormula const& formula, PreprocessorData& data); + static void preprocessTimeOperatorFormula(storm::logic::TimeOperatorFormula const& formula, PreprocessorData& data); + static void preprocessUntilFormula(storm::logic::UntilFormula const& formula, PreprocessorData& data); + static void preprocessBoundedUntilFormula(storm::logic::BoundedUntilFormula const& formula, PreprocessorData& data); + static void preprocessGloballyFormula(storm::logic::GloballyFormula const& formula, PreprocessorData& data); + static void preprocessEventuallyFormula(storm::logic::EventuallyFormula const& formula, PreprocessorData& data, boost::optional const& optionalRewardModelName = boost::none); + static void preprocessCumulativeRewardFormula(storm::logic::CumulativeRewardFormula const& formula, PreprocessorData& data, boost::optional const& optionalRewardModelName = boost::none); + static void preprocessTotalRewardFormula(PreprocessorData& data, boost::optional const& optionalRewardModelName = boost::none); // The total reward formula itself does not need to be provided as it is unique. + + + /*! + * Builds the result from preprocessing + */ + static ReturnType buildResult(SparseModelType const& originalModel, storm::logic::MultiObjectiveFormula const& originalFormula, PreprocessorData& data, std::shared_ptr const& preprocessedModel, storm::storage::SparseMatrix const& backwardTransitions); + + /*! + * Returns the query type + */ + static typename ReturnType::QueryType getQueryType(std::vector> const& objectives); + + + /*! + * Computes the set of states that have a non-zero reward w.r.t. all objectives, assuming that the objectives are all minimizing and maximizing, respectively. + */ + static std::pair getStatesWithNonZeroRewardMinMax(ReturnType& result, storm::storage::SparseMatrix const& backwardTransitions); + + + /*! + * Checks whether the occurring expected rewards are finite. If not, the input is rejected. + * Returns the set of states for which a scheduler exists that induces finite reward for all objectives + */ + static storm::storage::BitVector ensureRewardFiniteness(ReturnType& result, storm::storage::BitVector const& finiteRewardCheckObjectives, storm::storage::BitVector const& nonZeroRewardMin, storm::storage::SparseMatrix const& backwardTransitions); + + }; + } + } +} + diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessorReturnType.h b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorReturnType.h similarity index 54% rename from src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessorReturnType.h rename to src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorReturnType.h index 8237da3c0..8143447ed 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessorReturnType.h +++ b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorReturnType.h @@ -1,18 +1,12 @@ -#ifndef STORM_MODELCHECKER_MULTIOBJECTIVE_PCAA_SPARSEPCAAPREPROCESSORRETURNTYPE_H_ -#define STORM_MODELCHECKER_MULTIOBJECTIVE_PCAA_SPARSEPCAAPREPROCESSORRETURNTYPE_H_ +#pragma once #include #include -#include -#include #include #include "storm/logic/Formulas.h" -#include "storm/modelchecker/multiobjective/pcaa/PcaaObjective.h" -#include "storm/models/sparse/MarkovAutomaton.h" +#include "storm/modelchecker/multiobjective/Objective.h" #include "storm/storage/BitVector.h" -#include "storm/utility/macros.h" -#include "storm/utility/constants.h" #include "storm/exceptions/UnexpectedException.h" @@ -21,36 +15,24 @@ namespace storm { namespace multiobjective { template - struct SparsePcaaPreprocessorReturnType { + struct SparseMultiObjectivePreprocessorReturnType { enum class QueryType { Achievability, Quantitative, Pareto }; storm::logic::MultiObjectiveFormula const& originalFormula; SparseModelType const& originalModel; - SparseModelType preprocessedModel; + std::shared_ptr preprocessedModel; QueryType queryType; // The (preprocessed) objectives - std::vector> objectives; + std::vector> objectives; - // The index of the objective that is to be maximized (or minimized) in case of a quantitative Query - boost::optional indexOfOptimizingObjective; - - // Maps any state of the preprocessed model to the corresponding state of the original Model - std::vector newToOldStateIndexMapping; - - // The actions of the preprocessed model that have positive reward assigned for at least one objective (objectives with an upper time-bound are ignored!) - storm::storage::BitVector actionsWithPositiveReward; - // The actions of the preprocessed model that have negative reward assigned for at least one objective (objectives with an upper time-bound are ignored!) - storm::storage::BitVector actionsWithNegativeReward; - // The actions of the preprocessed model that are part of an EC - storm::storage::BitVector ecActions; - - // The set of states of the preprocessed model for which there is a scheduler such that - // the state is visited infinitely often and the induced reward is finite for all objectives - storm::storage::BitVector possiblyRecurrentStates; + // The states for which there is a scheduler such that all objectives have value zero + storm::storage::BitVector possibleBottomStates; + // Overapproximation of the set of choices that are part of an end component. + storm::storage::BitVector possibleECChoices; - SparsePcaaPreprocessorReturnType(storm::logic::MultiObjectiveFormula const& originalFormula, SparseModelType const& originalModel, SparseModelType&& preprocessedModel) : originalFormula(originalFormula), originalModel(originalModel), preprocessedModel(preprocessedModel) { + SparseMultiObjectivePreprocessorReturnType(storm::logic::MultiObjectiveFormula const& originalFormula, SparseModelType const& originalModel) : originalFormula(originalFormula), originalModel(originalModel) { // Intentionally left empty } @@ -75,12 +57,12 @@ namespace storm { originalModel.printModelInformationToStream(out); out << std::endl; out << "Preprocessed Model Information:" << std::endl; - preprocessedModel.printModelInformationToStream(out); + preprocessedModel->printModelInformationToStream(out); out << std::endl; out << "---------------------------------------------------------------------------------------------------------------------------------------" << std::endl; } - friend std::ostream& operator<<(std::ostream& out, SparsePcaaPreprocessorReturnType const& ret) { + friend std::ostream& operator<<(std::ostream& out, SparseMultiObjectivePreprocessorReturnType const& ret) { ret.printToStream(out); return out; } @@ -90,4 +72,3 @@ namespace storm { } } -#endif /* STORM_MODELCHECKER_MULTIOBJECTIVE_PCAA_SPARSEPCAAPREPROCESSORRETURNTYPE_H_ */ diff --git a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorTask.h b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorTask.h new file mode 100644 index 000000000..e34e37584 --- /dev/null +++ b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorTask.h @@ -0,0 +1,131 @@ +#pragma once + +#include +#include + +#include "storm/logic/Formula.h" +#include "storm/logic/Bound.h" +#include "storm/solver/OptimizationDirection.h" +#include "storm/modelchecker/multiobjective/Objective.h" +#include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h" +#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" +#include "storm/models/sparse/Mdp.h" +#include "storm/models/sparse/MarkovAutomaton.h" +#include "storm/models/sparse/StandardRewardModel.h" +#include "storm/utility/vector.h" + +namespace storm { + namespace modelchecker { + namespace multiobjective { + + template + class SparseMultiObjectivePreprocessorTask { + public: + SparseMultiObjectivePreprocessorTask(std::shared_ptr> const& objective) : objective(objective) { + // intentionally left empty + } + + virtual void perform(SparseModelType& preprocessedModel) const = 0; + + virtual bool requiresEndComponentAnalysis() const { + return false; + } + + + protected: + std::shared_ptr> objective; + }; + + // Transforms reachability probabilities to total expected rewards by adding a rewardModel + // such that one reward is given whenever a goal state is reached from a relevant state + template + class SparseMultiObjectivePreprocessorReachProbToTotalRewTask : public SparseMultiObjectivePreprocessorTask { + public: + SparseMultiObjectivePreprocessorReachProbToTotalRewTask(std::shared_ptr> const& objective, std::shared_ptr const& relevantStateFormula, std::shared_ptr const& goalStateFormula) : SparseMultiObjectivePreprocessorTask(objective), relevantStateFormula(relevantStateFormula), goalStateFormula(goalStateFormula) { + // Intentionally left empty + } + + virtual void perform(SparseModelType& preprocessedModel) const override { + + // build stateAction reward vector that gives (one*transitionProbability) reward whenever a transition leads from a relevantState to a goalState + storm::modelchecker::SparsePropositionalModelChecker mc(preprocessedModel); + storm::storage::BitVector relevantStates = mc.check(*relevantStateFormula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); + storm::storage::BitVector goalStates = mc.check(*goalStateFormula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); + + std::vector objectiveRewards(preprocessedModel.getTransitionMatrix().getRowCount(), storm::utility::zero()); + for (auto const& state : relevantStates) { + for (uint_fast64_t row = preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state]; row < preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state + 1]; ++row) { + objectiveRewards[row] = preprocessedModel.getTransitionMatrix().getConstrainedRowSum(row, goalStates); + } + } + STORM_LOG_ASSERT(this->objective->rewardModelName.is_initialized(), "No reward model name has been specified"); + preprocessedModel.addRewardModel(this->objective->rewardModelName.get(), typename SparseModelType::RewardModelType(boost::none, std::move(objectiveRewards))); + } + + private: + std::shared_ptr relevantStateFormula; + std::shared_ptr goalStateFormula; + }; + + // Transforms expected reachability rewards to total expected rewards by adding a rewardModel + // such that non-relevant states get reward zero + template + class SparseMultiObjectivePreprocessorReachRewToTotalRewTask : public SparseMultiObjectivePreprocessorTask { + public: + SparseMultiObjectivePreprocessorReachRewToTotalRewTask(std::shared_ptr> const& objective, std::shared_ptr const& relevantStateFormula, std::string const& originalRewardModelName) : SparseMultiObjectivePreprocessorTask(objective), relevantStateFormula(relevantStateFormula), originalRewardModelName(originalRewardModelName) { + // Intentionally left empty + } + + virtual void perform(SparseModelType& preprocessedModel) const override { + + // build stateAction reward vector that only gives reward for relevant states + storm::modelchecker::SparsePropositionalModelChecker mc(preprocessedModel); + storm::storage::BitVector nonRelevantStates = ~mc.check(*relevantStateFormula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); + typename SparseModelType::RewardModelType objectiveRewards = preprocessedModel.getRewardModel(originalRewardModelName); + objectiveRewards.reduceToStateBasedRewards(preprocessedModel.getTransitionMatrix(), false); + if (objectiveRewards.hasStateRewards()) { + storm::utility::vector::setVectorValues(objectiveRewards.getStateRewardVector(), nonRelevantStates, storm::utility::zero()); + } + if (objectiveRewards.hasStateActionRewards()) { + for (auto state : nonRelevantStates) { + std::fill_n(objectiveRewards.getStateActionRewardVector().begin() + preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state], preprocessedModel.getTransitionMatrix().getRowGroupSize(state), storm::utility::zero()); + } + } + STORM_LOG_ASSERT(this->objective->rewardModelName.is_initialized(), "No reward model name has been specified"); + preprocessedModel.addRewardModel(this->objective->rewardModelName.get(), std::move(objectiveRewards)); + } + + private: + std::shared_ptr relevantStateFormula; + std::string originalRewardModelName; + }; + + // Transforms expected reachability time to total expected rewards by adding a rewardModel + // such that every time step done from a relevant state yields one reward + template + class SparseMultiObjectivePreprocessorReachTimeToTotalRewTask : public SparseMultiObjectivePreprocessorTask { + public: + SparseMultiObjectivePreprocessorReachTimeToTotalRewTask(std::shared_ptr> const& objective, std::shared_ptr const& relevantStateFormula) : SparseMultiObjectivePreprocessorTask(objective), relevantStateFormula(relevantStateFormula) { + // Intentionally left empty + } + + virtual void perform(SparseModelType& preprocessedModel) const override { + + // build stateAction reward vector that only gives reward for relevant states + storm::modelchecker::SparsePropositionalModelChecker mc(preprocessedModel); + storm::storage::BitVector relevantStates = mc.check(*relevantStateFormula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); + + std::vector timeRewards(preprocessedModel.getNumberOfStates(), storm::utility::zero()); + storm::utility::vector::setVectorValues(timeRewards, dynamic_cast const&>(preprocessedModel).getMarkovianStates() & relevantStates, storm::utility::one()); + STORM_LOG_ASSERT(this->objective->rewardModelName.is_initialized(), "No reward model name has been specified"); + preprocessedModel.addRewardModel(this->objective->rewardModelName.get(), typename SparseModelType::RewardModelType(std::move(timeRewards))); + } + + private: + std::shared_ptr relevantStateFormula; + }; + + } + } +} + diff --git a/src/storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.cpp b/src/storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.cpp new file mode 100644 index 000000000..24b67bc03 --- /dev/null +++ b/src/storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.cpp @@ -0,0 +1,218 @@ +#include "storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.h" + +#include "storm/adapters/CarlAdapter.h" +#include "storm/models/sparse/Mdp.h" +#include "storm/models/sparse/MarkovAutomaton.h" +#include "storm/models/sparse/StandardRewardModel.h" +#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" +#include "storm/utility/constants.h" +#include "storm/utility/vector.h" +#include "storm/utility/solver.h" +#include "storm/utility/Stopwatch.h" +#include "storm/settings/SettingsManager.h" +#include "storm/settings/modules/GeneralSettings.h" +#include "storm/settings/modules/CoreSettings.h" +#include "storm/settings/modules/MultiObjectiveSettings.h" +#include "storm/storage/expressions/Expressions.h" + +#include "storm/exceptions/InvalidOperationException.h" +#include "storm/exceptions/NotSupportedException.h" +#include "storm/exceptions/UnexpectedException.h" + +namespace storm { + namespace modelchecker { + namespace multiobjective { + + + template + SparseCbAchievabilityQuery::SparseCbAchievabilityQuery(SparseMultiObjectivePreprocessorReturnType& preprocessorResult) : SparseCbQuery(preprocessorResult) { + STORM_LOG_ASSERT(preprocessorResult.queryType==SparseMultiObjectivePreprocessorReturnType::QueryType::Achievability, "Invalid query Type"); + solver = storm::utility::solver::SmtSolverFactory().create(*this->expressionManager); + } + + template + std::unique_ptr SparseCbAchievabilityQuery::check() { + + bool result = this->checkAchievability(); + + return std::unique_ptr(new ExplicitQualitativeCheckResult(this->originalModel.getInitialStates().getNextSetIndex(0), result)); + + } + + template + bool SparseCbAchievabilityQuery::checkAchievability() { + STORM_LOG_INFO("Building constraint system to check achievability."); + //this->preprocessedModel.writeDotToStream(std::cout); + storm::utility::Stopwatch swInitialization(true); + initializeConstraintSystem(); + STORM_LOG_INFO("Constraint system consists of " << expectedChoiceVariables.size() << " + " << bottomStateVariables.size() << " variables"); + addObjectiveConstraints(); + swInitialization.stop(); + + storm::utility::Stopwatch swCheck(true); + STORM_LOG_INFO("Invoking SMT Solver."); + storm::solver::SmtSolver::CheckResult result = solver->check(); + swCheck.stop(); + + if (storm::settings::getModule().isShowStatisticsSet()) { + STORM_PRINT_AND_LOG("Building the constraintsystem took " << swInitialization << " seconds and checking the SMT formula took " << swCheck << " seconds." << std::endl); + } + + switch(result) { + case storm::solver::SmtSolver::CheckResult::Sat: + // std::cout << std::endl << "Satisfying assignment: " << std::endl << solver->getModelAsValuation().toString(true) << std::endl; + return true; + case storm::solver::SmtSolver::CheckResult::Unsat: + // std::cout << std::endl << "Unsatisfiability core: {" << std::endl; + // for (auto const& expr : solver->getUnsatCore()) { + // std::cout << "\t " << expr << std::endl; + // } + // std::cout << "}" << std::endl; + return false; + default: + STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "SMT solver yielded an unexpected result"); + } + + return false; + } + + template + void SparseCbAchievabilityQuery::initializeConstraintSystem() { + uint_fast64_t numStates = this->preprocessedModel.getNumberOfStates(); + uint_fast64_t numChoices = this->preprocessedModel.getNumberOfChoices(); + uint_fast64_t numBottomStates = this->possibleBottomStates.getNumberOfSetBits(); + + storm::expressions::Expression zero = this->expressionManager->rational(storm::utility::zero()); + storm::expressions::Expression one = this->expressionManager->rational(storm::utility::one()); + + // Declare the variables for the choices and bottom states + expectedChoiceVariables.reserve(numChoices); + for (uint_fast64_t choice = 0; choice < numChoices; ++choice) { + expectedChoiceVariables.push_back(this->expressionManager->declareRationalVariable("y" + std::to_string(choice))); + } + bottomStateVariables.reserve(numBottomStates); + for (uint_fast64_t bottomState = 0; bottomState < numBottomStates; ++bottomState) { + bottomStateVariables.push_back(this->expressionManager->declareRationalVariable("z" + std::to_string(bottomState))); + } + + // assert that the values are greater zero and that the bottom state values sum up to one + for (auto& var : expectedChoiceVariables) { + solver->add(var.getExpression() >= zero); + } + storm::expressions::Expression bottomStateSum = zero; + for (auto& var : bottomStateVariables) { + solver->add(var.getExpression() >= zero); + bottomStateSum = bottomStateSum + var.getExpression(); + } + solver->add(bottomStateSum == one); + + // assert that the "incoming" value of each state equals the "outgoing" value + storm::storage::SparseMatrix backwardsTransitions = this->preprocessedModel.getTransitionMatrix().transpose(); + auto bottomStateVariableIt = bottomStateVariables.begin(); + for (uint_fast64_t state = 0; state < numStates; ++state) { + // get the "incomming" value + storm::expressions::Expression value = this->preprocessedModel.getInitialStates().get(state) ? one : zero; + for (auto const& backwardsEntry : backwardsTransitions.getRow(state)) { + value = value + (this->expressionManager->rational(backwardsEntry.getValue()) * expectedChoiceVariables[backwardsEntry.getColumn()].getExpression()); + } + + // subtract the "outgoing" value + for (uint_fast64_t choice = this->preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state]; choice < this->preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state + 1]; ++choice) { + value = value - expectedChoiceVariables[choice]; + } + if (this->possibleBottomStates.get(state)) { + value = value - (*bottomStateVariableIt); + ++bottomStateVariableIt; + } + solver->add(value == zero); + } + assert(bottomStateVariableIt == bottomStateVariables.end()); + + } + + template + void SparseCbAchievabilityQuery::addObjectiveConstraints() { + storm::expressions::Expression zero = this->expressionManager->rational(storm::utility::zero()); + for (Objective const& obj : this->objectives) { + if (obj.rewardModelName) { + STORM_LOG_THROW(obj.bound, storm::exceptions::InvalidOperationException, "Invoked achievability query but no bound was specified for at least one objective."); + STORM_LOG_THROW(!obj.lowerTimeBound && !obj.upperTimeBound, storm::exceptions::NotSupportedException, "Constraint based method currently does not support step bounds"); + std::vector rewards = getActionBasedExpectedRewards(*obj.rewardModelName); + storm::expressions::Expression objValue = zero; + for (uint_fast64_t choice = 0; choice < rewards.size(); ++choice) { + if (!storm::utility::isZero(rewards[choice])) { + objValue = objValue + (this->expressionManager->rational(rewards[choice]) * expectedChoiceVariables[choice].getExpression()); + } + } + // We need to actually evaluate the threshold as rational number. Otherwise a threshold like '<=16/9' might be considered as 1 due to integer division + STORM_LOG_THROW(!obj.bound->threshold.containsVariables(), storm::exceptions::InvalidOperationException, "The threshold for one objective still contains undefined variables"); + storm::expressions::Expression threshold = this->expressionManager->rational(obj.bound->threshold.evaluateAsRational()); + switch (obj.bound->comparisonType) { + case storm::logic::ComparisonType::Greater: + solver->add( objValue > threshold); + break; + case storm::logic::ComparisonType::GreaterEqual: + solver->add( objValue >= threshold); + break; + case storm::logic::ComparisonType::Less: + solver->add( objValue < threshold); + break; + case storm::logic::ComparisonType::LessEqual: + solver->add( objValue <= threshold); + break; + default: + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "One or more objectives have an invalid comparison type"); + } + } + } + } + + template <> + std::vector SparseCbAchievabilityQuery>::getActionBasedExpectedRewards(std::string const& rewardModelName) const { + return this->preprocessedModel.getRewardModel(rewardModelName).getTotalRewardVector(this->preprocessedModel.getTransitionMatrix()); + } + + template <> + std::vector SparseCbAchievabilityQuery>::getActionBasedExpectedRewards(std::string const& rewardModelName) const { + auto const& rewModel = this->preprocessedModel.getRewardModel(rewardModelName); + STORM_LOG_ASSERT(!rewModel.hasTransitionRewards(), "Preprocessed Reward model has transition rewards which is not expected."); + std::vector result = rewModel.hasStateActionRewards() ? rewModel.getStateActionRewardVector() : std::vector(this->preprocessedModel.getNumberOfChoices(), storm::utility::zero()); + if(rewModel.hasStateRewards()) { + // Note that state rewards are earned over time and thus play no role for probabilistic states + for(auto markovianState : this->preprocessedModel.getMarkovianStates()) { + result[this->preprocessedModel.getTransitionMatrix().getRowGroupIndices()[markovianState]] += rewModel.getStateReward(markovianState) / this->preprocessedModel.getExitRate(markovianState); + } + } + return result; + } + + template <> + std::vector SparseCbAchievabilityQuery>::getActionBasedExpectedRewards(std::string const& rewardModelName) const { + auto const& rewModel = this->preprocessedModel.getRewardModel(rewardModelName); + STORM_LOG_ASSERT(!rewModel.hasTransitionRewards(), "Preprocessed Reward model has transition rewards which is not expected."); + std::vector result = rewModel.hasStateActionRewards() ? rewModel.getStateActionRewardVector() : std::vector(this->preprocessedModel.getNumberOfChoices(), storm::utility::zero()); + if(rewModel.hasStateRewards()) { + // Note that state rewards are earned over time and thus play no role for probabilistic states + for(auto markovianState : this->preprocessedModel.getMarkovianStates()) { + result[this->preprocessedModel.getTransitionMatrix().getRowGroupIndices()[markovianState]] += rewModel.getStateReward(markovianState) / this->preprocessedModel.getExitRate(markovianState); + } + } + return result; + } + + template <> + std::vector SparseCbAchievabilityQuery>::getActionBasedExpectedRewards(std::string const& rewardModelName) const { + return this->preprocessedModel.getRewardModel(rewardModelName).getTotalRewardVector(this->preprocessedModel.getTransitionMatrix()); + } + + +#ifdef STORM_HAVE_CARL + template class SparseCbAchievabilityQuery>; + template class SparseCbAchievabilityQuery>; + + template class SparseCbAchievabilityQuery>; + template class SparseCbAchievabilityQuery>; +#endif + } + } +} diff --git a/src/storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.h b/src/storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.h new file mode 100644 index 000000000..24e3c3374 --- /dev/null +++ b/src/storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.h @@ -0,0 +1,63 @@ +#pragma once + + +#include "storm/modelchecker/multiobjective/constraintbased/SparseCbQuery.h" + +#include "storm/solver/SmtSolver.h" +#include "storm/storage/expressions/Variable.h" + +namespace storm { + namespace modelchecker { + namespace multiobjective { + + /* + * This class represents an achievability query for the constraint based approach (using SMT or LP solvers). + */ + template + class SparseCbAchievabilityQuery : public SparseCbQuery { + public: + + typedef typename SparseModelType::ValueType ValueType; + + SparseCbAchievabilityQuery(SparseMultiObjectivePreprocessorReturnType& preprocessorResult); + + virtual ~SparseCbAchievabilityQuery() = default; + + /* + * Invokes the computation and retrieves the result + */ + virtual std::unique_ptr check() override; + + private: + + /* + * Returns whether the given thresholds are achievable. + */ + bool checkAchievability(); + + + /* + * Adds variable y_i for each choice i and z_j for each possible bottom state j and asserts that for every solution of the + * constraint system there is a scheduler under which + * * if choice i yields reward for an expected value objective, then y_i is the expected number of times choice i is taken. + * * z_j/(z_j + Sum_{i in Choices(j)} y_i) is a lower bound for the probability that starting from j no more reward is collected + */ + void initializeConstraintSystem(); + + // Adds the thresholds of the objective values + void addObjectiveConstraints(); + + // Returns the action based rewards for the given reward model name. + std::vector getActionBasedExpectedRewards(std::string const& rewardModelName) const; + + + std::vector expectedChoiceVariables; + std::vector bottomStateVariables; + + + std::unique_ptr solver; + }; + + } + } +} diff --git a/src/storm/modelchecker/multiobjective/constraintbased/SparseCbQuery.cpp b/src/storm/modelchecker/multiobjective/constraintbased/SparseCbQuery.cpp new file mode 100644 index 000000000..99855e790 --- /dev/null +++ b/src/storm/modelchecker/multiobjective/constraintbased/SparseCbQuery.cpp @@ -0,0 +1,38 @@ +#include "storm/modelchecker/multiobjective/constraintbased/SparseCbQuery.h" + +#include "storm/adapters/CarlAdapter.h" +#include "storm/models/sparse/Mdp.h" +#include "storm/models/sparse/MarkovAutomaton.h" +#include "storm/models/sparse/StandardRewardModel.h" +#include "storm/modelchecker/multiobjective/Objective.h" +#include "storm/settings/SettingsManager.h" +#include "storm/settings/modules/MultiObjectiveSettings.h" +#include "storm/utility/constants.h" +#include "storm/utility/vector.h" + +#include "storm/exceptions/UnexpectedException.h" + +namespace storm { + namespace modelchecker { + namespace multiobjective { + + + template + SparseCbQuery::SparseCbQuery(SparseMultiObjectivePreprocessorReturnType& preprocessorResult) : + originalModel(preprocessorResult.originalModel), originalFormula(preprocessorResult.originalFormula), + preprocessedModel(std::move(*preprocessorResult.preprocessedModel)), objectives(std::move(preprocessorResult.objectives)), + possibleBottomStates(std::move(preprocessorResult.possibleBottomStates)) { + expressionManager = std::make_shared(); + } + + +#ifdef STORM_HAVE_CARL + template class SparseCbQuery>; + template class SparseCbQuery>; + + template class SparseCbQuery>; + template class SparseCbQuery>; +#endif + } + } +} diff --git a/src/storm/modelchecker/multiobjective/constraintbased/SparseCbQuery.h b/src/storm/modelchecker/multiobjective/constraintbased/SparseCbQuery.h new file mode 100644 index 000000000..d3bc42c91 --- /dev/null +++ b/src/storm/modelchecker/multiobjective/constraintbased/SparseCbQuery.h @@ -0,0 +1,46 @@ +#pragma once + +#include + +#include "storm/modelchecker/results/CheckResult.h" +#include "storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorReturnType.h" +#include "storm/storage/expressions/ExpressionManager.h" + +namespace storm { + namespace modelchecker { + namespace multiobjective { + + /* + * This class represents a multi-objective query for the constraint based approach (using SMT or LP solvers). + */ + template + class SparseCbQuery { + public: + + + virtual ~SparseCbQuery() = default; + + /* + * Invokes the computation and retrieves the result + */ + virtual std::unique_ptr check() = 0; + + protected: + + SparseCbQuery(SparseMultiObjectivePreprocessorReturnType& preprocessorResult); + + SparseModelType const& originalModel; + storm::logic::MultiObjectiveFormula const& originalFormula; + + SparseModelType preprocessedModel; + std::vector> objectives; + + std::shared_ptr expressionManager; + + storm::storage::BitVector possibleBottomStates; + + }; + + } + } +} diff --git a/src/storm/modelchecker/multiobjective/multiObjectiveModelChecking.cpp b/src/storm/modelchecker/multiobjective/multiObjectiveModelChecking.cpp new file mode 100644 index 000000000..cdec9b7c3 --- /dev/null +++ b/src/storm/modelchecker/multiobjective/multiObjectiveModelChecking.cpp @@ -0,0 +1,122 @@ +#include "storm/modelchecker/multiobjective/multiObjectiveModelChecking.h" + +#include "storm/utility/macros.h" + +#include "storm/models/sparse/Mdp.h" +#include "storm/models/sparse/MarkovAutomaton.h" +#include "storm/models/sparse/StandardRewardModel.h" +#include "storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.h" +#include "storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.h" +#include "storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.h" +#include "storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.h" +#include "storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.h" +#include "storm/settings/SettingsManager.h" +#include "storm/settings/modules/MultiObjectiveSettings.h" +#include "storm/settings/modules/CoreSettings.h" +#include "storm/utility/Stopwatch.h" + +#include "storm/exceptions/InvalidArgumentException.h" + + +namespace storm { + namespace modelchecker { + namespace multiobjective { + + template + std::unique_ptr performMultiObjectiveModelChecking(SparseModelType const& model, storm::logic::MultiObjectiveFormula const& formula, MultiObjectiveMethodSelection methodSelection) { + storm::utility::Stopwatch swTotal(true); + storm::utility::Stopwatch swPreprocessing(true); + STORM_LOG_ASSERT(model.getInitialStates().getNumberOfSetBits() == 1, "Multi-objective Model checking on model with multiple initial states is not supported."); + + // If we consider an MA, ensure that it is closed + if(model.isOfType(storm::models::ModelType::MarkovAutomaton)) { + STORM_LOG_THROW(dynamic_cast const *>(&model)->isClosed(), storm::exceptions::InvalidArgumentException, "Unable to check multi-objective formula on non-closed Markov automaton."); + } + + // Preprocess the model + auto preprocessorResult = SparseMultiObjectivePreprocessor::preprocess(model, formula); + swPreprocessing.stop(); + if (storm::settings::getModule().isShowStatisticsSet()) { + STORM_PRINT_AND_LOG("Preprocessing done in " << swPreprocessing << " seconds." << std::endl << " Result: " << preprocessorResult << std::endl); + } else { + STORM_LOG_INFO("Preprocessing done in " << swPreprocessing << " seconds." << std::endl << " Result: " << preprocessorResult << std::endl); + } + + // Get the solution method + MultiObjectiveMethod method; + if (methodSelection == MultiObjectiveMethodSelection::FROMSETTINGS) { + method = storm::settings::getModule().getMultiObjectiveMethod(); + } else { + method = convert(methodSelection); + } + + // Invoke the analysis + storm::utility::Stopwatch swAnalysis(true); + std::unique_ptr result; + switch (method) { + case MultiObjectiveMethod::Pcaa: + { + std::unique_ptr> query; + switch (preprocessorResult.queryType) { + case SparseMultiObjectivePreprocessorReturnType::QueryType::Achievability: + query = std::unique_ptr> (new SparsePcaaAchievabilityQuery(preprocessorResult)); + break; + case SparseMultiObjectivePreprocessorReturnType::QueryType::Quantitative: + query = std::unique_ptr> (new SparsePcaaQuantitativeQuery(preprocessorResult)); + break; + case SparseMultiObjectivePreprocessorReturnType::QueryType::Pareto: + query = std::unique_ptr> (new SparsePcaaParetoQuery(preprocessorResult)); + break; + default: + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The multi-objective query type is not supported for the selected solution method '" << toString(method) << "'."); + break; + } + + result = query->check(); + + if(storm::settings::getModule().isExportPlotSet()) { + query->exportPlotOfCurrentApproximation(storm::settings::getModule().getExportPlotDirectory()); + } + break; + } + case MultiObjectiveMethod::ConstraintBased: + { + std::unique_ptr> query; + switch (preprocessorResult.queryType) { + case SparseMultiObjectivePreprocessorReturnType::QueryType::Achievability: + query = std::unique_ptr> (new SparseCbAchievabilityQuery(preprocessorResult)); + break; + default: + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The multi-objective query type is not supported for the selected solution method '" << toString(method) << "'."); + break; + } + + result = query->check(); + + if(storm::settings::getModule().isExportPlotSet()) { + STORM_LOG_ERROR("Can not export plot for the constrained based solver."); + } + break; + } + default: + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The multi-objective solution method '" << toString(method) << "' is not supported."); + } + swAnalysis.stop(); + + swTotal.stop(); + if (storm::settings::getModule().isShowStatisticsSet()) { + STORM_PRINT_AND_LOG("Solving multi-objective query took " << swTotal << " seconds (consisting of " << swPreprocessing << " seconds for preprocessing and " << swAnalysis << " seconds for analyzing the preprocessed model)." << std::endl); + } + + return result; + } + + + template std::unique_ptr performMultiObjectiveModelChecking>(storm::models::sparse::Mdp const& model, storm::logic::MultiObjectiveFormula const& formula, MultiObjectiveMethodSelection methodSelection); + template std::unique_ptr performMultiObjectiveModelChecking>(storm::models::sparse::MarkovAutomaton const& model, storm::logic::MultiObjectiveFormula const& formula, MultiObjectiveMethodSelection methodSelection); + template std::unique_ptr performMultiObjectiveModelChecking>(storm::models::sparse::Mdp const& model, storm::logic::MultiObjectiveFormula const& formula, MultiObjectiveMethodSelection methodSelection); + template std::unique_ptr performMultiObjectiveModelChecking>(storm::models::sparse::MarkovAutomaton const& model, storm::logic::MultiObjectiveFormula const& formula, MultiObjectiveMethodSelection methodSelection); + + } + } +} diff --git a/src/storm/modelchecker/multiobjective/multiObjectiveModelChecking.h b/src/storm/modelchecker/multiobjective/multiObjectiveModelChecking.h new file mode 100644 index 000000000..380f79384 --- /dev/null +++ b/src/storm/modelchecker/multiobjective/multiObjectiveModelChecking.h @@ -0,0 +1,19 @@ +#pragma once + +#include + +#include "storm/modelchecker/results/CheckResult.h" +#include "storm/modelchecker/multiobjective/MultiObjectiveModelCheckingMethod.h" +#include "storm/logic/Formulas.h" + +namespace storm { + namespace modelchecker { + namespace multiobjective { + + + template + std::unique_ptr performMultiObjectiveModelChecking(SparseModelType const& model, storm::logic::MultiObjectiveFormula const& formula, MultiObjectiveMethodSelection methodSelection = MultiObjectiveMethodSelection::FROMSETTINGS); + + } + } +} diff --git a/src/storm/modelchecker/multiobjective/pcaa.cpp b/src/storm/modelchecker/multiobjective/pcaa.cpp deleted file mode 100644 index 421cbb566..000000000 --- a/src/storm/modelchecker/multiobjective/pcaa.cpp +++ /dev/null @@ -1,88 +0,0 @@ -#include "storm/modelchecker/multiobjective/pcaa.h" - -#include "storm/utility/macros.h" - -#include "storm/models/sparse/Mdp.h" -#include "storm/models/sparse/MarkovAutomaton.h" -#include "storm/models/sparse/StandardRewardModel.h" -#include "storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.h" -#include "storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.h" -#include "storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.h" -#include "storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.h" -#include "storm/settings/SettingsManager.h" -#include "storm/settings/modules/MultiObjectiveSettings.h" -#include "storm/settings/modules/CoreSettings.h" -#include "storm/utility/Stopwatch.h" - -#include "storm/exceptions/InvalidArgumentException.h" - - -namespace storm { - namespace modelchecker { - namespace multiobjective { - - template - std::unique_ptr performPcaa(SparseModelType const& model, storm::logic::MultiObjectiveFormula const& formula) { - storm::utility::Stopwatch swTotal(true); - storm::utility::Stopwatch swPreprocessing(true); - STORM_LOG_ASSERT(model.getInitialStates().getNumberOfSetBits() == 1, "Multi-objective Model checking on model with multiple initial states is not supported."); - -#ifdef STORM_HAVE_CARL - - // If we consider an MA, ensure that it is closed - if(model.isOfType(storm::models::ModelType::MarkovAutomaton)) { - STORM_LOG_THROW(dynamic_cast const *>(&model)->isClosed(), storm::exceptions::InvalidArgumentException, "Unable to check multi-objective formula on non-closed Markov automaton."); - } - - auto preprocessorResult = SparsePcaaPreprocessor::preprocess(model, formula); - swPreprocessing.stop(); - if (storm::settings::getModule().isShowStatisticsSet()) { - STORM_PRINT_AND_LOG("Preprocessing done in " << swPreprocessing << " seconds." << std::endl << " Result: " << preprocessorResult << std::endl); - } else { - STORM_LOG_INFO("Preprocessing done in " << swPreprocessing << " seconds." << std::endl << " Result: " << preprocessorResult << std::endl); - } - storm::utility::Stopwatch swValueIterations(true); - std::unique_ptr> query; - switch (preprocessorResult.queryType) { - case SparsePcaaPreprocessorReturnType::QueryType::Achievability: - query = std::unique_ptr> (new SparsePcaaAchievabilityQuery(preprocessorResult)); - break; - case SparsePcaaPreprocessorReturnType::QueryType::Quantitative: - query = std::unique_ptr> (new SparsePcaaQuantitativeQuery(preprocessorResult)); - break; - case SparsePcaaPreprocessorReturnType::QueryType::Pareto: - query = std::unique_ptr> (new SparsePcaaParetoQuery(preprocessorResult)); - break; - default: - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Unsupported multi-objective Query Type."); - break; - } - - auto result = query->check(); - swValueIterations.stop(); - swTotal.stop(); - if (storm::settings::getModule().isShowStatisticsSet()) { - STORM_PRINT_AND_LOG("Solving multi-objective query took " << swTotal << " seconds (consisting of " << swPreprocessing << " seconds for preprocessing and " << swValueIterations << " seconds for value iteration-based exploration of achievable points)." << std::endl); - } - - - if(storm::settings::getModule().isExportPlotSet()) { - query->exportPlotOfCurrentApproximation(storm::settings::getModule().getExportPlotDirectory()); - } - return result; -#else - STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Multi-objective model checking requires carl."); - return nullptr; -#endif - } - - template std::unique_ptr performPcaa>(storm::models::sparse::Mdp const& model, storm::logic::MultiObjectiveFormula const& formula); - template std::unique_ptr performPcaa>(storm::models::sparse::MarkovAutomaton const& model, storm::logic::MultiObjectiveFormula const& formula); -#ifdef STORM_HAVE_CARL - template std::unique_ptr performPcaa>(storm::models::sparse::Mdp const& model, storm::logic::MultiObjectiveFormula const& formula); - template std::unique_ptr performPcaa>(storm::models::sparse::MarkovAutomaton const& model, storm::logic::MultiObjectiveFormula const& formula); -#endif - - } - } -} diff --git a/src/storm/modelchecker/multiobjective/pcaa.h b/src/storm/modelchecker/multiobjective/pcaa.h deleted file mode 100644 index eca82b767..000000000 --- a/src/storm/modelchecker/multiobjective/pcaa.h +++ /dev/null @@ -1,20 +0,0 @@ -#ifndef STORM_MODELCHECKER_MULTIOBJECTIVE_PCAA_H_ -#define STORM_MODELCHECKER_MULTIOBJECTIVE_PCAA_H_ - -#include - -#include "storm/modelchecker/results/CheckResult.h" -#include "storm/logic/Formulas.h" - -namespace storm { - namespace modelchecker { - namespace multiobjective { - - template - std::unique_ptr performPcaa(SparseModelType const& model, storm::logic::MultiObjectiveFormula const& formula); - - } - } -} - -#endif /* STORM_MODELCHECKER_MULTIOBJECTIVE_PCAA_H_ */ diff --git a/src/storm/modelchecker/multiobjective/pcaa/PcaaObjective.h b/src/storm/modelchecker/multiobjective/pcaa/PcaaObjective.h deleted file mode 100644 index ac0043fae..000000000 --- a/src/storm/modelchecker/multiobjective/pcaa/PcaaObjective.h +++ /dev/null @@ -1,72 +0,0 @@ -#ifndef STORM_MODELCHECKER_MULTIOBJECTIVE_PCAA_PCAAOBJECTIVE_H_ -#define STORM_MODELCHECKER_MULTIOBJECTIVE_PCAA_PCAAOBJECTIVE_H_ - -#include -#include - -#include "storm/logic/Formulas.h" - -namespace storm { - namespace modelchecker { - namespace multiobjective { - template - struct PcaaObjective { - // the original input formula - std::shared_ptr 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 threshold; - // True iff the specified threshold is strict, i.e., > - bool thresholdIsStrict = false; - - // The time bound(s) for the formula (if given by the originalFormula) - boost::optional lowerTimeBound; - boost::optional upperTimeBound; - bool lowerTimeBoundStrict = false; - bool upperTimeBoundStrict = false; - - 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 << "time bounds:"; - if(lowerTimeBound) { - if(upperTimeBound) { - out << (lowerTimeBoundStrict ? "(" : "[") << *lowerTimeBound << ", " << *upperTimeBound << (upperTimeBoundStrict ? ")" : "]"); - } else { - out << (lowerTimeBoundStrict ? " >" : ">=") << std::setw(5) << *lowerTimeBound; - } - } else if (upperTimeBound) { - out << (upperTimeBoundStrict ? " <" : "<=") << std::setw(5) << *upperTimeBound; - } else { - out << " none"; - } - out << ")" << std::endl; - } - }; - } - } -} - -#endif /* STORM_MODELCHECKER_MULTIOBJECTIVE_PCAA_OBJECTIVE_H_ */ diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp index d06b3ce40..e70f89bbc 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp @@ -16,17 +16,17 @@ namespace storm { namespace modelchecker { namespace multiobjective { + template SparseMaPcaaWeightVectorChecker::SparseMaPcaaWeightVectorChecker(SparseMaModelType const& model, - std::vector> const& objectives, - storm::storage::BitVector const& actionsWithNegativeReward, - storm::storage::BitVector const& ecActions, - storm::storage::BitVector const& possiblyRecurrentStates) : - SparsePcaaWeightVectorChecker(model, objectives, actionsWithNegativeReward, ecActions, possiblyRecurrentStates) { + std::vector> const& objectives, + storm::storage::BitVector const& possibleECActions, + storm::storage::BitVector const& possibleBottomStates) : + SparsePcaaWeightVectorChecker(model, objectives, possibleECActions, possibleBottomStates) { // Set the (discretized) state action rewards. this->discreteActionRewards.resize(objectives.size()); for(auto objIndex : this->objectivesWithNoUpperTimeBound) { - typename SparseMaModelType::RewardModelType const& rewModel = this->model.getRewardModel(this->objectives[objIndex].rewardModelName); + typename SparseMaModelType::RewardModelType const& rewModel = this->model.getRewardModel(*this->objectives[objIndex].rewardModelName); STORM_LOG_ASSERT(!rewModel.hasTransitionRewards(), "Preprocessed Reward model has transition rewards which is not expected."); this->discreteActionRewards[objIndex] = rewModel.hasStateActionRewards() ? rewModel.getStateActionRewardVector() : std::vector(this->model.getTransitionMatrix().getRowCount(), storm::utility::zero()); if(rewModel.hasStateRewards()) { @@ -109,7 +109,7 @@ namespace storm { result.toMS = this->model.getTransitionMatrix().getSubmatrix(true, result.states, this->model.getMarkovianStates(), createMS); result.toPS = this->model.getTransitionMatrix().getSubmatrix(true, result.states, probabilisticStates, false); STORM_LOG_ASSERT(result.getNumberOfStates() == result.states.getNumberOfSetBits() && result.getNumberOfStates() == result.toMS.getRowGroupCount() && result.getNumberOfStates() == result.toPS.getRowGroupCount(), "Invalid state count for subsystem"); - STORM_LOG_ASSERT(result.getNumberOfChoices() == result.choices.getNumberOfSetBits() && result.getNumberOfChoices() == result.toMS.getRowCount() && result.getNumberOfChoices() == result.toPS.getRowCount(), "Invalid state count for subsystem"); + STORM_LOG_ASSERT(result.getNumberOfChoices() == result.choices.getNumberOfSetBits() && result.getNumberOfChoices() == result.toMS.getRowCount() && result.getNumberOfChoices() == result.toPS.getRowCount(), "Invalid choice count for subsystem"); result.weightedRewardVector.resize(result.getNumberOfChoices()); storm::utility::vector::selectVectorValues(result.weightedRewardVector, result.choices, weightedRewardVector); @@ -120,7 +120,7 @@ namespace storm { if(this->objectivesWithNoUpperTimeBound.get(objIndex)) { storm::utility::vector::selectVectorValues(objVector, result.choices, this->discreteActionRewards[objIndex]); } else { - typename SparseMaModelType::RewardModelType const& rewModel = this->model.getRewardModel(this->objectives[objIndex].rewardModelName); + typename SparseMaModelType::RewardModelType const& rewModel = this->model.getRewardModel(*this->objectives[objIndex].rewardModelName); STORM_LOG_ASSERT(!rewModel.hasTransitionRewards(), "Preprocessed Reward model has transition rewards which is not expected."); STORM_LOG_ASSERT(!rewModel.hasStateRewards(), "State rewards for bounded objectives for MAs are not expected (bounded rewards are not supported)."); if(rewModel.hasStateActionRewards()) { @@ -161,8 +161,8 @@ namespace storm { VT smallestNonZeroBound = storm::utility::zero(); for(auto const& obj : this->objectives) { if(obj.upperTimeBound){ - STORM_LOG_THROW(!obj.upperTimeBound->containsVariables(), storm::exceptions::InvalidOperationException, "The time bound '" << *obj.upperTimeBound << " contains undefined variables"); - timeBounds.push_back(storm::utility::convertNumber(obj.upperTimeBound->evaluateAsRational())); + STORM_LOG_THROW(!obj.upperTimeBound->getBound().containsVariables(), storm::exceptions::InvalidOperationException, "The time bound '" << obj.upperTimeBound->getBound() << " contains undefined variables"); + timeBounds.push_back(storm::utility::convertNumber(obj.upperTimeBound->getBound().evaluateAsRational())); STORM_LOG_ASSERT(!storm::utility::isZero(timeBounds.back()), "Got zero-valued upper time bound."); eToPowerOfMinusMaxRateTimesBound.push_back(std::exp(-maxRate * timeBounds.back())); smallestNonZeroBound = storm::utility::isZero(smallestNonZeroBound) ? timeBounds.back() : std::min(smallestNonZeroBound, timeBounds.back()); @@ -260,7 +260,7 @@ namespace storm { VT errorTowardsZero = storm::utility::zero(); VT errorAwayFromZero = storm::utility::zero(); if(obj.upperTimeBound) { - VT timeBound = storm::utility::convertNumber(obj.upperTimeBound->evaluateAsRational()); + VT timeBound = storm::utility::convertNumber(obj.upperTimeBound->getBound().evaluateAsRational()); uint_fast64_t digitizedBound = storm::utility::convertNumber(timeBound/digitizationConstant); auto timeBoundIt = upperTimeBounds.insert(std::make_pair(digitizedBound, storm::storage::BitVector(this->objectives.size(), false))).first; timeBoundIt->second.set(objIndex); @@ -268,12 +268,12 @@ namespace storm { digitizationError -= std::exp(-maxRate * timeBound) * storm::utility::pow(storm::utility::one() + maxRate * digitizationConstant, digitizedBound); errorAwayFromZero += digitizationError; } - if (obj.rewardsArePositive) { - this->offsetsToLowerBound[objIndex] = -errorTowardsZero; - this->offsetsToUpperBound[objIndex] = errorAwayFromZero; + if (storm::solver::maximize(obj.optimizationDirection)) { + this->offsetsToUnderApproximation[objIndex] = -errorTowardsZero; + this->offsetsToOverApproximation[objIndex] = errorAwayFromZero; } else { - this->offsetsToLowerBound[objIndex] = -errorAwayFromZero; - this->offsetsToUpperBound[objIndex] = errorTowardsZero; + this->offsetsToUnderApproximation[objIndex] = errorAwayFromZero; + this->offsetsToOverApproximation[objIndex] = -errorTowardsZero; } } } @@ -324,8 +324,9 @@ namespace storm { consideredObjectives |= upperTimeBoundIt->second; for(auto objIndex : upperTimeBoundIt->second) { // This objective now plays a role in the weighted sum - storm::utility::vector::addScaledVector(MS.weightedRewardVector, MS.objectiveRewardVectors[objIndex], weightVector[objIndex]); - storm::utility::vector::addScaledVector(PS.weightedRewardVector, PS.objectiveRewardVectors[objIndex], weightVector[objIndex]); + ValueType factor = storm::solver::minimize(this->objectives[objIndex].optimizationDirection) ? -weightVector[objIndex] : weightVector[objIndex]; + storm::utility::vector::addScaledVector(MS.weightedRewardVector, MS.objectiveRewardVectors[objIndex], factor); + storm::utility::vector::addScaledVector(PS.weightedRewardVector, PS.objectiveRewardVectors[objIndex], factor); } ++upperTimeBoundIt; } @@ -344,6 +345,9 @@ namespace storm { // In this case there is no need to perform the computation on the individual objectives optimalChoicesAtCurrentEpoch = newScheduler->getChoices(); PS.objectiveSolutionVectors[*consideredObjectives.begin()] = PS.weightedSolutionVector; + if (storm::solver::minimize(this->objectives[*consideredObjectives.begin()].optimizationDirection)) { + storm::utility::vector::scaleVectorInPlace(PS.objectiveSolutionVectors[*consideredObjectives.begin()], -storm::utility::one()); + } } else { // check whether the linEqSolver needs to be updated, i.e., whether the scheduler has changed if(linEq.solver == nullptr || newScheduler->getChoices() != optimalChoicesAtCurrentEpoch) { @@ -388,6 +392,9 @@ namespace storm { if(consideredObjectives.getNumberOfSetBits() == 1 && storm::utility::isOne(weightVector[*consideredObjectives.begin()])) { // In this case there is no need to perform the computation on the individual objectives MS.objectiveSolutionVectors[*consideredObjectives.begin()] = MS.weightedSolutionVector; + if (storm::solver::minimize(this->objectives[*consideredObjectives.begin()].optimizationDirection)) { + storm::utility::vector::scaleVectorInPlace(MS.objectiveSolutionVectors[*consideredObjectives.begin()], -storm::utility::one()); + } } else { for(auto objIndex : consideredObjectives) { MS.toMS.multiplyWithVector(MS.objectiveSolutionVectors[objIndex], MS.auxChoiceValues); diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.h b/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.h index ef3c6ea72..d3baaca42 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.h +++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.h @@ -25,10 +25,9 @@ namespace storm { typedef typename SparseMaModelType::ValueType ValueType; SparseMaPcaaWeightVectorChecker(SparseMaModelType const& model, - std::vector> const& objectives, - storm::storage::BitVector const& actionsWithNegativeReward, - storm::storage::BitVector const& ecActions, - storm::storage::BitVector const& possiblyRecurrentStates); + std::vector> const& objectives, + storm::storage::BitVector const& possibleECActions, + storm::storage::BitVector const& possibleBottomStates); virtual ~SparseMaPcaaWeightVectorChecker() = default; @@ -106,7 +105,7 @@ namespace storm { void digitize(SubModel& subModel, VT const& digitizationConstant) const; /* - * Fills the given map with the digitized time bounds. Also sets the offsetsToLowerBound / offsetsToUpperBound values + * Fills the given map with the digitized time bounds. Also sets the offsetsToUnderApproximation / offsetsToOverApproximation values * according to the digitization error */ template ::SupportsExponential, int>::type = 0> diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.cpp index a6dc7a3b4..01ea6f616 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.cpp @@ -14,14 +14,13 @@ namespace storm { template SparseMdpPcaaWeightVectorChecker::SparseMdpPcaaWeightVectorChecker(SparseMdpModelType const& model, - std::vector> const& objectives, - storm::storage::BitVector const& actionsWithNegativeReward, - storm::storage::BitVector const& ecActions, - storm::storage::BitVector const& possiblyRecurrentStates) : - SparsePcaaWeightVectorChecker(model, objectives, actionsWithNegativeReward, ecActions, possiblyRecurrentStates) { + std::vector> const& objectives, + storm::storage::BitVector const& possibleECActions, + storm::storage::BitVector const& possibleBottomStates) : + SparsePcaaWeightVectorChecker(model, objectives, possibleECActions, possibleBottomStates) { // set the state action rewards for (uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { - typename SparseMdpModelType::RewardModelType const& rewModel = this->model.getRewardModel(this->objectives[objIndex].rewardModelName); + typename SparseMdpModelType::RewardModelType const& rewModel = this->model.getRewardModel(*this->objectives[objIndex].rewardModelName); STORM_LOG_ASSERT(!rewModel.hasTransitionRewards(), "Reward model has transition rewards which is not expected."); this->discreteActionRewards[objIndex] = rewModel.getTotalRewardVector(this->model.getTransitionMatrix()); } @@ -33,33 +32,29 @@ namespace storm { std::vector optimalChoicesInCurrentEpoch(this->model.getNumberOfStates()); std::vector choiceValues(weightedRewardVector.size()); std::vector temporaryResult(this->model.getNumberOfStates()); - std::vector zeroReward(weightedRewardVector.size(), storm::utility::zero()); // Get for each occurring timeBound the indices of the objectives with that bound. std::map> stepBounds; for (uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { auto const& obj = this->objectives[objIndex]; STORM_LOG_THROW(!obj.lowerTimeBound, storm::exceptions::InvalidPropertyException, "Lower step bounds are not supported by this model checker"); if (obj.upperTimeBound) { - STORM_LOG_THROW(!obj.upperTimeBound->containsVariables(), storm::exceptions::InvalidPropertyException, "The step bound '" << * obj.upperTimeBound << " contains undefined variables"); - uint_fast64_t stepBound = (uint_fast64_t) obj.upperTimeBound->evaluateAsInt(); - if (obj.upperTimeBoundStrict) { + STORM_LOG_THROW(!obj.upperTimeBound->getBound().containsVariables(), storm::exceptions::InvalidPropertyException, "The step bound '" << obj.upperTimeBound->getBound() << " contains undefined variables"); + uint_fast64_t stepBound = (uint_fast64_t) obj.upperTimeBound->getBound().evaluateAsInt(); + if (obj.upperTimeBound->isStrict()) { --stepBound; } auto stepBoundIt = stepBounds.insert(std::make_pair(stepBound, storm::storage::BitVector(this->objectives.size(), false))).first; stepBoundIt->second.set(objIndex); // There is no error for the values of these objectives. - this->offsetsToLowerBound[objIndex] = storm::utility::zero(); - this->offsetsToUpperBound[objIndex] = storm::utility::zero(); + this->offsetsToUnderApproximation[objIndex] = storm::utility::zero(); + this->offsetsToOverApproximation[objIndex] = storm::utility::zero(); } } // Stores the objectives for which we need to compute values in the current time epoch. storm::storage::BitVector consideredObjectives = this->objectivesWithNoUpperTimeBound; - // Stores objectives for which the current epoch passed their lower bound - storm::storage::BitVector lowerBoundViolatedObjectives(consideredObjectives.size(), false); - auto stepBoundIt = stepBounds.begin(); uint_fast64_t currentEpoch = stepBounds.empty() ? 0 : stepBoundIt->first; @@ -69,7 +64,8 @@ namespace storm { consideredObjectives |= stepBoundIt->second; for(auto objIndex : stepBoundIt->second) { // This objective now plays a role in the weighted sum - storm::utility::vector::addScaledVector(weightedRewardVector, this->discreteActionRewards[objIndex], weightVector[objIndex]); + ValueType factor = storm::solver::minimize(this->objectives[objIndex].optimizationDirection) ? -weightVector[objIndex] : weightVector[objIndex]; + storm::utility::vector::addScaledVector(weightedRewardVector, this->discreteActionRewards[objIndex], factor); } ++stepBoundIt; } @@ -83,7 +79,7 @@ namespace storm { // TODO we could compute the result for one of the objectives from the weighted result, the given weight vector, and the remaining objective results. for (auto objIndex : consideredObjectives) { std::vector& objectiveResult = this->objectiveResults[objIndex]; - std::vector const& objectiveRewards = lowerBoundViolatedObjectives.get(objIndex) ? zeroReward : this->discreteActionRewards[objIndex]; + std::vector const& objectiveRewards = this->discreteActionRewards[objIndex]; auto rowGroupIndexIt = this->model.getTransitionMatrix().getRowGroupIndices().begin(); auto optimalChoiceIt = optimalChoicesInCurrentEpoch.begin(); for(ValueType& stateValue : temporaryResult){ diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.h b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.h index 8b56386c9..91cb862f1 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.h +++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.h @@ -20,11 +20,20 @@ namespace storm { public: typedef typename SparseMdpModelType::ValueType ValueType; + /* + * Creates a weight vextor checker. + * + * @param model The (preprocessed) model + * @param objectives The (preprocessed) objectives + * @param possibleECActions Overapproximation of the actions that are part of an EC + * @param possibleBottomStates The states for which it is posible to not collect further reward with prob. 1 + * + */ + SparseMdpPcaaWeightVectorChecker(SparseMdpModelType const& model, - std::vector> const& objectives, - storm::storage::BitVector const& actionsWithNegativeReward, - storm::storage::BitVector const& ecActions, - storm::storage::BitVector const& possiblyRecurrentStates); + std::vector> const& objectives, + storm::storage::BitVector const& possibleECActions, + storm::storage::BitVector const& possibleBottomStates); virtual ~SparseMdpPcaaWeightVectorChecker() = default; diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.cpp index db0c2da9d..fcf6ca98e 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.cpp @@ -7,18 +7,20 @@ #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "storm/utility/constants.h" #include "storm/utility/vector.h" -#include "storm/settings//SettingsManager.h" +#include "storm/settings/SettingsManager.h" #include "storm/settings/modules/GeneralSettings.h" #include "storm/settings/modules/MultiObjectiveSettings.h" +#include "storm/exceptions/InvalidOperationException.h" + namespace storm { namespace modelchecker { namespace multiobjective { template - SparsePcaaAchievabilityQuery::SparsePcaaAchievabilityQuery(SparsePcaaPreprocessorReturnType& preprocessorResult) : SparsePcaaQuery(preprocessorResult) { - STORM_LOG_ASSERT(preprocessorResult.queryType==SparsePcaaPreprocessorReturnType::QueryType::Achievability, "Invalid query Type"); + SparsePcaaAchievabilityQuery::SparsePcaaAchievabilityQuery(SparseMultiObjectivePreprocessorReturnType& preprocessorResult) : SparsePcaaQuery(preprocessorResult) { + STORM_LOG_ASSERT(preprocessorResult.queryType==SparseMultiObjectivePreprocessorReturnType::QueryType::Achievability, "Invalid query Type"); initializeThresholdData(); // Set the precision of the weight vector checker. Will be refined during the computation @@ -30,8 +32,17 @@ namespace storm { thresholds.reserve(this->objectives.size()); strictThresholds = storm::storage::BitVector(this->objectives.size(), false); for(uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { - thresholds.push_back(storm::utility::convertNumber(*this->objectives[objIndex].threshold)); - strictThresholds.set(objIndex, this->objectives[objIndex].thresholdIsStrict); + auto const& obj = this->objectives[objIndex]; + STORM_LOG_ASSERT(obj.bound.is_initialized(), "Achievability query invoked but there is an objective without bound."); + STORM_LOG_THROW(!obj.bound->threshold.containsVariables(), storm::exceptions::InvalidOperationException, "There is an objective whose bound contains undefined variables."); + thresholds.push_back(storm::utility::convertNumber(obj.bound->threshold.evaluateAsRational())); + if (storm::solver::minimize(obj.optimizationDirection)) { + STORM_LOG_ASSERT(!storm::logic::isLowerBound(obj.bound->comparisonType), "Minimizing objective should not specify an upper bound."); + // Values for minimizing objectives will be negated in order to convert them to maximizing objectives. + // Hence, we also negate the threshold + thresholds.back() *= -storm::utility::one(); + } + strictThresholds.set(objIndex, storm::logic::isStrict(obj.bound->comparisonType)); } } diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.h b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.h index c250f257b..fe455e457 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.h +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.h @@ -23,7 +23,7 @@ namespace storm { * Creates a new query for the Pareto curve approximation algorithm (Pcaa) * @param preprocessorResult the result from preprocessing */ - SparsePcaaAchievabilityQuery(SparsePcaaPreprocessorReturnType& preprocessorResult); + SparsePcaaAchievabilityQuery(SparseMultiObjectivePreprocessorReturnType& preprocessorResult); virtual ~SparsePcaaAchievabilityQuery() = default; diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp index 92717febb..488e3667b 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp @@ -17,8 +17,8 @@ namespace storm { namespace multiobjective { template - SparsePcaaParetoQuery::SparsePcaaParetoQuery(SparsePcaaPreprocessorReturnType& preprocessorResult) : SparsePcaaQuery(preprocessorResult) { - STORM_LOG_ASSERT(preprocessorResult.queryType==SparsePcaaPreprocessorReturnType::QueryType::Pareto, "Invalid query Type"); + SparsePcaaParetoQuery::SparsePcaaParetoQuery(SparseMultiObjectivePreprocessorReturnType& preprocessorResult) : SparsePcaaQuery(preprocessorResult) { + STORM_LOG_ASSERT(preprocessorResult.queryType==SparseMultiObjectivePreprocessorReturnType::QueryType::Pareto, "Invalid query Type"); // Set the precision of the weight vector checker typename SparseModelType::ValueType weightedPrecision = storm::utility::convertNumber(storm::settings::getModule().getPrecision()); diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.h b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.h index b6361faff..ffcf7bb3d 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.h +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.h @@ -23,7 +23,7 @@ namespace storm { * Creates a new query for the Pareto curve approximation algorithm (Pcaa) * @param preprocessorResult the result from preprocessing */ - SparsePcaaParetoQuery(SparsePcaaPreprocessorReturnType& preprocessorResult); + SparsePcaaParetoQuery(SparseMultiObjectivePreprocessorReturnType& preprocessorResult); virtual ~SparsePcaaParetoQuery() = default; diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.cpp deleted file mode 100644 index 58edc68a8..000000000 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.cpp +++ /dev/null @@ -1,416 +0,0 @@ -#include "storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.h" - -#include "storm/models/sparse/Mdp.h" -#include "storm/models/sparse/MarkovAutomaton.h" -#include "storm/models/sparse/StandardRewardModel.h" -#include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h" -#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" -#include "storm/storage/MaximalEndComponentDecomposition.h" -#include "storm/transformer/StateDuplicator.h" -#include "storm/transformer/SubsystemBuilder.h" -#include "storm/utility/macros.h" -#include "storm/utility/vector.h" -#include "storm/utility/graph.h" - -#include "storm/exceptions/InvalidPropertyException.h" -#include "storm/exceptions/UnexpectedException.h" - -namespace storm { - namespace modelchecker { - namespace multiobjective { - - template - typename SparsePcaaPreprocessor::ReturnType SparsePcaaPreprocessor::preprocess(SparseModelType const& originalModel, storm::logic::MultiObjectiveFormula const& originalFormula) { - - ReturnType result(originalFormula, originalModel, SparseModelType(originalModel)); - result.newToOldStateIndexMapping = storm::utility::vector::buildVectorForRange(0, originalModel.getNumberOfStates()); - - //Invoke preprocessing on the individual objectives - for(auto const& subFormula : originalFormula.getSubformulas()){ - STORM_LOG_INFO("Preprocessing objective " << *subFormula<< "."); - result.objectives.emplace_back(); - PcaaObjective& currentObjective = result.objectives.back(); - currentObjective.originalFormula = subFormula; - if(currentObjective.originalFormula->isOperatorFormula()) { - preprocessOperatorFormula(currentObjective.originalFormula->asOperatorFormula(), result, currentObjective); - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Could not preprocess the subformula " << *subFormula << " of " << originalFormula << " because it is not supported"); - } - } - // Set the query type. In case of a quantitative query, also set the index of the objective to be optimized. - // Note: If there are only zero (or one) objectives left, we should not consider a pareto query! - storm::storage::BitVector objectivesWithoutThreshold(result.objectives.size()); - for(uint_fast64_t objIndex = 0; objIndex < result.objectives.size(); ++objIndex) { - objectivesWithoutThreshold.set(objIndex, !result.objectives[objIndex].threshold); - } - uint_fast64_t numOfObjectivesWithoutThreshold = objectivesWithoutThreshold.getNumberOfSetBits(); - if(numOfObjectivesWithoutThreshold == 0) { - result.queryType = ReturnType::QueryType::Achievability; - } else if (numOfObjectivesWithoutThreshold == 1) { - result.queryType = ReturnType::QueryType::Quantitative; - result.indexOfOptimizingObjective = objectivesWithoutThreshold.getNextSetIndex(0); - } else if (numOfObjectivesWithoutThreshold == result.objectives.size()) { - result.queryType = ReturnType::QueryType::Pareto; - } else { - STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "The number of objectives without threshold is not valid. It should be either 0 (achievability query), 1 (quantitative query), or " << result.objectives.size() << " (Pareto Query). Got " << numOfObjectivesWithoutThreshold << " instead."); - } - - //We can remove the original reward models to save some memory - std::set origRewardModels = originalFormula.getReferencedRewardModels(); - for (auto const& rewModel : origRewardModels){ - result.preprocessedModel.removeRewardModel(rewModel); - } - - //Get actions to which a positive or negative reward is assigned for at least one objective - result.actionsWithPositiveReward = storm::storage::BitVector(result.preprocessedModel.getNumberOfChoices(), false); - result.actionsWithNegativeReward = storm::storage::BitVector(result.preprocessedModel.getNumberOfChoices(), false); - for(uint_fast64_t objIndex = 0; objIndex < result.objectives.size(); ++objIndex) { - if(!result.objectives[objIndex].upperTimeBound) { - if(result.objectives[objIndex].rewardsArePositive) { - result.actionsWithPositiveReward |= ~storm::utility::vector::filterZero(result.preprocessedModel.getRewardModel(result.objectives[objIndex].rewardModelName).getTotalRewardVector(result.preprocessedModel.getTransitionMatrix())); - } else { - result.actionsWithNegativeReward |= ~storm::utility::vector::filterZero(result.preprocessedModel.getRewardModel(result.objectives[objIndex].rewardModelName).getTotalRewardVector(result.preprocessedModel.getTransitionMatrix())); - } - } - } - - // Analyze End components and ensure reward finiteness. - // Note that this is only necessary if there is at least one objective with no upper time bound - for (auto const& obj : result.objectives) { - if(!obj.upperTimeBound) { - auto backwardTransitions = result.preprocessedModel.getBackwardTransitions(); - analyzeEndComponents(result, backwardTransitions); - ensureRewardFiniteness(result, backwardTransitions); - break; - } - } - return result; - } - - template - void SparsePcaaPreprocessor::updatePreprocessedModel(ReturnType& result, SparseModelType& newPreprocessedModel, std::vector& newToOldStateIndexMapping) { - result.preprocessedModel = std::move(newPreprocessedModel); - // the given newToOldStateIndexMapping reffers to the indices of the former preprocessedModel as 'old indices' - for(auto & preprocessedModelStateIndex : newToOldStateIndexMapping){ - preprocessedModelStateIndex = result.newToOldStateIndexMapping[preprocessedModelStateIndex]; - } - result.newToOldStateIndexMapping = std::move(newToOldStateIndexMapping); - } - - template - void SparsePcaaPreprocessor::preprocessOperatorFormula(storm::logic::OperatorFormula const& formula, ReturnType& result, PcaaObjective& currentObjective) { - - // Get a unique name for the new reward model. - currentObjective.rewardModelName = "objective" + std::to_string(result.objectives.size()); - while(result.preprocessedModel.hasRewardModel(currentObjective.rewardModelName)){ - currentObjective.rewardModelName = "_" + currentObjective.rewardModelName; - } - - currentObjective.toOriginalValueTransformationFactor = storm::utility::one(); - currentObjective.toOriginalValueTransformationOffset = storm::utility::zero(); - currentObjective.rewardsArePositive = true; - - bool formulaMinimizes = false; - if(formula.hasBound()) { - currentObjective.threshold = formula.template getThresholdAs(); - currentObjective.thresholdIsStrict = storm::logic::isStrict(formula.getBound().comparisonType); - //Note that we minimize for upper bounds since we are looking for the EXISTENCE of a satisfying scheduler - formulaMinimizes = !storm::logic::isLowerBound(formula.getBound().comparisonType); - } else if (formula.hasOptimalityType()){ - formulaMinimizes = storm::solver::minimize(formula.getOptimalityType()); - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Current objective " << formula << " does not specify whether to minimize or maximize"); - } - if(formulaMinimizes) { - // We negate all the values so we can consider the maximum for this objective - // Thus, all objectives will be maximized. - currentObjective.rewardsArePositive = false; - currentObjective.toOriginalValueTransformationFactor = -storm::utility::one(); - } - - if(formula.isProbabilityOperatorFormula()){ - preprocessProbabilityOperatorFormula(formula.asProbabilityOperatorFormula(), result, currentObjective); - } else if(formula.isRewardOperatorFormula()){ - preprocessRewardOperatorFormula(formula.asRewardOperatorFormula(), result, currentObjective); - } else if(formula.isTimeOperatorFormula()){ - preprocessTimeOperatorFormula(formula.asTimeOperatorFormula(), result, currentObjective); - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Could not preprocess the objective " << formula << " because it is not supported"); - } - - // Transform the threshold for the preprocessed Model - if(currentObjective.threshold) { - currentObjective.threshold = (currentObjective.threshold.get() - currentObjective.toOriginalValueTransformationOffset) / currentObjective.toOriginalValueTransformationFactor; - } - } - - template - void SparsePcaaPreprocessor::preprocessProbabilityOperatorFormula(storm::logic::ProbabilityOperatorFormula const& formula, ReturnType& result, PcaaObjective& currentObjective) { - - if(formula.getSubformula().isUntilFormula()){ - preprocessUntilFormula(formula.getSubformula().asUntilFormula(), result, currentObjective); - } else if(formula.getSubformula().isBoundedUntilFormula()){ - preprocessBoundedUntilFormula(formula.getSubformula().asBoundedUntilFormula(), result, currentObjective); - } else if(formula.getSubformula().isGloballyFormula()){ - preprocessGloballyFormula(formula.getSubformula().asGloballyFormula(), result, currentObjective); - } else if(formula.getSubformula().isEventuallyFormula()){ - preprocessEventuallyFormula(formula.getSubformula().asEventuallyFormula(), result, currentObjective); - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The subformula of " << formula << " is not supported."); - } - } - - template - void SparsePcaaPreprocessor::preprocessRewardOperatorFormula(storm::logic::RewardOperatorFormula const& formula, ReturnType& result, PcaaObjective& currentObjective) { - // Check if the reward model is uniquely specified - STORM_LOG_THROW((formula.hasRewardModelName() && result.preprocessedModel.hasRewardModel(formula.getRewardModelName())) - || result.preprocessedModel.hasUniqueRewardModel(), storm::exceptions::InvalidPropertyException, "The reward model is not unique and the formula " << formula << " does not specify a reward model."); - - if(formula.getSubformula().isEventuallyFormula()){ - preprocessEventuallyFormula(formula.getSubformula().asEventuallyFormula(), result, currentObjective, formula.getOptionalRewardModelName()); - } else if(formula.getSubformula().isCumulativeRewardFormula()) { - preprocessCumulativeRewardFormula(formula.getSubformula().asCumulativeRewardFormula(), result, currentObjective, formula.getOptionalRewardModelName()); - } else if(formula.getSubformula().isTotalRewardFormula()) { - preprocessTotalRewardFormula(result, currentObjective, formula.getOptionalRewardModelName()); - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The subformula of " << formula << " is not supported."); - } - } - - template - void SparsePcaaPreprocessor::preprocessTimeOperatorFormula(storm::logic::TimeOperatorFormula const& formula, ReturnType& result, PcaaObjective& currentObjective) { - // Time formulas are only supported for Markov automata - STORM_LOG_THROW(result.originalModel.isOfType(storm::models::ModelType::MarkovAutomaton), storm::exceptions::InvalidPropertyException, "Time operator formulas are only supported for Markov automata."); - - if(formula.getSubformula().isEventuallyFormula()){ - preprocessEventuallyFormula(formula.getSubformula().asEventuallyFormula(), result, currentObjective); - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The subformula of " << formula << " is not supported."); - } - } - - template - void SparsePcaaPreprocessor::preprocessUntilFormula(storm::logic::UntilFormula const& formula, ReturnType& result, PcaaObjective& currentObjective) { - CheckTask phiTask(formula.getLeftSubformula()); - CheckTask psiTask(formula.getRightSubformula()); - storm::modelchecker::SparsePropositionalModelChecker mc(result.preprocessedModel); - STORM_LOG_THROW(mc.canHandle(phiTask) && mc.canHandle(psiTask), storm::exceptions::InvalidPropertyException, "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(); - - if(!(psiStates & result.preprocessedModel.getInitialStates()).empty() && !currentObjective.lowerTimeBound) { - // The probability is always one as the initial state is a target state. - // For this special case, the transformation to an expected reward objective fails. - // We could handle this with further preprocessing steps but as this case is boring anyway, we simply reject the input. - STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The Probability for the objective " << currentObjective.originalFormula << " is always one as the rhs of the until formula is true in the initial state. Please omit this objective."); - } - - auto duplicatorResult = storm::transformer::StateDuplicator::transform(result.preprocessedModel, ~phiStates | psiStates); - updatePreprocessedModel(result, *duplicatorResult.model, duplicatorResult.newToOldStateIndexMapping); - - storm::storage::BitVector newPsiStates(result.preprocessedModel.getNumberOfStates(), false); - for(auto const& oldPsiState : psiStates){ - //note that psiStates are always located in the second copy - newPsiStates.set(duplicatorResult.secondCopyOldToNewStateIndexMapping[oldPsiState], true); - } - - // build stateAction reward vector that gives (one*transitionProbability) reward whenever a transition leads from the firstCopy to a psiState - std::vector objectiveRewards(result.preprocessedModel.getTransitionMatrix().getRowCount(), storm::utility::zero()); - for (auto const& firstCopyState : duplicatorResult.firstCopy) { - for (uint_fast64_t row = result.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[firstCopyState]; row < result.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[firstCopyState + 1]; ++row) { - objectiveRewards[row] = result.preprocessedModel.getTransitionMatrix().getConstrainedRowSum(row, newPsiStates); - } - } - if(!currentObjective.rewardsArePositive) { - storm::utility::vector::scaleVectorInPlace(objectiveRewards, -storm::utility::one()); - } - result.preprocessedModel.addRewardModel(currentObjective.rewardModelName, RewardModelType(boost::none, objectiveRewards)); - } - - template - void SparsePcaaPreprocessor::preprocessBoundedUntilFormula(storm::logic::BoundedUntilFormula const& formula, ReturnType& result, PcaaObjective& currentObjective) { - STORM_LOG_THROW(!result.originalModel.isOfType(storm::models::ModelType::MarkovAutomaton) || !formula.isStepBounded(), storm::exceptions::InvalidPropertyException, "Multi-objective model checking currently does not support STEP-bounded properties for Markov automata."); - - if (formula.hasLowerBound()) { - currentObjective.lowerTimeBound = formula.getLowerBound(); - currentObjective.lowerTimeBoundStrict = formula.isLowerBoundStrict(); - } - if (formula.hasUpperBound()) { - currentObjective.upperTimeBound = formula.getUpperBound(); - currentObjective.upperTimeBoundStrict = formula.isUpperBoundStrict(); - } - preprocessUntilFormula(storm::logic::UntilFormula(formula.getLeftSubformula().asSharedPointer(), formula.getRightSubformula().asSharedPointer()), result, currentObjective); - } - - template - void SparsePcaaPreprocessor::preprocessGloballyFormula(storm::logic::GloballyFormula const& formula, ReturnType& result, PcaaObjective& currentObjective) { - // The formula will be transformed to an until formula for the complementary event. - // If the original formula minimizes, the complementary one will maximize and vice versa. - // Hence, the decision whether to consider positive or negative rewards flips. - currentObjective.rewardsArePositive = !currentObjective.rewardsArePositive; - // To transform from the value of the preprocessed model back to the value of the original model, we have to add 1 to the result. - // The transformation factor has already been set correctly. - currentObjective.toOriginalValueTransformationOffset = storm::utility::one(); - - auto negatedSubformula = std::make_shared(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, formula.getSubformula().asSharedPointer()); - - preprocessUntilFormula(storm::logic::UntilFormula(storm::logic::Formula::getTrueFormula(), negatedSubformula), result, currentObjective); - } - - template - void SparsePcaaPreprocessor::preprocessEventuallyFormula(storm::logic::EventuallyFormula const& formula, ReturnType& result, PcaaObjective& currentObjective, boost::optional const& optionalRewardModelName) { - if(formula.isReachabilityProbabilityFormula()){ - preprocessUntilFormula(storm::logic::UntilFormula(storm::logic::Formula::getTrueFormula(), formula.getSubformula().asSharedPointer()), result, currentObjective); - return; - } - - CheckTask targetTask(formula.getSubformula()); - storm::modelchecker::SparsePropositionalModelChecker mc(result.preprocessedModel); - STORM_LOG_THROW(mc.canHandle(targetTask), storm::exceptions::InvalidPropertyException, "The subformula of " << formula << " should be propositional."); - storm::storage::BitVector targetStates = mc.check(targetTask)->asExplicitQualitativeCheckResult().getTruthValuesVector(); - - auto duplicatorResult = storm::transformer::StateDuplicator::transform(result.preprocessedModel, targetStates); - updatePreprocessedModel(result, *duplicatorResult.model, duplicatorResult.newToOldStateIndexMapping); - - // Add a reward model that gives zero reward to the actions of states of the second copy. - RewardModelType objectiveRewards(boost::none); - if(formula.isReachabilityRewardFormula()) { - objectiveRewards = result.preprocessedModel.getRewardModel(optionalRewardModelName ? optionalRewardModelName.get() : ""); - objectiveRewards.reduceToStateBasedRewards(result.preprocessedModel.getTransitionMatrix(), false); - if(objectiveRewards.hasStateRewards()) { - storm::utility::vector::setVectorValues(objectiveRewards.getStateRewardVector(), duplicatorResult.secondCopy, storm::utility::zero()); - } - if(objectiveRewards.hasStateActionRewards()) { - for(auto secondCopyState : duplicatorResult.secondCopy) { - std::fill_n(objectiveRewards.getStateActionRewardVector().begin() + result.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[secondCopyState], result.preprocessedModel.getTransitionMatrix().getRowGroupSize(secondCopyState), storm::utility::zero()); - } - } - } else if(formula.isReachabilityTimeFormula() && result.preprocessedModel.isOfType(storm::models::ModelType::MarkovAutomaton)) { - objectiveRewards = RewardModelType(std::vector(result.preprocessedModel.getNumberOfStates(), storm::utility::zero())); - storm::utility::vector::setVectorValues(objectiveRewards.getStateRewardVector(), dynamic_cast*>(&result.preprocessedModel)->getMarkovianStates() & duplicatorResult.firstCopy, storm::utility::one()); - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The formula " << formula << " neither considers reachability probabilities nor reachability rewards " << (result.preprocessedModel.isOfType(storm::models::ModelType::MarkovAutomaton) ? "nor reachability time" : "") << ". This is not supported."); - } - if(!currentObjective.rewardsArePositive){ - if(objectiveRewards.hasStateRewards()) { - storm::utility::vector::scaleVectorInPlace(objectiveRewards.getStateRewardVector(), -storm::utility::one()); - } - if(objectiveRewards.hasStateActionRewards()) { - storm::utility::vector::scaleVectorInPlace(objectiveRewards.getStateActionRewardVector(), -storm::utility::one()); - } - } - result.preprocessedModel.addRewardModel(currentObjective.rewardModelName, std::move(objectiveRewards)); - } - - template - void SparsePcaaPreprocessor::preprocessCumulativeRewardFormula(storm::logic::CumulativeRewardFormula const& formula, ReturnType& result, PcaaObjective& currentObjective, boost::optional const& optionalRewardModelName) { - STORM_LOG_THROW(result.originalModel.isOfType(storm::models::ModelType::Mdp), storm::exceptions::InvalidPropertyException, "Cumulative reward formulas are not supported for the given model type."); - currentObjective.upperTimeBound = formula.getBound(); - currentObjective.upperTimeBoundStrict = formula.isBoundStrict(); - - RewardModelType objectiveRewards = result.preprocessedModel.getRewardModel(optionalRewardModelName ? optionalRewardModelName.get() : ""); - objectiveRewards.reduceToStateBasedRewards(result.preprocessedModel.getTransitionMatrix(), false); - if(!currentObjective.rewardsArePositive){ - if(objectiveRewards.hasStateRewards()) { - storm::utility::vector::scaleVectorInPlace(objectiveRewards.getStateRewardVector(), -storm::utility::one()); - } - if(objectiveRewards.hasStateActionRewards()) { - storm::utility::vector::scaleVectorInPlace(objectiveRewards.getStateActionRewardVector(), -storm::utility::one()); - } - } - result.preprocessedModel.addRewardModel(currentObjective.rewardModelName, std::move(objectiveRewards)); - } - - template - void SparsePcaaPreprocessor::preprocessTotalRewardFormula(ReturnType& result, PcaaObjective& currentObjective, boost::optional const& optionalRewardModelName) { - RewardModelType objectiveRewards = result.preprocessedModel.getRewardModel(optionalRewardModelName ? optionalRewardModelName.get() : ""); - objectiveRewards.reduceToStateBasedRewards(result.preprocessedModel.getTransitionMatrix(), false); - if(!currentObjective.rewardsArePositive){ - if(objectiveRewards.hasStateRewards()) { - storm::utility::vector::scaleVectorInPlace(objectiveRewards.getStateRewardVector(), -storm::utility::one()); - } - if(objectiveRewards.hasStateActionRewards()) { - storm::utility::vector::scaleVectorInPlace(objectiveRewards.getStateActionRewardVector(), -storm::utility::one()); - } - } - result.preprocessedModel.addRewardModel(currentObjective.rewardModelName, std::move(objectiveRewards)); - } - - - template - void SparsePcaaPreprocessor::analyzeEndComponents(ReturnType& result, storm::storage::SparseMatrix const& backwardTransitions) { - - result.ecActions = storm::storage::BitVector(result.preprocessedModel.getNumberOfChoices(), false); - std::vector ecs; - auto mecDecomposition = storm::storage::MaximalEndComponentDecomposition(result.preprocessedModel.getTransitionMatrix(), backwardTransitions); - STORM_LOG_ASSERT(!mecDecomposition.empty(), "Empty maximal end component decomposition."); - ecs.reserve(mecDecomposition.size()); - for(auto& mec : mecDecomposition) { - for(auto const& stateActionsPair : mec) { - for(auto const& action : stateActionsPair.second) { - result.ecActions.set(action); - } - } - ecs.push_back(std::move(mec)); - } - - result.possiblyRecurrentStates = storm::storage::BitVector(result.preprocessedModel.getNumberOfStates(), false); - storm::storage::BitVector neutralActions = ~(result.actionsWithNegativeReward | result.actionsWithPositiveReward); - storm::storage::BitVector statesInCurrentECWithNeutralAction(result.preprocessedModel.getNumberOfStates(), false); - for(uint_fast64_t ecIndex = 0; ecIndex < ecs.size(); ++ecIndex) { //we will insert new ecs in the vector (thus no iterators for the loop) - bool currentECIsNeutral = true; - for(auto const& stateActionsPair : ecs[ecIndex]) { - bool stateHasNeutralActionWithinEC = false; - for(auto const& action : stateActionsPair.second) { - stateHasNeutralActionWithinEC |= neutralActions.get(action); - } - statesInCurrentECWithNeutralAction.set(stateActionsPair.first, stateHasNeutralActionWithinEC); - currentECIsNeutral &= stateHasNeutralActionWithinEC; - } - if(currentECIsNeutral) { - result.possiblyRecurrentStates |= statesInCurrentECWithNeutralAction; - }else{ - // Check if the ec contains neutral sub ecs. This is done by adding the subECs to our list of ECs - // A neutral subEC only consist of states that can stay in statesInCurrentECWithNeutralAction - statesInCurrentECWithNeutralAction = storm::utility::graph::performProb0E(result.preprocessedModel.getTransitionMatrix(), result.preprocessedModel.getTransitionMatrix().getRowGroupIndices(), backwardTransitions,statesInCurrentECWithNeutralAction, ~statesInCurrentECWithNeutralAction); - auto subECs = storm::storage::MaximalEndComponentDecomposition(result.preprocessedModel.getTransitionMatrix(), backwardTransitions, statesInCurrentECWithNeutralAction); - ecs.reserve(ecs.size() + subECs.size()); - for(auto& ec : subECs){ - ecs.push_back(std::move(ec)); - } - } - statesInCurrentECWithNeutralAction.clear(); - } - } - - template - void SparsePcaaPreprocessor::ensureRewardFiniteness(ReturnType& result, storm::storage::SparseMatrix const& backwardTransitions) { - STORM_LOG_THROW((result.actionsWithPositiveReward & result.ecActions).empty(), storm::exceptions::InvalidPropertyException, "Infinite reward: There is one maximizing objective for which infinite reward is possible. This is not supported."); - - //Check whether the states that can be visited inf. often are reachable with prob. 1 under some scheduler - storm::storage::BitVector statesReachingNegativeRewardsFinitelyOftenForSomeScheduler = storm::utility::graph::performProb1E(result.preprocessedModel.getTransitionMatrix(), result.preprocessedModel.getTransitionMatrix().getRowGroupIndices(), backwardTransitions, storm::storage::BitVector(result.preprocessedModel.getNumberOfStates(), true), result.possiblyRecurrentStates); - STORM_LOG_THROW(!(statesReachingNegativeRewardsFinitelyOftenForSomeScheduler & result.preprocessedModel.getInitialStates()).empty(), storm::exceptions::InvalidPropertyException, "Infinite Rewards: For every scheduler, the induced reward for one or more of the objectives that minimize rewards is infinity."); - - if(!statesReachingNegativeRewardsFinitelyOftenForSomeScheduler.full()) { - // Remove the states that for any scheduler have one objective with infinite expected reward. - auto subsystemBuilderResult = storm::transformer::SubsystemBuilder::transform(result.preprocessedModel, statesReachingNegativeRewardsFinitelyOftenForSomeScheduler, storm::storage::BitVector(result.preprocessedModel.getNumberOfChoices(), true)); - updatePreprocessedModel(result, *subsystemBuilderResult.model, subsystemBuilderResult.newToOldStateIndexMapping); - result.ecActions = result.ecActions % subsystemBuilderResult.keptActions; - result.actionsWithPositiveReward = result.actionsWithPositiveReward % subsystemBuilderResult.keptActions; - result.actionsWithNegativeReward = result.actionsWithNegativeReward % subsystemBuilderResult.keptActions; - result.possiblyRecurrentStates = result.possiblyRecurrentStates % statesReachingNegativeRewardsFinitelyOftenForSomeScheduler; - } - } - - - - template class SparsePcaaPreprocessor>; - template class SparsePcaaPreprocessor>; - -#ifdef STORM_HAVE_CARL - template class SparsePcaaPreprocessor>; - template class SparsePcaaPreprocessor>; -#endif - } - } -} diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.h b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.h deleted file mode 100644 index fb35fa9d1..000000000 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.h +++ /dev/null @@ -1,82 +0,0 @@ -#ifndef STORM_MODELCHECKER_MULTIOBJECTIVE_PCAA_SPARSEPCAAPREPROCESSOR_H_ -#define STORM_MODELCHECKER_MULTIOBJECTIVE_PCAA_SPARSEPCAAPREPROCESSOR_H_ - -#include - -#include "storm/logic/Formulas.h" -#include "storm/storage/BitVector.h" -#include "storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessorReturnType.h" - -namespace storm { - namespace modelchecker { - namespace multiobjective { - - /* - * This class invokes the necessary preprocessing for the Pareto Curve Approximation Algorithm (PCAA) - */ - template - class SparsePcaaPreprocessor { - public: - typedef typename SparseModelType::ValueType ValueType; - typedef typename SparseModelType::RewardModelType RewardModelType; - typedef SparsePcaaPreprocessorReturnType ReturnType; - - /*! - * 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 ReturnType preprocess(SparseModelType const& originalModel, storm::logic::MultiObjectiveFormula const& originalFormula); - - private: - /*! - * Initializes the returned Information - * @param originalModel The considered model - * @param originalFormula the considered formula - */ - static ReturnType initializeResult(storm::logic::MultiObjectiveFormula const& originalFormula, SparseModelType const& originalModel); - - /*! - * Updates the preprocessed model stored in the given result to the given model. - * The given newToOldStateIndexMapping should give for each state in the newPreprocessedModel - * the index of the state in the current result.preprocessedModel. - */ - static void updatePreprocessedModel(ReturnType& result, SparseModelType& newPreprocessedModel, std::vector& newToOldStateIndexMapping); - - /*! - * Apply the neccessary preprocessing for the given formula. - * @param formula the current (sub)formula - * @param result the information collected so far - * @param currentObjective the currently considered objective. The given formula should be a a (sub)formula of this objective - * @param optionalRewardModelName the reward model name that is considered for the formula (if available) - */ - static void preprocessOperatorFormula(storm::logic::OperatorFormula const& formula, ReturnType& result, PcaaObjective& currentObjective); - static void preprocessProbabilityOperatorFormula(storm::logic::ProbabilityOperatorFormula const& formula, ReturnType& result, PcaaObjective& currentObjective); - static void preprocessRewardOperatorFormula(storm::logic::RewardOperatorFormula const& formula, ReturnType& result, PcaaObjective& currentObjective); - static void preprocessTimeOperatorFormula(storm::logic::TimeOperatorFormula const& formula, ReturnType& result, PcaaObjective& currentObjective); - static void preprocessUntilFormula(storm::logic::UntilFormula const& formula, ReturnType& result, PcaaObjective& currentObjective); - static void preprocessBoundedUntilFormula(storm::logic::BoundedUntilFormula const& formula, ReturnType& result, PcaaObjective& currentObjective); - static void preprocessGloballyFormula(storm::logic::GloballyFormula const& formula, ReturnType& result, PcaaObjective& currentObjective); - static void preprocessEventuallyFormula(storm::logic::EventuallyFormula const& formula, ReturnType& result, PcaaObjective& currentObjective, boost::optional const& optionalRewardModelName = boost::none); - static void preprocessCumulativeRewardFormula(storm::logic::CumulativeRewardFormula const& formula, ReturnType& result, PcaaObjective& currentObjective, boost::optional const& optionalRewardModelName = boost::none); - static void preprocessTotalRewardFormula(ReturnType& result, PcaaObjective& currentObjective, boost::optional const& optionalRewardModelName = boost::none); // The total reward formula itself does not need to be provided as it is unique. - - /*! - * Analyzes the end components of the preprocessed model. That is: - * -get the set of actions that are part of an end component - * -Find the states that can be visited infinitely often without inducing infinite reward - */ - static void analyzeEndComponents(ReturnType& result, storm::storage::SparseMatrix const& backwardTransitions); - - /*! - * Checks whether the occurring expected rewards are finite. If not, the input is rejected. - * Also removes all states for which no finite reward wrt. all objectives is possible - */ - static void ensureRewardFiniteness(ReturnType& result, storm::storage::SparseMatrix const& backwardTransitions); - - }; - } - } -} - -#endif /* STORM_MODELCHECKER_MULTIOBJECTIVE_PCAA_SPARSEPCAAPREPROCESSOR_H_ */ diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.cpp index 9dd81014b..d648ae593 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.cpp @@ -8,20 +8,27 @@ #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "storm/utility/constants.h" #include "storm/utility/vector.h" -#include "storm/settings//SettingsManager.h" +#include "storm/settings/SettingsManager.h" #include "storm/settings/modules/MultiObjectiveSettings.h" #include "storm/settings/modules/GeneralSettings.h" +#include "storm/exceptions/InvalidOperationException.h" + namespace storm { namespace modelchecker { namespace multiobjective { template - SparsePcaaQuantitativeQuery::SparsePcaaQuantitativeQuery(SparsePcaaPreprocessorReturnType& preprocessorResult) : SparsePcaaQuery(preprocessorResult) { - STORM_LOG_ASSERT(preprocessorResult.queryType==SparsePcaaPreprocessorReturnType::QueryType::Quantitative, "Invalid query Type"); - STORM_LOG_ASSERT(preprocessorResult.indexOfOptimizingObjective, "Detected quantitative query but index of optimizing objective is not set."); - indexOfOptimizingObjective = *preprocessorResult.indexOfOptimizingObjective; + SparsePcaaQuantitativeQuery::SparsePcaaQuantitativeQuery(SparseMultiObjectivePreprocessorReturnType& preprocessorResult) : SparsePcaaQuery(preprocessorResult) { + STORM_LOG_ASSERT(preprocessorResult.queryType == SparseMultiObjectivePreprocessorReturnType::QueryType::Quantitative, "Invalid query Type"); + + for (uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { + if (!this->objectives[objIndex].bound.is_initialized()) { + indexOfOptimizingObjective = objIndex; + break; + } + } initializeThresholdData(); // Set the maximum distance between lower and upper bound of the weightVectorChecker result. @@ -30,17 +37,26 @@ namespace storm { template void SparsePcaaQuantitativeQuery::initializeThresholdData() { + thresholds.reserve(this->objectives.size()); strictThresholds = storm::storage::BitVector(this->objectives.size(), false); std::vector> thresholdConstraints; thresholdConstraints.reserve(this->objectives.size()-1); - for(uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { - if(this->objectives[objIndex].threshold) { - thresholds.push_back(storm::utility::convertNumber(*this->objectives[objIndex].threshold)); + for (uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { + auto const& obj = this->objectives[objIndex]; + if (obj.bound) { + STORM_LOG_THROW(!obj.bound->threshold.containsVariables(), storm::exceptions::InvalidOperationException, "There is an objective whose bound contains undefined variables."); + thresholds.push_back(storm::utility::convertNumber(obj.bound->threshold.evaluateAsRational())); + if (storm::solver::minimize(obj.optimizationDirection)) { + STORM_LOG_ASSERT(!storm::logic::isLowerBound(obj.bound->comparisonType), "Minimizing objective should not specify an upper bound."); + // Values for minimizing objectives will be negated in order to convert them to maximizing objectives. + // Hence, we also negate the threshold + thresholds.back() *= -storm::utility::one(); + } + strictThresholds.set(objIndex, storm::logic::isStrict(obj.bound->comparisonType)); WeightVector normalVector(this->objectives.size(), storm::utility::zero()); normalVector[objIndex] = -storm::utility::one(); thresholdConstraints.emplace_back(std::move(normalVector), -thresholds.back()); - strictThresholds.set(objIndex, this->objectives[objIndex].thresholdIsStrict); } else { thresholds.push_back(storm::utility::zero()); } @@ -52,26 +68,34 @@ namespace storm { template std::unique_ptr SparsePcaaQuantitativeQuery::check() { // First find one solution that achieves the given thresholds ... - if(this->checkAchievability()) { + if (this->checkAchievability()) { // ... then improve it GeometryValueType result = this->improveSolution(); // transform the obtained result for the preprocessed model to a result w.r.t. the original model and return the checkresult - typename SparseModelType::ValueType resultForOriginalModel = - storm::utility::convertNumber(result) * - this->objectives[indexOfOptimizingObjective].toOriginalValueTransformationFactor + - this->objectives[indexOfOptimizingObjective].toOriginalValueTransformationOffset; + auto const& obj = this->objectives[indexOfOptimizingObjective]; + if (storm::solver::maximize(obj.optimizationDirection)) { + if (obj.considersComplementaryEvent) { + result = storm::utility::one() - result; + } + } else { + if (obj.considersComplementaryEvent) { + result = storm::utility::one() + result; // 1 - (-result) + } else { + result *= -storm::utility::one(); + } + } + auto resultForOriginalModel = storm::utility::convertNumber(result); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(this->originalModel.getInitialStates().getNextSetIndex(0), resultForOriginalModel)); } else { return std::unique_ptr(new ExplicitQualitativeCheckResult(this->originalModel.getInitialStates().getNextSetIndex(0), false)); } - - } template bool SparsePcaaQuantitativeQuery::checkAchievability() { - if(this->objectives.size()>1) { + if (this->objectives.size()>1) { // We don't care for the optimizing objective at this point this->diracWeightVectorsToBeChecked.set(indexOfOptimizingObjective, false); @@ -81,10 +105,10 @@ namespace storm { this->performRefinementStep(std::move(separatingVector)); //Pick the threshold for the optimizing objective low enough so valid solutions are not excluded thresholds[indexOfOptimizingObjective] = std::min(thresholds[indexOfOptimizingObjective], this->refinementSteps.back().lowerBoundPoint[indexOfOptimizingObjective]); - if(!checkIfThresholdsAreSatisfied(this->overApproximation)){ + if (!checkIfThresholdsAreSatisfied(this->overApproximation)){ return false; } - if(checkIfThresholdsAreSatisfied(this->underApproximation)){ + if (checkIfThresholdsAreSatisfied(this->underApproximation)){ return true; } } @@ -100,9 +124,9 @@ namespace storm { void SparsePcaaQuantitativeQuery::updateWeightedPrecisionInAchievabilityPhase(WeightVector const& weights) { // Our heuristic considers the distance between the under- and the over approximation w.r.t. the given direction std::pair optimizationResOverApprox = this->overApproximation->optimize(weights); - if(optimizationResOverApprox.second) { + if (optimizationResOverApprox.second) { std::pair optimizationResUnderApprox = this->underApproximation->optimize(weights); - if(optimizationResUnderApprox.second) { + if (optimizationResUnderApprox.second) { GeometryValueType distance = storm::utility::vector::dotProduct(optimizationResOverApprox.first, weights) - storm::utility::vector::dotProduct(optimizationResUnderApprox.first, weights); STORM_LOG_ASSERT(distance >= storm::utility::zero(), "Negative distance between under- and over approximation was not expected"); // Normalize the distance by dividing it with the Euclidean Norm of the weight-vector @@ -127,7 +151,7 @@ namespace storm { // thresholds) and (with very low probability) a scheduler that satisfies all (possibly strict) thresholds. GeometryValueType result = storm::utility::zero(); while(!this->maxStepsPerformed()) { - if(this->refinementSteps.empty()) { + if (this->refinementSteps.empty()) { // We did not make any refinement steps during the checkAchievability phase (e.g., because there is only one objective). this->weightVectorChecker->setWeightedPrecision(storm::utility::convertNumber(storm::settings::getModule().getPrecision())); WeightVector separatingVector = directionOfOptimizingObjective; @@ -139,9 +163,9 @@ namespace storm { STORM_LOG_DEBUG("Best solution found so far is ~" << storm::utility::convertNumber(result) << "."); //Compute an upper bound for the optimum and check for convergence optimizationRes = this->overApproximation->intersection(thresholdsAsPolytope)->optimize(directionOfOptimizingObjective); - if(optimizationRes.second) { + if (optimizationRes.second) { GeometryValueType precisionOfResult = optimizationRes.first[indexOfOptimizingObjective] - result; - if(precisionOfResult < storm::utility::convertNumber(storm::settings::getModule().getPrecision())) { + if (precisionOfResult < storm::utility::convertNumber(storm::settings::getModule().getPrecision())) { // Goal precision reached! return result; } else { @@ -177,12 +201,12 @@ namespace storm { template bool SparsePcaaQuantitativeQuery::checkIfThresholdsAreSatisfied(std::shared_ptr> const& polytope) { std::vector> halfspaces = polytope->getHalfspaces(); - for(auto const& h : halfspaces) { - if(storm::utility::isZero(h.distance(thresholds))) { + for (auto const& h : halfspaces) { + if (storm::utility::isZero(h.distance(thresholds))) { // Check if the threshold point is on the boundary of the halfspace and whether this is violates strict thresholds - if(h.isPointOnBoundary(thresholds)) { - for(auto strictThreshold : strictThresholds) { - if(h.normalVector()[strictThreshold] > storm::utility::zero()) { + if (h.isPointOnBoundary(thresholds)) { + for (auto strictThreshold : strictThresholds) { + if (h.normalVector()[strictThreshold] > storm::utility::zero()) { return false; } } diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.h b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.h index ca2d8c81a..d28ea4e9f 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.h +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.h @@ -23,7 +23,7 @@ namespace storm { * Creates a new query for the Pareto curve approximation algorithm (Pcaa) * @param preprocessorResult the result from preprocessing */ - SparsePcaaQuantitativeQuery(SparsePcaaPreprocessorReturnType& preprocessorResult); + SparsePcaaQuantitativeQuery(SparseMultiObjectivePreprocessorReturnType& preprocessorResult); virtual ~SparsePcaaQuantitativeQuery() = default; diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp index 10652dd07..7ef64df2e 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp @@ -4,10 +4,10 @@ #include "storm/models/sparse/Mdp.h" #include "storm/models/sparse/MarkovAutomaton.h" #include "storm/models/sparse/StandardRewardModel.h" -#include "storm/modelchecker/multiobjective/pcaa/PcaaObjective.h" +#include "storm/modelchecker/multiobjective/Objective.h" #include "storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.h" #include "storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.h" -#include "storm/settings//SettingsManager.h" +#include "storm/settings/SettingsManager.h" #include "storm/settings/modules/MultiObjectiveSettings.h" #include "storm/storage/geometry/Hyperrectangle.h" #include "storm/utility/constants.h" @@ -22,35 +22,37 @@ namespace storm { template - SparsePcaaQuery::SparsePcaaQuery(SparsePcaaPreprocessorReturnType& preprocessorResult) : + SparsePcaaQuery::SparsePcaaQuery(SparseMultiObjectivePreprocessorReturnType& preprocessorResult) : originalModel(preprocessorResult.originalModel), originalFormula(preprocessorResult.originalFormula), - preprocessedModel(std::move(preprocessorResult.preprocessedModel)), objectives(std::move(preprocessorResult.objectives)) { - initializeWeightVectorChecker(preprocessedModel, objectives, preprocessorResult.actionsWithNegativeReward, preprocessorResult.ecActions, preprocessorResult.possiblyRecurrentStates); + preprocessedModel(std::move(*preprocessorResult.preprocessedModel)), objectives(std::move(preprocessorResult.objectives)) { + + initializeWeightVectorChecker(preprocessedModel, objectives, preprocessorResult.possibleECChoices, preprocessorResult.possibleBottomStates); this->diracWeightVectorsToBeChecked = storm::storage::BitVector(this->objectives.size(), true); this->overApproximation = storm::storage::geometry::Polytope::createUniversalPolytope(); this->underApproximation = storm::storage::geometry::Polytope::createEmptyPolytope(); } template<> - void SparsePcaaQuery, storm::RationalNumber>::initializeWeightVectorChecker(storm::models::sparse::Mdp const& model, std::vector> const& objectives, storm::storage::BitVector const& actionsWithNegativeReward, storm::storage::BitVector const& ecActions, storm::storage::BitVector const& possiblyRecurrentStates) { - this->weightVectorChecker = std::unique_ptr>>(new SparseMdpPcaaWeightVectorChecker>(model, objectives, actionsWithNegativeReward, ecActions, possiblyRecurrentStates)); + void SparsePcaaQuery, storm::RationalNumber>::initializeWeightVectorChecker(storm::models::sparse::Mdp const& model, std::vector> const& objectives, storm::storage::BitVector const& possibleECActions, storm::storage::BitVector const& possibleBottomStates) { + this->weightVectorChecker = std::unique_ptr>>(new SparseMdpPcaaWeightVectorChecker>(model, objectives, possibleECActions, possibleBottomStates)); } template<> - void SparsePcaaQuery, storm::RationalNumber>::initializeWeightVectorChecker(storm::models::sparse::Mdp const& model, std::vector> const& objectives, storm::storage::BitVector const& actionsWithNegativeReward, storm::storage::BitVector const& ecActions, storm::storage::BitVector const& possiblyRecurrentStates) { - this->weightVectorChecker = std::unique_ptr>>(new SparseMdpPcaaWeightVectorChecker>(model, objectives, actionsWithNegativeReward, ecActions, possiblyRecurrentStates)); + void SparsePcaaQuery, storm::RationalNumber>::initializeWeightVectorChecker(storm::models::sparse::Mdp const& model, std::vector> const& objectives, storm::storage::BitVector const& possibleECActions, storm::storage::BitVector const& possibleBottomStates) { + this->weightVectorChecker = std::unique_ptr>>(new SparseMdpPcaaWeightVectorChecker>(model, objectives, possibleECActions, possibleBottomStates)); } template<> - void SparsePcaaQuery, storm::RationalNumber>::initializeWeightVectorChecker(storm::models::sparse::MarkovAutomaton const& model, std::vector> const& objectives, storm::storage::BitVector const& actionsWithNegativeReward, storm::storage::BitVector const& ecActions, storm::storage::BitVector const& possiblyRecurrentStates) { - this->weightVectorChecker = std::unique_ptr>>(new SparseMaPcaaWeightVectorChecker>(model, objectives, actionsWithNegativeReward, ecActions, possiblyRecurrentStates)); + void SparsePcaaQuery, storm::RationalNumber>::initializeWeightVectorChecker(storm::models::sparse::MarkovAutomaton const& model, std::vector> const& objectives, storm::storage::BitVector const& possibleECActions, storm::storage::BitVector const& possibleBottomStates) { + this->weightVectorChecker = std::unique_ptr>>(new SparseMaPcaaWeightVectorChecker>(model, objectives, possibleECActions, possibleBottomStates)); } template<> - void SparsePcaaQuery, storm::RationalNumber>::initializeWeightVectorChecker(storm::models::sparse::MarkovAutomaton const& model, std::vector> const& objectives, storm::storage::BitVector const& actionsWithNegativeReward, storm::storage::BitVector const& ecActions, storm::storage::BitVector const& possiblyRecurrentStates) { - this->weightVectorChecker = std::unique_ptr>>(new SparseMaPcaaWeightVectorChecker>(model, objectives, actionsWithNegativeReward, ecActions, possiblyRecurrentStates)); + void SparsePcaaQuery, storm::RationalNumber>::initializeWeightVectorChecker(storm::models::sparse::MarkovAutomaton const& model, std::vector> const& objectives, storm::storage::BitVector const& possibleECActions, storm::storage::BitVector const& possibleBottomStates) { + this->weightVectorChecker = std::unique_ptr>>(new SparseMaPcaaWeightVectorChecker>(model, objectives, possibleECActions, possibleBottomStates)); } + template typename SparsePcaaQuery::WeightVector SparsePcaaQuery::findSeparatingVector(Point const& pointToBeSeparated) { STORM_LOG_DEBUG("Searching a weight vector to seperate the point given by " << storm::utility::vector::toString(storm::utility::vector::convertNumericVector(pointToBeSeparated)) << "."); @@ -98,11 +100,18 @@ namespace storm { // Normalize the direction vector so that the entries sum up to one storm::utility::vector::scaleVectorInPlace(direction, storm::utility::one() / std::accumulate(direction.begin(), direction.end(), storm::utility::zero())); weightVectorChecker->check(storm::utility::vector::convertNumericVector(direction)); - STORM_LOG_DEBUG("weighted objectives checker result (lower bounds) is " << storm::utility::vector::toString(storm::utility::vector::convertNumericVector(weightVectorChecker->getLowerBoundsOfInitialStateResults()))); + STORM_LOG_DEBUG("weighted objectives checker result (under approximation) is " << storm::utility::vector::toString(storm::utility::vector::convertNumericVector(weightVectorChecker->getUnderApproximationOfInitialStateResults()))); RefinementStep step; step.weightVector = direction; - step.lowerBoundPoint = storm::utility::vector::convertNumericVector(weightVectorChecker->getLowerBoundsOfInitialStateResults()); - step.upperBoundPoint = storm::utility::vector::convertNumericVector(weightVectorChecker->getUpperBoundsOfInitialStateResults()); + step.lowerBoundPoint = storm::utility::vector::convertNumericVector(weightVectorChecker->getUnderApproximationOfInitialStateResults()); + step.upperBoundPoint = storm::utility::vector::convertNumericVector(weightVectorChecker->getOverApproximationOfInitialStateResults()); + // For the minimizing objectives, we need to scale the corresponding entries with -1 as we want to consider the downward closure + for (uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { + if (storm::solver::minimize(this->objectives[objIndex].optimizationDirection)) { + step.lowerBoundPoint[objIndex] *= -storm::utility::one(); + step.upperBoundPoint[objIndex] *= -storm::utility::one(); + } + } refinementSteps.push_back(std::move(step)); updateOverApproximation(); @@ -151,7 +160,20 @@ namespace storm { Point result; result.reserve(point.size()); for(uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { - result.push_back(point[objIndex] * storm::utility::convertNumber(this->objectives[objIndex].toOriginalValueTransformationFactor) + storm::utility::convertNumber(this->objectives[objIndex].toOriginalValueTransformationOffset)); + auto const& obj = this->objectives[objIndex]; + if (storm::solver::maximize(obj.optimizationDirection)) { + if (obj.considersComplementaryEvent) { + result.push_back(storm::utility::one() - point[objIndex]); + } else { + result.push_back(point[objIndex]); + } + } else { + if (obj.considersComplementaryEvent) { + result.push_back(storm::utility::one() + point[objIndex]); + } else { + result.push_back(-point[objIndex]); + } + } } return result; } @@ -169,8 +191,24 @@ namespace storm { std::vector transformationVector; transformationVector.reserve(numObjectives); for(uint_fast64_t objIndex = 0; objIndex < numObjectives; ++objIndex) { - transformationMatrix[objIndex][objIndex] = storm::utility::convertNumber(this->objectives[objIndex].toOriginalValueTransformationFactor); - transformationVector.push_back(storm::utility::convertNumber(this->objectives[objIndex].toOriginalValueTransformationOffset)); + auto const& obj = this->objectives[objIndex]; + if (storm::solver::maximize(obj.optimizationDirection)) { + if (obj.considersComplementaryEvent) { + transformationMatrix[objIndex][objIndex] = -storm::utility::one(); + transformationVector.push_back(storm::utility::one()); + } else { + transformationMatrix[objIndex][objIndex] = storm::utility::one(); + transformationVector.push_back(storm::utility::zero()); + } + } else { + if (obj.considersComplementaryEvent) { + transformationMatrix[objIndex][objIndex] = storm::utility::one(); + transformationVector.push_back(storm::utility::one()); + } else { + transformationMatrix[objIndex][objIndex] = -storm::utility::one(); + transformationVector.push_back(storm::utility::zero()); + } + } } return polytope->affineTransformation(transformationMatrix, transformationVector); } diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.h b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.h index e6404c9ac..b652af562 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.h +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.h @@ -2,7 +2,7 @@ #define STORM_MODELCHECKER_MULTIOBJECTIVE_PCAA_SPARSEPCAAQUERY_H_ #include "storm/modelchecker/results/CheckResult.h" -#include "storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessorReturnType.h" +#include "storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorReturnType.h" #include "storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h" #include "storm/storage/geometry/Polytope.h" @@ -43,10 +43,9 @@ namespace storm { * Initializes the weight vector checker with the provided data from preprocessing */ void initializeWeightVectorChecker(SparseModelType const& model, - std::vector> const& objectives, - storm::storage::BitVector const& actionsWithNegativeReward, - storm::storage::BitVector const& ecActions, - storm::storage::BitVector const& possiblyRecurrentStates); + std::vector> const& objectives, + storm::storage::BitVector const& possibleECActions, + storm::storage::BitVector const& possibleBottomStates); /* * Represents the information obtained in a single iteration of the algorithm @@ -61,7 +60,7 @@ namespace storm { * Creates a new query for the Pareto curve approximation algorithm (Pcaa) * @param preprocessorResult the result from preprocessing */ - SparsePcaaQuery(SparsePcaaPreprocessorReturnType& preprocessorResult); + SparsePcaaQuery(SparseMultiObjectivePreprocessorReturnType& preprocessorResult); /* * Returns a weight vector w that separates the under approximation from the given point p, i.e., @@ -96,7 +95,7 @@ namespace storm { bool maxStepsPerformed() const; /* - * Transforms the given point (or polytope) to values w.r.t. the original model (e.g. negates negative rewards for minimizing objectives). + * Transforms the given point (or polytope) to values w.r.t. the original model/formula (e.g. negates values for minimizing objectives). */ Point transformPointToOriginalModel(Point const& polytope) const; std::shared_ptr> transformPolytopeToOriginalModel(std::shared_ptr> const& polytope) const; @@ -106,8 +105,7 @@ namespace storm { storm::logic::MultiObjectiveFormula const& originalFormula; SparseModelType preprocessedModel; - std::vector> objectives; - + std::vector> objectives; // The corresponding weight vector checker std::unique_ptr> weightVectorChecker; diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp index d93cedab8..3087ef7a1 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp @@ -24,25 +24,28 @@ namespace storm { template SparsePcaaWeightVectorChecker::SparsePcaaWeightVectorChecker(SparseModelType const& model, - std::vector> const& objectives, - storm::storage::BitVector const& actionsWithNegativeReward, - storm::storage::BitVector const& ecActions, - storm::storage::BitVector const& possiblyRecurrentStates) : + std::vector> const& objectives, + storm::storage::BitVector const& possibleECActions, + storm::storage::BitVector const& possibleBottomStates) : model(model), objectives(objectives), - actionsWithNegativeReward(actionsWithNegativeReward), - ecActions(ecActions), - possiblyRecurrentStates(possiblyRecurrentStates), - objectivesWithNoUpperTimeBound(objectives.size()), + possibleECActions(possibleECActions), + actionsWithoutRewardInUnboundedPhase(model.getNumberOfChoices(), true), + possibleBottomStates(possibleBottomStates), + objectivesWithNoUpperTimeBound(objectives.size(), false), discreteActionRewards(objectives.size()), checkHasBeenCalled(false), objectiveResults(objectives.size()), - offsetsToLowerBound(objectives.size()), - offsetsToUpperBound(objectives.size()) { + offsetsToUnderApproximation(objectives.size()), + offsetsToOverApproximation(objectives.size()) { - // set the unbounded objectives + // set data for unbounded objectives for(uint_fast64_t objIndex = 0; objIndex < objectives.size(); ++objIndex) { - objectivesWithNoUpperTimeBound.set(objIndex, !objectives[objIndex].upperTimeBound); + auto const& obj = objectives[objIndex]; + if (!obj.upperTimeBound) { + objectivesWithNoUpperTimeBound.set(objIndex, true); + actionsWithoutRewardInUnboundedPhase &= model.getRewardModel(*obj.rewardModelName).getChoicesWithZeroReward(model.getTransitionMatrix()); + } } } @@ -52,10 +55,37 @@ namespace storm { checkHasBeenCalled=true; STORM_LOG_INFO("Invoked WeightVectorChecker with weights " << std::endl << "\t" << storm::utility::vector::toString(storm::utility::vector::convertNumericVector(weightVector))); std::vector weightedRewardVector(model.getTransitionMatrix().getRowCount(), storm::utility::zero()); - for(auto objIndex : objectivesWithNoUpperTimeBound) { - storm::utility::vector::addScaledVector(weightedRewardVector, discreteActionRewards[objIndex], weightVector[objIndex]); + boost::optional weightedLowerResultBound = storm::utility::zero(); + boost::optional weightedUpperResultBound = storm::utility::zero(); + for (auto objIndex : objectivesWithNoUpperTimeBound) { + if (storm::solver::minimize(objectives[objIndex].optimizationDirection)) { + if (objectives[objIndex].lowerResultBound && weightedUpperResultBound) { + weightedUpperResultBound.get() -= weightVector[objIndex] * objectives[objIndex].lowerResultBound.get(); + } else { + weightedUpperResultBound = boost::none; + } + if (objectives[objIndex].upperResultBound && weightedLowerResultBound) { + weightedLowerResultBound.get() -= weightVector[objIndex] * objectives[objIndex].upperResultBound.get(); + } else { + weightedLowerResultBound = boost::none; + } + storm::utility::vector::addScaledVector(weightedRewardVector, discreteActionRewards[objIndex], -weightVector[objIndex]); + } else { + if (objectives[objIndex].lowerResultBound && weightedLowerResultBound) { + weightedLowerResultBound.get() += weightVector[objIndex] * objectives[objIndex].lowerResultBound.get(); + } else { + weightedLowerResultBound = boost::none; + } + if (objectives[objIndex].upperResultBound && weightedUpperResultBound) { + weightedUpperResultBound.get() += weightVector[objIndex] * objectives[objIndex].upperResultBound.get(); + } else { + weightedUpperResultBound = boost::none; + } + storm::utility::vector::addScaledVector(weightedRewardVector, discreteActionRewards[objIndex], weightVector[objIndex]); + } } - unboundedWeightedPhase(weightedRewardVector); + + unboundedWeightedPhase(weightedRewardVector, weightedLowerResultBound, weightedUpperResultBound); unboundedIndividualPhase(weightVector); // Only invoke boundedPhase if necessarry, i.e., if there is at least one objective with a time bound for(auto const& obj : this->objectives) { @@ -64,10 +94,9 @@ namespace storm { break; } } - STORM_LOG_INFO("Weight vector check done. Lower bounds for results in initial state: " << storm::utility::vector::toString(storm::utility::vector::convertNumericVector(getLowerBoundsOfInitialStateResults()))); + STORM_LOG_INFO("Weight vector check done. Lower bounds for results in initial state: " << storm::utility::vector::toString(storm::utility::vector::convertNumericVector(getUnderApproximationOfInitialStateResults()))); // Validate that the results are sufficiently precise - ValueType resultingWeightedPrecision = storm::utility::vector::dotProduct(getUpperBoundsOfInitialStateResults(), weightVector) - storm::utility::vector::dotProduct(getLowerBoundsOfInitialStateResults(), weightVector); - STORM_LOG_THROW(resultingWeightedPrecision >= storm::utility::zero(), storm::exceptions::UnexpectedException, "The distance between the lower and the upper result is negative."); + ValueType resultingWeightedPrecision = storm::utility::abs(storm::utility::vector::dotProduct(getOverApproximationOfInitialStateResults(), weightVector) - storm::utility::vector::dotProduct(getUnderApproximationOfInitialStateResults(), weightVector)); resultingWeightedPrecision /= storm::utility::sqrt(storm::utility::vector::dotProduct(weightVector, weightVector)); STORM_LOG_THROW(resultingWeightedPrecision <= weightedPrecision, storm::exceptions::UnexpectedException, "The desired precision was not reached"); } @@ -83,25 +112,25 @@ namespace storm { } template - std::vector::ValueType> SparsePcaaWeightVectorChecker::getLowerBoundsOfInitialStateResults() const { + std::vector::ValueType> SparsePcaaWeightVectorChecker::getUnderApproximationOfInitialStateResults() const { STORM_LOG_THROW(checkHasBeenCalled, storm::exceptions::IllegalFunctionCallException, "Tried to retrieve results but check(..) has not been called before."); uint_fast64_t initstate = *this->model.getInitialStates().begin(); std::vector res; res.reserve(this->objectives.size()); for(uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { - res.push_back(this->objectiveResults[objIndex][initstate] + this->offsetsToLowerBound[objIndex]); + res.push_back(this->objectiveResults[objIndex][initstate] + this->offsetsToUnderApproximation[objIndex]); } return res; } template - std::vector::ValueType> SparsePcaaWeightVectorChecker::getUpperBoundsOfInitialStateResults() const { + std::vector::ValueType> SparsePcaaWeightVectorChecker::getOverApproximationOfInitialStateResults() const { STORM_LOG_THROW(checkHasBeenCalled, storm::exceptions::IllegalFunctionCallException, "Tried to retrieve results but check(..) has not been called before."); uint_fast64_t initstate = *this->model.getInitialStates().begin(); std::vector res; res.reserve(this->objectives.size()); for(uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { - res.push_back(this->objectiveResults[objIndex][initstate] + this->offsetsToUpperBound[objIndex]); + res.push_back(this->objectiveResults[objIndex][initstate] + this->offsetsToOverApproximation[objIndex]); } return res; } @@ -116,14 +145,13 @@ namespace storm { } template - void SparsePcaaWeightVectorChecker::unboundedWeightedPhase(std::vector const& weightedRewardVector) { + void SparsePcaaWeightVectorChecker::unboundedWeightedPhase(std::vector const& weightedRewardVector, boost::optional const& lowerResultBound, boost::optional const& upperResultBound) { if(this->objectivesWithNoUpperTimeBound.empty() || !storm::utility::vector::hasNonZeroEntry(weightedRewardVector)) { this->weightedResult = std::vector(model.getNumberOfStates(), storm::utility::zero()); this->scheduler = storm::storage::TotalScheduler(model.getNumberOfStates()); return; } - // Only consider the states from which a transition with non-zero reward is reachable. (The remaining states always have reward zero). storm::storage::BitVector zeroRewardActions = storm::utility::vector::filterZero(weightedRewardVector); storm::storage::BitVector nonZeroRewardActions = ~zeroRewardActions; @@ -136,7 +164,7 @@ namespace storm { storm::storage::BitVector subsystemStates = storm::utility::graph::performProbGreater0E(model.getTransitionMatrix().transpose(true), storm::storage::BitVector(model.getNumberOfStates(), true), nonZeroRewardStates); // Remove neutral end components, i.e., ECs in which no reward is earned. - auto ecEliminatorResult = storm::transformer::EndComponentEliminator::transform(model.getTransitionMatrix(), subsystemStates, ecActions & zeroRewardActions, possiblyRecurrentStates); + auto ecEliminatorResult = storm::transformer::EndComponentEliminator::transform(model.getTransitionMatrix(), subsystemStates, possibleECActions & zeroRewardActions, possibleBottomStates); std::vector subRewardVector(ecEliminatorResult.newToOldRowMapping.size()); storm::utility::vector::selectVectorValues(subRewardVector, ecEliminatorResult.newToOldRowMapping, weightedRewardVector); @@ -146,6 +174,12 @@ namespace storm { std::unique_ptr> solver = solverFactory.create(ecEliminatorResult.matrix); solver->setOptimizationDirection(storm::solver::OptimizationDirection::Maximize); solver->setTrackScheduler(true); + if (lowerResultBound) { + solver->setLowerBound(*lowerResultBound); + } + if (upperResultBound) { + solver->setUpperBound(*upperResultBound); + } solver->solveEquations(subResult, subRewardVector); this->weightedResult = std::vector(model.getNumberOfStates()); @@ -158,10 +192,14 @@ namespace storm { template void SparsePcaaWeightVectorChecker::unboundedIndividualPhase(std::vector const& weightVector) { - if(objectivesWithNoUpperTimeBound.getNumberOfSetBits() == 1 && storm::utility::isOne(weightVector[*objectivesWithNoUpperTimeBound.begin()])) { - objectiveResults[*objectivesWithNoUpperTimeBound.begin()] = weightedResult; + if (objectivesWithNoUpperTimeBound.getNumberOfSetBits() == 1 && storm::utility::isOne(weightVector[*objectivesWithNoUpperTimeBound.begin()])) { + uint_fast64_t objIndex = *objectivesWithNoUpperTimeBound.begin(); + objectiveResults[objIndex] = weightedResult; + if (storm::solver::minimize(objectives[objIndex].optimizationDirection)) { + storm::utility::vector::scaleVectorInPlace(objectiveResults[objIndex], -storm::utility::one()); + } for (uint_fast64_t objIndex2 = 0; objIndex2 < objectives.size(); ++objIndex2) { - if(*objectivesWithNoUpperTimeBound.begin() != objIndex2) { + if (objIndex != objIndex2) { objectiveResults[objIndex2] = std::vector(model.getNumberOfStates(), storm::utility::zero()); } } @@ -177,9 +215,10 @@ namespace storm { ValueType sumOfWeightsOfUncheckedObjectives = storm::utility::vector::sum_if(weightVector, objectivesWithNoUpperTimeBound); for (uint_fast64_t const &objIndex : storm::utility::vector::getSortedIndices(weightVector)) { + auto const& obj = objectives[objIndex]; if (objectivesWithNoUpperTimeBound.get(objIndex)) { - offsetsToLowerBound[objIndex] = storm::utility::zero(); - offsetsToUpperBound[objIndex] = storm::utility::zero(); + offsetsToUnderApproximation[objIndex] = storm::utility::zero(); + offsetsToOverApproximation[objIndex] = storm::utility::zero(); storm::utility::vector::selectVectorValues(deterministicStateRewards, this->scheduler.getChoices(), model.getTransitionMatrix().getRowGroupIndices(), discreteActionRewards[objIndex]); storm::storage::BitVector statesWithRewards = ~storm::utility::vector::filterZero(deterministicStateRewards); // As maybestates we pick the states from which a state with reward is reachable @@ -188,7 +227,12 @@ namespace storm { // Compute the estimate for this objective if (!storm::utility::isZero(weightVector[objIndex])) { objectiveResults[objIndex] = weightedSumOfUncheckedObjectives; - storm::utility::vector::scaleVectorInPlace(objectiveResults[objIndex], storm::utility::one() / sumOfWeightsOfUncheckedObjectives); + ValueType scalingFactor = storm::utility::one() / sumOfWeightsOfUncheckedObjectives; + if (storm::solver::minimize(obj.optimizationDirection)) { + scalingFactor *= -storm::utility::one(); + } + storm::utility::vector::scaleVectorInPlace(objectiveResults[objIndex], scalingFactor); + storm::utility::vector::clip(objectiveResults[objIndex], obj.lowerResultBound, obj.upperResultBound); } // Make sure that the objectiveResult is initialized correctly objectiveResults[objIndex].resize(model.getNumberOfStates(), storm::utility::zero()); @@ -206,6 +250,12 @@ namespace storm { // Now solve the resulting equation system. std::unique_ptr> solver = linearEquationSolverFactory.create(std::move(submatrix)); + if (obj.lowerResultBound) { + solver->setLowerBound(*obj.lowerResultBound); + } + if (obj.upperResultBound) { + solver->setUpperBound(*obj.upperResultBound); + } solver->solveEquations(x, b); // Set the result for this objective accordingly @@ -234,7 +284,7 @@ namespace storm { std::vector& originalSolution, std::vector& originalOptimalChoices) const { - storm::storage::BitVector recurrentStates(model.getTransitionMatrix().getRowGroupCount(), false); + storm::storage::BitVector bottomStates(model.getTransitionMatrix().getRowGroupCount(), false); storm::storage::BitVector statesThatShouldStayInTheirEC(model.getTransitionMatrix().getRowGroupCount(), false); storm::storage::BitVector statesWithUndefSched(model.getTransitionMatrix().getRowGroupCount(), false); @@ -247,13 +297,13 @@ namespace storm { originalSolution[state] = reducedSolution[stateInReducedModel]; uint_fast64_t chosenRowInReducedModel = reducedMatrix.getRowGroupIndices()[stateInReducedModel] + reducedOptimalChoices[stateInReducedModel]; uint_fast64_t chosenRowInOriginalModel = reducedToOriginalChoiceMapping[chosenRowInReducedModel]; - // Check if the state is recurrent, i.e., the chosen row stays inside this EC. - bool stateIsRecurrent = possiblyRecurrentStates.get(state); + // Check if the state is a bottom state, i.e., the chosen row stays inside its EC. + bool stateIsBottom = possibleBottomStates.get(state); for(auto const& entry : model.getTransitionMatrix().getRow(chosenRowInOriginalModel)) { - stateIsRecurrent &= originalToReducedStateMapping[entry.getColumn()] == stateInReducedModel; + stateIsBottom &= originalToReducedStateMapping[entry.getColumn()] == stateInReducedModel; } - if(stateIsRecurrent) { - recurrentStates.set(state); + if(stateIsBottom) { + bottomStates.set(state); statesThatShouldStayInTheirEC.set(state); } else { // Check if the chosen row originaly belonged to the current state (and not to another state of the EC) @@ -269,42 +319,41 @@ namespace storm { // if the state does not exist in the reduced model, it means that the (weighted) result is always zero, independent of the scheduler. originalSolution[state] = storm::utility::zero(); // However, it might be the case that infinite reward is induced for an objective with weight 0. - // To avoid this, all possibly recurrent states are made recurrent and the remaining states have to reach a recurrent state with prob. one - if(possiblyRecurrentStates.get(state)) { - recurrentStates.set(state); + // To avoid this, all possible bottom states are made bottom and the remaining states have to reach a bottom state with prob. one + if(possibleBottomStates.get(state)) { + bottomStates.set(state); } else { statesWithUndefSched.set(state); } } } - // Handle recurrent states - for(auto state : recurrentStates) { + // Handle bottom states + for(auto state : bottomStates) { bool foundRowForState = false; - // Find a row with zero rewards that only leads to recurrent states. + // Find a row with zero rewards that only leads to bottom states. // If the state should stay in its EC, we also need to make sure that all successors map to the same state in the reduced model uint_fast64_t stateInReducedModel = originalToReducedStateMapping[state]; for(uint_fast64_t row = model.getTransitionMatrix().getRowGroupIndices()[state]; row < model.getTransitionMatrix().getRowGroupIndices()[state+1]; ++row) { - bool rowOnlyLeadsToRecurrentStates = true; + bool rowOnlyLeadsToBottomStates = true; bool rowStaysInEC = true; for( auto const& entry : model.getTransitionMatrix().getRow(row)) { - rowOnlyLeadsToRecurrentStates &= recurrentStates.get(entry.getColumn()); + rowOnlyLeadsToBottomStates &= bottomStates.get(entry.getColumn()); rowStaysInEC &= originalToReducedStateMapping[entry.getColumn()] == stateInReducedModel; } - if(rowOnlyLeadsToRecurrentStates && (rowStaysInEC || !statesThatShouldStayInTheirEC.get(state)) && !actionsWithNegativeReward.get(row)) { + if(rowOnlyLeadsToBottomStates && (rowStaysInEC || !statesThatShouldStayInTheirEC.get(state)) && actionsWithoutRewardInUnboundedPhase.get(row)) { foundRowForState = true; originalOptimalChoices[state] = row - model.getTransitionMatrix().getRowGroupIndices()[state]; break; } } - STORM_LOG_ASSERT(foundRowForState, "Could not find a suitable choice for a recurrent state."); + STORM_LOG_ASSERT(foundRowForState, "Could not find a suitable choice for a bottom state."); } // Handle remaining states with still undef. scheduler (either EC states or non-subsystem states) while(!statesWithUndefSched.empty()) { for(auto state : statesWithUndefSched) { - // Try to find a choice such that at least one successor has a defined scheduler. - // This way, a non-recurrent state will never become recurrent + // Iteratively Try to find a choice such that at least one successor has a defined scheduler. uint_fast64_t stateInReducedModel = originalToReducedStateMapping[state]; for(uint_fast64_t row = model.getTransitionMatrix().getRowGroupIndices()[state]; row < model.getTransitionMatrix().getRowGroupIndices()[state+1]; ++row) { bool rowStaysInEC = true; diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h index d80eb4931..691b69fad 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h @@ -5,7 +5,7 @@ #include "storm/storage/BitVector.h" #include "storm/storage/SparseMatrix.h" #include "storm/storage/TotalScheduler.h" -#include "storm/modelchecker/multiobjective/pcaa/PcaaObjective.h" +#include "storm/modelchecker/multiobjective/Objective.h" #include "storm/utility/vector.h" namespace storm { @@ -14,8 +14,8 @@ namespace storm { /*! * Helper Class that takes preprocessed Pcaa data and a weight vector and ... - * - computes the maximal expected reward w.r.t. the weighted sum of the rewards of the individual objectives - * - extracts the scheduler that induces this maximum + * - computes the optimal expected reward w.r.t. the weighted sum of the rewards of the individual objectives + * - extracts the scheduler that induces this optimum * - computes for each objective the value induced by this scheduler */ template @@ -28,23 +28,21 @@ namespace storm { * * @param model The (preprocessed) model * @param objectives The (preprocessed) objectives - * @param actionsWithNegativeReward The actions that have negative reward assigned for at least one objective - * @param ecActions The actions that are part of an EC - * @param possiblyRecurrentStates The states for which it is posible to visit them infinitely often (without inducing inf. reward) + * @param possibleECActions Overapproximation of the actions that are part of an EC + * @param possibleBottomStates The states for which it is posible to not collect further reward with prob. 1 * */ SparsePcaaWeightVectorChecker(SparseModelType const& model, - std::vector> const& objectives, - storm::storage::BitVector const& actionsWithNegativeReward, - storm::storage::BitVector const& ecActions, - storm::storage::BitVector const& possiblyRecurrentStates); + std::vector> const& objectives, + storm::storage::BitVector const& possibleECActions, + storm::storage::BitVector const& possibleBottomStates); virtual ~SparsePcaaWeightVectorChecker() = default; /*! - * - computes the maximal expected reward w.r.t. the weighted sum of the rewards of the individual objectives - * - extracts the scheduler that induces this maximum + * - computes the optimal expected reward w.r.t. the weighted sum of the rewards of the individual objectives + * - extracts the scheduler that induces this optimum * - computes for each objective the value induced by this scheduler */ void check(std::vector const& weightVector); @@ -52,19 +50,19 @@ namespace storm { /*! * Retrieves the results of the individual objectives at the initial state of the given model. * Note that check(..) has to be called before retrieving results. Otherwise, an exception is thrown. - * Also note that there is no guarantee that the lower/upper bounds are sound + * Also note that there is no guarantee that the under/over approximation is in fact correct * as long as the underlying solution methods are unsound (e.g., standard value iteration). */ - std::vector getLowerBoundsOfInitialStateResults() const; - std::vector getUpperBoundsOfInitialStateResults() const; + std::vector getUnderApproximationOfInitialStateResults() const; + std::vector getOverApproximationOfInitialStateResults() const; /*! * Sets the precision of this weight vector checker. After calling check() the following will hold: * Let h_lower and h_upper be two hyperplanes such that - * * the normal vector is the provided weight-vector - * * getLowerBoundsOfInitialStateResults() lies on h_lower and - * * getUpperBoundsOfInitialStateResults() lies on h_upper. + * * the normal vector is the provided weight-vector where the entry for minimizing objectives is negated + * * getUnderApproximationOfInitialStateResults() lies on h_lower and + * * getOverApproximationOfInitialStateResults() lies on h_upper. * Then the distance between the two hyperplanes is at most weightedPrecision */ void setWeightedPrecision(ValueType const& weightedPrecision); @@ -84,11 +82,11 @@ namespace storm { protected: /*! - * Determines the scheduler that maximizes the weighted reward vector of the unbounded objectives + * Determines the scheduler that optimizes the weighted reward vector of the unbounded objectives * * @param weightedRewardVector the weighted rewards (only considering the unbounded objectives) */ - void unboundedWeightedPhase(std::vector const& weightedRewardVector); + void unboundedWeightedPhase(std::vector const& weightedRewardVector, boost::optional const& lowerResultBound, boost::optional const& upperResultBound); /*! * Computes the values of the objectives that do not have a stepBound w.r.t. the scheduler computed in the unboundedWeightedPhase @@ -122,26 +120,21 @@ namespace storm { // The (preprocessed) model SparseModelType const& model; // The (preprocessed) objectives - std::vector> const& objectives; + std::vector> const& objectives; - // The actions that have negative reward assigned for at least one objective - storm::storage::BitVector actionsWithNegativeReward; - // The actions that are part of an EC - storm::storage::BitVector ecActions; + // Overapproximation of the set of choices that are part of an end component. + storm::storage::BitVector possibleECActions; + // The actions that have reward assigned for at least one objective without upper timeBound + storm::storage::BitVector actionsWithoutRewardInUnboundedPhase; // The states for which it is allowed to visit them infinitely often // Put differently, if one of the states is part of a neutral EC, it is possible to // stay in this EC forever (withoud inducing infinite reward for some objective). - storm::storage::BitVector possiblyRecurrentStates; + storm::storage::BitVector possibleBottomStates; // stores the indices of the objectives for which there is no upper time bound storm::storage::BitVector objectivesWithNoUpperTimeBound; // stores the (discretized) state action rewards for each objective. std::vector> discreteActionRewards; - /* stores the precision of this weight vector checker. After calling check() the following will hold: - * Let h_lower and h_upper be two hyperplanes such that - * * the normal vector is the provided weight-vector - * * getLowerBoundsOfInitialStateResults() lies on h_lower and - * * getUpperBoundsOfInitialStateResults() lies on h_upper. - * Then the distance between the two hyperplanes is at most weightedPrecision */ + // stores the precision of this weight vector checker. ValueType weightedPrecision; // Memory for the solution of the most recent call of check(..) // becomes true after the first call of check(..) @@ -150,11 +143,11 @@ namespace storm { std::vector weightedResult; // The results for the individual objectives (w.r.t. all states of the model) std::vector> objectiveResults; - // Stores for each objective the distance between the computed result (w.r.t. the initial state) and a lower/upper bound for the actual result. + // Stores for each objective the distance between the computed result (w.r.t. the initial state) and an over/under approximation for the actual result. // The distances are stored as a (possibly negative) offset that has to be added (+) to to the objectiveResults. - std::vector offsetsToLowerBound; - std::vector offsetsToUpperBound; - // The scheduler that maximizes the weighted rewards + std::vector offsetsToUnderApproximation; + std::vector offsetsToOverApproximation; + // The scheduler that optimizes the weighted rewards storm::storage::TotalScheduler scheduler; }; diff --git a/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp index 93f538987..9b97b9f25 100644 --- a/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp @@ -16,7 +16,7 @@ #include "storm/logic/FragmentSpecification.h" -#include "storm/modelchecker/multiobjective/pcaa.h" +#include "storm/modelchecker/multiobjective/multiObjectiveModelChecking.h" #include "storm/solver/MinMaxLinearEquationSolver.h" @@ -126,7 +126,7 @@ namespace storm { template std::unique_ptr HybridMdpPrctlModelChecker::checkMultiObjectiveFormula(CheckTask const& checkTask) { auto sparseModel = storm::transformer::SymbolicMdpToSparseMdpTransformer::translate(this->getModel()); - std::unique_ptr explicitResult = multiobjective::performPcaa(*sparseModel, checkTask.getFormula()); + std::unique_ptr explicitResult = multiobjective::performMultiObjectiveModelChecking(*sparseModel, checkTask.getFormula()); // Convert the explicit result if(explicitResult->isExplicitQualitativeCheckResult()) { diff --git a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index 44db5e635..4aaee1400 100644 --- a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -14,7 +14,7 @@ #include "storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h" -#include "storm/modelchecker/multiobjective/pcaa.h" +#include "storm/modelchecker/multiobjective/multiObjectiveModelChecking.h" #include "storm/solver/LpSolver.h" @@ -164,7 +164,7 @@ namespace storm { template std::unique_ptr SparseMdpPrctlModelChecker::checkMultiObjectiveFormula(CheckTask const& checkTask) { - return multiobjective::performPcaa(this->getModel(), checkTask.getFormula()); + return multiobjective::performMultiObjectiveModelChecking(this->getModel(), checkTask.getFormula()); } template class SparseMdpPrctlModelChecker>; diff --git a/src/storm/models/sparse/StandardRewardModel.cpp b/src/storm/models/sparse/StandardRewardModel.cpp index 78f4c39af..a4149709c 100644 --- a/src/storm/models/sparse/StandardRewardModel.cpp +++ b/src/storm/models/sparse/StandardRewardModel.cpp @@ -258,8 +258,36 @@ namespace storm { } return result; } + + template + template + storm::storage::BitVector StandardRewardModel::getChoicesWithZeroReward(storm::storage::SparseMatrix const& transitionMatrix) const { + storm::storage::BitVector result; + if (this->hasStateActionRewards()) { + result = storm::utility::vector::filterZero(this->getStateActionRewardVector()); + if (this->hasStateRewards()) { + result &= transitionMatrix.getRowFilter(storm::utility::vector::filterZero(this->getStateRewardVector())); + } + } else { + if (this->hasStateRewards()) { + result = transitionMatrix.getRowFilter(storm::utility::vector::filterZero(this->getStateRewardVector())); + } else { + result = storm::storage::BitVector(transitionMatrix.getRowCount(), true); + } + } + if (this->hasTransitionRewards()) { + for (uint_fast64_t row = 0; row < transitionMatrix.getRowCount(); ++row) { + for (auto const& rewardMatrixEntry : this->getTransitionRewardMatrix().getRow(row)) { + if(!storm::utility::isZero(rewardMatrixEntry.getValue())) { + result.set(row, false); + break; + } + } + } + } + return result; + } - template void StandardRewardModel::setStateActionRewardValue(uint_fast64_t row, ValueType const& value) { this->optionalStateActionRewardVector.get()[row] = value; @@ -333,6 +361,7 @@ namespace storm { template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& weights, bool scaleTransAndActions) const; template std::vector StandardRewardModel::getTotalActionRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& stateRewardWeights) const; template storm::storage::BitVector StandardRewardModel::getStatesWithZeroReward(storm::storage::SparseMatrix const& transitionMatrix) const; + template storm::storage::BitVector StandardRewardModel::getChoicesWithZeroReward(storm::storage::SparseMatrix const& transitionMatrix) const; template void StandardRewardModel::reduceToStateBasedRewards(storm::storage::SparseMatrix const& transitionMatrix, bool reduceToStateRewards); template void StandardRewardModel::setStateActionReward(uint_fast64_t choiceIndex, double const & newValue); template void StandardRewardModel::setStateReward(uint_fast64_t state, double const & newValue); @@ -355,6 +384,7 @@ namespace storm { template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& weights, bool scaleTransAndActions) const; template std::vector StandardRewardModel::getTotalActionRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& stateRewardWeights) const; template storm::storage::BitVector StandardRewardModel::getStatesWithZeroReward(storm::storage::SparseMatrix const& transitionMatrix) const; + template storm::storage::BitVector StandardRewardModel::getChoicesWithZeroReward(storm::storage::SparseMatrix const& transitionMatrix) const; template void StandardRewardModel::reduceToStateBasedRewards(storm::storage::SparseMatrix const& transitionMatrix, bool reduceToStateRewards); template void StandardRewardModel::setStateActionReward(uint_fast64_t choiceIndex, storm::RationalNumber const & newValue); template void StandardRewardModel::setStateReward(uint_fast64_t state, storm::RationalNumber const & newValue); @@ -365,6 +395,7 @@ namespace storm { template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix) const; template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& weights, bool scaleTransAndActions) const; template storm::storage::BitVector StandardRewardModel::getStatesWithZeroReward(storm::storage::SparseMatrix const& transitionMatrix) const; + template storm::storage::BitVector StandardRewardModel::getChoicesWithZeroReward(storm::storage::SparseMatrix const& transitionMatrix) const; template std::vector StandardRewardModel::getTotalActionRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& stateRewardWeights) const; template void StandardRewardModel::reduceToStateBasedRewards(storm::storage::SparseMatrix const& transitionMatrix, bool reduceToStateRewards); diff --git a/src/storm/models/sparse/StandardRewardModel.h b/src/storm/models/sparse/StandardRewardModel.h index 57b0d5c5a..f0449ce52 100644 --- a/src/storm/models/sparse/StandardRewardModel.h +++ b/src/storm/models/sparse/StandardRewardModel.h @@ -236,6 +236,15 @@ namespace storm { */ template storm::storage::BitVector getStatesWithZeroReward(storm::storage::SparseMatrix const& transitionMatrix) const; + + /*! + * Returns the set of choices at which all rewards (state-, action- and transition-rewards) are zero. + * + * @param transitionMatrix the transition matrix of the model (used to determine the state that belongs to a choice + * @ return a vector representing all choices at which the reward is zero + */ + template + storm::storage::BitVector getChoicesWithZeroReward(storm::storage::SparseMatrix const& transitionMatrix) const; /*! * Sets the given value in the state-action reward vector at the given row. This assumes that the reward diff --git a/src/storm/settings/modules/MultiObjectiveSettings.cpp b/src/storm/settings/modules/MultiObjectiveSettings.cpp index 4f7dee008..1ebc3464b 100644 --- a/src/storm/settings/modules/MultiObjectiveSettings.cpp +++ b/src/storm/settings/modules/MultiObjectiveSettings.cpp @@ -12,11 +12,14 @@ namespace storm { namespace modules { const std::string MultiObjectiveSettings::moduleName = "multiobjective"; + const std::string MultiObjectiveSettings::methodOptionName = "method"; const std::string MultiObjectiveSettings::exportPlotOptionName = "exportplot"; const std::string MultiObjectiveSettings::precisionOptionName = "precision"; const std::string MultiObjectiveSettings::maxStepsOptionName = "maxsteps"; MultiObjectiveSettings::MultiObjectiveSettings() : ModuleSettings(moduleName) { + std::vector methods = {"pcaa", "constraintbased"}; + this->addOption(storm::settings::OptionBuilder(moduleName, methodOptionName, true, "The method to be used for multi objective model checking.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the method to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(methods)).setDefaultValueString("pcaa").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, exportPlotOptionName, true, "Saves data for plotting of pareto curves and achievable values.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("directory", "A path to a directory in which the results will be saved.").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, true, "The precision used for the approximation of numerical- and pareto queries.") @@ -25,12 +28,26 @@ namespace storm { .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("value", "the threshold for the number of refinement steps to be performed.").build()).build()); } + storm::modelchecker::multiobjective::MultiObjectiveMethod MultiObjectiveSettings::getMultiObjectiveMethod() const { + std::string methodAsString = this->getOption(methodOptionName).getArgumentByName("name").getValueAsString(); + if (methodAsString == "pcaa") { + return storm::modelchecker::multiobjective::MultiObjectiveMethod::Pcaa; + } else { + STORM_LOG_ASSERT(methodAsString == "constraintbased", "Unexpected method name for multi objective model checking method."); + return storm::modelchecker::multiobjective::MultiObjectiveMethod::ConstraintBased; + } + } + bool MultiObjectiveSettings::isExportPlotSet() const { return this->getOption(exportPlotOptionName).getHasOptionBeenSet(); } std::string MultiObjectiveSettings::getExportPlotDirectory() const { - return this->getOption(exportPlotOptionName).getArgumentByName("directory").getValueAsString(); + std::string result = this->getOption(exportPlotOptionName).getArgumentByName("directory").getValueAsString(); + if (result.back() != '/') { + result.push_back('/'); + } + return result; } double MultiObjectiveSettings::getPrecision() const { diff --git a/src/storm/settings/modules/MultiObjectiveSettings.h b/src/storm/settings/modules/MultiObjectiveSettings.h index dc5c8c0f2..577b57308 100644 --- a/src/storm/settings/modules/MultiObjectiveSettings.h +++ b/src/storm/settings/modules/MultiObjectiveSettings.h @@ -2,6 +2,7 @@ #define STORM_SETTINGS_MODULES_MULTIOBJECTIVESETTINGS_H_ #include "storm/settings/modules/ModuleSettings.h" +#include "storm/modelchecker/multiobjective/MultiObjectiveModelCheckingMethod.h" namespace storm { namespace settings { @@ -18,6 +19,11 @@ namespace storm { */ MultiObjectiveSettings(); + /*! + * Returns the preferred method for multi objective model checking + */ + storm::modelchecker::multiobjective::MultiObjectiveMethod getMultiObjectiveMethod() const; + /*! * Retrieves whether the data for plotting should be exported. * @return True iff the data for plotting should be exported. @@ -63,6 +69,7 @@ namespace storm { const static std::string moduleName; private: + const static std::string methodOptionName; const static std::string exportPlotOptionName; const static std::string precisionOptionName; const static std::string maxStepsOptionName; diff --git a/src/storm/storage/SparseMatrix.cpp b/src/storm/storage/SparseMatrix.cpp index d481f7063..d2bcead60 100644 --- a/src/storm/storage/SparseMatrix.cpp +++ b/src/storm/storage/SparseMatrix.cpp @@ -14,6 +14,7 @@ #include "storm/storage/BitVector.h" #include "storm/utility/constants.h" #include "storm/utility/ConstantsComparator.h" +#include "storm/utility/vector.h" #include "storm/exceptions/InvalidStateException.h" #include "storm/exceptions/NotImplementedException.h" @@ -546,10 +547,7 @@ namespace storm { // If there is no current row grouping, we need to create it. if (!this->rowGroupIndices) { STORM_LOG_ASSERT(trivialRowGrouping, "Only trivial row-groupings can be constructed on-the-fly."); - this->rowGroupIndices = std::vector(this->getRowCount() + 1); - for (uint_fast64_t group = 0; group <= this->getRowCount(); ++group) { - this->rowGroupIndices.get()[group] = group; - } + this->rowGroupIndices = storm::utility::vector::buildVectorForRange(0, this->getRowGroupCount() + 1); } return rowGroupIndices.get(); } diff --git a/src/storm/storage/memorystructure/MemoryStructure.cpp b/src/storm/storage/memorystructure/MemoryStructure.cpp new file mode 100644 index 000000000..69266f562 --- /dev/null +++ b/src/storm/storage/memorystructure/MemoryStructure.cpp @@ -0,0 +1,137 @@ +#include "storm/storage/memorystructure/MemoryStructure.h" + +#include + +#include "storm/logic/Formulas.h" +#include "storm/utility/macros.h" +#include "storm/storage/memorystructure/SparseModelMemoryProduct.h" + +#include "storm/exceptions/InvalidOperationException.h" + +namespace storm { + namespace storage { + + MemoryStructure::MemoryStructure(TransitionMatrix const& transitionMatrix, storm::models::sparse::StateLabeling const& memoryStateLabeling) : transitions(transitionMatrix), stateLabeling(memoryStateLabeling) { + // intentionally left empty + } + + MemoryStructure::MemoryStructure(TransitionMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& memoryStateLabeling) : transitions(std::move(transitionMatrix)), stateLabeling(std::move(memoryStateLabeling)) { + // intentionally left empty + } + + MemoryStructure::TransitionMatrix const& MemoryStructure::getTransitionMatrix() const { + return transitions; + } + + storm::models::sparse::StateLabeling const& MemoryStructure::getStateLabeling() const { + return stateLabeling; + } + + uint_fast64_t MemoryStructure::getNumberOfStates() const { + return transitions.size(); + } + + MemoryStructure MemoryStructure::product(MemoryStructure const& rhs) const { + uint_fast64_t lhsNumStates = this->getTransitionMatrix().size(); + uint_fast64_t rhsNumStates = rhs.getTransitionMatrix().size(); + uint_fast64_t resNumStates = lhsNumStates * rhsNumStates; + + // Transition matrix + TransitionMatrix resultTransitions(resNumStates, std::vector>(resNumStates)); + uint_fast64_t resState = 0; + for (uint_fast64_t lhsState = 0; lhsState < lhsNumStates; ++lhsState) { + for (uint_fast64_t rhsState = 0; rhsState < rhsNumStates; ++rhsState) { + assert (resState == (lhsState * rhsNumStates) + rhsState); + auto& resStateTransitions = resultTransitions[resState]; + for (uint_fast64_t lhsTransitionTarget = 0; lhsTransitionTarget < lhsNumStates; ++lhsTransitionTarget) { + auto& lhsTransition = this->getTransitionMatrix()[lhsState][lhsTransitionTarget]; + if (lhsTransition) { + for (uint_fast64_t rhsTransitionTarget = 0; rhsTransitionTarget < rhsNumStates; ++rhsTransitionTarget) { + auto& rhsTransition = rhs.getTransitionMatrix()[rhsState][rhsTransitionTarget]; + if (rhsTransition) { + uint_fast64_t resTransitionTarget = (lhsTransitionTarget * rhsNumStates) + rhsTransitionTarget; + resStateTransitions[resTransitionTarget] = std::make_shared(storm::logic::BinaryBooleanStateFormula::OperatorType::And, lhsTransition,rhsTransition); + } + } + } + } + ++resState; + } + } + + // State Labels + storm::models::sparse::StateLabeling resultLabeling(resNumStates); + for (std::string lhsLabel : this->getStateLabeling().getLabels()) { + storm::storage::BitVector const& lhsLabeledStates = this->getStateLabeling().getStates(lhsLabel); + storm::storage::BitVector resLabeledStates(resNumStates, false); + for (auto const& lhsState : lhsLabeledStates) { + for (uint_fast64_t rhsState = 0; rhsState < rhsNumStates; ++rhsState) { + resState = (lhsState * rhsNumStates) + rhsState; + resLabeledStates.set(resState, true); + } + } + resultLabeling.addLabel(lhsLabel, std::move(resLabeledStates)); + } + for (std::string rhsLabel : rhs.getStateLabeling().getLabels()) { + STORM_LOG_THROW(!resultLabeling.containsLabel(rhsLabel), storm::exceptions::InvalidOperationException, "Failed to build the product of two memory structures: State labelings are not disjoint as both structures contain the label " << rhsLabel << "."); + storm::storage::BitVector const& rhsLabeledStates = rhs.getStateLabeling().getStates(rhsLabel); + storm::storage::BitVector resLabeledStates(resNumStates, false); + for (auto const& rhsState : rhsLabeledStates) { + for (uint_fast64_t lhsState = 0; lhsState < lhsNumStates; ++lhsState) { + resState = (lhsState * rhsNumStates) + rhsState; + resLabeledStates.set(resState, true); + } + } + resultLabeling.addLabel(rhsLabel, std::move(resLabeledStates)); + } + //return MemoryStructure(std::move(resultTransitions), std::move(resultLabeling)); + + MemoryStructure res(std::move(resultTransitions), std::move(resultLabeling)); + return res; + + } + + template + SparseModelMemoryProduct MemoryStructure::product(storm::models::sparse::Model const& sparseModel) const { + return SparseModelMemoryProduct(sparseModel, *this); + } + + std::string MemoryStructure::toString() const { + std::stringstream stream; + + stream << "Memory Structure with " << getNumberOfStates() << " states: " << std::endl; + + for (uint_fast64_t state = 0; state < getNumberOfStates(); ++state) { + stream << "State " << state << ": Labels = {"; + bool firstLabel = true; + for (auto const& label : getStateLabeling().getLabelsOfState(state)) { + if (!firstLabel) { + stream << ", "; + } + firstLabel = false; + stream << label; + } + stream << "}, Transitions: " << std::endl; + for (uint_fast64_t transitionTarget = 0; transitionTarget < getNumberOfStates(); ++transitionTarget) { + stream << "\t From " << state << " to " << transitionTarget << ": \t"; + auto const& transition = getTransitionMatrix()[state][transitionTarget]; + if (transition) { + stream << *transition; + } else { + stream << "false"; + } + stream << std::endl; + } + } + + return stream.str(); + } + + template SparseModelMemoryProduct MemoryStructure::product(storm::models::sparse::Model const& sparseModel) const; + template SparseModelMemoryProduct MemoryStructure::product(storm::models::sparse::Model const& sparseModel) const; + + + } +} + + diff --git a/src/storm/storage/memorystructure/MemoryStructure.h b/src/storm/storage/memorystructure/MemoryStructure.h new file mode 100644 index 000000000..41052c7fa --- /dev/null +++ b/src/storm/storage/memorystructure/MemoryStructure.h @@ -0,0 +1,68 @@ +#pragma once + +#include +#include + +#include "storm/logic/Formula.h" +#include "storm/models/sparse/StateLabeling.h" +#include "storm/models/sparse/Model.h" + +namespace storm { + namespace storage { + + template + class SparseModelMemoryProduct; + + /*! + * This class represents a (deterministic) memory structure that can be used to encode certain events + * (such as reaching a set of goal states) into the state space of the model. + */ + class MemoryStructure { + public: + + typedef std::vector>> TransitionMatrix; + + /*! + * Creates a memory structure with the given transition matrix and the given memory state labeling. + * The initial state is always the state with index 0. + * The transition matrix is assumed to contain propositional state formulas. The entry + * transitionMatrix[m][n] specifies the set of model states which trigger a transition from memory + * state m to memory state n. + * Transitions are assumed to be deterministic and complete, i.e., the formulas in + * transitionMatrix[m] form a partition of the state space of the considered model. + * + * @param transitionMatrix The transition matrix + * @param memoryStateLabeling A labeling of the memory states to specify, e.g., accepting states + */ + MemoryStructure(TransitionMatrix const& transitionMatrix, storm::models::sparse::StateLabeling const& memoryStateLabeling); + MemoryStructure(TransitionMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& memoryStateLabeling); + + TransitionMatrix const& getTransitionMatrix() const; + storm::models::sparse::StateLabeling const& getStateLabeling() const; + uint_fast64_t getNumberOfStates() const; + + /*! + * Builds the product of this memory structure and the given memory structure. + * The resulting memory structure will have the state labels of both given structures. + * Throws an exception if the state labelings are not disjoint. + */ + MemoryStructure product(MemoryStructure const& rhs) const; + + /*! + * Builds the product of this memory structure and the given sparse model. + * An exception is thrown if the state labelings of this memory structure and the given model are not disjoint. + */ + template + SparseModelMemoryProduct product(storm::models::sparse::Model const& sparseModel) const; + + std::string toString() const; + + private: + TransitionMatrix transitions; + storm::models::sparse::StateLabeling stateLabeling; + }; + + } +} + + diff --git a/src/storm/storage/memorystructure/MemoryStructureBuilder.cpp b/src/storm/storage/memorystructure/MemoryStructureBuilder.cpp new file mode 100644 index 000000000..b2b654a93 --- /dev/null +++ b/src/storm/storage/memorystructure/MemoryStructureBuilder.cpp @@ -0,0 +1,36 @@ +#include "storm/storage/memorystructure/MemoryStructureBuilder.h" + +#include "storm/logic/FragmentSpecification.h" +#include "storm/utility/macros.h" + +#include "storm/exceptions/InvalidOperationException.h" + +namespace storm { + namespace storage { + + MemoryStructureBuilder::MemoryStructureBuilder(uint_fast64_t const& numberOfStates) : transitions(numberOfStates, std::vector>(numberOfStates)), stateLabeling(numberOfStates) { + // Intentionally left empty + } + + void MemoryStructureBuilder::setTransition(uint_fast64_t const& startState, uint_fast64_t const& goalState, std::shared_ptr formula) { + STORM_LOG_THROW(startState < transitions.size(), storm::exceptions::InvalidOperationException, "Invalid index of start state: " << startState << ". There are only " << transitions.size() << " states in this memory structure."); + STORM_LOG_THROW(goalState < transitions.size(), storm::exceptions::InvalidOperationException, "Invalid index of goal state: " << startState << ". There are only " << transitions.size() << " states in this memory structure."); + STORM_LOG_THROW(formula->isInFragment(storm::logic::propositional()), storm::exceptions::InvalidOperationException, "The formula '" << *formula << "' is not propositional"); + + transitions[startState][goalState] = formula; + } + + void MemoryStructureBuilder::setLabel(uint_fast64_t const& state, std::string const& label) { + STORM_LOG_THROW(state < transitions.size(), storm::exceptions::InvalidOperationException, "Can not add label to state with index " << state << ". There are only " << transitions.size() << " states in this memory structure."); + if (!stateLabeling.containsLabel(label)) { + stateLabeling.addLabel(label); + } + stateLabeling.addLabelToState(label, state); + } + + MemoryStructure MemoryStructureBuilder::build() { + return MemoryStructure(std::move(transitions), std::move(stateLabeling)); + } + + } +} diff --git a/src/storm/storage/memorystructure/MemoryStructureBuilder.h b/src/storm/storage/memorystructure/MemoryStructureBuilder.h new file mode 100644 index 000000000..e87992d56 --- /dev/null +++ b/src/storm/storage/memorystructure/MemoryStructureBuilder.h @@ -0,0 +1,49 @@ +#pragma once + +#include +#include + +#include "storm/logic/Formula.h" +#include "storm/models/sparse/StateLabeling.h" +#include "storm/storage/memorystructure/MemoryStructure.h" + +namespace storm { + namespace storage { + + + class MemoryStructureBuilder { + public: + + /*! + * Initializes a new builder for a memory structure + * @param numberOfStates The number of states the resulting memory structure should have + */ + MemoryStructureBuilder(uint_fast64_t const& numberOfStates); + + /*! + * Specifies a transition. The formula should be a propositional formula + */ + void setTransition(uint_fast64_t const& startState, uint_fast64_t const& goalState, std::shared_ptr formula); + + /*! + * Sets a label to the given state. + */ + void setLabel(uint_fast64_t const& state, std::string const& label); + + /*! + * Builds the memory structure. + * @note Calling this invalidates this builder. + * @note When calling this method, the specified transitions should be deterministic and complete. This is not checked. + */ + MemoryStructure build(); + + + private: + MemoryStructure::TransitionMatrix transitions; + storm::models::sparse::StateLabeling stateLabeling; + }; + + } +} + + diff --git a/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp b/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp new file mode 100644 index 000000000..f37e380f7 --- /dev/null +++ b/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp @@ -0,0 +1,330 @@ +#include "storm/storage/memorystructure/SparseModelMemoryProduct.h" + +#include + +#include "storm/models/sparse/Dtmc.h" +#include "storm/models/sparse/Mdp.h" +#include "storm/models/sparse/Ctmc.h" +#include "storm/models/sparse/MarkovAutomaton.h" +#include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h" +#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" +#include "storm/utility/constants.h" +#include "storm/utility/macros.h" + +#include "storm/exceptions/InvalidOperationException.h" + +namespace storm { + namespace storage { + + template + SparseModelMemoryProduct::SparseModelMemoryProduct(storm::models::sparse::Model const& sparseModel, storm::storage::MemoryStructure const& memoryStructure) : model(sparseModel), memory(memoryStructure) { + // intentionally left empty + } + + template + std::shared_ptr> SparseModelMemoryProduct::build() { + uint_fast64_t modelStateCount = model.getNumberOfStates(); + uint_fast64_t memoryStateCount = memory.getNumberOfStates(); + + std::vector memorySuccessors = computeMemorySuccessors(); + + // Get the initial states and reachable states. A stateIndex s corresponds to the model state (s / memoryStateCount) and memory state (s % memoryStateCount) + storm::storage::BitVector initialStates(modelStateCount * memoryStateCount, false); + for (auto const& modelInit : model.getInitialStates()) { + // Note: The initial state of a memory structure is always 0. + initialStates.set(modelInit * memoryStateCount + memorySuccessors[modelInit * memoryStateCount], true); + } + storm::storage::BitVector reachableStates = computeReachableStates(memorySuccessors, initialStates); + // Compute the mapping to the states of the result + uint_fast64_t reachableStateCount = 0; + toResultStateMapping = std::vector (model.getNumberOfStates() * memory.getNumberOfStates(), std::numeric_limits::max()); + for (auto const& reachableState : reachableStates) { + toResultStateMapping[reachableState] = reachableStateCount; + ++reachableStateCount; + } + + // Build the model components + storm::storage::SparseMatrix transitionMatrix = model.getTransitionMatrix().hasTrivialRowGrouping() ? + buildDeterministicTransitionMatrix(reachableStates, memorySuccessors) : + buildNondeterministicTransitionMatrix(reachableStates, memorySuccessors); + storm::models::sparse::StateLabeling labeling = buildStateLabeling(transitionMatrix); + std::unordered_map> rewardModels = buildRewardModels(transitionMatrix, memorySuccessors); + + // Add the label for the initial states. We need to translate the state indices w.r.t. the set of reachable states. + labeling.addLabel("init", initialStates % reachableStates); + + return buildResult(std::move(transitionMatrix), std::move(labeling), std::move(rewardModels)); + + } + + template + uint_fast64_t const& SparseModelMemoryProduct::getResultState(uint_fast64_t const& modelState, uint_fast64_t const& memoryState) const { + return toResultStateMapping[modelState * memory.getNumberOfStates() + memoryState]; + } + + + template + std::vector SparseModelMemoryProduct::computeMemorySuccessors() const { + uint_fast64_t modelStateCount = model.getNumberOfStates(); + uint_fast64_t memoryStateCount = memory.getNumberOfStates(); + std::vector result(modelStateCount * memoryStateCount, std::numeric_limits::max()); + + storm::modelchecker::SparsePropositionalModelChecker> mc(model); + for (uint_fast64_t memoryState = 0; memoryState < memoryStateCount; ++memoryState) { + for (uint_fast64_t transitionGoal = 0; transitionGoal < memoryStateCount; ++transitionGoal) { + auto const& transition = memory.getTransitionMatrix()[memoryState][transitionGoal]; + if (transition) { + auto mcResult = mc.check(*transition); + for (auto const& modelState : mcResult->asExplicitQualitativeCheckResult().getTruthValuesVector()) { + result[modelState * memoryStateCount + memoryState] = transitionGoal; + } + } + } + } + return result; + } + + template + storm::storage::BitVector SparseModelMemoryProduct::computeReachableStates(std::vector const& memorySuccessors, storm::storage::BitVector const& initialStates) const { + uint_fast64_t memoryStateCount = memory.getNumberOfStates(); + // Explore the reachable states via DFS. + // A state s on the stack corresponds to the model state (s / memoryStateCount) and memory state (s % memoryStateCount) + storm::storage::BitVector reachableStates = initialStates; + std::vector stack(reachableStates.begin(), reachableStates.end()); + while (!stack.empty()) { + uint_fast64_t stateIndex = stack.back(); + stack.pop_back(); + uint_fast64_t modelState = stateIndex / memoryStateCount; + uint_fast64_t memoryState = stateIndex % memoryStateCount; + + for (auto const& modelTransition : model.getTransitionMatrix().getRowGroup(modelState)) { + if (!storm::utility::isZero(modelTransition.getValue())) { + uint_fast64_t successorModelState = modelTransition.getColumn(); + uint_fast64_t successorMemoryState = memorySuccessors[successorModelState * memoryStateCount + memoryState]; + uint_fast64_t successorStateIndex = successorModelState * memoryStateCount + successorMemoryState; + if (!reachableStates.get(successorStateIndex)) { + reachableStates.set(successorStateIndex, true); + stack.push_back(successorStateIndex); + } + } + } + } + return reachableStates; + } + + template + storm::storage::SparseMatrix SparseModelMemoryProduct::buildDeterministicTransitionMatrix(storm::storage::BitVector const& reachableStates, std::vector const& memorySuccessors) const { + uint_fast64_t memoryStateCount = memory.getNumberOfStates(); + uint_fast64_t numResStates = reachableStates.getNumberOfSetBits(); + uint_fast64_t numResTransitions = 0; + for (auto const& stateIndex : reachableStates) { + numResTransitions += model.getTransitionMatrix().getRow(stateIndex / memoryStateCount).getNumberOfEntries(); + } + + storm::storage::SparseMatrixBuilder builder(numResStates, numResStates, numResTransitions, true); + uint_fast64_t currentRow = 0; + for (auto const& stateIndex : reachableStates) { + uint_fast64_t modelState = stateIndex / memoryStateCount; + uint_fast64_t memoryState = stateIndex % memoryStateCount; + for (auto const& entry : model.getTransitionMatrix().getRow(modelState)) { + uint_fast64_t const& successorMemoryState = memorySuccessors[entry.getColumn() * memoryStateCount + memoryState]; + builder.addNextValue(currentRow, getResultState(entry.getColumn(), successorMemoryState), entry.getValue()); + } + ++currentRow; + } + + return builder.build(); + } + + template + storm::storage::SparseMatrix SparseModelMemoryProduct::buildNondeterministicTransitionMatrix(storm::storage::BitVector const& reachableStates, std::vector const& memorySuccessors) const { + uint_fast64_t memoryStateCount = memory.getNumberOfStates(); + uint_fast64_t numResStates = reachableStates.getNumberOfSetBits(); + uint_fast64_t numResChoices = 0; + uint_fast64_t numResTransitions = 0; + for (auto const& stateIndex : reachableStates) { + uint_fast64_t modelState = stateIndex / memoryStateCount; + for (uint_fast64_t modelRow = model.getTransitionMatrix().getRowGroupIndices()[modelState]; modelRow < model.getTransitionMatrix().getRowGroupIndices()[modelState + 1]; ++modelRow) { + ++numResChoices; + numResTransitions += model.getTransitionMatrix().getRow(modelRow).getNumberOfEntries(); + } + } + + storm::storage::SparseMatrixBuilder builder(numResChoices, numResStates, numResTransitions, true, true, numResStates); + uint_fast64_t currentRow = 0; + for (auto const& stateIndex : reachableStates) { + uint_fast64_t modelState = stateIndex / memoryStateCount; + uint_fast64_t memoryState = stateIndex % memoryStateCount; + builder.newRowGroup(currentRow); + for (uint_fast64_t modelRow = model.getTransitionMatrix().getRowGroupIndices()[modelState]; modelRow < model.getTransitionMatrix().getRowGroupIndices()[modelState + 1]; ++modelRow) { + for (auto const& entry : model.getTransitionMatrix().getRow(modelRow)) { + uint_fast64_t const& successorMemoryState = memorySuccessors[entry.getColumn() * memoryStateCount + memoryState]; + builder.addNextValue(currentRow, getResultState(entry.getColumn(), successorMemoryState), entry.getValue()); + } + ++currentRow; + } + } + + return builder.build(); + } + + template + storm::models::sparse::StateLabeling SparseModelMemoryProduct::buildStateLabeling(storm::storage::SparseMatrix const& resultTransitionMatrix) const { + uint_fast64_t modelStateCount = model.getNumberOfStates(); + uint_fast64_t memoryStateCount = memory.getNumberOfStates(); + + uint_fast64_t numResStates = resultTransitionMatrix.getRowGroupCount(); + storm::models::sparse::StateLabeling resultLabeling(numResStates); + + for (std::string modelLabel : model.getStateLabeling().getLabels()) { + if (modelLabel != "init") { + storm::storage::BitVector resLabeledStates(numResStates, false); + for (auto const& modelState : model.getStateLabeling().getStates(modelLabel)) { + for (uint_fast64_t memoryState = 0; memoryState < memoryStateCount; ++memoryState) { + uint_fast64_t const& resState = getResultState(modelState, memoryState); + // Check if the state exists in the result (i.e. if it is reachable) + if (resState < numResStates) { + resLabeledStates.set(resState, true); + } + } + } + resultLabeling.addLabel(modelLabel, std::move(resLabeledStates)); + } + } + for (std::string memoryLabel : memory.getStateLabeling().getLabels()) { + STORM_LOG_THROW(!resultLabeling.containsLabel(memoryLabel), storm::exceptions::InvalidOperationException, "Failed to build the product of model and memory structure: State labelings are not disjoint as both structures contain the label " << memoryLabel << "."); + storm::storage::BitVector resLabeledStates(numResStates, false); + for (auto const& memoryState : memory.getStateLabeling().getStates(memoryLabel)) { + for (uint_fast64_t modelState = 0; modelState < modelStateCount; ++modelState) { + uint_fast64_t const& resState = getResultState(modelState, memoryState); + // Check if the state exists in the result (i.e. if it is reachable) + if (resState < numResStates) { + resLabeledStates.set(resState, true); + } + } + } + resultLabeling.addLabel(memoryLabel, std::move(resLabeledStates)); + } + return resultLabeling; + } + + template + std::unordered_map> SparseModelMemoryProduct::buildRewardModels(storm::storage::SparseMatrix const& resultTransitionMatrix, std::vector const& memorySuccessors) const { + std::unordered_map> result; + uint_fast64_t memoryStateCount = memory.getNumberOfStates(); + uint_fast64_t numResStates = resultTransitionMatrix.getRowGroupCount(); + + for (auto const& rewardModel : model.getRewardModels()) { + boost::optional> stateRewards; + if (rewardModel.second.hasStateRewards()) { + stateRewards = std::vector(numResStates, storm::utility::zero()); + uint_fast64_t modelState = 0; + for (auto const& modelStateReward : rewardModel.second.getStateRewardVector()) { + if (!storm::utility::isZero(modelStateReward)) { + for (uint_fast64_t memoryState = 0; memoryState < memoryStateCount; ++memoryState) { + uint_fast64_t const& resState = getResultState(modelState, memoryState); + // Check if the state exists in the result (i.e. if it is reachable) + if (resState < numResStates) { + stateRewards.get()[resState] = modelStateReward; + } + } + } + ++modelState; + } + } + boost::optional> stateActionRewards; + if (rewardModel.second.hasStateActionRewards()) { + stateActionRewards = std::vector(resultTransitionMatrix.getRowCount(), storm::utility::zero()); + uint_fast64_t modelState = 0; + uint_fast64_t modelRow = 0; + for (auto const& modelStateActionReward : rewardModel.second.getStateActionRewardVector()) { + if (!storm::utility::isZero(modelStateActionReward)) { + while (modelRow >= model.getTransitionMatrix().getRowGroupIndices()[modelState + 1]) { + ++modelState; + } + uint_fast64_t rowOffset = modelRow - model.getTransitionMatrix().getRowGroupIndices()[modelState]; + for (uint_fast64_t memoryState = 0; memoryState < memoryStateCount; ++memoryState) { + uint_fast64_t const& resState = getResultState(modelState, memoryState); + // Check if the state exists in the result (i.e. if it is reachable) + if (resState < numResStates) { + stateActionRewards.get()[resultTransitionMatrix.getRowGroupIndices()[resState] + rowOffset] = modelStateActionReward; + } + } + } + ++modelRow; + } + } + boost::optional> transitionRewards; + if (rewardModel.second.hasTransitionRewards()) { + storm::storage::SparseMatrixBuilder builder(resultTransitionMatrix.getRowCount(), resultTransitionMatrix.getColumnCount()); + uint_fast64_t stateIndex = 0; + for (auto const& resState : toResultStateMapping) { + if (resState < numResStates) { + uint_fast64_t modelState = stateIndex / memoryStateCount; + uint_fast64_t memoryState = stateIndex % memoryStateCount; + uint_fast64_t rowGroupSize = resultTransitionMatrix.getRowGroupSize(resState); + for (uint_fast64_t rowOffset = 0; rowOffset < rowGroupSize; ++rowOffset) { + uint_fast64_t resRowIndex = resultTransitionMatrix.getRowGroupIndices()[resState] + rowOffset; + uint_fast64_t modelRowIndex = model.getTransitionMatrix().getRowGroupIndices()[modelState] + rowOffset; + for (auto const& entry : rewardModel.second.getTransitionRewardMatrix().getRow(modelRowIndex)) { + uint_fast64_t const& successorMemoryState = memorySuccessors[entry.getColumn() * memoryStateCount + memoryState]; + builder.addNextValue(resRowIndex, getResultState(entry.getColumn(), successorMemoryState), entry.getValue()); + } + } + } + ++stateIndex; + } + transitionRewards = builder.build(); + } + result.insert(std::make_pair(rewardModel.first, storm::models::sparse::StandardRewardModel(std::move(stateRewards), std::move(stateActionRewards), std::move(transitionRewards)))); + } + return result; + } + + template + std::shared_ptr> SparseModelMemoryProduct::buildResult(storm::storage::SparseMatrix&& matrix, storm::models::sparse::StateLabeling&& labeling, std::unordered_map>&& rewardModels) const { + switch (model.getType()) { + case storm::models::ModelType::Dtmc: + return std::make_shared> (std::move(matrix), std::move(labeling), std::move(rewardModels)); + case storm::models::ModelType::Mdp: + return std::make_shared> (std::move(matrix), std::move(labeling), std::move(rewardModels)); + case storm::models::ModelType::Ctmc: + return std::make_shared> (std::move(matrix), std::move(labeling), std::move(rewardModels)); + case storm::models::ModelType::MarkovAutomaton: + { + // We also need to translate the exit rates and the Markovian states + uint_fast64_t numResStates = matrix.getRowGroupCount(); + uint_fast64_t memoryStateCount = memory.getNumberOfStates(); + std::vector resultExitRates; + resultExitRates.reserve(matrix.getRowGroupCount()); + storm::storage::BitVector resultMarkovianStates(numResStates, false); + auto const& modelExitRates = dynamic_cast const&>(model).getExitRates(); + auto const& modelMarkovianStates = dynamic_cast const&>(model).getMarkovianStates(); + + uint_fast64_t stateIndex = 0; + for (auto const& resState : toResultStateMapping) { + if (resState < numResStates) { + assert(resState == resultExitRates.size()); + uint_fast64_t modelState = stateIndex / memoryStateCount; + resultExitRates.push_back(modelExitRates[modelState]); + if (modelMarkovianStates.get(modelState)) { + resultMarkovianStates.set(resState, true); + } + } + ++stateIndex; + } + return std::make_shared> (std::move(matrix), std::move(labeling), std::move(resultMarkovianStates), std::move(resultExitRates), true, std::move(rewardModels)); + } + default: + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Memory Structure Product for Model Type " << model.getType() << " is not supported"); + } + } + + template class SparseModelMemoryProduct; + template class SparseModelMemoryProduct; + template class SparseModelMemoryProduct; + + } +} + + diff --git a/src/storm/storage/memorystructure/SparseModelMemoryProduct.h b/src/storm/storage/memorystructure/SparseModelMemoryProduct.h new file mode 100644 index 000000000..170efba3f --- /dev/null +++ b/src/storm/storage/memorystructure/SparseModelMemoryProduct.h @@ -0,0 +1,72 @@ +#pragma once + +#include +#include +#include + +#include "storm/storage/BitVector.h" +#include "storm/storage/memorystructure/MemoryStructure.h" +#include "storm/models/sparse/Model.h" +#include "storm/models/sparse/StandardRewardModel.h" + +namespace storm { + namespace storage { + /*! + * This class builds the product of the given sparse model and the given memory structure. + * This is similar to the well-known product of a model with a deterministic rabin automaton. + * Note: we already do one memory-structure-step for the initial state, i.e., if s is an initial state of + * the given model and s satisfies memoryStructure.getTransitionMatrix[0][n], then (s,n) will be the corresponding + * initial state of the resulting model. + * + * The states of the resulting sparse model will have the original state labels plus the labels of this + * memory structure. + * An exception is thrown if the state labelings are not disjoint. + */ + template + class SparseModelMemoryProduct { + public: + + SparseModelMemoryProduct(storm::models::sparse::Model const& sparseModel, storm::storage::MemoryStructure const& memoryStructure); + + // Invokes the building of the product + std::shared_ptr> build(); + + // Retrieves the state of the resulting model that represents the given memory and model state. + // An invalid index is returned, if the specifyied state does not exist (i.e., if it is not reachable). + uint_fast64_t const& getResultState(uint_fast64_t const& modelState, uint_fast64_t const& memoryState) const; + + private: + + // Computes for each pair of memory and model state the successor memory state + // The resulting vector maps (modelState * memoryStateCount) + memoryState to the corresponding successor state of the memory structure + std::vector computeMemorySuccessors() const; + + // Computes the reachable states of the resulting model + storm::storage::BitVector computeReachableStates(std::vector const& memorySuccessors, storm::storage::BitVector const& initialStates) const; + + // Methods that build the model components + // Matrix for deterministic models + storm::storage::SparseMatrix buildDeterministicTransitionMatrix(storm::storage::BitVector const& reachableStates, std::vector const& memorySuccessors) const; + // Matrix for nondeterministic models + storm::storage::SparseMatrix buildNondeterministicTransitionMatrix(storm::storage::BitVector const& reachableStates, std::vector const& memorySuccessors) const; + // State labeling. Note: DOES NOT ADD A LABEL FOR THE INITIAL STATES + storm::models::sparse::StateLabeling buildStateLabeling(storm::storage::SparseMatrix const& resultTransitionMatrix) const; + // Reward models + std::unordered_map> buildRewardModels(storm::storage::SparseMatrix const& resultTransitionMatrix, std::vector const& memorySuccessors) const; + + // Builds the resulting model + std::shared_ptr> buildResult(storm::storage::SparseMatrix&& matrix, storm::models::sparse::StateLabeling&& labeling, std::unordered_map>&& rewardModels) const; + + + // Maps (modelState * memoryStateCount) + memoryState to the state in the result that represents (memoryState,modelState) + std::vector toResultStateMapping; + + + storm::models::sparse::Model const& model; + storm::storage::MemoryStructure const& memory; + + }; + } +} + + diff --git a/src/storm/transformer/GoalStateMerger.cpp b/src/storm/transformer/GoalStateMerger.cpp index f9b81f3f6..a6a0b21dc 100644 --- a/src/storm/transformer/GoalStateMerger.cpp +++ b/src/storm/transformer/GoalStateMerger.cpp @@ -2,15 +2,18 @@ #include #include +#include #include "storm/utility/constants.h" #include "storm/utility/macros.h" #include "storm/utility/vector.h" #include "storm/models/sparse/Dtmc.h" #include "storm/models/sparse/Mdp.h" +#include "storm/models/sparse/MarkovAutomaton.h" #include "storm/models/sparse/StandardRewardModel.h" #include "storm/exceptions/InvalidArgumentException.h" +#include "storm/exceptions/UnexpectedException.h" namespace storm { @@ -22,166 +25,267 @@ namespace storm { } template - std::shared_ptr GoalStateMerger::mergeTargetAndSinkStates(storm::storage::BitVector const& maybeStates, storm::storage::BitVector& targetStates, storm::storage::BitVector& sinkStates, std::vector const& selectedRewardModels) { + typename GoalStateMerger::ReturnType GoalStateMerger::mergeTargetAndSinkStates(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates, std::vector const& selectedRewardModels) const { STORM_LOG_THROW(maybeStates.isDisjointFrom(targetStates) && targetStates.isDisjointFrom(sinkStates) && sinkStates.isDisjointFrom(maybeStates), storm::exceptions::InvalidArgumentException, "maybestates, targetstates, and sinkstates are assumed to be disjoint when creating the submodel. However, this is not the case."); - boost::optional targetState, sinkState; - auto builder = initializeTransitionMatrixBuilder(maybeStates, targetStates, sinkStates, targetState, sinkState); - auto transitionMatrix = buildTransitionMatrix(maybeStates, targetStates, sinkStates, targetState, sinkState, builder); + auto result = initialize(maybeStates, targetStates, sinkStates); - uint_fast64_t resNumStates = transitionMatrix.getRowGroupCount(); - - // Get the labeling for the initial states - storm::storage::BitVector initialStates = originalModel.getInitialStates() % maybeStates; - initialStates.resize(resNumStates, false); - if(!originalModel.getInitialStates().isDisjointFrom(targetStates)) { - initialStates.set(*targetState, true); - } - if(!originalModel.getInitialStates().isDisjointFrom(sinkStates)) { - initialStates.set(*sinkState, true); - } - storm::models::sparse::StateLabeling labeling(resNumStates); - labeling.addLabel("init", std::move(initialStates)); - - // Get the reward models - std::unordered_map rewardModels; - for (auto rewardModelName : selectedRewardModels) { - auto totalRewards = originalModel.getRewardModel(rewardModelName).getTotalRewardVector(originalModel.getTransitionMatrix()); - auto choicesOfMaybeStates = originalModel.getTransitionMatrix().getRowFilter(maybeStates); - storm::utility::vector::filterVectorInPlace(totalRewards, choicesOfMaybeStates); - // add zero reward for the sink and goal states (if they exists) - totalRewards.resize(transitionMatrix.getRowCount(), storm::utility::zero()); - rewardModels.insert(std::make_pair(rewardModelName, typename SparseModelType::RewardModelType(boost::none, totalRewards))); - } - - // modify the given target and sink states - targetStates = storm::storage::BitVector(resNumStates, false); - if(targetState) { - targetStates.set(*targetState, true); - } - sinkStates = storm::storage::BitVector(resNumStates, false); - if(sinkState) { - sinkStates.set(*sinkState, true); - } - - // Return the result - return std::make_shared(std::move(transitionMatrix), std::move(labeling), std::move(rewardModels)); + auto transitionMatrix = buildTransitionMatrix(maybeStates, result.first, result.second); + auto labeling = buildStateLabeling(maybeStates, targetStates, sinkStates, result.first); + auto rewardModels = buildRewardModels(maybeStates, result.first, selectedRewardModels); + + result.first.model = buildOutputModel(maybeStates, result.first, std::move(transitionMatrix), std::move(labeling), std::move(rewardModels)); + + return result.first; } template - storm::storage::SparseMatrixBuilder GoalStateMerger::initializeTransitionMatrixBuilder(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates, boost::optional& newTargetState, boost::optional& newSinkState) { + std::pair::ReturnType, uint_fast64_t> GoalStateMerger::initialize(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates) const { storm::storage::SparseMatrix const& origMatrix = originalModel.getTransitionMatrix(); - - // Get the number of rows, cols and entries that the resulting transition matrix will have. - uint_fast64_t resNumStates(maybeStates.getNumberOfSetBits()), resNumActions(0), resNumTransitions(0); + + ReturnType result; + result.keptChoices = storm::storage::BitVector(origMatrix.getRowCount(), false); + result.oldToNewStateIndexMapping = std::vector(maybeStates.size(), std::numeric_limits::max()); // init with some invalid state + + uint_fast64_t transitionCount(0), stateCount(0); bool targetStateRequired = !originalModel.getInitialStates().isDisjointFrom(targetStates); bool sinkStateRequired = !originalModel.getInitialStates().isDisjointFrom(sinkStates); for( auto state : maybeStates) { - resNumActions += origMatrix.getRowGroupSize(state); + result.oldToNewStateIndexMapping[state] = stateCount; + auto const& endOfRowGroup = origMatrix.getRowGroupIndices()[state+1]; + bool stateIsDeadlock = true; for (uint_fast64_t row = origMatrix.getRowGroupIndices()[state]; row < endOfRowGroup; ++row) { - bool hasTransitionToTarget(false), hasTransitionToSink(false); + uint_fast64_t transitionsToMaybeStates = 0; + bool keepThisRow(true), hasTransitionToTarget(false), hasTransitionToSink(false); for (auto const& entry : origMatrix.getRow(row)) { - if(maybeStates.get(entry.getColumn())) { - ++resNumTransitions; + if (maybeStates.get(entry.getColumn())) { + ++transitionsToMaybeStates; } else if (targetStates.get(entry.getColumn())) { hasTransitionToTarget = true; } else if (sinkStates.get(entry.getColumn())) { hasTransitionToSink = true; } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "There is a transition originating from a maybestate that does not lead to a maybe-, target-, or sinkstate."); + keepThisRow = false; + break; } } - if(hasTransitionToTarget) { - ++resNumTransitions; - targetStateRequired = true; - } - if(hasTransitionToSink) { - ++resNumTransitions; - sinkStateRequired = true; + if (keepThisRow) { + stateIsDeadlock = false; + result.keptChoices.set(row, true); + transitionCount += transitionsToMaybeStates; + if (hasTransitionToTarget) { + ++transitionCount; + targetStateRequired = true; + } + if (hasTransitionToSink) { + ++transitionCount; + sinkStateRequired = true; + } } + STORM_LOG_THROW(!stateIsDeadlock, storm::exceptions::InvalidArgumentException, "Merging goal states leads to deadlocks!"); } + ++stateCount; } - // Get the index of the target/ sink state in the resulting model (if these states will exist) - if(targetStateRequired) { - newTargetState = resNumStates; - ++resNumStates; - ++resNumActions; - ++resNumTransitions; + // Treat the target and sink states (if these states will exist) + if (targetStateRequired) { + result.targetState = stateCount; + ++stateCount; + ++transitionCount; + storm::utility::vector::setVectorValues(result.oldToNewStateIndexMapping, targetStates, *result.targetState); } - if(sinkStateRequired) { - newSinkState = resNumStates; - ++resNumStates; - ++resNumActions; - ++resNumTransitions; + + if (sinkStateRequired) { + result.sinkState = stateCount; + ++stateCount; + ++transitionCount; + storm::utility::vector::setVectorValues(result.oldToNewStateIndexMapping, sinkStates, *result.sinkState); } - return storm::storage::SparseMatrixBuilder(resNumActions, resNumStates, resNumTransitions, true, true, resNumStates); + return std::make_pair(std::move(result), std::move(transitionCount)); } template - storm::storage::SparseMatrix GoalStateMerger::buildTransitionMatrix(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates, boost::optional const& newTargetState, boost::optionalconst& newSinkState, storm::storage::SparseMatrixBuilder& builder) { + storm::storage::SparseMatrix GoalStateMerger::buildTransitionMatrix(storm::storage::BitVector const& maybeStates, ReturnType const& resultData, uint_fast64_t transitionCount) const { - // Get a Mapping that yields for each column in the old matrix the corresponding column in the new matrix - std::vector oldToNewIndexMap(maybeStates.size(), std::numeric_limits::max()); // init with some invalid state - uint_fast64_t newStateIndex = 0; - for (auto maybeState : maybeStates) { - oldToNewIndexMap[maybeState] = newStateIndex; - ++newStateIndex; - } - - // Build the transition matrix storm::storage::SparseMatrix const& origMatrix = originalModel.getTransitionMatrix(); + + uint_fast64_t rowCount = resultData.keptChoices.getNumberOfSetBits() + (resultData.targetState ? 1 : 0) + (resultData.sinkState ? 1 : 0); + uint_fast64_t maybeStateCount = maybeStates.getNumberOfSetBits(); + uint_fast64_t stateCount = maybeStateCount + (resultData.targetState ? 1 : 0) + (resultData.sinkState ? 1 : 0); + storm::storage::SparseMatrixBuilder builder(rowCount, stateCount, transitionCount, true, !origMatrix.hasTrivialRowGrouping(), origMatrix.hasTrivialRowGrouping() ? 0 : stateCount); + uint_fast64_t currRow = 0; for (auto state : maybeStates) { - builder.newRowGroup(currRow); - auto const& endOfRowGroup = origMatrix.getRowGroupIndices()[state+1]; - for (uint_fast64_t row = origMatrix.getRowGroupIndices()[state]; row < endOfRowGroup; ++row) { - boost::optional targetProbability, sinkProbability; + if (!origMatrix.hasTrivialRowGrouping()) { + builder.newRowGroup(currRow); + } + auto const& endOfRowGroup = origMatrix.getRowGroupIndices()[state + 1]; + for (uint_fast64_t row = resultData.keptChoices.getNextSetIndex(origMatrix.getRowGroupIndices()[state]); row < endOfRowGroup; row = resultData.keptChoices.getNextSetIndex(row + 1)) { + boost::optional targetValue, sinkValue; for (auto const& entry : origMatrix.getRow(row)) { - if(maybeStates.get(entry.getColumn())) { - builder.addNextValue(currRow, oldToNewIndexMap[entry.getColumn()], entry.getValue()); - } else if (targetStates.get(entry.getColumn())) { - targetProbability = targetProbability.is_initialized() ? *targetProbability + entry.getValue() : entry.getValue(); - } else if (sinkStates.get(entry.getColumn())) { - sinkProbability = sinkProbability.is_initialized() ? *sinkProbability + entry.getValue() : entry.getValue(); + uint_fast64_t const& newColumn = resultData.oldToNewStateIndexMapping[entry.getColumn()]; + if (newColumn < maybeStateCount) { + builder.addNextValue(currRow, newColumn, entry.getValue()); + } else if (resultData.targetState && newColumn == resultData.targetState.get()) { + targetValue = targetValue.is_initialized() ? *targetValue + entry.getValue() : entry.getValue(); + } else if (resultData.sinkState && newColumn == resultData.sinkState.get()) { + sinkValue = sinkValue.is_initialized() ? *sinkValue + entry.getValue() : entry.getValue(); } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "There is a transition originating from a maybestate that does not lead to a maybe-, target-, or sinkstate."); + STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "There is a transition originating from a maybestate that does not lead to a maybe-, target-, or sinkstate."); } } - if(targetProbability) { - assert(newTargetState); - builder.addNextValue(currRow, *newTargetState, storm::utility::simplify(*targetProbability)); + if (targetValue) { + builder.addNextValue(currRow, *resultData.targetState, storm::utility::simplify(*targetValue)); } - if(sinkProbability) { - assert(newSinkState); - builder.addNextValue(currRow, *newSinkState, storm::utility::simplify(*sinkProbability)); + if (sinkValue) { + builder.addNextValue(currRow, *resultData.sinkState, storm::utility::simplify(*sinkValue)); } ++currRow; } } + // Add the selfloops at target and sink - if(newTargetState) { - builder.newRowGroup(currRow); - builder.addNextValue(currRow, *newTargetState, storm::utility::one()); + if (resultData.targetState) { + if (!origMatrix.hasTrivialRowGrouping()) { + builder.newRowGroup(currRow); + } + builder.addNextValue(currRow, *resultData.targetState, storm::utility::one()); ++currRow; } - if(newSinkState) { - builder.newRowGroup(currRow); - builder.addNextValue(currRow, *newSinkState, storm::utility::one()); + if (resultData.sinkState) { + if (!origMatrix.hasTrivialRowGrouping()) { + builder.newRowGroup(currRow); + } + builder.addNextValue(currRow, *resultData.sinkState, storm::utility::one()); ++currRow; } return builder.build(); } + + template + storm::models::sparse::StateLabeling GoalStateMerger::buildStateLabeling(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates, ReturnType const& resultData) const { + + uint_fast64_t stateCount = maybeStates.getNumberOfSetBits() + (resultData.targetState ? 1 : 0) + (resultData.sinkState ? 1 : 0); + storm::models::sparse::StateLabeling labeling(stateCount); + + for (auto const& label : originalModel.getStateLabeling().getLabels()) { + storm::storage::BitVector const& oldStatesWithLabel = originalModel.getStates(label); + storm::storage::BitVector newStatesWithLabel = oldStatesWithLabel % maybeStates; + newStatesWithLabel.resize(stateCount, false); + if (!oldStatesWithLabel.isDisjointFrom(targetStates) && resultData.targetState.is_initialized()) { + newStatesWithLabel.set(*resultData.targetState, true); + } + if (!oldStatesWithLabel.isDisjointFrom(sinkStates) && resultData.sinkState.is_initialized()) { + newStatesWithLabel.set(*resultData.sinkState, true); + } + labeling.addLabel(label, std::move(newStatesWithLabel)); + } + + return labeling; + } + + template + std::unordered_map GoalStateMerger::buildRewardModels(storm::storage::BitVector const& maybeStates, ReturnType const& resultData, std::vector const& selectedRewardModels) const { + + typedef typename SparseModelType::RewardModelType::ValueType RewardValueType; + + uint_fast64_t maybeStateCount = maybeStates.getNumberOfSetBits(); + uint_fast64_t stateCount = maybeStateCount + (resultData.targetState ? 1 : 0) + (resultData.sinkState ? 1 : 0); + uint_fast64_t choiceCount = resultData.keptChoices.getNumberOfSetBits() + (resultData.targetState ? 1 : 0) + (resultData.sinkState ? 1 : 0); + + std::unordered_map rewardModels; + for (auto rewardModelName : selectedRewardModels) { + auto origRewardModel = originalModel.getRewardModel(rewardModelName); + + boost::optional> stateRewards; + if (origRewardModel.hasStateRewards()) { + stateRewards = storm::utility::vector::filterVector(origRewardModel.getStateRewardVector(), maybeStates); + stateRewards->resize(stateCount, storm::utility::zero()); + } + + boost::optional> stateActionRewards; + if (origRewardModel.hasStateActionRewards()) { + stateActionRewards = storm::utility::vector::filterVector(origRewardModel.getStateActionRewardVector(), resultData.keptChoices); + stateActionRewards->resize(choiceCount, storm::utility::zero()); + } + + boost::optional> transitionRewards; + if (origRewardModel.hasTransitionRewards()) { + storm::storage::SparseMatrixBuilder builder(choiceCount, stateCount, 0, true); + for (auto const& row : resultData.keptChoices) { + boost::optional targetValue, sinkValue; + for (auto const& entry : origRewardModel.getTransitionRewardMatrix().getRow(row)) { + uint_fast64_t const& newColumn = resultData.oldToNewStateIndexMapping[entry.getColumn()]; + if (newColumn < maybeStateCount) { + builder.addNextValue(row, newColumn, entry.getValue()); + } else if (resultData.targetState && newColumn == resultData.targetState.get()) { + targetValue = targetValue.is_initialized() ? *targetValue + entry.getValue() : entry.getValue(); + } else if (resultData.sinkState && newColumn == resultData.sinkState.get()) { + sinkValue = sinkValue.is_initialized() ? *sinkValue + entry.getValue() : entry.getValue(); + } else { + STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "There is a transition reward originating from a maybestate that does not lead to a maybe-, target-, or sinkstate."); + } + } + if (targetValue) { + builder.addNextValue(row, *resultData.targetState, storm::utility::simplify(*targetValue)); + } + if (sinkValue) { + builder.addNextValue(row, *resultData.sinkState, storm::utility::simplify(*sinkValue)); + } + } + transitionRewards = builder.build(); + } + + rewardModels.insert(std::make_pair(rewardModelName, typename SparseModelType::RewardModelType(std::move(stateRewards), std::move(stateActionRewards), std::move(transitionRewards)))); + } + return rewardModels; + } + + template <> + std::shared_ptr> GoalStateMerger>::buildOutputModel(storm::storage::BitVector const& maybeStates, ReturnType const& resultData, storm::storage::SparseMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& labeling, std::unordered_map::RewardModelType>&& rewardModels) const { + + uint_fast64_t stateCount = maybeStates.getNumberOfSetBits() + (resultData.targetState ? 1 : 0) + (resultData.sinkState ? 1 : 0); + + storm::storage::BitVector markovianStates = originalModel.getMarkovianStates() % maybeStates; + markovianStates.resize(stateCount, true); + + std::vector exitRates = storm::utility::vector::filterVector(originalModel.getExitRates(), maybeStates); + exitRates.resize(stateCount, storm::utility::one()); + + return std::make_shared> (std::move(transitionMatrix), std::move(labeling), std::move(markovianStates), std::move(exitRates), true, std::move(rewardModels)); + } + template <> + std::shared_ptr> GoalStateMerger>::buildOutputModel(storm::storage::BitVector const& maybeStates, ReturnType const& resultData, storm::storage::SparseMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& labeling, std::unordered_map::RewardModelType>&& rewardModels) const { + + uint_fast64_t stateCount = maybeStates.getNumberOfSetBits() + (resultData.targetState ? 1 : 0) + (resultData.sinkState ? 1 : 0); + + storm::storage::BitVector markovianStates = originalModel.getMarkovianStates() % maybeStates; + markovianStates.resize(stateCount, true); + + std::vector exitRates = storm::utility::vector::filterVector(originalModel.getExitRates(), maybeStates); + exitRates.resize(stateCount, storm::utility::one()); + + return std::make_shared> (std::move(transitionMatrix), std::move(labeling), std::move(markovianStates), std::move(exitRates), true, std::move(rewardModels)); + } + + template + std::shared_ptr GoalStateMerger::buildOutputModel(storm::storage::BitVector const& maybeStates, GoalStateMerger::ReturnType const& resultData, storm::storage::SparseMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& labeling, std::unordered_map&& rewardModels) const { + + return std::make_shared(std::move(transitionMatrix), std::move(labeling), std::move(rewardModels)); + } + template class GoalStateMerger>; template class GoalStateMerger>; + template class GoalStateMerger>; template class GoalStateMerger>; template class GoalStateMerger>; + template class GoalStateMerger>; template class GoalStateMerger>; template class GoalStateMerger>; diff --git a/src/storm/transformer/GoalStateMerger.h b/src/storm/transformer/GoalStateMerger.h index 712eb9af6..bc9dadcda 100644 --- a/src/storm/transformer/GoalStateMerger.h +++ b/src/storm/transformer/GoalStateMerger.h @@ -3,56 +3,65 @@ #include #include #include +#include #include #include "storm/storage/BitVector.h" #include "storm/storage/SparseMatrix.h" +#include "storm/models/sparse/StateLabeling.h" namespace storm { namespace transformer { /* - * Merges the given target and sink states into a single state with a selfloop + * Merges the given target and sink states into single states with a selfloop */ template class GoalStateMerger { public: + + struct ReturnType { + std::shared_ptr model; // The output model + boost::optional targetState; // The target state of the output model (if reachable) + boost::optional sinkState; // The sink state of the output model (if reachable) + std::vector oldToNewStateIndexMapping; // maps a state from the input model to the corresponding state of the output model. Invalid index if the state does not exist + storm::storage::BitVector keptChoices; // The choices of the input model that are still present in the output model + }; GoalStateMerger(SparseModelType const& model); /* Computes a submodel of the specified model that only considers the states given by maybeStates as well as * * one target state to which all transitions to a state selected by targetStates are redirected and * * one sink state to which all transitions to a state selected by sinkStates are redirected. - * If there is no transition to either target or sink, the corresponding state will not be created. - * - * The two given bitvectors targetStates and sinkStates are modified such that they represent the corresponding state in the obtained submodel. * * Notes: - * * The resulting model will not have any labels (other then "init") and only the selected reward models. - * * Rewards are reduced to stateActionRewards. - * * The target and sink states will not get any reward - * * It is assumed that the given set of maybeStates can only be left via either a target or a sink state. Otherwise an exception is thrown. - * * It is assumed that maybeStates, targetStates, and sinkStates are all disjoint. Otherwise an exception is thrown. + * * the target (or sink) state is not created, if it is not reachable + * * the target (or sink) state will get a label iff it is reachable and at least one of the given targetStates (sinkStates) have that label. + * * Only the selected reward models will be kept. The target and sink states will not get any reward. + * * Choices that lead from a maybeState to a ~(target | sink) state will be removed. An exception is thrown if this leads to deadlocks. + * * It is assumed that maybeStates, targetStates, and sinkStates are pairwise disjoint. Otherwise an exception is thrown. + * * The order of the maybeStates will not be affected (i.e. s_1 < s_2 in the input model implies s'_1 < s'_2 in the output model). */ - std::shared_ptr mergeTargetAndSinkStates(storm::storage::BitVector const& maybeStates, storm::storage::BitVector& targetStates, storm::storage::BitVector& sinkStates, std::vector const& selectedRewardModels = std::vector()); + ReturnType mergeTargetAndSinkStates(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates, std::vector const& selectedRewardModels = std::vector()) const; private: SparseModelType const& originalModel; /*! - * Initializes the matrix builder for the transition matrix of the resulting model + * Initializes the data required to build the result model * - * @param newTargetState Will be set to the index of the target state of the resulting model (Only if it has a target state) - * @param newSinkState Will be set to the index of the sink state of the resulting model (Only if it has a sink state) + * @return The initialized result and the number of transitions of the result model */ - storm::storage::SparseMatrixBuilder initializeTransitionMatrixBuilder(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates, boost::optional& newTargetState, boost::optional& newSinkState); + std::pair initialize(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates) const; /*! * Builds the transition matrix of the resulting model */ - storm::storage::SparseMatrix buildTransitionMatrix(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates, boost::optional const& newTargetState, boost::optional const& newSinkState, storm::storage::SparseMatrixBuilder& builder); - + storm::storage::SparseMatrix buildTransitionMatrix(storm::storage::BitVector const& maybeStates, ReturnType const& resultData, uint_fast64_t transitionCount) const; + storm::models::sparse::StateLabeling buildStateLabeling(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates, ReturnType const& resultData) const; + std::unordered_map buildRewardModels(storm::storage::BitVector const& maybeStates, ReturnType const& resultData, std::vector const& selectedRewardModels) const; + std::shared_ptr buildOutputModel(storm::storage::BitVector const& maybeStates, ReturnType const& resultData, storm::storage::SparseMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& labeling, std::unordered_map&& rewardModels) const; }; } diff --git a/src/storm/transformer/SparseParametricDtmcSimplifier.cpp b/src/storm/transformer/SparseParametricDtmcSimplifier.cpp index 9e10e1fda..972863b1b 100644 --- a/src/storm/transformer/SparseParametricDtmcSimplifier.cpp +++ b/src/storm/transformer/SparseParametricDtmcSimplifier.cpp @@ -38,17 +38,32 @@ namespace storm { // obtain the resulting subsystem storm::transformer::GoalStateMerger goalStateMerger(this->originalModel); - this->simplifiedModel = goalStateMerger.mergeTargetAndSinkStates(maybeStates, statesWithProbability01.second, statesWithProbability01.first); - this->simplifiedModel->getStateLabeling().addLabel("target", statesWithProbability01.second); - this->simplifiedModel->getStateLabeling().addLabel("sink", statesWithProbability01.first); + typename storm::transformer::GoalStateMerger::ReturnType mergerResult = goalStateMerger.mergeTargetAndSinkStates(maybeStates, statesWithProbability01.second, statesWithProbability01.first); + this->simplifiedModel = mergerResult.model; + statesWithProbability01.second = storm::storage::BitVector(this->simplifiedModel->getNumberOfStates(), false); + if (mergerResult.targetState) { + statesWithProbability01.second.set(mergerResult.targetState.get(), true); + } + std::string targetLabel = "target"; + while (this->simplifiedModel->hasLabel(targetLabel)) { + targetLabel = "_" + targetLabel; + } + this->simplifiedModel->getStateLabeling().addLabel(targetLabel, std::move(statesWithProbability01.second)); // obtain the simplified formula for the simplified model - auto labelFormula = std::make_shared ("target"); + auto labelFormula = std::make_shared (targetLabel); auto eventuallyFormula = std::make_shared(labelFormula, storm::logic::FormulaContext::Probability); this->simplifiedFormula = std::make_shared(eventuallyFormula, formula.getOperatorInformation()); // Eliminate all states for which all outgoing transitions are constant - this->simplifiedModel = this->eliminateConstantDeterministicStates(*this->simplifiedModel); + storm::storage::BitVector considerForElimination = ~this->simplifiedModel->getInitialStates(); + if (mergerResult.targetState) { + considerForElimination.set(*mergerResult.targetState, false); + } + if (mergerResult.sinkState) { + considerForElimination.set(*mergerResult.sinkState, false); + } + this->simplifiedModel = this->eliminateConstantDeterministicStates(*this->simplifiedModel, considerForElimination); return true; } @@ -82,12 +97,20 @@ namespace storm { // obtain the resulting subsystem storm::transformer::GoalStateMerger goalStateMerger(this->originalModel); - this->simplifiedModel = goalStateMerger.mergeTargetAndSinkStates(maybeStates, prob0States, psiStates); - this->simplifiedModel->getStateLabeling().addLabel("target", psiStates); - this->simplifiedModel->getStateLabeling().addLabel("sink", prob0States); + typename storm::transformer::GoalStateMerger::ReturnType mergerResult = goalStateMerger.mergeTargetAndSinkStates(maybeStates, psiStates, prob0States); + this->simplifiedModel = mergerResult.model; + psiStates = storm::storage::BitVector(this->simplifiedModel->getNumberOfStates(), false); + if (mergerResult.targetState) { + psiStates.set(mergerResult.targetState.get(), true); + } + std::string targetLabel = "target"; + while (this->simplifiedModel->hasLabel(targetLabel)) { + targetLabel = "_" + targetLabel; + } + this->simplifiedModel->getStateLabeling().addLabel(targetLabel, std::move(psiStates)); // obtain the simplified formula for the simplified model - auto labelFormula = std::make_shared ("target"); + auto labelFormula = std::make_shared (targetLabel); auto boundedUntilFormula = std::make_shared(storm::logic::Formula::getTrueFormula(), labelFormula, boost::none, storm::logic::TimeBound(formula.getSubformula().asBoundedUntilFormula().isUpperBoundStrict(), formula.getSubformula().asBoundedUntilFormula().getUpperBound()), storm::logic::TimeBoundType::Steps); this->simplifiedFormula = std::make_shared(boundedUntilFormula, formula.getOperatorInformation()); @@ -116,17 +139,32 @@ namespace storm { // obtain the resulting subsystem std::vector rewardModelNameAsVector(1, formula.hasRewardModelName() ? formula.getRewardModelName() : this->originalModel.getRewardModels().begin()->first); storm::transformer::GoalStateMerger goalStateMerger(this->originalModel); - this->simplifiedModel = goalStateMerger.mergeTargetAndSinkStates(maybeStates, targetStates, infinityStates, rewardModelNameAsVector); - this->simplifiedModel->getStateLabeling().addLabel("target", targetStates); - this->simplifiedModel->getStateLabeling().addLabel("sink", infinityStates); + typename storm::transformer::GoalStateMerger::ReturnType mergerResult = goalStateMerger.mergeTargetAndSinkStates(maybeStates, targetStates, infinityStates, rewardModelNameAsVector); + this->simplifiedModel = mergerResult.model; + targetStates = storm::storage::BitVector(this->simplifiedModel->getNumberOfStates(), false); + if (mergerResult.targetState) { + targetStates.set(mergerResult.targetState.get(), true); + } + std::string targetLabel = "target"; + while (this->simplifiedModel->hasLabel(targetLabel)) { + targetLabel = "_" + targetLabel; + } + this->simplifiedModel->getStateLabeling().addLabel(targetLabel, std::move(targetStates)); // obtain the simplified formula for the simplified model - auto labelFormula = std::make_shared ("target"); + auto labelFormula = std::make_shared (targetLabel); auto eventuallyFormula = std::make_shared(labelFormula, storm::logic::FormulaContext::Reward); this->simplifiedFormula = std::make_shared(eventuallyFormula, rewardModelNameAsVector.front(), formula.getOperatorInformation(), storm::logic::RewardMeasureType::Expectation); // Eliminate all states for which all outgoing transitions are constant - this->simplifiedModel = this->eliminateConstantDeterministicStates(*this->simplifiedModel, rewardModelNameAsVector.front()); + storm::storage::BitVector considerForElimination = ~this->simplifiedModel->getInitialStates(); + if (mergerResult.targetState) { + considerForElimination.set(*mergerResult.targetState, false); + } + if (mergerResult.sinkState) { + considerForElimination.set(*mergerResult.sinkState, false); + } + this->simplifiedModel = this->eliminateConstantDeterministicStates(*this->simplifiedModel, considerForElimination, rewardModelNameAsVector.front()); return true; } @@ -151,7 +189,8 @@ namespace storm { // obtain the resulting subsystem std::vector rewardModelNameAsVector(1, formula.hasRewardModelName() ? formula.getRewardModelName() : this->originalModel.getRewardModels().begin()->first); storm::transformer::GoalStateMerger goalStateMerger(this->originalModel); - this->simplifiedModel = goalStateMerger.mergeTargetAndSinkStates(maybeStates, noStates, zeroRewardStates, rewardModelNameAsVector); + typename storm::transformer::GoalStateMerger::ReturnType mergerResult = goalStateMerger.mergeTargetAndSinkStates(maybeStates, noStates, zeroRewardStates, rewardModelNameAsVector); + this->simplifiedModel = mergerResult.model; // obtain the simplified formula for the simplified model this->simplifiedFormula = storm::logic::CloneVisitor().clone(formula); diff --git a/src/storm/transformer/SparseParametricMdpSimplifier.cpp b/src/storm/transformer/SparseParametricMdpSimplifier.cpp index 192545b2d..d84058637 100644 --- a/src/storm/transformer/SparseParametricMdpSimplifier.cpp +++ b/src/storm/transformer/SparseParametricMdpSimplifier.cpp @@ -45,21 +45,45 @@ namespace storm { // obtain the resulting subsystem storm::transformer::GoalStateMerger goalStateMerger(this->originalModel); - this->simplifiedModel = goalStateMerger.mergeTargetAndSinkStates(maybeStates, statesWithProbability01.second, statesWithProbability01.first); - this->simplifiedModel->getStateLabeling().addLabel("target", statesWithProbability01.second); - this->simplifiedModel->getStateLabeling().addLabel("sink", statesWithProbability01.first); + typename storm::transformer::GoalStateMerger::ReturnType mergerResult = goalStateMerger.mergeTargetAndSinkStates(maybeStates, statesWithProbability01.second, statesWithProbability01.first); + this->simplifiedModel = mergerResult.model; + statesWithProbability01.first = storm::storage::BitVector(this->simplifiedModel->getNumberOfStates(), false); + if (mergerResult.sinkState) { + statesWithProbability01.first.set(mergerResult.sinkState.get(), true); + } + std::string sinkLabel = "sink"; + while (this->simplifiedModel->hasLabel(sinkLabel)) { + sinkLabel = "_" + sinkLabel; + } + this->simplifiedModel->getStateLabeling().addLabel(sinkLabel, std::move(statesWithProbability01.first)); + statesWithProbability01.second = storm::storage::BitVector(this->simplifiedModel->getNumberOfStates(), false); + if (mergerResult.targetState) { + statesWithProbability01.second.set(mergerResult.targetState.get(), true); + } + std::string targetLabel = "target"; + while (this->simplifiedModel->hasLabel(targetLabel)) { + targetLabel = "_" + targetLabel; + } + this->simplifiedModel->getStateLabeling().addLabel(targetLabel, std::move(statesWithProbability01.second)); // obtain the simplified formula for the simplified model - auto labelFormula = std::make_shared ("target"); + auto labelFormula = std::make_shared (targetLabel); auto eventuallyFormula = std::make_shared(labelFormula, storm::logic::FormulaContext::Probability); this->simplifiedFormula = std::make_shared(eventuallyFormula, formula.getOperatorInformation()); // Eliminate all states for which all outgoing transitions are constant - this->simplifiedModel = this->eliminateConstantDeterministicStates(*this->simplifiedModel); + storm::storage::BitVector considerForElimination = ~this->simplifiedModel->getInitialStates(); + if (mergerResult.targetState) { + considerForElimination.set(*mergerResult.targetState, false); + } + if (mergerResult.sinkState) { + considerForElimination.set(*mergerResult.sinkState, false); + } + this->simplifiedModel = this->eliminateConstantDeterministicStates(*this->simplifiedModel, considerForElimination); // Eliminate the end components that do not contain a target or a sink state (only required if the probability is maximized) if(!minimizing) { - this->simplifiedModel = this->eliminateNeutralEndComponents(*this->simplifiedModel, this->simplifiedModel->getStates("target") | this->simplifiedModel->getStates("sink")); + this->simplifiedModel = this->eliminateNeutralEndComponents(*this->simplifiedModel, this->simplifiedModel->getStates(targetLabel) | this->simplifiedModel->getStates(sinkLabel)); } return true; @@ -97,12 +121,20 @@ namespace storm { // obtain the resulting subsystem storm::transformer::GoalStateMerger goalStateMerger(this->originalModel); - this->simplifiedModel = goalStateMerger.mergeTargetAndSinkStates(maybeStates, prob0States, psiStates); - this->simplifiedModel->getStateLabeling().addLabel("target", psiStates); - this->simplifiedModel->getStateLabeling().addLabel("sink", prob0States); + typename storm::transformer::GoalStateMerger::ReturnType mergerResult = goalStateMerger.mergeTargetAndSinkStates(maybeStates, psiStates, prob0States); + this->simplifiedModel = mergerResult.model; + psiStates = storm::storage::BitVector(this->simplifiedModel->getNumberOfStates(), false); + if (mergerResult.targetState) { + psiStates.set(mergerResult.targetState.get(), true); + } + std::string targetLabel = "target"; + while (this->simplifiedModel->hasLabel(targetLabel)) { + targetLabel = "_" + targetLabel; + } + this->simplifiedModel->getStateLabeling().addLabel(targetLabel, std::move(psiStates)); // obtain the simplified formula for the simplified model - auto labelFormula = std::make_shared ("target"); + auto labelFormula = std::make_shared (targetLabel); auto boundedUntilFormula = std::make_shared(storm::logic::Formula::getTrueFormula(), labelFormula, boost::none, storm::logic::TimeBound(formula.getSubformula().asBoundedUntilFormula().isUpperBoundStrict(), formula.getSubformula().asBoundedUntilFormula().getUpperBound()), storm::logic::TimeBoundType::Steps); this->simplifiedFormula = std::make_shared(boundedUntilFormula, formula.getOperatorInformation()); @@ -138,21 +170,46 @@ namespace storm { // obtain the resulting subsystem std::vector rewardModelNameAsVector(1, formula.hasRewardModelName() ? formula.getRewardModelName() : this->originalModel.getRewardModels().begin()->first); storm::transformer::GoalStateMerger goalStateMerger(this->originalModel); - this->simplifiedModel = goalStateMerger.mergeTargetAndSinkStates(maybeStates, targetStates, infinityStates, rewardModelNameAsVector); - this->simplifiedModel->getStateLabeling().addLabel("target", targetStates); - this->simplifiedModel->getStateLabeling().addLabel("sink", infinityStates); + typename storm::transformer::GoalStateMerger::ReturnType mergerResult = goalStateMerger.mergeTargetAndSinkStates(maybeStates, targetStates, infinityStates, rewardModelNameAsVector); + this->simplifiedModel = mergerResult.model; + infinityStates = storm::storage::BitVector(this->simplifiedModel->getNumberOfStates(), false); + if (mergerResult.sinkState) { + infinityStates.set(mergerResult.sinkState.get(), true); + } + std::string sinkLabel = "sink"; + while (this->simplifiedModel->hasLabel(sinkLabel)) { + sinkLabel = "_" + sinkLabel; + } + this->simplifiedModel->getStateLabeling().addLabel(sinkLabel, std::move(infinityStates)); + + targetStates = storm::storage::BitVector(this->simplifiedModel->getNumberOfStates(), false); + if (mergerResult.targetState) { + targetStates.set(mergerResult.targetState.get(), true); + } + std::string targetLabel = "target"; + while (this->simplifiedModel->hasLabel(targetLabel)) { + targetLabel = "_" + targetLabel; + } + this->simplifiedModel->getStateLabeling().addLabel(targetLabel, std::move(targetStates)); // obtain the simplified formula for the simplified model - auto labelFormula = std::make_shared ("target"); + auto labelFormula = std::make_shared (targetLabel); auto eventuallyFormula = std::make_shared(labelFormula, storm::logic::FormulaContext::Reward); this->simplifiedFormula = std::make_shared(eventuallyFormula, rewardModelNameAsVector.front(), formula.getOperatorInformation(), storm::logic::RewardMeasureType::Expectation); // Eliminate all states for which all outgoing transitions are constant - this->simplifiedModel = this->eliminateConstantDeterministicStates(*this->simplifiedModel, rewardModelNameAsVector.front()); + storm::storage::BitVector considerForElimination = ~this->simplifiedModel->getInitialStates(); + if (mergerResult.targetState) { + considerForElimination.set(*mergerResult.targetState, false); + } + if (mergerResult.sinkState) { + considerForElimination.set(*mergerResult.sinkState, false); + } + this->simplifiedModel = this->eliminateConstantDeterministicStates(*this->simplifiedModel, considerForElimination, rewardModelNameAsVector.front()); // Eliminate the end components in which no reward is collected (only required if rewards are minimized) if (minimizing) { - this->simplifiedModel = this->eliminateNeutralEndComponents(*this->simplifiedModel, this->simplifiedModel->getStates("target") | this->simplifiedModel->getStates("sink"), rewardModelNameAsVector.front()); + this->simplifiedModel = this->eliminateNeutralEndComponents(*this->simplifiedModel, this->simplifiedModel->getStates(targetLabel) | this->simplifiedModel->getStates(sinkLabel), rewardModelNameAsVector.front()); } return true; } @@ -180,7 +237,8 @@ namespace storm { // obtain the resulting subsystem std::vector rewardModelNameAsVector(1, formula.hasRewardModelName() ? formula.getRewardModelName() : this->originalModel.getRewardModels().begin()->first); storm::transformer::GoalStateMerger goalStateMerger(this->originalModel); - this->simplifiedModel = goalStateMerger.mergeTargetAndSinkStates(maybeStates, noStates, zeroRewardStates, rewardModelNameAsVector); + typename storm::transformer::GoalStateMerger::ReturnType mergerResult = goalStateMerger.mergeTargetAndSinkStates(maybeStates, noStates, zeroRewardStates, rewardModelNameAsVector); + this->simplifiedModel = mergerResult.model; // obtain the simplified formula for the simplified model this->simplifiedFormula = storm::logic::CloneVisitor().clone(formula); diff --git a/src/storm/transformer/SparseParametricModelSimplifier.cpp b/src/storm/transformer/SparseParametricModelSimplifier.cpp index 2dd62ce6b..744e07aa7 100644 --- a/src/storm/transformer/SparseParametricModelSimplifier.cpp +++ b/src/storm/transformer/SparseParametricModelSimplifier.cpp @@ -97,15 +97,9 @@ namespace storm { } template - std::shared_ptr SparseParametricModelSimplifier::eliminateConstantDeterministicStates(SparseModelType const& model, boost::optional const& rewardModelName) { + std::shared_ptr SparseParametricModelSimplifier::eliminateConstantDeterministicStates(SparseModelType const& model, storm::storage::BitVector const& consideredStates, boost::optional const& rewardModelName) { storm::storage::SparseMatrix const& sparseMatrix = model.getTransitionMatrix(); - // Get the states without any label - storm::storage::BitVector considerForElimination(model.getNumberOfStates(), false); - for(auto const& label : model.getStateLabeling().getLabels()) { - considerForElimination |= model.getStateLabeling().getStates(label); - } - considerForElimination.complement(); // get the action-based reward values std::vector actionRewards; @@ -116,8 +110,8 @@ namespace storm { } // Find the states that are to be eliminated - storm::storage::BitVector selectedStates = considerForElimination; - for (auto state : considerForElimination) { + storm::storage::BitVector selectedStates = consideredStates; + for (auto state : consideredStates) { if (sparseMatrix.getRowGroupSize(state) == 1 && (!rewardModelName.is_initialized() || storm::utility::isConstant(actionRewards[sparseMatrix.getRowGroupIndices()[state]]))) { for (auto const& entry : sparseMatrix.getRowGroup(state)) { if(!storm::utility::isConstant(entry.getValue())) { diff --git a/src/storm/transformer/SparseParametricModelSimplifier.h b/src/storm/transformer/SparseParametricModelSimplifier.h index bf1d95214..ac1ae2949 100644 --- a/src/storm/transformer/SparseParametricModelSimplifier.h +++ b/src/storm/transformer/SparseParametricModelSimplifier.h @@ -56,9 +56,10 @@ namespace storm { * * there is no statelabel defined, and * * (if rewardModelName is given) the reward collected at the state is constant. * - * The resulting model will only have the rewardModel with the provided name (or no reward model at all if no name was given) + * The resulting model will only have the rewardModel with the provided name (or no reward model at all if no name was given). + * Labelings of eliminated states will be lost */ - static std::shared_ptr eliminateConstantDeterministicStates(SparseModelType const& model, boost::optional const& rewardModelName = boost::none); + static std::shared_ptr eliminateConstantDeterministicStates(SparseModelType const& model, storm::storage::BitVector const& consideredStates, boost::optional const& rewardModelName = boost::none); SparseModelType const& originalModel; diff --git a/src/storm/utility/graph.cpp b/src/storm/utility/graph.cpp index 98dcd0c71..60f868135 100644 --- a/src/storm/utility/graph.cpp +++ b/src/storm/utility/graph.cpp @@ -103,6 +103,106 @@ namespace storm { return result; } + template + bool checkIfECWithChoiceExists(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& choices) { + + STORM_LOG_THROW(subsystem.size() == transitionMatrix.getRowGroupCount(), storm::exceptions::InvalidArgumentException, "Invalid size of subsystem"); + STORM_LOG_THROW(choices.size() == transitionMatrix.getRowCount(), storm::exceptions::InvalidArgumentException, "Invalid size of choice vector"); + + if (subsystem.empty() || choices.empty()) { + return false; + } + + storm::storage::BitVector statesWithChoice(transitionMatrix.getRowGroupCount(), false); + uint_fast64_t state = 0; + for (auto const& choice : choices) { + // Get the correct state + while (choice >= transitionMatrix.getRowGroupIndices()[state + 1]) { + ++state; + } + assert(choice >= transitionMatrix.getRowGroupIndices()[state]); + // make sure that the choice originates from the subsystem and also stays within the subsystem + if (subsystem.get(state)) { + bool choiceStaysInSubsys = true; + for (auto const& entry : transitionMatrix.getRow(choice)) { + if (!subsystem.get(entry.getColumn())) { + choiceStaysInSubsys = false; + break; + } + } + if (choiceStaysInSubsys) { + statesWithChoice.set(state, true); + } + } + } + + // Initialize candidate states that satisfy some necessary conditions for being part of an EC with a specified choice: + + // Get the states for which a policy can enforce that a choice is reached while staying inside the subsystem + storm::storage::BitVector candidateStates = storm::utility::graph::performProb1E(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, subsystem, statesWithChoice); + + // Only keep the states that can stay in the set of candidates forever + candidateStates = storm::utility::graph::performProb0E(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, candidateStates, ~candidateStates); + + // Only keep the states that can be reached after performing one of the specified choices + statesWithChoice &= candidateStates; + storm::storage::BitVector choiceTargets(transitionMatrix.getRowGroupCount(), false); + for (auto const& state : statesWithChoice) { + for (uint_fast64_t choice = choices.getNextSetIndex(transitionMatrix.getRowGroupIndices()[state]); choice < transitionMatrix.getRowGroupIndices()[state + 1]; choice = choices.getNextSetIndex(choice + 1)) { + bool choiceStaysInCandidateSet = true; + for (auto const& entry : transitionMatrix.getRow(choice)) { + if (!candidateStates.get(entry.getColumn())) { + choiceStaysInCandidateSet = false; + break; + } + } + if (choiceStaysInCandidateSet) { + for (auto const& entry : transitionMatrix.getRow(choice)) { + choiceTargets.set(entry.getColumn(), true); + } + } + } + } + candidateStates = storm::utility::graph::getReachableStates(transitionMatrix, choiceTargets, candidateStates, storm::storage::BitVector(candidateStates.size(), false)); + + // At this point we know that every candidate state can reach a choice at least once without leaving the set of candidate states. + // We now compute the states that can reach a choice at least twice, three times, four times, ... until a fixpoint is reached. + while (!candidateStates.empty()) { + // Update the states with a choice that stays within the set of candidates + statesWithChoice &= candidateStates; + for (auto const& state : statesWithChoice) { + bool stateHasChoice = false; + for (uint_fast64_t choice = choices.getNextSetIndex(transitionMatrix.getRowGroupIndices()[state]); choice < transitionMatrix.getRowGroupIndices()[state + 1]; choice = choices.getNextSetIndex(choice + 1)) { + bool choiceStaysInCandidateSet = true; + for (auto const& entry : transitionMatrix.getRow(choice)) { + if (!candidateStates.get(entry.getColumn())) { + choiceStaysInCandidateSet = false; + break; + } + } + if (choiceStaysInCandidateSet) { + stateHasChoice = true; + break; + } + } + if (!stateHasChoice) { + statesWithChoice.set(state, false); + } + } + + // Update the candidates + storm::storage::BitVector newCandidates = storm::utility::graph::performProb1E(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, candidateStates, statesWithChoice); + + // Check if conferged + if (newCandidates == candidateStates) { + assert(!candidateStates.empty()); + return true; + } + } + return false; + } + + template std::vector getDistances(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, boost::optional const& subsystem) { std::vector distances(transitionMatrix.getRowGroupCount()); @@ -570,7 +670,7 @@ namespace storm { } template - storm::storage::BitVector performProbGreater0A(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound, uint_fast64_t maximalSteps) { + storm::storage::BitVector performProbGreater0A(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound, uint_fast64_t maximalSteps, boost::optional const& choiceConstraint) { size_t numberOfStates = phiStates.size(); // Prepare resulting bit vector. @@ -613,40 +713,66 @@ namespace storm { if (!statesWithProbabilityGreater0.get(predecessorEntryIt->getColumn())) { // Check whether the predecessor has at least one successor in the current state set for every - // nondeterministic choice. - bool addToStatesWithProbabilityGreater0 = true; - for (uint_fast64_t row = nondeterministicChoiceIndices[predecessorEntryIt->getColumn()]; row < nondeterministicChoiceIndices[predecessorEntryIt->getColumn() + 1]; ++row) { - bool hasAtLeastOneSuccessorWithProbabilityGreater0 = false; - for (typename storm::storage::SparseMatrix::const_iterator successorEntryIt = transitionMatrix.begin(row), successorEntryIte = transitionMatrix.end(row); successorEntryIt != successorEntryIte; ++successorEntryIt) { - if (statesWithProbabilityGreater0.get(successorEntryIt->getColumn())) { - hasAtLeastOneSuccessorWithProbabilityGreater0 = true; - break; + // nondeterministic choice within the possibly given choiceConstraint. + + // Note: The backwards edge might be induced by a choice that violates the choiceConstraint. + // However this is not problematic as long as there is at least one enabled choice for the predecessor. + uint_fast64_t row = nondeterministicChoiceIndices[predecessorEntryIt->getColumn()]; + uint_fast64_t const& endOfGroup = nondeterministicChoiceIndices[predecessorEntryIt->getColumn() + 1]; + if (!choiceConstraint || choiceConstraint->getNextSetIndex(row) < endOfGroup) { + bool addToStatesWithProbabilityGreater0 = true; + for (; row < endOfGroup; ++row) { + if (!choiceConstraint || choiceConstraint->get(row)) { + bool hasAtLeastOneSuccessorWithProbabilityGreater0 = false; + for (typename storm::storage::SparseMatrix::const_iterator successorEntryIt = transitionMatrix.begin(row), successorEntryIte = transitionMatrix.end(row); successorEntryIt != successorEntryIte; ++successorEntryIt) { + if (statesWithProbabilityGreater0.get(successorEntryIt->getColumn())) { + hasAtLeastOneSuccessorWithProbabilityGreater0 = true; + break; + } + } + + if (!hasAtLeastOneSuccessorWithProbabilityGreater0) { + addToStatesWithProbabilityGreater0 = false; + break; + } } } - if (!hasAtLeastOneSuccessorWithProbabilityGreater0) { - addToStatesWithProbabilityGreater0 = false; - break; + // If we need to add the state, then actually add it and perform further search from the state. + if (addToStatesWithProbabilityGreater0) { + // If we don't have a bound on the number of steps to take, just add the state to the stack. + if (useStepBound) { + // If there is at least one more step to go, we need to push the state and the new number of steps. + remainingSteps[predecessorEntryIt->getColumn()] = currentStepBound - 1; + stepStack.push_back(currentStepBound - 1); + } + statesWithProbabilityGreater0.set(predecessorEntryIt->getColumn(), true); + stack.push_back(predecessorEntryIt->getColumn()); } } - // If we need to add the state, then actually add it and perform further search from the state. - if (addToStatesWithProbabilityGreater0) { - // If we don't have a bound on the number of steps to take, just add the state to the stack. - if (useStepBound) { - // If there is at least one more step to go, we need to push the state and the new number of steps. - remainingSteps[predecessorEntryIt->getColumn()] = currentStepBound - 1; - stepStack.push_back(currentStepBound - 1); + } else if (useStepBound && remainingSteps[predecessorEntryIt->getColumn()] < currentStepBound - 1) { + // We have found a shorter path to the predecessor. Hence, we need to explore it again. + // If there is a choiceConstraint, we still need to check whether the backwards edge was induced by a valid action + bool predecessorIsValid = true; + if (choiceConstraint) { + predecessorIsValid = false; + uint_fast64_t row = choiceConstraint->getNextSetIndex(nondeterministicChoiceIndices[predecessorEntryIt->getColumn()]); + uint_fast64_t const& endOfGroup = nondeterministicChoiceIndices[predecessorEntryIt->getColumn() + 1]; + for (; row < endOfGroup && !predecessorIsValid; row = choiceConstraint->getNextSetIndex(row + 1)) { + for (auto const& entry : transitionMatrix.getRow(row)) { + if (entry.getColumn() == currentState) { + predecessorIsValid = true; + break; + } + } } - statesWithProbabilityGreater0.set(predecessorEntryIt->getColumn(), true); + } + if (predecessorIsValid) { + remainingSteps[predecessorEntryIt->getColumn()] = currentStepBound - 1; + stepStack.push_back(currentStepBound - 1); stack.push_back(predecessorEntryIt->getColumn()); } - - } else if (useStepBound && remainingSteps[predecessorEntryIt->getColumn()] < currentStepBound - 1) { - // We have found a shorter path to the predecessor. Hence, we need to explore it again - remainingSteps[predecessorEntryIt->getColumn()] = currentStepBound - 1; - stepStack.push_back(currentStepBound - 1); - stack.push_back(predecessorEntryIt->getColumn()); } } } @@ -1162,6 +1288,8 @@ namespace storm { template storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, bool useStepBound, uint_fast64_t maximalSteps); template storm::storage::BitVector getBsccCover(storm::storage::SparseMatrix const& transitionMatrix); + + template bool checkIfECWithChoiceExists(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& choices); template std::vector getDistances(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, boost::optional const& subsystem); @@ -1201,7 +1329,7 @@ namespace storm { template std::pair performProb01Max(storm::models::sparse::NondeterministicModel> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; - template storm::storage::BitVector performProbGreater0A(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0); + template storm::storage::BitVector performProbGreater0A(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0, boost::optional const& choiceConstraint = boost::none); template storm::storage::BitVector performProb0E(storm::models::sparse::NondeterministicModel> const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); @@ -1231,7 +1359,9 @@ namespace storm { template storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, bool useStepBound, uint_fast64_t maximalSteps); template storm::storage::BitVector getBsccCover(storm::storage::SparseMatrix const& transitionMatrix); - + + template bool checkIfECWithChoiceExists(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& choices); + template std::vector getDistances(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, boost::optional const& subsystem); template storm::storage::BitVector performProbGreater0(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0); @@ -1262,7 +1392,7 @@ namespace storm { template std::pair performProb01Max(storm::models::sparse::NondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; - template storm::storage::BitVector performProbGreater0A(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0); + template storm::storage::BitVector performProbGreater0A(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0, boost::optional const& choiceConstraint = boost::none); template storm::storage::BitVector performProb0E(storm::models::sparse::NondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); @@ -1281,6 +1411,8 @@ namespace storm { template storm::storage::BitVector getBsccCover(storm::storage::SparseMatrix const& transitionMatrix); + template bool checkIfECWithChoiceExists(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& choices); + template std::vector getDistances(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, boost::optional const& subsystem); @@ -1309,11 +1441,9 @@ namespace storm { template std::pair performProb01Max(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; - template std::pair performProb01Max(storm::models::sparse::NondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; - template storm::storage::BitVector performProbGreater0A(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0); - + template storm::storage::BitVector performProbGreater0A(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0, boost::optional const& choiceConstraint = boost::none); template storm::storage::BitVector performProb0E(storm::models::sparse::NondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); template storm::storage::BitVector performProb0E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; @@ -1323,7 +1453,6 @@ namespace storm { template std::pair performProb01Min(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; - template std::pair performProb01Min(storm::models::sparse::NondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); diff --git a/src/storm/utility/graph.h b/src/storm/utility/graph.h index 7f51b20f6..9d6911479 100644 --- a/src/storm/utility/graph.h +++ b/src/storm/utility/graph.h @@ -74,7 +74,20 @@ namespace storm { */ template storm::storage::BitVector getBsccCover(storm::storage::SparseMatrix const& transitionMatrix); - + + /*! + * Checks whether there is an End Component that + * 1. contains at least one of the specified choices and + * 2. only contains states given by the specified subsystem. + * + * @param transitionMatrix the transition matrix + * @param backwardTransitions The reversed transition relation of the graph structure to search + * @param subsystem the subsystem which we consider + * @param choices the choices which are to be checked + */ + template + bool checkIfECWithChoiceExists(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& choices); + /*! * Performs a breadth-first search through the underlying graph structure to compute the distance from all * states to the starting states of the search. @@ -365,7 +378,7 @@ namespace storm { * @return A bit vector that represents all states with probability 0. */ template - storm::storage::BitVector performProbGreater0A(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0); + storm::storage::BitVector performProbGreater0A(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0, boost::optional const& choiceConstraint = boost::none); /*! * Computes the sets of states that have probability 0 of satisfying phi until psi under at least diff --git a/src/storm/utility/storm.h b/src/storm/utility/storm.h index 57a50bf92..6dd2b758c 100644 --- a/src/storm/utility/storm.h +++ b/src/storm/utility/storm.h @@ -113,16 +113,27 @@ namespace storm { class FormulaParser; } + template - std::shared_ptr> buildExplicitModel(std::string const& transitionsFile, std::string const& labelingFile, boost::optional const& stateRewardsFile = boost::none, boost::optional const& transitionRewardsFile = boost::none, boost::optional const& choiceLabelingFile = boost::none) { - return storm::parser::AutoParser<>::parseModel(transitionsFile, labelingFile, stateRewardsFile ? stateRewardsFile.get() : "", transitionRewardsFile ? transitionRewardsFile.get() : "", choiceLabelingFile ? choiceLabelingFile.get() : "" ); + inline std::shared_ptr> buildExplicitModel(std::string const&, std::string const&, boost::optional const& = boost::none, boost::optional const& = boost::none, boost::optional const& = boost::none) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Exact or parametric models with explicit input are not supported."); } + template<> + inline std::shared_ptr> buildExplicitModel(std::string const& transitionsFile, std::string const& labelingFile, boost::optional const& stateRewardsFile, boost::optional const& transitionRewardsFile, boost::optional const& choiceLabelingFile) { + return storm::parser::AutoParser::parseModel(transitionsFile, labelingFile, stateRewardsFile ? stateRewardsFile.get() : "", transitionRewardsFile ? transitionRewardsFile.get() : "", choiceLabelingFile ? choiceLabelingFile.get() : "" ); + } + template - std::shared_ptr> buildExplicitDRNModel(std::string const& drnFile) { + inline std::shared_ptr> buildExplicitDRNModel(std::string const& drnFile) { return storm::parser::DirectEncodingParser::parseModel(drnFile); } + template<> + inline std::shared_ptr> buildExplicitDRNModel(std::string const&) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Exact models with direct encoding are not supported."); + } + std::vector> extractFormulasFromProperties(std::vector const& properties); std::pair> parseJaniModel(std::string const& path); storm::prism::Program parseProgram(std::string const& path); diff --git a/src/test/modelchecker/SparseMaCbMultiObjectiveModelCheckerTest.cpp b/src/test/modelchecker/SparseMaCbMultiObjectiveModelCheckerTest.cpp new file mode 100644 index 000000000..69872ed95 --- /dev/null +++ b/src/test/modelchecker/SparseMaCbMultiObjectiveModelCheckerTest.cpp @@ -0,0 +1,35 @@ +#include "gtest/gtest.h" +#include "storm-config.h" + +#include "storm/modelchecker/multiobjective/multiObjectiveModelChecking.h" +#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" +#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" +#include "storm/models/sparse/MarkovAutomaton.h" +#include "storm/settings/modules/GeneralSettings.h" +#include "storm/settings/modules/MultiObjectiveSettings.h" +#include "storm/settings/SettingsManager.h" +#include "storm/utility/storm.h" + + +TEST(SparseMaCbMultiObjectiveModelCheckerTest, server) { + + std::string programFile = STORM_TEST_RESOURCES_DIR "/ma/server.ma"; + std::string formulasAsString = "multi(T>=5/3 [ F \"error\" ], P>=7/12 [ F \"processB\" ]) "; // true + formulasAsString += "; multi(T>=16/9 [ F \"error\" ], P>=7/12 [ F \"processB\" ]) "; // false + + storm::prism::Program program = storm::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, ""); + std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulasAsString, program)); + std::shared_ptr> ma = storm::buildSparseModel(program, formulas)->as>(); + uint_fast64_t const initState = *ma->getInitialStates().begin(); + + std::unique_ptr result; + + result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*ma, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::ConstraintBased); + ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); + EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]); + + result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*ma, formulas[1]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::ConstraintBased); + ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); + EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]); +} \ No newline at end of file diff --git a/src/test/modelchecker/SparseMaPcaaModelCheckerTest.cpp b/src/test/modelchecker/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp similarity index 87% rename from src/test/modelchecker/SparseMaPcaaModelCheckerTest.cpp rename to src/test/modelchecker/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp index e1390e171..51c3abd19 100644 --- a/src/test/modelchecker/SparseMaPcaaModelCheckerTest.cpp +++ b/src/test/modelchecker/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp @@ -3,7 +3,7 @@ #if defined STORM_HAVE_HYPRO || defined STORM_HAVE_Z3_OPTIMIZE -#include "storm/modelchecker/multiobjective/pcaa.h" +#include "storm/modelchecker/multiobjective/multiObjectiveModelChecking.h" #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "storm/modelchecker/results/ExplicitParetoCurveCheckResult.h" @@ -17,7 +17,7 @@ /* Rationals for MAs not supported at this point -TEST(SparseMaPcaaModelCheckerTest, serverRationalNumbers) { +TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, serverRationalNumbers) { std::string programFile = STORM_TEST_RESOURCES_DIR "/ma/server.ma"; std::string formulasAsString = "multi(Tmax=? [ F \"error\" ], Pmax=? [ F \"processB\" ]) "; // pareto @@ -48,7 +48,7 @@ TEST(SparseMaPcaaModelCheckerTest, serverRationalNumbers) { }*/ -TEST(SparseMaPcaaModelCheckerTest, server) { +TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, server) { std::string programFile = STORM_TEST_RESOURCES_DIR "/ma/server.ma"; std::string formulasAsString = "multi(Tmax=? [ F \"error\" ], Pmax=? [ F \"processB\" ]) "; // pareto @@ -58,7 +58,7 @@ TEST(SparseMaPcaaModelCheckerTest, server) { std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulasAsString, program)); std::shared_ptr> ma = storm::buildSparseModel(program, formulas).getModel()->as>(); - std::unique_ptr result = storm::modelchecker::multiobjective::performPcaa(*ma, formulas[0]->asMultiObjectiveFormula()); + std::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*ma, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa); ASSERT_TRUE(result->isExplicitParetoCurveCheckResult()); // we do our checks with rationals to avoid numerical issues when doing polytope computations... @@ -77,7 +77,7 @@ TEST(SparseMaPcaaModelCheckerTest, server) { } -TEST(SparseMaPcaaModelCheckerTest, jobscheduler_pareto_3Obj) { +TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, jobscheduler_pareto_3Obj) { std::string programFile = STORM_TEST_RESOURCES_DIR "/ma/jobscheduler.ma"; std::string formulasAsString = "multi(Tmin=? [ F \"all_jobs_finished\" ], Pmax=? [ F<=0.2 \"half_of_jobs_finished\" ], Pmin=? [ F \"slowest_before_fastest\" ]) "; @@ -87,7 +87,7 @@ TEST(SparseMaPcaaModelCheckerTest, jobscheduler_pareto_3Obj) { std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulasAsString, program)); std::shared_ptr> ma = storm::buildSparseModel(program, formulas).getModel()->as>(); - std::unique_ptr result = storm::modelchecker::multiobjective::performPcaa(*ma, formulas[0]->asMultiObjectiveFormula()); + std::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*ma, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa); ASSERT_TRUE(result->isExplicitParetoCurveCheckResult()); std::vector j12 = {1.266666667,0.1617571721,0.5}; @@ -107,7 +107,7 @@ TEST(SparseMaPcaaModelCheckerTest, jobscheduler_pareto_3Obj) { EXPECT_TRUE(result->asExplicitParetoCurveCheckResult().getOverApproximation()->convertNumberRepresentation()->minkowskiSum(bloatingBox)->contains(expectedAchievableValues)); } -TEST(SparseMaPcaaModelCheckerTest, jobscheduler_achievability_3Obj) { +TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, jobscheduler_achievability_3Obj) { std::string programFile = STORM_TEST_RESOURCES_DIR "/ma/jobscheduler.ma"; std::string formulasAsString = "multi(T<=1.31 [ F \"all_jobs_finished\" ], P>=0.17 [ F<=0.2 \"half_of_jobs_finished\" ], P<=0.31 [ F \"slowest_before_fastest\" ]) "; //true @@ -119,16 +119,16 @@ TEST(SparseMaPcaaModelCheckerTest, jobscheduler_achievability_3Obj) { std::shared_ptr> ma = storm::buildSparseModel(program, formulas).getModel()->as>(); uint_fast64_t const initState = *ma->getInitialStates().begin(); - std::unique_ptr result = storm::modelchecker::multiobjective::performPcaa(*ma, formulas[0]->asMultiObjectiveFormula()); + std::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*ma, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa); ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]); - std::unique_ptr result2 = storm::modelchecker::multiobjective::performPcaa(*ma, formulas[1]->asMultiObjectiveFormula()); + std::unique_ptr result2 = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*ma, formulas[1]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa); ASSERT_TRUE(result2->isExplicitQualitativeCheckResult()); EXPECT_FALSE(result2->asExplicitQualitativeCheckResult()[initState]); } -TEST(SparseMaPcaaModelCheckerTest, jobscheduler_quantitative_3Obj) { +TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, jobscheduler_quantitative_3Obj) { std::string programFile = STORM_TEST_RESOURCES_DIR "/ma/jobscheduler.ma"; std::string formulasAsString = "multi(Tmin=? [ F \"all_jobs_finished\" ], P>=0.1797900683 [ F<=0.2 \"half_of_jobs_finished\" ], P<=0.3 [ F \"slowest_before_fastest\" ]) "; //quantitative @@ -141,16 +141,16 @@ TEST(SparseMaPcaaModelCheckerTest, jobscheduler_quantitative_3Obj) { uint_fast64_t const initState = *ma->getInitialStates().begin(); - std::unique_ptr result = storm::modelchecker::multiobjective::performPcaa(*ma, formulas[0]->asMultiObjectiveFormula()); + std::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*ma, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa); ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); EXPECT_NEAR(1.3, result->asExplicitQuantitativeCheckResult()[initState], storm::settings::getModule().getPrecision()); - std::unique_ptr result2 = storm::modelchecker::multiobjective::performPcaa(*ma, formulas[1]->asMultiObjectiveFormula()); + std::unique_ptr result2 = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*ma, formulas[1]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa); ASSERT_TRUE(result2->isExplicitQualitativeCheckResult()); EXPECT_FALSE(result2->asExplicitQualitativeCheckResult()[initState]); } -TEST(SparseMaPcaaModelCheckerTest, jobscheduler_pareto_2Obj) { +TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, jobscheduler_pareto_2Obj) { std::string programFile = STORM_TEST_RESOURCES_DIR "/ma/jobscheduler.ma"; std::string formulasAsString = "multi( Pmax=? [ F<=0.1 \"one_job_finished\"], Pmin=? [F<=0.2 \"all_jobs_finished\"]) "; @@ -160,7 +160,7 @@ TEST(SparseMaPcaaModelCheckerTest, jobscheduler_pareto_2Obj) { std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulasAsString, program)); std::shared_ptr> ma = storm::buildSparseModel(program, formulas).getModel()->as>(); - std::unique_ptr result = storm::modelchecker::multiobjective::performPcaa(*ma, formulas[0]->asMultiObjectiveFormula()); + std::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*ma, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa); ASSERT_TRUE(result->isExplicitParetoCurveCheckResult()); std::vector j12 = {0.2591835573, 0.01990529674}; diff --git a/src/test/modelchecker/SparseMdpCbMultiObjectiveModelCheckerTest.cpp b/src/test/modelchecker/SparseMdpCbMultiObjectiveModelCheckerTest.cpp new file mode 100644 index 000000000..9f3525948 --- /dev/null +++ b/src/test/modelchecker/SparseMdpCbMultiObjectiveModelCheckerTest.cpp @@ -0,0 +1,74 @@ +#include "gtest/gtest.h" +#include "storm-config.h" + +#include "storm/modelchecker/multiobjective/multiObjectiveModelChecking.h" +#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" +#include "storm/models/sparse/Mdp.h" +#include "storm/settings/modules/GeneralSettings.h" +#include "storm/settings/SettingsManager.h" +#include "storm/utility/storm.h" + + +TEST(SparseMdpCbMultiObjectiveModelCheckerTest, consensus) { + + std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/multiobj_consensus2_3_2.nm"; + std::string formulasAsString = "multi(Pmax=? [ F \"one_proc_err\" ], P>=0.8916673903 [ G \"one_coin_ok\" ]) "; // numerical + formulasAsString += "; \n multi(P>=0.1 [ F \"one_proc_err\" ], P>=0.8916673903 [ G \"one_coin_ok\" ])"; // achievability (true) + formulasAsString += "; \n multi(P>=0.11 [ F \"one_proc_err\" ], P>=0.8916673903 [ G \"one_coin_ok\" ])"; // achievability (false) + + // programm, model, formula + storm::prism::Program program = storm::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, ""); + std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulasAsString, program)); + std::shared_ptr> mdp = storm::buildSparseModel(program, formulas)->as>(); + uint_fast64_t const initState = *mdp->getInitialStates().begin();; + + std::unique_ptr result; + + result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[1]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::ConstraintBased); + ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); + EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]); + + result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[2]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::ConstraintBased); + ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); + EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]); + +} + + +TEST(SparseMdpCbMultiObjectiveModelCheckerTest, zeroconf) { + + std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/multiobj_zeroconf4.nm"; + std::string formulasAsString = "multi(P>=0.0003 [ F l=4 & ip=1 ] , P>=0.993141[ G (error=0) ]) "; // numerical + + // programm, model, formula + storm::prism::Program program = storm::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, ""); + std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulasAsString, program)); + std::shared_ptr> mdp = storm::buildSparseModel(program, formulas)->as>(); + uint_fast64_t const initState = *mdp->getInitialStates().begin(); + + std::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::ConstraintBased); + ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); + EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]); +} + +/* This test takes a little bit too long ... +TEST(SparseMdpCbMultiObjectiveModelCheckerTest, team3with3objectives) { + + std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/multiobj_team3.nm"; + std::string formulasAsString = "multi(P>=0.75 [ F \"task1_compl\" ], R{\"w_1_total\"}>=2.210204082 [ C ], P>=0.5 [ F \"task2_compl\" ])"; // numerical + + // programm, model, formula + storm::prism::Program program = storm::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, ""); + std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulasAsString, program)); + std::shared_ptr> mdp = storm::buildSparseModel(program, formulas)->as>(); + uint_fast64_t const initState = *mdp->getInitialStates().begin(); + + std::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::ConstraintBased); + ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); + EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]); +} +*/ + diff --git a/src/test/modelchecker/SparseMdpPcaaModelCheckerTest.cpp b/src/test/modelchecker/SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp similarity index 78% rename from src/test/modelchecker/SparseMdpPcaaModelCheckerTest.cpp rename to src/test/modelchecker/SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp index 8fc87d315..996220281 100644 --- a/src/test/modelchecker/SparseMdpPcaaModelCheckerTest.cpp +++ b/src/test/modelchecker/SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp @@ -3,7 +3,7 @@ #if defined STORM_HAVE_HYPRO || defined STORM_HAVE_Z3_OPTIMIZE -#include "storm/modelchecker/multiobjective/pcaa.h" +#include "storm/modelchecker/multiobjective/multiObjectiveModelChecking.h" #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "storm/models/sparse/Mdp.h" @@ -12,7 +12,7 @@ #include "storm/utility/storm.h" -TEST(SparseMdpPcaaModelCheckerTest, consensus) { +TEST(SparseMdpPcaaMultiObjectiveModelCheckerTest, consensus) { std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/multiobj_consensus2_3_2.nm"; std::string formulasAsString = "multi(Pmax=? [ F \"one_proc_err\" ], P>=0.8916673903 [ G \"one_coin_ok\" ]) "; // numerical @@ -26,21 +26,21 @@ TEST(SparseMdpPcaaModelCheckerTest, consensus) { std::shared_ptr> mdp = storm::buildSparseModel(program, formulas).getModel()->as>(); uint_fast64_t const initState = *mdp->getInitialStates().begin();; - std::unique_ptr result = storm::modelchecker::multiobjective::performPcaa(*mdp, formulas[0]->asMultiObjectiveFormula()); + std::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa); ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); EXPECT_NEAR(0.10833260970000025, result->asExplicitQuantitativeCheckResult()[initState], storm::settings::getModule().getPrecision()); - result = storm::modelchecker::multiobjective::performPcaa(*mdp, formulas[1]->asMultiObjectiveFormula()); + result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[1]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa); ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]); - result = storm::modelchecker::multiobjective::performPcaa(*mdp, formulas[2]->asMultiObjectiveFormula()); + result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[2]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa); ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]); } -TEST(SparseMdpPcaaModelCheckerTest, zeroconf) { +TEST(SparseMdpPcaaMultiObjectiveModelCheckerTest, zeroconf) { std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/multiobj_zeroconf4.nm"; std::string formulasAsString = "multi(Pmax=? [ F l=4 & ip=1 ] , P>=0.993141[ G (error=0) ]) "; // numerical @@ -52,12 +52,12 @@ TEST(SparseMdpPcaaModelCheckerTest, zeroconf) { std::shared_ptr> mdp = storm::buildSparseModel(program, formulas).getModel()->as>(); uint_fast64_t const initState = *mdp->getInitialStates().begin(); - std::unique_ptr result = storm::modelchecker::multiobjective::performPcaa(*mdp, formulas[0]->asMultiObjectiveFormula()); + std::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa); ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); EXPECT_NEAR(0.0003075787401574803, result->asExplicitQuantitativeCheckResult()[initState], storm::settings::getModule().getPrecision()); } -TEST(SparseMdpPcaaModelCheckerTest, team3with3objectives) { +TEST(SparseMdpPcaaMultiObjectiveModelCheckerTest, team3with3objectives) { std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/multiobj_team3.nm"; std::string formulasAsString = "multi(Pmax=? [ F \"task1_compl\" ], R{\"w_1_total\"}>=2.210204082 [ C ], P>=0.5 [ F \"task2_compl\" ])"; // numerical @@ -69,12 +69,12 @@ TEST(SparseMdpPcaaModelCheckerTest, team3with3objectives) { std::shared_ptr> mdp = storm::buildSparseModel(program, formulas).getModel()->as>(); uint_fast64_t const initState = *mdp->getInitialStates().begin(); - std::unique_ptr result = storm::modelchecker::multiobjective::performPcaa(*mdp, formulas[0]->asMultiObjectiveFormula()); + std::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa); ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); EXPECT_NEAR(0.7448979591841851, result->asExplicitQuantitativeCheckResult()[initState], storm::settings::getModule().getPrecision()); } -TEST(SparseMdpPcaaModelCheckerTest, scheduler) { +TEST(SparseMdpPcaaMultiObjectiveModelCheckerTest, scheduler) { std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/multiobj_scheduler05.nm"; std::string formulasAsString = "multi(R{\"time\"}<= 11.778[ F \"tasks_complete\" ], R{\"energy\"}<=1.45 [ F \"tasks_complete\" ]) "; @@ -86,11 +86,11 @@ TEST(SparseMdpPcaaModelCheckerTest, scheduler) { std::shared_ptr> mdp = storm::buildSparseModel(program, formulas).getModel()->as>(); uint_fast64_t const initState = *mdp->getInitialStates().begin(); - std::unique_ptr result = storm::modelchecker::multiobjective::performPcaa(*mdp, formulas[0]->asMultiObjectiveFormula()); + std::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa); EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]); } -TEST(SparseMdpPcaaModelCheckerTest, dpm) { +TEST(SparseMdpPcaaMultiObjectiveModelCheckerTest, dpm) { std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/multiobj_dpm100.nm"; std::string formulasAsString = "multi(R{\"power\"}min=? [ C<=100 ], R{\"queue\"}<=70 [ C<=100 ])"; // numerical @@ -102,7 +102,7 @@ TEST(SparseMdpPcaaModelCheckerTest, dpm) { std::shared_ptr> mdp = storm::buildSparseModel(program, formulas).getModel()->as>(); uint_fast64_t const initState = *mdp->getInitialStates().begin(); - std::unique_ptr result = storm::modelchecker::multiobjective::performPcaa(*mdp, formulas[0]->asMultiObjectiveFormula()); + std::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa); ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); EXPECT_NEAR(121.6128842, result->asExplicitQuantitativeCheckResult()[initState], storm::settings::getModule().getPrecision()); }