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> dft = storm::api::loadDFTGalileoFile(file); + EXPECT_TRUE(storm::api::isWellFormed(*dft)); + std::string property = "Tmin=? [F \"failed\"]"; + std::vector> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property)); + std::map>> emptySymmetry; + storm::storage::DFTIndependentSymmetries symmetries(emptySymmetry); + typename storm::builder::ExplicitDFTModelBuilder::LabelOptions labeloptions(properties, false); + + + // Set relevant events (none) + std::set relevantEvents; + // Build model + storm::builder::ExplicitDFTModelBuilder builder(*dft, symmetries, relevantEvents); + builder.buildModel(labeloptions, 0, 0.0); + std::shared_ptr> 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 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 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 builder4(*dft, symmetries, relevantEvents); + builder4.buildModel(labeloptions, 0, 0.0); + model = builder4.getModel(); + EXPECT_EQ(14ul, model->getNumberOfStates()); + EXPECT_EQ(30ul, model->getNumberOfTransitions()); + } + +}