From d7b696a753292b46865f4fcf1bd7b204c14d7f38 Mon Sep 17 00:00:00 2001 From: hannah Date: Thu, 15 Jul 2021 20:21:00 +0200 Subject: [PATCH] restructured the ltl-scheduler --- .../helper/ltl/SparseLTLHelper.cpp | 225 ++++++++++-------- .../modelchecker/helper/ltl/SparseLTLHelper.h | 9 +- .../MemoryStructureBuilder.cpp | 2 +- src/storm/utility/graph.cpp | 1 - ...ulerGenerationMdpPrctlModelCheckerTest.cpp | 2 +- 5 files changed, 134 insertions(+), 105 deletions(-) diff --git a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp index bd782df1e..57efb19c3 100644 --- a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp +++ b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp @@ -50,7 +50,7 @@ namespace storm { } // initialMemoryStates: Assign an initial memory state to each initial state of the model. - for (uint_fast64_t s0 : model.getInitialStates()) { // TODO should be relevantStates? + for (uint_fast64_t s0 : model.getInitialStates()) { // TODO set all from _memoryInitialStates, not only mdoelInitial memoryBuilder.setInitialMemoryState(s0, this->_memoryInitialStates.get()[s0]); } @@ -62,15 +62,12 @@ namespace storm { // Use choices in the product model to create a choice based on model state and memory state for (const auto &choice : this->_productChoices.get()) { - // -> choice + // -> 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); + uint_fast64_t infSet = std::get<2>(choice.first); - // Encode as memory state - uint_fast64_t memoryState = (((infSet * _mecStatesInfSets.get().size()) + mec) * _numberOfDaStates.get()) + automatonState; - scheduler.setChoice(choice.second, modelState, memoryState); + scheduler.setChoice(choice.second, modelState, automatonState*(_infSets.get().size()+1)+ infSet); } // 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(..)) @@ -119,11 +116,10 @@ namespace storm { std::size_t i = 0; if (this->isProduceSchedulerSet()) { - _mecStatesInfSets.emplace(); + _infSets.emplace(); + _accInfSets.emplace(product->getProductModel().getNumberOfStates(), boost::none); _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 @@ -166,9 +162,6 @@ 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; @@ -191,10 +184,6 @@ namespace storm { break; } - if (this->isProduceSchedulerSet()) { - infSets.emplace_back(~accSet); - } - } else { STORM_LOG_DEBUG("Checking against " << accSet); if (!mec.containsAnyState(accSet)) { @@ -202,9 +191,7 @@ namespace storm { accepting = false; break; } - if (this->isProduceSchedulerSet()) { - infSets.emplace_back(accSet); - } + } } else if (atom.getType() == cpphoafparser::AtomAcceptance::TEMPORAL_FIN) { @@ -224,33 +211,87 @@ namespace storm { if (this->isProduceSchedulerSet()) { - storm::storage::BitVector mecStates(transitionMatrix.getRowGroupCount(), false); + // Save all states contained in this MEC + storm::storage::BitVector mecStates(product->getProductModel().getNumberOfStates(), 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); + // 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.get().begin(), _infSets.get().end(), infSet); + if (it == _infSets.get().end()) { + _infSets.get().emplace_back(infSet); + infSetIds.insert(_infSets.get().size() - 1); + } else { + // save ID for accCond of the MEC states + infSetIds.insert(distance(_infSets.get().begin(), it)); //TODO test + } + } } - // 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)}); + /* should not occur + if (infSetIds.empty()) { - // 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()); + auto it = std::find(_infSets.get().begin(), _infSets.get().end(), mecStates); + if(it == _infSets.get().end()) { + _infSets.get().emplace_back(mecStates); + infSetIds.insert(_infSets.get().size()-1); + } else { + // save ID for accCond of the MEC states + infSetIds.insert(distance(_infSets.get().begin(), it)); //TODO test + } + } + */ + // 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.get()[stateChoicePair.first] == boost::none) { + // state wasn't assigned to any other MEC yet. + _accInfSets.get()[stateChoicePair.first] = infSetIds; + newMecStates.set(stateChoicePair.first); + + } + } - // 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])) { + + // 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], mecScheduler); + + // States that already reached the InfSet: Prob1E sets an arbitrary choice for the psi states, but we want to stay in this accepting mec. + for (auto pState : (newMecStates & _infSets.get()[id])) { // If we are in the InfSet, we stay in mec-states // TODO is this correct: // (*std::next(mec.getChoicesForState(pState).begin(), 0)) @@ -258,29 +299,19 @@ namespace storm { } // 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)}); + for (auto pState : newMecStates) { + // We want to reach the InfSet, save choice: ---> choice + this->_productChoices.get().insert({std::make_tuple(product->getModelState(pState),product->getAutomatonState(pState), id), 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)."); @@ -399,29 +430,27 @@ namespace storm { prodNumericResult = std::move(prodCheckResult.values); 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) { - // ---> choice + // for state not in any accEC ---> 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)}); + this->_productChoices.get().insert({std::make_tuple(product->getModelState(pState), product->getAutomatonState(pState), _infSets.get().size()), prodCheckResult.scheduler->getChoice(pState)}); + // For non-accepting states that are not in any accepting EC we use the 'last' copy of the DA + this->_accInfSets.get()[pState] = {this->_infSets.get().size()}; } } // 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 (((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 + // 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 - // The next move function of the memory, will be build based on the transitions of the DA. + // 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))); @@ -431,43 +460,42 @@ namespace storm { 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. + // 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); - } + // Add the modelState to one outgoing transition of all states of the form (Inf=lenInfSet equals not in MEC) + + // 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(); + // Add modelState to the transition from > to . + _memoryTransitions.get()[(automatonFrom * (_infSets.get().size()+1)) + infSet][(automatonTo * (_infSets.get().size()+1)) + *newInfSet].set(modelState); + + } 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); } 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. - } + 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 it = std::find(_accInfSets.get()[product->getProductStateIndex(modelState, automatonTo)].get().begin(), _accInfSets.get()[product->getProductStateIndex(modelState, automatonTo)].get().end(), infSet); + STORM_LOG_ASSERT(it != _accInfSets.get()[product->getProductStateIndex(modelState, automatonTo)].get().end(), "The list of InfSets for the product state <" < does not contain the infSet " << infSet); + it++; + if (it == _accInfSets.get()[product->getProductStateIndex(modelState, automatonTo)].get().end()) { + // Start again. + it = _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)) + *it].set(modelState); } } - } } } @@ -478,17 +506,18 @@ namespace storm { // 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 of q0) + // 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 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; - } + 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(); } } diff --git a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h index 35bcfd220..d73fe39b4 100644 --- a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h +++ b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h @@ -97,12 +97,13 @@ namespace storm { std::size_t _numberOfStates; //TODO just use _transitionMatrix.getRowGroupCount instead? // 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) + boost::optional, storm::storage::SchedulerChoice>> _productChoices; // ---> ReachChoice and ---> MecChoice + 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 stateOfInterest s its initial memory state (which memory state is reached from the initial state after reading s) - boost::optional _numberOfDaStates; + 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) }; } diff --git a/src/storm/storage/memorystructure/MemoryStructureBuilder.cpp b/src/storm/storage/memorystructure/MemoryStructureBuilder.cpp index f3a3818cc..f659e3381 100644 --- a/src/storm/storage/memorystructure/MemoryStructureBuilder.cpp +++ b/src/storm/storage/memorystructure/MemoryStructureBuilder.cpp @@ -24,7 +24,7 @@ namespace storm { STORM_LOG_THROW(model.getInitialStates().get(initialModelState), storm::exceptions::InvalidOperationException, "Invalid index of initial model state: " << initialMemoryState << ". This is not an initial state of the model."); STORM_LOG_THROW(initialMemoryState < transitions.size(), storm::exceptions::InvalidOperationException, "Invalid index of initial memory state: " << initialMemoryState << ". There are only " << transitions.size() << " states in this memory structure."); - auto initMemStateIt = initialMemoryStates.begin(); + auto initMemStateIt = initialMemoryStates.begin(); // TODO allow all for (auto initState : model.getInitialStates()) { if (initState == initialModelState) { *initMemStateIt = initialMemoryState; diff --git a/src/storm/utility/graph.cpp b/src/storm/utility/graph.cpp index d5ca015c3..76203dbe9 100644 --- a/src/storm/utility/graph.cpp +++ b/src/storm/utility/graph.cpp @@ -1893,7 +1893,6 @@ 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) ; diff --git a/src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp index ba1e350dd..683cb14c7 100755 --- a/src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp @@ -232,7 +232,7 @@ namespace { 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>(); EXPECT_EQ(inducedMdp->getNumberOfChoices(), inducedMdp->getNumberOfStates()); storm::modelchecker::SparseMdpPrctlModelChecker> inducedChecker(*inducedMdp);