Storm 1.14.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/analysis.h"
5#include "storm-dft/api/io.h"
6#include "storm-dft/api/transformation.h"
7#include "storm-dft/environment/AnalysisEnvironment.h"
8#include "storm-dft/environment/DftEnvironment.h"
9#include "storm-dft/modelchecker/SFTBDDChecker.h"
10#include "storm-parsers/api/properties.h"
11#include "storm/api/properties.h"
12#include "storm/storage/jani/Property.h"
13
14namespace {
15
16TEST(BEDistributionTest, ConstantFail) {
17 auto dft = storm::dft::api::loadDFTGalileoFile<double>(STORM_TEST_RESOURCES_DIR "/dft/be_fail.dft");
18 double timebound = 0.8;
19
20#ifdef STORM_HAVE_SYLVAN
21 // Perform BDD-based analysis on FT
22 storm::Environment env;
23 auto checker = std::make_shared<storm::dft::modelchecker::SFTBDDChecker>(dft, std::make_shared<storm::dft::storage::SylvanBddManager>(env));
24 double resultBDD = checker->getProbabilityAtTimebound(timebound);
25 EXPECT_NEAR(resultBDD, 0.3296799540, 1e-10);
26#endif
27
28 // Perform Markovian analysis on FT
29 auto dft2 = storm::dft::api::prepareForMarkovAnalysis<double>(*dft);
30 EXPECT_TRUE(storm::dft::api::isWellFormed(*dft2).first);
31 std::string property = "Pmax=? [F<=" + std::to_string(timebound) + " \"failed\"]";
32 std::vector<std::shared_ptr<storm::logic::Formula const>> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property));
33 storm::dft::DftEnvironment dftEnv;
34 double resultMC = boost::get<double>(storm::dft::api::analyzeDFT<double>(dftEnv, *dft2, properties)[0]);
35 EXPECT_NEAR(resultMC, 0.3296799540, 1e-10);
36}
37
38TEST(BEDistributionTest, ConstantNonFail) {
39 auto dft = storm::dft::api::loadDFTGalileoFile<double>(STORM_TEST_RESOURCES_DIR "/dft/be_constant.dft");
40 double timebound = 0.8;
41
42#ifdef STORM_HAVE_SYLVAN
43 // Perform BDD-based analysis on FT
44 storm::Environment env;
45 auto checker = std::make_shared<storm::dft::modelchecker::SFTBDDChecker>(dft, std::make_shared<storm::dft::storage::SylvanBddManager>(env));
46 double resultBDD = checker->getProbabilityAtTimebound(timebound);
47 EXPECT_NEAR(resultBDD, 0.9592377960, 1e-10);
48#endif
49
50 // Perform Markovian analysis on FT
51 auto dft2 = storm::dft::api::prepareForMarkovAnalysis<double>(*dft);
52 EXPECT_TRUE(storm::dft::api::isWellFormed(*dft2).first);
53 std::string property = "P=? [F<=" + std::to_string(timebound) + " \"failed\"]";
54 std::vector<std::shared_ptr<storm::logic::Formula const>> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property));
55 storm::dft::DftEnvironment dftEnv;
56 double resultMC = boost::get<double>(storm::dft::api::analyzeDFT<double>(dftEnv, *dft2, properties)[0]);
57 EXPECT_NEAR(resultMC, 0.9592377960, 1e-10);
58}
59
60TEST(BEDistributionTest, ConstantNonFail2) {
61 auto dft = storm::dft::api::loadDFTGalileoFile<double>(STORM_TEST_RESOURCES_DIR "/dft/be_nonfail2.dft");
62 double timebound = 0.8;
63
64#ifdef STORM_HAVE_SYLVAN
65 // Perform BDD-based analysis on FT
66 storm::Environment env;
67 auto checker = std::make_shared<storm::dft::modelchecker::SFTBDDChecker>(dft, std::make_shared<storm::dft::storage::SylvanBddManager>(env));
68 double resultBDD = checker->getProbabilityAtTimebound(timebound);
69 EXPECT_EQ(resultBDD, 0);
70#endif
71
72 // Perform Markovian analysis on FT
73 auto dft2 = storm::dft::api::prepareForMarkovAnalysis<double>(*dft);
74 EXPECT_TRUE(storm::dft::api::isWellFormed(*dft2).first);
75 std::string property = "P=? [F<=" + std::to_string(timebound) + " \"failed\"]";
76 std::vector<std::shared_ptr<storm::logic::Formula const>> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property));
77 storm::dft::DftEnvironment dftEnv;
78 double resultMC = boost::get<double>(storm::dft::api::analyzeDFT<double>(dftEnv, *dft2, properties)[0]);
79 EXPECT_EQ(resultMC, 0);
80}
81
82TEST(BEDistributionTest, Probability) {
83 auto dft = storm::dft::api::loadDFTGalileoFile<double>(STORM_TEST_RESOURCES_DIR "/dft/be_probabilistic.dft");
84 double timebound = 0.8;
85
86#ifdef STORM_HAVE_SYLVAN
87 // Perform BDD-based analysis on FT
88 storm::Environment env;
89 auto checker = std::make_shared<storm::dft::modelchecker::SFTBDDChecker>(dft, std::make_shared<storm::dft::storage::SylvanBddManager>(env));
90 double resultBDD = checker->getProbabilityAtTimebound(timebound);
91 EXPECT_NEAR(resultBDD, 0.1095403852, 1e-10);
92#endif
93
94 // Perform Markovian analysis on FT
95 auto dft2 = storm::dft::api::prepareForMarkovAnalysis<double>(*dft);
96 EXPECT_TRUE(storm::dft::api::isWellFormed(*dft2).first);
97 std::string property = "Pmax=? [F<=" + std::to_string(timebound) + " \"failed\"]";
98 std::vector<std::shared_ptr<storm::logic::Formula const>> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property));
99 storm::dft::DftEnvironment dftEnv;
100 double resultMC = boost::get<double>(storm::dft::api::analyzeDFT<double>(dftEnv, *dft2, properties)[0]);
101 EXPECT_NEAR(resultMC, 0.1095403852, 1e-10);
102}
103
104TEST(BEDistributionTest, Exponential) {
105 auto dft = storm::dft::api::loadDFTGalileoFile<double>(STORM_TEST_RESOURCES_DIR "/dft/and.dft");
106 double timebound = 0.8;
107
108#ifdef STORM_HAVE_SYLVAN
109 // Perform BDD-based analysis on FT
110 storm::Environment env;
111 auto checker = std::make_shared<storm::dft::modelchecker::SFTBDDChecker>(dft, std::make_shared<storm::dft::storage::SylvanBddManager>(env));
112 double resultBDD = checker->getProbabilityAtTimebound(timebound);
113 EXPECT_NEAR(resultBDD, 0.108688872, 1e-10);
114#endif
115
116 // Perform Markovian analysis on FT
117 auto dft2 = storm::dft::api::prepareForMarkovAnalysis<double>(*dft);
118 EXPECT_TRUE(storm::dft::api::isWellFormed(*dft2).first);
119 std::string property = "P=? [F<=" + std::to_string(timebound) + " \"failed\"]";
120 std::vector<std::shared_ptr<storm::logic::Formula const>> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property));
121 storm::dft::DftEnvironment dftEnv;
122 double resultMC = boost::get<double>(storm::dft::api::analyzeDFT<double>(dftEnv, *dft2, properties)[0]);
123 EXPECT_NEAR(resultMC, 0.108688872, 1e-10);
124}
125
126TEST(BEDistributionTest, Erlang) {
127 auto dft = storm::dft::api::loadDFTGalileoFile<double>(STORM_TEST_RESOURCES_DIR "/dft/be_erlang.dft");
128 double timebound = 0.8;
129
130#ifdef STORM_HAVE_SYLVAN
131 // Perform BDD-based analysis on FT
132 storm::Environment env;
133 auto checker = std::make_shared<storm::dft::modelchecker::SFTBDDChecker>(dft, std::make_shared<storm::dft::storage::SylvanBddManager>(env));
134 double resultBDD = checker->getProbabilityAtTimebound(timebound);
135 EXPECT_NEAR(resultBDD, 0.4949009834, 1e-10);
136#endif
137
138 // Perform Markovian analysis on FT
139 auto dft2 = storm::dft::api::prepareForMarkovAnalysis<double>(*dft);
140 EXPECT_TRUE(storm::dft::api::isWellFormed(*dft2).first);
141 std::string property = "P=? [F<=" + std::to_string(timebound) + " \"failed\"]";
142 std::vector<std::shared_ptr<storm::logic::Formula const>> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property));
143 storm::dft::DftEnvironment dftEnv;
144 double resultMC = boost::get<double>(storm::dft::api::analyzeDFT<double>(dftEnv, *dft2, properties)[0]);
145 EXPECT_NEAR(resultMC, 0.4949009834, 1e-10);
146}
147
148TEST(BEDistributionTest, Weibull) {
149#ifdef STORM_HAVE_SYLVAN
150 auto dft = storm::dft::api::loadDFTGalileoFile<double>(STORM_TEST_RESOURCES_DIR "/dft/be_weibull.dft");
151 double timebound = 2;
152
153 // Perform BDD-based analysis on FT
154 storm::Environment env;
155 auto checker = std::make_shared<storm::dft::modelchecker::SFTBDDChecker>(dft, std::make_shared<storm::dft::storage::SylvanBddManager>(env));
156 double resultBDD = checker->getProbabilityAtTimebound(timebound);
157 EXPECT_NEAR(resultBDD, 0.0382982486, 1e-10);
158#else
159 GTEST_SKIP() << "Library Sylvan not available.";
160#endif
161}
162
163TEST(BEDistributionTest, LogNormal) {
164#ifdef STORM_HAVE_SYLVAN
165 auto dft = storm::dft::api::loadDFTGalileoFile<double>(STORM_TEST_RESOURCES_DIR "/dft/be_lognormal.dft");
166 double timebound = 0.8;
167
168 // Perform BDD-based analysis on FT
169 storm::Environment env;
170 auto checker = std::make_shared<storm::dft::modelchecker::SFTBDDChecker>(dft, std::make_shared<storm::dft::storage::SylvanBddManager>(env));
171 double resultBDD = checker->getProbabilityAtTimebound(timebound);
172 EXPECT_NEAR(resultBDD, 0.2336675428, 1e-10);
173#else
174 GTEST_SKIP() << "Library Sylvan not available.";
175#endif
176}
177
178} // namespace
TEST
TEST(RegionConstraintCheckerTest, AffineConstraintHoldsThroughout)
Definition RegionConstraintCheckerTest.cpp:75
storm::dft::DftEnvironment
Environment for storm-dft.
Definition DftEnvironment.h:39
storm::api::extractFormulasFromProperties
std::vector< std::shared_ptr< storm::logic::Formula const > > extractFormulasFromProperties(std::vector< storm::jani::Property > const &properties)
Definition properties.cpp:62
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::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 transformation.cpp:47
storm::dft::api::loadDFTGalileoFile
std::shared_ptr< storm::dft::storage::DFT< ValueType > > loadDFTGalileoFile(std::string const &file)
Load DFT from Galileo file.
Definition io.cpp:14
storm::dft::api::isWellFormed
std::pair< bool, std::string > isWellFormed(storm::dft::storage::DFT< ValueType > const &dft, bool validForMarkovianAnalysis)
Check whether the DFT is well-formed.
Definition transformation.cpp:12
storm::dft::api::analyzeDFT
storm::dft::modelchecker::DFTModelChecker< ValueType >::dft_results analyzeDFT(storm::dft::DftEnvironment const &env, storm::dft::storage::DFT< ValueType > const &dft, std::vector< std::shared_ptr< storm::logic::Formula const > > const &properties, storm::dft::utility::RelevantEvents const &relevantEvents, bool printOutput, typename storm::dft::modelchecker::DFTModelChecker< ValueType >::ModelExportCallback const &exportCallback)
Compute the exact or approximate analysis result of the given DFT according to the given properties.
Definition analysis.cpp:27
storm_gtest.h