From 6af47eaadcea0cb7d40087d7c0339f16d931ed3b Mon Sep 17 00:00:00 2001 From: hannah Date: Thu, 12 Aug 2021 12:45:59 +0200 Subject: [PATCH] new class for scheduler computation during LTL-MC --- .../helper/ltl/SparseLTLHelper.cpp | 296 +---------------- .../modelchecker/helper/ltl/SparseLTLHelper.h | 65 +--- .../ltl/internal/SparseLTLSchedulerHelper.cpp | 308 ++++++++++++++++++ .../ltl/internal/SparseLTLSchedulerHelper.h | 102 ++++++ 4 files changed, 445 insertions(+), 326 deletions(-) create mode 100644 src/storm/modelchecker/helper/ltl/internal/SparseLTLSchedulerHelper.cpp create mode 100644 src/storm/modelchecker/helper/ltl/internal/SparseLTLSchedulerHelper.h diff --git a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp index 151e3892e..2c01f8c4b 100644 --- a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp +++ b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp @@ -12,10 +12,8 @@ #include "storm/storage/StronglyConnectedComponentDecomposition.h" #include "storm/storage/MaximalEndComponentDecomposition.h" -#include "storm/storage/memorystructure/MemoryStructure.h" -#include "storm/storage/memorystructure/MemoryStructureBuilder.h" #include "storm/solver/SolveGoal.h" -#include "storm/utility/graph.h" + #include "storm/exceptions/InvalidPropertyException.h" @@ -25,90 +23,19 @@ namespace storm { namespace helper { template - SparseLTLHelper::SparseLTLHelper(storm::storage::SparseMatrix const& transitionMatrix) : _transitionMatrix(transitionMatrix){ + SparseLTLHelper::SparseLTLHelper(storm::storage::SparseMatrix const& transitionMatrix) : _transitionMatrix(transitionMatrix) { // 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) { STORM_LOG_ASSERT(this->isProduceSchedulerSet(), "Trying to get the produced optimal choices although no scheduler was requested."); - // If Pmax(phi) = 0 or Pmin(phi) = 1, we return a memoryless scheduler with arbitrary choices - if (_randomScheduler) { - storm::storage::Scheduler scheduler(this->_transitionMatrix.getRowGroupCount()); - for (storm::storage::sparse::state_type state = 0; state < this->_transitionMatrix.getRowGroupCount(); ++state) { - scheduler.setChoice(0, state); - - } - return scheduler; - } - - // Otherwise, we compute a scheduler with memory. - STORM_LOG_ASSERT(this->_producedChoices.is_initialized(), "Trying to extract the produced scheduler but none is available. Was there a computation call before?"); - STORM_LOG_ASSERT(this->_memoryTransitions.is_initialized(), "Trying to extract the DA transition structure but none is available. Was there a computation call before?"); - STORM_LOG_ASSERT(this->_memoryInitialStates.is_initialized(), "Trying to extract the initial states of the DA but there are none available. Was there a computation call before?"); - STORM_LOG_ASSERT(this->_dontCareStates.is_initialized(), "Trying to extract the Scheduler-dontCare states but there are none available. Was there a computation call before?"); - - - // 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 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. - memoryBuilder.setTransition(startState, goalState, this->_memoryTransitions.get()[startState][goalState]); - } - } - - // InitialMemoryStates: Assign an initial memory state model states - if (this->hasRelevantStates()) { - // Only consider initial model states - for (uint_fast64_t modelState : model.getInitialStates()) { - memoryBuilder.setInitialMemoryState(modelState, this->_memoryInitialStates.get()[modelState]); - } - } else { - // All model states are relevant - for (uint_fast64_t modelState = 0; modelState < model.getNumberOfStates(); ++modelState) { - memoryBuilder.setInitialMemoryState(modelState, this->_memoryInitialStates.get()[modelState]); - } - } - - // Build the memoryStructure. - storm::storage::MemoryStructure memoryStructure = memoryBuilder.build(); - - // Create a scheduler (with memory) for the model from the REACH and MEC scheduler of the MDP-DA-product model. - storm::storage::Scheduler scheduler(this->_transitionMatrix.getRowGroupCount(), memoryStructure); - - // Use choices in the product model to create a choice based on model state and memory state - for (const auto &choice : this->_producedChoices.get()) { - // -> choice - storm::storage::sparse::state_type modelState = std::get<0>(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()[getMemoryState(daState, infSet)].get(modelState), "Tried to set choice for dontCare state."); - scheduler.setChoice(choice.second, modelState, getMemoryState(daState, infSet)); - } - - // 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); - } - } - - // 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; + STORM_LOG_ASSERT(this->_schedulerHelper.is_initialized(), "Trying to get the produced optimal choices but none were available. Was there a computation call before?"); + return this->_schedulerHelper.get().extractScheduler(model, this->hasRelevantStates()); } + template std::vector SparseLTLHelper::computeLTLProbabilities(Environment const &env, storm::logic::PathFormula const& formula, CheckFormulaCallback const& formulaChecker) { // Replace state-subformulae by atomic propositions (APs) @@ -156,11 +83,6 @@ namespace storm { std::size_t accMECs = 0; std::size_t allMECs = 0; - if (this->isProduceSchedulerSet()) { - _infSets.emplace(); - _accInfSets.emplace(product->getProductModel().getNumberOfStates(), boost::none); - _producedChoices.emplace(); - } for (auto const& conjunction : dnf) { // Determine the set of states of the subMDP that can satisfy the condition, remove all states that would violate Fins in the conjunction. @@ -238,82 +160,9 @@ namespace storm { } if (this->isProduceSchedulerSet()) { + // save choices for states that weren't assigned to any other MEC yet. + this->_schedulerHelper.get().saveProductEcChoices(acceptance, mec, conjunction, product); - // Save all states contained in this MEC - storm::storage::BitVector mecStates(transitionMatrix.getRowGroupCount(), false); - for (auto const &stateChoicePair : mec) { - 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(transitionMatrix.getRowGroupCount(), 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()); - } - } - 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; - } - } - - // Save new InfSets - if (infSet.size() > 0) { - auto it = std::find(_infSets.get().begin(), _infSets.get().end(), infSet); - if (it == _infSets.get().end()) { - infSetIds.insert(_infSets.get().size()); - _infSets.get().emplace_back(infSet); - } else { - // save ID for accCond of the MEC states - infSetIds.insert(distance(_infSets.get().begin(), it)); - } - } - } - - // 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(transitionMatrix.getRowGroupCount(), false); - for (auto const &stateChoicePair : mec) { - if (_accInfSets.get()[stateChoicePair.first] == boost::none) { - // state wasn't assigned to any other MEC yet. - _accInfSets.get()[stateChoicePair.first].emplace(infSetIds); - newMecStates.set(stateChoicePair.first); - - } - } - - - // 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(transitionMatrix.getRowGroupCount()); - - // 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, transitionMatrix, backwardTransitions, mecStates, _infSets.get()[id] & mecStates, mecScheduler); - - // States that already reached the InfSet - for (auto pState : (newMecStates & _infSets.get()[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() - transitionMatrix.getRowGroupIndices()[pState], pState); - } - - // 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.get().insert({std::make_tuple(product->getModelState(pState), product->getAutomatonState(pState), id), mecScheduler.getChoice(pState)}); - } - } } } @@ -345,125 +194,6 @@ namespace storm { return acceptingStates; } - template - void SparseLTLHelper::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_LOG_ASSERT(this->_producedChoices.is_initialized(), "Trying to extract the produced scheduler but none is available. Was there a computation call before?"); - STORM_LOG_ASSERT(this->_infSets.is_initialized(), "Was there a computation call before?"); - STORM_LOG_ASSERT(this->_accInfSets.is_initialized(), "Was there a computation call before?"); - - // Compute size of the resulting memory structure: A state is encoded as (q* (|infSets|+1))+ |infSet| - uint64 numMemoryStates = (numDaStates) * (_infSets.get().size()+1); //+1 for states outside accECs - _dontCareStates.emplace(numMemoryStates, storm::storage::BitVector(this->_transitionMatrix.getRowGroupCount(), false)); - - // Set choices for states or consider them "dontCare" - for (storm::storage::sparse::state_type automatonState= 0; automatonState < numDaStates; ++automatonState) { - for (storm::storage::sparse::state_type modelState = 0; modelState < this->_transitionMatrix.getRowGroupCount(); ++modelState) { - - 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()[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. //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()[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.get()[pState] = std::set({_infSets.get().size()}); - if (reachScheduler->isDontCare(pState)) { - // Mark the maybe States of the untilProbability scheduler as "dontCare" - _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()[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. - _memoryTransitions.emplace(numMemoryStates, std::vector(numMemoryStates, storm::storage::BitVector(_transitionMatrix.getRowGroupCount(), false))); - for (storm::storage::sparse::state_type automatonFrom = 0; automatonFrom < numDaStates; ++automatonFrom) { - for (storm::storage::sparse::state_type modelState = 0; modelState < _transitionMatrix.getRowGroupCount(); ++modelState) { - 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.get().size()+1; ++infSet) { - // Check if we need to switch the acceptance condition - STORM_LOG_ASSERT(_accInfSets.get()[product->getProductStateIndex(modelState, automatonTo)] != boost::none, "The list of InfSets for the product state <" < is undefined."); - - 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()[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()[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."); - // satisfies the InfSet, find the next one. - 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. - nextInfSet = _accInfSets.get()[product->getProductStateIndex(modelState, automatonTo)].get().begin(); - } - // Add modelState to the transition from > to >. - _memoryTransitions.get()[getMemoryState(automatonFrom, infSet)][getMemoryState(automatonTo, *nextInfSet)].set(modelState); - } - } - } - } - - } - } - // Finished creation of transitions. - - // Find initial memory states - this->_memoryInitialStates.emplace(); - this->_memoryInitialStates->resize(this->_transitionMatrix.getRowGroupCount()); - // Save for each relevant model state its initial memory state (get the s-successor q of q0) - 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.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] = getMemoryState(automatonState, *infSet); - - } else { - _memoryInitialStates.get()[modelState] = getMemoryState(automatonState, _infSets.get().size()); - } - - } - - } template std::vector SparseLTLHelper::computeDAProductProbabilities(Environment const& env, storm::automata::DeterministicAutomaton const& da, std::map& apSatSets) { @@ -497,6 +227,12 @@ namespace storm { STORM_LOG_INFO("Product "+ (Nondeterministic ? std::string("MDP-DA") : std::string("DTMC-DA")) +" has " << product->getProductModel().getNumberOfStates() << " states and " << product->getProductModel().getNumberOfTransitions() << " transitions."); + // Prepare scheduler + if (this->isProduceSchedulerSet()) { + STORM_LOG_THROW(Nondeterministic, storm::exceptions::InvalidOperationException, "Scheduler export only supported for nondeterministic models."); + this->_schedulerHelper.emplace(product->getProductModel().getNumberOfStates()); + } + // Compute accepting states storm::storage::BitVector acceptingStates; if (Nondeterministic) { @@ -511,8 +247,10 @@ namespace storm { if (acceptingStates.empty()) { STORM_LOG_INFO("No accepting states, skipping probability computation."); + if (this->isProduceSchedulerSet()) { + this->_schedulerHelper.get().setRandom(); + } std::vector numericResult(this->_transitionMatrix.getRowGroupCount(), storm::utility::zero()); - this->_randomScheduler = true; return numericResult; } @@ -546,7 +284,7 @@ namespace storm { prodNumericResult = std::move(prodCheckResult.values); if (this->isProduceSchedulerSet()) { - prepareScheduler(da.getNumberOfStates(), acceptingStates, std::move(prodCheckResult.scheduler), productBuilder, product, statesOfInterest); + this->_schedulerHelper.get().prepareScheduler(da.getNumberOfStates(), acceptingStates, std::move(prodCheckResult.scheduler), productBuilder, product, statesOfInterest, this->_transitionMatrix); } } else { diff --git a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h index 5a46b4bc9..ff19e475c 100644 --- a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h +++ b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h @@ -1,7 +1,8 @@ #include "storm/modelchecker/helper/SingleValueModelCheckerHelper.h" +#include "storm/modelchecker/helper/ltl/internal/SparseLTLSchedulerHelper.h" + #include "storm/storage/SparseMatrix.h" -#include "storm/storage/Scheduler.h" #include "storm/models/sparse/Dtmc.h" #include "storm/models/sparse/Mdp.h" #include "storm/transformer/DAProductBuilder.h" @@ -25,7 +26,7 @@ namespace storm { /*! * Helper class for LTL model checking * @tparam ValueType the type a value can have - * @tparam Nondeterministic true if there is nondeterminism in the Model (MDP) + * @tparam Nondeterministic A flag indicating if there is nondeterminism in the Model (MDP) */ template class SparseLTLHelper: public SingleValueModelCheckerHelper { @@ -35,30 +36,28 @@ namespace storm { typedef std::function CheckFormulaCallback; /*! - * The type of the product automaton (DTMC or MDP) that is used during the computation. + * The type of the product model (DTMC or MDP) that is used during the computation. */ using productModelType = typename std::conditional, storm::models::sparse::Dtmc>::type; /*! * Initializes the helper for a discrete time model (i.e. DTMC, MDP) - * @param the transition matrix of the model - * @param the number of states of the model + * @param transitionMatrix the transition matrix of the model */ SparseLTLHelper(storm::storage::SparseMatrix const& transitionMatrix); /*! * @pre before calling this, a computation call should have been performed during which scheduler production was enabled. - * @param the model + * @param model the model * @return a new scheduler containing optimal choices for each state that yield the long run average values of the most recent call. */ storm::storage::Scheduler extractScheduler(storm::models::sparse::Model const& model); /*! * Computes the LTL probabilities - * @param the LTL formula (allowing PCTL* like nesting) - * @param formulaChecker lambda that evaluates sub-formulas checks the provided formula and returns the set of states in which the formula holds - * @param the atomic propositions occuring in the formula together with the satisfaction sets + * @param formula the LTL formula (allowing PCTL* like nesting) + * @param formulaChecker lambda that evaluates sub-formulas checks the provided formula and returns the set of states in which the formula holds< * @return a value for each state */ std::vector computeLTLProbabilities(Environment const &env, storm::logic::PathFormula const& formula, CheckFormulaCallback const& formulaChecker); @@ -73,9 +72,8 @@ namespace storm { /*! * Computes the (maximizing) probabilities for the constructed DA product - * @param the DA to build the product with - * @param the atomic propositions and satisfaction sets - * @param a flag indicating whether qualitative model checking is performed + * @param da the DA to build the product with + * @param apSatSets the atomic propositions and satisfaction sets * @return a value for each state */ std::vector computeDAProductProbabilities(Environment const& env, storm::automata::DeterministicAutomaton const& da, std::map& apSatSets); @@ -97,50 +95,23 @@ namespace storm { * P1acc be the set of states that satisfy Pmax=1[ F accEC ]. * This function then computes a set that contains accEC and is contained by P1acc. * However, if the acceptance condition consists of 'true', the whole state space can be returned. - * @param the acceptance condition (in DNF) - * @param the transition matrix of the model - * @param the reversed transition relation + * @param acceptance the acceptance condition (in DNF) + * @param transitionMatrix the transition matrix of the model + * @param backwardTransitions the reversed transition relation */ storm::storage::BitVector computeAcceptingECs(automata::AcceptanceCondition const& acceptance, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, typename transformer::DAProduct::ptr product); - /** + /*! * Computes a set S of states that are contained in BSCCs that satisfy the given acceptance conditon. - * @param the acceptance condition - * @param the transition matrix of the model + * @param acceptance the acceptance condition + * @param transitionMatrix the transition matrix of the model */ storm::storage::BitVector computeAcceptingBCCs(automata::AcceptanceCondition const& acceptance, storm::storage::SparseMatrix const& transitionMatrix); - /** - * Helper function, extracts scheduler choices and creates the memory structure for the LTL-Scheduler. - * @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; - - // scheduler - bool _randomScheduler = false; - boost::optional, storm::storage::SchedulerChoice>> _producedChoices; // ---> ReachChoice and ---> MecChoice - boost::optional> _dontCareStates; // memory state combinations that are never visited - - 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) - // Memory structure - boost::optional>> _memoryTransitions; // The BitVector contains the model states that lead from startState to . This is deterministic, because each state is assigned to a unique MEC (scheduler). - boost::optional> _memoryInitialStates; // Save for each relevant state (initial or all) s its unique initial memory state (which memory state is reached from the initial state after reading s) + + boost::optional> _schedulerHelper; }; } diff --git a/src/storm/modelchecker/helper/ltl/internal/SparseLTLSchedulerHelper.cpp b/src/storm/modelchecker/helper/ltl/internal/SparseLTLSchedulerHelper.cpp new file mode 100644 index 000000000..03db6d7ba --- /dev/null +++ b/src/storm/modelchecker/helper/ltl/internal/SparseLTLSchedulerHelper.cpp @@ -0,0 +1,308 @@ +#include "SparseLTLSchedulerHelper.h" +#include "storm/storage/memorystructure/MemoryStructure.h" +#include "storm/storage/memorystructure/MemoryStructureBuilder.h" +#include "storm/transformer/DAProductBuilder.h" + +#include "storm/utility/graph.h" + + +namespace storm { + namespace modelchecker { + namespace helper { + namespace internal { + + template + SparseLTLSchedulerHelper::SparseLTLSchedulerHelper(uint_fast64_t numProductStates) : _randomScheduler(false), _producedChoices(), _infSets(), _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; + } + + template + void SparseLTLSchedulerHelper::SparseLTLSchedulerHelper::setRandom() { + this->_randomScheduler = true; + } + + 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 + storm::storage::BitVector mecStates(product->getProductModel().getNumberOfStates(), false); + for (auto const &stateChoicePair : mec) { + 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()); + } + } + 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; + } + } + + // 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)); + } + } + } + + // 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); + } + } + + + // 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); + } + + // 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)}); + } + } + } + + + 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 + _dontCareStates = std::vector(numMemoryStates, storm::storage::BitVector(transitionMatrix.getRowGroupCount(), false)); + + // Set choices for states or consider them "dontCare" + for (storm::storage::sparse::state_type automatonState= 0; automatonState < numDaStates; ++automatonState) { + for (storm::storage::sparse::state_type modelState = 0; modelState < transitionMatrix.getRowGroupCount(); ++modelState) { + + 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) { + _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() ) { + _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()}); + 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); + } 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)}); + }; + // All other InfSet combinations are unreachable (dontCare) + for (uint_fast64_t infSet = 0; 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. + _memoryTransitions = std::vector>(numMemoryStates, std::vector(numMemoryStates, storm::storage::BitVector(transitionMatrix.getRowGroupCount(), false))); + for (storm::storage::sparse::state_type automatonFrom = 0; automatonFrom < numDaStates; ++automatonFrom) { + for (storm::storage::sparse::state_type modelState = 0; modelState < transitionMatrix.getRowGroupCount(); ++modelState) { + 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); + } + } + } + } + + } + } + // Finished creation of transitions. + + // Find initial memory states + this->_memoryInitialStates = std::vector(transitionMatrix.getRowGroupCount()); + // Save for each relevant model state its initial memory state (get the s-successor q of q0) + 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()); + } + + } + + } + + + template + storm::storage::Scheduler SparseLTLSchedulerHelper::SparseLTLSchedulerHelper::extractScheduler(storm::models::sparse::Model const& model, bool onlyInitialStatesRelevant) { + + if (_randomScheduler) { + storm::storage::Scheduler scheduler(model.getNumberOfStates()); + for (storm::storage::sparse::state_type state = 0; state < model.getNumberOfStates(); ++state) { + scheduler.setChoice(0, state); + + } + return scheduler; + } + + // Otherwise, we compute a scheduler with memory. + + // 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.size(), model, onlyInitialStatesRelevant); + + // Build the transitions between the memory states: startState to goalState using modelStates (transitionVector). + for (storm::storage::sparse::state_type startState = 0; startState < this->_memoryTransitions.size(); ++startState) { + for (storm::storage::sparse::state_type goalState = 0; goalState < this->_memoryTransitions.size(); ++goalState) { + // Bitvector that represents modelStates the model states that trigger this transition. + memoryBuilder.setTransition(startState, goalState, this->_memoryTransitions[startState][goalState]); + } + } + + // InitialMemoryStates: Assign an initial memory state model states + if (onlyInitialStatesRelevant) { + // Only consider initial model states + for (uint_fast64_t modelState : model.getInitialStates()) { + memoryBuilder.setInitialMemoryState(modelState, this->_memoryInitialStates[modelState]); + } + } else { + // All model states are relevant + for (uint_fast64_t modelState = 0; modelState < model.getNumberOfStates(); ++modelState) { + memoryBuilder.setInitialMemoryState(modelState, this->_memoryInitialStates[modelState]); + } + } + + // Build the memoryStructure. + storm::storage::MemoryStructure memoryStructure = memoryBuilder.build(); + + // Create a scheduler (with memory) for the model from the REACH and MEC scheduler of the MDP-DA-product model. + storm::storage::Scheduler scheduler(model.getNumberOfStates(), memoryStructure); + + // Use choices in the product model to create a choice based on model state and memory state + for (const auto &choice : this->_producedChoices) { + // -> choice + storm::storage::sparse::state_type modelState = std::get<0>(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[getMemoryState(daState, infSet)].get(modelState), "Tried to set choice for dontCare state."); + scheduler.setChoice(choice.second, modelState, getMemoryState(daState, infSet)); + } + + // Set "dontCare" states + for (uint_fast64_t memoryState = 0; memoryState < this->_dontCareStates.size(); ++memoryState) { + for (auto state : this->_dontCareStates[memoryState]) { + scheduler.setDontCare(state, memoryState); + } + } + + // 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; + + } + + template class SparseLTLSchedulerHelper; + template class SparseLTLSchedulerHelper; + +#ifdef STORM_HAVE_CARL + template class SparseLTLSchedulerHelper; + template class SparseLTLSchedulerHelper; + template class SparseLTLSchedulerHelper; + +#endif + + } + } + } +} \ No newline at end of file diff --git a/src/storm/modelchecker/helper/ltl/internal/SparseLTLSchedulerHelper.h b/src/storm/modelchecker/helper/ltl/internal/SparseLTLSchedulerHelper.h new file mode 100644 index 000000000..89f5075c0 --- /dev/null +++ b/src/storm/modelchecker/helper/ltl/internal/SparseLTLSchedulerHelper.h @@ -0,0 +1,102 @@ +#include "storm/storage/Scheduler.h" +#include "storm/models/sparse/Dtmc.h" +#include "storm/models/sparse/Mdp.h" +#include "storm/storage/MaximalEndComponent.h" +#include "storm/transformer/DAProductBuilder.h" + +namespace storm { + + + namespace modelchecker { + namespace helper { + namespace internal { + + /*! + * Helper class for scheduler construction in LTL model checking + * @tparam ValueType the type a value can have + * @tparam Nondeterministic A flag indicating if there is nondeterminism in the Model (MDP) + */ + template + class SparseLTLSchedulerHelper { + + public: + /*! + * The type of the product model (DTMC or MDP) that is used during the computation. + */ + using productModelType = typename std::conditional, storm::models::sparse::Dtmc>::type; + + /*! + * Initializes the helper. + * @param numProductStates number of product states + */ + SparseLTLSchedulerHelper(uint_fast64_t numProductStates); + + + /*! + * Set the scheduler choices to random. + */ + 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. + * 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. + * + * @param acceptance the acceptance condition (in DNF) + * @param mec the accepting end component + * @param conjunction the conjunction satisfied by the end component + * @param product the product model + */ + void saveProductEcChoices(automata::AcceptanceCondition const& acceptance, storm::storage::MaximalEndComponent const& mec, std::vector const& conjunction, typename transformer::DAProduct::ptr product); + + /*! + * Extracts scheduler choices and creates the memory structure for the LTL-Scheduler. + * + * @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 + * @param productBuilder the product builder + * @param product the model-DA product + * @param modelStatesOfInterest relevant states of the model + * @param transitionMatrix the transition matrix 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, storm::storage::SparseMatrix const& transitionMatrix); + + /*! + * Returns a deterministic fully defined scheduler (except for dontCareStates) for the given model. + * The choices are random if isRandom was set to true. + * + * @param model the model to construct the scheduler for + * @param onlyInitialStatesRelevant flag indicating whether we only consider the fragment reachable from initial model states. + * @return the scheduler + */ + storm::storage::Scheduler extractScheduler(storm::models::sparse::Model const& model, bool onlyInitialStatesRelevant); + + private: + + /** + * 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 daState DA-state + * @param infSet infSet ID + */ + uint_fast64_t getMemoryState(uint_fast64_t daState, uint_fast64_t infSet); + + + 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::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 + std::vector> _memoryTransitions; // The BitVector contains the model states that lead from startState to . This is deterministic, because each state is assigned to a unique MEC (scheduler). + std::vector _memoryInitialStates; // Save for each relevant state (initial or all) s its unique initial memory state (which memory state is reached from the initial state after reading s) + + }; + } + } + } +} \ No newline at end of file