Storm 1.13.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
BEDistributionTest.cpp
Go to the documentation of this file.
1#include "storm-config.h"
2#include "test/storm_gtest.h"
3
4#include "storm-dft/api/storm-dft.h"
5#include "storm-dft/modelchecker/SFTBDDChecker.h"
6#include "storm-parsers/api/storm-parsers.h"
7
8namespace {
9
10TEST(BEDistributionTest, ConstantFail) {
11 auto dft = storm::dft::api::loadDFTGalileoFile<double>(STORM_TEST_RESOURCES_DIR "/dft/be_fail.dft");
12 double timebound = 0.8;
13
14#ifdef STORM_HAVE_SYLVAN
15 // Perform BDD-based analysis on FT
16 auto checker = std::make_shared<storm::dft::modelchecker::SFTBDDChecker>(dft);
17 double resultBDD = checker->getProbabilityAtTimebound(timebound);
18 EXPECT_NEAR(resultBDD, 0.3296799540, 1e-10);
19#endif
20
21 // Perform Markovian analysis on FT
22 auto dft2 = storm::dft::api::prepareForMarkovAnalysis<double>(*dft);
23 EXPECT_TRUE(storm::dft::api::isWellFormed(*dft2).first);
24 std::string property = "Pmax=? [F<=" + std::to_string(timebound) + " \"failed\"]";
25 std::vector<std::shared_ptr<storm::logic::Formula const>> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property));
26 double resultMC = boost::get<double>(storm::dft::api::analyzeDFT<double>(*dft2, properties)[0]);
27 EXPECT_NEAR(resultMC, 0.3296799540, 1e-10);
28}
29
30TEST(BEDistributionTest, ConstantNonFail) {
31 auto dft = storm::dft::api::loadDFTGalileoFile<double>(STORM_TEST_RESOURCES_DIR "/dft/be_constant.dft");
32 double timebound = 0.8;
33
34#ifdef STORM_HAVE_SYLVAN
35 // Perform BDD-based analysis on FT
36 auto checker = std::make_shared<storm::dft::modelchecker::SFTBDDChecker>(dft);
37 double resultBDD = checker->getProbabilityAtTimebound(timebound);
38 EXPECT_NEAR(resultBDD, 0.9592377960, 1e-10);
39#endif
40
41 // Perform Markovian analysis on FT
42 auto dft2 = storm::dft::api::prepareForMarkovAnalysis<double>(*dft);
43 EXPECT_TRUE(storm::dft::api::isWellFormed(*dft2).first);
44 std::string property = "P=? [F<=" + std::to_string(timebound) + " \"failed\"]";
45 std::vector<std::shared_ptr<storm::logic::Formula const>> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property));
46 double resultMC = boost::get<double>(storm::dft::api::analyzeDFT<double>(*dft2, properties)[0]);
47 EXPECT_NEAR(resultMC, 0.9592377960, 1e-10);
48}
49
50TEST(BEDistributionTest, ConstantNonFail2) {
51 auto dft = storm::dft::api::loadDFTGalileoFile<double>(STORM_TEST_RESOURCES_DIR "/dft/be_nonfail2.dft");
52 double timebound = 0.8;
53
54#ifdef STORM_HAVE_SYLVAN
55 // Perform BDD-based analysis on FT
56 auto checker = std::make_shared<storm::dft::modelchecker::SFTBDDChecker>(dft);
57 double resultBDD = checker->getProbabilityAtTimebound(timebound);
58 EXPECT_EQ(resultBDD, 0);
59#endif
60
61 // Perform Markovian analysis on FT
62 auto dft2 = storm::dft::api::prepareForMarkovAnalysis<double>(*dft);
63 EXPECT_TRUE(storm::dft::api::isWellFormed(*dft2).first);
64 std::string property = "P=? [F<=" + std::to_string(timebound) + " \"failed\"]";
65 std::vector<std::shared_ptr<storm::logic::Formula const>> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property));
66 double resultMC = boost::get<double>(storm::dft::api::analyzeDFT<double>(*dft2, properties)[0]);
67 EXPECT_EQ(resultMC, 0);
68}
69
70TEST(BEDistributionTest, Probability) {
71 auto dft = storm::dft::api::loadDFTGalileoFile<double>(STORM_TEST_RESOURCES_DIR "/dft/be_probabilistic.dft");
72 double timebound = 0.8;
73
74#ifdef STORM_HAVE_SYLVAN
75 // Perform BDD-based analysis on FT
76 auto checker = std::make_shared<storm::dft::modelchecker::SFTBDDChecker>(dft);
77 double resultBDD = checker->getProbabilityAtTimebound(timebound);
78 EXPECT_NEAR(resultBDD, 0.1095403852, 1e-10);
79#endif
80
81 // Perform Markovian analysis on FT
82 auto dft2 = storm::dft::api::prepareForMarkovAnalysis<double>(*dft);
83 EXPECT_TRUE(storm::dft::api::isWellFormed(*dft2).first);
84 std::string property = "Pmax=? [F<=" + std::to_string(timebound) + " \"failed\"]";
85 std::vector<std::shared_ptr<storm::logic::Formula const>> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property));
86 double resultMC = boost::get<double>(storm::dft::api::analyzeDFT<double>(*dft2, properties)[0]);
87 EXPECT_NEAR(resultMC, 0.1095403852, 1e-10);
88}
89
90TEST(BEDistributionTest, Exponential) {
91 auto dft = storm::dft::api::loadDFTGalileoFile<double>(STORM_TEST_RESOURCES_DIR "/dft/and.dft");
92 double timebound = 0.8;
93
94#ifdef STORM_HAVE_SYLVAN
95 // Perform BDD-based analysis on FT
96 auto checker = std::make_shared<storm::dft::modelchecker::SFTBDDChecker>(dft);
97 double resultBDD = checker->getProbabilityAtTimebound(timebound);
98 EXPECT_NEAR(resultBDD, 0.108688872, 1e-10);
99#endif
100
101 // Perform Markovian analysis on FT
102 auto dft2 = storm::dft::api::prepareForMarkovAnalysis<double>(*dft);
103 EXPECT_TRUE(storm::dft::api::isWellFormed(*dft2).first);
104 std::string property = "P=? [F<=" + std::to_string(timebound) + " \"failed\"]";
105 std::vector<std::shared_ptr<storm::logic::Formula const>> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property));
106 double resultMC = boost::get<double>(storm::dft::api::analyzeDFT<double>(*dft2, properties)[0]);
107 EXPECT_NEAR(resultMC, 0.108688872, 1e-10);
108}
109
110TEST(BEDistributionTest, Erlang) {
111 auto dft = storm::dft::api::loadDFTGalileoFile<double>(STORM_TEST_RESOURCES_DIR "/dft/be_erlang.dft");
112 double timebound = 0.8;
113
114#ifdef STORM_HAVE_SYLVAN
115 // Perform BDD-based analysis on FT
116 auto checker = std::make_shared<storm::dft::modelchecker::SFTBDDChecker>(dft);
117 double resultBDD = checker->getProbabilityAtTimebound(timebound);
118 EXPECT_NEAR(resultBDD, 0.4949009834, 1e-10);
119#endif
120
121 // Perform Markovian analysis on FT
122 auto dft2 = storm::dft::api::prepareForMarkovAnalysis<double>(*dft);
123 EXPECT_TRUE(storm::dft::api::isWellFormed(*dft2).first);
124 std::string property = "P=? [F<=" + std::to_string(timebound) + " \"failed\"]";
125 std::vector<std::shared_ptr<storm::logic::Formula const>> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property));
126 double resultMC = boost::get<double>(storm::dft::api::analyzeDFT<double>(*dft2, properties)[0]);
127 EXPECT_NEAR(resultMC, 0.4949009834, 1e-10);
128}
129
130TEST(BEDistributionTest, Weibull) {
131#ifdef STORM_HAVE_SYLVAN
132 auto dft = storm::dft::api::loadDFTGalileoFile<double>(STORM_TEST_RESOURCES_DIR "/dft/be_weibull.dft");
133 double timebound = 2;
134
135 // Perform BDD-based analysis on FT
136 auto checker = std::make_shared<storm::dft::modelchecker::SFTBDDChecker>(dft);
137 double resultBDD = checker->getProbabilityAtTimebound(timebound);
138 EXPECT_NEAR(resultBDD, 0.0382982486, 1e-10);
139#else
140 GTEST_SKIP() << "Library Sylvan not available.";
141#endif
142}
143
144TEST(BEDistributionTest, LogNormal) {
145#ifdef STORM_HAVE_SYLVAN
146 auto dft = storm::dft::api::loadDFTGalileoFile<double>(STORM_TEST_RESOURCES_DIR "/dft/be_lognormal.dft");
147 double timebound = 0.8;
148
149 // Perform BDD-based analysis on FT
150 auto checker = std::make_shared<storm::dft::modelchecker::SFTBDDChecker>(dft);
151 double resultBDD = checker->getProbabilityAtTimebound(timebound);
152 EXPECT_NEAR(resultBDD, 0.2336675428, 1e-10);
153#else
154 GTEST_SKIP() << "Library Sylvan not available.";
155#endif
156}
157
158} // namespace
TEST
TEST(OrderTest, Simple)
Definition OrderTest.cpp:15
storm::api::parseProperties
std::vector< storm::jani::Property > parseProperties(storm::parser::FormulaParser &formulaParser, std::string const &inputString, boost::optional< std::set< std::string > > const &propertyFilter)
Definition properties.cpp:27
storm::api::extractFormulasFromProperties
std::vector< std::shared_ptr< storm::logic::Formula const > > extractFormulasFromProperties(std::vector< storm::jani::Property > const &properties)
Definition properties.cpp:64
storm::dft::api::analyzeDFT
storm::dft::modelchecker::DFTModelChecker< ValueType >::dft_results analyzeDFT(storm::dft::storage::DFT< ValueType > const &dft, std::vector< std::shared_ptr< storm::logic::Formula const > > const &properties, bool symred=true, bool allowModularisation=true, storm::dft::utility::RelevantEvents const &relevantEvents={}, bool allowDCForRelevant=false, double approximationError=0.0, storm::dft::builder::ApproximationHeuristic approximationHeuristic=storm::dft::builder::ApproximationHeuristic::DEPTH, bool eliminateChains=false, storm::transformer::EliminationLabelBehavior labelBehavior=storm::transformer::EliminationLabelBehavior::KeepLabels, bool printOutput=false)
Compute the exact or approximate analysis result of the given DFT according to the given properties.
Definition storm-dft.h:181
storm::dft::api::prepareForMarkovAnalysis
std::shared_ptr< storm::dft::storage::DFT< ValueType > > prepareForMarkovAnalysis(storm::dft::storage::DFT< ValueType > const &dft)
Apply transformations to make DFT feasible for Markovian analysis.
Definition storm-dft.h:119
storm::dft::api::isWellFormed
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
storm::dft::api::loadDFTGalileoFile
std::shared_ptr< storm::dft::storage::DFT< ValueType > > loadDFTGalileoFile(std::string const &file)
Load DFT from Galileo file.
Definition storm-dft.h:29
storm_gtest.h