Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
DftParserTest.cpp
Go to the documentation of this file.
1#include "storm-config.h"
2#include "test/storm_gtest.h"
3
6
7namespace {
8
9TEST(DftParserTest, LoadFromGalileoFile) {
10 std::string file = STORM_TEST_RESOURCES_DIR "/dft/and.dft";
11 std::shared_ptr<storm::dft::storage::DFT<double>> dft = storm::dft::api::loadDFTGalileoFile<double>(file);
12 EXPECT_EQ(3ul, dft->nrElements());
13 EXPECT_EQ(2ul, dft->nrBasicElements());
14 EXPECT_TRUE(storm::dft::api::isWellFormed(*dft).first);
15}
16
17TEST(DftParserTest, LoadFromJsonFile) {
18 std::string file = STORM_TEST_RESOURCES_DIR "/dft/and.json";
19 std::shared_ptr<storm::dft::storage::DFT<double>> dft = storm::dft::api::loadDFTJsonFile<double>(file);
20 EXPECT_EQ(3ul, dft->nrElements());
21 EXPECT_EQ(2ul, dft->nrBasicElements());
22 EXPECT_TRUE(storm::dft::api::isWellFormed(*dft).first);
23}
24
25TEST(DftParserTest, LoadAllBeDistributionsFromGalileoFile) {
26 std::string file = STORM_TEST_RESOURCES_DIR "/dft/all_be_distributions.dft";
27 std::shared_ptr<storm::dft::storage::DFT<double>> dft = storm::dft::api::loadDFTGalileoFile<double>(file);
28 EXPECT_EQ(8ul, dft->nrElements());
29 EXPECT_EQ(7ul, dft->nrBasicElements());
30 EXPECT_TRUE(storm::dft::api::isWellFormed(*dft, false).first);
31 EXPECT_EQ(storm::dft::storage::elements::BEType::CONSTANT, dft->getBasicElement(dft->getIndex("A"))->beType());
32 EXPECT_EQ(storm::dft::storage::elements::BEType::CONSTANT, dft->getBasicElement(dft->getIndex("B"))->beType());
33 EXPECT_EQ(storm::dft::storage::elements::BEType::PROBABILITY, dft->getBasicElement(dft->getIndex("C"))->beType());
34 EXPECT_EQ(storm::dft::storage::elements::BEType::EXPONENTIAL, dft->getBasicElement(dft->getIndex("D"))->beType());
35 EXPECT_EQ(storm::dft::storage::elements::BEType::ERLANG, dft->getBasicElement(dft->getIndex("E"))->beType());
36 EXPECT_EQ(storm::dft::storage::elements::BEType::LOGNORMAL, dft->getBasicElement(dft->getIndex("F"))->beType());
37 EXPECT_EQ(storm::dft::storage::elements::BEType::WEIBULL, dft->getBasicElement(dft->getIndex("G"))->beType());
38}
39
40TEST(DftParserTest, LoadAllGatesFromGalileoFile) {
41 std::string file = STORM_TEST_RESOURCES_DIR "/dft/all_gates.dft";
42 std::shared_ptr<storm::dft::storage::DFT<double>> dft = storm::dft::api::loadDFTGalileoFile<double>(file);
43 EXPECT_EQ(42ul, dft->nrElements());
44 EXPECT_EQ(19ul, dft->nrBasicElements());
45 EXPECT_EQ(5ul, dft->nrStaticElements());
46 EXPECT_EQ(18ul, dft->nrDynamicElements());
47 EXPECT_TRUE(storm::dft::api::isWellFormed(*dft).first);
48}
49
50TEST(DftParserTest, LoadAllBEDistributionsFromJsonFile) {
51 std::string file = STORM_TEST_RESOURCES_DIR "/dft/all_be_distributions.json";
52 std::shared_ptr<storm::dft::storage::DFT<double>> dft = storm::dft::api::loadDFTJsonFile<double>(file);
53 EXPECT_EQ(8ul, dft->nrElements());
54 EXPECT_EQ(7ul, dft->nrBasicElements());
55 EXPECT_TRUE(storm::dft::api::isWellFormed(*dft, false).first);
56 EXPECT_EQ(storm::dft::storage::elements::BEType::CONSTANT, dft->getBasicElement(dft->getIndex("A"))->beType());
57 EXPECT_EQ(storm::dft::storage::elements::BEType::CONSTANT, dft->getBasicElement(dft->getIndex("B"))->beType());
58 EXPECT_EQ(storm::dft::storage::elements::BEType::PROBABILITY, dft->getBasicElement(dft->getIndex("C"))->beType());
59 EXPECT_EQ(storm::dft::storage::elements::BEType::EXPONENTIAL, dft->getBasicElement(dft->getIndex("D"))->beType());
60 EXPECT_EQ(storm::dft::storage::elements::BEType::ERLANG, dft->getBasicElement(dft->getIndex("E"))->beType());
61 EXPECT_EQ(storm::dft::storage::elements::BEType::LOGNORMAL, dft->getBasicElement(dft->getIndex("F"))->beType());
62 EXPECT_EQ(storm::dft::storage::elements::BEType::WEIBULL, dft->getBasicElement(dft->getIndex("G"))->beType());
63}
64
65TEST(DftParserTest, LoadAllGatesFromJsonFile) {
66 std::string file = STORM_TEST_RESOURCES_DIR "/dft/all_gates.json";
67 std::shared_ptr<storm::dft::storage::DFT<double>> dft = storm::dft::api::loadDFTJsonFile<double>(file);
68 EXPECT_EQ(42ul, dft->nrElements());
69 EXPECT_EQ(19ul, dft->nrBasicElements());
70 EXPECT_EQ(5ul, dft->nrStaticElements());
71 EXPECT_EQ(18ul, dft->nrDynamicElements());
72 EXPECT_TRUE(storm::dft::api::isWellFormed(*dft).first);
73}
74
75TEST(DftParserTest, CatchCycles) {
76 std::string file = STORM_TEST_RESOURCES_DIR "/dft/cyclic.dft";
77 STORM_SILENT_EXPECT_THROW(storm::dft::api::loadDFTGalileoFile<double>(file), storm::exceptions::WrongFormatException);
78}
79
80TEST(DftParserTest, LoadSeqChildren) {
81 std::string file = STORM_TEST_RESOURCES_DIR "/dft/seqChild.dft";
82 std::shared_ptr<storm::dft::storage::DFT<double>> dft = storm::dft::api::loadDFTGalileoFile<double>(file);
83 EXPECT_EQ(4ul, dft->nrElements());
84 EXPECT_EQ(2ul, dft->nrBasicElements());
85 EXPECT_TRUE(storm::dft::api::isWellFormed(*dft).first);
86}
87
88TEST(DftParserTest, LoadParametricFromGalileoFile) {
89 std::string file = STORM_TEST_RESOURCES_DIR "/dft/and_param.dft";
90 std::shared_ptr<storm::dft::storage::DFT<storm::RationalFunction>> dft = storm::dft::api::loadDFTGalileoFile<storm::RationalFunction>(file);
91 EXPECT_EQ(3ul, dft->nrElements());
92 EXPECT_EQ(2ul, dft->nrBasicElements());
93 EXPECT_TRUE(storm::dft::api::isWellFormed(*dft).first);
94 auto parameters = storm::dft::storage::getParameters(*dft);
95 EXPECT_TRUE(parameters.size() == 1);
96 auto it = std::find_if(parameters.begin(), parameters.end(), [](storm::RationalFunctionVariable const& x) { return x.name() == "x"; });
97 EXPECT_TRUE(it != parameters.end());
98}
99
100TEST(DftParserTest, LoadParametricFromJsonFile) {
101 std::string file = STORM_TEST_RESOURCES_DIR "/dft/and_param.json";
102 std::shared_ptr<storm::dft::storage::DFT<storm::RationalFunction>> dft = storm::dft::api::loadDFTJsonFile<storm::RationalFunction>(file);
103 EXPECT_EQ(3ul, dft->nrElements());
104 EXPECT_EQ(2ul, dft->nrBasicElements());
105 EXPECT_TRUE(storm::dft::api::isWellFormed(*dft).first);
106 auto parameters = storm::dft::storage::getParameters(*dft);
107 EXPECT_TRUE(parameters.size() == 1);
108 auto it = std::find_if(parameters.begin(), parameters.end(), [](storm::RationalFunctionVariable const& x) { return x.name() == "x"; });
109 EXPECT_TRUE(it != parameters.end());
110}
111} // namespace
TEST(OrderTest, Simple)
Definition OrderTest.cpp:8
std::pair< bool, std::string > isWellFormed(storm::dft::storage::DFT< ValueType > const &dft, bool validForMarkovianAnalysis=true)
Check whether the DFT is well-formed.
Definition storm-dft.h:64
std::set< storm::RationalFunctionVariable > getParameters(DFT< storm::RationalFunction > const &dft)
Get all rate/probability parameters occurring in the DFT.
Definition DFT.cpp:825
carl::Variable RationalFunctionVariable
#define STORM_SILENT_EXPECT_THROW(statement, expected_exception)