diff --git a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp index d0f195604..a1bb1f016 100644 --- a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp +++ b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp @@ -86,18 +86,25 @@ namespace storm { uint_fast64_t infSet = std::get<2>(choice.first); scheduler.setChoice(choice.second, modelState, (automatonState*(_infSets.get().size()+1))+ infSet); + + // TODO: shouldn't happen? + //STORM_LOG_ASSERT(!this->_unreachableStates.get()[(automatonState*(_infSets.get().size()+1))+ infSet].get(modelState), "Tried to set choice for unreachable state."); + } + + /* + for (uint_fast64_t memoryState = 0; this->_unreachableStates.get().size(); ++memoryState) { + for (auto state : this->_unreachableStates.get()[memoryState]) { + // todo fails, memory state = 9 + scheduler.setStateUnreachable(state, memoryState); + } } - // TODO - // set non-reachable (modelState,memoryState)-Pairs (i.e. those that are not contained in _productChoices) to "unreachable", - // also: states that are never reached using the scheduler - // (extend Scheduler by something like std::vector> - // + reachableSchedulerChoices; isChoiceReachable(..)) - // + change definition of partialScheduler/undefinedstates (true if there are undefined states (undefined states are always reachable)) - // + maybe states in trueUpsi are unreachable - // + */ + + // Sanity check for created scheduler. STORM_LOG_ASSERT(scheduler.isDeterministicScheduler(), "Expected a deterministic scheduler"); + STORM_LOG_ASSERT(!scheduler.isPartialScheduler(), "Expected a fully defined scheduler"); return scheduler; } @@ -290,7 +297,6 @@ namespace storm { } - // Define scheduler choices for the states in this MEC (that are not in any other MEC) for (uint_fast64_t id : infSetIds) { // Scheduler that satisfies the MEC acceptance condition (visit each InfSet inf often, or switch to scheduler of another MEC) @@ -311,7 +317,6 @@ namespace storm { // We want to reach the InfSet, save choice: ---> choice this->_productChoices.get().insert({std::make_tuple(product->getModelState(pState), product->getAutomatonState(pState), id), mecScheduler.getChoice(pState)}); } - } } } @@ -441,68 +446,87 @@ namespace storm { // TODO asserts _mecStatesInfSets initialized etc. + // Compute size of the resulting memory structure: a state corresponds to > encoded as (q* (|infSets|+1))+infSet + uint64 numMemoryStates = (da.getNumberOfStates() * (_infSets.get().size()+1)) + _infSets.get().size()+1; //+1 for states outside accECs + + _unreachableStates.emplace(numMemoryStates, storm::storage::BitVector(this->_transitionMatrix.getRowGroupCount(), false)); + + // Extract the choices of the REACH-scheduler (choices to reach an acc. MEC) for the MDP-DA product: -> choice for (storm::storage::sparse::state_type pState : ~acceptingStates) { - // for state not in any accEC ---> choice - // Do not overwrite choices of states in an accepting MEC - this->_productChoices.get().insert({std::make_tuple(product->getModelState(pState), product->getAutomatonState(pState), _infSets.get().size()), prodCheckResult.scheduler->getChoice(pState)}); // For non-accepting states that are not in any accepting EC we use the 'last' copy of the DA - this->_accInfSets.get()[pState] = {this->_infSets.get().size()}; + this->_accInfSets.get()[pState] = {_infSets.get().size()}; + // For state not in any accEC ---> choice. Do not overwrite choices of states in an accepting MEC. + this->_productChoices.get().insert({std::make_tuple(product->getModelState(pState), product->getAutomatonState(pState), _infSets.get().size()), prodCheckResult.scheduler->getChoice(pState)}); + if (!prodCheckResult.scheduler->isStateReachable(pState)) { + //TODO + this->_unreachableStates.get()[(product->getAutomatonState(pState)) * (_infSets.get().size()+1) + _infSets.get().size()].set(product->getModelState(pState)); + } } // Prepare the memory structure. For that, we need: transitions, initialMemoryStates (and memoryStateLabeling) - // Compute size of the resulting memory structure: a state corresponds to > encoded as (q* (|infSets|+1))+infSet - uint64 numMemoryStates = (da.getNumberOfStates() * (_infSets.get().size()+1)) + _infSets.get().size()+1; //+1 for states outside accECs + // The next move function of the memory, will be build based on the transitions of the DA and jumps between InfSets. this->_memoryTransitions.emplace(numMemoryStates, std::vector(numMemoryStates, storm::storage::BitVector(this->_transitionMatrix.getRowGroupCount(), false))); + + for (storm::storage::sparse::state_type automatonFrom = 0; automatonFrom < da.getNumberOfStates(); ++automatonFrom) { for (storm::storage::sparse::state_type automatonTo = 0; automatonTo < da.getNumberOfStates(); ++automatonTo) { // Find the modelStates that trigger this transition. for (storm::storage::sparse::state_type modelState = 0; modelState < this->_transitionMatrix.getRowGroupCount(); ++modelState) { if(!product->isValidProductState(modelState, automatonTo)) { - // Memory state successor of the modelState-transition emanating not defined/reachable. - // TODO save as unreachable in scheduler - //STORM_PRINT("set to unreachable : <" << modelState <<" , " << automatonTo <<">"); + // is not defined in the Product. Thus, considered not reachable for the scheduler. + for (uint_fast64_t infSet = 0; infSet < _infSets.get().size(); ++infSet) { + this->_unreachableStates.get()[ (automatonTo* (_infSets.get().size()+1)) + infSet].set(modelState); + } } else if (automatonTo == productBuilder.getSuccessor(modelState, automatonFrom, modelState)) { //TODO remove first parameter of getSuccessor - // Add the modelState to one outgoing transition of all states of the form (Inf=lenInfSet equals not in MEC) + // Add the modelState to one outgoing transition of all states of the form (Inf=lenInfSet equals not in MEC) // For non-accepting states that are not in any accepting EC we use the 'last' copy of the DA - - // For the accepting states we jump through copies of the DA wrt. the infinity sets. + // and for the accepting states we jump through copies of the DA wrt. the infinity sets. for (uint_fast64_t infSet = 0; infSet < _infSets.get().size()+1; ++infSet) { - // Check if we need to switch the acceptance condition if (_accInfSets.get()[product->getProductStateIndex(modelState, automatonTo)].get().count(infSet) == 0) { // the state is is in a different accepting MEC with a different accepting conjunction of InfSets. auto newInfSet = _accInfSets.get()[product->getProductStateIndex(modelState, automatonTo)].get().begin(); _memoryTransitions.get()[(automatonFrom * (_infSets.get().size()+1)) + infSet][(automatonTo * (_infSets.get().size()+1)) + *newInfSet].set(modelState); + // TODO problem other inf set combis may not be reachable? + // this->_reachableStates.get()[(automatonTo * (_infSets.get().size()+1)) + *newInfSet].set(modelState, true); + } else { // The state is either not in an accepting EC or in an accepting EC that needs to satisfy the infSet. if (infSet == _infSets.get().size() || !(_infSets.get()[infSet].get(product->getProductStateIndex(modelState, automatonTo)))) { // is not in any accepting EC or does not satisfy the InfSet, we stay there. // Add modelState to the transition from to _memoryTransitions.get()[(automatonFrom * (_infSets.get().size()+1)) + infSet][(automatonTo * (_infSets.get().size()+1)) + infSet].set(modelState); + + // TODO problem other inf set combis may not be reachable? + //this->_reachableStates.get()[(automatonTo * (_infSets.get().size()+1)) + infSet].set(modelState, true); + } else { STORM_LOG_ASSERT(_accInfSets.get()[product->getProductStateIndex(modelState, automatonTo)] != boost::none, "The list of InfSets for the product state <" < is undefined."); // satisfies the InfSet, find the next one - auto it = std::find(_accInfSets.get()[product->getProductStateIndex(modelState, automatonTo)].get().begin(), _accInfSets.get()[product->getProductStateIndex(modelState, automatonTo)].get().end(), infSet); - STORM_LOG_ASSERT(it != _accInfSets.get()[product->getProductStateIndex(modelState, automatonTo)].get().end(), "The list of InfSets for the product state <" < does not contain the infSet " << infSet); - it++; - if (it == _accInfSets.get()[product->getProductStateIndex(modelState, automatonTo)].get().end()) { + auto nextInfSet = std::find(_accInfSets.get()[product->getProductStateIndex(modelState, automatonTo)].get().begin(), _accInfSets.get()[product->getProductStateIndex(modelState, automatonTo)].get().end(), infSet); + STORM_LOG_ASSERT(nextInfSet != _accInfSets.get()[product->getProductStateIndex(modelState, automatonTo)].get().end(), "The list of InfSets for the product state <" < does not contain the infSet " << infSet); + nextInfSet++; + if (nextInfSet == _accInfSets.get()[product->getProductStateIndex(modelState, automatonTo)].get().end()) { // Start again. - it = _accInfSets.get()[product->getProductStateIndex(modelState, automatonTo)].get().begin(); + nextInfSet = _accInfSets.get()[product->getProductStateIndex(modelState, automatonTo)].get().begin(); } // Add modelState to the transition from > to >. - _memoryTransitions.get()[(automatonFrom * (_infSets.get().size()+1)) + infSet][(automatonTo * (_infSets.get().size()+1)) + *it].set(modelState); + _memoryTransitions.get()[(automatonFrom * (_infSets.get().size()+1)) + infSet][(automatonTo * (_infSets.get().size()+1)) + *nextInfSet].set(modelState); + + // TODO problem other inf set combis may not be reachable? + // this->_reachableStates.get()[(automatonTo * (_infSets.get().size()+1)) + *nextInfSet].set(modelState, true); } } } diff --git a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h index d60027ade..919efc898 100644 --- a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h +++ b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h @@ -70,7 +70,6 @@ namespace storm { std::vector computeLTLProbabilities(Environment const &env, storm::logic::Formula const& formula, std::map& apSatSets); private: - /*! * Compute a set S of states that admit a probability 1 strategy of satisfying the given acceptance condition (in DNF). * More precisely, let @@ -99,6 +98,7 @@ namespace storm { // scheduler bool _randomScheduler = false; boost::optional, storm::storage::SchedulerChoice>> _productChoices; // ---> ReachChoice and ---> MecChoice + boost::optional> _unreachableStates; // unreachable memory state and model state combinations boost::optional> _infSets; // Save the InfSets of the Acceptance condition. boost::optional>>> _accInfSets; // Save for each product state (which is assigned to an acceptingMEC), the infSets that need to be visited inf often to satisfy the acceptance condition. Remaining states belonging to no accepting EC, are assigned len(_infSets) (REACH scheduler) diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index 9193c8f26..5321960a9 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -609,14 +609,21 @@ namespace storm { // Set values of resulting vector that are known exactly. storm::utility::vector::setVectorValues(result, qualitativeStateSets.statesWithProbability1, storm::utility::one()); + // Check if the values of the maybe states are relevant for the SolveGoal + bool maybeStatesNotRelevant = goal.hasRelevantValues() && goal.relevantValues().isDisjointFrom(qualitativeStateSets.maybeStates); + // If requested, we will produce a scheduler. std::unique_ptr> scheduler; if (produceScheduler) { scheduler = std::make_unique>(transitionMatrix.getRowGroupCount()); - } + // If maybeStatesNotRelevant is true, we have to set the scheduler for maybe states as "unreachable" + if (maybeStatesNotRelevant) { + for (auto state : qualitativeStateSets.maybeStates) { + scheduler->setStateUnreachable(state); + } - // Check if the values of the maybe states are relevant for the SolveGoal - bool maybeStatesNotRelevant = goal.hasRelevantValues() && goal.relevantValues().isDisjointFrom(qualitativeStateSets.maybeStates); + } + } // create multiplier and execute the calculation for 1 additional step auto multiplier = storm::solver::MultiplierFactory().create(env, transitionMatrix); @@ -628,8 +635,6 @@ namespace storm { } } - std::vector maybeStateChoiceValues = std::vector(sizeMaybeStateChoiceValues, storm::utility::zero()); - // TODO: if a scheduler is to be produced and maybestatesNotRelevant is true, we have to set the scheduler for maybsetsates as "unreachable" TODO // Check whether we need to compute exact probabilities for some states. if ((qualitative || maybeStatesNotRelevant) && !goal.isShieldingTask()) { // Set the values for all maybe-states to 0.5 to indicate that their probability values are neither 0 nor 1. diff --git a/src/storm/storage/Scheduler.cpp b/src/storm/storage/Scheduler.cpp index 4dbc1df8f..ab9fc40e3 100644 --- a/src/storm/storage/Scheduler.cpp +++ b/src/storm/storage/Scheduler.cpp @@ -13,41 +13,48 @@ namespace storm { 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)); + reachableStates = std::vector(numOfMemoryStates, storm::storage::BitVector(numberOfModelStates, true)); numOfUndefinedChoices = numOfMemoryStates * numberOfModelStates; numOfDeterministicChoices = 0; + numOfUnreachableStates = 0; } template Scheduler::Scheduler(uint_fast64_t numberOfModelStates, boost::optional&& memoryStructure) : memoryStructure(std::move(memoryStructure)) { uint_fast64_t numOfMemoryStates = this->memoryStructure ? this->memoryStructure->getNumberOfStates() : 1; schedulerChoices = std::vector>>(numOfMemoryStates, std::vector>(numberOfModelStates)); + reachableStates = std::vector(numOfMemoryStates, storm::storage::BitVector(numberOfModelStates, true)); numOfUndefinedChoices = numOfMemoryStates * numberOfModelStates; numOfDeterministicChoices = 0; + numOfUnreachableStates = 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; + if (reachableStates[memoryState].get(modelState)) { + if (schedulerChoice.isDefined()) { + if (!choice.isDefined()) { + ++numOfUndefinedChoices; + } + } else { + if (choice.isDefined()) { + assert(numOfUndefinedChoices > 0); + --numOfUndefinedChoices; + } } - } else { - if (choice.isDeterministic()) { - ++numOfDeterministicChoices; + if (schedulerChoice.isDeterministic()) { + if (!choice.isDeterministic()) { + assert(numOfDeterministicChoices > 0); + --numOfDeterministicChoices; + } + } else { + if (choice.isDeterministic()) { + ++numOfDeterministicChoices; + } } } @@ -79,6 +86,49 @@ namespace storm { return schedulerChoices[memoryState][modelState]; } + template + void Scheduler::setStateUnreachable(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 (reachableStates[memoryState].get(modelState)) { + reachableStates[memoryState].set(modelState, false); + ++numOfUnreachableStates; + + // Choices for unreachable states are not considered undefined or deterministic + if (!schedulerChoice.isDefined()) { + --numOfUndefinedChoices; + } else if (schedulerChoice.isDeterministic()) { + --numOfDeterministicChoices; + } + + } + } + + template + void Scheduler::setStateReachable(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 (!reachableStates[memoryState].get(modelState)) { + reachableStates[memoryState].set(modelState, true); + --numOfUnreachableStates; + + // Choices for unreachable states are not considered undefined or deterministic + if (!schedulerChoice.isDefined()) { + ++numOfUndefinedChoices; + } else if (schedulerChoice.isDeterministic()) { + ++numOfDeterministicChoices; + } + + } + } + + template + bool Scheduler::isStateReachable(uint_fast64_t modelState, uint64_t memoryState) const { + return reachableStates[memoryState].get(modelState); + } + template storm::storage::BitVector Scheduler::computeActionSupport(std::vector const& nondeterministicChoiceIndices) const { auto nrActions = nondeterministicChoiceIndices.back(); @@ -104,7 +154,7 @@ namespace storm { template bool Scheduler::isDeterministicScheduler() const { - return numOfDeterministicChoices == (schedulerChoices.size() * schedulerChoices.begin()->size()) - numOfUndefinedChoices; + return numOfDeterministicChoices == (schedulerChoices.size() * schedulerChoices.begin()->size()) - numOfUndefinedChoices - numOfUnreachableStates; } template @@ -124,6 +174,7 @@ namespace storm { template void Scheduler::printToStream(std::ostream& out, std::shared_ptr> model, bool skipUniqueChoices) const { + // TODO ignore unreachable states 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(); @@ -260,6 +311,7 @@ namespace storm { template void Scheduler::printJsonToStream(std::ostream& out, std::shared_ptr> model, bool skipUniqueChoices) const { + //TODO not defined for memory and unreachable states are not considered STORM_LOG_THROW(model == nullptr || model->getNumberOfStates() == schedulerChoices.front().size(), storm::exceptions::InvalidOperationException, "The given model is not compatible with this scheduler."); STORM_LOG_WARN_COND(!(skipUniqueChoices && model == nullptr), "Can not skip unique choices if the model is not given."); STORM_LOG_THROW(isMemorylessScheduler(), storm::exceptions::NotImplementedException, "Json export of schedulers with memory not implemented."); diff --git a/src/storm/storage/Scheduler.h b/src/storm/storage/Scheduler.h index 5107bb1cf..18e3a8fb7 100644 --- a/src/storm/storage/Scheduler.h +++ b/src/storm/storage/Scheduler.h @@ -60,6 +60,27 @@ namespace storm { */ SchedulerChoice const& getChoice(uint_fast64_t modelState, uint_fast64_t memoryState = 0) const; + /*! + * Set the combination of model state and memoryStructure state to unreachable. + * + * @param modelState The state of the model. + * @param memoryState The state of the memoryStructure. + */ + void setStateUnreachable(uint_fast64_t modelState, uint_fast64_t memoryState = 0); + + /*! + * Set the combination of model state and memoryStructure state to reachable. + * + * @param modelState The state of the model. + * @param memoryState The state of the memoryStructure. + */ + void setStateReachable(uint_fast64_t modelState, uint_fast64_t memoryState = 0); + + /*! + * Is the combination of model state and memoryStructure state to reachable? + */ + bool isStateReachable(uint_fast64_t modelState, uint64_t memoryState = 0) const; + /*! * Compute the Action Support: A bit vector that indicates all actions that are selected with positive probability in some memory state */ diff --git a/src/storm/transformer/DAProductBuilder.h b/src/storm/transformer/DAProductBuilder.h index 7c882b3e8..a6a53f9bd 100644 --- a/src/storm/transformer/DAProductBuilder.h +++ b/src/storm/transformer/DAProductBuilder.h @@ -35,7 +35,7 @@ namespace storm { return da.getSuccessor(da.getInitialState(), getLabelForState(modelState)); } - storm::storage::sparse::state_type getSuccessor(storm::storage::sparse::state_type modelFrom, //TODO delete modelFrom? + storm::storage::sparse::state_type getSuccessor(storm::storage::sparse::state_type modelFrom, storm::storage::sparse::state_type automatonFrom, storm::storage::sparse::state_type modelTo) const { return da.getSuccessor(automatonFrom, getLabelForState(modelTo)); diff --git a/src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp index cddf22db4..0ad528920 100755 --- a/src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp @@ -221,7 +221,7 @@ namespace { storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp); { - tasks[0].setOnlyInitialStatesRelevant(true); // TODO for false, but need equivalent inducedModel state for model state + tasks[0].setOnlyInitialStatesRelevant(true); auto result = checker.check(this->env(), tasks[0]); ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); EXPECT_NEAR(this->parseNumber("81/100"), result->template asExplicitQuantitativeCheckResult()[*mdp->getInitialStates().begin()],storm::settings::getModule().getPrecision()); @@ -244,7 +244,7 @@ namespace { EXPECT_NEAR(this->parseNumber("81/100"), inducedResult->template asExplicitQuantitativeCheckResult()[*inducedMdp->getInitialStates().begin()],storm::settings::getModule().getPrecision()); } { - tasks[1].setOnlyInitialStatesRelevant(true); + tasks[1].setOnlyInitialStatesRelevant(false); auto result = checker.check(this->env(), tasks[1]); ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); EXPECT_NEAR(this->parseNumber("1/2"), result->template asExplicitQuantitativeCheckResult()[*mdp->getInitialStates().begin()],storm::settings::getModule().getPrecision()); @@ -258,7 +258,7 @@ namespace { ASSERT_EQ(inducedModel->getType(), storm::models::ModelType::Mdp); auto const &inducedMdp = inducedModel->template as>(); EXPECT_EQ(inducedMdp->getNumberOfChoices(), inducedMdp->getNumberOfStates()); - storm::modelchecker::SparseMdpPrctlModelChecker> inducedChecker( *inducedMdp); + storm::modelchecker::SparseMdpPrctlModelChecker> inducedChecker(*inducedMdp); auto inducedResult = inducedChecker.check(this->env(), tasks[1]); ASSERT_TRUE(inducedResult->isExplicitQuantitativeCheckResult()); EXPECT_NEAR(this->parseNumber("1/2"),inducedResult->template asExplicitQuantitativeCheckResult()[*inducedMdp->getInitialStates().begin()],storm::settings::getModule().getPrecision());