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

updated scheduler-print and tests 

Conflicts:
	src/storm/storage/Scheduler.cpp
tempestpy_adaptions
hannah 3 years ago
committed by Stefan Pranger
parent
93c2e92c2a
commit
dd8d410748
3 changed files with 13 additions and 21 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. 2
      src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp
  2. 8
      src/storm/storage/Scheduler.cpp
  3. 24
      src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp

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

@ -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()) {
for (uint_fast64_t s0 : model.getInitialStates()) { // TODO should be relevantStates?
memoryBuilder.setInitialMemoryState(s0, this->_memoryInitialStates.get()[s0]);
}

8
src/storm/storage/Scheduler.cpp
View File

@ -145,7 +145,7 @@ namespace storm {
}
out << ":" << std::endl;
STORM_LOG_WARN_COND(!(skipUniqueChoices && model == nullptr), "Can not skip unique choices if the model is not given.");
out << std::setw(widthOfStates) << "model state:" << " " << (isMemorylessScheduler() ? "" : " memory: ") << "choice(s)" << std::endl;
out << std::setw(widthOfStates) << "model state:" << " " << (isMemorylessScheduler() ? "" : " memory: ") << "choice(s)" << (isMemorylessScheduler() ? "" : " memory updates: ") << std::endl;
for (uint_fast64_t state = 0; state < schedulerChoices.front().size(); ++state) {
std::stringstream stateString;
// Check whether the state is skipped
@ -215,11 +215,12 @@ namespace storm {
stateString << "undefined.";
}
// Print memory updates
if(!isMemorylessScheduler()) {
stateString << " ";
out << " ";
for (auto const& choiceProbPair : choice.getChoiceAsDistribution()) {
for (auto entryIt = model->getTransitionMatrix().getRow(state + choiceProbPair.first).begin(); entryIt < model->getTransitionMatrix().getRow(state + choiceProbPair.first).end(); ++entryIt) {
out << ", model state' = " << entryIt->getColumn() << ": (transition = " << state+choiceProbPair.first << ") -> " << "(m' = "<<this->memoryStructure->getSuccessorMemoryState(memoryState, entryIt - model->getTransitionMatrix().begin()) <<")";
out << ", model state' = " << entryIt->getColumn() << ": (transition = " << entryIt - model->getTransitionMatrix().begin() << ") -> " << "(m' = "<<this->memoryStructure->getSuccessorMemoryState(memoryState, entryIt - model->getTransitionMatrix().begin()) <<")";
}
}
@ -227,7 +228,6 @@ namespace storm {
stateString << std::endl;
}
// Todo: print memory updates
out << stateString.str();
out << std::endl;
}

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

@ -204,10 +204,10 @@ namespace {
}
TYPED_TEST(SchedulerGenerationMdpPrctlModelCheckerTest, ltl) {
typedef typename TestFixture::ValueType ValueType;
// TODO skip without LTL support
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);
@ -238,11 +238,8 @@ namespace {
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> inducedChecker(*inducedMdp);
auto inducedResult = inducedChecker.check(this->env(), tasks[0]);
ASSERT_TRUE(inducedResult->isExplicitQuantitativeCheckResult());
EXPECT_NEAR(this->parseNumber("9/10"),
inducedResult->template asExplicitQuantitativeCheckResult<ValueType>()[*mdp->getInitialStates().begin()], //TODO other states, too
storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(this->parseNumber("9/10"), inducedResult->template asExplicitQuantitativeCheckResult<ValueType>()[*mdp->getInitialStates().begin()],storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
}
{
auto result = checker.check(this->env(), tasks[1]);
ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
@ -256,15 +253,11 @@ namespace {
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::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> inducedChecker( *inducedMdp);
auto inducedResult = inducedChecker.check(this->env(), tasks[1]);
ASSERT_TRUE(inducedResult->isExplicitQuantitativeCheckResult());
EXPECT_NEAR(this->parseNumber("1/2"),
inducedResult->template asExplicitQuantitativeCheckResult<ValueType>()[*mdp->getInitialStates().begin()],
storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(this->parseNumber("1/2"),inducedResult->template asExplicitQuantitativeCheckResult<ValueType>()[*mdp->getInitialStates().begin()],storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
}
{
auto result = checker.check(this->env(), tasks[2]);
EXPECT_NEAR(this->parseNumber("1/2"),
@ -293,11 +286,10 @@ namespace {
}
TYPED_TEST(SchedulerGenerationMdpPrctlModelCheckerTest, ltl2) {
TYPED_TEST(SchedulerGenerationMdpPrctlModelCheckerTest, ltlMec) {
typedef typename TestFixture::ValueType ValueType;
//TODO find noMEC-scheduler-error (need nondet in EC)
// Todo unreachable Product state error
// TODO skip without LTL 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);
@ -329,7 +321,7 @@ namespace {
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> inducedChecker(*inducedMdp);
auto inducedResult = inducedChecker.check(this->env(), tasks[0]);
ASSERT_TRUE(inducedResult->isExplicitQuantitativeCheckResult());
// EXPECT_NEAR(this->parseNumber("todo"), inducedResult->template asExplicitQuantitativeCheckResult<ValueType>()[*mdp->getInitialStates().begin()], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(this->parseNumber("0.5"), inducedResult->template asExplicitQuantitativeCheckResult<ValueType>()[*mdp->getInitialStates().begin()], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
}
}

Write Preview
Loading…
Cancel
Save