From f92b2104b599a4a2bd6b16f41cbda529d0b6c05a Mon Sep 17 00:00:00 2001 From: hannah Date: Tue, 27 Jul 2021 11:07:10 +0200 Subject: [PATCH] TODOs and fixed an error during scheduler creation --- .../csl/SparseCtmcCslModelChecker.cpp | 2 +- .../SparseMarkovAutomatonCslModelChecker.cpp | 2 +- .../helper/ltl/SparseLTLHelper.cpp | 306 +++++++++--------- .../modelchecker/helper/ltl/SparseLTLHelper.h | 39 +-- .../prctl/SparseDtmcPrctlModelChecker.cpp | 4 +- .../prctl/SparseMdpPrctlModelChecker.cpp | 2 +- .../prctl/helper/SparseMdpPrctlHelper.cpp | 4 +- 7 files changed, 187 insertions(+), 172 deletions(-) diff --git a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp index 28824477f..e83b692b7 100644 --- a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp @@ -130,7 +130,7 @@ namespace storm { modelDot.close(); } - storm::modelchecker::helper::SparseLTLHelper helper(embeddedDtmc.getTransitionMatrix(), embeddedDtmc.getNumberOfStates()); + storm::modelchecker::helper::SparseLTLHelper helper(embeddedDtmc.getTransitionMatrix()); storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, embeddedDtmc); // Compute Satisfaction sets for APs diff --git a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp index 641882d27..9ef8c5f1f 100644 --- a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp @@ -144,7 +144,7 @@ namespace storm { modelDot.close(); } - storm::modelchecker::helper::SparseLTLHelper helper(embeddedMdp.getTransitionMatrix(), embeddedMdp.getNumberOfStates()); + storm::modelchecker::helper::SparseLTLHelper helper(embeddedMdp.getTransitionMatrix()); storm::modelchecker::helper::setInformationFromCheckTaskNondeterministic(helper, checkTask, embeddedMdp); // Compute Satisfaction sets for APs diff --git a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp index 0235fa073..5c86422c1 100644 --- a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp +++ b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp @@ -23,7 +23,7 @@ namespace storm { namespace helper { template - SparseLTLHelper::SparseLTLHelper(storm::storage::SparseMatrix const& transitionMatrix, std::size_t numberOfStates) : _transitionMatrix(transitionMatrix), _numberOfStates(numberOfStates){ + SparseLTLHelper::SparseLTLHelper(storm::storage::SparseMatrix const& transitionMatrix) : _transitionMatrix(transitionMatrix){ // Intentionally left empty. } @@ -45,6 +45,7 @@ namespace storm { 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?"); + // todo STORM_LOG_ASSERT(this->_dontCareSates.is_initialized(), "Trying to extract the dontCare states of the Scheduler 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. @@ -71,8 +72,7 @@ namespace storm { } } - - // Now, we can build the memoryStructure. + // 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. @@ -84,27 +84,23 @@ namespace storm { storm::storage::sparse::state_type modelState = std::get<0>(choice.first); storm::storage::sparse::state_type automatonState = 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); - - // 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 don't care states + for (uint_fast64_t memoryState = 0; memoryState < this->_dontCareStates.get().size(); ++memoryState) { + for (auto state : this->_dontCareStates.get()[memoryState]) { + scheduler.setDontCare(state, memoryState); } + STORM_LOG_ASSERT(scheduler.isChoiceSelected(~_dontCareStates.get()[memoryState], memoryState), "choice missing" << memoryState); } - */ - // Sanity check for created scheduler. STORM_LOG_ASSERT(scheduler.isDeterministicScheduler(), "Expected a deterministic scheduler"); - // TODO STORM_LOG_ASSERT(!scheduler.isPartialScheduler(), "Expected a fully defined scheduler"); + STORM_LOG_ASSERT(!scheduler.isPartialScheduler(), "Expected a fully defined scheduler"); + return scheduler; } @@ -290,7 +286,7 @@ namespace storm { 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] = infSetIds; + _accInfSets.get()[stateChoicePair.first].emplace(infSetIds); newMecStates.set(stateChoicePair.first); } @@ -303,19 +299,18 @@ namespace storm { 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); //todo &mecstates? nec.? - - // States that already reached the InfSet: Prob1E sets an arbitrary choice for the psi states, but we want to stay in this accepting 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])) { - // If we are in the InfSet, we move to some state in this MEC. + // 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 - // TODO _mecChoices ---> choice (remove product arg, transform directly to memoryState) + // TODO internal mec choices and transform to _producedChoices at end of fct? want to remove product ptr this->_producedChoices.get().insert({std::make_tuple(product->getModelState(pState), product->getAutomatonState(pState), id), mecScheduler.getChoice(pState)}); } } @@ -351,6 +346,89 @@ namespace storm { return acceptingStates; } + template + void SparseLTLHelper::createMemoryStructure(uint_fast64_t numDaStates, transformer::DAProductBuilder const& productBuilder, typename transformer::DAProduct::ptr product, storm::storage::BitVector const& acceptingProductStates, storm::storage::BitVector const& modelStatesOfInterest) { + // 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 = ((numDaStates-1) * (_infSets.get().size()+1)) + _infSets.get().size()+1; //+1 for states outside accECs + uint64 numMemoryStates = (numDaStates) * (_infSets.get().size()+1); //+1 for states outside accECs + STORM_LOG_INFO(" INF SETS: "<< (_infSets.get().size()+1)); + STORM_LOG_INFO(" INF SETS: "<< (numDaStates)); + + // 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 < numDaStates; ++automatonFrom) { + for (storm::storage::sparse::state_type modelState = 0; modelState < this->_transitionMatrix.getRowGroupCount(); ++modelState) { + uint_fast64_t automatonTo = productBuilder.getSuccessor(modelState, automatonFrom, modelState); //TODO remove first parameter of getSuccessor + + 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()[(automatonFrom * (_infSets.get().size()+1)) + infSet][(automatonTo * (_infSets.get().size()+1)) + *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); + + } 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()[(automatonFrom * (_infSets.get().size()+1)) + infSet][(automatonTo * (_infSets.get().size()+1)) + *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] = (automatonState * (_infSets.get().size()+1)) + *infSet; + + } else { + _memoryInitialStates.get()[modelState] = (automatonState * (_infSets.get().size()+1)) + _infSets.get().size(); + } + + } + // Finished creation of initial states. + + } + template std::vector SparseLTLHelper::computeDAProductProbabilities(Environment const& env, storm::automata::DeterministicAutomaton const& da, std::map& apSatSets) { const storm::automata::APSet& apSet = da.getAPSet(); @@ -370,18 +448,18 @@ namespace storm { statesOfInterest = this->getRelevantStates(); } else { // product from all model states - statesOfInterest = storm::storage::BitVector(this->_numberOfStates, true); + statesOfInterest = storm::storage::BitVector(this->_transitionMatrix.getRowGroupCount(), true); } STORM_LOG_INFO("Building "+ (Nondeterministic ? std::string("MDP-DA") : std::string("DTMC-DA")) +" product with deterministic automaton, starting from " << statesOfInterest.getNumberOfSetBits() << " model states..."); transformer::DAProductBuilder productBuilder(da, statesForAP); - typename transformer::DAProduct::ptr product = productBuilder.build(this->_transitionMatrix, statesOfInterest); + auto product = productBuilder.build(this->_transitionMatrix, statesOfInterest); STORM_LOG_INFO("Product "+ (Nondeterministic ? std::string("MDP-DA") : std::string("DTMC-DA")) +" has " << product->getProductModel().getNumberOfStates() << " states and " - << product->getProductModel().getNumberOfTransitions() << " transitions."); + << product->getProductModel().getNumberOfTransitions() << " transitions."); if (storm::settings::getModule().isTraceSet()) { STORM_LOG_TRACE("Writing product model to product.dot"); @@ -401,7 +479,7 @@ namespace storm { STORM_LOG_INFO("Computing MECs and checking for acceptance..."); acceptingStates = computeAcceptingECs(*product->getAcceptance(), product->getProductModel().getTransitionMatrix(), product->getProductModel().getBackwardTransitions(), product); //TODO product is only needed for ->getModelState(pState) (remove arg) - } else { + } else { STORM_LOG_INFO("Computing BSCCs and checking for acceptance..."); acceptingStates = computeAcceptingBCCs(*product->getAcceptance(), product->getProductModel().getTransitionMatrix()); @@ -409,7 +487,7 @@ namespace storm { if (acceptingStates.empty()) { STORM_LOG_INFO("No accepting states, skipping probability computation."); - std::vector numericResult(this->_numberOfStates, storm::utility::zero()); + std::vector numericResult(this->_transitionMatrix.getRowGroupCount(), storm::utility::zero()); this->_randomScheduler = true; return numericResult; } @@ -433,139 +511,73 @@ namespace storm { if (Nondeterministic) { MDPSparseModelCheckingHelperReturnType prodCheckResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeUntilProbabilities(env, - std::move(solveGoalProduct), - product->getProductModel().getTransitionMatrix(), - product->getProductModel().getBackwardTransitions(), - bvTrue, - acceptingStates, - this->isQualitativeSet(), - this->isProduceSchedulerSet() // Whether to create memoryless scheduler for the Model-DA Product. - ); + std::move(solveGoalProduct), + product->getProductModel().getTransitionMatrix(), + product->getProductModel().getBackwardTransitions(), + bvTrue, + acceptingStates, + this->isQualitativeSet(), + this->isProduceSchedulerSet() // Whether to create memoryless scheduler for the Model-DA Product. + ); prodNumericResult = std::move(prodCheckResult.values); - if (this->isProduceSchedulerSet()) { // TODO create fct for this + if (this->isProduceSchedulerSet()) { - // TODO asserts _mecStatesInfSets initialized etc. + 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 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)); + // TODO fct + //_dontCareStates.emplace(((da.getNumberOfStates()-1) * (_infSets.get().size()+1)) + _infSets.get().size()+1, storm::storage::BitVector(this->_transitionMatrix.getRowGroupCount(), false)); + _dontCareStates.emplace(((da.getNumberOfStates()) * (_infSets.get().size()+1)), storm::storage::BitVector(this->_transitionMatrix.getRowGroupCount(), false)); + // TODO optimize: + for (storm::storage::sparse::state_type automatonState= 0; automatonState < da.getNumberOfStates(); ++automatonState) { + for (storm::storage::sparse::state_type modelState = 0; modelState < this->_transitionMatrix.getRowGroupCount(); ++modelState) { - // 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 = 0; pState < this->_transitionMatrix.getRowGroupCount(); ++pState) { - - - // set _producedChoices > ---> choice. - if (acceptingStates.get(pState)) { - // TODO extract _mecProductChoices // TODO directly translate into memstate , modelstate - } else { - // For non-accepting states that are not in any accepting EC we use the 'last' copy of the DA - this->_accInfSets.get()[pState] = {_infSets.get().size()}; - - // For state not in any accEC: ---> choice. - // TODO directly translate into memstate , modelstate - this->_producedChoices.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)); + if (! product->isValidProductState(modelState, automatonState)) { + for (uint_fast64_t infSet = 0; infSet < _infSets.get().size()+1; ++infSet) { + _dontCareStates.get()[automatonState * (_infSets.get().size() + 1) + infSet].set(modelState, 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. - 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)) { - // 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) - // 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 - 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); + // and optimize dontCare below: + // 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 = 0; pState < product->getProductModel().getTransitionMatrix().getRowGroupCount(); ++pState) { + if (acceptingStates.get(pState)) { + // Set the undefined MEC-scheduler combinations to dontCare. + for (uint_fast64_t infSet = 0; infSet < _infSets.get().size()+1; ++infSet) { // TODO infset+1 too? + // todo If is not in _mecProductChoices it is dont Care? + 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); + } + } + } else { + // Set choice For non-accepting states that are not in any accepting EC + this->_accInfSets.get()[pState] = {_infSets.get().size()}; + if (prodCheckResult.scheduler->isDontCare(pState)) { + _dontCareStates.get()[(product->getAutomatonState(pState)) * (_infSets.get().size()+1) + _infSets.get().size()].set(product->getModelState(pState), true); + } else { + // For state not in any accEC: ---> choice. + // Use the 'last' copy of the DA + this->_producedChoices.get().insert({std::make_tuple(product->getModelState(pState),product->getAutomatonState(pState),_infSets.get().size()),prodCheckResult.scheduler->getChoice(pState)}); + }; - // TODO problem other inf set combis may not be reachable? - // this->_reachableStates.get()[(automatonTo * (_infSets.get().size()+1)) + *newInfSet].set(modelState, true); + // todo correct? nonMec state x infSet do not exist + 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); - } 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 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()[(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); - } - } - } - } } } } - // 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 : statesOfInterest) { - 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 (acceptingStates[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] = (automatonState * (_infSets.get().size()+1)) + *infSet; - } else { - _memoryInitialStates.get()[modelState] = (automatonState * (_infSets.get().size()+1)) + _infSets.get().size(); - } + // todo extend by scheduler choices? + // todo extractSchedulerChoices() + createMemoryStructure(da.getNumberOfStates(), productBuilder, product, acceptingStates, statesOfInterest); - } - // Finished creation of initial states. } } else { @@ -576,9 +588,9 @@ namespace storm { bvTrue, acceptingStates, this->isQualitativeSet()); - } + } - std::vector numericResult = product->projectToOriginalModel(this->_numberOfStates, prodNumericResult); + std::vector numericResult = product->projectToOriginalModel(this->_transitionMatrix.getRowGroupCount(), prodNumericResult); return numericResult; } @@ -612,10 +624,10 @@ namespace storm { da = storm::automata::LTL2DeterministicAutomaton::ltl2daSpot(*ltlFormula, Nondeterministic); } - STORM_LOG_DEBUG("Deterministic automaton for LTL formula has " - << da->getNumberOfStates() << " states, " - << da->getAPSet().size() << " atomic propositions and " - << *da->getAcceptance()->getAcceptanceExpression() << " as acceptance condition." << std::endl); + STORM_LOG_INFO("Deterministic automaton for LTL formula has " + << da->getNumberOfStates() << " states, " + << da->getAPSet().size() << " atomic propositions and " + << *da->getAcceptance()->getAcceptanceExpression() << " as acceptance condition." << std::endl); std::vector numericResult = computeDAProductProbabilities(env, *da, apSatSets); diff --git a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h index e710676c9..fb7bf0101 100644 --- a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h +++ b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h @@ -25,8 +25,8 @@ namespace storm { public: /*! - * The type of the product automaton (DTMC or MDP) that is used during the computation. - */ + * The type of the product automaton (DTMC or MDP) that is used during the computation. + */ using productModelType = typename std::conditional, storm::models::sparse::Dtmc>::type; /*! @@ -34,21 +34,21 @@ namespace storm { * @param the transition matrix of the model * @param the number of states of the model */ - SparseLTLHelper(storm::storage::SparseMatrix const& transitionMatrix, std::size_t numberOfSates); + SparseLTLHelper(storm::storage::SparseMatrix const& transitionMatrix); /*! * @pre before calling this, a computation call should have been performed during which scheduler production was enabled. - * @param TODO + * @param 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); /*! - * todo computes Sat sets of AP - * @param - * @param - * @return + * Computes the states that are satisfying the AP. + * @param mapping from Ap to formula + * @param lambda that checks the provided formula + * @return mapping from AP to satisfaction sets */ static std::map computeApSets(std::map> const& extracted, std::function(std::shared_ptr const& formula)> formulaChecker); @@ -71,7 +71,7 @@ namespace storm { private: /*! - * Compute a set S of states that admit a probability 1 strategy of satisfying the given acceptance condition (in DNF). + * Computes a set S of states that admit a probability 1 strategy of satisfying the given acceptance condition (in DNF). * More precisely, let * accEC be the set of states that are contained in end components that satisfy the acceptance condition * and let @@ -85,24 +85,27 @@ namespace storm { storm::storage::BitVector computeAcceptingECs(automata::AcceptanceCondition const& acceptance, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, typename transformer::DAProduct::ptr product); /** - * Compute a set S of states that are contained in BSCCs that satisfy the given acceptance conditon. - * @tparam the acceptance condition - * @tparam the transition matrix of the model + * 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 */ storm::storage::BitVector computeAcceptingBCCs(automata::AcceptanceCondition const& acceptance, storm::storage::SparseMatrix const& transitionMatrix); + /** + * Helper function, creates the memory structure for the LTL-Scheduler. + * @param the acceptance condition + * @param the transition matrix of the model + */ + void createMemoryStructure(uint_fast64_t numDaStates, transformer::DAProductBuilder const& productBuilder, typename transformer::DAProduct::ptr product, storm::storage::BitVector const& acceptingProductStates, storm::storage::BitVector const& modelStatesOfInterest); + storm::storage::SparseMatrix const& _transitionMatrix; - std::size_t _numberOfStates; //TODO just use _transitionMatrix.getRowGroupCount instead? // scheduler bool _randomScheduler = false; - // todo directly memstate, state -> choice - boost::optional, storm::storage::SchedulerChoice>> _producedChoices; // ---> ReachChoice and ---> MecChoice - boost::optional> _unreachableStates; // unreachable memory state and model state combinations + boost::optional, storm::storage::SchedulerChoice>> _producedChoices; // ---> ReachChoice and ---> MecChoice + boost::optional> _dontCareStates; // memory state combinations that are never visited - // Mec Scheduler - // _mecProductChoices -> choice 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 diff --git a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp index 2e14c8fdb..870a9a09a 100644 --- a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp @@ -132,7 +132,7 @@ namespace storm { << *da->getAcceptance()->getAcceptanceExpression() << " as acceptance condition."); const SparseDtmcModelType& dtmc = this->getModel(); - storm::modelchecker::helper::SparseLTLHelper helper(dtmc.getTransitionMatrix(), dtmc.getNumberOfStates()); + storm::modelchecker::helper::SparseLTLHelper helper(dtmc.getTransitionMatrix()); storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, dtmc); // Compute Satisfaction sets for APs @@ -164,7 +164,7 @@ namespace storm { modelDot.close(); } - storm::modelchecker::helper::SparseLTLHelper helper(dtmc.getTransitionMatrix(), dtmc.getNumberOfStates()); + storm::modelchecker::helper::SparseLTLHelper helper(dtmc.getTransitionMatrix()); storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, dtmc); // Compute Satisfaction sets for APs diff --git a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index 1d68b1d1f..cba1864d2 100644 --- a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -198,7 +198,7 @@ namespace storm { } - storm::modelchecker::helper::SparseLTLHelper helper(mdp.getTransitionMatrix(), mdp.getNumberOfStates()); + storm::modelchecker::helper::SparseLTLHelper helper(mdp.getTransitionMatrix()); storm::modelchecker::helper::setInformationFromCheckTaskNondeterministic(helper, checkTask, mdp); // Compute Satisfaction sets for APs diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index 5321960a9..de837daa3 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -616,10 +616,10 @@ namespace storm { 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 is true, we have to set the scheduler for maybe states as "dontCare" if (maybeStatesNotRelevant) { for (auto state : qualitativeStateSets.maybeStates) { - scheduler->setStateUnreachable(state); + scheduler->setDontCare(state); } }