From 5b053fa59c59a4dd01eaa6314af1f087d1733f4b Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Sun, 24 Jan 2021 23:23:20 +0100 Subject: [PATCH] Tests for DFT simulator --- src/test/storm-dft/CMakeLists.txt | 2 +- .../storm-dft/simulator/DftSimulatorTest.cpp | 49 +++++ .../simulator/DftTraceGeneratorTest.cpp | 188 ++++++++++++++++++ src/test/storm-dft/simulator/SamplingTest.cpp | 19 ++ 4 files changed, 257 insertions(+), 1 deletion(-) create mode 100644 src/test/storm-dft/simulator/DftSimulatorTest.cpp create mode 100644 src/test/storm-dft/simulator/DftTraceGeneratorTest.cpp create mode 100644 src/test/storm-dft/simulator/SamplingTest.cpp diff --git a/src/test/storm-dft/CMakeLists.txt b/src/test/storm-dft/CMakeLists.txt index a2ef04a4b..c54a09ec4 100644 --- a/src/test/storm-dft/CMakeLists.txt +++ b/src/test/storm-dft/CMakeLists.txt @@ -9,7 +9,7 @@ register_source_groups_from_filestructure("${ALL_FILES}" test) # Note that the tests also need the source files, except for the main file include_directories(${GTEST_INCLUDE_DIR}) -foreach (testsuite api storage) +foreach (testsuite api simulator storage) file(GLOB_RECURSE TEST_${testsuite}_FILES ${STORM_TESTS_BASE_PATH}/${testsuite}/*.h ${STORM_TESTS_BASE_PATH}/${testsuite}/*.cpp) add_executable (test-dft-${testsuite} ${TEST_${testsuite}_FILES} ${STORM_TESTS_BASE_PATH}/storm-test.cpp) diff --git a/src/test/storm-dft/simulator/DftSimulatorTest.cpp b/src/test/storm-dft/simulator/DftSimulatorTest.cpp new file mode 100644 index 000000000..9826c8ae3 --- /dev/null +++ b/src/test/storm-dft/simulator/DftSimulatorTest.cpp @@ -0,0 +1,49 @@ +#include "test/storm_gtest.h" +#include "storm-config.h" + +#include "storm-dft/api/storm-dft.h" +#include "storm-dft/transformations/DftTransformator.h" +#include "storm-dft/generator/DftNextStateGenerator.h" +#include "storm-dft/simulator/DFTTraceSimulator.h" +#include "storm-dft/storage/dft/SymmetricUnits.h" + + +namespace { + + // Helper function + double simulateDft(std::string const& file, double timebound, size_t noRuns) { + // Load, build and prepare DFT + storm::transformations::dft::DftTransformator dftTransformator = storm::transformations::dft::DftTransformator(); + std::shared_ptr> dft = dftTransformator.transformBinaryFDEPs(*(storm::api::loadDFTGalileoFile(file))); + EXPECT_TRUE(storm::api::isWellFormed(*dft).first); + + // Set relevant events + storm::utility::RelevantEvents relevantEvents = storm::api::computeRelevantEvents(*dft, {}, {}, false); + dft->setRelevantEvents(relevantEvents); + + // Find symmetries + std::map>> emptySymmetry; + storm::storage::DFTIndependentSymmetries symmetries(emptySymmetry); + storm::storage::DFTStateGenerationInfo stateGenerationInfo(dft->buildStateGenerationInfo(symmetries)); + + // Init random number generator + boost::mt19937 gen(5u); + storm::dft::simulator::DFTTraceSimulator simulator(*dft, stateGenerationInfo, gen); + + size_t count = 0;; + bool res; + for (size_t i=0; i + class DftTraceGeneratorTest : public ::testing::Test { + public: + typedef typename TestType::ValueType ValueType; + + DftTraceGeneratorTest() : config(TestType::createConfig()) { + } + + DftTracesConfig const& getConfig() const { + return config; + } + + std::pair>, storm::storage::DFTStateGenerationInfo> prepareDFT(std::string const& file) { + // Load, build and prepare DFT + storm::transformations::dft::DftTransformator dftTransformator = storm::transformations::dft::DftTransformator(); + std::shared_ptr> dft = dftTransformator.transformBinaryFDEPs(*(storm::api::loadDFTGalileoFile(file))); + EXPECT_TRUE(storm::api::isWellFormed(*dft).first); + + // Compute relevant events + std::vector relevantNames; + if (!config.useDC) { + relevantNames.push_back("all"); + } + storm::utility::RelevantEvents relevantEvents = storm::api::computeRelevantEvents(*dft, {}, relevantNames, false); + dft->setRelevantEvents(relevantEvents); + + // Find symmetries + std::map>> emptySymmetry; + storm::storage::DFTIndependentSymmetries symmetries(emptySymmetry); + if (config.useSR) { + auto colouring = dft->colourDFT(); + symmetries = dft->findSymmetries(colouring); + } + EXPECT_EQ(config.useSR && config.useDC, !symmetries.sortedSymmetries.empty()); + storm::storage::DFTStateGenerationInfo stateGenerationInfo(dft->buildStateGenerationInfo(symmetries)); + return std::make_pair(dft, stateGenerationInfo); + } + + private: + DftTracesConfig config; + }; + + typedef ::testing::Types< + NoOptimizationsConfig, + DontCareConfig, + SymmetryReductionConfig, + AllOptimizationsConfig + > TestingTypes; + + TYPED_TEST_SUITE(DftTraceGeneratorTest, TestingTypes,); + + TYPED_TEST(DftTraceGeneratorTest, And) { + auto pair = this->prepareDFT(STORM_TEST_RESOURCES_DIR "/dft/and.dft"); + auto dft = pair.first; + storm::generator::DftNextStateGenerator generator(*dft, pair.second); + + // Start with initial state + auto state = generator.createInitialState(); + EXPECT_FALSE(state->hasFailed(dft->getTopLevelIndex())); + + bool changed = state->orderBySymmetry(); + EXPECT_FALSE(changed); + + // Let C fail + auto iterFailable = state->getFailableElements().begin(); + ASSERT_NE(iterFailable, state->getFailableElements().end()); + ++iterFailable; + ASSERT_NE(iterFailable, state->getFailableElements().end()); + + auto nextBEPair = iterFailable.getFailBE(*dft); + auto nextBE = nextBEPair.first; + auto triggerDep = nextBEPair.second; + ASSERT_TRUE(nextBE); + ASSERT_FALSE(triggerDep); + ASSERT_EQ(nextBE->name(), "C"); + state = generator.createSuccessorState(state, nextBE, triggerDep); + EXPECT_FALSE(state->hasFailed(dft->getTopLevelIndex())); + changed = state->orderBySymmetry(); + EXPECT_EQ(this->getConfig().useSR && this->getConfig().useDC, changed); + if (this->getConfig().useSR && this->getConfig().useDC) { + EXPECT_TRUE(state->hasFailed(0)); + } else { + EXPECT_TRUE(state->hasFailed(1)); + } + + // Let B fail + iterFailable = state->getFailableElements().begin(); + ASSERT_NE(iterFailable, state->getFailableElements().end()); + + nextBEPair = iterFailable.getFailBE(*dft); + nextBE = nextBEPair.first; + triggerDep = nextBEPair.second; + ASSERT_TRUE(nextBE); + ASSERT_FALSE(triggerDep); + if (this->getConfig().useSR && this->getConfig().useDC){ + // TODO: Apply symmetry to failable elements as well + return; + ASSERT_EQ(nextBE->name(), "C"); + } else { + ASSERT_EQ(nextBE->name(), "B"); + } + state = generator.createSuccessorState(state, nextBE, triggerDep); + changed = state->orderBySymmetry(); + EXPECT_FALSE(changed); + EXPECT_TRUE(state->hasFailed(dft->getTopLevelIndex())); + } + + TYPED_TEST(DftTraceGeneratorTest, RandomStepsAnd) { + auto pair = this->prepareDFT(STORM_TEST_RESOURCES_DIR "/dft/and.dft"); + auto dft = pair.first; + + // Init random number generator + boost::mt19937 gen(5u); + storm::dft::simulator::DFTTraceSimulator simulator(*dft, pair.second, gen); + + auto state = simulator.getCurrentState(); + EXPECT_FALSE(state->hasFailed(dft->getTopLevelIndex())); + + // First random step + double timebound = simulator.randomStep(); + EXPECT_FLOAT_EQ(timebound, 0.522079); + state = simulator.getCurrentState(); + EXPECT_FALSE(state->hasFailed(dft->getTopLevelIndex())); + + timebound = simulator.randomStep(); + EXPECT_FLOAT_EQ(timebound, 0.9497214); + state = simulator.getCurrentState(); + EXPECT_TRUE(state->hasFailed(dft->getTopLevelIndex())); + } + +} diff --git a/src/test/storm-dft/simulator/SamplingTest.cpp b/src/test/storm-dft/simulator/SamplingTest.cpp new file mode 100644 index 000000000..f02ff0031 --- /dev/null +++ b/src/test/storm-dft/simulator/SamplingTest.cpp @@ -0,0 +1,19 @@ +#include "test/storm_gtest.h" +#include "storm-config.h" + +#include + +namespace { + + TEST(SamplingTest, SampleExponential) { + boost::mt19937 gen(5u); + storm::utility::ExponentialDistributionGenerator dist(5); + + // Ensure that pseudo random numbers are the same on all machines + double reference[] = {0.18241937154, 0.0522078772595, 0.0949721368604, 0.246869315378, 0.765000791199, 0.0177096648877, 0.225167598601, 0.23538530391, 1.01605360643, 0.138846355094}; + for (int i =0; i < 10; ++i) { + EXPECT_FLOAT_EQ(dist.random(gen), reference[i]); + } + } + +}