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;