From ad34cbb95175fd861f2281469012b0bdb92ebcb7 Mon Sep 17 00:00:00 2001 From: radioGiorgio Date: Wed, 24 Jul 2019 09:18:46 +0200 Subject: [PATCH] testing --- ...istic_transitions_based_memory_product.lab | 4 + ...nistic_transitions_based_memory_product.nm | 24 ++++ ...transitions_based_memory_product.trans.rew | 17 +++ ...istic_transitions_based_memory_product.tra | 18 +++ ...isticTransitionsBasedMemoryProductTest.cpp | 118 ++++++++++++++++++ 5 files changed, 181 insertions(+) create mode 100644 resources/examples/testfiles/lab/nondeterministic_transitions_based_memory_product.lab create mode 100644 resources/examples/testfiles/mdp/nondeterministic_transitions_based_memory_product.nm create mode 100644 resources/examples/testfiles/rew/nondeterministic_transitions_based_memory_product.trans.rew create mode 100644 resources/examples/testfiles/tra/nondeterministic_transitions_based_memory_product.tra create mode 100644 src/test/storm/storage/SparseModelNondeterministicTransitionsBasedMemoryProductTest.cpp diff --git a/resources/examples/testfiles/lab/nondeterministic_transitions_based_memory_product.lab b/resources/examples/testfiles/lab/nondeterministic_transitions_based_memory_product.lab new file mode 100644 index 000000000..187a60224 --- /dev/null +++ b/resources/examples/testfiles/lab/nondeterministic_transitions_based_memory_product.lab @@ -0,0 +1,4 @@ +#DECLARATION +init +#END +3 init diff --git a/resources/examples/testfiles/mdp/nondeterministic_transitions_based_memory_product.nm b/resources/examples/testfiles/mdp/nondeterministic_transitions_based_memory_product.nm new file mode 100644 index 000000000..0f596dc18 --- /dev/null +++ b/resources/examples/testfiles/mdp/nondeterministic_transitions_based_memory_product.nm @@ -0,0 +1,24 @@ +mdp + +module example + +s: [0..5] init 0; + +[a] s=0 -> 3/4: (s'=1) + 1/4: (s'=0); +[a] s=1 -> (s'=0); +[c] s=1 -> 1/2: (s'=1) + 1/3: (s'=0) + 1/6: (s'=2); +[b] s=0 -> (s'=2); +[a] s=2 -> (s'=2); +[a] s=3 -> 1/4: (s'=4) + 3/4: (s'=5); +[b] s=3 -> (s'=4); +[a] s=4 -> (s'=5); +[b] s=4 -> 2/9: (s'=3) + 7/9: (s'=5); +[c] s=4 -> 1/2: (s'=0) + 1/2: (s'=5); +[a] s=5 -> (s'=0); + +endmodule + +rewards "weights" + [a] true: 5; + [b] true: -2; +endrewards diff --git a/resources/examples/testfiles/rew/nondeterministic_transitions_based_memory_product.trans.rew b/resources/examples/testfiles/rew/nondeterministic_transitions_based_memory_product.trans.rew new file mode 100644 index 000000000..3f6cdfaeb --- /dev/null +++ b/resources/examples/testfiles/rew/nondeterministic_transitions_based_memory_product.trans.rew @@ -0,0 +1,17 @@ +0 0 1 5 +0 0 2 5 +0 1 1 2 +1 0 2 5 +1 1 0 2 +1 1 2 2 +1 2 3 0 +1 2 2 0 +2 0 3 5 +3 0 3 5 +3 0 4 5 +3 1 5 2 +4 0 3 5 +4 1 3 0 +4 1 4 0 +4 1 5 0 +5 0 5 5 \ No newline at end of file diff --git a/resources/examples/testfiles/tra/nondeterministic_transitions_based_memory_product.tra b/resources/examples/testfiles/tra/nondeterministic_transitions_based_memory_product.tra new file mode 100644 index 000000000..924adf230 --- /dev/null +++ b/resources/examples/testfiles/tra/nondeterministic_transitions_based_memory_product.tra @@ -0,0 +1,18 @@ +mdp +0 0 1 0.25 +0 0 2 0.75 +0 1 1 1 +1 0 2 1 +1 1 0 0.2222222222222222 +1 1 2 0.7777777777777777 +1 2 3 0.5 +1 2 2 0.5 +2 0 3 1 +3 0 3 0.25 +3 0 4 0.75 +3 1 5 1 +4 0 3 1 +4 1 3 0.3333333333333333 +4 1 4 0.5 +4 1 5 0.16666666666666666 +5 0 5 1 \ No newline at end of file diff --git a/src/test/storm/storage/SparseModelNondeterministicTransitionsBasedMemoryProductTest.cpp b/src/test/storm/storage/SparseModelNondeterministicTransitionsBasedMemoryProductTest.cpp new file mode 100644 index 000000000..d7f80bccd --- /dev/null +++ b/src/test/storm/storage/SparseModelNondeterministicTransitionsBasedMemoryProductTest.cpp @@ -0,0 +1,118 @@ +#include "gtest/gtest.h" +#include "storm-parsers/parser/PrismParser.h" +#include "storm/builder/ExplicitModelBuilder.h" +#include "storm/models/sparse/Mdp.h" +#include "storm-parsers/parser/NondeterministicModelParser.h" +#include "storm/storage/memorystructure/NondeterministicMemoryStructure.h" +#include "storm/storage/memorystructure/NondeterministicMemoryStructureBuilder.h" +#include "storm/storage/memorystructure/SparseModelNondeterministicTransitionsBasedMemoryProduct.h" + +TEST(SparseModelNondeterministicTransitionsBasedMemoryProduct, productStatesMapping) { + + std::string prismModelPath = STORM_TEST_RESOURCES_DIR "/mdp/nondeterministic_transitions_based_memory_product.nm"; + + storm::prism::Program program = storm::parser::PrismParser::parse(prismModelPath); + storm::builder::BuilderOptions options = storm::builder::BuilderOptions(true, true); + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, options).build(); + std::shared_ptr> mdp = model->as>(); + + storm::storage::NondeterministicMemoryStructure completeMemory = storm::storage::NondeterministicMemoryStructureBuilder().buildFullyConnectedMemory(2); + storm::storage::SparseModelNondeterministicTransitionsBasedMemoryProduct> product(*mdp, completeMemory, true); + model = product.build(); + + ASSERT_EQ(22, model->getNumberOfStates()); + // mapping between original states and memory states to product states + ASSERT_EQ(0, product.getModelState(0)); ASSERT_EQ(0, product.getMemoryState(0)); + ASSERT_EQ(0, product.getModelState(1)); ASSERT_EQ(0, product.getMemoryState(1)); + ASSERT_EQ(0, product.getModelState(2)); ASSERT_EQ(0, product.getMemoryState(2)); + ASSERT_EQ(0, product.getModelState(3)); ASSERT_EQ(0, product.getMemoryState(3)); + ASSERT_EQ(0, product.getModelState(4)); ASSERT_EQ(1, product.getMemoryState(4)); + ASSERT_EQ(0, product.getModelState(5)); ASSERT_EQ(1, product.getMemoryState(5)); + ASSERT_EQ(0, product.getModelState(6)); ASSERT_EQ(1, product.getMemoryState(6)); + ASSERT_EQ(0, product.getModelState(7)); ASSERT_EQ(1, product.getMemoryState(7)); + ASSERT_EQ(1, product.getModelState(8)); ASSERT_EQ(0, product.getMemoryState(8)); + ASSERT_EQ(1, product.getModelState(9)); ASSERT_EQ(0, product.getMemoryState(9)); + ASSERT_EQ(1, product.getModelState(10)); ASSERT_EQ(0, product.getMemoryState(10)); + ASSERT_EQ(1, product.getModelState(11)); ASSERT_EQ(0, product.getMemoryState(11)); + ASSERT_EQ(1, product.getModelState(12)); ASSERT_EQ(0, product.getMemoryState(12)); + ASSERT_EQ(1, product.getModelState(13)); ASSERT_EQ(1, product.getMemoryState(13)); + ASSERT_EQ(1, product.getModelState(14)); ASSERT_EQ(1, product.getMemoryState(14)); + ASSERT_EQ(1, product.getModelState(15)); ASSERT_EQ(1, product.getMemoryState(15)); + ASSERT_EQ(1, product.getModelState(16)); ASSERT_EQ(1, product.getMemoryState(16)); + ASSERT_EQ(1, product.getModelState(17)); ASSERT_EQ(1, product.getMemoryState(17)); + ASSERT_EQ(2, product.getModelState(18)); ASSERT_EQ(0, product.getMemoryState(18)); + ASSERT_EQ(2, product.getModelState(19)); ASSERT_EQ(0, product.getMemoryState(19)); + ASSERT_EQ(2, product.getModelState(20)); ASSERT_EQ(1, product.getMemoryState(20)); + ASSERT_EQ(2, product.getModelState(21)); ASSERT_EQ(1, product.getMemoryState(21)); + + for (uint_fast64_t state = 0; state < mdp->getNumberOfStates(); ++state) { + for (uint_fast64_t memory = 0; memory < completeMemory.getNumberOfStates(); ++memory) { + ASSERT_TRUE(product.isProductStateReachable(state, memory)); + } + } + + ASSERT_EQ(0, product.getProductState(0, 0)); + ASSERT_EQ(4, product.getProductState(0, 1)); + ASSERT_EQ(8, product.getProductState(1, 0)); + ASSERT_EQ(13, product.getProductState(1, 1)); + ASSERT_EQ(18, product.getProductState(2, 0)); + ASSERT_EQ(20, product.getProductState(2, 1)); + +} + +TEST(SparseModelNondeterministicTransitionsBasedMemoryProduct, productMappingWithUnreachableStates) { + std::string tra_file = STORM_TEST_RESOURCES_DIR "/tra/nondeterministic_transitions_based_memory_product.tra"; + std::string lab_file = STORM_TEST_RESOURCES_DIR "/lab/nondeterministic_transitions_based_memory_product.lab"; + std::string rew_file = STORM_TEST_RESOURCES_DIR "/rew/nondeterministic_transitions_based_memory_product.trans.rew"; + storm::models::sparse::Mdp mdp(storm::parser::NondeterministicModelParser<>::parseMdp(tra_file, lab_file, "", rew_file)); + storm::models::sparse::StandardRewardModel rewardModel = mdp.getUniqueRewardModel(); + rewardModel.reduceToStateBasedRewards(mdp.getTransitionMatrix()); + mdp.addRewardModel("weights", storm::models::sparse::StandardRewardModel(boost::none, rewardModel.getStateActionRewardVector())); + mdp.restrictRewardModels({"weights"}); + + storm::storage::NondeterministicMemoryStructure completeMemory = storm::storage::NondeterministicMemoryStructureBuilder().buildFullyConnectedMemory(2); + storm::storage::SparseModelNondeterministicTransitionsBasedMemoryProduct> product(mdp, completeMemory, true); + std::shared_ptr> model = product.build(); + + ASSERT_EQ(22, model->getNumberOfStates()); + // mapping between original states and memory states to product states + ASSERT_EQ(3, product.getModelState(0)); ASSERT_EQ(0, product.getMemoryState(0)); + ASSERT_EQ(3, product.getModelState(1)); ASSERT_EQ(0, product.getMemoryState(1)); + ASSERT_EQ(3, product.getModelState(2)); ASSERT_EQ(0, product.getMemoryState(2)); + ASSERT_EQ(3, product.getModelState(3)); ASSERT_EQ(0, product.getMemoryState(3)); + ASSERT_EQ(3, product.getModelState(4)); ASSERT_EQ(1, product.getMemoryState(4)); + ASSERT_EQ(3, product.getModelState(5)); ASSERT_EQ(1, product.getMemoryState(5)); + ASSERT_EQ(3, product.getModelState(6)); ASSERT_EQ(1, product.getMemoryState(6)); + ASSERT_EQ(3, product.getModelState(7)); ASSERT_EQ(1, product.getMemoryState(7)); + ASSERT_EQ(4, product.getModelState(8)); ASSERT_EQ(0, product.getMemoryState(8)); + ASSERT_EQ(4, product.getModelState(9)); ASSERT_EQ(0, product.getMemoryState(9)); + ASSERT_EQ(4, product.getModelState(10)); ASSERT_EQ(0, product.getMemoryState(10)); + ASSERT_EQ(4, product.getModelState(11)); ASSERT_EQ(0, product.getMemoryState(11)); + ASSERT_EQ(4, product.getModelState(12)); ASSERT_EQ(0, product.getMemoryState(12)); + ASSERT_EQ(4, product.getModelState(13)); ASSERT_EQ(1, product.getMemoryState(13)); + ASSERT_EQ(4, product.getModelState(14)); ASSERT_EQ(1, product.getMemoryState(14)); + ASSERT_EQ(4, product.getModelState(15)); ASSERT_EQ(1, product.getMemoryState(15)); + ASSERT_EQ(4, product.getModelState(16)); ASSERT_EQ(1, product.getMemoryState(16)); + ASSERT_EQ(4, product.getModelState(17)); ASSERT_EQ(1, product.getMemoryState(17)); + ASSERT_EQ(5, product.getModelState(18)); ASSERT_EQ(0, product.getMemoryState(18)); + ASSERT_EQ(5, product.getModelState(19)); ASSERT_EQ(0, product.getMemoryState(19)); + ASSERT_EQ(5, product.getModelState(20)); ASSERT_EQ(1, product.getMemoryState(20)); + ASSERT_EQ(5, product.getModelState(21)); ASSERT_EQ(1, product.getMemoryState(21)); + + ASSERT_FALSE(product.isProductStateReachable(0, 0)); ASSERT_FALSE(product.isProductStateReachable(2, 0)); + ASSERT_FALSE(product.isProductStateReachable(0, 1)); ASSERT_FALSE(product.isProductStateReachable(2, 1)); + ASSERT_FALSE(product.isProductStateReachable(1, 0)); + ASSERT_FALSE(product.isProductStateReachable(1, 1)); + + ASSERT_TRUE(product.isProductStateReachable(3, 0)); ASSERT_TRUE(product.isProductStateReachable(5, 0)); + ASSERT_TRUE(product.isProductStateReachable(3, 1)); ASSERT_TRUE(product.isProductStateReachable(5, 1)); + ASSERT_TRUE(product.isProductStateReachable(4, 0)); + ASSERT_TRUE(product.isProductStateReachable(4, 1)); + + ASSERT_EQ(0, product.getProductState(3, 0)); + ASSERT_EQ(4, product.getProductState(3, 1)); + ASSERT_EQ(8, product.getProductState(4, 0)); + ASSERT_EQ(13, product.getProductState(4, 1)); + ASSERT_EQ(18, product.getProductState(5, 0)); + ASSERT_EQ(20, product.getProductState(5, 1)); +}