sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

set states to dontCare during scheduler computations, adapted Tests

tempestpy_adaptions
hannah 3 years ago
committed by Stefan Pranger
parent
f92b2104b5
commit
cceb3513ce
6 changed files with 109 additions and 116 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 5
      src/storm/automata/LTL2DeterministicAutomaton.cpp
  2. 132
      src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp
  3. 10
      src/storm/modelchecker/helper/ltl/SparseLTLHelper.h
  4. 3
      src/storm/transformer/DAProductBuilder.h
  5. 4
      src/storm/transformer/ProductBuilder.h
  6. 71
      src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp

5
src/storm/automata/LTL2DeterministicAutomaton.cpp
View File

@ -64,7 +64,6 @@ namespace storm {
#endif
}
// TODO: this is quite hacky, improve robustness
std::shared_ptr<DeterministicAutomaton> 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");

132
src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp
View File

@ -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: <s, q, InfSetID> ---> 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 <typename ValueType, bool Nondeterministic>
void SparseLTLHelper<ValueType, Nondeterministic>::createMemoryStructure(uint_fast64_t numDaStates, transformer::DAProductBuilder const& productBuilder, typename transformer::DAProduct<productModelType>::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<ValueType, Nondeterministic>::prepareScheduler(uint_fast64_t numDaStates, storm::storage::BitVector const& acceptingProductStates, std::unique_ptr<storm::storage::Scheduler<ValueType>> reachScheduler, transformer::DAProductBuilder const& productBuilder, typename transformer::DAProduct<productModelType>::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 <q, infSet>> 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 <q, infSet> 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<storm::storage::BitVector>(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 <s,q> 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: <s,q> -> 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<storm::storage::BitVector>(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 <automatonFrom, InfSet> (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: <s,q> -> 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 <s, q, infSet> 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 <s,q> not in any accEC: <s,q, REACH> ---> 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 {

10
src/storm/modelchecker/helper/ltl/SparseLTLHelper.h
View File

@ -92,11 +92,13 @@ namespace storm {
storm::storage::BitVector computeAcceptingBCCs(automata::AcceptanceCondition const& acceptance, storm::storage::SparseMatrix<ValueType> 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<productModelType>::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<storm::storage::Scheduler<ValueType>> reachScheduler, transformer::DAProductBuilder const& productBuilder, typename transformer::DAProduct<productModelType>::ptr product, storm::storage::BitVector const& modelStatesOfInterest);
storm::storage::SparseMatrix<ValueType> const& _transitionMatrix;

3
src/storm/transformer/DAProductBuilder.h
View File

@ -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));
}

4
src/storm/transformer/ProductBuilder.h
View File

@ -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;

71
src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp
View File

@ -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<storm::models::sparse::Mdp<ValueType>>();
EXPECT_EQ(inducedMdp->getNumberOfChoices(), inducedMdp->getNumberOfStates());
ASSERT_EQ(inducedModel->getType(), storm::models::ModelType::Dtmc);
auto const &inducedDtmc = inducedModel->template as<storm::models::sparse::Dtmc<ValueType>>();
EXPECT_EQ(inducedDtmc->getNumberOfChoices(), inducedDtmc->getNumberOfStates());
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> inducedChecker(*inducedMdp);
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ValueType>> inducedChecker(*inducedDtmc);
auto inducedResult = inducedChecker.check(this->env(), tasks[0]);
ASSERT_TRUE(inducedResult->isExplicitQuantitativeCheckResult());
EXPECT_NEAR(this->parseNumber("81/100"), inducedResult->template asExplicitQuantitativeCheckResult<ValueType>()[*inducedMdp->getInitialStates().begin()],storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(this->parseNumber("81/100"), inducedResult->template asExplicitQuantitativeCheckResult<ValueType>()[*inducedDtmc->getInitialStates().begin()],storm::settings::getModule<storm::settings::modules::GeneralSettings>().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<storm::models::sparse::Mdp<ValueType>>();
EXPECT_EQ(inducedMdp->getNumberOfChoices(), inducedMdp->getNumberOfStates());
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> inducedChecker(*inducedMdp);
ASSERT_EQ(inducedModel->getType(), storm::models::ModelType::Dtmc);
auto const &inducedDtmc = inducedModel->template as<storm::models::sparse::Dtmc<ValueType>>();
EXPECT_EQ(inducedDtmc->getNumberOfChoices(), inducedDtmc->getNumberOfStates());
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ValueType>> inducedChecker(*inducedDtmc);
auto inducedResult = inducedChecker.check(this->env(), tasks[1]);
ASSERT_TRUE(inducedResult->isExplicitQuantitativeCheckResult());
EXPECT_NEAR(this->parseNumber("1/2"),inducedResult->template asExplicitQuantitativeCheckResult<ValueType>()[*inducedMdp->getInitialStates().begin()],storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(this->parseNumber("1/2"),inducedResult->template asExplicitQuantitativeCheckResult<ValueType>()[*inducedDtmc->getInitialStates().begin()],storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
// TODO EXPECT_NEAR(this->parseNumber("1/2"),inducedResult->template asExplicitQuantitativeCheckResult<ValueType>()[*std::next(inducedDtmc->getInitialStates().begin())],storm::settings::getModule<storm::settings::modules::GeneralSettings>().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<storm::models::sparse::Mdp<ValueType>>();
EXPECT_EQ(inducedMdp->getNumberOfChoices(), inducedMdp->getNumberOfStates());
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> inducedChecker(
*inducedMdp);
ASSERT_EQ(inducedModel->getType(), storm::models::ModelType::Dtmc);
auto const &inducedDtmc = inducedModel->template as<storm::models::sparse::Dtmc<ValueType>>();
EXPECT_EQ(inducedDtmc->getNumberOfChoices(), inducedDtmc->getNumberOfStates());
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ValueType>> inducedChecker(*inducedDtmc);
auto inducedResult = inducedChecker.check(this->env(), tasks[2]);
ASSERT_TRUE(inducedResult->isExplicitQuantitativeCheckResult());
EXPECT_NEAR(this->parseNumber("1/2"),
inducedResult->template asExplicitQuantitativeCheckResult<ValueType>()[*inducedMdp->getInitialStates().begin()],
inducedResult->template asExplicitQuantitativeCheckResult<ValueType>()[*inducedDtmc->getInitialStates().begin()],
storm::settings::getModule<storm::settings::modules::GeneralSettings>().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<storm::models::sparse::Dtmc<ValueType>>();
EXPECT_EQ(inducedDtmc->getNumberOfChoices(), inducedDtmc->getNumberOfStates());
ASSERT_EQ(inducedModel->getType(), storm::models::ModelType::Mdp);
auto const &inducedMdp = inducedModel->template as<storm::models::sparse::Mdp<ValueType>>();
EXPECT_EQ(inducedMdp->getNumberOfChoices(), inducedMdp->getNumberOfStates());
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> inducedChecker(*inducedMdp);
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ValueType>> inducedChecker(*inducedDtmc);
auto inducedResult = inducedChecker.check(this->env(), tasks[0]);
ASSERT_TRUE(inducedResult->isExplicitQuantitativeCheckResult());
EXPECT_NEAR(this->parseNumber("1"), inducedResult->template asExplicitQuantitativeCheckResult<ValueType>()[*inducedMdp->getInitialStates().begin()], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(this->parseNumber("1"), inducedResult->template asExplicitQuantitativeCheckResult<ValueType>()[*inducedDtmc->getInitialStates().begin()], storm::settings::getModule<storm::settings::modules::GeneralSettings>().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<storm::models::sparse::Mdp<ValueType>>();
EXPECT_EQ(inducedMdp->getNumberOfChoices(), inducedMdp->getNumberOfStates());
@ -398,6 +408,9 @@ namespace {
ASSERT_TRUE(inducedResult->isExplicitQuantitativeCheckResult());
EXPECT_NEAR(this->parseNumber("1"), inducedResult->template asExplicitQuantitativeCheckResult<ValueType>()[*inducedMdp->getInitialStates().begin()], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
}
#else
GTEST_SKIP();
#endif
}
Write Preview
Loading…
Cancel
Save