diff --git a/src/storm/automata/LTL2DeterministicAutomaton.cpp b/src/storm/automata/LTL2DeterministicAutomaton.cpp index 52e1192f0..e33939f7b 100644 --- a/src/storm/automata/LTL2DeterministicAutomaton.cpp +++ b/src/storm/automata/LTL2DeterministicAutomaton.cpp @@ -64,7 +64,6 @@ namespace storm { #endif } - // TODO: this is quite hacky, improve robustness std::shared_ptr LTL2DeterministicAutomaton::ltl2daExternalTool(storm::logic::Formula const& f, std::string ltl2daTool) { std::string prefixLtl = f.toPrefixString(); @@ -97,8 +96,8 @@ namespace storm { } STORM_LOG_THROW(rv == 0, storm::exceptions::FileIoException, "Could not construct deterministic automaton for " << prefixLtl << ", return code = " << rv); - // TODO transition-based acceptance is required, - // and for MDP-MC the acceptance condition must be in DNF, otherwise an exception is thrown during computation if accepting ECs + // Transition-based acceptance is required. + // For MDP-MC the acceptance condition must be in DNF, otherwise an exception is thrown during computation if accepting ECs STORM_LOG_INFO("Reading automaton for " << prefixLtl << " from da.hoa"); return DeterministicAutomaton::parseFromFile("da.hoa"); diff --git a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp index 5c86422c1..b315aa2c0 100644 --- a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp +++ b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp @@ -45,7 +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?"); + STORM_LOG_ASSERT(this->_dontCareStates.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. @@ -88,15 +88,13 @@ namespace storm { scheduler.setChoice(choice.second, modelState, (automatonState*(_infSets.get().size()+1))+ infSet); } - // todo Set don't care states + // 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"); STORM_LOG_ASSERT(!scheduler.isPartialScheduler(), "Expected a fully defined scheduler"); @@ -149,8 +147,7 @@ namespace storm { } 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 + // determine the set of states of the subMDP that can satisfy the condition, remove all states that would violate Fins in the conjunction storm::storage::BitVector allowed(transitionMatrix.getRowGroupCount(), true); STORM_LOG_INFO("Handle conjunction " << i); @@ -310,7 +307,6 @@ namespace storm { // 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 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)}); } } @@ -347,22 +343,63 @@ namespace storm { } 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) + void SparseLTLHelper::prepareScheduler(uint_fast64_t numDaStates, storm::storage::BitVector const& acceptingProductStates, std::unique_ptr> reachScheduler, transformer::DAProductBuilder const& productBuilder, typename transformer::DAProduct::ptr product, storm::storage::BitVector const& modelStatesOfInterest) { + STORM_LOG_ASSERT(this->_producedChoices.is_initialized(), "Trying to extract the produced scheduler but none is available. Was there a computation call before?"); + STORM_LOG_ASSERT(this->_infSets.is_initialized(), "Was there a computation call before?"); + STORM_LOG_ASSERT(this->_accInfSets.is_initialized(), "Was there a computation call before?"); - // Compute size of the resulting memory structure: a state 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 + // Compute size of the resulting memory structure: A state is encoded as (q* (|infSets|+1))+ |infSet| uint64 numMemoryStates = (numDaStates) * (_infSets.get().size()+1); //+1 for states outside accECs - STORM_LOG_INFO(" INF SETS: "<< (_infSets.get().size()+1)); - STORM_LOG_INFO(" INF SETS: "<< (numDaStates)); + _dontCareStates.emplace(numMemoryStates, storm::storage::BitVector(this->_transitionMatrix.getRowGroupCount(), false)); - // 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))); + // Set choices for states or consider them "dontCare" + for (storm::storage::sparse::state_type automatonState= 0; automatonState < numDaStates; ++automatonState) { + for (storm::storage::sparse::state_type modelState = 0; modelState < this->_transitionMatrix.getRowGroupCount(); ++modelState) { + if (!product->isValidProductState(modelState, automatonState)) { + // If the state does not occur in the product model, all the infSet combinations are irrelevant for the scheduler. + for (uint_fast64_t infSet = 0; infSet < _infSets.get().size()+1; ++infSet) { + _dontCareStates.get()[automatonState * (_infSets.get().size() + 1) + infSet].set(modelState, true); + } + } else { + auto pState = product->getProductStateIndex(modelState, automatonState); + if (acceptingProductStates.get(pState)) { + // For states in accepting ECs set the missing MEC-scheduler combinations are "dontCare", they are not reachable using the scheduler choices. //TODO is this correct? + for (uint_fast64_t infSet = 0; infSet < _infSets.get().size()+1; ++infSet) { + if (_producedChoices.get().find(std::make_tuple(product->getModelState(pState), product->getAutomatonState(pState), infSet)) == _producedChoices.get().end() ) { + _dontCareStates.get()[(product->getAutomatonState(pState)) * (_infSets.get().size()+1) + infSet].set(product->getModelState(pState), true); + } + } + } else { + // Extract the choices of the REACH-scheduler (choices to reach an acc. MEC) for the MDP-DA product: -> choice. The memory structure corresponds to the "last" copy of the DA (_infSets.get().size()). + this->_accInfSets.get()[pState] = {_infSets.get().size()}; + if (reachScheduler->isDontCare(pState)) { + // Mark the maybe States of the untilProbability scheduler as "dontCare" + _dontCareStates.get()[(product->getAutomatonState(pState)) * (_infSets.get().size()+1) + _infSets.get().size()].set(product->getModelState(pState), true); + } else { + // Set choice For non-accepting states that are not in any accepting EC + this->_producedChoices.get().insert({std::make_tuple(product->getModelState(pState),product->getAutomatonState(pState),_infSets.get().size()),reachScheduler->getChoice(pState)}); + }; + // All other InfSet combinations are unreachable (dontCare) + for (uint_fast64_t infSet = 0; infSet < _infSets.get().size(); ++infSet) { + _dontCareStates.get()[(product->getAutomatonState(pState)) * (_infSets.get().size()+1) + infSet].set(product->getModelState(pState), true); + + } + } + + } + } + } + + + // Prepare the memory structure. For that, we need: transitions, initialMemoryStates (and memoryStateLabeling) + + // The next move function of the memory, will be build based on the transitions of the DA and jumps between InfSets. + _memoryTransitions.emplace(numMemoryStates, std::vector(numMemoryStates, storm::storage::BitVector(_transitionMatrix.getRowGroupCount(), false))); for (storm::storage::sparse::state_type automatonFrom = 0; automatonFrom < numDaStates; ++automatonFrom) { - for (storm::storage::sparse::state_type modelState = 0; modelState < this->_transitionMatrix.getRowGroupCount(); ++modelState) { - uint_fast64_t automatonTo = productBuilder.getSuccessor(modelState, automatonFrom, modelState); //TODO remove first parameter of getSuccessor + for (storm::storage::sparse::state_type modelState = 0; modelState < _transitionMatrix.getRowGroupCount(); ++modelState) { + uint_fast64_t automatonTo = productBuilder.getSuccessor(automatonFrom, modelState); if (product->isValidProductState(modelState, automatonTo)) { // Add the modelState to one outgoing transition of all states of the form (Inf=lenInfSet equals not in MEC) @@ -377,7 +414,6 @@ namespace storm { 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)))) { @@ -407,7 +443,6 @@ namespace storm { // 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) @@ -447,7 +482,7 @@ namespace storm { if (this->hasRelevantStates()) { statesOfInterest = this->getRelevantStates(); } else { - // product from all model states + // Product from all model states statesOfInterest = storm::storage::BitVector(this->_transitionMatrix.getRowGroupCount(), true); } @@ -522,62 +557,7 @@ namespace storm { prodNumericResult = std::move(prodCheckResult.values); if (this->isProduceSchedulerSet()) { - - 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?"); - - // 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) { - - 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); - } - } - } - } - - // 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 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); - - } - } - } - - // todo extend by scheduler choices? - // todo extractSchedulerChoices() - createMemoryStructure(da.getNumberOfStates(), productBuilder, product, acceptingStates, statesOfInterest); - + prepareScheduler(da.getNumberOfStates(), acceptingStates, std::move(prodCheckResult.scheduler), productBuilder, product, statesOfInterest); } } else { diff --git a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h index fb7bf0101..8b85a07de 100644 --- a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h +++ b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h @@ -92,11 +92,13 @@ namespace storm { 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 + * Helper function, extracts scheduler choices and creates the memory structure for the LTL-Scheduler. + * @param + * @param + * @param the scheduler enuring to reach some acceptingState, defined on the model-DA product + * @param */ - 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); + void prepareScheduler(uint_fast64_t numDaStates, storm::storage::BitVector const& acceptingProductStates, std::unique_ptr> reachScheduler, transformer::DAProductBuilder const& productBuilder, typename transformer::DAProduct::ptr product, storm::storage::BitVector const& modelStatesOfInterest); storm::storage::SparseMatrix const& _transitionMatrix; diff --git a/src/storm/transformer/DAProductBuilder.h b/src/storm/transformer/DAProductBuilder.h index a6a53f9bd..c9e72331a 100644 --- a/src/storm/transformer/DAProductBuilder.h +++ b/src/storm/transformer/DAProductBuilder.h @@ -35,8 +35,7 @@ namespace storm { return da.getSuccessor(da.getInitialState(), getLabelForState(modelState)); } - storm::storage::sparse::state_type getSuccessor(storm::storage::sparse::state_type modelFrom, - storm::storage::sparse::state_type automatonFrom, + storm::storage::sparse::state_type getSuccessor(storm::storage::sparse::state_type automatonFrom, storm::storage::sparse::state_type modelTo) const { return da.getSuccessor(automatonFrom, getLabelForState(modelTo)); } diff --git a/src/storm/transformer/ProductBuilder.h b/src/storm/transformer/ProductBuilder.h index a398a1811..4be4bf045 100644 --- a/src/storm/transformer/ProductBuilder.h +++ b/src/storm/transformer/ProductBuilder.h @@ -58,7 +58,7 @@ namespace storm { typename matrix_type::const_rows row = originalMatrix.getRow(from.first); for (auto const& entry : row) { state_type t = entry.getColumn(); - state_type p = prodOp.getSuccessor(from.first, from.second, t); + state_type p = prodOp.getSuccessor(from.second, t); // std::cout << " p = " << p << "\n"; product_state_type t_p(t, p); state_type prodIndexTo; @@ -84,7 +84,7 @@ namespace storm { auto const& row = originalMatrix.getRow(from.first, i); for (auto const& entry : row) { state_type t = entry.getColumn(); - state_type p = prodOp.getSuccessor(from.first, from.second, t); + state_type p = prodOp.getSuccessor(from.second, t); // std::cout << " p = " << p << "\n"; product_state_type t_p(t, p); state_type prodIndexTo; diff --git a/src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp index 0ad528920..33f97bed2 100755 --- a/src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp @@ -11,6 +11,7 @@ #include "storm/logic/Formulas.h" #include "storm/models/sparse/StandardRewardModel.h" #include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h" +#include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/GeneralSettings.h" @@ -207,7 +208,7 @@ namespace { TYPED_TEST(SchedulerGenerationMdpPrctlModelCheckerTest, ltl) { typedef typename TestFixture::ValueType ValueType; - // TODO skip without LTL support +#ifdef STORM_HAVE_LTL_MODELCHECKING_SUPPORT std::string formulasString = "Pmax=? [X X s=0]; 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); @@ -231,17 +232,17 @@ namespace { EXPECT_TRUE(scheduler.isDeterministicScheduler()); EXPECT_TRUE(!scheduler.isMemorylessScheduler()); - EXPECT_TRUE(scheduler.isPartialScheduler()); + EXPECT_TRUE(!scheduler.isPartialScheduler()); auto inducedModel = mdp->applyScheduler(scheduler); - ASSERT_EQ(inducedModel->getType(), storm::models::ModelType::Mdp); - auto const &inducedMdp = inducedModel->template as>(); - EXPECT_EQ(inducedMdp->getNumberOfChoices(), inducedMdp->getNumberOfStates()); + ASSERT_EQ(inducedModel->getType(), storm::models::ModelType::Dtmc); + auto const &inducedDtmc = inducedModel->template as>(); + EXPECT_EQ(inducedDtmc->getNumberOfChoices(), inducedDtmc->getNumberOfStates()); - storm::modelchecker::SparseMdpPrctlModelChecker> inducedChecker(*inducedMdp); + storm::modelchecker::SparseDtmcPrctlModelChecker> inducedChecker(*inducedDtmc); auto inducedResult = inducedChecker.check(this->env(), tasks[0]); ASSERT_TRUE(inducedResult->isExplicitQuantitativeCheckResult()); - EXPECT_NEAR(this->parseNumber("81/100"), inducedResult->template asExplicitQuantitativeCheckResult()[*inducedMdp->getInitialStates().begin()],storm::settings::getModule().getPrecision()); + EXPECT_NEAR(this->parseNumber("81/100"), inducedResult->template asExplicitQuantitativeCheckResult()[*inducedDtmc->getInitialStates().begin()],storm::settings::getModule().getPrecision()); } { tasks[1].setOnlyInitialStatesRelevant(false); @@ -253,15 +254,18 @@ namespace { EXPECT_TRUE(scheduler.isDeterministicScheduler()); EXPECT_TRUE(!scheduler.isMemorylessScheduler()); - EXPECT_TRUE(scheduler.isPartialScheduler()); + EXPECT_TRUE(!scheduler.isPartialScheduler()); auto inducedModel = mdp->applyScheduler(scheduler); - ASSERT_EQ(inducedModel->getType(), storm::models::ModelType::Mdp); - auto const &inducedMdp = inducedModel->template as>(); - EXPECT_EQ(inducedMdp->getNumberOfChoices(), inducedMdp->getNumberOfStates()); - storm::modelchecker::SparseMdpPrctlModelChecker> inducedChecker(*inducedMdp); + + ASSERT_EQ(inducedModel->getType(), storm::models::ModelType::Dtmc); + auto const &inducedDtmc = inducedModel->template as>(); + EXPECT_EQ(inducedDtmc->getNumberOfChoices(), inducedDtmc->getNumberOfStates()); + + storm::modelchecker::SparseDtmcPrctlModelChecker> inducedChecker(*inducedDtmc); auto inducedResult = inducedChecker.check(this->env(), tasks[1]); ASSERT_TRUE(inducedResult->isExplicitQuantitativeCheckResult()); - EXPECT_NEAR(this->parseNumber("1/2"),inducedResult->template asExplicitQuantitativeCheckResult()[*inducedMdp->getInitialStates().begin()],storm::settings::getModule().getPrecision()); + EXPECT_NEAR(this->parseNumber("1/2"),inducedResult->template asExplicitQuantitativeCheckResult()[*inducedDtmc->getInitialStates().begin()],storm::settings::getModule().getPrecision()); + // TODO EXPECT_NEAR(this->parseNumber("1/2"),inducedResult->template asExplicitQuantitativeCheckResult()[*std::next(inducedDtmc->getInitialStates().begin())],storm::settings::getModule().getPrecision()); } { tasks[2].setOnlyInitialStatesRelevant(true); @@ -275,24 +279,27 @@ namespace { EXPECT_TRUE(scheduler.isDeterministicScheduler()); EXPECT_TRUE(!scheduler.isMemorylessScheduler()); - EXPECT_TRUE(scheduler.isPartialScheduler()); + EXPECT_TRUE(!scheduler.isPartialScheduler()); auto inducedModel = mdp->applyScheduler(scheduler); - ASSERT_EQ(inducedModel->getType(), storm::models::ModelType::Mdp); - auto const &inducedMdp = inducedModel->template as>(); - EXPECT_EQ(inducedMdp->getNumberOfChoices(), inducedMdp->getNumberOfStates()); - storm::modelchecker::SparseMdpPrctlModelChecker> inducedChecker( - *inducedMdp); + ASSERT_EQ(inducedModel->getType(), storm::models::ModelType::Dtmc); + auto const &inducedDtmc = inducedModel->template as>(); + EXPECT_EQ(inducedDtmc->getNumberOfChoices(), inducedDtmc->getNumberOfStates()); + + storm::modelchecker::SparseDtmcPrctlModelChecker> inducedChecker(*inducedDtmc); auto inducedResult = inducedChecker.check(this->env(), tasks[2]); ASSERT_TRUE(inducedResult->isExplicitQuantitativeCheckResult()); EXPECT_NEAR(this->parseNumber("1/2"), - inducedResult->template asExplicitQuantitativeCheckResult()[*inducedMdp->getInitialStates().begin()], + inducedResult->template asExplicitQuantitativeCheckResult()[*inducedDtmc->getInitialStates().begin()], storm::settings::getModule().getPrecision()); } +#else + GTEST_SKIP(); +#endif } TYPED_TEST(SchedulerGenerationMdpPrctlModelCheckerTest, ltlNondetChoice) { typedef typename TestFixture::ValueType ValueType; - // TODO skip without LTL support +#ifdef STORM_HAVE_LTL_MODELCHECKING_SUPPORT // Nondeterministic choice in an accepting EC. std::string formulasString = "Pmax=? [X X !(x=0)];"; auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/prism-mec-example1.nm", formulasString); @@ -317,26 +324,28 @@ namespace { EXPECT_TRUE(scheduler.isDeterministicScheduler()); EXPECT_TRUE(!scheduler.isMemorylessScheduler()); - EXPECT_TRUE(scheduler.isPartialScheduler()); + EXPECT_TRUE(!scheduler.isPartialScheduler()); auto inducedModel = mdp->applyScheduler(scheduler, true); + ASSERT_EQ(inducedModel->getType(), storm::models::ModelType::Dtmc); + auto const &inducedDtmc = inducedModel->template as>(); + EXPECT_EQ(inducedDtmc->getNumberOfChoices(), inducedDtmc->getNumberOfStates()); - ASSERT_EQ(inducedModel->getType(), storm::models::ModelType::Mdp); - auto const &inducedMdp = inducedModel->template as>(); - EXPECT_EQ(inducedMdp->getNumberOfChoices(), inducedMdp->getNumberOfStates()); - - storm::modelchecker::SparseMdpPrctlModelChecker> inducedChecker(*inducedMdp); + storm::modelchecker::SparseDtmcPrctlModelChecker> inducedChecker(*inducedDtmc); auto inducedResult = inducedChecker.check(this->env(), tasks[0]); ASSERT_TRUE(inducedResult->isExplicitQuantitativeCheckResult()); - EXPECT_NEAR(this->parseNumber("1"), inducedResult->template asExplicitQuantitativeCheckResult()[*inducedMdp->getInitialStates().begin()], storm::settings::getModule().getPrecision()); + EXPECT_NEAR(this->parseNumber("1"), inducedResult->template asExplicitQuantitativeCheckResult()[*inducedDtmc->getInitialStates().begin()], storm::settings::getModule().getPrecision()); } +#else + GTEST_SKIP(); +#endif } TYPED_TEST(SchedulerGenerationMdpPrctlModelCheckerTest, ltlUnsat) { typedef typename TestFixture::ValueType ValueType; - // TODO skip without LTL support +#ifdef STORM_HAVE_LTL_MODELCHECKING_SUPPORT // Nondeterministic choice in an accepting EC, Pmax unsatisfiable, Pmin tautology (compute 1-Pmax(!phi)) std::string formulasString = "Pmax=? [(X X !(s=0)) & (X X (s=0))]; Pmin=? [(X X !(s=0)) | (X X (s=0))];"; auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/scheduler_generation.nm", formulasString); @@ -364,6 +373,7 @@ namespace { EXPECT_TRUE(!scheduler.isPartialScheduler()); auto inducedModel = mdp->applyScheduler(scheduler, true); + // TODO not DTMC? ASSERT_EQ(inducedModel->getType(), storm::models::ModelType::Mdp); auto const &inducedMdp = inducedModel->template as>(); EXPECT_EQ(inducedMdp->getNumberOfChoices(), inducedMdp->getNumberOfStates()); @@ -398,6 +408,9 @@ namespace { ASSERT_TRUE(inducedResult->isExplicitQuantitativeCheckResult()); EXPECT_NEAR(this->parseNumber("1"), inducedResult->template asExplicitQuantitativeCheckResult()[*inducedMdp->getInitialStates().begin()], storm::settings::getModule().getPrecision()); } +#else + GTEST_SKIP(); +#endif }