From 93c2e92c2a3fd794c6c765280bafd27b390d1121 Mon Sep 17 00:00:00 2001 From: hannah Date: Sun, 11 Jul 2021 03:01:58 +0200 Subject: [PATCH] updated LTL-scheduler --- .../helper/ltl/SparseLTLHelper.cpp | 223 ++++++++++++++---- .../modelchecker/helper/ltl/SparseLTLHelper.h | 17 +- .../SparseModelMemoryProduct.cpp | 2 +- src/storm/transformer/Product.h | 8 + src/storm/utility/graph.cpp | 9 +- ...ulerGenerationMdpPrctlModelCheckerTest.cpp | 93 ++++++-- 6 files changed, 278 insertions(+), 74 deletions(-) diff --git a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp index 07940e3a7..c102b800b 100644 --- a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp +++ b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp @@ -16,6 +16,8 @@ #include "storm/environment/modelchecker/ModelCheckerEnvironment.h" +#include "storm/utility/graph.h" + namespace storm { namespace modelchecker { namespace helper { @@ -30,9 +32,12 @@ namespace storm { 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."); STORM_LOG_ASSERT(this->_productChoices.is_initialized(), "Trying to extract the produced scheduler but none is available. Was there a computation call before?"); + + // TODO fails for No accepting states, skipping probability computation. 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?"); + // Create a memory structure for the MDP scheduler with memory. typename storm::storage::MemoryStructureBuilder::MemoryStructureBuilder memoryBuilder(this->_memoryTransitions.get().size(), model); @@ -44,36 +49,36 @@ namespace storm { } } - /* - memoryStateLabeling: Label the memory states to specify, e.g., accepting states // TODO where are these labels used? - for (storm::storage::sparse::state_type q : set) { - memoryBuilder.setLabel(q,//todo); - } - */ - // initialMemoryStates: Assign an initial memory state to each initial state of the model. for (uint_fast64_t s0 : model.getInitialStates()) { - // Label the state as initial TODO unnecessary? - //memoryBuilder.setLabel(q, "Initial for model state " s0) memoryBuilder.setInitialMemoryState(s0, this->_memoryInitialStates.get()[s0]); } - - // Finally, we can build the memoryStructure. + // Now, we can build the memoryStructure. storm::storage::MemoryStructure memoryStructure = memoryBuilder.build(); - // Create a scheduler (with memory of size DA) for the model from the scheduler of the MDP-DA-product model. + // 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->_productChoices.get()) { - uint_fast64_t modelState = choice.first.first; - uint_fast64_t memoryState = choice.first.second; + // -> choice + 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 mec = std::get<2>(choice.first); + uint_fast64_t infSet = std::get<3>(choice.first); + + // Encode as memory state + uint_fast64_t memoryState = (((infSet * _mecStatesInfSets.get().size()) + mec) * _numberOfDaStates.get()) + automatonState; scheduler.setChoice(choice.second, modelState, memoryState); } - // TODO set non-reachable (modelState,memoryState)-Pairs (i.e. those that are not contained in _productChoices) to "unreachable", (extend Scheduler by something like std::vector> reachableSchedulerChoices; und isChoiceReachable(..)) + // TODO + // set non-reachable (modelState,memoryState)-Pairs (i.e. those that are not contained in _productChoices) to "unreachable", (extend Scheduler by something like std::vector> reachableSchedulerChoices; und isChoiceReachable(..)) + // Sanity check for created scheduler. + STORM_LOG_ASSERT(scheduler.isDeterministicScheduler(), "Expected a deterministic scheduler"); return scheduler; + } template @@ -95,7 +100,7 @@ namespace storm { template - storm::storage::BitVector SparseLTLHelper::computeAcceptingECs(automata::AcceptanceCondition const& acceptance, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions) { + storm::storage::BitVector SparseLTLHelper::computeAcceptingECs(automata::AcceptanceCondition const& acceptance, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, typename transformer::DAProduct::ptr product) { STORM_LOG_INFO("Computing accepting states for acceptance condition " << *acceptance.getAcceptanceExpression()); if (acceptance.getAcceptanceExpression()->isTRUE()) { STORM_LOG_INFO(" TRUE -> all states accepting (assumes no deadlock in the model)"); @@ -112,6 +117,14 @@ namespace storm { std::size_t accMECs = 0; std::size_t allMECs = 0; std::size_t i = 0; + + if (this->isProduceSchedulerSet()) { + _mecStatesInfSets.emplace(); + _productChoices.emplace(); + } + // Save the states that are already assigned a scheduler (MEC), a state is assigned to the first MEC we find. + storm::storage::BitVector finishedStates(transitionMatrix.getRowGroupCount(), false); + 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 @@ -153,12 +166,16 @@ namespace storm { storm::storage::MaximalEndComponentDecomposition mecs(transitionMatrix, backwardTransitions, allowed); allMECs += mecs.size(); for (const auto& mec : mecs) { + // Save the accSets that need to be visited inf often to satisfy a specific accepting MEC. + std::vector infSets = std::vector(); + STORM_LOG_DEBUG("Inspect MEC: " << mec); bool accepting = true; for (auto const& literal : conjunction) { if (literal->isTRUE()) { // skip + } else if (literal->isFALSE()) { accepting = false; break; @@ -173,6 +190,11 @@ namespace storm { accepting = false; break; } + + if (this->isProduceSchedulerSet()) { + infSets.emplace_back(~accSet); + } + } else { STORM_LOG_DEBUG("Checking against " << accSet); if (!mec.containsAnyState(accSet)) { @@ -180,7 +202,11 @@ namespace storm { accepting = false; break; } + if (this->isProduceSchedulerSet()) { + infSets.emplace_back(accSet); + } } + } else if (atom.getType() == cpphoafparser::AtomAcceptance::TEMPORAL_FIN) { // do only sanity checks here STORM_LOG_ASSERT(atom.isNegated() ? !mec.containsAnyState(~accSet) : !mec.containsAnyState(accSet), "MEC contains Fin-states, which should have been removed"); @@ -192,14 +218,69 @@ namespace storm { accMECs++; STORM_LOG_DEBUG("MEC is accepting"); - for (auto const& stateChoicePair : mec) { + for (auto const &stateChoicePair : mec) { acceptingStates.set(stateChoicePair.first); } + + if (this->isProduceSchedulerSet()) { + + storm::storage::BitVector mecStates(transitionMatrix.getRowGroupCount(), false); + for (auto const &stateChoicePair : mec) { + mecStates.set(stateChoicePair.first); + } + + // If there are no InfSets (either all TRUE or only FIN in conjunction) + if (infSets.empty()) { + // We want to visit some states of this MEC inf. often + infSets.emplace_back(mecStates); + } + + // Save the states of this MEC (that are not contained in any other MEC yet) and the InfSets need to be visited inf. often to sat. the acc. cond. + _mecStatesInfSets.get().insert({accMECs, std::make_pair(mecStates & ~finishedStates, infSets)}); + + // Define scheduler choices for the states in this MEC (that are not in any other MEC) + for (uint_fast64_t infSet = 0; infSet < infSets.size(); ++infSet) { + // 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()); + + + + // 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(_mecStatesInfSets.get()[accMECs].first, transitionMatrix, backwardTransitions, mecStates, _mecStatesInfSets.get()[accMECs].second[infSet], mecScheduler); + + // Prob1E sets an arbitrary choice for the psi states, but we want to stay in this accepting mec. + for (auto pState : (_mecStatesInfSets.get()[accMECs].first & _mecStatesInfSets.get()[accMECs].second[infSet])) { + // If we are in the InfSet, we stay in mec-states + // TODO is this correct: + // (*std::next(mec.getChoicesForState(pState).begin(), 0)) + mecScheduler.setChoice(storm::storage::SchedulerChoice((*std::next(mec.getChoicesForState(pState).begin()), 0)), pState); + } + + // Extract scheduler choices (only for states that are already assigned a scheduler, i.e are in another MEC) + for (auto pState : _mecStatesInfSets.get()[accMECs].first) { + //if (!_mecStatesInfSets.get()[accMECs].second[infSet].get(pState)) { + // We want to reach the InfSet, save choice: ---> choice + // TODO find test that fails, when ignoring these: + this->_productChoices.get().insert({std::make_tuple(product->getModelState(pState),product->getAutomatonState(pState), accMECs, infSet), mecScheduler.getChoice(pState)}); + } + + + } + + // The states in this MEC will not be reassigned + finishedStates = finishedStates | mecStates; + } } } } + if (this->isProduceSchedulerSet()) { + // Remaining states belong to no mec (REACH scheduler is computed later) + _mecStatesInfSets.get()[0] = std::make_pair(~finishedStates,std::vector(1,~finishedStates)); + } + STORM_LOG_DEBUG("Accepting states: " << acceptingStates); STORM_LOG_INFO("Found " << acceptingStates.getNumberOfSetBits() << " states in " << accMECs << " accepting MECs (considered " << allMECs << " MECs)."); @@ -209,7 +290,6 @@ namespace storm { template storm::storage::BitVector SparseLTLHelper::computeAcceptingBCCs(automata::AcceptanceCondition const& acceptance, storm::storage::SparseMatrix const& transitionMatrix) { storm::storage::StronglyConnectedComponentDecomposition bottomSccs(transitionMatrix, storage::StronglyConnectedComponentDecompositionOptions().onlyBottomSccs().dropNaiveSccs()); - //storm::storage::BitVector acceptingStates = storm::storage::BitVector(product->getProductModel().getNumberOfStates()); storm::storage::BitVector acceptingStates(transitionMatrix.getRowGroupCount(), false); std::size_t checkedBSCCs = 0, acceptingBSCCs = 0, acceptingBSCCStates = 0; @@ -275,9 +355,9 @@ namespace storm { storm::storage::BitVector acceptingStates; if (Nondeterministic) { STORM_LOG_INFO("Computing MECs and checking for acceptance..."); - acceptingStates = computeAcceptingECs(*product->getAcceptance(), product->getProductModel().getTransitionMatrix(), product->getProductModel().getBackwardTransitions()); + acceptingStates = computeAcceptingECs(*product->getAcceptance(), product->getProductModel().getTransitionMatrix(), product->getProductModel().getBackwardTransitions(), product); //TODO product is only needed for ->getModelState(pState) and DAStates for scheduler creation (maybe lambda instead) - } else { + } else { STORM_LOG_INFO("Computing BSCCs and checking for acceptance..."); acceptingStates = computeAcceptingBCCs(*product->getAcceptance(), product->getProductModel().getTransitionMatrix()); @@ -318,44 +398,101 @@ namespace storm { ); prodNumericResult = std::move(prodCheckResult.values); - if (this->isProduceSchedulerSet()) { - // Extract the choices of the scheduler for the MDP-DA product: -> choice - this->_productChoices.emplace(); + if (this->isProduceSchedulerSet()) { // TODO create fct for this + _numberOfDaStates = da.getNumberOfStates(); + // TODO asserts _mecStatesInfSets initialized etc. + + // 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().getNumberOfStates(); ++pState) { - this->_productChoices.get().insert({std::make_pair(product->getModelState(pState), product->getAutomatonState(pState)), prodCheckResult.scheduler->getChoice(pState)}); + // ---> choice + if(! acceptingStates.get(pState)){ + // Do not overwrite choices of states in an accepting MEC + this->_productChoices.get().insert({std::make_tuple(product->getModelState(pState), product->getAutomatonState(pState), 0, 0), prodCheckResult.scheduler->getChoice(pState)}); + } } + // Prepare the memory structure. For that, we need: transitions, initialMemoryStates (and memoryStateLabeling) - // Prepare the memory structure. For that, we need: transitions, initialMemoryStates (and todo: memoryStateLabeling) + // Compute size of the resulting memory structure: a state corresponds to > encoded as (((infSet * |mecs|) + mec) * |DAStates|) +q + uint64 numCopies =0; + for (auto const& mec: _mecStatesInfSets.get()) { + numCopies += mec.second.second.size(); + } + uint64 numMemoryStates = numCopies * _mecStatesInfSets.get().size() * da.getNumberOfStates() + da.getNumberOfStates(); //TODO is this correct // The next move function of the memory, will be build based on the transitions of the DA. - this->_memoryTransitions.emplace(da.getNumberOfStates(), std::vector(da.getNumberOfStates())); - - for (storm::storage::sparse::state_type startState = 0; startState < da.getNumberOfStates(); ++startState) { - for (storm::storage::sparse::state_type goalState = 0; - goalState < da.getNumberOfStates(); ++goalState) { - // Bitvector that represents modelStates the model states that trigger this transition. - storm::storage::BitVector modelStates(this->_transitionMatrix.getRowGroupCount(), false); - for (storm::storage::sparse::state_type modelState = 0; - modelState < this->_transitionMatrix.getRowGroupCount(); ++modelState) { - if (goalState == productBuilder.getSuccessor(modelState, startState, modelState)) { //todo remove first parameter - modelStates.set(modelState); + this->_memoryTransitions.emplace(numMemoryStates, std::vector(numMemoryStates, storm::storage::BitVector(this->_transitionMatrix.getRowGroupCount(), false))); + + + for (storm::storage::sparse::state_type automatonFrom = 0; automatonFrom < da.getNumberOfStates(); ++automatonFrom) { + for (storm::storage::sparse::state_type automatonTo = 0; automatonTo < da.getNumberOfStates(); ++automatonTo) { + // Find the modelStates that trigger this transition. + for (storm::storage::sparse::state_type modelState = 0; modelState < this->_transitionMatrix.getRowGroupCount(); ++modelState) { + + if(!product->isValidProductState(modelState, automatonTo)) { + // Memory state successor of the modelState-transition emanating not defined/reachable. + // TODO save as unreachable in scheduler + // STORM_PRINT("set to unreachable : (" << modelState <<" , " << automatonTo <<")"); + + } 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 > (mec=0 equals NoMec) + for (uint_fast64_t mec = 0; mec < _mecStatesInfSets.get().size(); ++mec) { + for (uint_fast64_t infSet = 0; infSet < _mecStatesInfSets.get()[mec].second.size(); ++infSet) { + + // Find the goalState >, where is in mec'. + if (_mecStatesInfSets.get()[mec].first.get(product->getProductStateIndex(modelState, automatonTo))) { + // in contained in this MEC. Now check if we have reached the current InfSet. + if(_mecStatesInfSets.get()[mec].second[infSet].get(product->getProductStateIndex(modelState, automatonTo))){ + // InfSet satisfied: Add modelState to the transition from > to >. + uint64 from = (((infSet * _mecStatesInfSets.get().size()) + mec) * da.getNumberOfStates()) + automatonFrom; + uint64 to = ((((infSet+1 < _mecStatesInfSets.get()[mec].second.size() ? infSet+1 : 0) * _mecStatesInfSets.get().size()) + mec) * da.getNumberOfStates()) + automatonTo; + _memoryTransitions.get()[from][to].set(modelState); + } else { + // InfSet not satisfied: Add modelState to the transition from > to >. + uint64 from = (((infSet * _mecStatesInfSets.get().size()) + mec) * da.getNumberOfStates()) + automatonFrom; + uint64 to = (((infSet * _mecStatesInfSets.get().size()) + mec) * da.getNumberOfStates()) + automatonTo; + _memoryTransitions.get()[from][to].set(modelState); + } + } else { + // We need to find the unique MEC containing and start in InfSet 0. + for (uint_fast64_t nextMec = 0; nextMec < _mecStatesInfSets.get().size(); ++nextMec) { + if (_mecStatesInfSets.get()[nextMec].first.get(product->getProductStateIndex(modelState, automatonTo))) { + // Add modelState to the transition from > to > + uint64 from = (((infSet * _mecStatesInfSets.get().size()) + mec) * da.getNumberOfStates()) + automatonFrom; + uint64 to = (((0 * _mecStatesInfSets.get().size()) + nextMec) * da.getNumberOfStates()) + automatonTo; + _memoryTransitions.get()[from][to].set(modelState); + break; // Can stop, because the state is only contained in one MEC. + } + } + } + } + + } } } - // Insert a transition: startState--{modelStates}-->goalState - this->_memoryTransitions.get()[startState][goalState] = std::move(modelStates); } } + // Finished creation of transitions. + // Find initial memory states this->_memoryInitialStates.emplace(); this->_memoryInitialStates->resize(this->_transitionMatrix.getRowGroupCount()); - // Save for each automaton state for which model state it is initial. - for (storm::storage::sparse::state_type modelState = 0; modelState< this->_transitionMatrix.getRowGroupCount(); ++modelState) { - this->_memoryInitialStates.get().at(modelState) = productBuilder.getInitialState(modelState); - } + // Save for each relevant model state its initial memory state (get the s-successor of q0) + for (storm::storage::sparse::state_type modelState : statesOfInterest) { + storm::storage::sparse::state_type automatonInit = productBuilder.getInitialState(modelState); + STORM_LOG_ASSERT(product->isValidProductState(modelState, automatonInit), "The memory successor state for the model state "<< modelState << "does not exist in the DA-Model Product."); + + // Search mec which contains + for (uint_fast64_t mec = 0; mec < _mecStatesInfSets.get().size(); ++mec) { + if (_mecStatesInfSets.get()[mec].first.get(product->getProductStateIndex(modelState, automatonInit))) { + this->_memoryInitialStates.get().at(modelState) = (((0 * _mecStatesInfSets.get().size()) + mec) * da.getNumberOfStates()) + automatonInit; + break; + } + } - // TODO labels (e.g. the accepting set?) for the automaton states + } + // Finished creation of initial states. } } else { diff --git a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h index 0e7277b54..35bcfd220 100644 --- a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h +++ b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h @@ -83,7 +83,7 @@ namespace storm { * @param the transition matrix of the model * @param the reversed transition relation */ - storm::storage::BitVector computeAcceptingECs(automata::AcceptanceCondition const& acceptance, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions); + 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. @@ -96,14 +96,13 @@ namespace storm { storm::storage::SparseMatrix const& _transitionMatrix; std::size_t _numberOfStates; //TODO just use _transitionMatrix.getRowGroupCount instead? - // REACH scheduler - boost::optional, storm::storage::SchedulerChoice>> _productChoices; // --> choice - boost::optional>> _memoryTransitions; // BitVector contains the model states that lead from startState to goalSate of the DA - boost::optional> _memoryInitialStates; // Saves for each modelState which automaton state is reached from the initial state //TODO improve - - // MEC scheduler - boost::optional> , storm::storage::SchedulerChoice>> _mecProductChoices; // <#literal, > ---> choice - boost::optional>> _mecMemoryTransitions; // BitVector contains the model states that lead from #INF(i) to #INF(i+1) of the AccCondition (#INF(1) AND #INF(2) ....) OR (..) + // REACH scheduler and MEC scheduler + boost::optional, storm::storage::SchedulerChoice>> _productChoices; // ---> ReachChoice and ---> MecChoice + boost::optional>>> _mecStatesInfSets; // Save for each accepting mec, its states and the infinity sets that need to be visited inf. often (mec 0 corresponds to NoMec) + // 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 stateOfInterest s its initial memory state (which memory state is reached from the initial state after reading s) + boost::optional _numberOfDaStates; }; } diff --git a/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp b/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp index 31708544d..029387288 100644 --- a/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp +++ b/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp @@ -288,7 +288,7 @@ namespace storm { uint64_t transitionId = entryIt - model.getTransitionMatrix().begin(); uint64_t successorMemoryState = memorySuccessors[transitionId * memoryStateCount + memoryState]; builder.addNextValue(currentRow, getResultState(entryIt->getColumn(), successorMemoryState), entryIt->getValue()); - } //TODO successor MemoryState is a problem here 8382838738483264 oder so + } } else { std::map transitions; for (auto const& choiceIndex : choice.getChoiceAsDistribution()) { diff --git a/src/storm/transformer/Product.h b/src/storm/transformer/Product.h index ee037784b..b30362466 100644 --- a/src/storm/transformer/Product.h +++ b/src/storm/transformer/Product.h @@ -36,6 +36,14 @@ namespace storm { return productIndexToProductState.at(productStateIndex).second; } + state_type getProductStateIndex(state_type modelState, state_type automatonState) const { + return productStateToProductIndex.at(product_state_type(modelState, automatonState)); //TODO does this work? + } + + bool isValidProductState(state_type modelState, state_type automatonState) const { + return (productStateToProductIndex.count(product_state_type(modelState, automatonState)) >0); //TODO does this work? + } + storm::storage::BitVector liftFromAutomaton(const storm::storage::BitVector& vector) const { state_type n = productModel.getNumberOfStates(); storm::storage::BitVector lifted(n, false); diff --git a/src/storm/utility/graph.cpp b/src/storm/utility/graph.cpp index 5df06c585..d5ca015c3 100644 --- a/src/storm/utility/graph.cpp +++ b/src/storm/utility/graph.cpp @@ -1764,7 +1764,7 @@ namespace storm { template void computeSchedulerProb1E(storm::storage::BitVector const& prob1EStates, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::Scheduler& scheduler, boost::optional const& rowFilter = boost::none); - + template storm::storage::BitVector performProbGreater0E(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0) ; template storm::storage::BitVector performProb0A(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); @@ -1892,9 +1892,10 @@ namespace storm { template std::pair performProb01(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); - - - + + // TODO remove? + template void computeSchedulerProb1E(storm::storage::BitVector const& prob1EStates, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::Scheduler& scheduler, boost::optional const& rowFilter = boost::none); + template storm::storage::BitVector performProbGreater0E(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0) ; template storm::storage::BitVector performProb0A(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); diff --git a/src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp index 45362994a..dd8846f74 100755 --- a/src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp @@ -203,11 +203,14 @@ namespace { } } + + TYPED_TEST(SchedulerGenerationMdpPrctlModelCheckerTest, ltl) { typedef typename TestFixture::ValueType ValueType; - std::string formulasString = "Pmax=? [X X \"target\"]; Pmin=? [G F \"target\"]; Pmax=? [(G F s>2) & (F G (!s=3))];"; - auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/scheduler_generation.nm", formulasString); + std::string formulasString = "Pmax=? [X X \"target\"]; Pmin=? [G F \"target\"]; Pmax=? [(G F s>2) & (F G !(s=3))];"; + auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/scheduler_generation.nm", + formulasString); auto mdp = std::move(modelFormulas.first); auto tasks = this->getTasks(modelFormulas.second); EXPECT_EQ(4ull, mdp->getNumberOfStates()); @@ -221,58 +224,114 @@ namespace { auto result = checker.check(this->env(), tasks[0]); ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); ASSERT_TRUE(result->template asExplicitQuantitativeCheckResult().hasScheduler()); - storm::storage::Scheduler const& scheduler = result->template asExplicitQuantitativeCheckResult().getScheduler(); + storm::storage::Scheduler const &scheduler = result->template asExplicitQuantitativeCheckResult().getScheduler(); EXPECT_TRUE(scheduler.isDeterministicScheduler()); - EXPECT_TRUE(! scheduler.isMemorylessScheduler()); + EXPECT_TRUE(!scheduler.isMemorylessScheduler()); EXPECT_TRUE(scheduler.isPartialScheduler()); auto inducedModel = mdp->applyScheduler(scheduler); + ASSERT_EQ(inducedModel->getType(), storm::models::ModelType::Mdp); - auto const& inducedMdp = inducedModel->template as>(); // TODO DTMC! + auto const &inducedMdp = inducedModel->template as>(); // TODO DTMC! EXPECT_EQ(inducedMdp->getNumberOfChoices(), inducedMdp->getNumberOfStates()); + storm::modelchecker::SparseMdpPrctlModelChecker> inducedChecker(*inducedMdp); auto inducedResult = inducedChecker.check(this->env(), tasks[0]); ASSERT_TRUE(inducedResult->isExplicitQuantitativeCheckResult()); - EXPECT_NEAR(this->parseNumber("9/10"), inducedResult->template asExplicitQuantitativeCheckResult()[*mdp->getInitialStates().begin()], storm::settings::getModule().getPrecision()); + EXPECT_NEAR(this->parseNumber("9/10"), + inducedResult->template asExplicitQuantitativeCheckResult()[*mdp->getInitialStates().begin()], //TODO other states, too + storm::settings::getModule().getPrecision()); } + { auto result = checker.check(this->env(), tasks[1]); ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); ASSERT_TRUE(result->template asExplicitQuantitativeCheckResult().hasScheduler()); - storm::storage::Scheduler const& scheduler = result->template asExplicitQuantitativeCheckResult().getScheduler(); + storm::storage::Scheduler const &scheduler = result->template asExplicitQuantitativeCheckResult().getScheduler(); EXPECT_TRUE(scheduler.isDeterministicScheduler()); EXPECT_TRUE(!scheduler.isMemorylessScheduler()); EXPECT_TRUE(scheduler.isPartialScheduler()); auto inducedModel = mdp->applyScheduler(scheduler); ASSERT_EQ(inducedModel->getType(), storm::models::ModelType::Mdp); - auto const& inducedMdp = inducedModel->template as>(); + auto const &inducedMdp = inducedModel->template as>(); EXPECT_EQ(inducedMdp->getNumberOfChoices(), inducedMdp->getNumberOfStates()); - storm::modelchecker::SparseMdpPrctlModelChecker> inducedChecker(*inducedMdp); + storm::modelchecker::SparseMdpPrctlModelChecker> inducedChecker( + *inducedMdp); auto inducedResult = inducedChecker.check(this->env(), tasks[1]); ASSERT_TRUE(inducedResult->isExplicitQuantitativeCheckResult()); - EXPECT_NEAR(this->parseNumber("1/2"), inducedResult->template asExplicitQuantitativeCheckResult()[*mdp->getInitialStates().begin()], storm::settings::getModule().getPrecision()); + EXPECT_NEAR(this->parseNumber("1/2"), + inducedResult->template asExplicitQuantitativeCheckResult()[*mdp->getInitialStates().begin()], + storm::settings::getModule().getPrecision()); } + { auto result = checker.check(this->env(), tasks[2]); - EXPECT_NEAR(this->parseNumber("1/2"), result->template asExplicitQuantitativeCheckResult()[*mdp->getInitialStates().begin()], storm::settings::getModule().getPrecision()); - + EXPECT_NEAR(this->parseNumber("1/2"), + result->template asExplicitQuantitativeCheckResult()[*mdp->getInitialStates().begin()], + storm::settings::getModule().getPrecision()); ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); ASSERT_TRUE(result->template asExplicitQuantitativeCheckResult().hasScheduler()); - storm::storage::Scheduler const& scheduler = result->template asExplicitQuantitativeCheckResult().getScheduler(); + storm::storage::Scheduler const &scheduler = result->template asExplicitQuantitativeCheckResult().getScheduler(); EXPECT_TRUE(scheduler.isDeterministicScheduler()); EXPECT_TRUE(!scheduler.isMemorylessScheduler()); EXPECT_TRUE(scheduler.isPartialScheduler()); auto inducedModel = mdp->applyScheduler(scheduler); ASSERT_EQ(inducedModel->getType(), storm::models::ModelType::Mdp); - auto const& inducedMdp = inducedModel->template as>(); + auto const &inducedMdp = inducedModel->template as>(); EXPECT_EQ(inducedMdp->getNumberOfChoices(), inducedMdp->getNumberOfStates()); - storm::modelchecker::SparseMdpPrctlModelChecker> inducedChecker(*inducedMdp); + storm::modelchecker::SparseMdpPrctlModelChecker> inducedChecker( + *inducedMdp); auto inducedResult = inducedChecker.check(this->env(), tasks[2]); ASSERT_TRUE(inducedResult->isExplicitQuantitativeCheckResult()); - EXPECT_NEAR(this->parseNumber("1/2"), inducedResult->template asExplicitQuantitativeCheckResult()[*mdp->getInitialStates().begin()], storm::settings::getModule().getPrecision()); + EXPECT_NEAR(this->parseNumber("1/2"), + inducedResult->template asExplicitQuantitativeCheckResult()[*mdp->getInitialStates().begin()], + storm::settings::getModule().getPrecision()); } + } - + + + TYPED_TEST(SchedulerGenerationMdpPrctlModelCheckerTest, ltl2) { + typedef typename TestFixture::ValueType ValueType; + //TODO find noMEC-scheduler-error (need nondet in EC) + + // Todo unreachable Product state error + std::string formulasString = "Pmax=? [X X !(x=0)];"; + auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/prism-mec-example1.nm", formulasString); + + auto mdp = std::move(modelFormulas.first); + auto tasks = this->getTasks(modelFormulas.second); + EXPECT_EQ(3ull, mdp->getNumberOfStates()); + EXPECT_EQ(5ull, mdp->getNumberOfTransitions()); + ASSERT_EQ(mdp->getType(), storm::models::ModelType::Mdp); + EXPECT_EQ(4ull, mdp->getNumberOfChoices()); + + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp); + + { + auto result = checker.check(this->env(), tasks[0]); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + ASSERT_TRUE(result->template asExplicitQuantitativeCheckResult().hasScheduler()); + storm::storage::Scheduler const &scheduler = result->template asExplicitQuantitativeCheckResult().getScheduler(); + + EXPECT_TRUE(scheduler.isDeterministicScheduler()); + EXPECT_TRUE(!scheduler.isMemorylessScheduler()); + EXPECT_TRUE(scheduler.isPartialScheduler()); + auto inducedModel = mdp->applyScheduler(scheduler, true); + + + ASSERT_EQ(inducedModel->getType(), storm::models::ModelType::Mdp); + auto const &inducedMdp = inducedModel->template as>(); // TODO DTMC! + EXPECT_EQ(inducedMdp->getNumberOfChoices(), inducedMdp->getNumberOfStates()); + + storm::modelchecker::SparseMdpPrctlModelChecker> inducedChecker(*inducedMdp); + auto inducedResult = inducedChecker.check(this->env(), tasks[0]); + ASSERT_TRUE(inducedResult->isExplicitQuantitativeCheckResult()); + // EXPECT_NEAR(this->parseNumber("todo"), inducedResult->template asExplicitQuantitativeCheckResult()[*mdp->getInitialStates().begin()], storm::settings::getModule().getPrecision()); + } + + } + } \ No newline at end of file