Skip to content

Commit

Permalink
Skip tests when z3 is not present
Browse files Browse the repository at this point in the history
  • Loading branch information
@volkm
volkm committed Jul 3, 2024
1 parent 5bac172 commit 68ab41c
Show file tree
Hide file tree
Showing 50 changed files with 525 additions and 184 deletions.
27 changes: 18 additions & 9 deletions src/test/storm-dft/api/DftSmtTest.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,16 @@
#include "storm-dft/api/storm-dft.h"

namespace {
TEST(DftSmtTest, AndTest) {
class DftSmt : public ::testing::Test {
protected:
void SetUp() override {
#ifndef STORM_HAVE_Z3
GTEST_SKIP() << "Z3 not available.";
#endif
}
};

TEST_F(DftSmt, AndTest) {
std::shared_ptr<storm::dft::storage::DFT<double>> dft = storm::dft::api::loadDFTGalileoFile<double>(STORM_TEST_RESOURCES_DIR "/dft/and.dft");
EXPECT_TRUE(storm::dft::api::isWellFormed(*dft).first);
storm::dft::modelchecker::DFTASFChecker smtChecker(*dft);
Expand All @@ -13,7 +22,7 @@ TEST(DftSmtTest, AndTest) {
EXPECT_EQ(smtChecker.checkTleNeverFailed(), storm::solver::SmtSolver::CheckResult::Unsat);
}

TEST(DftSmtTest, PandTest) {
TEST_F(DftSmt, PandTest) {
std::shared_ptr<storm::dft::storage::DFT<double>> dft = storm::dft::api::loadDFTGalileoFile<double>(STORM_TEST_RESOURCES_DIR "/dft/pand.dft");
EXPECT_TRUE(storm::dft::api::isWellFormed(*dft).first);
storm::dft::modelchecker::DFTASFChecker smtChecker(*dft);
Expand All @@ -22,7 +31,7 @@ TEST(DftSmtTest, PandTest) {
EXPECT_EQ(smtChecker.checkTleNeverFailed(), storm::solver::SmtSolver::CheckResult::Sat);
}

TEST(DftSmtTest, SpareTest) {
TEST_F(DftSmt, SpareTest) {
std::shared_ptr<storm::dft::storage::DFT<double>> dft = storm::dft::api::loadDFTGalileoFile<double>(STORM_TEST_RESOURCES_DIR "/dft/spare_two_modules.dft");
EXPECT_TRUE(storm::dft::api::isWellFormed(*dft).first);
storm::dft::modelchecker::DFTASFChecker smtChecker(*dft);
Expand All @@ -32,7 +41,7 @@ TEST(DftSmtTest, SpareTest) {
EXPECT_EQ(smtChecker.checkTleFailsWithEq(3), storm::solver::SmtSolver::CheckResult::Sat);
}

TEST(DftSmtTest, BoundTest) {
TEST_F(DftSmt, BoundTest) {
std::shared_ptr<storm::dft::storage::DFT<double>> dft = storm::dft::api::loadDFTGalileoFile<double>(STORM_TEST_RESOURCES_DIR "/dft/spare5.dft");
EXPECT_TRUE(storm::dft::api::isWellFormed(*dft).first);
storm::dft::modelchecker::DFTASFChecker smtChecker(*dft);
Expand All @@ -42,7 +51,7 @@ TEST(DftSmtTest, BoundTest) {
EXPECT_EQ(storm::dft::utility::FailureBoundFinder::getAlwaysFailedBound(*dft, true, 30), uint64_t(4));
}

TEST(DftSmtTest, FDEPBoundTest) {
TEST_F(DftSmt, FDEPBoundTest) {
std::shared_ptr<storm::dft::storage::DFT<double>> dft = storm::dft::api::loadDFTGalileoFile<double>(STORM_TEST_RESOURCES_DIR "/dft/fdep_bound.dft");
EXPECT_TRUE(storm::dft::api::isWellFormed(*dft, false).first);
storm::dft::modelchecker::DFTASFChecker smtChecker(*dft);
Expand All @@ -52,7 +61,7 @@ TEST(DftSmtTest, FDEPBoundTest) {
EXPECT_EQ(storm::dft::utility::FailureBoundFinder::getAlwaysFailedBound(*dft, true, 30), uint64_t(5));
}

TEST(DftSmtTest, FDEPConflictTest) {
TEST_F(DftSmt, FDEPConflictTest) {
std::shared_ptr<storm::dft::storage::DFT<double>> dft =
storm::dft::api::loadDFTGalileoFile<double>(STORM_TEST_RESOURCES_DIR "/dft/spare_conflict_test.dft");
EXPECT_TRUE(storm::dft::api::isWellFormed(*dft).first);
Expand All @@ -62,7 +71,7 @@ TEST(DftSmtTest, FDEPConflictTest) {
EXPECT_TRUE(storm::dft::utility::FDEPConflictFinder<double>::getDependencyConflicts(*dft, true).empty());
}

TEST(DftSmtTest, FDEPConflictSPARETest) {
TEST_F(DftSmt, FDEPConflictSPARETest) {
std::shared_ptr<storm::dft::storage::DFT<double>> dft =
storm::dft::api::loadDFTGalileoFile<double>(STORM_TEST_RESOURCES_DIR "/dft/spare_conflict_test.dft");
EXPECT_TRUE(storm::dft::api::isWellFormed(*dft).first);
Expand All @@ -72,7 +81,7 @@ TEST(DftSmtTest, FDEPConflictSPARETest) {
EXPECT_TRUE(storm::dft::utility::FDEPConflictFinder<double>::getDependencyConflicts(*dft, true).empty());
}

TEST(DftSmtTest, FDEPConflictSEQTest) {
TEST_F(DftSmt, FDEPConflictSEQTest) {
std::shared_ptr<storm::dft::storage::DFT<double>> dft = storm::dft::api::loadDFTGalileoFile<double>(STORM_TEST_RESOURCES_DIR "/dft/seq_conflict_test.dft");
EXPECT_TRUE(storm::dft::api::isWellFormed(*dft).first);
std::vector<bool> expected_dynamic_vector(dft->nrElements(), true);
Expand All @@ -81,4 +90,4 @@ TEST(DftSmtTest, FDEPConflictSEQTest) {
EXPECT_EQ(storm::dft::utility::FDEPConflictFinder<double>::getDynamicBehavior(*dft), expected_dynamic_vector);
EXPECT_EQ(storm::dft::utility::FDEPConflictFinder<double>::getDependencyConflicts(*dft, true).size(), uint64_t(3));
}
} // namespace
} // namespace
19 changes: 14 additions & 5 deletions src/test/storm-pars/analysis/AssumptionCheckerTest.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,16 @@

#include "test/storm_gtest.h"

TEST(AssumptionCheckerTest, Brp_no_bisimulation) {
class AssumptionCheckerTest : public ::testing::Test {
protected:
void SetUp() override {
#ifndef STORM_HAVE_Z3
GTEST_SKIP() << "Z3 not available.";
#endif
}
};

TEST_F(AssumptionCheckerTest, Brp_no_bisimulation) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm";
std::string formulaAsString = "P=? [F s=4 & i=N ]";
std::string constantsAsString = ""; // e.g. pL=0.9,TOACK=0.5
Expand Down Expand Up @@ -93,7 +102,7 @@ TEST(AssumptionCheckerTest, Brp_no_bisimulation) {
EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, dummyOrder, region));
}

TEST(AssumptionCheckerTest, Simple1) {
TEST_F(AssumptionCheckerTest, Simple1) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/simple1.pm";
std::string formulaAsString = "P=? [F s=3]";
std::string constantsAsString = ""; // e.g. pL=0.9,TOACK=0.5
Expand Down Expand Up @@ -167,7 +176,7 @@ TEST(AssumptionCheckerTest, Simple1) {
EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order, region));
}

TEST(AssumptionCheckerTest, Casestudy1) {
TEST_F(AssumptionCheckerTest, Casestudy1) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/casestudy1.pm";
std::string formulaAsString = "P=? [F s=3]";
std::string constantsAsString = ""; // e.g. pL=0.9,TOACK=0.5
Expand Down Expand Up @@ -242,7 +251,7 @@ TEST(AssumptionCheckerTest, Casestudy1) {
EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order, region));
}

TEST(AssumptionCheckerTest, Casestudy2) {
TEST_F(AssumptionCheckerTest, Casestudy2) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/casestudy2.pm";
std::string formulaAsString = "P=? [F s=4]";
std::string constantsAsString = ""; // e.g. pL=0.9,TOACK=0.5
Expand Down Expand Up @@ -302,7 +311,7 @@ TEST(AssumptionCheckerTest, Casestudy2) {
EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order, region));
}

TEST(AssumptionCheckerTest, Casestudy3) {
TEST_F(AssumptionCheckerTest, Casestudy3) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/casestudy3.pm";
std::string formulaAsString = "P=? [F s=3]";
std::string constantsAsString = ""; // e.g. pL=0.9,TOACK=0.5
Expand Down
15 changes: 12 additions & 3 deletions src/test/storm-pars/analysis/AssumptionMakerTest.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,16 @@
#include "storm/models/sparse/StandardRewardModel.h"
#include "storm/utility/graph.h"

TEST(AssumptionMakerTest, Brp_without_bisimulation) {
class AssumptionMakerTest : public ::testing::Test {
protected:
void SetUp() override {
#ifndef STORM_HAVE_Z3
GTEST_SKIP() << "Z3 not available.";
#endif
}
};

TEST_F(AssumptionMakerTest, Brp_without_bisimulation) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm";
std::string formulaAsString = "P=? [F s=4 & i=N ]";
std::string constantsAsString = ""; // e.g. pL=0.9,TOACK=0.5
Expand Down Expand Up @@ -68,7 +77,7 @@ TEST(AssumptionMakerTest, Brp_without_bisimulation) {
EXPECT_EQ(storm::expressions::RelationType::Greater, itr->first->getRelationType());
}

TEST(AssumptionMakerTest, Simple1) {
TEST_F(AssumptionMakerTest, Simple1) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/simple1.pm";
std::string formulaAsString = "P=? [F s=3 ]";
std::string constantsAsString = "";
Expand Down Expand Up @@ -121,7 +130,7 @@ TEST(AssumptionMakerTest, Simple1) {
EXPECT_EQ(storm::expressions::RelationType::Greater, itr->first->getRelationType());
}

TEST(AssumptionMakerTest, Casestudy1) {
TEST_F(AssumptionMakerTest, Casestudy1) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/casestudy1.pm";
std::string formulaAsString = "P=? [F s=3 ]";
std::string constantsAsString = "";
Expand Down
19 changes: 14 additions & 5 deletions src/test/storm-pars/analysis/MonotonicityCheckerTest.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,16 @@

#include "test/storm_gtest.h"

TEST(MonotonicityCheckerTest, Simple1_larger_region) {
class MonotonicityCheckerTest : public ::testing::Test {
protected:
void SetUp() override {
#ifndef STORM_HAVE_Z3
GTEST_SKIP() << "Z3 not available.";
#endif
}
};

TEST_F(MonotonicityCheckerTest, Simple1_larger_region) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/simple1.pm";
std::string formulaAsString = "P=? [F s=3 ]";
std::string constantsAsString = "";
Expand Down Expand Up @@ -66,7 +75,7 @@ TEST(MonotonicityCheckerTest, Simple1_larger_region) {
EXPECT_EQ(storm::analysis::MonotonicityChecker<storm::RationalFunction>::Monotonicity::Decr, monChecker->checkLocalMonotonicity(order, 2, *var, region));
}

TEST(MonotonicityCheckerTest, Simple1_small_region) {
TEST_F(MonotonicityCheckerTest, Simple1_small_region) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/simple1.pm";
std::string formulaAsString = "P=? [F s=3 ]";
std::string constantsAsString = "";
Expand Down Expand Up @@ -115,7 +124,7 @@ TEST(MonotonicityCheckerTest, Simple1_small_region) {
EXPECT_EQ(storm::analysis::MonotonicityChecker<storm::RationalFunction>::Monotonicity::Decr, monChecker->checkLocalMonotonicity(order, 2, *var, region));
}

TEST(MonotonicityCheckerTest, Casestudy1) {
TEST_F(MonotonicityCheckerTest, Casestudy1) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/casestudy1.pm";
std::string formulaAsString = "P=? [F s=3 ]";
std::string constantsAsString = "";
Expand Down Expand Up @@ -168,7 +177,7 @@ TEST(MonotonicityCheckerTest, Casestudy1) {
}
}

TEST(MonotonicityCheckerTest, Casestudy2) {
TEST_F(MonotonicityCheckerTest, Casestudy2) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/casestudy2.pm";
std::string formulaAsString = "P=? [F s=4 ]";
std::string constantsAsString = "";
Expand Down Expand Up @@ -222,7 +231,7 @@ TEST(MonotonicityCheckerTest, Casestudy2) {
}
}

TEST(MonotonicityCheckerTest, Casestudy3) {
TEST_F(MonotonicityCheckerTest, Casestudy3) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/casestudy3.pm";
std::string formulaAsString = "P=? [F s=3 ]";
std::string constantsAsString = "";
Expand Down
27 changes: 18 additions & 9 deletions src/test/storm-pars/analysis/MonotonicityHelperTest.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,16 @@

#include "carl/util/stringparser.h"

TEST(MonotonicityHelperTest, Derivative_checker) {
class MonotonicityHelperTest : public ::testing::Test {
protected:
void SetUp() override {
#ifndef STORM_HAVE_Z3
GTEST_SKIP() << "Z3 not available.";
#endif
}
};

TEST_F(MonotonicityHelperTest, Derivative_checker) {
// Create the region
typename storm::storage::ParameterRegion<storm::RationalFunction>::Valuation lowerBoundaries;
typename storm::storage::ParameterRegion<storm::RationalFunction>::Valuation upperBoundaries;
Expand Down Expand Up @@ -108,7 +117,7 @@ TEST(MonotonicityHelperTest, Derivative_checker) {
EXPECT_FALSE(functionRes.second);
}

TEST(MonotonicityHelperTest, Brp_with_bisimulation_no_samples) {
TEST_F(MonotonicityHelperTest, Brp_with_bisimulation_no_samples) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm";
std::string formulaAsString = "P=? [true U s=4 & i=N ]";
std::string constantsAsString = ""; // e.g. pL=0.9,TOACK=0.5
Expand Down Expand Up @@ -163,7 +172,7 @@ TEST(MonotonicityHelperTest, Brp_with_bisimulation_no_samples) {
}
}

TEST(MonotonicityHelperTest, Brp_with_bisimulation_samples) {
TEST_F(MonotonicityHelperTest, Brp_with_bisimulation_samples) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm";
std::string formulaAsString = "P=? [true U s=4 & i=N ]";
std::string constantsAsString = ""; // e.g. pL=0.9,TOACK=0.5
Expand Down Expand Up @@ -218,7 +227,7 @@ TEST(MonotonicityHelperTest, Brp_with_bisimulation_samples) {
}
}

TEST(MonotonicityHelperTest, zeroconf) {
TEST_F(MonotonicityHelperTest, zeroconf) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/zeroconf4.pm";
std::string formulaAsString = "P > 0.5 [ F s=5 ]";
std::string constantsAsString = "n = 4"; // e.g. pL=0.9,TOACK=0.5
Expand Down Expand Up @@ -272,7 +281,7 @@ TEST(MonotonicityHelperTest, zeroconf) {
}
}

TEST(MonotonicityHelperTest, Simple1) {
TEST_F(MonotonicityHelperTest, Simple1) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/simple1.pm";
std::string formulaAsString = "P > 0.5 [ F s=3 ]";
std::string constantsAsString = "";
Expand Down Expand Up @@ -318,7 +327,7 @@ TEST(MonotonicityHelperTest, Simple1) {
}
}

TEST(MonotonicityHelperTest, Casestudy1) {
TEST_F(MonotonicityHelperTest, Casestudy1) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/casestudy1.pm";
std::string formulaAsString = "P > 0.5 [ F s=3 ]";
std::string constantsAsString = "";
Expand Down Expand Up @@ -360,7 +369,7 @@ TEST(MonotonicityHelperTest, Casestudy1) {
}
}

TEST(MonotonicityHelperTest, CaseStudy2) {
TEST_F(MonotonicityHelperTest, CaseStudy2) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/casestudy2.pm";
std::string formulaAsString = "P > 0.5 [ F s=4 ]";
std::string constantsAsString = "";
Expand Down Expand Up @@ -393,7 +402,7 @@ TEST(MonotonicityHelperTest, CaseStudy2) {
EXPECT_FALSE(result.begin()->first->getDoneBuilding());
}

TEST(MonotonicityHelperTest, Casestudy3_not_monotone) {
TEST_F(MonotonicityHelperTest, Casestudy3_not_monotone) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/casestudy3.pm";
std::string formulaAsString = "P > 0.5 [ F s=3 ]";
std::string constantsAsString = "";
Expand Down Expand Up @@ -436,7 +445,7 @@ TEST(MonotonicityHelperTest, Casestudy3_not_monotone) {
}
}

TEST(MonotonicityHelperTest, Casestudy3_monotone) {
TEST_F(MonotonicityHelperTest, Casestudy3_monotone) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/casestudy3.pm";
std::string formulaAsString = "P > 0.5 [ F s=3 ]";
std::string constantsAsString = "";
Expand Down
Loading

0 comments on commit 68ab41c

Please sign in to comment.