Browse Source

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: a400a36f69
main
PBerger 12 years ago
parent
commit
11cc7fc6bc
  1. 70
      src/settings/InternalOptionMemento.h
  2. 4
      src/settings/Option.h
  3. 32
      src/settings/Settings.h
  4. 9
      test/functional/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp
  5. 30
      test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp
  6. 16
      test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
  7. 8
      test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp
  8. 14
      test/functional/parser/ParsePrismTest.cpp
  9. 11
      test/functional/storm-functional-tests.cpp
  10. 48
      test/performance/graph/GraphTest.cpp
  11. 17
      test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp
  12. 30
      test/performance/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp
  13. 24
      test/performance/modelchecker/SparseMdpPrctlModelCheckerTest.cpp

70
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_

4
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;

32
src/settings/Settings.h

@ -47,6 +47,7 @@ namespace settings {
typedef std::pair<bool, std::string> 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);
}
};
/*!

9
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<double> 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<double> 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<double> 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);

30
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<double> 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<storm::models::Dtmc<double>> dtmc = parser.getModel<storm::models::Dtmc<double>>();
ASSERT_EQ(dtmc->getNumberOfStates(), 13u);
ASSERT_EQ(dtmc->getNumberOfTransitions(), 27u);
ASSERT_EQ(dtmc->getNumberOfStates(), 13ull);
ASSERT_EQ(dtmc->getNumberOfTransitions(), 27ull);
storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(*dtmc, new storm::solver::GmmxxLinearEquationSolver<double>());
@ -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<double> 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<storm::models::Dtmc<double>> dtmc = parser.getModel<storm::models::Dtmc<double>>();
ASSERT_EQ(dtmc->getNumberOfStates(), 8607u);
ASSERT_EQ(dtmc->getNumberOfTransitions(), 22460u);
ASSERT_EQ(dtmc->getNumberOfStates(), 8607ull);
ASSERT_EQ(dtmc->getNumberOfTransitions(), 22460ull);
storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(*dtmc, new storm::solver::GmmxxLinearEquationSolver<double>());
@ -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<double> 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<storm::models::Dtmc<double>> dtmc = parser.getModel<storm::models::Dtmc<double>>();
ASSERT_EQ(dtmc->getNumberOfStates(), 12400u);
ASSERT_EQ(dtmc->getNumberOfTransitions(), 28894u);
ASSERT_EQ(dtmc->getNumberOfStates(), 12400ull);
ASSERT_EQ(dtmc->getNumberOfTransitions(), 28894ull);
storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(*dtmc, new storm::solver::GmmxxLinearEquationSolver<double>());
@ -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;

16
test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp

@ -14,8 +14,8 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) {
std::shared_ptr<storm::models::Mdp<double>> mdp = parser.getModel<storm::models::Mdp<double>>();
ASSERT_EQ(mdp->getNumberOfStates(), 169u);
ASSERT_EQ(mdp->getNumberOfTransitions(), 436u);
ASSERT_EQ(mdp->getNumberOfStates(), 169ull);
ASSERT_EQ(mdp->getNumberOfTransitions(), 436ull);
storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> mc(*mdp, new storm::solver::GmmxxNondeterministicLinearEquationSolver<double>());
@ -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<storm::models::Mdp<double>> mdp = parser.getModel<storm::models::Mdp<double>>();
ASSERT_EQ(mdp->getNumberOfStates(), 3172u);
ASSERT_EQ(mdp->getNumberOfTransitions(), 7144u);
ASSERT_EQ(mdp->getNumberOfStates(), 3172ull);
ASSERT_EQ(mdp->getNumberOfTransitions(), 7144ull);
storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> mc(*mdp, new storm::solver::GmmxxNondeterministicLinearEquationSolver<double>());
@ -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;

8
test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp

@ -13,8 +13,8 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) {
std::shared_ptr<storm::models::Mdp<double>> mdp = parser.getModel<storm::models::Mdp<double>>();
ASSERT_EQ(mdp->getNumberOfStates(), 169u);
ASSERT_EQ(mdp->getNumberOfTransitions(), 436u);
ASSERT_EQ(mdp->getNumberOfStates(), 169ull);
ASSERT_EQ(mdp->getNumberOfTransitions(), 436ull);
storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> mc(*mdp, new storm::solver::AbstractNondeterministicLinearEquationSolver<double>());
@ -176,8 +176,8 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) {
std::shared_ptr<storm::models::Mdp<double>> mdp = parser.getModel<storm::models::Mdp<double>>();
ASSERT_EQ(mdp->getNumberOfStates(), 3172u);
ASSERT_EQ(mdp->getNumberOfTransitions(), 7144u);
ASSERT_EQ(mdp->getNumberOfStates(), 3172ull);
ASSERT_EQ(mdp->getNumberOfTransitions(), 7144ull);
storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> mc(*mdp, new storm::solver::AbstractNondeterministicLinearEquationSolver<double>());

14
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<storm::models::Dtmc<double>> model = adapter.getModel()->as<storm::models::Dtmc<double>>();
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<storm::models::Mdp<double>> model = adapter.getModel()->as<storm::models::Mdp<double>>();
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);
}

11
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();

48
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<storm::storage::BitVector, storm::storage::BitVector> 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<storm::storage::BitVector, storm::storage::BitVector> 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<std::vector<uint_fast64_t>> 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<bool> 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;
}

17
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<double> 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<storm::models::Dtmc<double>> dtmc = parser.getModel<storm::models::Dtmc<double>>();
ASSERT_EQ(dtmc->getNumberOfStates(), 2036647u);
ASSERT_EQ(dtmc->getNumberOfTransitions(), 8973900u);
ASSERT_EQ(dtmc->getNumberOfStates(), 2036647ull);
ASSERT_EQ(dtmc->getNumberOfTransitions(), 8973900ull);
storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(*dtmc, new storm::solver::GmmxxLinearEquationSolver<double>());
@ -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<double> 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<storm::models::Dtmc<double>> dtmc = parser.getModel<storm::models::Dtmc<double>>();
ASSERT_EQ(dtmc->getNumberOfStates(), 1312334u);
ASSERT_EQ(dtmc->getNumberOfTransitions(), 2886810u);
ASSERT_EQ(dtmc->getNumberOfStates(), 1312334ull);
ASSERT_EQ(dtmc->getNumberOfTransitions(), 2886810ull);
storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(*dtmc, new storm::solver::GmmxxLinearEquationSolver<double>());
@ -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;

30
test/performance/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp

@ -14,8 +14,8 @@ TEST(GmmxxMdpPrctlModelCheckerTest, AsynchronousLeader) {
std::shared_ptr<storm::models::Mdp<double>> mdp = parser.getModel<storm::models::Mdp<double>>();
ASSERT_EQ(mdp->getNumberOfStates(), 2095783u);
ASSERT_EQ(mdp->getNumberOfTransitions(), 7714385u);
ASSERT_EQ(mdp->getNumberOfStates(), 2095783ull);
ASSERT_EQ(mdp->getNumberOfTransitions(), 7714385ull);
storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> mc(*mdp, new storm::solver::GmmxxNondeterministicLinearEquationSolver<double>());
@ -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<double>("elected");
storm::property::prctl::BoundedEventually<double>* boundedEventuallyFormula = new storm::property::prctl::BoundedEventually<double>(apFormula, 25);
storm::property::prctl::BoundedEventually<double>* boundedEventuallyFormula = new storm::property::prctl::BoundedEventually<double>(apFormula, 25ull);
probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(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<double>("elected");
boundedEventuallyFormula = new storm::property::prctl::BoundedEventually<double>(apFormula, 25);
boundedEventuallyFormula = new storm::property::prctl::BoundedEventually<double>(apFormula, 25ull);
probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(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<storm::models::Mdp<double>> mdp = parser.getModel<storm::models::Mdp<double>>();
ASSERT_EQ(mdp->getNumberOfStates(), 63616u);
ASSERT_EQ(mdp->getNumberOfTransitions(), 213472u);
ASSERT_EQ(mdp->getNumberOfStates(), 63616ull);
ASSERT_EQ(mdp->getNumberOfTransitions(), 213472ull);
storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> mc(*mdp, new storm::solver::GmmxxNondeterministicLinearEquationSolver<double>());
@ -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<double>("finished");
storm::property::prctl::BoundedEventually<double>* boundedEventuallyFormula = new storm::property::prctl::BoundedEventually<double>(apFormula, 50);
storm::property::prctl::BoundedEventually<double>* boundedEventuallyFormula = new storm::property::prctl::BoundedEventually<double>(apFormula, 50ull);
probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(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<double>("finished");
boundedEventuallyFormula = new storm::property::prctl::BoundedEventually<double>(apFormula, 50);
boundedEventuallyFormula = new storm::property::prctl::BoundedEventually<double>(apFormula, 50ull);
probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(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;

24
test/performance/modelchecker/SparseMdpPrctlModelCheckerTest.cpp

@ -14,8 +14,8 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) {
std::shared_ptr<storm::models::Mdp<double>> mdp = parser.getModel<storm::models::Mdp<double>>();
ASSERT_EQ(mdp->getNumberOfStates(), 2095783u);
ASSERT_EQ(mdp->getNumberOfTransitions(), 7714385u);
ASSERT_EQ(mdp->getNumberOfStates(), 2095783ull);
ASSERT_EQ(mdp->getNumberOfTransitions(), 7714385ull);
storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> mc(*mdp, new storm::solver::AbstractNondeterministicLinearEquationSolver<double>());
@ -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<storm::models::Mdp<double>> mdp = parser.getModel<storm::models::Mdp<double>>();
ASSERT_EQ(mdp->getNumberOfStates(), 63616u);
ASSERT_EQ(mdp->getNumberOfTransitions(), 213472u);
ASSERT_EQ(mdp->getNumberOfStates(), 63616ull);
ASSERT_EQ(mdp->getNumberOfTransitions(), 213472ull);
storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> mc(*mdp, new storm::solver::AbstractNondeterministicLinearEquationSolver<double>());
@ -187,7 +187,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Consensus) {
delete result;
apFormula = new storm::property::prctl::Ap<double>("finished");
storm::property::prctl::BoundedEventually<double>* boundedEventuallyFormula = new storm::property::prctl::BoundedEventually<double>(apFormula, 50);
storm::property::prctl::BoundedEventually<double>* boundedEventuallyFormula = new storm::property::prctl::BoundedEventually<double>(apFormula, 50ull);
probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(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<double>("finished");
boundedEventuallyFormula = new storm::property::prctl::BoundedEventually<double>(apFormula, 50);
boundedEventuallyFormula = new storm::property::prctl::BoundedEventually<double>(apFormula, 50ull);
probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(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;

Loading…
Cancel
Save