diff --git a/src/storm/modelchecker/helper/ltl/internal/SparseLTLSchedulerHelper.cpp b/src/storm/modelchecker/helper/ltl/internal/SparseLTLSchedulerHelper.cpp index 03db6d7ba..b4a599634 100644 --- a/src/storm/modelchecker/helper/ltl/internal/SparseLTLSchedulerHelper.cpp +++ b/src/storm/modelchecker/helper/ltl/internal/SparseLTLSchedulerHelper.cpp @@ -12,14 +12,38 @@ namespace storm { namespace internal { template - SparseLTLSchedulerHelper::SparseLTLSchedulerHelper(uint_fast64_t numProductStates) : _randomScheduler(false), _producedChoices(), _infSets(), _accInfSets(numProductStates, boost::none) { + const uint_fast64_t SparseLTLSchedulerHelper::DEFAULT_INFSET = 0; + + template + uint_fast64_t SparseLTLSchedulerHelper::InfSetPool::getOrCreateIndex(storm::storage::BitVector&& infSet) { + auto it = std::find(_storage.begin(), _storage.end(), infSet); + if (it == _storage.end()) { + _storage.push_back(std::move(infSet)); + return _storage.size() - 1; + } else { + return distance(_storage.begin(), it); + } + } + + template + storm::storage::BitVector const& SparseLTLSchedulerHelper::InfSetPool::get(uint_fast64_t index) const { + STORM_LOG_ASSERT(index < size(), "inf set index " << index << " is invalid."); + return _storage[index]; + } + + template + uint_fast64_t SparseLTLSchedulerHelper::InfSetPool::size() const { + return _storage.size(); + } + + template + SparseLTLSchedulerHelper::SparseLTLSchedulerHelper(uint_fast64_t numProductStates) : _randomScheduler(false), _accInfSets(numProductStates, boost::none) { // Intentionally left empty. } - template uint_fast64_t SparseLTLSchedulerHelper::SparseLTLSchedulerHelper::getMemoryState(uint_fast64_t daState, uint_fast64_t infSet) { - return (daState * (_infSets.size()+1))+ infSet; + return (daState * _infSets.size())+ infSet; } template @@ -29,79 +53,94 @@ namespace storm { template void SparseLTLSchedulerHelper::saveProductEcChoices(automata::AcceptanceCondition const& acceptance, storm::storage::MaximalEndComponent const& mec, std::vector const& conjunction, typename transformer::DAProduct::ptr product) { - // Save all states contained in this MEC + // Save all states contained in this MEC and find out whether there is some overlap with another, already processed accepting mec storm::storage::BitVector mecStates(product->getProductModel().getNumberOfStates(), false); + storm::storage::BitVector overlapStates; + for (auto const &stateChoicePair : mec) { - mecStates.set(stateChoicePair.first); + if (_accInfSets[stateChoicePair.first].is_initialized()) { + overlapStates.resize(product->getProductModel().getNumberOfStates(), false); + overlapStates.set(stateChoicePair.first); + } else { + mecStates.set(stateChoicePair.first); + } } - - // We know the MEC satisfied the conjunction: Save InfSets. - std::set infSetIds; - for (auto const& literal : conjunction) { - storm::storage::BitVector infSet; - if (literal->isTRUE()) { - // All states - infSet = storm::storage::BitVector(product->getProductModel().getNumberOfStates(), true); - - } else if (literal->isAtom()) { - const cpphoafparser::AtomAcceptance &atom = literal->getAtom(); - if (atom.getType() == cpphoafparser::AtomAcceptance::TEMPORAL_INF) { - if (atom.isNegated()) { - infSet = ~acceptance.getAcceptanceSet(atom.getAcceptanceSet()); - - } else { - infSet = acceptance.getAcceptanceSet(atom.getAcceptanceSet()); - } + + if (!overlapStates.empty()) { + // If all the states in mec are overlapping, we are done already. + if (!mecStates.empty()) { + // Simply Reach the overlapStates almost surely + // set inf sets + for (auto mecState : mecStates) { + STORM_LOG_ASSERT(!_accInfSets[mecState].is_initialized(), "accepting inf sets were already defined for a MEC state which is not expected."); + _accInfSets[mecState] = std::set({DEFAULT_INFSET}); } - else if (atom.getType() == cpphoafparser::AtomAcceptance::TEMPORAL_FIN) { - // If there are FinSets in the conjunction we use the InfSet containing all states in this MEC - infSet = mecStates; + + // Define scheduler choices for the states in this MEC (that are not in any other MEC) + // Compute a scheduler that, with prob=1 reaches the overlap states + storm::storage::Scheduler mecScheduler(product->getProductModel().getNumberOfStates()); + storm::utility::graph::computeSchedulerProb1E(mecStates, product->getProductModel().getTransitionMatrix(), product->getProductModel().getBackwardTransitions(), mecStates, overlapStates, mecScheduler); + + // Extract scheduler choices + for (auto pState : mecStates) { + this->_producedChoices.insert({std::make_tuple(product->getModelState(pState), product->getAutomatonState(pState), DEFAULT_INFSET), mecScheduler.getChoice(pState)}); } } - - // Save new InfSets - if (infSet.size() > 0) { - auto it = std::find(_infSets.begin(), _infSets.end(), infSet); - if (it == _infSets.end()) { - infSetIds.insert(_infSets.size()); - _infSets.emplace_back(infSet); - } else { - // save ID for accCond of the MEC states - infSetIds.insert(distance(_infSets.begin(), it)); + } else { + // No overlap! Let's do actual work. + + // We know the MEC satisfied the conjunction: Save InfSets. + std::set infSetIds; + for (auto const& literal : conjunction) { + if (literal->isAtom()) { + const cpphoafparser::AtomAcceptance &atom = literal->getAtom(); + if (atom.getType() == cpphoafparser::AtomAcceptance::TEMPORAL_INF) { + storm::storage::BitVector infSet; + if (atom.isNegated()) { + infSet = ~acceptance.getAcceptanceSet(atom.getAcceptanceSet()); + } else { + infSet = acceptance.getAcceptanceSet(atom.getAcceptanceSet()); + } + // Save new InfSet + infSetIds.insert(_infSets.getOrCreateIndex(std::move(infSet))); + } + // A TEMPORAL_FIN atom can be ignored at this point since the mec is already known to only contain "allowed" states } + // TRUE literals can be ignored since those will be satisfied anyway + // FALSE literals are not possible here since the MEC is known to be accepting. } - } - - // Save the InfSets into the _accInfSets for states in this MEC, but only if there weren't assigned to any other MEC yet. - storm::storage::BitVector newMecStates(product->getProductModel().getNumberOfStates(), false); - for (auto const &stateChoicePair : mec) { - - if (_accInfSets[stateChoicePair.first] == boost::none) { - // state wasn't assigned to any other MEC yet. - _accInfSets[stateChoicePair.first].emplace(infSetIds); - newMecStates.set(stateChoicePair.first); + if (infSetIds.empty()) { + // There might not be any infSet at this point (e.g. because all literals are TEMPORAL_FIN atoms). We need at least one infset, though + infSetIds.insert(_infSets.getOrCreateIndex(storm::storage::BitVector(product->getProductModel().getNumberOfStates(), true))); } - } - - - // 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) - storm::storage::Scheduler mecScheduler(product->getProductModel().getNumberOfStates()); - - // States not in InfSet: Compute a scheduler that, with prob=1, reaches the infSet via mecStates starting from states that are not yet in other MEC - storm::utility::graph::computeSchedulerProb1E(newMecStates, product->getProductModel().getTransitionMatrix(), product->getProductModel().getBackwardTransitions(), mecStates, _infSets[id] & mecStates, mecScheduler); - - // States that already reached the InfSet - for (auto pState : (newMecStates & _infSets[id])) { - // Prob1E sets an arbitrary choice for the psi states, but we want to stay in this accepting MEC. - mecScheduler.setChoice(*mec.getChoicesForState(pState).begin() - product->getProductModel().getTransitionMatrix().getRowGroupIndices()[pState], pState); + + // Save the InfSets into the _accInfSets for states in this MEC + for (auto const &mecState : mecStates) { + STORM_LOG_ASSERT(!_accInfSets[mecState].is_initialized(), "accepting inf sets were already defined for a MEC state which is not expected."); + _accInfSets[mecState].emplace(infSetIds); } - - // Extract scheduler choices (only for states that are already assigned a scheduler, i.e are in another MEC) - for (auto pState : newMecStates) { - // We want to reach the InfSet, save choice: ---> choice - this->_producedChoices.insert({std::make_tuple(product->getModelState(pState), product->getAutomatonState(pState), id), mecScheduler.getChoice(pState)}); + + // Define scheduler choices for the states in this MEC (that are not in any other MEC) + // The resulting scheduler will visit each InfSet inf often + for (uint_fast64_t id : infSetIds) { + // Scheduler that satisfies the MEC acceptance condition + storm::storage::Scheduler mecScheduler(product->getProductModel().getNumberOfStates()); + + storm::storage::BitVector infStatesWithinMec = _infSets.get(id) & mecStates; + // States not in InfSet: Compute a scheduler that, with prob=1, reaches the infSet via mecStates + storm::utility::graph::computeSchedulerProb1E(mecStates, product->getProductModel().getTransitionMatrix(), product->getProductModel().getBackwardTransitions(), mecStates, infStatesWithinMec, mecScheduler); + + // States that already reached the InfSet + for (auto pState : infStatesWithinMec) { + // Prob1E sets an arbitrary choice for the psi states, but we want to stay in this accepting MEC. + mecScheduler.setChoice(*mec.getChoicesForState(pState).begin() - product->getProductModel().getTransitionMatrix().getRowGroupIndices()[pState], pState); + } + + // Extract scheduler choices + for (auto pState : mecStates) { + // We want to reach the InfSet, save choice: ---> choice + this->_producedChoices.insert({std::make_tuple(product->getModelState(pState), product->getAutomatonState(pState), id), mecScheduler.getChoice(pState)}); + } } } } @@ -109,8 +148,10 @@ namespace storm { template void SparseLTLSchedulerHelper::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, storm::storage::SparseMatrix const& transitionMatrix) { - // Compute size of the resulting memory structure: A state is encoded as (q* (|infSets|+1))+ |infSet| - uint64 numMemoryStates = (numDaStates) * (_infSets.size()+1); //+1 for states outside accECs + STORM_LOG_ASSERT(_infSets.size() > 0, "There is no inf set. Were the accepting ECs processed before?"); + + // Compute size of the resulting memory structure: A state is encoded as (q* (|infSets|))+ |infSet| + uint64 numMemoryStates = (numDaStates) * (_infSets.size()); _dontCareStates = std::vector(numMemoryStates, storm::storage::BitVector(transitionMatrix.getRowGroupCount(), false)); // Set choices for states or consider them "dontCare" @@ -119,40 +160,39 @@ 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.size()+1; ++infSet) { + for (uint_fast64_t infSet = 0; infSet < _infSets.size(); ++infSet) { _dontCareStates[getMemoryState(automatonState, infSet)].set(modelState, true); } } else { auto pState = product->getProductStateIndex(modelState, automatonState); if (acceptingProductStates.get(pState)) { - // For states in accepting ECs set the missing MEC-scheduler combinations are "dontCare", they are not reachable using the scheduler choices. - for (uint_fast64_t infSet = 0; infSet < _infSets.size()+1; ++infSet) { - if (_producedChoices.find(std::make_tuple(product->getModelState(pState), product->getAutomatonState(pState), infSet)) == _producedChoices.end() ) { + // For states in accepting ECs set the MEC-scheduler. Missing combinations are "dontCare", they are not reachable using the scheduler choices. + for (uint_fast64_t infSet = 0; infSet < _infSets.size(); ++infSet) { + if (_producedChoices.count(std::make_tuple(product->getModelState(pState), product->getAutomatonState(pState), infSet)) == 0 ) { _dontCareStates[getMemoryState(product->getAutomatonState(pState), infSet)].set(product->getModelState(pState), true); } } } else { - // Extract the choices of the REACH-scheduler (choices to reach an acc. MEC) for the MDP-DA product: -> choice. The memory structure corresponds to the "last" copy of the DA (_infSets.get().size()). - this->_accInfSets[pState] = std::set({_infSets.size()}); + // Extract the choices of the REACH-scheduler (choices to reach an acc. MEC) for the MDP-DA product: -> choice. The memory structure corresponds to the "0th" copy of the DA (DEFAULT_INFSET). + this->_accInfSets[pState] = std::set({DEFAULT_INFSET}); if (reachScheduler->isDontCare(pState)) { // Mark the maybe States of the untilProbability scheduler as "dontCare" - _dontCareStates[getMemoryState(product->getAutomatonState(pState), _infSets.size())].set(product->getModelState(pState), true); + _dontCareStates[getMemoryState(product->getAutomatonState(pState), DEFAULT_INFSET)].set(product->getModelState(pState), true); } else { // Set choice For non-accepting states that are not in any accepting EC - this->_producedChoices.insert({std::make_tuple(product->getModelState(pState),product->getAutomatonState(pState),_infSets.size()),reachScheduler->getChoice(pState)}); + this->_producedChoices.insert({std::make_tuple(product->getModelState(pState), product->getAutomatonState(pState), DEFAULT_INFSET), reachScheduler->getChoice(pState)}); }; // All other InfSet combinations are unreachable (dontCare) - for (uint_fast64_t infSet = 0; infSet < _infSets.size(); ++infSet) { + static_assert(DEFAULT_INFSET == 0, "This code assumes that the default infset is 0"); + for (uint_fast64_t infSet = 1; infSet < _infSets.size(); ++infSet) { _dontCareStates[getMemoryState(product->getAutomatonState(pState), infSet)].set(product->getModelState(pState), true); - } } } } } - // Prepare the memory structure. For that, we need: transitions, initialMemoryStates (and memoryStateLabeling) // The next move function of the memory, will be build based on the transitions of the DA and jumps between InfSets. @@ -162,42 +202,37 @@ namespace storm { uint_fast64_t automatonTo = productBuilder.getSuccessor(automatonFrom, modelState); if (product->isValidProductState(modelState, automatonTo)) { - // 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 - // and for the accepting states we jump through copies of the DA wrt. the infinity sets. - for (uint_fast64_t infSet = 0; infSet < _infSets.size()+1; ++infSet) { - // Check if we need to switch the acceptance condition - STORM_LOG_ASSERT(_accInfSets[product->getProductStateIndex(modelState, automatonTo)] != boost::none, "The list of InfSets for the product state <" < is undefined."); - - if (_accInfSets[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[product->getProductStateIndex(modelState, automatonTo)].get().begin(); - _memoryTransitions[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.size() || !(_infSets[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[getMemoryState(automatonFrom, infSet)][getMemoryState(automatonTo, infSet)].set(modelState); - - } else { - STORM_LOG_ASSERT(_accInfSets[product->getProductStateIndex(modelState, automatonTo)] != boost::none, "The list of InfSets for the product state <" < is undefined."); - // satisfies the InfSet, find the next one. - auto nextInfSet = std::find(_accInfSets[product->getProductStateIndex(modelState, automatonTo)].get().begin(), _accInfSets[product->getProductStateIndex(modelState, automatonTo)].get().end(), infSet); - STORM_LOG_ASSERT(nextInfSet != _accInfSets[product->getProductStateIndex(modelState, automatonTo)].get().end(), "The list of InfSets for the product state <" < does not contain the infSet " << infSet); - nextInfSet++; - if (nextInfSet == _accInfSets[product->getProductStateIndex(modelState, automatonTo)].get().end()) { - // Start again. - nextInfSet = _accInfSets[product->getProductStateIndex(modelState, automatonTo)].get().begin(); - } - // Add modelState to the transition from > to >. - _memoryTransitions[getMemoryState(automatonFrom, infSet)][getMemoryState(automatonTo, *nextInfSet)].set(modelState); + uint_fast64_t daProductState = product->getProductStateIndex(modelState, automatonTo); + STORM_LOG_ASSERT(_accInfSets[daProductState] != boost::none, "The list of InfSets for the product state <" < is undefined."); + std::set const& daProductStateInfSets = _accInfSets[daProductState].get(); + // Add the modelState to one outgoing transition of all states of the form + // For non-accepting states that are not in any accepting EC and for overlapping accepting ECs we always use the '0th' copy of the DA. + // For the states in accepting ECs that do not overlap we cycle through copies 0,1,2, ... k of the DA (skipping copies whose inf-sets are not needed for the accepting EC). + for (uint_fast64_t currentInfSet = 0; currentInfSet < _infSets.size(); ++currentInfSet) { + uint_fast64_t newInfSet; + // Check if we need to switch the inf set (i.e. the DA copy) + if (daProductStateInfSets.count(currentInfSet) == 0) { + // This infSet is not relevant for the daProductState. We need to switch to a copy representing a relevant infset. + newInfSet = *daProductStateInfSets.begin(); + } else if (daProductStateInfSets.size() > 1 && (_infSets.get(currentInfSet).get(daProductState))) { + // We have reached a state from the current infSet and thus need to move on to the next infSet in the list. + // Note that if the list contains just a single item, the switch would have no effect. + // In particular, this is the case for states that are not in an accepting MEC as those only have DEFAULT_INFSET in their list + auto nextInfSetIt = daProductStateInfSets.find(currentInfSet); + STORM_LOG_ASSERT(nextInfSetIt != daProductStateInfSets.end(), "The list of InfSets for the product state <" < does not contain the infSet " << currentInfSet); + nextInfSetIt++; + if (nextInfSetIt == daProductStateInfSets.end()) { + // Start again. + nextInfSetIt = daProductStateInfSets.begin(); } + newInfSet = *nextInfSetIt; + } else { + // In all other cases we can keep the current inf set (i.e. the DA copy) + newInfSet = currentInfSet; } + _memoryTransitions[getMemoryState(automatonFrom, currentInfSet)][getMemoryState(automatonTo, newInfSet)].set(modelState); } } - } } // Finished creation of transitions. @@ -208,21 +243,13 @@ namespace storm { for (storm::storage::sparse::state_type modelState : modelStatesOfInterest) { storm::storage::sparse::state_type automatonState = productBuilder.getInitialState(modelState); STORM_LOG_ASSERT(product->isValidProductState(modelState, automatonState), "The memory successor state for the model state "<< modelState << "does not exist in the DA-Model Product."); - if (acceptingProductStates[product->getProductStateIndex(modelState, automatonState)]) { - STORM_LOG_ASSERT(_accInfSets[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[product->getProductStateIndex(modelState, automatonState)].get().begin(); - _memoryInitialStates[modelState] = getMemoryState(automatonState, *infSet); - - } else { - _memoryInitialStates[modelState] = getMemoryState(automatonState, _infSets.size()); - } - + STORM_LOG_ASSERT(_accInfSets[product->getProductStateIndex(modelState, automatonState)] != boost::none, "The list of InfSets for the product state <" < is undefined."); + // Start in the first InfSet of + auto infSet = _accInfSets[product->getProductStateIndex(modelState, automatonState)].get().begin(); + _memoryInitialStates[modelState] = getMemoryState(automatonState, *infSet); } - } - template storm::storage::Scheduler SparseLTLSchedulerHelper::SparseLTLSchedulerHelper::extractScheduler(storm::models::sparse::Model const& model, bool onlyInitialStatesRelevant) { diff --git a/src/storm/modelchecker/helper/ltl/internal/SparseLTLSchedulerHelper.h b/src/storm/modelchecker/helper/ltl/internal/SparseLTLSchedulerHelper.h index 89f5075c0..5f22a698a 100644 --- a/src/storm/modelchecker/helper/ltl/internal/SparseLTLSchedulerHelper.h +++ b/src/storm/modelchecker/helper/ltl/internal/SparseLTLSchedulerHelper.h @@ -38,13 +38,16 @@ namespace storm { void setRandom(); /*! - * Save choices for states in the accepting end component of the DA-Model product, - * but only set new choices for states that are not in any other EC yet. + * Save choices for states in the accepting end component of the DA-Model product. * We know the EC satisfies the given conjunction of the acceptance condition. Therefore, we want to reach each infinity set in the conjunction infinitely often. * Choices are of the Form -> choice. * + * @note The given end component might overlap with another accepting EC (that potentially satisfies another conjunction of the DNF-acceptance condition). + * If this is the case, this method will set a scheduler under which the states of the overlapping EC are reached almost surely. + * This method only sets new choices for states that are not in any other accepting EC (yet). + * * @param acceptance the acceptance condition (in DNF) - * @param mec the accepting end component + * @param mec the accepting end component which shall only contain states that can be visited infinitely often (without violating the acc cond.) * @param conjunction the conjunction satisfied by the end component * @param product the product model */ @@ -53,6 +56,8 @@ namespace storm { /*! * Extracts scheduler choices and creates the memory structure for the LTL-Scheduler. * + * @pre saveProductEcChoices has been called on some mec before, in particular there must be at least one accepting product state. + * * @param numDaStates number of DA-states * @param acceptingProductStates states in accepting end components of the model-DA product * @param reachScheduler the scheduler ensuring to reach some acceptingState, defined on the model-DA product @@ -82,13 +87,44 @@ namespace storm { * @param infSet infSet ID */ uint_fast64_t getMemoryState(uint_fast64_t daState, uint_fast64_t infSet); - - + + + /*! + * Manages the InfSets of the acceptance condition by maintaining an assignment from infSets to unique indices + * An infSet is a BitVector that encodes the product model states that are contained in the infSet + */ + class InfSetPool { + public: + InfSetPool() = default; + + /*! + * If the given infSet has been seen before, the corresponding index is returned. Otherwise, a new index is assigned to the infset. + * Indices are assigned in a consecutive way starting from 0 + */ + uint_fast64_t getOrCreateIndex(storm::storage::BitVector&& infSet); + /*! + * Gets the inf set from the given index. + * @param index + * @return + */ + storm::storage::BitVector const& get(uint_fast64_t index) const; + + /*! + * @return The current number of stored infSets (which coincides with the index of the most recently added infSet (or 0 if there is none) + */ + uint_fast64_t size() const; + + private: + std::vector _storage; + } _infSets; + + static const uint_fast64_t DEFAULT_INFSET; /// Some arbitrary fixed infset index that will be used e.g. for states that are not in any accepting EC + bool _randomScheduler; - std::map , storm::storage::SchedulerChoice> _producedChoices; // -> ReachChoice and -> MecChoice std::vector _dontCareStates; // memorySate-modelState combinations that are never visited - std::vector _infSets; // Save the InfSets of the acceptance condition. The BitVector contains the product model states that are contained in the infSet + std::map , storm::storage::SchedulerChoice> _producedChoices; // -> ReachChoice and -> MecChoice + std::vector>> _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) // Memory structure