Storm 1.13.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
DftSmtTest.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
6namespace {
7class DftSmt : public ::testing::Test {
8 protected:
9 void SetUp() override {
10#ifndef STORM_HAVE_Z3
11 GTEST_SKIP() << "Z3 not available.";
12#endif
13 }
14};
15
16TEST_F(DftSmt, AndTest) {
17 std::shared_ptr<storm::dft::storage::DFT<double>> dft = storm::dft::api::loadDFTGalileoFile<double>(STORM_TEST_RESOURCES_DIR "/dft/and.dft");
18 EXPECT_TRUE(storm::dft::api::isWellFormed(*dft).first);
19 storm::dft::modelchecker::DFTASFChecker smtChecker(*dft);
20 smtChecker.convert();
21 smtChecker.toSolver();
22 EXPECT_EQ(smtChecker.checkTleNeverFailed(), storm::solver::SmtSolver::CheckResult::Unsat);
23}
24
25TEST_F(DftSmt, PandTest) {
26 std::shared_ptr<storm::dft::storage::DFT<double>> dft = storm::dft::api::loadDFTGalileoFile<double>(STORM_TEST_RESOURCES_DIR "/dft/pand.dft");
27 EXPECT_TRUE(storm::dft::api::isWellFormed(*dft).first);
28 storm::dft::modelchecker::DFTASFChecker smtChecker(*dft);
29 smtChecker.convert();
30 smtChecker.toSolver();
31 EXPECT_EQ(smtChecker.checkTleNeverFailed(), storm::solver::SmtSolver::CheckResult::Sat);
32}
33
34TEST_F(DftSmt, SpareTest) {
35 std::shared_ptr<storm::dft::storage::DFT<double>> dft = storm::dft::api::loadDFTGalileoFile<double>(STORM_TEST_RESOURCES_DIR "/dft/spare_two_modules.dft");
36 EXPECT_TRUE(storm::dft::api::isWellFormed(*dft).first);
37 storm::dft::modelchecker::DFTASFChecker smtChecker(*dft);
38 smtChecker.convert();
39 smtChecker.toSolver();
40 EXPECT_EQ(smtChecker.checkTleFailsWithLeq(2), storm::solver::SmtSolver::CheckResult::Unsat);
41 EXPECT_EQ(smtChecker.checkTleFailsWithEq(3), storm::solver::SmtSolver::CheckResult::Sat);
42}
43
44TEST_F(DftSmt, BoundTest) {
45 std::shared_ptr<storm::dft::storage::DFT<double>> dft = storm::dft::api::loadDFTGalileoFile<double>(STORM_TEST_RESOURCES_DIR "/dft/spare5.dft");
46 EXPECT_TRUE(storm::dft::api::isWellFormed(*dft).first);
47 storm::dft::modelchecker::DFTASFChecker smtChecker(*dft);
48 smtChecker.convert();
49 smtChecker.toSolver();
50 EXPECT_EQ(storm::dft::utility::FailureBoundFinder::getLeastFailureBound(*dft, true, 30), uint64_t(2));
51 EXPECT_EQ(storm::dft::utility::FailureBoundFinder::getAlwaysFailedBound(*dft, true, 30), uint64_t(4));
52}
53
54TEST_F(DftSmt, FDEPBoundTest) {
55 std::shared_ptr<storm::dft::storage::DFT<double>> dft = storm::dft::api::loadDFTGalileoFile<double>(STORM_TEST_RESOURCES_DIR "/dft/fdep_bound.dft");
56 EXPECT_TRUE(storm::dft::api::isWellFormed(*dft, false).first);
57 storm::dft::modelchecker::DFTASFChecker smtChecker(*dft);
58 smtChecker.convert();
59 smtChecker.toSolver();
60 EXPECT_EQ(storm::dft::utility::FailureBoundFinder::getLeastFailureBound(*dft, true, 30), uint64_t(1));
61 EXPECT_EQ(storm::dft::utility::FailureBoundFinder::getAlwaysFailedBound(*dft, true, 30), uint64_t(5));
62}
63
64TEST_F(DftSmt, FDEPConflictTest) {
65 std::shared_ptr<storm::dft::storage::DFT<double>> dft =
66 storm::dft::api::loadDFTGalileoFile<double>(STORM_TEST_RESOURCES_DIR "/dft/spare_conflict_test.dft");
67 EXPECT_TRUE(storm::dft::api::isWellFormed(*dft).first);
68 std::vector<bool> true_vector(10, true);
69
70 EXPECT_EQ(storm::dft::utility::FDEPConflictFinder<double>::getDynamicBehavior(*dft), true_vector);
71 EXPECT_TRUE(storm::dft::utility::FDEPConflictFinder<double>::getDependencyConflicts(*dft, true).empty());
72}
73
74TEST_F(DftSmt, FDEPConflictSPARETest) {
75 std::shared_ptr<storm::dft::storage::DFT<double>> dft =
76 storm::dft::api::loadDFTGalileoFile<double>(STORM_TEST_RESOURCES_DIR "/dft/spare_conflict_test.dft");
77 EXPECT_TRUE(storm::dft::api::isWellFormed(*dft).first);
78 std::vector<bool> true_vector(10, true);
79
80 EXPECT_EQ(storm::dft::utility::FDEPConflictFinder<double>::getDynamicBehavior(*dft), true_vector);
81 EXPECT_TRUE(storm::dft::utility::FDEPConflictFinder<double>::getDependencyConflicts(*dft, true).empty());
82}
83
84TEST_F(DftSmt, FDEPConflictSEQTest) {
85 std::shared_ptr<storm::dft::storage::DFT<double>> dft = storm::dft::api::loadDFTGalileoFile<double>(STORM_TEST_RESOURCES_DIR "/dft/seq_conflict_test.dft");
86 EXPECT_TRUE(storm::dft::api::isWellFormed(*dft).first);
87 std::vector<bool> expected_dynamic_vector(dft->nrElements(), true);
88 expected_dynamic_vector.at(dft->getTopLevelIndex()) = false;
89
90 EXPECT_EQ(storm::dft::utility::FDEPConflictFinder<double>::getDynamicBehavior(*dft), expected_dynamic_vector);
91 EXPECT_EQ(storm::dft::utility::FDEPConflictFinder<double>::getDependencyConflicts(*dft, true).size(), uint64_t(3));
92}
93} // namespace
TEST_F
TEST_F(AssumptionCheckerTest, Brp_no_bisimulation)
Definition AssumptionCheckerTest.cpp:34
storm::dft::utility::FDEPConflictFinder::getDynamicBehavior
static std::vector< bool > getDynamicBehavior(storm::dft::storage::DFT< ValueType > const &dft)
Definition FDEPConflictFinder.cpp:92
storm::dft::utility::FDEPConflictFinder::getDependencyConflicts
static std::vector< std::pair< uint64_t, uint64_t > > getDependencyConflicts(storm::dft::storage::DFT< ValueType > const &dft, bool useSMT=false, uint_fast64_t timeout=10)
Get a vector of index pairs of FDEPs in the DFT which are conflicting.
storm::dft::utility::FailureBoundFinder::getLeastFailureBound
static uint64_t getLeastFailureBound(storm::dft::storage::DFT< double > const &dft, bool useSMT=false, uint_fast64_t timeout=10)
Get the minimal number of BEs necessary for the TLE to fail (lower bound for number of failures to ch...
Definition FailureBoundFinder.cpp:107
storm::dft::utility::FailureBoundFinder::getAlwaysFailedBound
static uint64_t getAlwaysFailedBound(storm::dft::storage::DFT< double > const &dft, bool useSMT=false, uint_fast64_t timeout=10)
Get the number of BE failures for which the TLE always fails (upper bound for number of failures to c...
Definition FailureBoundFinder.cpp:149
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