diff --git a/CMakeLists.txt b/CMakeLists.txt index ae2c1fa2c..91df3d3f4 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -130,7 +130,7 @@ 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_TEST_FILES ${PROJECT_SOURCE_DIR}/test/*.h ${PROJECT_SOURCE_DIR}/test/*.cpp) +file(GLOB_RECURSE STORM_FUNCTIONAL_TEST_FILES ${PROJECT_SOURCE_DIR}/test/functional/*.h ${PROJECT_SOURCE_DIR}/test/functional/*.cpp) # Group the headers and sources source_group(main FILES ${STORM_MAIN_FILE}) @@ -226,7 +226,8 @@ endif(CUDD_LIBRARY_DIRS) # Add the executables # Must be created *after* Boost was added because of LINK_DIRECTORIES add_executable(storm ${STORM_SOURCES} ${STORM_HEADERS}) -add_executable(storm-tests ${STORM_TEST_FILES} ${STORM_SOURCES_WITHOUT_MAIN} ${STORM_HEADERS}) +add_executable(storm-functional-tests ${STORM_FUNCTIONAL_TEST_FILES} ${STORM_SOURCES_WITHOUT_MAIN} ${STORM_HEADERS}) +add_executable(storm-performance-tests ${STORM_PERFORMANCE_TEST_FILES} ${STORM_SOURCES_WITHOUT_MAIN} ${STORM_HEADERS}) # Add target link deps for Boost program options target_link_libraries(storm ${Boost_LIBRARIES}) diff --git a/resources/3rdparty/cudd-2.5.0/Makefile b/resources/3rdparty/cudd-2.5.0/Makefile index 6c7fbb4d3..95a0a47d5 100644 --- a/resources/3rdparty/cudd-2.5.0/Makefile +++ b/resources/3rdparty/cudd-2.5.0/Makefile @@ -51,7 +51,7 @@ RANLIB = ranlib #ICFLAGS = # These two are typical settings for optimized code with gcc. #ICFLAGS = -g -O3 -Wall -ICFLAGS = -O3 +ICFLAGS = -O4 # Use XCFLAGS to specify machine-dependent compilation flags. # For some platforms no special flags are needed. diff --git a/test/eigen/EigenSparseMatrixTest.cpp b/test/functional/eigen/EigenSparseMatrixTest.cpp similarity index 100% rename from test/eigen/EigenSparseMatrixTest.cpp rename to test/functional/eigen/EigenSparseMatrixTest.cpp diff --git a/test/functional/EigenDtmcPrctModelCheckerTest.cpp b/test/functional/modelchecker/EigenDtmcPrctModelCheckerTest.cpp similarity index 91% rename from test/functional/EigenDtmcPrctModelCheckerTest.cpp rename to test/functional/modelchecker/EigenDtmcPrctModelCheckerTest.cpp index f2774c259..ced6139cb 100644 --- a/test/functional/EigenDtmcPrctModelCheckerTest.cpp +++ b/test/functional/modelchecker/EigenDtmcPrctModelCheckerTest.cpp @@ -9,7 +9,7 @@ TEST(EigenDtmcPrctModelCheckerTest, Die) { storm::settings::Settings* s = storm::settings::instance(); s->set("fix-deadlocks"); - storm::parser::AutoParser parser(STORM_CPP_TESTS_BASE_PATH "/functional/die/die.tra", STORM_CPP_TESTS_BASE_PATH "/functional/die/die.lab", "", STORM_CPP_TESTS_BASE_PATH "/functional/die/die.coin_flips.trans.rew"); + 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); @@ -69,7 +69,7 @@ TEST(EigenDtmcPrctModelCheckerTest, Die) { TEST(EigenDtmcPrctModelCheckerTest, Crowds) { storm::settings::Settings* s = storm::settings::instance(); s->set("fix-deadlocks"); - storm::parser::AutoParser parser(STORM_CPP_TESTS_BASE_PATH "/functional/crowds/crowds5_5.tra", STORM_CPP_TESTS_BASE_PATH "/functional/crowds/crowds5_5.lab", "", ""); + 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); @@ -117,7 +117,7 @@ TEST(EigenDtmcPrctModelCheckerTest, Crowds) { TEST(EigenDtmcPrctModelCheckerTest, SynchronousLeader) { storm::settings::Settings* s = storm::settings::instance(); s->set("fix-deadlocks"); - storm::parser::AutoParser parser(STORM_CPP_TESTS_BASE_PATH "/functional/synchronous_leader/leader4_8.tra", STORM_CPP_TESTS_BASE_PATH "/functional/synchronous_leader/leader4_8.lab", "", STORM_CPP_TESTS_BASE_PATH "/functional/synchronous_leader/leader4_8.pick.trans.rew"); + 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/GmmxxDtmcPrctModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp similarity index 92% rename from test/functional/GmmxxDtmcPrctModelCheckerTest.cpp rename to test/functional/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp index aa2a014fa..2286cd8d9 100644 --- a/test/functional/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/die/die.tra", STORM_CPP_TESTS_BASE_PATH "/functional/die/die.lab", "", STORM_CPP_TESTS_BASE_PATH "/functional/die/die.coin_flips.trans.rew"); + 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); @@ -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/crowds/crowds5_5.tra", STORM_CPP_TESTS_BASE_PATH "/functional/crowds/crowds5_5.lab", "", ""); + 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); @@ -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/synchronous_leader/leader4_8.tra", STORM_CPP_TESTS_BASE_PATH "/functional/synchronous_leader/leader4_8.lab", "", STORM_CPP_TESTS_BASE_PATH "/functional/synchronous_leader/leader4_8.pick.trans.rew"); + 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/GmmxxMdpPrctModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp similarity index 95% rename from test/functional/GmmxxMdpPrctModelCheckerTest.cpp rename to test/functional/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp index 13136cc69..43fbd9c35 100644 --- a/test/functional/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/two_dice/two_dice.tra", STORM_CPP_TESTS_BASE_PATH "/functional/two_dice/two_dice.lab", "", STORM_CPP_TESTS_BASE_PATH "/functional/two_dice/two_dice.flip.trans.rew"); + 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"); ASSERT_EQ(parser.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/asynchronous_leader/leader4.tra", STORM_CPP_TESTS_BASE_PATH "/functional/asynchronous_leader/leader4.lab", "", STORM_CPP_TESTS_BASE_PATH "/functional/asynchronous_leader/leader4.trans.rew"); + 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"); ASSERT_EQ(parser.getType(), storm::models::MDP); diff --git a/test/functional/die/testFormulas.prctl b/test/functional/modelchecker/die/testFormulas.prctl similarity index 100% rename from test/functional/die/testFormulas.prctl rename to test/functional/modelchecker/die/testFormulas.prctl diff --git a/test/parser/.gitignore b/test/functional/parser/.gitignore similarity index 100% rename from test/parser/.gitignore rename to test/functional/parser/.gitignore diff --git a/test/parser/CslParserTest.cpp b/test/functional/parser/CslParserTest.cpp similarity index 100% rename from test/parser/CslParserTest.cpp rename to test/functional/parser/CslParserTest.cpp diff --git a/test/parser/LtlParserTest.cpp b/test/functional/parser/LtlParserTest.cpp similarity index 100% rename from test/parser/LtlParserTest.cpp rename to test/functional/parser/LtlParserTest.cpp diff --git a/test/parser/ParseMdpTest.cpp b/test/functional/parser/ParseMdpTest.cpp similarity index 100% rename from test/parser/ParseMdpTest.cpp rename to test/functional/parser/ParseMdpTest.cpp diff --git a/test/parser/ParsePrismTest.cpp b/test/functional/parser/ParsePrismTest.cpp similarity index 100% rename from test/parser/ParsePrismTest.cpp rename to test/functional/parser/ParsePrismTest.cpp diff --git a/test/parser/PrctlParserTest.cpp b/test/functional/parser/PrctlParserTest.cpp similarity index 100% rename from test/parser/PrctlParserTest.cpp rename to test/functional/parser/PrctlParserTest.cpp diff --git a/test/parser/ReadLabFileTest.cpp b/test/functional/parser/ReadLabFileTest.cpp similarity index 100% rename from test/parser/ReadLabFileTest.cpp rename to test/functional/parser/ReadLabFileTest.cpp diff --git a/test/parser/ReadTraFileTest.cpp b/test/functional/parser/ReadTraFileTest.cpp similarity index 100% rename from test/parser/ReadTraFileTest.cpp rename to test/functional/parser/ReadTraFileTest.cpp diff --git a/test/parser/prctl_files/apOnly.prctl b/test/functional/parser/prctl_files/apOnly.prctl similarity index 100% rename from test/parser/prctl_files/apOnly.prctl rename to test/functional/parser/prctl_files/apOnly.prctl diff --git a/test/parser/prctl_files/complexFormula.prctl b/test/functional/parser/prctl_files/complexFormula.prctl similarity index 100% rename from test/parser/prctl_files/complexFormula.prctl rename to test/functional/parser/prctl_files/complexFormula.prctl diff --git a/test/parser/prctl_files/probabilisticFormula.prctl b/test/functional/parser/prctl_files/probabilisticFormula.prctl similarity index 100% rename from test/parser/prctl_files/probabilisticFormula.prctl rename to test/functional/parser/prctl_files/probabilisticFormula.prctl diff --git a/test/parser/prctl_files/probabilisticNoBoundFormula.prctl b/test/functional/parser/prctl_files/probabilisticNoBoundFormula.prctl similarity index 100% rename from test/parser/prctl_files/probabilisticNoBoundFormula.prctl rename to test/functional/parser/prctl_files/probabilisticNoBoundFormula.prctl diff --git a/test/parser/prctl_files/propositionalFormula.prctl b/test/functional/parser/prctl_files/propositionalFormula.prctl similarity index 100% rename from test/parser/prctl_files/propositionalFormula.prctl rename to test/functional/parser/prctl_files/propositionalFormula.prctl diff --git a/test/parser/prctl_files/rewardFormula.prctl b/test/functional/parser/prctl_files/rewardFormula.prctl similarity index 100% rename from test/parser/prctl_files/rewardFormula.prctl rename to test/functional/parser/prctl_files/rewardFormula.prctl diff --git a/test/parser/prctl_files/rewardNoBoundFormula.prctl b/test/functional/parser/prctl_files/rewardNoBoundFormula.prctl similarity index 100% rename from test/parser/prctl_files/rewardNoBoundFormula.prctl rename to test/functional/parser/prctl_files/rewardNoBoundFormula.prctl diff --git a/test/parser/readme.txt b/test/functional/parser/readme.txt similarity index 100% rename from test/parser/readme.txt rename to test/functional/parser/readme.txt diff --git a/test/storage/BitVectorTest.cpp b/test/functional/storage/BitVectorTest.cpp similarity index 100% rename from test/storage/BitVectorTest.cpp rename to test/functional/storage/BitVectorTest.cpp diff --git a/test/storage/SparseMatrixTest.cpp b/test/functional/storage/SparseMatrixTest.cpp similarity index 100% rename from test/storage/SparseMatrixTest.cpp rename to test/functional/storage/SparseMatrixTest.cpp diff --git a/test/storage/adapters/EigenAdapterTest.cpp b/test/functional/storage/adapters/EigenAdapterTest.cpp similarity index 100% rename from test/storage/adapters/EigenAdapterTest.cpp rename to test/functional/storage/adapters/EigenAdapterTest.cpp diff --git a/test/storage/adapters/GmmAdapterTest.cpp b/test/functional/storage/adapters/GmmAdapterTest.cpp similarity index 100% rename from test/storage/adapters/GmmAdapterTest.cpp rename to test/functional/storage/adapters/GmmAdapterTest.cpp diff --git a/test/storage/adapters/StormAdapterTest.cpp b/test/functional/storage/adapters/StormAdapterTest.cpp similarity index 100% rename from test/storage/adapters/StormAdapterTest.cpp rename to test/functional/storage/adapters/StormAdapterTest.cpp diff --git a/test/storm-tests.cpp b/test/functional/storm-functional-tests.cpp similarity index 100% rename from test/storm-tests.cpp rename to test/functional/storm-functional-tests.cpp