From 58a4491f72ab801d1bd9f87daa988197485132af Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Wed, 17 Apr 2019 15:01:50 +0200
Subject: [PATCH] Test cases for DFT model building with relevant events

---
 .../examples/testfiles/dft/dont_care.dft      | 17 +++++
 .../storm-dft/api/DftModelBuildingTest.cpp    | 64 +++++++++++++++++++
 2 files changed, 81 insertions(+)
 create mode 100644 resources/examples/testfiles/dft/dont_care.dft
 create mode 100644 src/test/storm-dft/api/DftModelBuildingTest.cpp

diff --git a/resources/examples/testfiles/dft/dont_care.dft b/resources/examples/testfiles/dft/dont_care.dft
new file mode 100644
index 000000000..1ddf82757
--- /dev/null
+++ b/resources/examples/testfiles/dft/dont_care.dft
@@ -0,0 +1,17 @@
+toplevel "T";
+"T" and "A" "B" "C";
+"A" or "D" "E";
+"B" or "F" "G";
+"C" or "H" "I";
+"D" or "K" "M";
+"F" or "N" "O";
+"H" or "P" "Q";
+"E" lambda=9 dorm=1;
+"G" lambda=1 dorm=1;
+"I" lambda=7 dorm=1;
+"K" lambda=4 dorm=1;
+"M" lambda=5 dorm=1;
+"N" lambda=3 dorm=1;
+"O" lambda=8 dorm=1;
+"P" lambda=6 dorm=1;
+"Q" lambda=2 dorm=1;
diff --git a/src/test/storm-dft/api/DftModelBuildingTest.cpp b/src/test/storm-dft/api/DftModelBuildingTest.cpp
new file mode 100644
index 000000000..cbaa53e82
--- /dev/null
+++ b/src/test/storm-dft/api/DftModelBuildingTest.cpp
@@ -0,0 +1,64 @@
+#include "gtest/gtest.h"
+#include "storm-config.h"
+
+#include "storm-dft/api/storm-dft.h"
+#include "storm-dft/builder/ExplicitDFTModelBuilder.h"
+#include "storm-parsers/api/storm-parsers.h"
+
+namespace {
+
+    TEST(DftModelBuildingTest, RelevantEvents) {
+        // Initialize
+        std::string file = STORM_TEST_RESOURCES_DIR "/dft/dont_care.dft";
+        std::shared_ptr<storm::storage::DFT<double>> dft = storm::api::loadDFTGalileoFile<double>(file);
+        EXPECT_TRUE(storm::api::isWellFormed(*dft));
+        std::string property = "Tmin=? [F \"failed\"]";
+        std::vector<std::shared_ptr<storm::logic::Formula const>> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property));
+        std::map<size_t, std::vector<std::vector<size_t>>> emptySymmetry;
+        storm::storage::DFTIndependentSymmetries symmetries(emptySymmetry);
+        typename storm::builder::ExplicitDFTModelBuilder<double>::LabelOptions labeloptions(properties, false);
+
+
+        // Set relevant events (none)
+        std::set<size_t> relevantEvents;
+        // Build model
+        storm::builder::ExplicitDFTModelBuilder<double> builder(*dft, symmetries, relevantEvents);
+        builder.buildModel(labeloptions, 0, 0.0);
+        std::shared_ptr<storm::models::sparse::Model<double>> model = builder.getModel();
+        EXPECT_EQ(8ul, model->getNumberOfStates());
+        EXPECT_EQ(13ul, model->getNumberOfTransitions());
+
+        // Set relevant events (all)
+        relevantEvents = dft->getAllIds();
+        // Build model
+        storm::builder::ExplicitDFTModelBuilder<double> builder2(*dft, symmetries, relevantEvents);
+        builder2.buildModel(labeloptions, 0, 0.0);
+        model = builder2.getModel();
+        EXPECT_EQ(170ul, model->getNumberOfStates());
+        EXPECT_EQ(688ul, model->getNumberOfTransitions());
+
+
+        // Set relevant events (H)
+        relevantEvents.clear();
+        relevantEvents.insert(dft->getIndex("H"));
+        // Build model
+        storm::builder::ExplicitDFTModelBuilder<double> builder3(*dft, symmetries, relevantEvents);
+        builder3.buildModel(labeloptions, 0, 0.0);
+        model = builder3.getModel();
+        EXPECT_EQ(11ul, model->getNumberOfStates());
+        EXPECT_EQ(23ul, model->getNumberOfTransitions());
+
+
+        // Set relevant events (H, I)
+        relevantEvents.clear();
+        relevantEvents.insert(dft->getIndex("H"));
+        relevantEvents.insert(dft->getIndex("I"));
+        // Build model
+        storm::builder::ExplicitDFTModelBuilder<double> builder4(*dft, symmetries, relevantEvents);
+        builder4.buildModel(labeloptions, 0, 0.0);
+        model = builder4.getModel();
+        EXPECT_EQ(14ul, model->getNumberOfStates());
+        EXPECT_EQ(30ul, model->getNumberOfTransitions());
+    }
+
+}