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