diff --git a/CMakeLists.txt b/CMakeLists.txt index a99f224da..744e10d9b 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -130,8 +130,8 @@ file(GLOB_RECURSE STORM_IR_FILES ${PROJECT_SOURCE_DIR}/src/ir/*.h ${PROJECT_SOUR # Test Sources # Note that the tests also need the source files, except for the main file -file(GLOB_RECURSE STORM_FUNCTIONAL_TEST_FILES ${PROJECT_SOURCE_DIR}/test/functional/*.h ${PROJECT_SOURCE_DIR}/test/functional/*.cpp) -file(GLOB_RECURSE STORM_PERFORMANCE_TEST_FILES ${PROJECT_SOURCE_DIR}/test/performance/*.h ${PROJECT_SOURCE_DIR}/test/performance/*.cpp) +file(GLOB_RECURSE STORM_FUNCTIONAL_TEST_FILES ${STORM_CPP_TESTS_BASE_PATH}/functional/*.h ${STORM_CPP_TESTS_BASE_PATH}/functional/*.cpp) +file(GLOB_RECURSE STORM_PERFORMANCE_TEST_FILES ${STORM_CPP_TESTS_BASE_PATH}/performance/*.h ${STORM_CPP_TESTS_BASE_PATH}/performance/*.cpp) # Group the headers and sources source_group(main FILES ${STORM_MAIN_FILE}) diff --git a/examples/mdp/two_dice/two_dice.nm b/examples/mdp/two_dice/two_dice.nm index e1bf34aea..778153138 100644 --- a/examples/mdp/two_dice/two_dice.nm +++ b/examples/mdp/two_dice/two_dice.nm @@ -17,7 +17,7 @@ module die1 [] s1=4 -> 0.5 : (s1'=7) & (d1'=2) + 0.5 : (s1'=7) & (d1'=3); [] s1=5 -> 0.5 : (s1'=7) & (d1'=4) + 0.5 : (s1'=7) & (d1'=5); [] s1=6 -> 0.5 : (s1'=2) + 0.5 : (s1'=7) & (d1'=6); - [] s1=7 & s2=7 -> (s1'=7); + [] s1=7 & s2=7 -> 1: (s1'=7); endmodule module die2 = die1 [ s1=s2, s2=s1, d1=d2 ] endmodule diff --git a/src/modelchecker/SparseMdpPrctlModelChecker.h b/src/modelchecker/SparseMdpPrctlModelChecker.h index b9c80e24b..0c951ae8f 100644 --- a/src/modelchecker/SparseMdpPrctlModelChecker.h +++ b/src/modelchecker/SparseMdpPrctlModelChecker.h @@ -99,7 +99,7 @@ public: // Make all rows absorbing that violate both sub-formulas or satisfy the second sub-formula. tmpMatrix.makeRowsAbsorbing(~(*leftStates | *rightStates) | *rightStates, *this->getModel().getNondeterministicChoiceIndices()); - + // Create the vector with which to multiply. std::vector* result = new std::vector(this->getModel().getNumberOfStates()); storm::utility::setVectorValues(result, *rightStates, storm::utility::constGetOne()); diff --git a/storm-config.h.in b/storm-config.h.in index bb44dec25..0b1cd5134 100644 --- a/storm-config.h.in +++ b/storm-config.h.in @@ -1,4 +1,5 @@ // the configured options and settings for STORM #define STORM_CPP_VERSION_MAJOR @STORM_CPP_VERSION_MAJOR@ #define STORM_CPP_VERSION_MINOR @STORM_CPP_VERSION_MINOR@ -#define STORM_CPP_TESTS_BASE_PATH "@STORM_CPP_TESTS_BASE_PATH@" \ No newline at end of file +#define STORM_CPP_BASE_PATH "@PROJECT_SOURCE_DIR@" +#define STORM_CPP_TESTS_BASE_PATH "@STORM_CPP_TESTS_BASE_PATH@" diff --git a/test/functional/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp index 2286cd8d9..e3eb08b68 100644 --- a/test/functional/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp @@ -8,7 +8,7 @@ TEST(GmmxxDtmcPrctModelCheckerTest, Die) { storm::settings::Settings* s = storm::settings::instance(); s->set("fix-deadlocks"); - 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"); + 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); @@ -75,7 +75,7 @@ TEST(GmmxxDtmcPrctModelCheckerTest, Die) { TEST(GmmxxDtmcPrctModelCheckerTest, Crowds) { storm::settings::Settings* s = storm::settings::instance(); s->set("fix-deadlocks"); - 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", "", ""); + 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); @@ -129,7 +129,7 @@ TEST(GmmxxDtmcPrctModelCheckerTest, Crowds) { TEST(GmmxxDtmcPrctModelCheckerTest, SynchronousLeader) { storm::settings::Settings* s = storm::settings::instance(); s->set("fix-deadlocks"); - 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"); + 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); diff --git a/test/functional/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp index b440df38d..32cf5b9a4 100644 --- a/test/functional/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp @@ -7,7 +7,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) { storm::settings::Settings* s = storm::settings::instance(); - storm::parser::AutoParser parser(STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/two_dice/two_dice.tra", STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/two_dice/two_dice.lab", "", STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/two_dice/two_dice.flip.trans.rew"); + storm::parser::AutoParser parser(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.trans.rew"); ASSERT_EQ(parser.getType(), storm::models::MDP); @@ -108,7 +108,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) { delete rewardFormula; delete result; - storm::parser::AutoParser stateRewardParser(STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/two_dice/two_dice.tra", STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/two_dice/two_dice.lab", STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/two_dice/two_dice.flip.state.rew", ""); + storm::parser::AutoParser stateRewardParser(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.state.rew", ""); ASSERT_EQ(stateRewardParser.getType(), storm::models::MDP); @@ -138,7 +138,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) { delete rewardFormula; delete result; - storm::parser::AutoParser stateAndTransitionRewardParser(STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/two_dice/two_dice.tra", STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/two_dice/two_dice.lab", STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/two_dice/two_dice.flip.state.rew", STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/two_dice/two_dice.flip.trans.rew"); + storm::parser::AutoParser stateAndTransitionRewardParser(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.state.rew", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.trans.rew"); ASSERT_EQ(stateAndTransitionRewardParser.getType(), storm::models::MDP); @@ -171,7 +171,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) { TEST(GmmxxMdpPrctModelCheckerTest, AsynchronousLeader) { storm::settings::Settings* s = storm::settings::instance(); - storm::parser::AutoParser parser(STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/asynchronous_leader/leader4.tra", STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/asynchronous_leader/leader4.lab", "", STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/asynchronous_leader/leader4.trans.rew"); + storm::parser::AutoParser parser(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.trans.rew"); ASSERT_EQ(parser.getType(), storm::models::MDP); diff --git a/test/functional/modelchecker/die/testFormulas.prctl b/test/functional/modelchecker/die/testFormulas.prctl deleted file mode 100644 index 8deea6c43..000000000 --- a/test/functional/modelchecker/die/testFormulas.prctl +++ /dev/null @@ -1,4 +0,0 @@ -P=? [ F one ] -P=? [ F two ] -P=? [ F three ] -R=? [ F done ] diff --git a/test/performance/storm-performance-tests.cpp b/test/performance/storm-performance-tests.cpp new file mode 100644 index 000000000..1e1317a80 --- /dev/null +++ b/test/performance/storm-performance-tests.cpp @@ -0,0 +1,66 @@ +#include + +#include "gtest/gtest.h" +#include "log4cplus/logger.h" +#include "log4cplus/loggingmacros.h" +#include "log4cplus/consoleappender.h" +#include "log4cplus/fileappender.h" + +#include "src/utility/Settings.h" +#include "src/modelchecker/GmmxxDtmcPrctlModelChecker.h" + +log4cplus::Logger logger; + +/*! + * Initializes the logging framework. + */ +void setUpLogging() { + log4cplus::SharedAppenderPtr fileLogAppender(new log4cplus::FileAppender("storm-functional-tests.log")); + fileLogAppender->setName("mainFileAppender"); + fileLogAppender->setLayout(std::auto_ptr(new log4cplus::PatternLayout("%-5p - %D{%H:%M} (%r ms) - %F:%L : %m%n"))); + logger = log4cplus::Logger::getInstance("mainLogger"); + logger.addAppender(fileLogAppender); + + // Uncomment these lines to enable console logging output + // log4cplus::SharedAppenderPtr consoleLogAppender(new log4cplus::ConsoleAppender()); + // consoleLogAppender->setName("mainConsoleAppender"); + // consoleLogAppender->setLayout(std::auto_ptr(new log4cplus::PatternLayout("%-5p - %D{%H:%M:%s} (%r ms) - %F:%L : %m%n"))); + // logger.addAppender(consoleLogAppender); +} + +/*! + * Function that parses the command line options. + * @param argc The argc argument of main(). + * @param argv The argv argument of main(). + * @return True iff the program should continue to run after parsing the options. + */ +bool parseOptions(int const argc, char const * const argv[]) { + storm::settings::Settings* s = nullptr; + try { + storm::settings::Settings::registerModule>(); + s = storm::settings::newInstance(argc, argv, nullptr, true); + } catch (storm::exceptions::InvalidSettingsException& e) { + std::cout << "Could not recover from settings error: " << e.what() << "." << std::endl; + std::cout << std::endl << storm::settings::help; + return false; + } + + if (s->isSet("help")) { + std::cout << storm::settings::help; + return false; + } + + return true; +} + +int main(int argc, char* argv[]) { + setUpLogging(); + if (!parseOptions(argc, argv)) { + return 0; + } + std::cout << "StoRM (Performance) Testing Suite" << std::endl; + + testing::InitGoogleTest(&argc, argv); + + return RUN_ALL_TESTS(); +}