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