Browse Source

build memory structure from all states

tempestpy_adaptions
hannah 3 years ago
committed by Stefan Pranger
parent
commit
6865ae1464
  1. 35
      src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp
  2. 18
      src/storm/storage/memorystructure/MemoryStructure.cpp
  3. 6
      src/storm/storage/memorystructure/MemoryStructure.h
  4. 39
      src/storm/storage/memorystructure/MemoryStructureBuilder.cpp
  5. 10
      src/storm/storage/memorystructure/MemoryStructureBuilder.h
  6. 14
      src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp
  7. 12
      src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp

35
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<ValueType>::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<ValueType>::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<std::Bitvector>> 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<std::Bitvector>>
// + 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 <automatonFrom, InfSet>> to <automatonTo, firstInfSet>.
_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.

18
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<uint_fast64_t> const& initialMemoryStates) : transitions(transitionMatrix), stateLabeling(memoryStateLabeling), initialMemoryStates(initialMemoryStates) {
MemoryStructure::MemoryStructure(TransitionMatrix const& transitionMatrix, storm::models::sparse::StateLabeling const& memoryStateLabeling, std::vector<uint_fast64_t> const& initialMemoryStates) : transitions(transitionMatrix), stateLabeling(memoryStateLabeling), initialMemoryStates(initialMemoryStates), onlyInitialStatesRelevant(true) {
// intentionally left empty
}
MemoryStructure::MemoryStructure(TransitionMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& memoryStateLabeling, std::vector<uint_fast64_t>&& initialMemoryStates) : transitions(std::move(transitionMatrix)), stateLabeling(std::move(memoryStateLabeling)), initialMemoryStates(std::move(initialMemoryStates)) {
MemoryStructure::MemoryStructure(TransitionMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& memoryStateLabeling, std::vector<uint_fast64_t>&& 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<uint_fast64_t> 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<uint_fast64_t>&& 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;
}

6
src/storm/storage/memorystructure/MemoryStructure.h

@ -37,7 +37,10 @@ namespace storm {
*/
MemoryStructure(TransitionMatrix const& transitionMatrix, storm::models::sparse::StateLabeling const& memoryStateLabeling, std::vector<uint_fast64_t> const& initialMemoryStates);
MemoryStructure(TransitionMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& memoryStateLabeling, std::vector<uint_fast64_t>&& initialMemoryStates);
MemoryStructure(TransitionMatrix const& transitionMatrix, storm::models::sparse::StateLabeling const& memoryStateLabeling, std::vector<uint_fast64_t> const& initialMemoryStates, bool onlyInitialStatesRelevant);
MemoryStructure(TransitionMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& memoryStateLabeling, std::vector<uint_fast64_t>&& initialMemoryStates, bool onlyInitialStatesRelevant);
bool IsOnlyInitialStatesRelevantSet () const;
TransitionMatrix const& getTransitionMatrix() const;
storm::models::sparse::StateLabeling const& getStateLabeling() const;
std::vector<uint_fast64_t> const& getInitialMemoryStates() const;
@ -65,6 +68,7 @@ namespace storm {
TransitionMatrix transitions;
storm::models::sparse::StateLabeling stateLabeling;
std::vector<uint_fast64_t> initialMemoryStates;
bool onlyInitialStatesRelevant; // Whether initial memory states are only defined for initial model states or for all model states
};
}

39
src/storm/storage/memorystructure/MemoryStructureBuilder.cpp

@ -10,28 +10,47 @@ namespace storm {
namespace storage {
template <typename ValueType, typename RewardModelType>
MemoryStructureBuilder<ValueType, RewardModelType>::MemoryStructureBuilder(uint_fast64_t numberOfMemoryStates, storm::models::sparse::Model<ValueType, RewardModelType> const& model) : model(model), transitions(numberOfMemoryStates, std::vector<boost::optional<storm::storage::BitVector>>(numberOfMemoryStates)), stateLabeling(numberOfMemoryStates), initialMemoryStates(model.getInitialStates().getNumberOfSetBits(), 0) {
MemoryStructureBuilder<ValueType, RewardModelType>::MemoryStructureBuilder(uint_fast64_t numberOfMemoryStates, storm::models::sparse::Model<ValueType, RewardModelType> const& model) : model(model), transitions(numberOfMemoryStates, std::vector<boost::optional<storm::storage::BitVector>>(numberOfMemoryStates)), stateLabeling(numberOfMemoryStates), initialMemoryStates(model.getInitialStates().getNumberOfSetBits(), 0), onlyInitialStatesRelevant(true) {
// Intentionally left empty
}
template <typename ValueType, typename RewardModelType>
MemoryStructureBuilder<ValueType, RewardModelType>::MemoryStructureBuilder(uint_fast64_t numberOfMemoryStates, storm::models::sparse::Model<ValueType, RewardModelType> const& model, bool onlyInitialStatesRelevant) : model(model), transitions(numberOfMemoryStates, std::vector<boost::optional<storm::storage::BitVector>>(numberOfMemoryStates)), stateLabeling(numberOfMemoryStates), initialMemoryStates(onlyInitialStatesRelevant ? model.getInitialStates().getNumberOfSetBits() : model.getNumberOfStates(), 0), onlyInitialStatesRelevant(onlyInitialStatesRelevant) {
// Intentionally left empty
}
template <typename ValueType, typename RewardModelType>
MemoryStructureBuilder<ValueType, RewardModelType>::MemoryStructureBuilder(MemoryStructure const& memoryStructure, storm::models::sparse::Model<ValueType, RewardModelType> const& model) : model(model), transitions(memoryStructure.getTransitionMatrix()), stateLabeling(memoryStructure.getStateLabeling()), initialMemoryStates(memoryStructure.getInitialMemoryStates()) {
MemoryStructureBuilder<ValueType, RewardModelType>::MemoryStructureBuilder(MemoryStructure const& memoryStructure, storm::models::sparse::Model<ValueType, RewardModelType> const& model) : model(model), transitions(memoryStructure.getTransitionMatrix()), stateLabeling(memoryStructure.getStateLabeling()), initialMemoryStates(memoryStructure.getInitialMemoryStates()), onlyInitialStatesRelevant(true) {
// Intentionally left empty
}
template <typename ValueType, typename RewardModelType>
void MemoryStructureBuilder<ValueType, RewardModelType>::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 <typename ValueType, typename RewardModelType>
MemoryStructure MemoryStructureBuilder<ValueType, RewardModelType>::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 <typename ValueType, typename RewardModelType>

10
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<ValueType, RewardModelType> 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<ValueType, RewardModelType> 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<uint_fast64_t> initialMemoryStates;
bool onlyInitialStatesRelevant;
};
}

14
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.");

12
src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp

@ -221,6 +221,7 @@ namespace {
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> 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<ValueType>()[*mdp->getInitialStates().begin()],storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
@ -243,6 +244,7 @@ namespace {
EXPECT_NEAR(this->parseNumber("81/100"), inducedResult->template asExplicitQuantitativeCheckResult<ValueType>()[*inducedMdp->getInitialStates().begin()],storm::settings::getModule<storm::settings::modules::GeneralSettings>().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<ValueType>()[*mdp->getInitialStates().begin()],storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
@ -262,6 +264,7 @@ namespace {
EXPECT_NEAR(this->parseNumber("1/2"),inducedResult->template asExplicitQuantitativeCheckResult<ValueType>()[*inducedMdp->getInitialStates().begin()],storm::settings::getModule<storm::settings::modules::GeneralSettings>().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<storm::models::sparse::Mdp<ValueType>> 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<ValueType>()[*mdp->getInitialStates().begin()],
EXPECT_NEAR(this->parseNumber("1"),result->template asExplicitQuantitativeCheckResult<ValueType>()[*mdp->getInitialStates().begin()],
storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
ASSERT_TRUE(result->template asExplicitQuantitativeCheckResult<ValueType>().hasScheduler());
storm::storage::Scheduler<ValueType> const &scheduler = result->template asExplicitQuantitativeCheckResult<ValueType>().getScheduler();
@ -324,7 +328,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("0.5"), inducedResult->template asExplicitQuantitativeCheckResult<ValueType>()[*mdp->getInitialStates().begin()], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(this->parseNumber("1"), inducedResult->template asExplicitQuantitativeCheckResult<ValueType>()[*inducedMdp->getInitialStates().begin()], storm::settings::getModule<storm::settings::modules::GeneralSettings>().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<storm::models::sparse::Mdp<ValueType>> 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<ValueType>()[*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<ValueType>().hasScheduler());

Loading…
Cancel
Save