From c80a62ce0694710bbbbbe2bddc59b0b5d0715c85 Mon Sep 17 00:00:00 2001 From: hannah Date: Tue, 27 Jul 2021 21:35:48 +0200 Subject: [PATCH] added function for computation of memory states --- .../helper/ltl/SparseLTLHelper.cpp | 39 ++++++++++--------- .../modelchecker/helper/ltl/SparseLTLHelper.h | 17 ++++++-- 2 files changed, 34 insertions(+), 22 deletions(-) diff --git a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp index 527cb3868..7bf56ce4c 100644 --- a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp +++ b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp @@ -27,6 +27,10 @@ namespace storm { // Intentionally left empty. } + template + uint_fast64_t SparseLTLHelper::SparseLTLHelper::getMemoryState(uint_fast64_t daState, uint_fast64_t infSet) { + return (daState * (_infSets.get().size()+1))+ infSet; + } template storm::storage::Scheduler SparseLTLHelper::SparseLTLHelper::extractScheduler(storm::models::sparse::Model const& model) { @@ -51,7 +55,7 @@ namespace storm { // Create a memory structure for the MDP scheduler with memory. If hasRelevantStates is set, we only consider initial model states relevant. auto memoryBuilder = storm::storage::MemoryStructureBuilder(this->_memoryTransitions.get().size(), model, this->hasRelevantStates()); - // Build the transitions between the memory states: startState--- modelStates (transitionVector) --->goalState + // Build the transitions between the memory states: startState to goalState using modelStates (transitionVector). for (storm::storage::sparse::state_type startState = 0; startState < this->_memoryTransitions.get().size(); ++startState) { for (storm::storage::sparse::state_type goalState = 0; goalState < this->_memoryTransitions.get().size(); ++goalState) { // Bitvector that represents modelStates the model states that trigger this transition. @@ -59,7 +63,7 @@ namespace storm { } } - // initialMemoryStates: Assign an initial memory state model states + // InitialMemoryStates: Assign an initial memory state model states if (this->hasRelevantStates()) { // Only consider initial model states for (uint_fast64_t modelState : model.getInitialStates()) { @@ -82,13 +86,13 @@ namespace storm { for (const auto &choice : this->_producedChoices.get()) { // -> choice storm::storage::sparse::state_type modelState = std::get<0>(choice.first); - storm::storage::sparse::state_type automatonState = std::get<1>(choice.first); + storm::storage::sparse::state_type daState = std::get<1>(choice.first); uint_fast64_t infSet = std::get<2>(choice.first); - STORM_LOG_ASSERT(!this->_dontCareStates.get()[(automatonState*(_infSets.get().size()+1))+ infSet].get(modelState), "Tried to set choice for dontCare state."); - scheduler.setChoice(choice.second, modelState, (automatonState*(_infSets.get().size()+1))+ infSet); + STORM_LOG_ASSERT(!this->_dontCareStates.get()[getMemoryState(daState, infSet)].get(modelState), "Tried to set choice for dontCare state."); + scheduler.setChoice(choice.second, modelState, getMemoryState(daState, infSet)); } - // Set "don't care" states + // Set "dontCare" states for (uint_fast64_t memoryState = 0; memoryState < this->_dontCareStates.get().size(); ++memoryState) { for (auto state : this->_dontCareStates.get()[memoryState]) { scheduler.setDontCare(state, memoryState); @@ -219,7 +223,7 @@ namespace storm { } } else if (atom.getType() == cpphoafparser::AtomAcceptance::TEMPORAL_FIN) { - // do only sanity checks here + // Do only sanity checks here. STORM_LOG_ASSERT(atom.isNegated() ? !mec.containsAnyState(~accSet) : !mec.containsAnyState(accSet), "MEC contains Fin-states, which should have been removed"); } } @@ -241,7 +245,7 @@ namespace storm { mecStates.set(stateChoicePair.first); } - // We know the MEC satisfied the conjunction: Save InfSets + // We know the MEC satisfied the conjunction: Save InfSets. std::set infSetIds; for (auto const& literal : conjunction) { storm::storage::BitVector infSet; @@ -359,7 +363,7 @@ namespace storm { if (!product->isValidProductState(modelState, automatonState)) { // If the state does not occur in the product model, all the infSet combinations are irrelevant for the scheduler. for (uint_fast64_t infSet = 0; infSet < _infSets.get().size()+1; ++infSet) { - _dontCareStates.get()[automatonState * (_infSets.get().size() + 1) + infSet].set(modelState, true); + _dontCareStates.get()[getMemoryState(automatonState, infSet)].set(modelState, true); } } else { auto pState = product->getProductStateIndex(modelState, automatonState); @@ -367,7 +371,7 @@ namespace storm { // For states in accepting ECs set the missing MEC-scheduler combinations are "dontCare", they are not reachable using the scheduler choices. //TODO is this correct? for (uint_fast64_t infSet = 0; infSet < _infSets.get().size()+1; ++infSet) { if (_producedChoices.get().find(std::make_tuple(product->getModelState(pState), product->getAutomatonState(pState), infSet)) == _producedChoices.get().end() ) { - _dontCareStates.get()[(product->getAutomatonState(pState)) * (_infSets.get().size()+1) + infSet].set(product->getModelState(pState), true); + _dontCareStates.get()[getMemoryState(product->getAutomatonState(pState), infSet)].set(product->getModelState(pState), true); } } @@ -376,14 +380,14 @@ namespace storm { this->_accInfSets.get()[pState] = {_infSets.get().size()}; if (reachScheduler->isDontCare(pState)) { // Mark the maybe States of the untilProbability scheduler as "dontCare" - _dontCareStates.get()[(product->getAutomatonState(pState)) * (_infSets.get().size()+1) + _infSets.get().size()].set(product->getModelState(pState), true); + _dontCareStates.get()[getMemoryState(product->getAutomatonState(pState), _infSets.get().size())].set(product->getModelState(pState), true); } else { // Set choice For non-accepting states that are not in any accepting EC this->_producedChoices.get().insert({std::make_tuple(product->getModelState(pState),product->getAutomatonState(pState),_infSets.get().size()),reachScheduler->getChoice(pState)}); }; // All other InfSet combinations are unreachable (dontCare) for (uint_fast64_t infSet = 0; infSet < _infSets.get().size(); ++infSet) { - _dontCareStates.get()[(product->getAutomatonState(pState)) * (_infSets.get().size()+1) + infSet].set(product->getModelState(pState), true); + _dontCareStates.get()[getMemoryState(product->getAutomatonState(pState), infSet)].set(product->getModelState(pState), true); } } @@ -411,14 +415,14 @@ namespace storm { 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); + _memoryTransitions.get()[getMemoryState(automatonFrom, infSet)][getMemoryState(automatonTo, *newInfSet)].set(modelState); } else { // Continue looking for any accepting EC (if we haven't reached one yet) or stay in the corresponding accepting EC, test whether we have reached the next 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); + _memoryTransitions.get()[getMemoryState(automatonFrom, infSet)][getMemoryState(automatonTo, infSet)].set(modelState); } else { STORM_LOG_ASSERT(_accInfSets.get()[product->getProductStateIndex(modelState, automatonTo)] != boost::none, "The list of InfSets for the product state <" < is undefined."); @@ -431,7 +435,7 @@ namespace storm { 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)) + *nextInfSet].set(modelState); + _memoryTransitions.get()[getMemoryState(automatonFrom, infSet)][getMemoryState(automatonTo, *nextInfSet)].set(modelState); } } } @@ -452,14 +456,13 @@ namespace storm { STORM_LOG_ASSERT(_accInfSets.get()[product->getProductStateIndex(modelState, automatonState)] != boost::none, "The list of InfSets for the product state <" < is undefined."); // If is an accepting state start in the first InfSet of . auto infSet = _accInfSets.get()[product->getProductStateIndex(modelState, automatonState)].get().begin(); - _memoryInitialStates.get()[modelState] = (automatonState * (_infSets.get().size()+1)) + *infSet; + _memoryInitialStates.get()[modelState] = getMemoryState(automatonState, *infSet); } else { - _memoryInitialStates.get()[modelState] = (automatonState * (_infSets.get().size()+1)) + _infSets.get().size(); + _memoryInitialStates.get()[modelState] = getMemoryState(automatonState, _infSets.get().size()); } } - // Finished creation of initial states. } diff --git a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h index 3d7c21abe..82d81c598 100644 --- a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h +++ b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h @@ -93,13 +93,22 @@ namespace storm { /** * Helper function, extracts scheduler choices and creates the memory structure for the LTL-Scheduler. - * @param - * @param - * @param the scheduler enuring to reach some acceptingState, defined on the model-DA product - * @param + * @param number of DA-states + * @param states in accepting end components of the model-DA product + * @param the scheduler ensuring to reach some acceptingState, defined on the model-DA product + * @param the product builder + * @param the model-DA product + * @param relevant states of the model */ void prepareScheduler(uint_fast64_t numDaStates, storm::storage::BitVector const& acceptingProductStates, std::unique_ptr> reachScheduler, transformer::DAProductBuilder const& productBuilder, typename transformer::DAProduct::ptr product, storm::storage::BitVector const& modelStatesOfInterest); + /** + * Helper function, computes the memory state for a given DA-state and infSet ID. + * Encoded as (DA-state * (numberOfInfSets+1)) + infSet. (+1 because an additional "copy" of the DA is used for states outside accepting ECs) + * @param DA-state + * @param infSet ID + */ + uint_fast64_t getMemoryState(uint_fast64_t daState, uint_fast64_t infSet); storm::storage::SparseMatrix const& _transitionMatrix;