2 changed files with 81 additions and 0 deletions
-
17resources/examples/testfiles/dft/dont_care.dft
-
64src/test/storm-dft/api/DftModelBuildingTest.cpp
@ -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; |
@ -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()); |
||||
|
} |
||||
|
|
||||
|
} |
Reference in new issue
xxxxxxxxxx