From 6865ae14640bacd54a9d609b3be49d78ca19b8fc Mon Sep 17 00:00:00 2001 From: hannah Date: Tue, 20 Jul 2021 16:31:49 +0200 Subject: [PATCH] build memory structure from all states --- .../helper/ltl/SparseLTLHelper.cpp | 35 ++++++++++------- .../memorystructure/MemoryStructure.cpp | 18 +++++++-- .../storage/memorystructure/MemoryStructure.h | 6 ++- .../MemoryStructureBuilder.cpp | 39 ++++++++++++++----- .../memorystructure/MemoryStructureBuilder.h | 10 ++++- .../SparseModelMemoryProduct.cpp | 14 +++++-- ...ulerGenerationMdpPrctlModelCheckerTest.cpp | 12 ++++-- 7 files changed, 100 insertions(+), 34 deletions(-) diff --git a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp index a6502927b..e097eaab5 100644 --- a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp +++ b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp @@ -47,8 +47,8 @@ namespace storm { 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); + // Create a memory structure for the MDP scheduler with memory. If hasRelevantStates is set, we only consider initial model states relevant. + typename storm::storage::MemoryStructureBuilder::MemoryStructureBuilder memoryBuilder(this->_memoryTransitions.get().size(), model, this->hasRelevantStates()); // Build the transitions between the memory states: startState--- modelStates (transitionVector) --->goalState for (storm::storage::sparse::state_type startState = 0; startState < this->_memoryTransitions.get().size(); ++startState) { @@ -58,11 +58,20 @@ namespace storm { } } - // initialMemoryStates: Assign an initial memory state to each initial state of the model. - for (uint_fast64_t s0 : model.getInitialStates()) { // TODO set all from _memoryInitialStates, not only modelInitial - memoryBuilder.setInitialMemoryState(s0, this->_memoryInitialStates.get()[s0]); + // initialMemoryStates: Assign an initial memory state model states + if (this->hasRelevantStates()) { + // Only consider initial model states + for (uint_fast64_t modelState : model.getInitialStates()) { + memoryBuilder.setInitialMemoryState(modelState, this->_memoryInitialStates.get()[modelState]); + } + } else { + // All model states are relevant + for (uint_fast64_t modelState = 0; modelState < model.getNumberOfStates(); ++modelState) { + memoryBuilder.setInitialMemoryState(modelState, this->_memoryInitialStates.get()[modelState]); + } } + // Now, we can build the memoryStructure. storm::storage::MemoryStructure memoryStructure = memoryBuilder.build(); @@ -79,7 +88,13 @@ namespace storm { 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(..)) + // set non-reachable (modelState,memoryState)-Pairs (i.e. those that are not contained in _productChoices) to "unreachable", + // also: states that are never reached using the scheduler + // (extend Scheduler by something like std::vector> + // + reachableSchedulerChoices; isChoiceReachable(..)) + // + change definition of partialScheduler/undefinedstates (true if there are undefined states (undefined states are always reachable)) + // + maybe states in trueUpsi are unreachable + // // Sanity check for created scheduler. STORM_LOG_ASSERT(scheduler.isDeterministicScheduler(), "Expected a deterministic scheduler"); @@ -471,13 +486,7 @@ namespace storm { 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(); - - // todo Never switch from NoMc to Mec? - //if (*newInfSet != _infSets.get().size() ){ - // Add modelState to the transition from > to . - _memoryTransitions.get()[(automatonFrom * (_infSets.get().size()+1)) + infSet][(automatonTo * (_infSets.get().size()+1)) + *newInfSet].set(modelState); - // } - + _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. diff --git a/src/storm/storage/memorystructure/MemoryStructure.cpp b/src/storm/storage/memorystructure/MemoryStructure.cpp index 83bc7ad81..6103c05dd 100644 --- a/src/storm/storage/memorystructure/MemoryStructure.cpp +++ b/src/storm/storage/memorystructure/MemoryStructure.cpp @@ -11,14 +11,26 @@ namespace storm { namespace storage { - MemoryStructure::MemoryStructure(TransitionMatrix const& transitionMatrix, storm::models::sparse::StateLabeling const& memoryStateLabeling, std::vector const& initialMemoryStates) : transitions(transitionMatrix), stateLabeling(memoryStateLabeling), initialMemoryStates(initialMemoryStates) { + MemoryStructure::MemoryStructure(TransitionMatrix const& transitionMatrix, storm::models::sparse::StateLabeling const& memoryStateLabeling, std::vector const& initialMemoryStates) : transitions(transitionMatrix), stateLabeling(memoryStateLabeling), initialMemoryStates(initialMemoryStates), onlyInitialStatesRelevant(true) { // intentionally left empty } - MemoryStructure::MemoryStructure(TransitionMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& memoryStateLabeling, std::vector&& initialMemoryStates) : transitions(std::move(transitionMatrix)), stateLabeling(std::move(memoryStateLabeling)), initialMemoryStates(std::move(initialMemoryStates)) { + MemoryStructure::MemoryStructure(TransitionMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& memoryStateLabeling, std::vector&& initialMemoryStates) : transitions(std::move(transitionMatrix)), stateLabeling(std::move(memoryStateLabeling)), initialMemoryStates(std::move(initialMemoryStates)), onlyInitialStatesRelevant(true) { // intentionally left empty } - + + MemoryStructure::MemoryStructure(TransitionMatrix const& transitionMatrix, storm::models::sparse::StateLabeling const& memoryStateLabeling, std::vector const& initialMemoryStates, bool onlyInitialStatesRelevant) : transitions(transitionMatrix), stateLabeling(memoryStateLabeling), initialMemoryStates(initialMemoryStates), onlyInitialStatesRelevant(onlyInitialStatesRelevant) { + // intentionally left empty + } + + MemoryStructure::MemoryStructure(TransitionMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& memoryStateLabeling, std::vector&& initialMemoryStates, bool onlyInitialStatesRelevant) : transitions(std::move(transitionMatrix)), stateLabeling(std::move(memoryStateLabeling)), initialMemoryStates(std::move(initialMemoryStates)), onlyInitialStatesRelevant(onlyInitialStatesRelevant) { + // intentionally left empty + } + + bool MemoryStructure::IsOnlyInitialStatesRelevantSet() const { + return onlyInitialStatesRelevant; + } + MemoryStructure::TransitionMatrix const& MemoryStructure::getTransitionMatrix() const { return transitions; } diff --git a/src/storm/storage/memorystructure/MemoryStructure.h b/src/storm/storage/memorystructure/MemoryStructure.h index c1a255f29..2476a4e63 100644 --- a/src/storm/storage/memorystructure/MemoryStructure.h +++ b/src/storm/storage/memorystructure/MemoryStructure.h @@ -37,7 +37,10 @@ namespace storm { */ MemoryStructure(TransitionMatrix const& transitionMatrix, storm::models::sparse::StateLabeling const& memoryStateLabeling, std::vector const& initialMemoryStates); MemoryStructure(TransitionMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& memoryStateLabeling, std::vector&& initialMemoryStates); - + MemoryStructure(TransitionMatrix const& transitionMatrix, storm::models::sparse::StateLabeling const& memoryStateLabeling, std::vector const& initialMemoryStates, bool onlyInitialStatesRelevant); + MemoryStructure(TransitionMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& memoryStateLabeling, std::vector&& initialMemoryStates, bool onlyInitialStatesRelevant); + + bool IsOnlyInitialStatesRelevantSet () const; TransitionMatrix const& getTransitionMatrix() const; storm::models::sparse::StateLabeling const& getStateLabeling() const; std::vector const& getInitialMemoryStates() const; @@ -65,6 +68,7 @@ namespace storm { TransitionMatrix transitions; storm::models::sparse::StateLabeling stateLabeling; std::vector initialMemoryStates; + bool onlyInitialStatesRelevant; // Whether initial memory states are only defined for initial model states or for all model states }; } diff --git a/src/storm/storage/memorystructure/MemoryStructureBuilder.cpp b/src/storm/storage/memorystructure/MemoryStructureBuilder.cpp index f659e3381..859a92635 100644 --- a/src/storm/storage/memorystructure/MemoryStructureBuilder.cpp +++ b/src/storm/storage/memorystructure/MemoryStructureBuilder.cpp @@ -10,28 +10,47 @@ namespace storm { namespace storage { template - MemoryStructureBuilder::MemoryStructureBuilder(uint_fast64_t numberOfMemoryStates, storm::models::sparse::Model const& model) : model(model), transitions(numberOfMemoryStates, std::vector>(numberOfMemoryStates)), stateLabeling(numberOfMemoryStates), initialMemoryStates(model.getInitialStates().getNumberOfSetBits(), 0) { + MemoryStructureBuilder::MemoryStructureBuilder(uint_fast64_t numberOfMemoryStates, storm::models::sparse::Model const& model) : model(model), transitions(numberOfMemoryStates, std::vector>(numberOfMemoryStates)), stateLabeling(numberOfMemoryStates), initialMemoryStates(model.getInitialStates().getNumberOfSetBits(), 0), onlyInitialStatesRelevant(true) { + // Intentionally left empty + } + + template + MemoryStructureBuilder::MemoryStructureBuilder(uint_fast64_t numberOfMemoryStates, storm::models::sparse::Model const& model, bool onlyInitialStatesRelevant) : model(model), transitions(numberOfMemoryStates, std::vector>(numberOfMemoryStates)), stateLabeling(numberOfMemoryStates), initialMemoryStates(onlyInitialStatesRelevant ? model.getInitialStates().getNumberOfSetBits() : model.getNumberOfStates(), 0), onlyInitialStatesRelevant(onlyInitialStatesRelevant) { // Intentionally left empty } template - MemoryStructureBuilder::MemoryStructureBuilder(MemoryStructure const& memoryStructure, storm::models::sparse::Model const& model) : model(model), transitions(memoryStructure.getTransitionMatrix()), stateLabeling(memoryStructure.getStateLabeling()), initialMemoryStates(memoryStructure.getInitialMemoryStates()) { + MemoryStructureBuilder::MemoryStructureBuilder(MemoryStructure const& memoryStructure, storm::models::sparse::Model const& model) : model(model), transitions(memoryStructure.getTransitionMatrix()), stateLabeling(memoryStructure.getStateLabeling()), initialMemoryStates(memoryStructure.getInitialMemoryStates()), onlyInitialStatesRelevant(true) { // Intentionally left empty } + template void MemoryStructureBuilder::setInitialMemoryState(uint_fast64_t initialModelState, uint_fast64_t initialMemoryState) { - 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(!onlyInitialStatesRelevant || 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(); // TODO allow all - for (auto initState : model.getInitialStates()) { - if (initState == initialModelState) { - *initMemStateIt = initialMemoryState; - break; + auto initMemStateIt = initialMemoryStates.begin(); + + if (onlyInitialStatesRelevant) { + for (auto initState : model.getInitialStates()) { + if (initState == initialModelState) { + *initMemStateIt = initialMemoryState; + break; + } + ++initMemStateIt; + } + } else { + // Consider non-initial model states + for (uint_fast64_t state = 0; state < model.getNumberOfStates(); ++state) { + if (state == initialModelState) { + *initMemStateIt = initialMemoryState; + break; + } + ++initMemStateIt; } - ++initMemStateIt; } + assert(initMemStateIt != initialMemoryStates.end()); } @@ -85,7 +104,7 @@ namespace storm { template MemoryStructure MemoryStructureBuilder::build() { - return MemoryStructure(std::move(transitions), std::move(stateLabeling), std::move(initialMemoryStates)); + return MemoryStructure(std::move(transitions), std::move(stateLabeling), std::move(initialMemoryStates), onlyInitialStatesRelevant); } template diff --git a/src/storm/storage/memorystructure/MemoryStructureBuilder.h b/src/storm/storage/memorystructure/MemoryStructureBuilder.h index 0b3c6e9cf..1d067a4bc 100644 --- a/src/storm/storage/memorystructure/MemoryStructureBuilder.h +++ b/src/storm/storage/memorystructure/MemoryStructureBuilder.h @@ -19,7 +19,14 @@ namespace storm { * @param numberOfMemoryStates The number of states the resulting memory structure should have */ MemoryStructureBuilder(uint_fast64_t numberOfMemoryStates, storm::models::sparse::Model const& model); - // TODO: Add variant with a flag: Consider non-initial model states + + /*! + * Initializes a new builder with the data from the provided memory structure + * @param numberOfMemoryStates The number of states the resulting memory structure should have + * @param allModelStatesRelevant Consider non-initial model states + */ + MemoryStructureBuilder(uint_fast64_t numberOfMemoryStates, storm::models::sparse::Model const& model, bool onlyInitialStatesRelevant); + /*! * Initializes a new builder with the data from the provided memory structure */ @@ -73,6 +80,7 @@ namespace storm { MemoryStructure::TransitionMatrix transitions; storm::models::sparse::StateLabeling stateLabeling; std::vector initialMemoryStates; + bool onlyInitialStatesRelevant; }; } diff --git a/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp b/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp index 029387288..fd9163fa5 100644 --- a/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp +++ b/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp @@ -38,9 +38,17 @@ namespace storm { // Get the initial states and reachable states. A stateIndex s corresponds to the model state (s / memoryStateCount) and memory state (s % memoryStateCount) storm::storage::BitVector initialStates(modelStateCount * memoryStateCount, false); auto memoryInitIt = memory.getInitialMemoryStates().begin(); - for (auto modelInit : model.getInitialStates()) { - initialStates.set(modelInit * memoryStateCount + *memoryInitIt, true); - ++memoryInitIt; + if (memory.IsOnlyInitialStatesRelevantSet()) { + for (auto modelInit : model.getInitialStates()) { + initialStates.set(modelInit * memoryStateCount + *memoryInitIt, true); + ++memoryInitIt; + } + } else { + // Build Product from all model states + for (uint_fast64_t modelState = 0; modelState < model.getNumberOfStates(); ++modelState) { + initialStates.set(modelState * memoryStateCount + *memoryInitIt, true); + ++memoryInitIt; + } } STORM_LOG_ASSERT(memoryInitIt == memory.getInitialMemoryStates().end(), "Unexpected number of initial states."); diff --git a/src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp index e7ee44930..cddf22db4 100755 --- a/src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp @@ -221,6 +221,7 @@ namespace { storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp); { + tasks[0].setOnlyInitialStatesRelevant(true); // TODO for false, but need equivalent inducedModel state for model state auto result = checker.check(this->env(), tasks[0]); ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); EXPECT_NEAR(this->parseNumber("81/100"), result->template asExplicitQuantitativeCheckResult()[*mdp->getInitialStates().begin()],storm::settings::getModule().getPrecision()); @@ -243,6 +244,7 @@ namespace { EXPECT_NEAR(this->parseNumber("81/100"), inducedResult->template asExplicitQuantitativeCheckResult()[*inducedMdp->getInitialStates().begin()],storm::settings::getModule().getPrecision()); } { + tasks[1].setOnlyInitialStatesRelevant(true); auto result = checker.check(this->env(), tasks[1]); ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); EXPECT_NEAR(this->parseNumber("1/2"), result->template asExplicitQuantitativeCheckResult()[*mdp->getInitialStates().begin()],storm::settings::getModule().getPrecision()); @@ -262,6 +264,7 @@ namespace { EXPECT_NEAR(this->parseNumber("1/2"),inducedResult->template asExplicitQuantitativeCheckResult()[*inducedMdp->getInitialStates().begin()],storm::settings::getModule().getPrecision()); } { + tasks[2].setOnlyInitialStatesRelevant(true); auto result = checker.check(this->env(), tasks[2]); ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); EXPECT_NEAR(this->parseNumber("1/2"), @@ -304,9 +307,10 @@ namespace { storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp); { + tasks[0].setOnlyInitialStatesRelevant(true); auto result = checker.check(this->env(), tasks[0]); ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); - EXPECT_NEAR(this->parseNumber("0.5"),result->template asExplicitQuantitativeCheckResult()[*mdp->getInitialStates().begin()], + EXPECT_NEAR(this->parseNumber("1"),result->template asExplicitQuantitativeCheckResult()[*mdp->getInitialStates().begin()], storm::settings::getModule().getPrecision()); ASSERT_TRUE(result->template asExplicitQuantitativeCheckResult().hasScheduler()); storm::storage::Scheduler const &scheduler = result->template asExplicitQuantitativeCheckResult().getScheduler(); @@ -324,7 +328,7 @@ namespace { storm::modelchecker::SparseMdpPrctlModelChecker> inducedChecker(*inducedMdp); auto inducedResult = inducedChecker.check(this->env(), tasks[0]); ASSERT_TRUE(inducedResult->isExplicitQuantitativeCheckResult()); - EXPECT_NEAR(this->parseNumber("0.5"), inducedResult->template asExplicitQuantitativeCheckResult()[*mdp->getInitialStates().begin()], storm::settings::getModule().getPrecision()); + EXPECT_NEAR(this->parseNumber("1"), inducedResult->template asExplicitQuantitativeCheckResult()[*inducedMdp->getInitialStates().begin()], storm::settings::getModule().getPrecision()); } } @@ -335,7 +339,7 @@ namespace { // TODO skip without LTL 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); + 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); @@ -347,6 +351,7 @@ namespace { storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp); { + tasks[0].setOnlyInitialStatesRelevant(true); auto result = checker.check(this->env(), tasks[0]); ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); EXPECT_NEAR(this->parseNumber("0"),result->template asExplicitQuantitativeCheckResult()[*mdp->getInitialStates().begin()], @@ -370,6 +375,7 @@ namespace { } { + tasks[1].setOnlyInitialStatesRelevant(true); auto result = checker.check(this->env(), tasks[1]); ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); ASSERT_TRUE(result->template asExplicitQuantitativeCheckResult().hasScheduler());