diff --git a/src/storm/api/builder.h b/src/storm/api/builder.h index dab7ac5d5..b2ecc2626 100644 --- a/src/storm/api/builder.h +++ b/src/storm/api/builder.h @@ -61,7 +61,7 @@ namespace storm { } template - std::shared_ptr> buildSparseModel(storm::storage::SymbolicModelDescription const& model, std::vector> const& formulas, bool buildChoiceLabels = false, bool buildChoiceOrigins = false) { + std::shared_ptr> buildSparseModel(storm::storage::SymbolicModelDescription const& model, std::vector> const& formulas, bool buildChoiceLabels = false, bool buildChoiceOrigins = false, bool buildStateValuations = false) { storm::builder::BuilderOptions options(formulas); if (storm::settings::getModule().isBuildFullModelSet()) { @@ -69,8 +69,9 @@ namespace storm { options.setBuildAllRewardModels(); options.clearTerminalStates(); } - options.setBuildChoiceOrigins(buildChoiceOrigins); options.setBuildChoiceLabels(buildChoiceLabels); + options.setBuildChoiceOrigins(buildChoiceOrigins); + options.setBuildStateValuations(buildStateValuations); if (storm::settings::getModule().isJitSet()) { STORM_LOG_THROW(model.isJaniModel(), storm::exceptions::NotSupportedException, "Cannot use JIT-based model builder for non-JANI model."); diff --git a/src/storm/cli/cli.cpp b/src/storm/cli/cli.cpp index c1f2cf960..0f53aa2d3 100644 --- a/src/storm/cli/cli.cpp +++ b/src/storm/cli/cli.cpp @@ -808,10 +808,12 @@ namespace storm { uint64_t maximumResidentSizeInMegabytes = ru.ru_maxrss / 1024; #endif std::cout << " * peak memory usage: " << maximumResidentSizeInMegabytes << "MB" << std::endl; - std::cout << " * CPU time: " << ru.ru_utime.tv_sec << "." << std::setw(3) << std::setfill('0') << ru.ru_utime.tv_usec/1000 << "s" << std::endl; + char oldFillChar = std::cout.fill('0'); + std::cout << " * CPU time: " << ru.ru_utime.tv_sec << "." << std::setw(3) << ru.ru_utime.tv_usec/1000 << "s" << std::endl; if (wallclockMilliseconds != 0) { - std::cout << " * wallclock time: " << (wallclockMilliseconds/1000) << "." << std::setw(3) << std::setfill('0') << (wallclockMilliseconds % 1000) << "s" << std::endl; + std::cout << " * wallclock time: " << (wallclockMilliseconds/1000) << "." << std::setw(3) << (wallclockMilliseconds % 1000) << "s" << std::endl; } + std::cout.fill(oldFillChar); } } diff --git a/src/storm/modelchecker/hints/ExplicitModelCheckerHint.cpp b/src/storm/modelchecker/hints/ExplicitModelCheckerHint.cpp index b68ab9508..14ebc0f07 100644 --- a/src/storm/modelchecker/hints/ExplicitModelCheckerHint.cpp +++ b/src/storm/modelchecker/hints/ExplicitModelCheckerHint.cpp @@ -85,22 +85,22 @@ namespace storm { } template - storm::storage::TotalScheduler const& ExplicitModelCheckerHint::getSchedulerHint() const { + storm::storage::Scheduler const& ExplicitModelCheckerHint::getSchedulerHint() const { return *schedulerHint; } template - storm::storage::TotalScheduler& ExplicitModelCheckerHint::getSchedulerHint() { + storm::storage::Scheduler& ExplicitModelCheckerHint::getSchedulerHint() { return *schedulerHint; } template - void ExplicitModelCheckerHint::setSchedulerHint(boost::optional const& schedulerHint) { + void ExplicitModelCheckerHint::setSchedulerHint(boost::optional> const& schedulerHint) { this->schedulerHint = schedulerHint; } template - void ExplicitModelCheckerHint::setSchedulerHint(boost::optional&& schedulerHint) { + void ExplicitModelCheckerHint::setSchedulerHint(boost::optional>&& schedulerHint) { this->schedulerHint = schedulerHint; } diff --git a/src/storm/modelchecker/hints/ExplicitModelCheckerHint.h b/src/storm/modelchecker/hints/ExplicitModelCheckerHint.h index 33acd89ce..797ec2826 100644 --- a/src/storm/modelchecker/hints/ExplicitModelCheckerHint.h +++ b/src/storm/modelchecker/hints/ExplicitModelCheckerHint.h @@ -5,7 +5,7 @@ #include #include "storm/modelchecker/hints/ModelCheckerHint.h" -#include "storm/storage/TotalScheduler.h" +#include "storm/storage/Scheduler.h" namespace storm { namespace modelchecker { @@ -46,10 +46,10 @@ namespace storm { void setMaybeStates(storm::storage::BitVector&& maybeStates); bool hasSchedulerHint() const; - storm::storage::TotalScheduler const& getSchedulerHint() const; - storm::storage::TotalScheduler& getSchedulerHint(); - void setSchedulerHint(boost::optional const& schedulerHint); - void setSchedulerHint(boost::optional&& schedulerHint); + storm::storage::Scheduler const& getSchedulerHint() const; + storm::storage::Scheduler& getSchedulerHint(); + void setSchedulerHint(boost::optional> const& schedulerHint); + void setSchedulerHint(boost::optional>&& schedulerHint); // If set, it is assumed that there are no end components that consist only of maybestates. // May only be enabled iff maybestates are given. @@ -58,7 +58,7 @@ namespace storm { private: boost::optional> resultHint; - boost::optional schedulerHint; + boost::optional> schedulerHint; bool computeOnlyMaybeStates; boost::optional maybeStates; diff --git a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp index 252af5a7a..b2da20897 100644 --- a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp +++ b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp @@ -69,8 +69,8 @@ namespace storm { template SparseMultiObjectivePreprocessor::PreprocessorData::PreprocessorData(SparseModelType const& model) : originalModel(model) { - storm::storage::MemoryStructureBuilder memoryBuilder(1); - memoryBuilder.setTransition(0,0, storm::logic::Formula::getTrueFormula()); + storm::storage::MemoryStructureBuilder memoryBuilder(1, model); + memoryBuilder.setTransition(0,0, storm::storage::BitVector(model.getNumberOfStates(), true)); 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 @@ -232,24 +232,28 @@ namespace storm { template void SparseMultiObjectivePreprocessor::preprocessUntilFormula(storm::logic::UntilFormula const& formula, PreprocessorData& data) { + storm::modelchecker::SparsePropositionalModelChecker mc(data.originalModel); + storm::storage::BitVector rightSubformulaResult = mc.check(formula.getRightSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); + storm::storage::BitVector leftSubformulaResult = mc.check(formula.getLeftSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); // 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()) { + if (!(data.originalModel.getInitialStates() & rightSubformulaResult).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); + storm::storage::MemoryStructureBuilder builder(2, data.originalModel); 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::BitVector nonRelevantStates = ~leftSubformulaResult | rightSubformulaResult; + builder.setTransition(0, 0, ~nonRelevantStates); + builder.setTransition(0, 1, nonRelevantStates); + builder.setTransition(1, 1, storm::storage::BitVector(data.originalModel.getNumberOfStates(), true)); + for (auto const& initState : data.originalModel.getInitialStates()) { + builder.setInitialMemoryState(initState, nonRelevantStates.get(initState) ? 1 : 0); + } storm::storage::MemoryStructure objectiveMemory = builder.build(); data.memory = std::make_shared(data.memory->product(objectiveMemory)); @@ -295,15 +299,22 @@ namespace storm { preprocessUntilFormula(storm::logic::UntilFormula(storm::logic::Formula::getTrueFormula(), formula.getSubformula().asSharedPointer()), data); return; } - + + // Analyze the subformula + storm::modelchecker::SparsePropositionalModelChecker mc(data.originalModel); + storm::storage::BitVector subFormulaResult = mc.check(formula.getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); + // Create a memory structure that stores whether a target state has already been reached - storm::storage::MemoryStructureBuilder builder(2); + storm::storage::MemoryStructureBuilder builder(2, data.originalModel); // 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)); + builder.setTransition(0, 0, ~subFormulaResult); + builder.setTransition(0, 1, subFormulaResult); + builder.setTransition(1, 1, storm::storage::BitVector(data.originalModel.getNumberOfStates(), true)); + for (auto const& initState : data.originalModel.getInitialStates()) { + builder.setInitialMemoryState(initState, subFormulaResult.get(initState) ? 1 : 0); + } storm::storage::MemoryStructure objectiveMemory = builder.build(); data.memory = std::make_shared(data.memory->product(objectiveMemory)); diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp index 9064acc97..d3c8e3026 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp @@ -340,18 +340,18 @@ namespace storm { void SparseMaPcaaWeightVectorChecker::performPSStep(SubModel& PS, SubModel const& MS, MinMaxSolverData& minMax, LinEqSolverData& linEq, std::vector& optimalChoicesAtCurrentEpoch, storm::storage::BitVector const& consideredObjectives, std::vector const& weightVector) const { // compute a choice vector for the probabilistic states that is optimal w.r.t. the weighted reward vector minMax.solver->solveEquations(PS.weightedSolutionVector, minMax.b); - auto newScheduler = minMax.solver->getScheduler(); + auto const& newChoices = minMax.solver->getSchedulerChoices(); 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 - optimalChoicesAtCurrentEpoch = newScheduler->getChoices(); + optimalChoicesAtCurrentEpoch = newChoices; 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) { - optimalChoicesAtCurrentEpoch = newScheduler->getChoices(); + if(linEq.solver == nullptr || newChoices != optimalChoicesAtCurrentEpoch) { + optimalChoicesAtCurrentEpoch = newChoices; linEq.solver = nullptr; storm::storage::SparseMatrix linEqMatrix = PS.toPS.selectRowsFromRowGroups(optimalChoicesAtCurrentEpoch, true); linEqMatrix.convertToEquationSystem(); diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp index 497bce790..be8727462 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp @@ -37,7 +37,8 @@ namespace storm { checkHasBeenCalled(false), objectiveResults(objectives.size()), offsetsToUnderApproximation(objectives.size()), - offsetsToOverApproximation(objectives.size()) { + offsetsToOverApproximation(objectives.size()), + optimalChoices(model.getNumberOfStates(), 0) { // set data for unbounded objectives for(uint_fast64_t objIndex = 0; objIndex < objectives.size(); ++objIndex) { @@ -86,6 +87,7 @@ namespace storm { } 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) { @@ -136,19 +138,27 @@ namespace storm { } template - storm::storage::TotalScheduler const& SparsePcaaWeightVectorChecker::getScheduler() const { + storm::storage::Scheduler::ValueType> SparsePcaaWeightVectorChecker::computeScheduler() const { STORM_LOG_THROW(this->checkHasBeenCalled, storm::exceptions::IllegalFunctionCallException, "Tried to retrieve results but check(..) has not been called before."); for(auto const& obj : this->objectives) { STORM_LOG_THROW(!obj.lowerTimeBound && !obj.upperTimeBound, storm::exceptions::NotImplementedException, "Scheduler retrival is not implemented for timeBounded objectives."); } - return scheduler; + + storm::storage::Scheduler result(this->optimalChoices.size()); + uint_fast64_t state = 0; + for (auto const& choice : optimalChoices) { + result.setChoice(choice, state); + ++state; + } + return result; } template void SparsePcaaWeightVectorChecker::unboundedWeightedPhase(std::vector const& weightedRewardVector, boost::optional const& lowerResultBound, boost::optional const& upperResultBound) { - if(this->objectivesWithNoUpperTimeBound.empty() || !storm::utility::vector::hasNonZeroEntry(weightedRewardVector)) { + + 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()); + this->optimalChoices = std::vector(model.getNumberOfStates(), 0); return; } @@ -183,16 +193,13 @@ namespace storm { solver->solveEquations(subResult, subRewardVector); this->weightedResult = std::vector(model.getNumberOfStates()); - std::vector optimalChoices(model.getNumberOfStates()); - - transformReducedSolutionToOriginalModel(ecEliminatorResult.matrix, subResult, solver->getScheduler()->getChoices(), ecEliminatorResult.newToOldRowMapping, ecEliminatorResult.oldToNewStateMapping, this->weightedResult, optimalChoices); - this->scheduler = storm::storage::TotalScheduler(std::move(optimalChoices)); + transformReducedSolutionToOriginalModel(ecEliminatorResult.matrix, subResult, solver->getSchedulerChoices(), ecEliminatorResult.newToOldRowMapping, ecEliminatorResult.oldToNewStateMapping, this->weightedResult, this->optimalChoices); } template void SparsePcaaWeightVectorChecker::unboundedIndividualPhase(std::vector const& weightVector) { - if (objectivesWithNoUpperTimeBound.getNumberOfSetBits() == 1 && storm::utility::isOne(weightVector[*objectivesWithNoUpperTimeBound.begin()])) { + 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)) { @@ -203,8 +210,8 @@ namespace storm { objectiveResults[objIndex2] = std::vector(model.getNumberOfStates(), storm::utility::zero()); } } - } else { - storm::storage::SparseMatrix deterministicMatrix = model.getTransitionMatrix().selectRowsFromRowGroups(this->scheduler.getChoices(), true); + } else { + storm::storage::SparseMatrix deterministicMatrix = model.getTransitionMatrix().selectRowsFromRowGroups(this->optimalChoices, true); storm::storage::SparseMatrix deterministicBackwardTransitions = deterministicMatrix.transpose(); std::vector deterministicStateRewards(deterministicMatrix.getRowCount()); storm::solver::GeneralLinearEquationSolverFactory linearEquationSolverFactory; @@ -219,7 +226,7 @@ namespace storm { if (objectivesWithNoUpperTimeBound.get(objIndex)) { offsetsToUnderApproximation[objIndex] = storm::utility::zero(); offsetsToOverApproximation[objIndex] = storm::utility::zero(); - storm::utility::vector::selectVectorValues(deterministicStateRewards, this->scheduler.getChoices(), model.getTransitionMatrix().getRowGroupIndices(), discreteActionRewards[objIndex]); + storm::utility::vector::selectVectorValues(deterministicStateRewards, this->optimalChoices, 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 storm::storage::BitVector maybeStates = storm::utility::graph::performProbGreater0(deterministicBackwardTransitions, storm::storage::BitVector(deterministicMatrix.getRowCount(), true), statesWithRewards); diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h index 691b69fad..3cf75c83b 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h @@ -4,7 +4,7 @@ #include "storm/storage/BitVector.h" #include "storm/storage/SparseMatrix.h" -#include "storm/storage/TotalScheduler.h" +#include "storm/storage/Scheduler.h" #include "storm/modelchecker/multiobjective/Objective.h" #include "storm/utility/vector.h" @@ -75,8 +75,9 @@ namespace storm { /*! * Retrieves a scheduler that induces the current values * Note that check(..) has to be called before retrieving the scheduler. Otherwise, an exception is thrown. + * Also note that (currently) the scheduler only supports unbounded objectives. */ - storm::storage::TotalScheduler const& getScheduler() const; + storm::storage::Scheduler computeScheduler() const; protected: @@ -147,8 +148,8 @@ namespace storm { // The distances are stored as a (possibly negative) offset that has to be added (+) to to the objectiveResults. std::vector offsetsToUnderApproximation; std::vector offsetsToOverApproximation; - // The scheduler that optimizes the weighted rewards - storm::storage::TotalScheduler scheduler; + // The scheduler choices that optimize the weighted rewards of undounded objectives. + std::vector optimalChoices; }; diff --git a/src/storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.cpp b/src/storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.cpp index b652f6e60..0a802b584 100644 --- a/src/storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.cpp +++ b/src/storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.cpp @@ -186,8 +186,8 @@ namespace storm { if (lowerResultBound) solver->setLowerBound(lowerResultBound.get()); if (upperResultBound) solver->setUpperBound(upperResultBound.get()); if (!stepBound) solver->setTrackScheduler(true); - if (storm::solver::minimize(dirForParameters) && minSched && !stepBound) solver->setSchedulerHint(std::move(minSched.get())); - if (storm::solver::maximize(dirForParameters) && maxSched && !stepBound) solver->setSchedulerHint(std::move(maxSched.get())); + if (storm::solver::minimize(dirForParameters) && minSchedChoices && !stepBound) solver->setSchedulerHint(std::move(minSchedChoices.get())); + if (storm::solver::maximize(dirForParameters) && maxSchedChoices && !stepBound) solver->setSchedulerHint(std::move(maxSchedChoices.get())); if (this->currentCheckTask->isBoundSet() && solver->hasSchedulerHint()) { // If we reach this point, we know that after applying the hint, the x-values can only become larger (if we maximize) or smaller (if we minimize). std::unique_ptr> termCond; @@ -211,9 +211,9 @@ namespace storm { x.resize(maybeStates.getNumberOfSetBits(), storm::utility::zero()); solver->solveEquations(dirForParameters, x, parameterLifter->getVector()); if(storm::solver::minimize(dirForParameters)) { - minSched = std::move(*solver->getScheduler()); + minSchedChoices = solver->getSchedulerChoices(); } else { - maxSched = std::move(*solver->getScheduler()); + maxSchedChoices = solver->getSchedulerChoices(); } } @@ -234,21 +234,43 @@ namespace storm { resultsForNonMaybeStates.clear(); stepBound = boost::none; parameterLifter = nullptr; - minSched = boost::none; - maxSched = boost::none; + minSchedChoices = boost::none; + maxSchedChoices = boost::none; x.clear(); lowerResultBound = boost::none; upperResultBound = boost::none; } template - boost::optional& SparseDtmcParameterLiftingModelChecker::getCurrentMinScheduler() { - return minSched; + boost::optional> SparseDtmcParameterLiftingModelChecker::getCurrentMinScheduler() { + if (!minSchedChoices) { + return boost::none; + } + + storm::storage::Scheduler result(minSchedChoices->size()); + uint_fast64_t state = 0; + for (auto const& schedulerChoice : minSchedChoices.get()) { + result.setChoice(schedulerChoice, state); + ++state; + } + + return result; } template - boost::optional& SparseDtmcParameterLiftingModelChecker::getCurrentMaxScheduler() { - return maxSched; + boost::optional> SparseDtmcParameterLiftingModelChecker::getCurrentMaxScheduler() { + if (!maxSchedChoices) { + return boost::none; + } + + storm::storage::Scheduler result(maxSchedChoices->size()); + uint_fast64_t state = 0; + for (auto const& schedulerChoice : maxSchedChoices.get()) { + result.setChoice(schedulerChoice, state); + ++state; + } + + return result; } template class SparseDtmcParameterLiftingModelChecker, double>; diff --git a/src/storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.h b/src/storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.h index 331219a39..73ee17fe7 100644 --- a/src/storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.h +++ b/src/storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.h @@ -6,7 +6,7 @@ #include "storm/modelchecker/parametric/SparseParameterLiftingModelChecker.h" #include "storm/storage/BitVector.h" -#include "storm/storage/TotalScheduler.h" +#include "storm/storage/Scheduler.h" #include "storm/solver/MinMaxLinearEquationSolver.h" #include "storm/transformer/ParameterLifter.h" #include "storm/logic/FragmentSpecification.h" @@ -24,8 +24,8 @@ namespace storm { virtual bool canHandle(CheckTask const& checkTask) const override; - boost::optional& getCurrentMinScheduler(); - boost::optional& getCurrentMaxScheduler(); + boost::optional> getCurrentMinScheduler(); + boost::optional> getCurrentMaxScheduler(); protected: @@ -47,7 +47,7 @@ namespace storm { std::unique_ptr> solverFactory; // Results from the most recent solver call. - boost::optional minSched, maxSched; + boost::optional> minSchedChoices, maxSchedChoices; std::vector x; boost::optional lowerResultBound, upperResultBound; }; diff --git a/src/storm/modelchecker/parametric/SparseDtmcRegionChecker.cpp b/src/storm/modelchecker/parametric/SparseDtmcRegionChecker.cpp index 97d9d1973..b280bc046 100644 --- a/src/storm/modelchecker/parametric/SparseDtmcRegionChecker.cpp +++ b/src/storm/modelchecker/parametric/SparseDtmcRegionChecker.cpp @@ -47,8 +47,12 @@ namespace storm { STORM_LOG_ASSERT(dtmcPLChecker, "Underlying Parameter lifting checker has unexpected type"); auto exactDtmcPLChecker = dynamic_cast*>(this->exactParameterLiftingChecker.get()); STORM_LOG_ASSERT(exactDtmcPLChecker, "Underlying exact parameter lifting checker has unexpected type"); - exactDtmcPLChecker->getCurrentMaxScheduler() = dtmcPLChecker->getCurrentMaxScheduler(); - exactDtmcPLChecker->getCurrentMinScheduler() = dtmcPLChecker->getCurrentMinScheduler(); + if (dtmcPLChecker->getCurrentMaxScheduler()) { + exactDtmcPLChecker->getCurrentMaxScheduler() = dtmcPLChecker->getCurrentMaxScheduler()->template toValueType(); + } + if (dtmcPLChecker->getCurrentMinScheduler()) { + exactDtmcPLChecker->getCurrentMinScheduler() = dtmcPLChecker->getCurrentMinScheduler()->template toValueType(); + } } #ifdef STORM_HAVE_CARL diff --git a/src/storm/modelchecker/parametric/SparseMdpInstantiationModelChecker.cpp b/src/storm/modelchecker/parametric/SparseMdpInstantiationModelChecker.cpp index dbc0fc88e..1be1e9ac8 100644 --- a/src/storm/modelchecker/parametric/SparseMdpInstantiationModelChecker.cpp +++ b/src/storm/modelchecker/parametric/SparseMdpInstantiationModelChecker.cpp @@ -4,6 +4,7 @@ #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "storm/modelchecker/hints/ExplicitModelCheckerHint.h" +#include "storm/storage/Scheduler.h" #include "storm/utility/graph.h" #include "storm/utility/vector.h" @@ -53,16 +54,16 @@ namespace storm { // For qualitative properties, we still want a quantitative result hint. Hence we perform the check on the subformula if(this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) { result = modelChecker.check(*this->currentCheckTask); - storm::storage::Scheduler const& scheduler = result->template asExplicitQuantitativeCheckResult().getScheduler(); + storm::storage::Scheduler const& scheduler = result->template asExplicitQuantitativeCheckResult().getScheduler(); hint.setResultHint(result->template asExplicitQuantitativeCheckResult().getValueVector()); - hint.setSchedulerHint(dynamic_cast(scheduler)); + hint.setSchedulerHint(dynamic_cast const&>(scheduler)); } else { auto newCheckTask = this->currentCheckTask->substituteFormula(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula()).setOnlyInitialStatesRelevant(false); std::unique_ptr quantitativeResult = modelChecker.computeProbabilities(newCheckTask); result = quantitativeResult->template asExplicitQuantitativeCheckResult().compareAgainstBound(this->currentCheckTask->getFormula().asOperatorFormula().getComparisonType(), this->currentCheckTask->getFormula().asOperatorFormula().template getThresholdAs()); - storm::storage::Scheduler& scheduler = quantitativeResult->template asExplicitQuantitativeCheckResult().getScheduler(); + storm::storage::Scheduler& scheduler = quantitativeResult->template asExplicitQuantitativeCheckResult().getScheduler(); hint.setResultHint(std::move(quantitativeResult->template asExplicitQuantitativeCheckResult().getValueVector())); - hint.setSchedulerHint(std::move(dynamic_cast(scheduler))); + hint.setSchedulerHint(std::move(dynamic_cast&>(scheduler))); } if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) { @@ -98,16 +99,16 @@ namespace storm { // For qualitative properties, we still want a quantitative result hint. Hence we perform the check on the subformula if(this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) { std::unique_ptr result = modelChecker.check(*this->currentCheckTask); - storm::storage::Scheduler const& scheduler = result->template asExplicitQuantitativeCheckResult().getScheduler(); + storm::storage::Scheduler const& scheduler = result->template asExplicitQuantitativeCheckResult().getScheduler(); hint.setResultHint(result->template asExplicitQuantitativeCheckResult().getValueVector()); - hint.setSchedulerHint(dynamic_cast(scheduler)); + hint.setSchedulerHint(dynamic_cast const&>(scheduler)); } else { auto newCheckTask = this->currentCheckTask->substituteFormula(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula()).setOnlyInitialStatesRelevant(false); std::unique_ptr quantitativeResult = modelChecker.computeRewards(this->currentCheckTask->getFormula().asRewardOperatorFormula().getMeasureType(), newCheckTask); result = quantitativeResult->template asExplicitQuantitativeCheckResult().compareAgainstBound(this->currentCheckTask->getFormula().asOperatorFormula().getComparisonType(), this->currentCheckTask->getFormula().asOperatorFormula().template getThresholdAs()); - storm::storage::Scheduler& scheduler = quantitativeResult->template asExplicitQuantitativeCheckResult().getScheduler(); + storm::storage::Scheduler& scheduler = quantitativeResult->template asExplicitQuantitativeCheckResult().getScheduler(); hint.setResultHint(std::move(quantitativeResult->template asExplicitQuantitativeCheckResult().getValueVector())); - hint.setSchedulerHint(std::move(dynamic_cast(scheduler))); + hint.setSchedulerHint(std::move(dynamic_cast&>(scheduler))); } if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) { diff --git a/src/storm/modelchecker/parametric/SparseMdpInstantiationModelChecker.h b/src/storm/modelchecker/parametric/SparseMdpInstantiationModelChecker.h index f9fc7e4ec..a5570acc0 100644 --- a/src/storm/modelchecker/parametric/SparseMdpInstantiationModelChecker.h +++ b/src/storm/modelchecker/parametric/SparseMdpInstantiationModelChecker.h @@ -8,7 +8,6 @@ #include "storm/modelchecker/parametric/SparseInstantiationModelChecker.h" #include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h" #include "storm/utility/ModelInstantiator.h" -#include "storm/storage/TotalScheduler.h" namespace storm { namespace modelchecker { diff --git a/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.cpp b/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.cpp index 6d9bc4d36..7b8df081a 100644 --- a/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.cpp +++ b/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.cpp @@ -214,8 +214,8 @@ namespace storm { if (applyPreviousResultAsHint) { solver->setTrackSchedulers(true); x.resize(maybeStates.getNumberOfSetBits(), storm::utility::zero()); - if(storm::solver::minimize(dirForParameters) && minSched && player1Sched) solver->setSchedulerHints(std::move(player1Sched.get()), std::move(minSched.get())); - if(storm::solver::maximize(dirForParameters) && maxSched && player1Sched) solver->setSchedulerHints(std::move(player1Sched.get()), std::move(maxSched.get())); + if(storm::solver::minimize(dirForParameters) && minSchedChoices && player1SchedChoices) solver->setSchedulerHints(std::move(player1SchedChoices.get()), std::move(minSchedChoices.get())); + if(storm::solver::maximize(dirForParameters) && maxSchedChoices && player1SchedChoices) solver->setSchedulerHints(std::move(player1SchedChoices.get()), std::move(maxSchedChoices.get())); } else { x.assign(maybeStates.getNumberOfSetBits(), storm::utility::zero()); } @@ -241,11 +241,11 @@ namespace storm { solver->solveGame(this->currentCheckTask->getOptimizationDirection(), dirForParameters, x, parameterLifter->getVector()); if(applyPreviousResultAsHint) { if(storm::solver::minimize(dirForParameters)) { - minSched = std::move(*solver->getPlayer2Scheduler()); + minSchedChoices = solver->getPlayer2SchedulerChoices(); } else { - maxSched = std::move(*solver->getPlayer2Scheduler()); + maxSchedChoices = solver->getPlayer2SchedulerChoices(); } - player1Sched = std::move(*solver->getPlayer1Scheduler()); + player1SchedChoices = solver->getPlayer1SchedulerChoices(); } } @@ -285,8 +285,8 @@ namespace storm { stepBound = boost::none; player1Matrix = storm::storage::SparseMatrix(); parameterLifter = nullptr; - minSched = boost::none; - maxSched = boost::none; + minSchedChoices = boost::none; + maxSchedChoices = boost::none; x.clear(); lowerResultBound = boost::none; upperResultBound = boost::none; @@ -294,18 +294,51 @@ namespace storm { } template - boost::optional& SparseMdpParameterLiftingModelChecker::getCurrentMinScheduler() { - return minSched; + boost::optional> SparseMdpParameterLiftingModelChecker::getCurrentMinScheduler() { + if (!minSchedChoices) { + return boost::none; + } + + storm::storage::Scheduler result(minSchedChoices->size()); + uint_fast64_t state = 0; + for (auto const& schedulerChoice : minSchedChoices.get()) { + result.setChoice(schedulerChoice, state); + ++state; + } + + return result; } template - boost::optional& SparseMdpParameterLiftingModelChecker::getCurrentMaxScheduler() { - return maxSched; + boost::optional> SparseMdpParameterLiftingModelChecker::getCurrentMaxScheduler() { + if (!maxSchedChoices) { + return boost::none; + } + + storm::storage::Scheduler result(maxSchedChoices->size()); + uint_fast64_t state = 0; + for (auto const& schedulerChoice : maxSchedChoices.get()) { + result.setChoice(schedulerChoice, state); + ++state; + } + + return result; } template - boost::optional& SparseMdpParameterLiftingModelChecker::getCurrentPlayer1Scheduler() { - return player1Sched; + boost::optional> SparseMdpParameterLiftingModelChecker::getCurrentPlayer1Scheduler() { + if (!player1SchedChoices) { + return boost::none; + } + + storm::storage::Scheduler result(player1SchedChoices->size()); + uint_fast64_t state = 0; + for (auto const& schedulerChoice : player1SchedChoices.get()) { + result.setChoice(schedulerChoice, state); + ++state; + } + + return result; } template class SparseMdpParameterLiftingModelChecker, double>; diff --git a/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.h b/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.h index 0e2c4a3c4..4e0b6e068 100644 --- a/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.h +++ b/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.h @@ -10,7 +10,7 @@ #include "storm/storage/sparse/StateType.h" #include "storm/solver/GameSolver.h" #include "storm/transformer/ParameterLifter.h" -#include "storm/storage/TotalScheduler.h" +#include "storm/storage/Scheduler.h" namespace storm { namespace modelchecker { @@ -24,9 +24,9 @@ namespace storm { virtual bool canHandle(CheckTask const& checkTask) const override; - boost::optional& getCurrentMinScheduler(); - boost::optional& getCurrentMaxScheduler(); - boost::optional& getCurrentPlayer1Scheduler(); + boost::optional> getCurrentMinScheduler(); + boost::optional> getCurrentMaxScheduler(); + boost::optional> getCurrentPlayer1Scheduler(); protected: @@ -52,8 +52,8 @@ namespace storm { std::unique_ptr> solverFactory; // Results from the most recent solver call. - boost::optional minSched, maxSched; - boost::optional player1Sched; + boost::optional> minSchedChoices, maxSchedChoices; + boost::optional> player1SchedChoices; std::vector x; boost::optional lowerResultBound, upperResultBound; bool applyPreviousResultAsHint; diff --git a/src/storm/modelchecker/parametric/SparseMdpRegionChecker.cpp b/src/storm/modelchecker/parametric/SparseMdpRegionChecker.cpp index e61201415..9ffa707fa 100644 --- a/src/storm/modelchecker/parametric/SparseMdpRegionChecker.cpp +++ b/src/storm/modelchecker/parametric/SparseMdpRegionChecker.cpp @@ -48,9 +48,15 @@ namespace storm { STORM_LOG_ASSERT(MdpPLChecker, "Underlying Parameter lifting checker has unexpected type"); auto exactMdpPLChecker = dynamic_cast*>(this->exactParameterLiftingChecker.get()); STORM_LOG_ASSERT(exactMdpPLChecker, "Underlying exact parameter lifting checker has unexpected type"); - exactMdpPLChecker->getCurrentMaxScheduler() = MdpPLChecker->getCurrentMaxScheduler(); - exactMdpPLChecker->getCurrentMinScheduler() = MdpPLChecker->getCurrentMinScheduler(); - exactMdpPLChecker->getCurrentPlayer1Scheduler() = MdpPLChecker->getCurrentPlayer1Scheduler(); + if (MdpPLChecker->getCurrentMaxScheduler()) { + exactMdpPLChecker->getCurrentMaxScheduler() = MdpPLChecker->getCurrentMaxScheduler()->template toValueType(); + } + if (MdpPLChecker->getCurrentMinScheduler()) { + exactMdpPLChecker->getCurrentMinScheduler() = MdpPLChecker->getCurrentMinScheduler()->template toValueType(); + } + if (MdpPLChecker->getCurrentPlayer1Scheduler()) { + exactMdpPLChecker->getCurrentPlayer1Scheduler() = MdpPLChecker->getCurrentPlayer1Scheduler()->template toValueType(); + } } diff --git a/src/storm/modelchecker/prctl/helper/MDPModelCheckingHelperReturnType.h b/src/storm/modelchecker/prctl/helper/MDPModelCheckingHelperReturnType.h index 19fb2de22..d40c5ade0 100644 --- a/src/storm/modelchecker/prctl/helper/MDPModelCheckingHelperReturnType.h +++ b/src/storm/modelchecker/prctl/helper/MDPModelCheckingHelperReturnType.h @@ -18,7 +18,7 @@ namespace storm { MDPSparseModelCheckingHelperReturnType(MDPSparseModelCheckingHelperReturnType const&) = delete; MDPSparseModelCheckingHelperReturnType(MDPSparseModelCheckingHelperReturnType&&) = default; - MDPSparseModelCheckingHelperReturnType(std::vector&& values, std::unique_ptr&& scheduler = nullptr) : values(std::move(values)), scheduler(std::move(scheduler)) { + MDPSparseModelCheckingHelperReturnType(std::vector&& values, std::unique_ptr>&& scheduler = nullptr) : values(std::move(values)), scheduler(std::move(scheduler)) { // Intentionally left empty. } @@ -30,7 +30,7 @@ namespace storm { std::vector values; // A scheduler, if it was computed. - std::unique_ptr scheduler; + std::unique_ptr> scheduler; }; } diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index b4d818ad2..b10934fdb 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -13,7 +13,7 @@ #include "storm/storage/expressions/Variable.h" #include "storm/storage/expressions/Expression.h" -#include "storm/storage/TotalScheduler.h" +#include "storm/storage/Scheduler.h" #include "storm/solver/MinMaxLinearEquationSolver.h" #include "storm/solver/LpSolver.h" @@ -126,9 +126,9 @@ namespace storm { } // If requested, we will produce a scheduler. - std::unique_ptr scheduler; + std::unique_ptr> scheduler; if (produceScheduler) { - scheduler = std::make_unique(transitionMatrix.getRowGroupCount()); + scheduler = std::make_unique>(transitionMatrix.getRowGroupCount()); } // Check whether we need to compute exact probabilities for some states. @@ -147,43 +147,105 @@ namespace storm { // the accumulated probability of going from state i to some 'yes' state. std::vector b = transitionMatrix.getConstrainedRowGroupSumVector(maybeStates, statesWithProbability1); - // Now compute the results for the maybeStates + // obtain hint information if possible bool skipEcWithinMaybeStatesCheck = goal.minimize() || (hint.isExplicitModelCheckerHint() && hint.asExplicitModelCheckerHint().getNoEndComponentsInMaybeStates()); - MDPSparseModelCheckingHelperReturnType resultForMaybeStates = computeValuesOnlyMaybeStates(goal, transitionMatrix, backwardTransitions, maybeStates, submatrix, b, produceScheduler, minMaxLinearEquationSolverFactory, hint, skipEcWithinMaybeStatesCheck, storm::utility::zero(), storm::utility::one()); + std::pair>, boost::optional>> hintInformation = extractHintInformationForMaybeStates(transitionMatrix, backwardTransitions, maybeStates, boost::none, hint, skipEcWithinMaybeStatesCheck); + + // Now compute the results for the maybeStates + std::pair, boost::optional>> resultForMaybeStates = computeValuesOnlyMaybeStates(goal, submatrix, b, produceScheduler, minMaxLinearEquationSolverFactory, std::move(hintInformation.first), std::move(hintInformation.second), storm::utility::zero(), storm::utility::one()); // Set values of resulting vector according to result. - storm::utility::vector::setVectorValues(result, maybeStates, resultForMaybeStates.values); + storm::utility::vector::setVectorValues(result, maybeStates, resultForMaybeStates.first); if (produceScheduler) { - storm::storage::Scheduler const& subscheduler = *resultForMaybeStates.scheduler; - uint_fast64_t currentSubState = 0; + std::vector const& subChoices = resultForMaybeStates.second.get(); + auto subChoiceIt = subChoices.begin(); for (auto maybeState : maybeStates) { - scheduler->setChoice(maybeState, subscheduler.getChoice(currentSubState)); - ++currentSubState; + scheduler->setChoice(*subChoiceIt, maybeState); + ++subChoiceIt; } + assert(subChoiceIt == subChoices.end()); } } } // Finally, if we need to produce a scheduler, we also need to figure out the parts of the scheduler for - // the states with probability 0 or 1 (depending on whether we maximize or minimize). + // the states with probability 1 or 0 (depending on whether we maximize or minimize). + // We also need to define some arbitrary choice for the remaining states to obtain a fully defined scheduler. if (produceScheduler) { - storm::storage::PartialScheduler relevantQualitativeScheduler; if (goal.minimize()) { - relevantQualitativeScheduler = storm::utility::graph::computeSchedulerProb0E(statesWithProbability0, transitionMatrix); + storm::utility::graph::computeSchedulerProb0E(statesWithProbability0, transitionMatrix, *scheduler); + for (auto const& prob1State : statesWithProbability1) { + scheduler->setChoice(0, prob1State); + } } else { - relevantQualitativeScheduler = storm::utility::graph::computeSchedulerProb1E(statesWithProbability1, transitionMatrix, backwardTransitions, phiStates, psiStates); - } - for (auto const& stateChoicePair : relevantQualitativeScheduler) { - scheduler->setChoice(stateChoicePair.first, stateChoicePair.second); + storm::utility::graph::computeSchedulerProb1E(statesWithProbability1, transitionMatrix, backwardTransitions, phiStates, psiStates, *scheduler); + for (auto const& prob0State : statesWithProbability0) { + scheduler->setChoice(0, prob0State); + } } } + STORM_LOG_ASSERT((!produceScheduler && !scheduler) || (!scheduler->isPartialScheduler() && scheduler->isDeterministicScheduler() && scheduler->isMemorylessScheduler()), "Unexpected format of obtained scheduler."); + + return MDPSparseModelCheckingHelperReturnType(std::move(result), std::move(scheduler)); } template - MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelper::computeValuesOnlyMaybeStates(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& maybeStates, storm::storage::SparseMatrix const& submatrix, std::vector const& b, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint, bool skipECWithinMaybeStatesCheck, boost::optional const& lowerResultBound, boost::optional const& upperResultBound) { + std::pair>, boost::optional>> SparseMdpPrctlHelper::extractHintInformationForMaybeStates(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& maybeStates, boost::optional const& selectedChoices, ModelCheckerHint const& hint, bool skipECWithinMaybeStatesCheck) { + + // Scheduler hint + boost::optional> subSchedulerChoices; + if (hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint().hasSchedulerHint()) { + auto const& schedulerHint = hint.template asExplicitModelCheckerHint().getSchedulerHint(); + std::vector hintChoices; + + // the scheduler hint is only applicable if it induces no BSCC consisting of maybestates + bool hintApplicable; + if (!skipECWithinMaybeStatesCheck) { + hintChoices.reserve(maybeStates.size()); + for (uint_fast64_t state = 0; state < maybeStates.size(); ++state) { + hintChoices.push_back(schedulerHint.getChoice(state).getDeterministicChoice()); + } + hintApplicable = storm::utility::graph::performProb1(transitionMatrix.transposeSelectedRowsFromRowGroups(hintChoices), maybeStates, ~maybeStates).full(); + } else { + hintApplicable = true; + } + + if (hintApplicable) { + // Compute the hint w.r.t. the given subsystem + hintChoices.clear(); + hintChoices.reserve(maybeStates.getNumberOfSetBits()); + for (auto const& state : maybeStates) { + uint_fast64_t hintChoice = schedulerHint.getChoice(state).getDeterministicChoice(); + if (selectedChoices) { + uint_fast64_t firstChoice = transitionMatrix.getRowGroupIndices()[state]; + uint_fast64_t lastChoice = firstChoice + hintChoice; + hintChoice = 0; + for (uint_fast64_t choice = selectedChoices->getNextSetIndex(firstChoice); choice < lastChoice; choice = selectedChoices->getNextSetIndex(choice + 1)) { + ++hintChoice; + } + } + hintChoices.push_back(hintChoice); + } + subSchedulerChoices = std::move(hintChoices); + } + } + + // Solution value hint + boost::optional> subValues; + // The result hint is only applicable if there are no End Components consisting of maybestates + if (hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint().hasResultHint() && + (skipECWithinMaybeStatesCheck || subSchedulerChoices || + storm::utility::graph::performProb1A(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, maybeStates, ~maybeStates).full())) { + subValues = storm::utility::vector::filterVector(hint.template asExplicitModelCheckerHint().getResultHint(), maybeStates); + } + return std::make_pair(std::move(subValues), std::move(subSchedulerChoices)); + } + + template + std::pair, boost::optional>> SparseMdpPrctlHelper::computeValuesOnlyMaybeStates(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix const& submatrix, std::vector const& b, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, boost::optional>&& hintValues, boost::optional>&& hintChoices, boost::optional const& lowerResultBound, boost::optional const& upperResultBound) { // Set up the solver std::unique_ptr> solver = storm::solver::configureMinMaxLinearEquationSolver(goal, minMaxLinearEquationSolverFactory, submatrix); @@ -193,33 +255,22 @@ namespace storm { if (upperResultBound) { solver->setUpperBound(upperResultBound.get()); } - // the scheduler hint is only applicable if it induces no BSCC consisting of maybestates - if (hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint().hasSchedulerHint() && - (skipECWithinMaybeStatesCheck || - storm::utility::graph::performProb1(transitionMatrix.transposeSelectedRowsFromRowGroups(hint.template asExplicitModelCheckerHint().getSchedulerHint().getChoices()), maybeStates, ~maybeStates).full())) { - solver->setSchedulerHint(hint.template asExplicitModelCheckerHint().getSchedulerHint().getSchedulerForSubsystem(maybeStates)); + if (hintChoices) { + solver->setSchedulerHint(std::move(hintChoices.get())); } solver->setTrackScheduler(produceScheduler); - // Create the solution vector. - std::vector x; - // The result hint is only applicable if there are no End Components consisting of maybestates - if (hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint().hasResultHint() && - (skipECWithinMaybeStatesCheck || solver->hasSchedulerHint() || - storm::utility::graph::performProb1A(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, maybeStates, ~maybeStates).full())) { - x = storm::utility::vector::filterVector(hint.template asExplicitModelCheckerHint().getResultHint(), maybeStates); - } else { - x = std::vector(submatrix.getRowGroupCount(), lowerResultBound ? lowerResultBound.get() : storm::utility::zero()); - } + // Initialize the solution vector. + std::vector x = hintValues ? std::move(hintValues.get()) : std::vector(submatrix.getRowGroupCount(), lowerResultBound ? lowerResultBound.get() : storm::utility::zero()); // Solve the corresponding system of equations. solver->solveEquations(x, b); // If requested, a scheduler was produced if (produceScheduler) { - return MDPSparseModelCheckingHelperReturnType(std::move(x), std::move(solver->getScheduler())); + return std::pair, boost::optional>>(std::move(x), std::move(solver->getSchedulerChoices())); } else { - return MDPSparseModelCheckingHelperReturnType(std::move(x)); + return std::pair, boost::optional>>(std::move(x), boost::none); } } @@ -363,9 +414,9 @@ namespace storm { storm::utility::vector::setVectorValues(result, infinityStates, storm::utility::infinity()); // If requested, we will produce a scheduler. - std::unique_ptr scheduler; + std::unique_ptr> scheduler; if (produceScheduler) { - scheduler = std::make_unique(transitionMatrix.getRowGroupCount()); + scheduler = std::make_unique>(transitionMatrix.getRowGroupCount()); } // Check whether we need to compute exact rewards for some states. @@ -394,50 +445,58 @@ namespace storm { storm::utility::vector::filterVectorInPlace(b, *selectedChoices); } + // obtain hint information if possible bool skipEcWithinMaybeStatesCheck = !goal.minimize() || (hint.isExplicitModelCheckerHint() && hint.asExplicitModelCheckerHint().getNoEndComponentsInMaybeStates()); + std::pair>, boost::optional>> hintInformation = extractHintInformationForMaybeStates(transitionMatrix, backwardTransitions, maybeStates, selectedChoices, hint, skipEcWithinMaybeStatesCheck); + // Now compute the results for the maybeStates - MDPSparseModelCheckingHelperReturnType resultForMaybeStates = computeValuesOnlyMaybeStates(goal, transitionMatrix, backwardTransitions, maybeStates, submatrix, b, produceScheduler, minMaxLinearEquationSolverFactory, hint, skipEcWithinMaybeStatesCheck, storm::utility::zero()); + std::pair, boost::optional>> resultForMaybeStates = computeValuesOnlyMaybeStates(goal, submatrix, b, produceScheduler, minMaxLinearEquationSolverFactory, std::move(hintInformation.first), std::move(hintInformation.second), storm::utility::zero()); // Set values of resulting vector according to result. - storm::utility::vector::setVectorValues(result, maybeStates, resultForMaybeStates.values); + storm::utility::vector::setVectorValues(result, maybeStates, resultForMaybeStates.first); if (produceScheduler) { - storm::storage::Scheduler const& subscheduler = *resultForMaybeStates.scheduler; + std::vector const& subChoices = resultForMaybeStates.second.get(); + auto subChoiceIt = subChoices.begin(); if (selectedChoices) { - uint_fast64_t currentSubState = 0; for (auto maybeState : maybeStates) { - uint_fast64_t subChoice = subscheduler.getChoice(currentSubState); // find the rowindex that corresponds to the selected row of the submodel uint_fast64_t firstRowIndex = transitionMatrix.getRowGroupIndices()[maybeState]; uint_fast64_t selectedRowIndex = selectedChoices->getNextSetIndex(firstRowIndex); - for (uint_fast64_t choice = 0; choice < subChoice; ++choice) { + for (uint_fast64_t choice = 0; choice < *subChoiceIt; ++choice) { selectedRowIndex = selectedChoices->getNextSetIndex(selectedRowIndex + 1); } - scheduler->setChoice(maybeState, selectedRowIndex - firstRowIndex); - ++currentSubState; + scheduler->setChoice(selectedRowIndex - firstRowIndex, maybeState); + ++subChoiceIt; } } else { - uint_fast64_t currentSubState = 0; for (auto maybeState : maybeStates) { - scheduler->setChoice(maybeState, subscheduler.getChoice(currentSubState)); - ++currentSubState; + scheduler->setChoice(*subChoiceIt, maybeState); + ++subChoiceIt; } } + assert(subChoiceIt == subChoices.end()); } } } // Finally, if we need to produce a scheduler, we also need to figure out the parts of the scheduler for - // the states with reward infinity. + // the states with reward infinity. Moreover, we have to set some arbitrary choice for the remaining states + // to obtain a fully defined scheduler if (produceScheduler) { - storm::storage::PartialScheduler relevantQualitativeScheduler; if (!goal.minimize()) { - relevantQualitativeScheduler = storm::utility::graph::computeSchedulerProb0E(infinityStates, transitionMatrix); + storm::utility::graph::computeSchedulerProb0E(infinityStates, transitionMatrix, *scheduler); + } else { + for (auto const& state : infinityStates) { + scheduler->setChoice(0, state); + } } - for (auto const& stateChoicePair : relevantQualitativeScheduler) { - scheduler->setChoice(stateChoicePair.first, stateChoicePair.second); + for (auto const& state : targetStates) { + scheduler->setChoice(0, state); } } + STORM_LOG_ASSERT((!produceScheduler && !scheduler) || (!scheduler->isPartialScheduler() && scheduler->isDeterministicScheduler() && scheduler->isMemorylessScheduler()), "Unexpected format of obtained scheduler."); + return MDPSparseModelCheckingHelperReturnType(std::move(result), std::move(scheduler)); } diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h index 357fb07b5..926fa208c 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h @@ -39,7 +39,9 @@ namespace storm { static MDPSparseModelCheckingHelperReturnType computeUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint = ModelCheckerHint()); - static MDPSparseModelCheckingHelperReturnType computeValuesOnlyMaybeStates(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& maybeStates, storm::storage::SparseMatrix const& submatrix, std::vector const& b, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint = ModelCheckerHint(), bool skipECWithinMaybeStatesCheck = false, boost::optional const& lowerResultBound = boost::none, boost::optional const& upperResultBound = boost::none); + static std::pair>, boost::optional>> extractHintInformationForMaybeStates(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& maybeStates, boost::optional const& selectedChoices, ModelCheckerHint const& hint, bool skipECWithinMaybeStatesCheck); + + static std::pair, boost::optional>> computeValuesOnlyMaybeStates(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix const& submatrix, std::vector const& b, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, boost::optional>&& hintValues = boost::none, boost::optional>&& hintChoices = boost::none, boost::optional const& lowerResultBound = boost::none, boost::optional const& upperResultBound = boost::none); static MDPSparseModelCheckingHelperReturnType computeUntilProbabilities(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint = ModelCheckerHint()); diff --git a/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp b/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp index 31bb67b5d..5077aa263 100644 --- a/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp +++ b/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp @@ -166,18 +166,18 @@ namespace storm { } template - void ExplicitQuantitativeCheckResult::setScheduler(std::unique_ptr&& scheduler) { + void ExplicitQuantitativeCheckResult::setScheduler(std::unique_ptr>&& scheduler) { this->scheduler = std::move(scheduler); } template - storm::storage::Scheduler const& ExplicitQuantitativeCheckResult::getScheduler() const { + storm::storage::Scheduler const& ExplicitQuantitativeCheckResult::getScheduler() const { STORM_LOG_THROW(this->hasScheduler(), storm::exceptions::InvalidOperationException, "Unable to retrieve non-existing scheduler."); return *scheduler.get(); } template - storm::storage::Scheduler& ExplicitQuantitativeCheckResult::getScheduler() { + storm::storage::Scheduler& ExplicitQuantitativeCheckResult::getScheduler() { STORM_LOG_THROW(this->hasScheduler(), storm::exceptions::InvalidOperationException, "Unable to retrieve non-existing scheduler."); return *scheduler.get(); } diff --git a/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.h b/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.h index bd0a2387f..41a0f8477 100644 --- a/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.h +++ b/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.h @@ -62,16 +62,16 @@ namespace storm { virtual ValueType sum() const override; bool hasScheduler() const; - void setScheduler(std::unique_ptr&& scheduler); - storm::storage::Scheduler const& getScheduler() const; - storm::storage::Scheduler& getScheduler(); + void setScheduler(std::unique_ptr>&& scheduler); + storm::storage::Scheduler const& getScheduler() const; + storm::storage::Scheduler& getScheduler(); private: // The values of the quantitative check result. boost::variant values; // An optional scheduler that accompanies the values. - boost::optional> scheduler; + boost::optional>> scheduler; }; } } diff --git a/src/storm/solver/GameSolver.cpp b/src/storm/solver/GameSolver.cpp index c08db00e6..f637f805d 100644 --- a/src/storm/solver/GameSolver.cpp +++ b/src/storm/solver/GameSolver.cpp @@ -18,8 +18,8 @@ namespace storm { void GameSolver::setTrackSchedulers(bool value) { trackSchedulers = value; if (!trackSchedulers) { - player1Scheduler = boost::none; - player2Scheduler = boost::none; + player1SchedulerChoices = boost::none; + player2SchedulerChoices = boost::none; } } @@ -30,42 +30,54 @@ namespace storm { template bool GameSolver::hasSchedulers() const { - return player1Scheduler.is_initialized() && player2Scheduler.is_initialized(); + return player1SchedulerChoices.is_initialized() && player2SchedulerChoices.is_initialized(); } template - storm::storage::TotalScheduler const& GameSolver::getPlayer1Scheduler() const { - STORM_LOG_THROW(player1Scheduler, storm::exceptions::IllegalFunctionCallException, "Cannot retrieve player 1 scheduler, because none was generated."); - return *player1Scheduler.get(); + storm::storage::Scheduler GameSolver::computePlayer1Scheduler() const { + STORM_LOG_THROW(hasSchedulers(), storm::exceptions::IllegalFunctionCallException, "Cannot retrieve player 1 scheduler, because none was generated."); + storm::storage::Scheduler result(player1SchedulerChoices->size()); + uint_fast64_t state = 0; + for (auto const& schedulerChoice : player1SchedulerChoices.get()) { + result.setChoice(schedulerChoice, state); + ++state; + } + return result; } template - storm::storage::TotalScheduler const& GameSolver::getPlayer2Scheduler() const { - STORM_LOG_THROW(player2Scheduler, storm::exceptions::IllegalFunctionCallException, "Cannot retrieve player 2 scheduler, because none was generated."); - return *player2Scheduler.get(); + storm::storage::Scheduler GameSolver::computePlayer2Scheduler() const { + STORM_LOG_THROW(hasSchedulers(), storm::exceptions::IllegalFunctionCallException, "Cannot retrieve player 2 scheduler, because none was generated."); + storm::storage::Scheduler result(player2SchedulerChoices->size()); + uint_fast64_t state = 0; + for (auto const& schedulerChoice : player2SchedulerChoices.get()) { + result.setChoice(schedulerChoice, state); + ++state; + } + return result; } template - std::unique_ptr GameSolver::getPlayer1Scheduler() { - STORM_LOG_THROW(player1Scheduler, storm::exceptions::IllegalFunctionCallException, "Cannot retrieve player 1 scheduler, because none was generated."); - return std::move(player1Scheduler.get()); + std::vector const& GameSolver::getPlayer1SchedulerChoices() const { + STORM_LOG_THROW(hasSchedulers(), storm::exceptions::IllegalFunctionCallException, "Cannot retrieve player 1 scheduler choices, because they were not generated."); + return player1SchedulerChoices.get(); } template - std::unique_ptr GameSolver::getPlayer2Scheduler() { - STORM_LOG_THROW(player2Scheduler, storm::exceptions::IllegalFunctionCallException, "Cannot retrieve player 2 scheduler, because none was generated."); - return std::move(player2Scheduler.get()); + std::vector const& GameSolver::getPlayer2SchedulerChoices() const { + STORM_LOG_THROW(hasSchedulers(), storm::exceptions::IllegalFunctionCallException, "Cannot retrieve player 2 scheduler choices, because they were not generated."); + return player2SchedulerChoices.get(); } template - void GameSolver::setSchedulerHints(storm::storage::TotalScheduler&& player1Scheduler, storm::storage::TotalScheduler&& player2Scheduler) { - this->player1SchedulerHint = std::move(player1Scheduler); - this->player2SchedulerHint = std::move(player2Scheduler); + void GameSolver::setSchedulerHints(std::vector&& player1Choices, std::vector&& player2Choices) { + this->player1ChoicesHint = std::move(player1Choices); + this->player2ChoicesHint = std::move(player2Choices); } template bool GameSolver::hasSchedulerHints() const { - return player1SchedulerHint.is_initialized() && player2SchedulerHint.is_initialized(); + return player1ChoicesHint.is_initialized() && player2ChoicesHint.is_initialized(); } template diff --git a/src/storm/solver/GameSolver.h b/src/storm/solver/GameSolver.h index 0940ac75b..a2f6888d4 100644 --- a/src/storm/solver/GameSolver.h +++ b/src/storm/solver/GameSolver.h @@ -7,7 +7,7 @@ #include "storm/solver/AbstractEquationSolver.h" #include "storm/solver/OptimizationDirection.h" #include "storm/storage/sparse/StateType.h" -#include "storm/storage/TotalScheduler.h" +#include "storm/storage/Scheduler.h" #include "storm/utility/macros.h" #include "storm/exceptions/InvalidSettingsException.h" @@ -72,23 +72,21 @@ namespace storm { bool hasSchedulers() const; /*! - * Retrieves the generated schedulers. Note: it is only legal to call this function if schedulers were generated. + * Retrieves the generated scheduler. Note: it is only legal to call this function if schedulers were generated. */ - storm::storage::TotalScheduler const& getPlayer1Scheduler() const; - storm::storage::TotalScheduler const& getPlayer2Scheduler() const; - + storm::storage::Scheduler computePlayer1Scheduler() const; + storm::storage::Scheduler computePlayer2Scheduler() const; + /*! - * Retrieves the generated schedulers and takes ownership of it. Note: it is only legal to call this functions - * if scheduler were generated and after calling this methods, the solver will not contain the corresponding scheduler - * any more (i.e. it is illegal to call this methods again until new schedulers have been generated). + * Retrieves the generated (deterministic) choices of the optimal scheduler. Note: it is only legal to call this function if schedulers were generated. */ - std::unique_ptr getPlayer1Scheduler(); - std::unique_ptr getPlayer2Scheduler(); + std::vector const& getPlayer1SchedulerChoices() const; + std::vector const& getPlayer2SchedulerChoices() const; /*! * Sets scheduler hints that might be considered by the solver as an initial guess */ - void setSchedulerHints(storm::storage::TotalScheduler&& player1Scheduler, storm::storage::TotalScheduler&& player2Scheduler); + void setSchedulerHints(std::vector&& player1Choices, std::vector&& player2Choices); /*! * Returns whether Scheduler hints are available @@ -145,9 +143,9 @@ namespace storm { /// Whether we generate schedulers during solving. bool trackSchedulers; - /// The schedulers (if they could be successfully generated). - mutable boost::optional> player1Scheduler; - mutable boost::optional> player2Scheduler; + /// The scheduler choices that induce the optimal values (if they could be successfully generated). + mutable boost::optional> player1SchedulerChoices; + mutable boost::optional> player2SchedulerChoices; // A lower bound if one was set. boost::optional lowerBound; @@ -155,9 +153,9 @@ namespace storm { // An upper bound if one was set. boost::optional upperBound; - // schedulers that might be considered by the solver as an initial guess - boost::optional player1SchedulerHint; - boost::optional player2SchedulerHint; + // scheduler choices that might be considered by the solver as an initial guess + boost::optional> player1ChoicesHint; + boost::optional> player2ChoicesHint; private: /// Whether some of the generated data during solver calls should be cached. diff --git a/src/storm/solver/MinMaxLinearEquationSolver.cpp b/src/storm/solver/MinMaxLinearEquationSolver.cpp index 6cdc2cf2b..5f1e0c176 100644 --- a/src/storm/solver/MinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/MinMaxLinearEquationSolver.cpp @@ -53,7 +53,7 @@ namespace storm { void MinMaxLinearEquationSolver::setTrackScheduler(bool trackScheduler) { this->trackScheduler = trackScheduler; if (!this->trackScheduler) { - scheduler = boost::none; + schedulerChoices = boost::none; } } @@ -64,19 +64,25 @@ namespace storm { template bool MinMaxLinearEquationSolver::hasScheduler() const { - return static_cast(scheduler); + return static_cast(schedulerChoices); } template - storm::storage::TotalScheduler const& MinMaxLinearEquationSolver::getScheduler() const { - STORM_LOG_THROW(scheduler, storm::exceptions::IllegalFunctionCallException, "Cannot retrieve scheduler, because none was generated."); - return *scheduler.get(); + storm::storage::Scheduler MinMaxLinearEquationSolver::computeScheduler() const { + STORM_LOG_THROW(hasScheduler(), storm::exceptions::IllegalFunctionCallException, "Cannot retrieve scheduler, because none was generated."); + storm::storage::Scheduler result(schedulerChoices->size()); + uint_fast64_t state = 0; + for (auto const& schedulerChoice : schedulerChoices.get()) { + result.setChoice(schedulerChoice, state); + ++state; + } + return result; } template - std::unique_ptr MinMaxLinearEquationSolver:: getScheduler() { - STORM_LOG_THROW(scheduler, storm::exceptions::IllegalFunctionCallException, "Cannot retrieve scheduler, because none was generated."); - return std::move(scheduler.get()); + std::vector const& MinMaxLinearEquationSolver::getSchedulerChoices() const { + STORM_LOG_THROW(hasScheduler(), storm::exceptions::IllegalFunctionCallException, "Cannot retrieve scheduler choices, because they were not generated."); + return schedulerChoices.get(); } template @@ -115,13 +121,13 @@ namespace storm { } template - void MinMaxLinearEquationSolver::setSchedulerHint(storm::storage::TotalScheduler&& scheduler) { - schedulerHint = scheduler; + void MinMaxLinearEquationSolver::setSchedulerHint(std::vector&& choices) { + choicesHint = std::move(choices); } template bool MinMaxLinearEquationSolver::hasSchedulerHint() const { - return schedulerHint.is_initialized(); + return choicesHint.is_initialized(); } template diff --git a/src/storm/solver/MinMaxLinearEquationSolver.h b/src/storm/solver/MinMaxLinearEquationSolver.h index 852e06cfe..1b869d165 100644 --- a/src/storm/solver/MinMaxLinearEquationSolver.h +++ b/src/storm/solver/MinMaxLinearEquationSolver.h @@ -10,7 +10,7 @@ #include "storm/solver/AbstractEquationSolver.h" #include "storm/solver/SolverSelectionOptions.h" #include "storm/storage/sparse/StateType.h" -#include "storm/storage/TotalScheduler.h" +#include "storm/storage/Scheduler.h" #include "storm/solver/OptimizationDirection.h" #include "storm/exceptions/InvalidSettingsException.h" @@ -108,14 +108,12 @@ namespace storm { /*! * Retrieves the generated scheduler. Note: it is only legal to call this function if a scheduler was generated. */ - storm::storage::TotalScheduler const& getScheduler() const; - + storm::storage::Scheduler computeScheduler() const; + /*! - * Retrieves the generated scheduler and takes ownership of it. Note: it is only legal to call this function - * if a scheduler was generated and after a call to this method, the solver will not contain the scheduler - * any more (i.e. it is illegal to call this method again until a new scheduler has been generated). + * Retrieves the generated (deterministic) choices of the optimal scheduler. Note: it is only legal to call this function if a scheduler was generated. */ - std::unique_ptr getScheduler(); + std::vector const& getSchedulerChoices() const; /** * Gets the precision after which the solver takes two numbers as equal. @@ -163,7 +161,7 @@ namespace storm { /*! * Sets a scheduler that might be considered by the solver as an initial guess */ - void setSchedulerHint(storm::storage::TotalScheduler&& scheduler); + void setSchedulerHint(std::vector&& choices); /*! * Returns true iff a scheduler hint was defined @@ -177,8 +175,8 @@ namespace storm { /// Whether we generate a scheduler during solving. bool trackScheduler; - /// The scheduler (if it could be successfully generated). - mutable boost::optional> scheduler; + /// The scheduler choices that induce the optimal values (if they could be successfully generated). + mutable boost::optional> schedulerChoices; // A lower bound if one was set. boost::optional lowerBound; @@ -186,8 +184,8 @@ namespace storm { // An upper bound if one was set. boost::optional upperBound; - // A scheduler that might be considered by the solver as an initial guess - boost::optional schedulerHint; + // Scheduler choices that might be considered by the solver as an initial guess + boost::optional> choicesHint; private: /// Whether some of the generated data during solver calls should be cached. diff --git a/src/storm/solver/StandardGameSolver.cpp b/src/storm/solver/StandardGameSolver.cpp index 49998ab46..af38b7a8c 100644 --- a/src/storm/solver/StandardGameSolver.cpp +++ b/src/storm/solver/StandardGameSolver.cpp @@ -101,8 +101,8 @@ namespace storm { bool StandardGameSolver::solveGamePolicyIteration(OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector& x, std::vector const& b) const { // Create the initial choice selections. - std::vector player1Choices = this->hasSchedulerHints() ? this->player1SchedulerHint->getChoices() : std::vector(this->player1Matrix.getRowGroupCount(), 0); - std::vector player2Choices = this->hasSchedulerHints() ? this->player2SchedulerHint->getChoices() : std::vector(this->player2Matrix.getRowGroupCount(), 0); + std::vector player1Choices = this->hasSchedulerHints() ? this->player1ChoicesHint.get() : std::vector(this->player1Matrix.getRowGroupCount(), 0); + std::vector player2Choices = this->hasSchedulerHints() ? this->player2ChoicesHint.get() : std::vector(this->player2Matrix.getRowGroupCount(), 0); if(!auxiliaryP2RowGroupVector) { auxiliaryP2RowGroupVector = std::make_unique>(this->player2Matrix.getRowGroupCount()); @@ -149,8 +149,8 @@ namespace storm { // If requested, we store the scheduler for retrieval. if (this->isTrackSchedulersSet()) { - this->player1Scheduler = std::make_unique(std::move(player1Choices)); - this->player2Scheduler = std::make_unique(std::move(player2Choices)); + this->player1SchedulerChoices = std::move(player1Choices); + this->player2SchedulerChoices = std::move(player2Choices); } if(!this->isCachingEnabled()) { @@ -205,7 +205,7 @@ namespace storm { if (this->hasSchedulerHints()) { // Solve the equation system induced by the two schedulers. storm::storage::SparseMatrix submatrix; - getInducedMatrixVector(x, b, this->player1SchedulerHint->getChoices(), this->player2SchedulerHint->getChoices(), submatrix, *auxiliaryP1RowGroupVector); + getInducedMatrixVector(x, b, this->player1ChoicesHint.get(), this->player2ChoicesHint.get(), submatrix, *auxiliaryP1RowGroupVector); submatrix.convertToEquationSystem(); auto submatrixSolver = linearEquationSolverFactory->create(std::move(submatrix)); if (this->lowerBound) { submatrixSolver->setLowerBound(this->lowerBound.get()); } @@ -244,11 +244,9 @@ namespace storm { // If requested, we store the scheduler for retrieval. if (this->isTrackSchedulersSet()) { - std::vector player1Choices(player1Matrix.getRowGroupCount(), 0); - std::vector player2Choices(player2Matrix.getRowGroupCount(), 0); - extractChoices(player1Dir, player2Dir, x, b, *auxiliaryP2RowGroupVector, player1Choices, player2Choices); - this->player1Scheduler = std::make_unique(std::move(player1Choices)); - this->player2Scheduler = std::make_unique(std::move(player2Choices)); + this->player1SchedulerChoices = std::vector(player1Matrix.getRowGroupCount(), 0); + this->player2SchedulerChoices = std::vector(player2Matrix.getRowGroupCount(), 0); + extractChoices(player1Dir, player2Dir, x, b, *auxiliaryP2RowGroupVector, this->player1SchedulerChoices.get(), this->player2SchedulerChoices.get()); } if(!this->isCachingEnabled()) { diff --git a/src/storm/solver/StandardGameSolver.h b/src/storm/solver/StandardGameSolver.h index 0f52867f6..dd0964fd9 100644 --- a/src/storm/solver/StandardGameSolver.h +++ b/src/storm/solver/StandardGameSolver.h @@ -62,7 +62,7 @@ namespace storm { void getInducedMatrixVector(std::vector& x, std::vector const& b, std::vector const& player1Choices, std::vector const& player2Choices, storm::storage::SparseMatrix& inducedMatrix, std::vector& inducedVector) const; // Extracts the choices of the different players for the given solution x. - // Returns true iff there are "better" choices for one of the players. + // Returns true iff the newly extracted choices yield "better" values then the given choices for one of the players. bool extractChoices(OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector const& x, std::vector const& b, std::vector& player2ChoiceValues, std::vector& player1Choices, std::vector& player2Choices) const; bool valueImproved(OptimizationDirection dir, ValueType const& value1, ValueType const& value2) const; diff --git a/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp b/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp index 4d68f00c1..0a93a70f4 100644 --- a/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp @@ -100,7 +100,7 @@ namespace storm { template bool StandardMinMaxLinearEquationSolver::solveEquationsPolicyIteration(OptimizationDirection dir, std::vector& x, std::vector const& b) const { // Create the initial scheduler. - std::vector scheduler = this->schedulerHint ? this->schedulerHint->getChoices() : std::vector(this->A.getRowGroupCount()); + std::vector scheduler = this->hasSchedulerHint() ? this->choicesHint.get() : std::vector(this->A.getRowGroupCount()); // Get a vector for storing the right-hand side of the inner equation system. if(!auxiliaryRowGroupVector) { @@ -180,7 +180,7 @@ namespace storm { // If requested, we store the scheduler for retrieval. if (this->isTrackSchedulerSet()) { - this->scheduler = std::make_unique(std::move(scheduler)); + this->schedulerChoices = std::move(scheduler); } if(!this->isCachingEnabled()) { @@ -225,11 +225,11 @@ namespace storm { auxiliaryRowGroupVector = std::make_unique>(A.getRowGroupCount()); } - if(this->schedulerHint) { + if (this->hasSchedulerHint()) { // Resolve the nondeterminism according to the scheduler hint - storm::storage::SparseMatrix submatrix = this->A.selectRowsFromRowGroups(this->schedulerHint->getChoices(), true); + storm::storage::SparseMatrix submatrix = this->A.selectRowsFromRowGroups(this->choicesHint.get(), true); submatrix.convertToEquationSystem(); - storm::utility::vector::selectVectorValues(*auxiliaryRowGroupVector, this->schedulerHint->getChoices(), this->A.getRowGroupIndices(), b); + storm::utility::vector::selectVectorValues(*auxiliaryRowGroupVector, this->choicesHint.get(), this->A.getRowGroupIndices(), b); // Solve the resulting equation system. // Note that the linEqSolver might consider a slightly different interpretation of "equalModuloPrecision". Hence, we iteratively increase its precision. @@ -281,13 +281,12 @@ namespace storm { if (iterations==0) { linEqSolverA->multiply(x, &b, multiplyResult); } - std::vector choices(this->A.getRowGroupCount()); + this->schedulerChoices = std::vector(this->A.getRowGroupCount()); // Reduce the multiplyResult and keep track of the choices made - storm::utility::vector::reduceVectorMinOrMax(dir, multiplyResult, x, this->A.getRowGroupIndices(), &choices); - this->scheduler = std::make_unique(std::move(choices)); + storm::utility::vector::reduceVectorMinOrMax(dir, multiplyResult, x, this->A.getRowGroupIndices(), &this->schedulerChoices.get()); } - if(!this->isCachingEnabled()) { + if (!this->isCachingEnabled()) { clearCache(); } diff --git a/src/storm/storage/Distribution.cpp b/src/storm/storage/Distribution.cpp index d918e4717..0c2ac73db 100644 --- a/src/storm/storage/Distribution.cpp +++ b/src/storm/storage/Distribution.cpp @@ -158,13 +158,21 @@ namespace storm { template class Distribution; template std::ostream& operator<<(std::ostream& out, Distribution const& distribution); + template class Distribution; + template std::ostream& operator<<(std::ostream& out, Distribution const& distribution); + template class Distribution; + template std::ostream& operator<<(std::ostream& out, Distribution const& distribution); #ifdef STORM_HAVE_CARL template class Distribution; template std::ostream& operator<<(std::ostream& out, Distribution const& distribution); + template class Distribution; + template std::ostream& operator<<(std::ostream& out, Distribution const& distribution); template class Distribution; template std::ostream& operator<<(std::ostream& out, Distribution const& distribution); + template class Distribution; + template std::ostream& operator<<(std::ostream& out, Distribution const& distribution); #endif } } diff --git a/src/storm/storage/PartialScheduler.cpp b/src/storm/storage/PartialScheduler.cpp deleted file mode 100644 index ad938a53d..000000000 --- a/src/storm/storage/PartialScheduler.cpp +++ /dev/null @@ -1,48 +0,0 @@ -#include "storm/storage/PartialScheduler.h" -#include "storm/exceptions/InvalidArgumentException.h" - -namespace storm { - namespace storage { - - void PartialScheduler::setChoice(uint_fast64_t state, uint_fast64_t choice) { - stateToChoiceMapping[state] = choice; - } - - bool PartialScheduler::isChoiceDefined(uint_fast64_t state) const { - return stateToChoiceMapping.find(state) != stateToChoiceMapping.end(); - } - - uint_fast64_t PartialScheduler::getChoice(uint_fast64_t state) const { - auto stateChoicePair = stateToChoiceMapping.find(state); - - if (stateChoicePair == stateToChoiceMapping.end()) { - throw storm::exceptions::InvalidArgumentException() << "Invalid call to PartialScheduler::getChoice: scheduler does not define a choice for state " << state << "."; - } - - return stateChoicePair->second; - } - - PartialScheduler::map_type::const_iterator PartialScheduler::begin() const { - return stateToChoiceMapping.begin(); - } - - PartialScheduler::map_type::const_iterator PartialScheduler::end() const { - return stateToChoiceMapping.end(); - } - - std::ostream& operator<<(std::ostream& out, PartialScheduler const& scheduler) { - out << "partial scheduler (defined on " << scheduler.stateToChoiceMapping.size() << " states) [ "; - uint_fast64_t remainingEntries = scheduler.stateToChoiceMapping.size(); - for (auto const& stateChoicePair : scheduler.stateToChoiceMapping) { - out << stateChoicePair.first << " -> " << stateChoicePair.second; - --remainingEntries; - if (remainingEntries > 0) { - out << ", "; - } - } - out << "]"; - return out; - } - - } // namespace storage -} // namespace storm diff --git a/src/storm/storage/PartialScheduler.h b/src/storm/storage/PartialScheduler.h deleted file mode 100644 index 3f16c868c..000000000 --- a/src/storm/storage/PartialScheduler.h +++ /dev/null @@ -1,34 +0,0 @@ -#ifndef STORM_STORAGE_PARTIALSCHEDULER_H_ -#define STORM_STORAGE_PARTIALSCHEDULER_H_ - -#include -#include - -#include "storm/storage/Scheduler.h" - -namespace storm { - namespace storage { - - class PartialScheduler : public Scheduler { - public: - typedef std::unordered_map map_type; - - void setChoice(uint_fast64_t state, uint_fast64_t choice) override; - - bool isChoiceDefined(uint_fast64_t state) const override; - - uint_fast64_t getChoice(uint_fast64_t state) const override; - - map_type::const_iterator begin() const; - map_type::const_iterator end() const; - - friend std::ostream& operator<<(std::ostream& out, PartialScheduler const& scheduler); - - private: - // A mapping from all states that have defined choices to their respective choices. - map_type stateToChoiceMapping; - }; - } -} - -#endif /* STORM_STORAGE_PARTIALSCHEDULER_H_ */ diff --git a/src/storm/storage/Scheduler.cpp b/src/storm/storage/Scheduler.cpp new file mode 100644 index 000000000..b7e842951 --- /dev/null +++ b/src/storm/storage/Scheduler.cpp @@ -0,0 +1,187 @@ +#include +#include "storm/storage/Scheduler.h" + +#include "storm/utility/macros.h" +#include "storm/exceptions/NotImplementedException.h" + +namespace storm { + namespace storage { + + template + Scheduler::Scheduler(uint_fast64_t numberOfModelStates, boost::optional const& memoryStructure) : memoryStructure(memoryStructure) { + uint_fast64_t numOfMemoryStates = memoryStructure ? memoryStructure->getNumberOfStates() : 1; + schedulerChoices = std::vector>>(numOfMemoryStates, std::vector>(numberOfModelStates)); + numOfUndefinedChoices = numOfMemoryStates * numberOfModelStates; + numOfDeterministicChoices = 0; + } + + template + Scheduler::Scheduler(uint_fast64_t numberOfModelStates, boost::optional&& memoryStructure) : memoryStructure(std::move(memoryStructure)) { + uint_fast64_t numOfMemoryStates = memoryStructure ? memoryStructure->getNumberOfStates() : 1; + schedulerChoices = std::vector>>(numOfMemoryStates, std::vector>(numberOfModelStates)); + numOfUndefinedChoices = numOfMemoryStates * numberOfModelStates; + numOfDeterministicChoices = 0; + } + + template + void Scheduler::setChoice(SchedulerChoice const& choice, uint_fast64_t modelState, uint_fast64_t memoryState) { + STORM_LOG_ASSERT(memoryState < getNumberOfMemoryStates(), "Illegal memory state index"); + STORM_LOG_ASSERT(modelState < schedulerChoices[memoryState].size(), "Illegal model state index"); + auto& schedulerChoice = schedulerChoices[memoryState][modelState]; + if (schedulerChoice.isDefined()) { + if (!choice.isDefined()) { + ++numOfUndefinedChoices; + } + } else { + if (choice.isDefined()) { + assert(numOfUndefinedChoices > 0); + --numOfUndefinedChoices; + } + } + if (schedulerChoice.isDeterministic()) { + if (!choice.isDeterministic()) { + assert(numOfDeterministicChoices > 0); + --numOfDeterministicChoices; + } + } else { + if (choice.isDeterministic()) { + ++numOfDeterministicChoices; + } + } + + schedulerChoice = choice; + } + + template + void Scheduler::clearChoice(uint_fast64_t modelState, uint_fast64_t memoryState) { + STORM_LOG_ASSERT(memoryState < getNumberOfMemoryStates(), "Illegal memory state index"); + STORM_LOG_ASSERT(modelState < schedulerChoices[memoryState].size(), "Illegal model state index"); + setChoice(SchedulerChoice(), modelState, memoryState); + } + + template + SchedulerChoice const& Scheduler::getChoice(uint_fast64_t modelState, uint_fast64_t memoryState) const { + STORM_LOG_ASSERT(memoryState < getNumberOfMemoryStates(), "Illegal memory state index"); + STORM_LOG_ASSERT(modelState < schedulerChoices[memoryState].size(), "Illegal model state index"); + return schedulerChoices[memoryState][modelState]; + } + + template + bool Scheduler::isPartialScheduler() const { + return numOfUndefinedChoices != 0; + } + + template + bool Scheduler::isDeterministicScheduler() const { + return numOfDeterministicChoices == (schedulerChoices.size() * schedulerChoices.begin()->size()) - numOfUndefinedChoices; + } + + template + bool Scheduler::isMemorylessScheduler() const { + return getNumberOfMemoryStates() == 1; + } + + template + uint_fast64_t Scheduler::getNumberOfMemoryStates() const { + return memoryStructure ? memoryStructure->getNumberOfStates() : 1; + } + + template + void Scheduler::printToStream(std::ostream& out, std::shared_ptr> model, bool skipUniqueChoices) const { + STORM_LOG_THROW(model == nullptr || model->getNumberOfStates() == schedulerChoices.front().size(), storm::exceptions::InvalidOperationException, "The given model is not compatible with this scheduler."); + + bool const stateValuationsGiven = model != nullptr && model->hasStateValuations(); + bool const choiceOriginsGiven = model != nullptr && model->hasChoiceOrigins(); + uint_fast64_t widthOfStates = std::to_string(schedulerChoices.front().size()).length(); + if (stateValuationsGiven) { + widthOfStates += model->getStateValuations().getStateInfo(schedulerChoices.front().size() - 1).length() + 5; + } + widthOfStates = std::max(widthOfStates, 12ull); + uint_fast64_t numOfSkippedStatesWithUniqueChoice = 0; + + out << "___________________________________________________________________" << std::endl; + out << (isPartialScheduler() ? "Partially" : "Fully") << " defined "; + out << (isMemorylessScheduler() ? "memoryless " : ""); + out << (isDeterministicScheduler() ? "deterministic" : "randomized") << " scheduler"; + if (!isMemorylessScheduler()) { + out << " with " << getNumberOfMemoryStates() << " memory states"; + } + out << ":" << std::endl; + STORM_LOG_WARN_COND(!(skipUniqueChoices && model == nullptr), "Can not skip unique choices if the model is not given."); + out << std::setw(widthOfStates) << "model state:" << " " << (isMemorylessScheduler() ? "" : " memory: ") << "choice(s)" << std::endl; + for (uint_fast64_t state = 0; state < schedulerChoices.front().size(); ++state) { + // Check whether the state is skipped + if (skipUniqueChoices && model != nullptr && model->getTransitionMatrix().getRowGroupSize(state) == 1) { + ++numOfSkippedStatesWithUniqueChoice; + continue; + } + + // Print the state info + if (stateValuationsGiven) { + out << std::setw(widthOfStates) << (std::to_string(state) + ": " + model->getStateValuations().getStateInfo(state)); + } else { + out << std::setw(widthOfStates) << state; + } + out << " "; + + bool firstMemoryState = true; + for (uint_fast64_t memoryState = 0; memoryState < getNumberOfMemoryStates(); ++memoryState) { + // Indent if this is not the first memory state + if (firstMemoryState) { + firstMemoryState = false; + } else { + out << std::setw(widthOfStates) << ""; + out << " "; + } + // Print the memory state info + if (!isMemorylessScheduler()) { + out << "m" << std::setw(8) << memoryState; + } + + // Print choice info + SchedulerChoice const& choice = schedulerChoices[memoryState][state]; + if (choice.isDefined()) { + if (choice.isDeterministic()) { + if (choiceOriginsGiven) { + out << model->getChoiceOrigins()->getChoiceInfo(model->getTransitionMatrix().getRowGroupIndices()[state] + choice.getDeterministicChoice()); + } else { + out << choice.getDeterministicChoice(); + } + } else { + bool firstChoice = true; + for (auto const& choiceProbPair : choice.getChoiceAsDistribution()) { + if (firstChoice) { + firstChoice = false; + } else { + out << " + "; + } + out << choiceProbPair.second << ": ("; + if (choiceOriginsGiven) { + out << model->getChoiceOrigins()->getChoiceInfo(model->getTransitionMatrix().getRowGroupIndices()[state] + choiceProbPair.first); + } else { + out << choiceProbPair.first; + } + out << ")"; + } + } + } else { + out << "undefined."; + } + + // Todo: print memory updates + out << std::endl; + } + } + if (numOfSkippedStatesWithUniqueChoice > 0) { + out << "Skipped " << numOfSkippedStatesWithUniqueChoice << " deterministic states with unique choice." << std::endl; + } + out << "___________________________________________________________________" << std::endl; + } + + template class Scheduler; + template class Scheduler; + template class Scheduler; + template class Scheduler; + + } +} \ No newline at end of file diff --git a/src/storm/storage/Scheduler.h b/src/storm/storage/Scheduler.h index a98a6bd50..c1c3a5f88 100644 --- a/src/storm/storage/Scheduler.h +++ b/src/storm/storage/Scheduler.h @@ -2,37 +2,106 @@ #define STORM_STORAGE_SCHEDULER_H_ #include +#include "storm/storage/memorystructure/MemoryStructure.h" +#include "storm/storage/SchedulerChoice.h" namespace storm { namespace storage { /* - * This class is the abstract base class of all scheduler classes. Scheduler classes define which action is - * chosen in a particular state of a non-deterministic model. More concretely, a scheduler maps a state s to i + * This class defines which action is chosen in a particular state of a non-deterministic model. More concretely, a scheduler maps a state s to i * if the scheduler takes the i-th action available in s (i.e. the choices are relative to the states). + * A Choice can be undefined, deterministic */ + template class Scheduler { public: - /* + + /*! + * Initializes a scheduler for the given number of model states. + * + * @param numberOfModelStates number of model states + * @param memoryStructure the considered memory structure. If not given, the scheduler is considered as memoryless. + */ + Scheduler(uint_fast64_t numberOfModelStates, boost::optional const& memoryStructure = boost::none); + Scheduler(uint_fast64_t numberOfModelStates, boost::optional&& memoryStructure); + + /*! * Sets the choice defined by the scheduler for the given state. * - * @param state The state for which to set the choice. * @param choice The choice to set for the given state. + * @param modelState The state of the model for which to set the choice. + * @param memoryState The state of the memoryStructure for which to set the choice. + */ + void setChoice(SchedulerChoice const& choice, uint_fast64_t modelState, uint_fast64_t memoryState = 0); + + /*! + * Clears the choice defined by the scheduler for the given state. + * + * @param modelState The state of the model for which to clear the choice. + * @param memoryState The state of the memoryStructure for which to clear the choice. */ - virtual void setChoice(uint_fast64_t state, uint_fast64_t choice) = 0; + void clearChoice(uint_fast64_t modelState, uint_fast64_t memoryState = 0); - /* - * Retrieves whether this scheduler defines a choice for the given state. + /*! + * Sets the choice defined by the scheduler for the given model and memory state. * - * @param state The state for which to check whether the scheduler defines a choice. - * @return True if the scheduler defines a choice for the given state. + * @param state The state for which to set the choice. + * @param choice The choice to set for the given state. + */ + SchedulerChoice const& getChoice(uint_fast64_t modelState, uint_fast64_t memoryState = 0) const; + + /*! + * Retrieves whether there is a pair of model and memory state for which the choice is undefined. + */ + bool isPartialScheduler() const; + + /*! + * Retrieves whether all defined choices are deterministic */ - virtual bool isChoiceDefined(uint_fast64_t state) const = 0; + bool isDeterministicScheduler() const; /*! - * Retrieves the choice for the given state under the assumption that the scheduler defines a proper choice for the state. + * Retrieves whether the scheduler considers a trivial memory structure (i.e., a memory structure with just a single state) + */ + bool isMemorylessScheduler() const; + + /*! + * Retrieves the number of memory states this scheduler considers. + */ + uint_fast64_t getNumberOfMemoryStates() const; + + /*! + * Returns a copy of this scheduler with the new value type + */ + template + Scheduler toValueType() const { + uint_fast64_t numModelStates = schedulerChoices.front().size(); + Scheduler newScheduler(numModelStates, memoryStructure); + for (uint_fast64_t memState = 0; memState < this->getNumberOfMemoryStates(); ++memState) { + for (uint_fast64_t modelState = 0; modelState < numModelStates; ++modelState) { + newScheduler.setChoice(getChoice(modelState, memState).template toValueType(), modelState, memState); + } + } + return newScheduler; + } + + /*! + * Prints the scheduler to the given output stream. + * @param out The output stream + * @param model If given, provides additional information for printing (e.g., displaying the state valuations instead of state indices) + * @param skipUniqueChoices If true, the (unique) choice for deterministic states (i.e., states with only one enabled choice) is not printed explicitly. + * Requires a model to be given. */ - virtual uint_fast64_t getChoice(uint_fast64_t state) const = 0; + void printToStream(std::ostream& out, std::shared_ptr> model = nullptr, bool skipUniqueChoices = false) const; + + + private: + + boost::optional memoryStructure; + std::vector>> schedulerChoices; + uint_fast64_t numOfUndefinedChoices; + uint_fast64_t numOfDeterministicChoices; }; } } diff --git a/src/storm/storage/SchedulerChoice.cpp b/src/storm/storage/SchedulerChoice.cpp new file mode 100644 index 000000000..c0ab1d793 --- /dev/null +++ b/src/storm/storage/SchedulerChoice.cpp @@ -0,0 +1,82 @@ +#include "storm/storage/SchedulerChoice.h" + +#include "storm/utility/constants.h" +#include "storm/utility/macros.h" + +#include "storm/exceptions/InvalidOperationException.h" +#include "storm/adapters/RationalFunctionAdapter.h" +#include "storm/adapters/RationalNumberAdapter.h" + +namespace storm { + namespace storage { + + + + template + SchedulerChoice::SchedulerChoice() { + // Intentionally left empty + } + + template + SchedulerChoice::SchedulerChoice(uint_fast64_t deterministicChoice) { + distribution.addProbability(deterministicChoice, storm::utility::one()); + } + + template + SchedulerChoice::SchedulerChoice(storm::storage::Distribution const& randomizedChoice) : distribution(randomizedChoice) { + // Intentionally left empty + } + + template + SchedulerChoice::SchedulerChoice(storm::storage::Distribution&& randomizedChoice) : distribution(std::move(randomizedChoice)) { + // Intentionally left empty + } + + template + bool SchedulerChoice::isDefined() const { + return distribution.size() != 0; + } + + template + bool SchedulerChoice::isDeterministic() const { + return distribution.size() == 1; + } + + template + uint_fast64_t SchedulerChoice::getDeterministicChoice() const { + STORM_LOG_THROW(isDeterministic(), storm::exceptions::InvalidOperationException, "Tried to obtain the deterministic choice of a scheduler, but the choice is not deterministic"); + return distribution.begin()->first; + } + + template + storm::storage::Distribution const& SchedulerChoice::getChoiceAsDistribution() const { + return distribution; + } + + template + std::ostream& operator<<(std::ostream& out, SchedulerChoice const& schedulerChoice) { + if (schedulerChoice.isDefined()) { + if (schedulerChoice.isDeterministic()) { + out << schedulerChoice.getDeterministicChoice(); + } else { + out << schedulerChoice.getChoiceAsDistribution(); + } + } else { + out << "undefined"; + } + return out; + } + + template class SchedulerChoice; + template std::ostream& operator<<(std::ostream& out, SchedulerChoice const& schedulerChoice); + template class SchedulerChoice; + template std::ostream& operator<<(std::ostream& out, SchedulerChoice const& schedulerChoice); + template class SchedulerChoice; + template std::ostream& operator<<(std::ostream& out, SchedulerChoice const& schedulerChoice); + template class SchedulerChoice; + template std::ostream& operator<<(std::ostream& out, SchedulerChoice const& schedulerChoice); + + } +} + + diff --git a/src/storm/storage/SchedulerChoice.h b/src/storm/storage/SchedulerChoice.h new file mode 100644 index 000000000..f758e38c6 --- /dev/null +++ b/src/storm/storage/SchedulerChoice.h @@ -0,0 +1,79 @@ +#pragma once + +#include "storm/utility/constants.h" +#include "storm/storage/Distribution.h" + +namespace storm { + namespace storage { + + template + class SchedulerChoice { + + public: + + /*! + * Creates an undefined scheduler choice + */ + SchedulerChoice(); + + /*! + * Creates a deterministic scheduler choice + * @param deterministicChoice the (local) choice index + */ + SchedulerChoice(uint_fast64_t deterministicChoice); + + /*! + * Creates a scheduler choice that potentially considers randomization + * @param randomizedChoice a distribution over the (local) choice indices + */ + SchedulerChoice(storm::storage::Distribution const& randomizedChoice); + + /*! + * Creates a scheduler choice that potentially considers randomization + * @param randomizedChoice a distribution over the (local) choice indices + */ + SchedulerChoice(storm::storage::Distribution&& randomizedChoice); + + /*! + * Returns true iff this scheduler choice is defined + */ + bool isDefined() const; + + /*! + * Returns true iff this scheduler choice is deterministic (i.e., not randomized) + */ + bool isDeterministic() const; + + /*! + * If this choice is deterministic, this function returns the selected (local) choice index. + * Otherwise, an exception is thrown. + */ + uint_fast64_t getDeterministicChoice() const; + + /*! + * Retrieves this choice in the form of a probability distribution. + */ + storm::storage::Distribution const& getChoiceAsDistribution() const; + + /*! + * Changes the value type of this scheduler choice to the given one. + */ + template + SchedulerChoice toValueType() const { + storm::storage::Distribution newDistribution; + for (auto const& stateValuePair : distribution) { + newDistribution.addProbability(stateValuePair.first, storm::utility::convertNumber(stateValuePair.second)); + } + return SchedulerChoice(std::move(newDistribution)); + } + + private: + storm::storage::Distribution distribution; + }; + + template + std::ostream& operator<<(std::ostream& out, SchedulerChoice const& schedulerChoice); + } +} + + diff --git a/src/storm/storage/TotalScheduler.cpp b/src/storm/storage/TotalScheduler.cpp deleted file mode 100644 index 65904222d..000000000 --- a/src/storm/storage/TotalScheduler.cpp +++ /dev/null @@ -1,68 +0,0 @@ -#include "storm/storage/TotalScheduler.h" -#include "storm/exceptions/InvalidArgumentException.h" -#include "storm/utility/Hash.h" -#include "storm/utility/vector.h" - -namespace storm { - namespace storage { - TotalScheduler::TotalScheduler(uint_fast64_t numberOfStates) : choices(numberOfStates) { - // Intentionally left empty. - } - - TotalScheduler::TotalScheduler(std::vector const& choices) : choices(choices) { - // Intentionally left empty. - } - - TotalScheduler::TotalScheduler(std::vector&& choices) : choices(std::move(choices)) { - // Intentionally left empty. - } - - bool TotalScheduler::operator==(storm::storage::TotalScheduler const& other) const { - return this->choices == other.choices; - } - - void TotalScheduler::setChoice(uint_fast64_t state, uint_fast64_t choice) { - if (state > choices.size()) { - throw storm::exceptions::InvalidArgumentException() << "Invalid call to TotalScheduler::setChoice: scheduler cannot not define a choice for state " << state << "."; - } - choices[state] = choice; - } - - bool TotalScheduler::isChoiceDefined(uint_fast64_t state) const { - return state < choices.size(); - } - - uint_fast64_t TotalScheduler::getChoice(uint_fast64_t state) const { - if (state >= choices.size()) { - throw storm::exceptions::InvalidArgumentException() << "Invalid call to TotalScheduler::getChoice: scheduler does not define a choice for state " << state << "."; - } - - return choices[state]; - } - - std::vector const& TotalScheduler::getChoices() const { - return choices; - } - - TotalScheduler TotalScheduler::getSchedulerForSubsystem(storm::storage::BitVector const& subsystem) const { - return TotalScheduler(storm::utility::vector::filterVector(choices, subsystem)); - } - - std::ostream& operator<<(std::ostream& out, TotalScheduler const& scheduler) { - out << "total scheduler (defined on " << scheduler.choices.size() << " states) [ "; - for (uint_fast64_t state = 0; state < scheduler.choices.size() - 1; ++state) { - out << state << " -> " << scheduler.choices[state] << ", "; - } - if (scheduler.choices.size() > 0) { - out << (scheduler.choices.size() - 1) << " -> " << scheduler.choices[scheduler.choices.size() - 1] << " ]"; - } - return out; - } - } -} - -namespace std { - std::size_t hash::operator()(storm::storage::TotalScheduler const& totalScheduler) const { - return storm::utility::Hash::getHash(totalScheduler.choices); - } -} diff --git a/src/storm/storage/TotalScheduler.h b/src/storm/storage/TotalScheduler.h deleted file mode 100644 index d70017b91..000000000 --- a/src/storm/storage/TotalScheduler.h +++ /dev/null @@ -1,78 +0,0 @@ -#ifndef STORM_STORAGE_TOTALSCHEDULER_H_ -#define STORM_STORAGE_TOTALSCHEDULER_H_ - -#include -#include - -#include "storm/storage/Scheduler.h" -#include "storm/storage/BitVector.h" - -namespace storm { - namespace storage { - - class TotalScheduler : public Scheduler { - public: - - TotalScheduler(TotalScheduler const& other) = default; - TotalScheduler(TotalScheduler&& other) = default; - TotalScheduler& operator=(TotalScheduler const& other) = default; - TotalScheduler& operator=(TotalScheduler&& other) = default; - - /*! - * Creates a total scheduler that defines a choice for the given number of states. By default, all choices - * are initialized to zero. - * - * @param numberOfStates The number of states for which the scheduler defines a choice. - */ - TotalScheduler(uint_fast64_t numberOfStates = 0); - - /*! - * Creates a total scheduler that defines the choices for states according to the given vector. - * - * @param choices A vector whose i-th entry defines the choice of state i. - */ - TotalScheduler(std::vector const& choices); - - /*! - * Creates a total scheduler that defines the choices for states according to the given vector. - * - * @param choices A vector whose i-th entry defines the choice of state i. - */ - TotalScheduler(std::vector&& choices); - - bool operator==(TotalScheduler const& other) const; - - void setChoice(uint_fast64_t state, uint_fast64_t choice) override; - - bool isChoiceDefined(uint_fast64_t state) const override; - - uint_fast64_t getChoice(uint_fast64_t state) const override; - - std::vector const& getChoices() const; - - /*! - * Constructs the scheduler for the subsystem indicated by the given BitVector - * - * @param subsystem A BitVector whose i-th entry is true iff state i is part of the subsystem - */ - TotalScheduler getSchedulerForSubsystem(storm::storage::BitVector const& subsystem) const; - - friend std::ostream& operator<<(std::ostream& out, TotalScheduler const& scheduler); - friend struct std::hash; - - private: - // A vector that stores the choice for each state. - std::vector choices; - }; - } // namespace storage -} // namespace storm - - -namespace std { - template <> - struct hash { - std::size_t operator()(storm::storage::TotalScheduler const& totalScheduler) const; - }; -} - -#endif /* STORM_STORAGE_TOTALSCHEDULER_H_ */ diff --git a/src/storm/storage/memorystructure/MemoryStructure.cpp b/src/storm/storage/memorystructure/MemoryStructure.cpp index 69266f562..3d9348c44 100644 --- a/src/storm/storage/memorystructure/MemoryStructure.cpp +++ b/src/storm/storage/memorystructure/MemoryStructure.cpp @@ -11,11 +11,11 @@ namespace storm { namespace storage { - MemoryStructure::MemoryStructure(TransitionMatrix const& transitionMatrix, storm::models::sparse::StateLabeling const& memoryStateLabeling) : transitions(transitionMatrix), stateLabeling(memoryStateLabeling) { + MemoryStructure::MemoryStructure(TransitionMatrix const& transitionMatrix, storm::models::sparse::StateLabeling const& memoryStateLabeling, std::vector const& initialMemoryStates) : transitions(transitionMatrix), stateLabeling(memoryStateLabeling), initialMemoryStates(initialMemoryStates) { // intentionally left empty } - MemoryStructure::MemoryStructure(TransitionMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& memoryStateLabeling) : transitions(std::move(transitionMatrix)), stateLabeling(std::move(memoryStateLabeling)) { + MemoryStructure::MemoryStructure(TransitionMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& memoryStateLabeling, std::vector&& initialMemoryStates) : transitions(std::move(transitionMatrix)), stateLabeling(std::move(memoryStateLabeling)), initialMemoryStates(std::move(initialMemoryStates)) { // intentionally left empty } @@ -27,6 +27,10 @@ namespace storm { return stateLabeling; } + std::vector const& MemoryStructure::getInitialMemoryStates() const { + return initialMemoryStates; + } + uint_fast64_t MemoryStructure::getNumberOfStates() const { return transitions.size(); } @@ -37,7 +41,7 @@ namespace storm { uint_fast64_t resNumStates = lhsNumStates * rhsNumStates; // Transition matrix - TransitionMatrix resultTransitions(resNumStates, std::vector>(resNumStates)); + 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) { @@ -50,7 +54,11 @@ namespace storm { 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); + resStateTransitions[resTransitionTarget] = rhsTransition.get() & lhsTransition.get(); + // If it is not possible to take the considered transition w.r.t. the considered model, we can delete it. + if (resStateTransitions[resTransitionTarget]->empty()) { + resStateTransitions[resTransitionTarget] = boost::none; + } } } } @@ -84,11 +92,18 @@ namespace storm { } resultLabeling.addLabel(rhsLabel, std::move(resLabeledStates)); } - //return MemoryStructure(std::move(resultTransitions), std::move(resultLabeling)); - MemoryStructure res(std::move(resultTransitions), std::move(resultLabeling)); - return res; + // Initial States + std::vector resultInitialMemoryStates; + STORM_LOG_THROW(this->getInitialMemoryStates().size() == rhs.getInitialMemoryStates().size(), storm::exceptions::InvalidOperationException, "Tried to build the product of two memory structures that consider a different number of initial model states."); + resultInitialMemoryStates.reserve(this->getInitialMemoryStates().size()); + auto lhsStateIt = this->getInitialMemoryStates().begin(); + auto rhsStateIt = rhs.getInitialMemoryStates().begin(); + for (; lhsStateIt != this->getInitialMemoryStates().end(); ++lhsStateIt, ++rhsStateIt) { + resultInitialMemoryStates.push_back(*lhsStateIt * rhsNumStates + *rhsStateIt); + } + return MemoryStructure(std::move(resultTransitions), std::move(resultLabeling), std::move(resultInitialMemoryStates)); } template @@ -129,8 +144,6 @@ namespace storm { 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 index 41052c7fa..9df320fd3 100644 --- a/src/storm/storage/memorystructure/MemoryStructure.h +++ b/src/storm/storage/memorystructure/MemoryStructure.h @@ -20,7 +20,7 @@ namespace storm { class MemoryStructure { public: - typedef std::vector>> TransitionMatrix; + typedef std::vector>> TransitionMatrix; /*! * Creates a memory structure with the given transition matrix and the given memory state labeling. @@ -34,11 +34,12 @@ namespace storm { * @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); + MemoryStructure(TransitionMatrix const& transitionMatrix, storm::models::sparse::StateLabeling const& memoryStateLabeling, std::vector const& initialMemoryStates); + MemoryStructure(TransitionMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& memoryStateLabeling, std::vector&& initialMemoryStates); TransitionMatrix const& getTransitionMatrix() const; storm::models::sparse::StateLabeling const& getStateLabeling() const; + std::vector const& getInitialMemoryStates() const; uint_fast64_t getNumberOfStates() const; /*! @@ -60,6 +61,7 @@ namespace storm { private: TransitionMatrix transitions; storm::models::sparse::StateLabeling stateLabeling; + std::vector initialMemoryStates; }; } diff --git a/src/storm/storage/memorystructure/MemoryStructureBuilder.cpp b/src/storm/storage/memorystructure/MemoryStructureBuilder.cpp index b2b654a93..9ee23eaa6 100644 --- a/src/storm/storage/memorystructure/MemoryStructureBuilder.cpp +++ b/src/storm/storage/memorystructure/MemoryStructureBuilder.cpp @@ -1,6 +1,7 @@ #include "storm/storage/memorystructure/MemoryStructureBuilder.h" -#include "storm/logic/FragmentSpecification.h" +#include "storm/models/sparse/Model.h" +#include "storm/storage/BitVector.h" #include "storm/utility/macros.h" #include "storm/exceptions/InvalidOperationException.h" @@ -8,29 +9,83 @@ namespace storm { namespace storage { - MemoryStructureBuilder::MemoryStructureBuilder(uint_fast64_t const& numberOfStates) : transitions(numberOfStates, std::vector>(numberOfStates)), stateLabeling(numberOfStates) { + template + MemoryStructureBuilder::MemoryStructureBuilder(uint_fast64_t numberOfMemoryStates, storm::models::sparse::Model const& model) : model(model), transitions(numberOfMemoryStates, std::vector>(numberOfMemoryStates)), stateLabeling(numberOfMemoryStates), initialMemoryStates(model.getInitialStates().getNumberOfSetBits(), 0) { // Intentionally left empty } + + template + void MemoryStructureBuilder::setInitialMemoryState(uint_fast64_t initialModelState, uint_fast64_t initialMemoryState) { + STORM_LOG_THROW(model.getInitialStates().get(initialModelState), storm::exceptions::InvalidOperationException, "Invalid index of initial model state: " << initialMemoryState << ". This is not an initial state of the model."); + STORM_LOG_THROW(initialMemoryState < transitions.size(), storm::exceptions::InvalidOperationException, "Invalid index of initial memory state: " << initialMemoryState << ". There are only " << transitions.size() << " states in this memory structure."); + + auto initMemStateIt = initialMemoryStates.begin(); + for (auto const& initState : model.getInitialStates()) { + if (initState == initialModelState) { + *initMemStateIt = initialMemoryState; + break; + } + ++initMemStateIt; + } + assert(initMemStateIt != initialMemoryStates.end()); + } + + template + void MemoryStructureBuilder::setTransition(uint_fast64_t const& startState, uint_fast64_t const& goalState, storm::storage::BitVector const& modelStates, boost::optional const& modelChoices) { + + auto const& modelTransitions = model.getTransitionMatrix(); - 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"); + STORM_LOG_THROW(modelStates.size() == modelTransitions.getRowGroupCount(), storm::exceptions::InvalidOperationException, "The modelStates have invalid size."); + STORM_LOG_THROW(!modelChoices || modelChoices->size() == modelTransitions.getRowGroupCount(), storm::exceptions::InvalidOperationException, "The modelChoices have invalid size."); + + // translate the two bitvectors to a single BitVector that indicates the corresponding model transitions. - transitions[startState][goalState] = formula; + storm::storage::BitVector transitionVector(modelTransitions.getEntryCount(), false); + if (modelChoices) { + for (auto const& choice : modelChoices.get()) { + for (auto entryIt = modelTransitions.getRow(choice).begin(); entryIt < modelTransitions.getRow(choice).end(); ++entryIt) { + if (modelStates.get(entryIt->getColumn())) { + transitionVector.set(entryIt - modelTransitions.begin()); + } + } + } + } else { + for (uint_fast64_t choice = 0; choice < modelTransitions.getRowCount(); ++choice) { + for (auto entryIt = modelTransitions.getRow(choice).begin(); entryIt < modelTransitions.getRow(choice).end(); ++entryIt) { + if (modelStates.get(entryIt->getColumn())) { + transitionVector.set(entryIt - modelTransitions.begin()); + } + } + } + } + + // Do not insert the transition if it is never taken. + if (transitionVector.empty()) { + transitions[startState][goalState] = boost::none; + } else { + transitions[startState][goalState] = std::move(transitionVector); + } } - - void MemoryStructureBuilder::setLabel(uint_fast64_t const& state, std::string const& label) { + + template + 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)); + + template + MemoryStructure MemoryStructureBuilder::build() { + return MemoryStructure(std::move(transitions), std::move(stateLabeling), std::move(initialMemoryStates)); } + template class MemoryStructureBuilder; + template class MemoryStructureBuilder; + template class MemoryStructureBuilder; + } } diff --git a/src/storm/storage/memorystructure/MemoryStructureBuilder.h b/src/storm/storage/memorystructure/MemoryStructureBuilder.h index e87992d56..9fbe65c78 100644 --- a/src/storm/storage/memorystructure/MemoryStructureBuilder.h +++ b/src/storm/storage/memorystructure/MemoryStructureBuilder.h @@ -3,44 +3,66 @@ #include #include -#include "storm/logic/Formula.h" #include "storm/models/sparse/StateLabeling.h" +#include "storm/models/sparse/StandardRewardModel.h" #include "storm/storage/memorystructure/MemoryStructure.h" namespace storm { namespace storage { - + template > class MemoryStructureBuilder { public: /*! * Initializes a new builder for a memory structure - * @param numberOfStates The number of states the resulting memory structure should have + * @param numberOfMemoryStates The number of states the resulting memory structure should have */ - MemoryStructureBuilder(uint_fast64_t const& numberOfStates); + MemoryStructureBuilder(uint_fast64_t numberOfMemoryStates, storm::models::sparse::Model const& model); /*! - * Specifies a transition. The formula should be a propositional formula + * Specifies for the given initial state of the model the corresponding initial memory state. + * + * @note The default initial memory state is 0. + * + * @param initialModelState the index of an initial state of the model. + * @param initialMemoryState the initial memory state associated to the corresponding model state. */ - void setTransition(uint_fast64_t const& startState, uint_fast64_t const& goalState, std::shared_ptr formula); - + void setInitialMemoryState(uint_fast64_t initialModelState, uint_fast64_t initialMemoryState); + + /*! + * Specifies a transition of the memory structure. + * The interpretation is that we switch from startState to goalState upon entering one of the specified model states (via one of the specified choices). + * + * @note If it is not possible to move from startState to goalState, such a transition does not have to be set explicitly. + * + * @param startState the memorystate in which the transition starts + * @param goalState the memorystate in which the transition ends + * @param modelStates the model states that trigger this transition. + * @param modelChoices if given, filers the choices of the model that trigger this transition. + * + */ + void setTransition(uint_fast64_t const& startState, uint_fast64_t const& goalState, storm::storage::BitVector const& modelStates, boost::optional const& modelChoices = boost::none); + /*! - * Sets a label to the given state. + * Sets a label to the given memory 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. + * @note When calling this method, the specified transitions should be deterministic and complete, i.e., every triple + * (memoryState, modelChoice, modelState) should uniquely specify a successor memory state. */ MemoryStructure build(); private: + storm::models::sparse::Model const& model; MemoryStructure::TransitionMatrix transitions; storm::models::sparse::StateLabeling stateLabeling; + std::vector initialMemoryStates; }; } diff --git a/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp b/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp index bc4e49782..56b3a6aa0 100644 --- a/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp +++ b/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp @@ -31,11 +31,15 @@ namespace storm { // 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); + auto memoryInitIt = memory.getInitialMemoryStates().begin(); 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); + initialStates.set(modelInit * memoryStateCount + *memoryInitIt, true); + ++memoryInitIt; } + STORM_LOG_ASSERT(memoryInitIt == memory.getInitialMemoryStates().end(), "Unexpected number of initial states."); + 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()); @@ -64,21 +68,18 @@ namespace storm { return toResultStateMapping[modelState * memory.getNumberOfStates() + memoryState]; } - template std::vector SparseModelMemoryProduct::computeMemorySuccessors() const { - uint_fast64_t modelStateCount = model.getNumberOfStates(); + uint_fast64_t modelTransitionCount = model.getTransitionMatrix().getEntryCount(); uint_fast64_t memoryStateCount = memory.getNumberOfStates(); - std::vector result(modelStateCount * memoryStateCount, std::numeric_limits::max()); + std::vector result(modelTransitionCount * 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; + auto const& memoryTransition = memory.getTransitionMatrix()[memoryState][transitionGoal]; + if (memoryTransition) { + for (auto const& modelTransitionIndex : memoryTransition.get()) { + result[modelTransitionIndex * memoryStateCount + memoryState] = transitionGoal; } } } @@ -99,10 +100,12 @@ namespace storm { 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]; + auto const& rowGroup = model.getTransitionMatrix().getRowGroup(modelState); + for (auto modelTransitionIt = rowGroup.begin(); modelTransitionIt != rowGroup.end(); ++modelTransitionIt) { + if (!storm::utility::isZero(modelTransitionIt->getValue())) { + uint_fast64_t successorModelState = modelTransitionIt->getColumn(); + uint_fast64_t modelTransitionId = modelTransitionIt - model.getTransitionMatrix().begin(); + uint_fast64_t successorMemoryState = memorySuccessors[modelTransitionId * memoryStateCount + memoryState]; uint_fast64_t successorStateIndex = successorModelState * memoryStateCount + successorMemoryState; if (!reachableStates.get(successorStateIndex)) { reachableStates.set(successorStateIndex, true); @@ -128,9 +131,11 @@ namespace storm { 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()); + auto const& modelRow = model.getTransitionMatrix().getRow(modelState); + for (auto entryIt = modelRow.begin(); entryIt != modelRow.end(); ++entryIt) { + uint_fast64_t transitionId = entryIt - model.getTransitionMatrix().begin(); + uint_fast64_t const& successorMemoryState = memorySuccessors[transitionId * memoryStateCount + memoryState]; + builder.addNextValue(currentRow, getResultState(entryIt->getColumn(), successorMemoryState), entryIt->getValue()); } ++currentRow; } @@ -158,10 +163,12 @@ namespace storm { 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()); + for (uint_fast64_t modelRowIndex = model.getTransitionMatrix().getRowGroupIndices()[modelState]; modelRowIndex < model.getTransitionMatrix().getRowGroupIndices()[modelState + 1]; ++modelRowIndex) { + auto const& modelRow = model.getTransitionMatrix().getRow(modelRowIndex); + for (auto entryIt = modelRow.begin(); entryIt != modelRow.end(); ++entryIt) { + uint_fast64_t transitionId = entryIt - model.getTransitionMatrix().begin(); + uint_fast64_t const& successorMemoryState = memorySuccessors[transitionId * memoryStateCount + memoryState]; + builder.addNextValue(currentRow, getResultState(entryIt->getColumn(), successorMemoryState), entryIt->getValue()); } ++currentRow; } @@ -268,9 +275,11 @@ namespace storm { 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()); + auto const& rewardMatrixRow = rewardModel.second.getTransitionRewardMatrix().getRow(modelRowIndex); + for (auto entryIt = rewardMatrixRow.begin(); entryIt != rewardMatrixRow.end(); ++entryIt) { + uint_fast64_t transitionId = entryIt - rewardModel.second.getTransitionRewardMatrix().begin(); + uint_fast64_t const& successorMemoryState = memorySuccessors[transitionId * memoryStateCount + memoryState]; + builder.addNextValue(resRowIndex, getResultState(entryIt->getColumn(), successorMemoryState), entryIt->getValue()); } } } diff --git a/src/storm/storage/memorystructure/SparseModelMemoryProduct.h b/src/storm/storage/memorystructure/SparseModelMemoryProduct.h index 170efba3f..0c60923e7 100644 --- a/src/storm/storage/memorystructure/SparseModelMemoryProduct.h +++ b/src/storm/storage/memorystructure/SparseModelMemoryProduct.h @@ -37,8 +37,8 @@ namespace storm { 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 + // Computes for each pair of memory state and model transition index the successor memory state + // The resulting vector maps (modelTransition * memoryStateCount) + memoryState to the corresponding successor state of the memory structure std::vector computeMemorySuccessors() const; // Computes the reachable states of the resulting model diff --git a/src/storm/utility/Stopwatch.cpp b/src/storm/utility/Stopwatch.cpp index faefdb472..0a08a4e19 100644 --- a/src/storm/utility/Stopwatch.cpp +++ b/src/storm/utility/Stopwatch.cpp @@ -43,7 +43,9 @@ namespace storm { } std::ostream& operator<<(std::ostream& out, Stopwatch const& stopwatch) { - out << stopwatch.getTimeInSeconds() << "." << std::setw(3) << std::setfill('0') << (stopwatch.getTimeInMilliseconds() % 1000) << "s"; + char oldFillChar = out.fill('0'); + out << stopwatch.getTimeInSeconds() << "." << std::setw(3) << (stopwatch.getTimeInMilliseconds() % 1000) << "s"; + out.fill(oldFillChar); return out; } diff --git a/src/storm/utility/graph.cpp b/src/storm/utility/graph.cpp index 2cd3360b4..13065000a 100644 --- a/src/storm/utility/graph.cpp +++ b/src/storm/utility/graph.cpp @@ -385,8 +385,7 @@ namespace storm { } template - storm::storage::PartialScheduler computeSchedulerStayingInStates(storm::storage::BitVector const& states, storm::storage::SparseMatrix const& transitionMatrix) { - storm::storage::PartialScheduler result; + void computeSchedulerStayingInStates(storm::storage::BitVector const& states, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::Scheduler& scheduler) { std::vector const& nondeterministicChoiceIndices = transitionMatrix.getRowGroupIndices(); for (auto const& state : states) { @@ -399,18 +398,17 @@ namespace storm { } } if (allSuccessorsInStates) { - result.setChoice(state, choice - nondeterministicChoiceIndices[state]); + for (uint_fast64_t memState = 0; memState < scheduler.getNumberOfMemoryStates(); ++memState) { + scheduler.setChoice(choice - nondeterministicChoiceIndices[state], state, memState); + } break; } } } - - return result; } template - storm::storage::PartialScheduler computeSchedulerWithOneSuccessorInStates(storm::storage::BitVector const& states, storm::storage::SparseMatrix const& transitionMatrix) { - storm::storage::PartialScheduler result; + void computeSchedulerWithOneSuccessorInStates(storm::storage::BitVector const& states, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::Scheduler& scheduler) { std::vector const& nondeterministicChoiceIndices = transitionMatrix.getRowGroupIndices(); for (auto const& state : states) { @@ -423,20 +421,19 @@ namespace storm { } } if (oneSuccessorInStates) { - result.setChoice(state, choice - nondeterministicChoiceIndices[state]); + for (uint_fast64_t memState = 0; memState < scheduler.getNumberOfMemoryStates(); ++memState) { + scheduler.setChoice(choice - nondeterministicChoiceIndices[state], state, memState); + } break; } } } - - return result; } template - storm::storage::PartialScheduler computeSchedulerProbGreater0E(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::optional const& rowFilter) { + void computeSchedulerProbGreater0E(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::Scheduler& scheduler, boost::optional const& rowFilter) { //Perform backwards DFS from psiStates and find a valid choice for each visited state. - storm::storage::PartialScheduler result; std::vector stack; storm::storage::BitVector currentStates(psiStates); //the states that are either psiStates or for which we have found a valid choice. stack.insert(stack.end(), currentStates.begin(), currentStates.end()); @@ -462,7 +459,9 @@ namespace storm { } } if(foundValidChoice){ - result.setChoice(predecessor, row - transitionMatrix.getRowGroupIndices()[predecessor]); + for (uint_fast64_t memState = 0; memState < scheduler.getNumberOfMemoryStates(); ++memState) { + scheduler.setChoice(row - transitionMatrix.getRowGroupIndices()[predecessor], predecessor, memState); + } currentStates.set(predecessor, true); stack.push_back(predecessor); break; @@ -472,18 +471,24 @@ namespace storm { } } } - return result; } template - storm::storage::PartialScheduler computeSchedulerProb0E(storm::storage::BitVector const& prob0EStates, storm::storage::SparseMatrix const& transitionMatrix) { - return computeSchedulerStayingInStates(prob0EStates, transitionMatrix); + void computeSchedulerProb0E(storm::storage::BitVector const& prob0EStates, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::Scheduler& scheduler) { + computeSchedulerStayingInStates(prob0EStates, transitionMatrix, scheduler); } template - storm::storage::PartialScheduler computeSchedulerProb1E(storm::storage::BitVector const& prob1EStates, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + void computeSchedulerProb1E(storm::storage::BitVector const& prob1EStates, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::Scheduler& scheduler) { + + // set an arbitrary choice for the psi states. + for (auto const& psiState : psiStates) { + for (uint_fast64_t memState = 0; memState < scheduler.getNumberOfMemoryStates(); ++memState) { + scheduler.setChoice(0, psiState, memState); + } + } - storm::storage::PartialScheduler result; + // Now perform a backwards search from the psi states and store choices with prob. 1 std::vector const& nondeterministicChoiceIndices = transitionMatrix.getRowGroupIndices(); std::vector stack; storm::storage::BitVector currentStates(psiStates); @@ -513,7 +518,9 @@ namespace storm { // If all successors for a given nondeterministic choice are in the prob1E state set, we // perform a backward search from that state. if (allSuccessorsInProb1EStates && hasSuccessorInCurrentStates) { - result.setChoice(predecessorEntryIt->getColumn(), row - nondeterministicChoiceIndices[predecessorEntryIt->getColumn()]); + for (uint_fast64_t memState = 0; memState < scheduler.getNumberOfMemoryStates(); ++memState) { + scheduler.setChoice(row - nondeterministicChoiceIndices[predecessorEntryIt->getColumn()], predecessorEntryIt->getColumn(), memState); + } currentStates.set(predecessorEntryIt->getColumn(), true); stack.push_back(predecessorEntryIt->getColumn()); break; @@ -522,8 +529,6 @@ namespace storm { } } } - - return result; } template @@ -1309,11 +1314,11 @@ namespace storm { - template storm::storage::PartialScheduler computeSchedulerProbGreater0E(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::optional const& rowFilter); + template void computeSchedulerProbGreater0E(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::Scheduler& scheduler, boost::optional const& rowFilter); - template storm::storage::PartialScheduler computeSchedulerProb0E(storm::storage::BitVector const& prob0EStates, storm::storage::SparseMatrix const& transitionMatrix); + template void computeSchedulerProb0E(storm::storage::BitVector const& prob0EStates, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::Scheduler& scheduler); - template storm::storage::PartialScheduler computeSchedulerProb1E(storm::storage::BitVector const& prob1EStates, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); + template void computeSchedulerProb1E(storm::storage::BitVector const& prob1EStates, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::Scheduler& scheduler); template storm::storage::BitVector performProbGreater0E(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0) ; @@ -1374,11 +1379,11 @@ namespace storm { template std::pair performProb01(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); - template storm::storage::PartialScheduler computeSchedulerProbGreater0E(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::optional const& rowFilter); + template void computeSchedulerProbGreater0E(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::Scheduler& scheduler, boost::optional const& rowFilter); - template storm::storage::PartialScheduler computeSchedulerProb0E(storm::storage::BitVector const& prob0EStates, storm::storage::SparseMatrix const& transitionMatrix); + template void computeSchedulerProb0E(storm::storage::BitVector const& prob0EStates, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::Scheduler& scheduler); - template storm::storage::PartialScheduler computeSchedulerProb1E(storm::storage::BitVector const& prob1EStates, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); + template void computeSchedulerProb1E(storm::storage::BitVector const& prob1EStates, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::Scheduler& scheduler); template storm::storage::BitVector performProbGreater0E(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0) ; diff --git a/src/storm/utility/graph.h b/src/storm/utility/graph.h index 9d6911479..ff8b30287 100644 --- a/src/storm/utility/graph.h +++ b/src/storm/utility/graph.h @@ -7,7 +7,7 @@ #include "storm/utility/OsDetection.h" #include "storm/storage/sparse/StateType.h" -#include "storm/storage/PartialScheduler.h" +#include "storm/storage/Scheduler.h" #include "storm/models/sparse/NondeterministicModel.h" #include "storm/models/sparse/DeterministicModel.h" #include "storm/storage/dd/DdType.h" @@ -245,9 +245,10 @@ namespace storm { * * @param states The set of states for which to compute the scheduler that stays in this very set. * @param transitionMatrix The transition matrix. + * @param scheduler The resulting scheduler. The scheduler is only set at the given states. */ template - storm::storage::PartialScheduler computeSchedulerStayingInStates(storm::storage::BitVector const& states, storm::storage::SparseMatrix const& transitionMatrix); + void computeSchedulerStayingInStates(storm::storage::BitVector const& states, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::Scheduler& scheduler); /*! * Computes a scheduler for the given states that chooses an action that has at least one successor in the @@ -256,9 +257,10 @@ namespace storm { * @param states The set of states for which to compute the scheduler that chooses an action with a successor * in this very set. * @param transitionMatrix The transition matrix. + * @param scheduler The resulting scheduler. The scheduler is only set at the given states. */ template - storm::storage::PartialScheduler computeSchedulerWithOneSuccessorInStates(storm::storage::BitVector const& states, storm::storage::SparseMatrix const& transitionMatrix); + void computeSchedulerWithOneSuccessorInStates(storm::storage::BitVector const& states, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::Scheduler& scheduler); /*! * Computes a scheduler for the ProbGreater0E-States such that in the induced system the given psiStates are reachable via phiStates @@ -268,22 +270,23 @@ namespace storm { * @param phiStates The set of states satisfying phi. * @param psiStates The set of states satisfying psi. * @param rowFilter If given, the returned scheduler will only pick choices such that rowFilter is true for the corresponding matrixrow. - * @return A Scheduler for the ProbGreater0E-States + * @param scheduler The resulting scheduler for the ProbGreater0E-States. The scheduler is not set at prob0A states. * * @note No choice is defined for ProbGreater0E-States if all the probGreater0-choices violate the row filter. * This also holds for states that only reach psi via such states. */ template - storm::storage::PartialScheduler computeSchedulerProbGreater0E(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::optional const& rowFilter = boost::none); + void computeSchedulerProbGreater0E(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::Scheduler& scheduler, boost::optional const& rowFilter = boost::none); /*! * Computes a scheduler for the given states that have a scheduler that has a probability 0. * * @param prob0EStates The states that have a scheduler achieving probablity 0. * @param transitionMatrix The transition matrix of the system. + * @param scheduler The resulting scheduler for the prob0EStates States. The scheduler is not set at probGreater0A states. */ template - storm::storage::PartialScheduler computeSchedulerProb0E(storm::storage::BitVector const& prob0EStates, storm::storage::SparseMatrix const& transitionMatrix); + void computeSchedulerProb0E(storm::storage::BitVector const& prob0EStates, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::Scheduler& scheduler); /*! * Computes a scheduler for the given prob1EStates such that in the induced system the given psiStates are reached with probability 1. @@ -293,10 +296,10 @@ namespace storm { * @param backwardTransitions The reversed transition relation. * @param phiStates The set of states satisfying phi. * @param psiStates The set of states satisfying psi. - * @return A scheduler for the Prob1E-States + * @param scheduler The resulting scheduler for the prob1EStates. The scheduler is not set at the remaining states. */ template - storm::storage::PartialScheduler computeSchedulerProb1E(storm::storage::BitVector const& prob1EStates, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); + void computeSchedulerProb1E(storm::storage::BitVector const& prob1EStates, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::Scheduler& scheduler); /*! * Computes the sets of states that have probability greater 0 of satisfying phi until psi under at least diff --git a/src/test/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp b/src/test/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp index 3a38b9dc4..8ddc74d27 100644 --- a/src/test/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp +++ b/src/test/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp @@ -222,11 +222,11 @@ TEST(GmmxxMdpPrctlModelCheckerTest, SchedulerGeneration) { ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); ASSERT_TRUE(result->asExplicitQuantitativeCheckResult().hasScheduler()); - storm::storage::Scheduler const& scheduler = result->asExplicitQuantitativeCheckResult().getScheduler(); - EXPECT_EQ(0ull, scheduler.getChoice(0)); - EXPECT_EQ(1ull, scheduler.getChoice(1)); - EXPECT_EQ(0ull, scheduler.getChoice(2)); - EXPECT_EQ(0ull, scheduler.getChoice(3)); + storm::storage::Scheduler const& scheduler = result->asExplicitQuantitativeCheckResult().getScheduler(); + EXPECT_EQ(0ull, scheduler.getChoice(0).getDeterministicChoice()); + EXPECT_EQ(1ull, scheduler.getChoice(1).getDeterministicChoice()); + EXPECT_EQ(0ull, scheduler.getChoice(2).getDeterministicChoice()); + EXPECT_EQ(0ull, scheduler.getChoice(3).getDeterministicChoice()); formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"target\"]"); @@ -236,11 +236,11 @@ TEST(GmmxxMdpPrctlModelCheckerTest, SchedulerGeneration) { ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); ASSERT_TRUE(result->asExplicitQuantitativeCheckResult().hasScheduler()); - storm::storage::Scheduler const& scheduler2 = result->asExplicitQuantitativeCheckResult().getScheduler(); - EXPECT_EQ(1ull, scheduler2.getChoice(0)); - EXPECT_EQ(2ull, scheduler2.getChoice(1)); - EXPECT_EQ(0ull, scheduler2.getChoice(2)); - EXPECT_EQ(0ull, scheduler2.getChoice(3)); + storm::storage::Scheduler const& scheduler2 = result->asExplicitQuantitativeCheckResult().getScheduler(); + EXPECT_EQ(1ull, scheduler2.getChoice(0).getDeterministicChoice()); + EXPECT_EQ(2ull, scheduler2.getChoice(1).getDeterministicChoice()); + EXPECT_EQ(0ull, scheduler2.getChoice(2).getDeterministicChoice()); + EXPECT_EQ(0ull, scheduler2.getChoice(3).getDeterministicChoice()); } // Test is currently disabled as the computation of this property requires eliminating the zero-reward MECs, which is diff --git a/src/test/storage/SchedulerTest.cpp b/src/test/storage/SchedulerTest.cpp index 3e157a483..ea4be9402 100644 --- a/src/test/storage/SchedulerTest.cpp +++ b/src/test/storage/SchedulerTest.cpp @@ -1,42 +1,53 @@ #include "gtest/gtest.h" #include "storm-config.h" -#include "storm/exceptions/InvalidArgumentException.h" -#include "storm/storage/PartialScheduler.h" -#include "storm/storage/TotalScheduler.h" +#include "storm/exceptions/InvalidOperationException.h" +#include "storm/storage/Scheduler.h" -TEST(SchedulerTest, PartialScheduler) { - storm::storage::PartialScheduler scheduler; +TEST(SchedulerTest, TotalDeterministicMemorylessScheduler) { + storm::storage::Scheduler scheduler(4); - ASSERT_NO_THROW(scheduler.setChoice(0, 1)); - ASSERT_NO_THROW(scheduler.setChoice(0, 3)); - ASSERT_NO_THROW(scheduler.setChoice(3, 4)); + ASSERT_NO_THROW(scheduler.setChoice(1, 0)); + ASSERT_NO_THROW(scheduler.setChoice(3, 1)); + ASSERT_NO_THROW(scheduler.setChoice(5, 2)); + ASSERT_NO_THROW(scheduler.setChoice(4, 3)); - ASSERT_TRUE(scheduler.isChoiceDefined(0)); - ASSERT_EQ(3ul, scheduler.getChoice(0)); + ASSERT_FALSE(scheduler.isPartialScheduler()); + ASSERT_TRUE(scheduler.isMemorylessScheduler()); + ASSERT_TRUE(scheduler.isDeterministicScheduler()); - ASSERT_TRUE(scheduler.isChoiceDefined(3)); - ASSERT_EQ(4ul, scheduler.getChoice(3)); + ASSERT_TRUE(scheduler.getChoice(0).isDefined()); + ASSERT_EQ(1ul, scheduler.getChoice(0).getDeterministicChoice()); + + ASSERT_TRUE(scheduler.getChoice(1).isDefined()); + ASSERT_EQ(3ul, scheduler.getChoice(1).getDeterministicChoice()); + + ASSERT_TRUE(scheduler.getChoice(2).isDefined()); + ASSERT_EQ(5ul, scheduler.getChoice(2).getDeterministicChoice()); + + ASSERT_TRUE(scheduler.getChoice(3).isDefined()); + ASSERT_EQ(4ul, scheduler.getChoice(3).getDeterministicChoice()); - ASSERT_FALSE(scheduler.isChoiceDefined(1)); - ASSERT_THROW(scheduler.getChoice(1), storm::exceptions::InvalidArgumentException); } -TEST(SchedulerTest, TotalScheduler) { - storm::storage::TotalScheduler scheduler(4); +TEST(SchedulerTest, PartialDeterministicMemorylessScheduler) { + storm::storage::Scheduler scheduler(4); + + ASSERT_NO_THROW(scheduler.setChoice(1, 0)); + ASSERT_NO_THROW(scheduler.setChoice(3, 0)); + ASSERT_NO_THROW(scheduler.setChoice(5, 2)); + ASSERT_NO_THROW(scheduler.setChoice(4, 3)); + ASSERT_NO_THROW(scheduler.clearChoice(2)); - ASSERT_NO_THROW(scheduler.setChoice(0, 1)); - ASSERT_NO_THROW(scheduler.setChoice(0, 3)); - ASSERT_NO_THROW(scheduler.setChoice(3, 4)); + ASSERT_TRUE(scheduler.isPartialScheduler()); + ASSERT_TRUE(scheduler.isMemorylessScheduler()); + ASSERT_TRUE(scheduler.isDeterministicScheduler()); - ASSERT_TRUE(scheduler.isChoiceDefined(0)); - ASSERT_EQ(3ul, scheduler.getChoice(0)); + ASSERT_TRUE(scheduler.getChoice(0).isDefined()); + ASSERT_EQ(3ul, scheduler.getChoice(0).getDeterministicChoice()); - ASSERT_TRUE(scheduler.isChoiceDefined(3)); - ASSERT_EQ(4ul, scheduler.getChoice(3)); + ASSERT_TRUE(scheduler.getChoice(3).isDefined()); + ASSERT_EQ(4ul, scheduler.getChoice(3).getDeterministicChoice()); - ASSERT_TRUE(scheduler.isChoiceDefined(1)); - ASSERT_EQ(0ul, scheduler.getChoice(1)); - - ASSERT_THROW(scheduler.getChoice(4), storm::exceptions::InvalidArgumentException); - ASSERT_THROW(scheduler.setChoice(5, 2), storm::exceptions::InvalidArgumentException); + ASSERT_FALSE(scheduler.getChoice(1).isDefined()); + ASSERT_FALSE(scheduler.getChoice(2).isDefined()); }