From 11cc7fc6bc48b10f3544e31fa4d7a4bd83879921 Mon Sep 17 00:00:00 2001 From: PBerger Date: Tue, 24 Sep 2013 17:30:18 +0200 Subject: [PATCH] Introduced a new Object called InternalOptionMemento to handle required settings for tests which auto-reset after the test is done Refactored many constants to be of type ull where required Edited all tests that used the set() function of the Settings to make use of the new InternalOptionMemento Former-commit-id: a400a36f699433da15ec8c19b6956e8c2cb18690 --- src/settings/InternalOptionMemento.h | 70 +++++++++++++++++++ src/settings/Option.h | 4 +- src/settings/Settings.h | 32 ++++++--- .../EigenDtmcPrctlModelCheckerTest.cpp | 9 ++- .../GmmxxDtmcPrctlModelCheckerTest.cpp | 30 ++++---- .../GmmxxMdpPrctlModelCheckerTest.cpp | 16 ++--- .../SparseMdpPrctlModelCheckerTest.cpp | 8 +-- test/functional/parser/ParsePrismTest.cpp | 14 ++-- test/functional/storm-functional-tests.cpp | 11 +++ test/performance/graph/GraphTest.cpp | 48 ++++++------- .../GmmxxDtmcPrctModelCheckerTest.cpp | 17 +++-- .../GmmxxMdpPrctModelCheckerTest.cpp | 30 ++++---- .../SparseMdpPrctlModelCheckerTest.cpp | 24 +++---- 13 files changed, 210 insertions(+), 103 deletions(-) create mode 100644 src/settings/InternalOptionMemento.h diff --git a/src/settings/InternalOptionMemento.h b/src/settings/InternalOptionMemento.h new file mode 100644 index 000000000..75243d169 --- /dev/null +++ b/src/settings/InternalOptionMemento.h @@ -0,0 +1,70 @@ +#ifndef STORM_SETTINGS_INTERNALOPTIONMEMENTO_H_ +#define STORM_SETTINGS_INTERNALOPTIONMEMENTO_H_ + +#include "src/settings/Settings.h" +#include "log4cplus/logger.h" +#include "log4cplus/loggingmacros.h" + +extern log4cplus::Logger logger; + +namespace storm { +namespace settings { + + /*! + * @brief THIS CLASS IS FOR INTERNAL USE IN THE TESTS ONLY + * + * + * If an option is required to be set when executing a test + * the test may instantiate an Object of this class while the + * test itself is executed. + * + * This class ensures that the option has the requested value + * and resets it to its previous value as soon as its destructor + * is called. + */ + class InternalOptionMemento { + public: + /*! + * @brief The constructor. + * + * @param + */ + InternalOptionMemento(std::string const& longOptionName, bool requiredHasBeenSetState): instance(storm::settings::Settings::getInstance()), optionName(longOptionName), stateRequired(requiredHasBeenSetState) { + this->stateBefore = instance->isSet(optionName); + if (stateRequired) { + instance->set(optionName); + } else { + instance->unset(optionName); + } + } + + /*! + * @brief The destructor. + * + * Resets the Options state to its previous state + */ + virtual ~InternalOptionMemento() { + // Reset the state of the Option + if (stateBefore) { + instance->set(optionName); + } else { + instance->unset(optionName); + } + this->instance = nullptr; + } + + + + private: + storm::settings::Settings* instance; + std::string const optionName; + bool stateBefore; + bool stateRequired; + + InternalOptionMemento(InternalOptionMemento& other) {} + }; + +} // namespace settings +} // namespace storm + +#endif // STORM_SETTINGS_INTERNALOPTIONMEMENTO_H_ \ No newline at end of file diff --git a/src/settings/Option.h b/src/settings/Option.h index fd980c923..3e82376b2 100644 --- a/src/settings/Option.h +++ b/src/settings/Option.h @@ -183,8 +183,8 @@ namespace storm { return this->hasBeenSet; } - void setHasOptionBeenSet() { - this->hasBeenSet = true; + void setHasOptionBeenSet(bool newValue = true) { + this->hasBeenSet = newValue; } private: std::string longName; diff --git a/src/settings/Settings.h b/src/settings/Settings.h index 8b27e79c0..2fb63fc7f 100644 --- a/src/settings/Settings.h +++ b/src/settings/Settings.h @@ -47,6 +47,7 @@ namespace settings { typedef std::pair fromStringAssignmentResult_t; class Destroyer; + class InternalOptionMemento; /*! * @brief Settings class with command line parser and type validation @@ -127,16 +128,6 @@ namespace settings { return this->getByLongName(longName).getHasOptionBeenSet(); } - /*! - * Sets the Option with the specified longName - * This function requires the Option to have no arguments - * This is for TESTING only and should not be used outside of the testing code! - * @throws InvalidArgumentException - */ - void set(std::string const& longName) const { - return this->getByLongName(longName).setHasOptionBeenSet(); - } - /*! * This generated a list of all registered options and their arguments together with descriptions and defaults. * @return A std::string containing the help text, delimited by \n @@ -149,6 +140,7 @@ namespace settings { */ static Settings* getInstance(); friend class Destroyer; + friend class InternalOptionMemento; private: /*! * @brief Private constructor. @@ -277,6 +269,26 @@ namespace settings { } return this->options.find(shortNameIterator->second)->second.get(); } + + /*! + * Sets the Option with the specified longName + * This function requires the Option to have no arguments + * This is for TESTING only and should not be used outside of the testing code! + * @throws InvalidArgumentException + */ + void set(std::string const& longName) const { + return this->getByLongName(longName).setHasOptionBeenSet(); + } + + /*! + * Unsets the Option with the specified longName + * This function requires the Option to have no arguments + * This is for TESTING only and should not be used outside of the testing code! + * @throws InvalidArgumentException + */ + void unset(std::string const& longName) const { + return this->getByLongName(longName).setHasOptionBeenSet(false); + } }; /*! diff --git a/test/functional/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp index c1d6698ee..0d36a1d77 100644 --- a/test/functional/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp @@ -8,7 +8,8 @@ TEST(EigenDtmcPrctlModelCheckerTest, Die) { storm::settings::Settings* s = storm::settings::Settings::getInstance(); - s->set("fixDeadlocks"); + storm::settings::InternalOptionMemento deadlockOption("fixDeadlocks", true); + ASSERT_TRUE(s->isSet("fixDeadlocks")); storm::parser::AutoParser parser(STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/die/die.tra", STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/die/die.lab", "", STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/die/die.coin_flips.trans.rew"); ASSERT_EQ(parser.getType(), storm::models::DTMC); @@ -68,7 +69,8 @@ TEST(EigenDtmcPrctlModelCheckerTest, Die) { TEST(EigenDtmcPrctlModelCheckerTest, Crowds) { storm::settings::Settings* s = storm::settings::Settings::getInstance(); - s->set("fixDeadlocks"); + storm::settings::InternalOptionMemento deadlockOption("fixDeadlocks", true); + ASSERT_TRUE(s->isSet("fixDeadlocks")); storm::parser::AutoParser parser(STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/crowds/crowds5_5.tra", STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/crowds/crowds5_5.lab", "", ""); ASSERT_EQ(parser.getType(), storm::models::DTMC); @@ -116,7 +118,8 @@ TEST(EigenDtmcPrctlModelCheckerTest, Crowds) { TEST(EigenDtmcPrctlModelCheckerTest, SynchronousLeader) { storm::settings::Settings* s = storm::settings::Settings::getInstance(); - s->set("fixDeadlocks"); + storm::settings::InternalOptionMemento deadlockOption("fixDeadlocks", true); + ASSERT_TRUE(s->isSet("fixDeadlocks")); storm::parser::AutoParser parser(STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/synchronous_leader/leader4_8.tra", STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/synchronous_leader/leader4_8.lab", "", STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/synchronous_leader/leader4_8.pick.trans.rew"); ASSERT_EQ(parser.getType(), storm::models::DTMC); diff --git a/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp index 9800b8764..1461da33a 100644 --- a/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp @@ -4,19 +4,21 @@ #include "src/solver/GmmxxLinearEquationSolver.h" #include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" #include "src/settings/Settings.h" +#include "src/settings/InternalOptionMemento.h" #include "src/parser/AutoParser.h" TEST(GmmxxDtmcPrctlModelCheckerTest, Die) { storm::settings::Settings* s = storm::settings::Settings::getInstance(); - s->set("fixDeadlocks"); + storm::settings::InternalOptionMemento deadlockOption("fixDeadlocks", true); + ASSERT_TRUE(s->isSet("fixDeadlocks")); storm::parser::AutoParser parser(STORM_CPP_BASE_PATH "/examples/dtmc/die/die.tra", STORM_CPP_BASE_PATH "/examples/dtmc/die/die.lab", "", STORM_CPP_BASE_PATH "/examples/dtmc/die/die.coin_flips.trans.rew"); ASSERT_EQ(parser.getType(), storm::models::DTMC); std::shared_ptr> dtmc = parser.getModel>(); - ASSERT_EQ(dtmc->getNumberOfStates(), 13u); - ASSERT_EQ(dtmc->getNumberOfTransitions(), 27u); + ASSERT_EQ(dtmc->getNumberOfStates(), 13ull); + ASSERT_EQ(dtmc->getNumberOfTransitions(), 27ull); storm::modelchecker::prctl::SparseDtmcPrctlModelChecker mc(*dtmc, new storm::solver::GmmxxLinearEquationSolver()); @@ -28,7 +30,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Die) { ASSERT_NE(nullptr, result); - ASSERT_LT(std::abs((*result)[0] - ((double)1/6)), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); + ASSERT_LT(std::abs((*result)[0] - ((double)1.0/6.0)), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); delete probFormula; delete result; @@ -41,7 +43,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Die) { ASSERT_NE(nullptr, result); - ASSERT_LT(std::abs((*result)[0] - ((double)1/6)), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); + ASSERT_LT(std::abs((*result)[0] - ((double)1.0/6.0)), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); delete probFormula; delete result; @@ -54,7 +56,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Die) { ASSERT_NE(nullptr, result); - ASSERT_LT(std::abs((*result)[0] - ((double)1/6)), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); + ASSERT_LT(std::abs((*result)[0] - ((double)1.0/6.0)), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); delete probFormula; delete result; @@ -75,15 +77,16 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Die) { TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) { storm::settings::Settings* s = storm::settings::Settings::getInstance(); - s->set("fixDeadlocks"); + storm::settings::InternalOptionMemento deadlockOption("fixDeadlocks", true); + ASSERT_TRUE(s->isSet("fixDeadlocks")); storm::parser::AutoParser parser(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds5_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds5_5.lab", "", ""); ASSERT_EQ(parser.getType(), storm::models::DTMC); std::shared_ptr> dtmc = parser.getModel>(); - ASSERT_EQ(dtmc->getNumberOfStates(), 8607u); - ASSERT_EQ(dtmc->getNumberOfTransitions(), 22460u); + ASSERT_EQ(dtmc->getNumberOfStates(), 8607ull); + ASSERT_EQ(dtmc->getNumberOfTransitions(), 22460ull); storm::modelchecker::prctl::SparseDtmcPrctlModelChecker mc(*dtmc, new storm::solver::GmmxxLinearEquationSolver()); @@ -129,15 +132,16 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) { TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) { storm::settings::Settings* s = storm::settings::Settings::getInstance(); - s->set("fixDeadlocks"); + storm::settings::InternalOptionMemento deadlockOption("fixDeadlocks", true); + ASSERT_TRUE(s->isSet("fixDeadlocks")); storm::parser::AutoParser parser(STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader4_8.tra", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader4_8.lab", "", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader4_8.pick.trans.rew"); ASSERT_EQ(parser.getType(), storm::models::DTMC); std::shared_ptr> dtmc = parser.getModel>(); - ASSERT_EQ(dtmc->getNumberOfStates(), 12400u); - ASSERT_EQ(dtmc->getNumberOfTransitions(), 28894u); + ASSERT_EQ(dtmc->getNumberOfStates(), 12400ull); + ASSERT_EQ(dtmc->getNumberOfTransitions(), 28894ull); storm::modelchecker::prctl::SparseDtmcPrctlModelChecker mc(*dtmc, new storm::solver::GmmxxLinearEquationSolver()); @@ -149,7 +153,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) { ASSERT_NE(nullptr, result); - ASSERT_LT(std::abs((*result)[0] - 1), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); + ASSERT_LT(std::abs((*result)[0] - 1.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); delete probFormula; delete result; diff --git a/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp index 2f076a940..da942de5c 100644 --- a/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp @@ -14,8 +14,8 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) { std::shared_ptr> mdp = parser.getModel>(); - ASSERT_EQ(mdp->getNumberOfStates(), 169u); - ASSERT_EQ(mdp->getNumberOfTransitions(), 436u); + ASSERT_EQ(mdp->getNumberOfStates(), 169ull); + ASSERT_EQ(mdp->getNumberOfTransitions(), 436ull); storm::modelchecker::prctl::SparseMdpPrctlModelChecker mc(*mdp, new storm::solver::GmmxxNondeterministicLinearEquationSolver()); @@ -153,7 +153,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) { result = stateAndTransitionRewardModelChecker.checkNoBoundOperator(*rewardFormula); - ASSERT_LT(std::abs((*result)[0] - (2 * 7.3333294987678527832)), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); + ASSERT_LT(std::abs((*result)[0] - (2.0 * 7.3333294987678527832)), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); delete rewardFormula; delete result; @@ -164,7 +164,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) { result = stateAndTransitionRewardModelChecker.checkNoBoundOperator(*rewardFormula); - ASSERT_LT(std::abs((*result)[0] - (2 * 7.3333294987678527832)), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); + ASSERT_LT(std::abs((*result)[0] - (2.0 * 7.3333294987678527832)), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); delete rewardFormula; delete result; @@ -178,8 +178,8 @@ TEST(GmmxxMdpPrctlModelCheckerTest, AsynchronousLeader) { std::shared_ptr> mdp = parser.getModel>(); - ASSERT_EQ(mdp->getNumberOfStates(), 3172u); - ASSERT_EQ(mdp->getNumberOfTransitions(), 7144u); + ASSERT_EQ(mdp->getNumberOfStates(), 3172ull); + ASSERT_EQ(mdp->getNumberOfTransitions(), 7144ull); storm::modelchecker::prctl::SparseMdpPrctlModelChecker mc(*mdp, new storm::solver::GmmxxNondeterministicLinearEquationSolver()); @@ -191,7 +191,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, AsynchronousLeader) { ASSERT_NE(nullptr, result); - ASSERT_LT(std::abs((*result)[0] - 1), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); + ASSERT_LT(std::abs((*result)[0] - 1.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); delete probFormula; delete result; @@ -204,7 +204,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, AsynchronousLeader) { ASSERT_NE(nullptr, result); - ASSERT_LT(std::abs((*result)[0] - 1), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); + ASSERT_LT(std::abs((*result)[0] - 1.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); delete probFormula; delete result; diff --git a/test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp index 237bb591c..10a0173de 100644 --- a/test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp @@ -13,8 +13,8 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) { std::shared_ptr> mdp = parser.getModel>(); - ASSERT_EQ(mdp->getNumberOfStates(), 169u); - ASSERT_EQ(mdp->getNumberOfTransitions(), 436u); + ASSERT_EQ(mdp->getNumberOfStates(), 169ull); + ASSERT_EQ(mdp->getNumberOfTransitions(), 436ull); storm::modelchecker::prctl::SparseMdpPrctlModelChecker mc(*mdp, new storm::solver::AbstractNondeterministicLinearEquationSolver()); @@ -176,8 +176,8 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) { std::shared_ptr> mdp = parser.getModel>(); - ASSERT_EQ(mdp->getNumberOfStates(), 3172u); - ASSERT_EQ(mdp->getNumberOfTransitions(), 7144u); + ASSERT_EQ(mdp->getNumberOfStates(), 3172ull); + ASSERT_EQ(mdp->getNumberOfTransitions(), 7144ull); storm::modelchecker::prctl::SparseMdpPrctlModelChecker mc(*mdp, new storm::solver::AbstractNondeterministicLinearEquationSolver()); diff --git a/test/functional/parser/ParsePrismTest.cpp b/test/functional/parser/ParsePrismTest.cpp index c40e5201d..3cf963872 100644 --- a/test/functional/parser/ParsePrismTest.cpp +++ b/test/functional/parser/ParsePrismTest.cpp @@ -6,16 +6,20 @@ #include "src/adapters/ExplicitModelAdapter.h" #include "src/models/Dtmc.h" #include "src/models/Mdp.h" +#include "src/settings/Settings.h" +#include "src/settings/InternalOptionMemento.h" TEST(ParsePrismTest, parseCrowds5_5) { + storm::settings::InternalOptionMemento deadlockOption("fixDeadlocks", true); + ASSERT_TRUE(storm::settings::Settings::getInstance()->isSet("fixDeadlocks")); storm::ir::Program program; ASSERT_NO_THROW(program = storm::parser::PrismParserFromFile(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds5_5.pm")); storm::adapters::ExplicitModelAdapter adapter(program); std::shared_ptr> model = adapter.getModel()->as>(); - ASSERT_EQ(model->getNumberOfStates(), (uint_fast64_t)8607); - ASSERT_EQ(model->getNumberOfTransitions(), (uint_fast64_t)15113); + ASSERT_EQ(model->getNumberOfStates(), 8607ull); + ASSERT_EQ(model->getNumberOfTransitions(), 15113ull); } TEST(ParsePrismTest, parseTwoDice) { @@ -25,7 +29,7 @@ TEST(ParsePrismTest, parseTwoDice) { std::shared_ptr> model = adapter.getModel()->as>(); - ASSERT_EQ(model->getNumberOfStates(), (uint_fast64_t)169); - ASSERT_EQ(model->getNumberOfChoices(), (uint_fast64_t)254); - ASSERT_EQ(model->getNumberOfTransitions(), (uint_fast64_t)436); + ASSERT_EQ(model->getNumberOfStates(), 169ull); + ASSERT_EQ(model->getNumberOfChoices(), 254ull); + ASSERT_EQ(model->getNumberOfTransitions(), 436ull); } diff --git a/test/functional/storm-functional-tests.cpp b/test/functional/storm-functional-tests.cpp index 5d77d5a81..1b113d92c 100644 --- a/test/functional/storm-functional-tests.cpp +++ b/test/functional/storm-functional-tests.cpp @@ -51,6 +51,17 @@ int main(int argc, char* argv[]) { testing::InitGoogleTest(&argc, argv); + // now all Google Test Options have been removed + storm::settings::Settings* instance = storm::settings::Settings::getInstance(); + + try { + storm::settings::Settings::parse(argc, argv); + } catch (storm::exceptions::OptionParserException& e) { + std::cout << "Could not recover from settings error: " << e.what() << "." << std::endl; + std::cout << std::endl << instance->getHelpText(); + return false; + } + int result = RUN_ALL_TESTS(); logger.closeNestedAppenders(); diff --git a/test/performance/graph/GraphTest.cpp b/test/performance/graph/GraphTest.cpp index bf62d4632..47c589a86 100644 --- a/test/performance/graph/GraphTest.cpp +++ b/test/performance/graph/GraphTest.cpp @@ -13,18 +13,18 @@ TEST(GraphTest, PerformProb01) { LOG4CPLUS_WARN(logger, "Computing prob01 (3 times) for crowds/crowds20_5..."); std::pair prob01(storm::utility::graph::performProb01(*dtmc, trueStates, storm::storage::BitVector(dtmc->getLabeledStates("observe0Greater1")))); - ASSERT_EQ(prob01.first.getNumberOfSetBits(), 1724414u); - ASSERT_EQ(prob01.second.getNumberOfSetBits(), 46046u); + ASSERT_EQ(prob01.first.getNumberOfSetBits(), 1724414ull); + ASSERT_EQ(prob01.second.getNumberOfSetBits(), 46046ull); prob01 = storm::utility::graph::performProb01(*dtmc, trueStates, storm::storage::BitVector(dtmc->getLabeledStates("observeIGreater1"))); - ASSERT_EQ(prob01.first.getNumberOfSetBits(), 574016u); - ASSERT_EQ(prob01.second.getNumberOfSetBits(), 825797u); + ASSERT_EQ(prob01.first.getNumberOfSetBits(), 574016ull); + ASSERT_EQ(prob01.second.getNumberOfSetBits(), 825797ull); prob01 = storm::utility::graph::performProb01(*dtmc, trueStates, storm::storage::BitVector(dtmc->getLabeledStates("observeOnlyTrueSender"))); - ASSERT_EQ(prob01.first.getNumberOfSetBits(), 1785309u); - ASSERT_EQ(prob01.second.getNumberOfSetBits(), 40992u); + ASSERT_EQ(prob01.first.getNumberOfSetBits(), 1785309ull); + ASSERT_EQ(prob01.second.getNumberOfSetBits(), 40992ull); LOG4CPLUS_WARN(logger, "Done."); dtmc = nullptr; @@ -38,8 +38,8 @@ TEST(GraphTest, PerformProb01) { prob01 = storm::utility::graph::performProb01(*dtmc2, trueStates, storm::storage::BitVector(dtmc2->getLabeledStates("elected"))); LOG4CPLUS_WARN(logger, "Done."); - ASSERT_EQ(prob01.first.getNumberOfSetBits(), 0u); - ASSERT_EQ(prob01.second.getNumberOfSetBits(), 1312334u); + ASSERT_EQ(prob01.first.getNumberOfSetBits(), 0ull); + ASSERT_EQ(prob01.second.getNumberOfSetBits(), 1312334ull); dtmc2 = nullptr; } @@ -53,15 +53,15 @@ TEST(GraphTest, PerformProb01MinMax) { std::pair prob01(storm::utility::graph::performProb01Min(*mdp, trueStates, mdp->getLabeledStates("elected"))); LOG4CPLUS_WARN(logger, "Done."); - ASSERT_EQ(prob01.first.getNumberOfSetBits(), 0u); - ASSERT_EQ(prob01.second.getNumberOfSetBits(), 2095783u); + ASSERT_EQ(prob01.first.getNumberOfSetBits(), 0ull); + ASSERT_EQ(prob01.second.getNumberOfSetBits(), 2095783ull); LOG4CPLUS_WARN(logger, "Computing prob01max for asynchronous_leader/leader7..."); prob01 = storm::utility::graph::performProb01Max(*mdp, trueStates, mdp->getLabeledStates("elected")); LOG4CPLUS_WARN(logger, "Done."); - ASSERT_EQ(prob01.first.getNumberOfSetBits(), 0u); - ASSERT_EQ(prob01.second.getNumberOfSetBits(), 2095783u); + ASSERT_EQ(prob01.first.getNumberOfSetBits(), 0ull); + ASSERT_EQ(prob01.second.getNumberOfSetBits(), 2095783ull); mdp = nullptr; @@ -73,15 +73,15 @@ TEST(GraphTest, PerformProb01MinMax) { prob01 = storm::utility::graph::performProb01Min(*mdp2, trueStates, mdp2->getLabeledStates("finished")); LOG4CPLUS_WARN(logger, "Done."); - ASSERT_EQ(prob01.first.getNumberOfSetBits(), 0u); - ASSERT_EQ(prob01.second.getNumberOfSetBits(), 63616u); + ASSERT_EQ(prob01.first.getNumberOfSetBits(), 0ull); + ASSERT_EQ(prob01.second.getNumberOfSetBits(), 63616ull); LOG4CPLUS_WARN(logger, "Computing prob01max for consensus/coin4_6..."); prob01 = storm::utility::graph::performProb01Max(*mdp2, trueStates, mdp2->getLabeledStates("finished")); LOG4CPLUS_WARN(logger, "Done."); - ASSERT_EQ(prob01.first.getNumberOfSetBits(), 0u); - ASSERT_EQ(prob01.second.getNumberOfSetBits(), 63616u); + ASSERT_EQ(prob01.first.getNumberOfSetBits(), 0ull); + ASSERT_EQ(prob01.second.getNumberOfSetBits(), 63616ull); mdp2 = nullptr; } @@ -94,13 +94,13 @@ TEST(GraphTest, PerformSCCDecompositionAndGetDependencyGraph) { std::vector> sccDecomposition(std::move(storm::utility::graph::performSccDecomposition(*dtmc))); LOG4CPLUS_WARN(logger, "Done."); - ASSERT_EQ(sccDecomposition.size(), 1290297u); + ASSERT_EQ(sccDecomposition.size(), 1290297ull); LOG4CPLUS_WARN(logger, "Extracting SCC dependency graph of crowds/crowds20_5..."); storm::storage::SparseMatrix sccDependencyGraph(std::move(dtmc->extractPartitionDependencyGraph(sccDecomposition))); LOG4CPLUS_WARN(logger, "Done."); - ASSERT_EQ(sccDependencyGraph.getNonZeroEntryCount(), 1371253u); + ASSERT_EQ(sccDependencyGraph.getNonZeroEntryCount(), 1371253ull); dtmc = nullptr; @@ -111,13 +111,13 @@ TEST(GraphTest, PerformSCCDecompositionAndGetDependencyGraph) { sccDecomposition = std::move(storm::utility::graph::performSccDecomposition(*dtmc2)); LOG4CPLUS_WARN(logger, "Done."); - ASSERT_EQ(sccDecomposition.size(), 1279673u); + ASSERT_EQ(sccDecomposition.size(), 1279673ull); LOG4CPLUS_WARN(logger, "Extracting SCC dependency graph of synchronous_leader/leader6_8..."); sccDependencyGraph = std::move(dtmc2->extractPartitionDependencyGraph(sccDecomposition)); LOG4CPLUS_WARN(logger, "Done."); - ASSERT_EQ(sccDependencyGraph.getNonZeroEntryCount(), 1535367u); + ASSERT_EQ(sccDependencyGraph.getNonZeroEntryCount(), 1535367ull); dtmc2 = nullptr; @@ -128,13 +128,13 @@ TEST(GraphTest, PerformSCCDecompositionAndGetDependencyGraph) { sccDecomposition = std::move(storm::utility::graph::performSccDecomposition(*mdp)); LOG4CPLUS_WARN(logger, "Done."); - ASSERT_EQ(sccDecomposition.size(), 214675); + ASSERT_EQ(sccDecomposition.size(), 214675ull); LOG4CPLUS_WARN(logger, "Extracting SCC dependency graph of asynchronous_leader/leader6..."); sccDependencyGraph = std::move(mdp->extractPartitionDependencyGraph(sccDecomposition)); LOG4CPLUS_WARN(logger, "Done."); - ASSERT_EQ(sccDependencyGraph.getNonZeroEntryCount(), 684093u); + ASSERT_EQ(sccDependencyGraph.getNonZeroEntryCount(), 684093ull); mdp = nullptr; @@ -145,13 +145,13 @@ TEST(GraphTest, PerformSCCDecompositionAndGetDependencyGraph) { sccDecomposition = std::move(storm::utility::graph::performSccDecomposition(*mdp2)); LOG4CPLUS_WARN(logger, "Done."); - ASSERT_EQ(sccDecomposition.size(), 63611u); + ASSERT_EQ(sccDecomposition.size(), 63611ull); LOG4CPLUS_WARN(logger, "Extracting SCC dependency graph of consensus/coin4_6..."); sccDependencyGraph = std::move(mdp2->extractPartitionDependencyGraph(sccDecomposition)); LOG4CPLUS_WARN(logger, "Done."); - ASSERT_EQ(sccDependencyGraph.getNonZeroEntryCount(), 213400u); + ASSERT_EQ(sccDependencyGraph.getNonZeroEntryCount(), 213400ull); mdp2 = nullptr; } \ No newline at end of file diff --git a/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp b/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp index 09c958323..d41221bf5 100644 --- a/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp +++ b/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp @@ -1,21 +1,23 @@ #include "gtest/gtest.h" #include "storm-config.h" #include "src/settings/Settings.h" +#include "src/settings/InternalOptionMemento.h" #include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" #include "src/solver/GmmxxLinearEquationSolver.h" #include "src/parser/AutoParser.h" TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) { storm::settings::Settings* s = storm::settings::Settings::getInstance(); - s->set("fixDeadlocks"); + storm::settings::InternalOptionMemento deadlockOption("fixDeadlocks", true); + ASSERT_TRUE(s->isSet("fixDeadlocks")); storm::parser::AutoParser parser(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.lab", "", ""); ASSERT_EQ(parser.getType(), storm::models::DTMC); std::shared_ptr> dtmc = parser.getModel>(); - ASSERT_EQ(dtmc->getNumberOfStates(), 2036647u); - ASSERT_EQ(dtmc->getNumberOfTransitions(), 8973900u); + ASSERT_EQ(dtmc->getNumberOfStates(), 2036647ull); + ASSERT_EQ(dtmc->getNumberOfTransitions(), 8973900ull); storm::modelchecker::prctl::SparseDtmcPrctlModelChecker mc(*dtmc, new storm::solver::GmmxxLinearEquationSolver()); @@ -68,15 +70,16 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) { TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) { storm::settings::Settings* s = storm::settings::Settings::getInstance(); - s->set("fixDeadlocks"); + storm::settings::InternalOptionMemento deadlockOption("fixDeadlocks", true); + ASSERT_TRUE(s->isSet("fixDeadlocks")); storm::parser::AutoParser parser(STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.tra", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.lab", "", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.pick.trans.rew"); ASSERT_EQ(parser.getType(), storm::models::DTMC); std::shared_ptr> dtmc = parser.getModel>(); - ASSERT_EQ(dtmc->getNumberOfStates(), 1312334u); - ASSERT_EQ(dtmc->getNumberOfTransitions(), 2886810u); + ASSERT_EQ(dtmc->getNumberOfStates(), 1312334ull); + ASSERT_EQ(dtmc->getNumberOfTransitions(), 2886810ull); storm::modelchecker::prctl::SparseDtmcPrctlModelChecker mc(*dtmc, new storm::solver::GmmxxLinearEquationSolver()); @@ -90,7 +93,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) { ASSERT_NE(nullptr, result); - ASSERT_LT(std::abs((*result)[0] - 1), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); + ASSERT_LT(std::abs((*result)[0] - 1.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); delete probFormula; delete result; diff --git a/test/performance/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp b/test/performance/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp index faabd6038..7f2d45d00 100644 --- a/test/performance/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp +++ b/test/performance/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp @@ -14,8 +14,8 @@ TEST(GmmxxMdpPrctlModelCheckerTest, AsynchronousLeader) { std::shared_ptr> mdp = parser.getModel>(); - ASSERT_EQ(mdp->getNumberOfStates(), 2095783u); - ASSERT_EQ(mdp->getNumberOfTransitions(), 7714385u); + ASSERT_EQ(mdp->getNumberOfStates(), 2095783ull); + ASSERT_EQ(mdp->getNumberOfTransitions(), 7714385ull); storm::modelchecker::prctl::SparseMdpPrctlModelChecker mc(*mdp, new storm::solver::GmmxxNondeterministicLinearEquationSolver()); @@ -29,7 +29,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, AsynchronousLeader) { ASSERT_NE(nullptr, result); - ASSERT_LT(std::abs((*result)[0] - 1), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); + ASSERT_LT(std::abs((*result)[0] - 1.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); delete probFormula; delete result; @@ -44,13 +44,13 @@ TEST(GmmxxMdpPrctlModelCheckerTest, AsynchronousLeader) { ASSERT_NE(nullptr, result); - ASSERT_LT(std::abs((*result)[0] - 1), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); + ASSERT_LT(std::abs((*result)[0] - 1.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); delete probFormula; delete result; apFormula = new storm::property::prctl::Ap("elected"); - storm::property::prctl::BoundedEventually* boundedEventuallyFormula = new storm::property::prctl::BoundedEventually(apFormula, 25); + storm::property::prctl::BoundedEventually* boundedEventuallyFormula = new storm::property::prctl::BoundedEventually(apFormula, 25ull); probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(boundedEventuallyFormula, true); LOG4CPLUS_WARN(logger, "Model Checking Pmin=? [F<=25 elected] on asynchronous_leader/leader7..."); @@ -59,13 +59,13 @@ TEST(GmmxxMdpPrctlModelCheckerTest, AsynchronousLeader) { ASSERT_NE(nullptr, result); - ASSERT_LT(std::abs((*result)[0] - 0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); + ASSERT_LT(std::abs((*result)[0] - 0.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); delete probFormula; delete result; apFormula = new storm::property::prctl::Ap("elected"); - boundedEventuallyFormula = new storm::property::prctl::BoundedEventually(apFormula, 25); + boundedEventuallyFormula = new storm::property::prctl::BoundedEventually(apFormula, 25ull); probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(boundedEventuallyFormula, false); LOG4CPLUS_WARN(logger, "Model Checking Pmax=? [F<=25 elected] on asynchronous_leader/leader7..."); @@ -74,7 +74,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, AsynchronousLeader) { ASSERT_NE(nullptr, result); - ASSERT_LT(std::abs((*result)[0] - 0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); + ASSERT_LT(std::abs((*result)[0] - 0.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); delete probFormula; delete result; @@ -117,8 +117,8 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Consensus) { std::shared_ptr> mdp = parser.getModel>(); - ASSERT_EQ(mdp->getNumberOfStates(), 63616u); - ASSERT_EQ(mdp->getNumberOfTransitions(), 213472u); + ASSERT_EQ(mdp->getNumberOfStates(), 63616ull); + ASSERT_EQ(mdp->getNumberOfTransitions(), 213472ull); storm::modelchecker::prctl::SparseMdpPrctlModelChecker mc(*mdp, new storm::solver::GmmxxNondeterministicLinearEquationSolver()); @@ -132,7 +132,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Consensus) { ASSERT_NE(nullptr, result); - ASSERT_LT(std::abs((*result)[31168] - 1), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); + ASSERT_LT(std::abs((*result)[31168] - 1.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); delete probFormula; delete result; @@ -188,7 +188,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Consensus) { delete result; apFormula = new storm::property::prctl::Ap("finished"); - storm::property::prctl::BoundedEventually* boundedEventuallyFormula = new storm::property::prctl::BoundedEventually(apFormula, 50); + storm::property::prctl::BoundedEventually* boundedEventuallyFormula = new storm::property::prctl::BoundedEventually(apFormula, 50ull); probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(boundedEventuallyFormula, true); LOG4CPLUS_WARN(logger, "Model Checking Pmin=? [F<=50 finished] on consensus/coin4_6..."); @@ -196,13 +196,13 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Consensus) { LOG4CPLUS_WARN(logger, "Done."); ASSERT_NE(nullptr, result); - ASSERT_LT(std::abs((*result)[31168] - 0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); + ASSERT_LT(std::abs((*result)[31168] - 0.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); delete probFormula; delete result; apFormula = new storm::property::prctl::Ap("finished"); - boundedEventuallyFormula = new storm::property::prctl::BoundedEventually(apFormula, 50); + boundedEventuallyFormula = new storm::property::prctl::BoundedEventually(apFormula, 50ull); probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(boundedEventuallyFormula, false); LOG4CPLUS_WARN(logger, "Model Checking Pmax=? [F<=50 finished] on consensus/coin4_6..."); @@ -210,7 +210,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Consensus) { LOG4CPLUS_WARN(logger, "Done."); ASSERT_NE(nullptr, result); - ASSERT_LT(std::abs((*result)[31168] - 0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); + ASSERT_LT(std::abs((*result)[31168] - 0.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); delete probFormula; delete result; diff --git a/test/performance/modelchecker/SparseMdpPrctlModelCheckerTest.cpp b/test/performance/modelchecker/SparseMdpPrctlModelCheckerTest.cpp index f451620ba..877a5aaa6 100644 --- a/test/performance/modelchecker/SparseMdpPrctlModelCheckerTest.cpp +++ b/test/performance/modelchecker/SparseMdpPrctlModelCheckerTest.cpp @@ -14,8 +14,8 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) { std::shared_ptr> mdp = parser.getModel>(); - ASSERT_EQ(mdp->getNumberOfStates(), 2095783u); - ASSERT_EQ(mdp->getNumberOfTransitions(), 7714385u); + ASSERT_EQ(mdp->getNumberOfStates(), 2095783ull); + ASSERT_EQ(mdp->getNumberOfTransitions(), 7714385ull); storm::modelchecker::prctl::SparseMdpPrctlModelChecker mc(*mdp, new storm::solver::AbstractNondeterministicLinearEquationSolver()); @@ -28,7 +28,7 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) { LOG4CPLUS_WARN(logger, "Done."); ASSERT_NE(nullptr, result); - ASSERT_LT(std::abs((*result)[0] - 1), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); + ASSERT_LT(std::abs((*result)[0] - 1.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); delete probFormula; delete result; @@ -43,7 +43,7 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) { ASSERT_NE(nullptr, result); - ASSERT_LT(std::abs((*result)[0] - 1), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); + ASSERT_LT(std::abs((*result)[0] - 1.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); delete probFormula; delete result; @@ -58,7 +58,7 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) { ASSERT_NE(nullptr, result); - ASSERT_LT(std::abs((*result)[0] - 0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); + ASSERT_LT(std::abs((*result)[0] - 0.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); delete probFormula; delete result; @@ -72,7 +72,7 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) { LOG4CPLUS_WARN(logger, "Done."); ASSERT_NE(nullptr, result); - ASSERT_LT(std::abs((*result)[0] - 0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); + ASSERT_LT(std::abs((*result)[0] - 0.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); delete probFormula; delete result; @@ -117,8 +117,8 @@ TEST(SparseMdpPrctlModelCheckerTest, Consensus) { std::shared_ptr> mdp = parser.getModel>(); - ASSERT_EQ(mdp->getNumberOfStates(), 63616u); - ASSERT_EQ(mdp->getNumberOfTransitions(), 213472u); + ASSERT_EQ(mdp->getNumberOfStates(), 63616ull); + ASSERT_EQ(mdp->getNumberOfTransitions(), 213472ull); storm::modelchecker::prctl::SparseMdpPrctlModelChecker mc(*mdp, new storm::solver::AbstractNondeterministicLinearEquationSolver()); @@ -187,7 +187,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Consensus) { delete result; apFormula = new storm::property::prctl::Ap("finished"); - storm::property::prctl::BoundedEventually* boundedEventuallyFormula = new storm::property::prctl::BoundedEventually(apFormula, 50); + storm::property::prctl::BoundedEventually* boundedEventuallyFormula = new storm::property::prctl::BoundedEventually(apFormula, 50ull); probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(boundedEventuallyFormula, true); LOG4CPLUS_WARN(logger, "Model Checking Pmin=? [F<=50 finished] on consensus/coin4_6..."); @@ -195,13 +195,13 @@ TEST(SparseMdpPrctlModelCheckerTest, Consensus) { LOG4CPLUS_WARN(logger, "Done."); ASSERT_NE(nullptr, result); - ASSERT_LT(std::abs((*result)[31168] - 0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); + ASSERT_LT(std::abs((*result)[31168] - 0.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); delete probFormula; delete result; apFormula = new storm::property::prctl::Ap("finished"); - boundedEventuallyFormula = new storm::property::prctl::BoundedEventually(apFormula, 50); + boundedEventuallyFormula = new storm::property::prctl::BoundedEventually(apFormula, 50ull); probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(boundedEventuallyFormula, false); LOG4CPLUS_WARN(logger, "Model Checking Pmax=? [F<=50 finished] on consensus/coin4_6..."); @@ -209,7 +209,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Consensus) { LOG4CPLUS_WARN(logger, "Done."); ASSERT_NE(nullptr, result); - ASSERT_LT(std::abs((*result)[31168] - 0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); + ASSERT_LT(std::abs((*result)[31168] - 0.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); delete probFormula; delete result;