Tests for DFT simulator

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)

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<double> dftTransformator = storm::transformations::dft::DftTransformator<double>();
+        std::shared_ptr<storm::storage::DFT<double>> dft = dftTransformator.transformBinaryFDEPs(*(storm::api::loadDFTGalileoFile<double>(file)));
+        EXPECT_TRUE(storm::api::isWellFormed(*dft).first);
+
+        // Set relevant events
+        storm::utility::RelevantEvents relevantEvents = storm::api::computeRelevantEvents<double>(*dft, {}, {}, false);
+        dft->setRelevantEvents(relevantEvents);
+
+        // Find symmetries
+        std::map<size_t, std::vector<std::vector<size_t>>> 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<double> simulator(*dft, stateGenerationInfo, gen);
+        
+        size_t count = 0;;
+        bool res;
+        for (size_t i=0; i<noRuns; ++i) {
+            res = simulator.simulateCompleteTrace(timebound);
+            if (res) {
+                ++count;
+            }
+        }
+        return (double) count / noRuns;
+    }
+
+    TEST(DftSimulatorTest, And) {
+        double result = simulateDft(STORM_TEST_RESOURCES_DIR "/dft/and.dft", 2, 10000);
+        EXPECT_NEAR(result, 0.3995764009, 0.01);
+    }
+
+}

src/test/storm-dft/simulator/DftTraceGeneratorTest.cpp

@@ -0,0 +1,188 @@
+#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"
+#include "storm-dft/storage/dft/DFTIsomorphism.h"
+
+#include "storm-parsers/api/storm-parsers.h"
+
+namespace {
+
+    // Configurations for DFT traces
+    struct DftTracesConfig {
+        bool useDC;
+        bool useSR;
+    };
+
+    class NoOptimizationsConfig {
+    public:
+        typedef double ValueType;
+
+        static DftTracesConfig createConfig() {
+            return DftTracesConfig{false, false};
+        }
+    };
+
+    class DontCareConfig {
+    public:
+        typedef double ValueType;
+
+        static DftTracesConfig createConfig() {
+            return DftTracesConfig{true, false};
+        }
+    };
+
+    class SymmetryReductionConfig {
+    public:
+        typedef double ValueType;
+
+        static DftTracesConfig createConfig() {
+            return DftTracesConfig{false, true};
+        }
+    };
+
+    class AllOptimizationsConfig {
+    public:
+        typedef double ValueType;
+
+        static DftTracesConfig createConfig() {
+            return DftTracesConfig{true, true};
+        }
+    };
+
+    // General base class for testing of generating DFT traces.
+    template<typename TestType>
+    class DftTraceGeneratorTest : public ::testing::Test {
+    public:
+        typedef typename TestType::ValueType ValueType;
+
+        DftTraceGeneratorTest() : config(TestType::createConfig()) {
+        }
+
+        DftTracesConfig const& getConfig() const {
+            return config;
+        }
+
+        std::pair<std::shared_ptr<storm::storage::DFT<double>>, storm::storage::DFTStateGenerationInfo> prepareDFT(std::string const& file) {
+            // Load, build and prepare DFT
+            storm::transformations::dft::DftTransformator<double> dftTransformator = storm::transformations::dft::DftTransformator<double>();
+            std::shared_ptr<storm::storage::DFT<double>> dft = dftTransformator.transformBinaryFDEPs(*(storm::api::loadDFTGalileoFile<double>(file)));
+            EXPECT_TRUE(storm::api::isWellFormed(*dft).first);
+
+            // Compute relevant events
+            std::vector<std::string> relevantNames;
+            if (!config.useDC) {
+                relevantNames.push_back("all");
+            }
+            storm::utility::RelevantEvents relevantEvents = storm::api::computeRelevantEvents<double>(*dft, {}, relevantNames, false);
+            dft->setRelevantEvents(relevantEvents);
+
+            // Find symmetries
+            std::map<size_t, std::vector<std::vector<size_t>>> 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<double> 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<double> 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()));
+    }
+
+}

src/test/storm-dft/simulator/SamplingTest.cpp

@@ -0,0 +1,19 @@
+#include "test/storm_gtest.h"
+#include "storm-config.h"
+
+#include <storm/utility/random.h>
+
+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]);
+        }
+    }
+
+}