sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Introduced executable storm-functional-tests and storm-performance-tests. While the former contains the previous tests, the latter is currently empty, but will hold performance tests in the future.

main
dehnert 12 years ago
parent
27de566228
commit
3851377064
9 changed files with 109 additions and 105 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 45
      CMakeLists.txt
  2. 8
      src/modelchecker/SparseDtmcPrctlModelChecker.h
  3. 2
      test/functional/eigen/EigenSparseMatrixTest.cpp
  4. 128
      test/functional/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp
  5. 7
      test/functional/parser/CslParserTest.cpp
  6. 4
      test/functional/parser/ParseMdpTest.cpp
  7. 8
      test/functional/parser/ReadLabFileTest.cpp
  8. 8
      test/functional/parser/ReadTraFileTest.cpp
  9. 4
      test/functional/storm-functional-tests.cpp

45
CMakeLists.txt
View File

@ -95,7 +95,7 @@ else(CLANG)
# As CLANG is not set as a variable, we need to set it in case we have not matched another compiler. # As CLANG is not set as a variable, we need to set it in case we have not matched another compiler.
set (CLANG ON) set (CLANG ON)
# Set standard flags for clang # Set standard flags for clang
set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -funroll-loops -O4")
set (CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -funroll-loops -O4")
set (CMAKE_CXX_FLAGS "-std=c++11 -stdlib=libc++ -Wall -Werror -pedantic -Wno-unused-variable -DBOOST_RESULT_OF_USE_TR1 -DBOOST_NO_DECLTYPE") set (CMAKE_CXX_FLAGS "-std=c++11 -stdlib=libc++ -Wall -Werror -pedantic -Wno-unused-variable -DBOOST_RESULT_OF_USE_TR1 -DBOOST_NO_DECLTYPE")
set (CMAKE_CXX_FLAGS_DEBUG "-g") set (CMAKE_CXX_FLAGS_DEBUG "-g")
@ -131,6 +131,7 @@ file(GLOB_RECURSE STORM_IR_FILES ${PROJECT_SOURCE_DIR}/src/ir/*.h ${PROJECT_SOUR
# Test Sources # Test Sources
# Note that the tests also need the source files, except for the main file # 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_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)
# Group the headers and sources # Group the headers and sources
source_group(main FILES ${STORM_MAIN_FILE}) source_group(main FILES ${STORM_MAIN_FILE})
@ -143,7 +144,8 @@ source_group(parser FILES ${STORM_PARSER_FILES})
source_group(storage FILES ${STORM_STORAGE_FILES}) source_group(storage FILES ${STORM_STORAGE_FILES})
source_group(utility FILES ${STORM_UTILITY_FILES}) source_group(utility FILES ${STORM_UTILITY_FILES})
source_group(ir FILES ${STORM_IR_FILES}) source_group(ir FILES ${STORM_IR_FILES})
source_group(test FILES ${STORM_TEST_FILES})
source_group(functional-test FILES ${STORM_FUNCTIONAL_TEST_FILES})
source_group(performance-test FILES ${STORM_PERFORMANCE_TEST_FILES})
# Add base folder for better inclusion paths # Add base folder for better inclusion paths
include_directories("${PROJECT_SOURCE_DIR}") include_directories("${PROJECT_SOURCE_DIR}")
@ -231,11 +233,13 @@ add_executable(storm-performance-tests ${STORM_PERFORMANCE_TEST_FILES} ${STORM_S
# Add target link deps for Boost program options # Add target link deps for Boost program options
target_link_libraries(storm ${Boost_LIBRARIES}) target_link_libraries(storm ${Boost_LIBRARIES})
target_link_libraries(storm-tests ${Boost_LIBRARIES})
target_link_libraries(storm-functional-tests ${Boost_LIBRARIES})
target_link_libraries(storm-performance-tests ${Boost_LIBRARIES})
if (USE_INTELTBB) if (USE_INTELTBB)
target_link_libraries(storm tbb tbbmalloc) target_link_libraries(storm tbb tbbmalloc)
target_link_libraries(storm-tests tbb tbbmalloc)
target_link_libraries(storm-functional-tests tbb tbbmalloc)
target_link_libraries(storm-performance-tests tbb tbbmalloc)
endif(USE_INTELTBB) endif(USE_INTELTBB)
if (APPLE) if (APPLE)
@ -256,14 +260,16 @@ if (STORM_USE_COTIRE)
cotire(storm) cotire(storm)
target_link_libraries(storm_unity ${Boost_LIBRARIES}) target_link_libraries(storm_unity ${Boost_LIBRARIES})
#cotire(storm-tests)
#cotire(storm-functional-tests)
#cotire(storm-performance-tests)
endif() endif()
# Link against libc++abi if requested. May be needed to build on Linux systems using clang. # Link against libc++abi if requested. May be needed to build on Linux systems using clang.
if (LINK_LIBCXXABI) if (LINK_LIBCXXABI)
message (STATUS "Linking against libc++abi.") message (STATUS "Linking against libc++abi.")
target_link_libraries(storm "c++abi") target_link_libraries(storm "c++abi")
target_link_libraries(storm-tests "c++abi")
target_link_libraries(storm-functional-tests "c++abi")
target_link_libraries(storm-performance-tests "c++abi")
endif(LINK_LIBCXXABI) endif(LINK_LIBCXXABI)
# Add a target to generate API documentation with Doxygen # Add a target to generate API documentation with Doxygen
@ -282,9 +288,11 @@ if (GTEST_INCLUDE_DIR)
enable_testing() enable_testing()
include_directories(${GTEST_INCLUDE_DIR}) include_directories(${GTEST_INCLUDE_DIR})
target_link_libraries(storm-tests ${GTEST_LIBRARIES})
target_link_libraries(storm-functional-tests ${GTEST_LIBRARIES})
target_link_libraries(storm-performance-tests ${GTEST_LIBRARIES})
add_test(NAME storm-tests COMMAND storm-tests)
add_test(NAME storm-functional-tests COMMAND storm-functional-tests)
add_test(NAME storm-performance-tests COMMAND storm-performance-tests)
if(MSVC) # VS2012 doesn't support correctly the tuples yet if(MSVC) # VS2012 doesn't support correctly the tuples yet
add_definitions( /D _VARIADIC_MAX=10 ) add_definitions( /D _VARIADIC_MAX=10 )
endif() endif()
@ -296,20 +304,23 @@ if (LOG4CPLUS_INCLUDE_DIR)
if (STORM_USE_COTIRE) if (STORM_USE_COTIRE)
target_link_libraries(storm_unity ${LOG4CPLUS_LIBRARIES}) target_link_libraries(storm_unity ${LOG4CPLUS_LIBRARIES})
endif(STORM_USE_COTIRE) endif(STORM_USE_COTIRE)
target_link_libraries(storm-tests ${LOG4CPLUS_LIBRARIES})
target_link_libraries(storm-functional-tests ${LOG4CPLUS_LIBRARIES})
target_link_libraries(storm-performance-tests ${LOG4CPLUS_LIBRARIES})
# On Linux, we have to link against librt # On Linux, we have to link against librt
if (UNIX AND NOT APPLE) if (UNIX AND NOT APPLE)
target_link_libraries(storm rt) target_link_libraries(storm rt)
if (STORM_USE_COTIRE) if (STORM_USE_COTIRE)
target_link_libraries(storm_unity rt) target_link_libraries(storm_unity rt)
endif(STORM_USE_COTIRE) endif(STORM_USE_COTIRE)
target_link_libraries(storm-tests rt)
target_link_libraries(storm-functional-tests rt)
target_link_libraries(storm-performance-tests rt)
endif(UNIX AND NOT APPLE) endif(UNIX AND NOT APPLE)
endif(LOG4CPLUS_INCLUDE_DIR) endif(LOG4CPLUS_INCLUDE_DIR)
if (CUDD_LIBRARY_DIRS) if (CUDD_LIBRARY_DIRS)
target_link_libraries(storm "-lobj -lcudd -lmtr -lst -lutil -lepd") target_link_libraries(storm "-lobj -lcudd -lmtr -lst -lutil -lepd")
target_link_libraries(storm-tests "-lobj -lcudd -lmtr -lst -lutil -lepd")
target_link_libraries(storm-functional-tests "-lobj -lcudd -lmtr -lst -lutil -lepd")
target_link_libraries(storm-performance-tests "-lobj -lcudd -lmtr -lst -lutil -lepd")
endif(CUDD_LIBRARY_DIRS) endif(CUDD_LIBRARY_DIRS)
if (THREADS_FOUND) if (THREADS_FOUND)
@ -318,7 +329,8 @@ if (THREADS_FOUND)
if (STORM_USE_COTIRE) if (STORM_USE_COTIRE)
target_link_libraries(storm_unity ${CMAKE_THREAD_LIBS_INIT}) target_link_libraries(storm_unity ${CMAKE_THREAD_LIBS_INIT})
endif(STORM_USE_COTIRE) endif(STORM_USE_COTIRE)
target_link_libraries(storm-tests ${CMAKE_THREAD_LIBS_INIT})
target_link_libraries(storm-functional-tests ${CMAKE_THREAD_LIBS_INIT})
target_link_libraries(storm-performance-tests ${CMAKE_THREAD_LIBS_INIT})
endif(THREADS_FOUND) endif(THREADS_FOUND)
# Configure a header file to pass some of the CMake settings to the source code # Configure a header file to pass some of the CMake settings to the source code
@ -327,10 +339,9 @@ configure_file (
"${PROJECT_BINARY_DIR}/storm-config.h" "${PROJECT_BINARY_DIR}/storm-config.h"
) )
add_custom_target(memcheck valgrind --leak-check=full --show-reachable=yes ${PROJECT_BINARY_DIR}/storm -v --fix-deadlocks ${PROJECT_SOURCE_DIR}/examples/dtmc/crowds/crowds5_5.tra examples/dtmc/crowds/crowds5_5.lab
DEPENDS storm)
add_custom_target(memcheck-tests valgrind --leak-check=full --show-reachable=yes ${PROJECT_BINARY_DIR}/storm-tests -v --fix-deadlocks
DEPENDS storm-tests)
add_custom_target(memcheck valgrind --leak-check=full --show-reachable=yes ${PROJECT_BINARY_DIR}/storm -v --fix-deadlocks ${PROJECT_SOURCE_DIR}/examples/dtmc/crowds/crowds5_5.tra examples/dtmc/crowds/crowds5_5.lab DEPENDS storm)
add_custom_target(memcheck-functional-tests valgrind --leak-check=full --show-reachable=yes ${PROJECT_BINARY_DIR}/storm-functional-tests -v --fix-deadlocks DEPENDS storm-functional-tests)
add_custom_target(memcheck-performance-tests valgrind --leak-check=full --show-reachable=yes ${PROJECT_BINARY_DIR}/storm-performance-tests -v --fix-deadlocks DEPENDS storm-performance-tests)
set (CPPLINT_ARGS --filter=-whitespace/tab,-whitespace/line_length,-legal/copyright,-readability/streams) set (CPPLINT_ARGS --filter=-whitespace/tab,-whitespace/line_length,-legal/copyright,-readability/streams)
add_custom_target(style python cpplint.py ${CPPLINT_ARGS} `find ./src/ -iname "*.h" -or -iname "*.cpp"`) add_custom_target(style python cpplint.py ${CPPLINT_ARGS} `find ./src/ -iname "*.h" -or -iname "*.cpp"`)

8
src/modelchecker/SparseDtmcPrctlModelChecker.h
View File

@ -94,10 +94,6 @@ public:
// Make all rows absorbing that violate both sub-formulas or satisfy the second sub-formula. // Make all rows absorbing that violate both sub-formulas or satisfy the second sub-formula.
tmpMatrix.makeRowsAbsorbing(~(*leftStates | *rightStates) | *rightStates); tmpMatrix.makeRowsAbsorbing(~(*leftStates | *rightStates) | *rightStates);
// Delete obsolete intermediates.
delete leftStates;
delete rightStates;
// Create the vector with which to multiply. // Create the vector with which to multiply.
std::vector<Type>* result = new std::vector<Type>(this->getModel().getNumberOfStates()); std::vector<Type>* result = new std::vector<Type>(this->getModel().getNumberOfStates());
storm::utility::setVectorValues(result, *rightStates, storm::utility::constGetOne<Type>()); storm::utility::setVectorValues(result, *rightStates, storm::utility::constGetOne<Type>());
@ -105,7 +101,9 @@ public:
// Perform the matrix vector multiplication as often as required by the formula bound. // Perform the matrix vector multiplication as often as required by the formula bound.
this->performMatrixVectorMultiplication(tmpMatrix, *result, nullptr, formula.getBound()); this->performMatrixVectorMultiplication(tmpMatrix, *result, nullptr, formula.getBound());
// Return result.
// Delete obsolete intermediates and return result.
delete leftStates;
delete rightStates;
return result; return result;
} }

2
test/functional/eigen/EigenSparseMatrixTest.cpp
View File

@ -18,7 +18,7 @@ TEST(EigenSparseMatrixTest, BasicReadWriteTest) {
int position_row[50] = { int position_row[50] = {
2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
2, 2, 2, 2, /* first row empty, one full row ��� 25 minus the diagonal entry */
2, 2, 2, 2, /* first row empty, one full row 25 minus the diagonal entry */
4, 4, /* one empty row, then first and last column */ 4, 4, /* one empty row, then first and last column */
13, 13, 13, 13, /* a few empty rows, middle columns */ 13, 13, 13, 13, /* a few empty rows, middle columns */
24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24,

128
test/functional/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp
View File

@ -7,164 +7,164 @@
TEST(GmmxxMdpPrctModelCheckerTest, Dice) { TEST(GmmxxMdpPrctModelCheckerTest, Dice) {
storm::settings::Settings* s = storm::settings::instance(); storm::settings::Settings* s = storm::settings::instance();
storm::parser::AutoParser<double> 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<double> 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); ASSERT_EQ(parser.getType(), storm::models::MDP);
std::shared_ptr<storm::models::Mdp<double>> mdp = parser.getModel<storm::models::Mdp<double>>(); std::shared_ptr<storm::models::Mdp<double>> mdp = parser.getModel<storm::models::Mdp<double>>();
ASSERT_EQ(mdp->getNumberOfStates(), 169u); ASSERT_EQ(mdp->getNumberOfStates(), 169u);
ASSERT_EQ(mdp->getNumberOfTransitions(), 436u); ASSERT_EQ(mdp->getNumberOfTransitions(), 436u);
storm::modelchecker::GmmxxMdpPrctlModelChecker<double> mc(*mdp); storm::modelchecker::GmmxxMdpPrctlModelChecker<double> mc(*mdp);
storm::property::prctl::Ap<double>* apFormula = new storm::property::prctl::Ap<double>("two"); storm::property::prctl::Ap<double>* apFormula = new storm::property::prctl::Ap<double>("two");
storm::property::prctl::Eventually<double>* eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula); storm::property::prctl::Eventually<double>* eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
storm::property::prctl::ProbabilisticNoBoundOperator<double>* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true); storm::property::prctl::ProbabilisticNoBoundOperator<double>* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
std::vector<double>* result = mc.checkNoBoundOperator(*probFormula); std::vector<double>* result = mc.checkNoBoundOperator(*probFormula);
ASSERT_NE(nullptr, result); ASSERT_NE(nullptr, result);
ASSERT_LT(std::abs((*result)[0] - 0.0277777612209320068), s->get<double>("precision")); ASSERT_LT(std::abs((*result)[0] - 0.0277777612209320068), s->get<double>("precision"));
delete probFormula; delete probFormula;
delete result; delete result;
apFormula = new storm::property::prctl::Ap<double>("two"); apFormula = new storm::property::prctl::Ap<double>("two");
eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula); eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false); probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false);
result = mc.checkNoBoundOperator(*probFormula); result = mc.checkNoBoundOperator(*probFormula);
ASSERT_LT(std::abs((*result)[0] - 0.0277777612209320068), s->get<double>("precision")); ASSERT_LT(std::abs((*result)[0] - 0.0277777612209320068), s->get<double>("precision"));
delete probFormula; delete probFormula;
delete result; delete result;
apFormula = new storm::property::prctl::Ap<double>("three"); apFormula = new storm::property::prctl::Ap<double>("three");
eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula); eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true); probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
result = mc.checkNoBoundOperator(*probFormula); result = mc.checkNoBoundOperator(*probFormula);
ASSERT_LT(std::abs((*result)[0] - 0.0555555224418640136), s->get<double>("precision")); ASSERT_LT(std::abs((*result)[0] - 0.0555555224418640136), s->get<double>("precision"));
delete probFormula; delete probFormula;
delete result; delete result;
apFormula = new storm::property::prctl::Ap<double>("three"); apFormula = new storm::property::prctl::Ap<double>("three");
eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula); eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false); probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false);
result = mc.checkNoBoundOperator(*probFormula); result = mc.checkNoBoundOperator(*probFormula);
ASSERT_LT(std::abs((*result)[0] - 0.0555555224418640136), s->get<double>("precision")); ASSERT_LT(std::abs((*result)[0] - 0.0555555224418640136), s->get<double>("precision"));
delete probFormula; delete probFormula;
delete result; delete result;
apFormula = new storm::property::prctl::Ap<double>("four"); apFormula = new storm::property::prctl::Ap<double>("four");
eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula); eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true); probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
result = mc.checkNoBoundOperator(*probFormula); result = mc.checkNoBoundOperator(*probFormula);
ASSERT_LT(std::abs((*result)[0] - 0.083333283662796020508), s->get<double>("precision")); ASSERT_LT(std::abs((*result)[0] - 0.083333283662796020508), s->get<double>("precision"));
delete probFormula; delete probFormula;
delete result; delete result;
apFormula = new storm::property::prctl::Ap<double>("four"); apFormula = new storm::property::prctl::Ap<double>("four");
eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula); eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false); probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false);
result = mc.checkNoBoundOperator(*probFormula); result = mc.checkNoBoundOperator(*probFormula);
ASSERT_LT(std::abs((*result)[0] - 0.083333283662796020508), s->get<double>("precision")); ASSERT_LT(std::abs((*result)[0] - 0.083333283662796020508), s->get<double>("precision"));
delete probFormula; delete probFormula;
delete result; delete result;
apFormula = new storm::property::prctl::Ap<double>("done"); apFormula = new storm::property::prctl::Ap<double>("done");
storm::property::prctl::ReachabilityReward<double>* reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula); storm::property::prctl::ReachabilityReward<double>* reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
storm::property::prctl::RewardNoBoundOperator<double>* rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, true); storm::property::prctl::RewardNoBoundOperator<double>* rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, true);
result = mc.checkNoBoundOperator(*rewardFormula); result = mc.checkNoBoundOperator(*rewardFormula);
ASSERT_LT(std::abs((*result)[0] - 7.3333294987678527832), s->get<double>("precision")); ASSERT_LT(std::abs((*result)[0] - 7.3333294987678527832), s->get<double>("precision"));
delete rewardFormula; delete rewardFormula;
delete result; delete result;
apFormula = new storm::property::prctl::Ap<double>("done"); apFormula = new storm::property::prctl::Ap<double>("done");
reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula); reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, false); rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, false);
result = mc.checkNoBoundOperator(*rewardFormula);; result = mc.checkNoBoundOperator(*rewardFormula);;
ASSERT_LT(std::abs((*result)[0] - 7.3333294987678527832), s->get<double>("precision")); ASSERT_LT(std::abs((*result)[0] - 7.3333294987678527832), s->get<double>("precision"));
delete rewardFormula; delete rewardFormula;
delete result; delete result;
storm::parser::AutoParser<double> stateRewardParser(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.state.rew", "");
storm::parser::AutoParser<double> 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", "");
ASSERT_EQ(stateRewardParser.getType(), storm::models::MDP); ASSERT_EQ(stateRewardParser.getType(), storm::models::MDP);
std::shared_ptr<storm::models::Mdp<double>> stateRewardMdp = stateRewardParser.getModel<storm::models::Mdp<double>>(); std::shared_ptr<storm::models::Mdp<double>> stateRewardMdp = stateRewardParser.getModel<storm::models::Mdp<double>>();
storm::modelchecker::GmmxxMdpPrctlModelChecker<double> stateRewardModelChecker(*stateRewardMdp); storm::modelchecker::GmmxxMdpPrctlModelChecker<double> stateRewardModelChecker(*stateRewardMdp);
apFormula = new storm::property::prctl::Ap<double>("done"); apFormula = new storm::property::prctl::Ap<double>("done");
reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula); reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, true); rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, true);
result = stateRewardModelChecker.checkNoBoundOperator(*rewardFormula); result = stateRewardModelChecker.checkNoBoundOperator(*rewardFormula);
ASSERT_LT(std::abs((*result)[0] - 7.3333294987678527832), s->get<double>("precision")); ASSERT_LT(std::abs((*result)[0] - 7.3333294987678527832), s->get<double>("precision"));
delete rewardFormula; delete rewardFormula;
delete result; delete result;
apFormula = new storm::property::prctl::Ap<double>("done"); apFormula = new storm::property::prctl::Ap<double>("done");
reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula); reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, false); rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, false);
result = stateRewardModelChecker.checkNoBoundOperator(*rewardFormula); result = stateRewardModelChecker.checkNoBoundOperator(*rewardFormula);
ASSERT_LT(std::abs((*result)[0] - 7.3333294987678527832), s->get<double>("precision")); ASSERT_LT(std::abs((*result)[0] - 7.3333294987678527832), s->get<double>("precision"));
delete rewardFormula; delete rewardFormula;
delete result; delete result;
storm::parser::AutoParser<double> stateAndTransitionRewardParser(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.state.rew", STORM_CPP_TESTS_BASE_PATH "/functional/two_dice/two_dice.flip.trans.rew");
storm::parser::AutoParser<double> 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");
ASSERT_EQ(stateAndTransitionRewardParser.getType(), storm::models::MDP); ASSERT_EQ(stateAndTransitionRewardParser.getType(), storm::models::MDP);
std::shared_ptr<storm::models::Mdp<double>> stateAndTransitionRewardMdp = stateAndTransitionRewardParser.getModel<storm::models::Mdp<double>>(); std::shared_ptr<storm::models::Mdp<double>> stateAndTransitionRewardMdp = stateAndTransitionRewardParser.getModel<storm::models::Mdp<double>>();
storm::modelchecker::GmmxxMdpPrctlModelChecker<double> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp); storm::modelchecker::GmmxxMdpPrctlModelChecker<double> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp);
apFormula = new storm::property::prctl::Ap<double>("done"); apFormula = new storm::property::prctl::Ap<double>("done");
reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula); reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, true); rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, true);
result = stateAndTransitionRewardModelChecker.checkNoBoundOperator(*rewardFormula); result = stateAndTransitionRewardModelChecker.checkNoBoundOperator(*rewardFormula);
ASSERT_LT(std::abs((*result)[0] - (2 * 7.3333294987678527832)), s->get<double>("precision")); ASSERT_LT(std::abs((*result)[0] - (2 * 7.3333294987678527832)), s->get<double>("precision"));
delete rewardFormula; delete rewardFormula;
delete result; delete result;
apFormula = new storm::property::prctl::Ap<double>("done"); apFormula = new storm::property::prctl::Ap<double>("done");
reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula); reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, false); rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, false);
result = stateAndTransitionRewardModelChecker.checkNoBoundOperator(*rewardFormula); result = stateAndTransitionRewardModelChecker.checkNoBoundOperator(*rewardFormula);
ASSERT_LT(std::abs((*result)[0] - (2 * 7.3333294987678527832)), s->get<double>("precision")); ASSERT_LT(std::abs((*result)[0] - (2 * 7.3333294987678527832)), s->get<double>("precision"));
delete rewardFormula; delete rewardFormula;
delete result; delete result;
} }

7
test/functional/parser/CslParserTest.cpp
View File

@ -127,14 +127,9 @@ TEST(CslParserTest, parseComplexFormulaTest) {
} }
TEST(CslParserTest, wrongProbabilisticFormulaTest) { TEST(CslParserTest, wrongProbabilisticFormulaTest) {
storm::parser::CslParser* cslParser = nullptr; storm::parser::CslParser* cslParser = nullptr;
ASSERT_THROW(
cslParser = new storm::parser::CslParser("P > 0.5 [ a ]"),
storm::exceptions::WrongFormatException
);
ASSERT_THROW(cslParser = new storm::parser::CslParser("P > 0.5 [ a ]"), storm::exceptions::WrongFormatException);
delete cslParser; delete cslParser;
} }

4
test/functional/parser/ParseMdpTest.cpp
View File

@ -13,8 +13,8 @@
TEST(ParseMdpTest, parseAndOutput) { TEST(ParseMdpTest, parseAndOutput) {
storm::parser::NondeterministicModelParser* mdpParser = nullptr; storm::parser::NondeterministicModelParser* mdpParser = nullptr;
ASSERT_NO_THROW(mdpParser = new storm::parser::NondeterministicModelParser( ASSERT_NO_THROW(mdpParser = new storm::parser::NondeterministicModelParser(
STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/mdp_general_input_01.tra",
STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/pctl_general_input_01.lab"));
STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_general_input_01.tra",
STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/pctl_general_input_01.lab"));
std::shared_ptr<storm::models::Mdp<double>> mdp = mdpParser->getMdp(); std::shared_ptr<storm::models::Mdp<double>> mdp = mdpParser->getMdp();
std::shared_ptr<storm::storage::SparseMatrix<double>> matrix = mdp->getTransitionMatrix(); std::shared_ptr<storm::storage::SparseMatrix<double>> matrix = mdp->getTransitionMatrix();

8
test/functional/parser/ReadLabFileTest.cpp
View File

@ -25,7 +25,7 @@ TEST(ReadLabFileTest, ParseTest) {
storm::parser::AtomicPropositionLabelingParser* parser = nullptr; storm::parser::AtomicPropositionLabelingParser* parser = nullptr;
//Parsing the file //Parsing the file
ASSERT_NO_THROW(parser = new storm::parser::AtomicPropositionLabelingParser(12, STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/pctl_general_input_01.lab"));
ASSERT_NO_THROW(parser = new storm::parser::AtomicPropositionLabelingParser(12, STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/pctl_general_input_01.lab"));
std::shared_ptr<storm::models::AtomicPropositionsLabeling> labeling(parser->getLabeling()); std::shared_ptr<storm::models::AtomicPropositionsLabeling> labeling(parser->getLabeling());
//Checking whether all propositions are in the labelling //Checking whether all propositions are in the labelling
@ -89,14 +89,14 @@ TEST(ReadLabFileTest, ParseTest) {
} }
TEST(ReadLabFileTest, WrongHeaderTest1) { TEST(ReadLabFileTest, WrongHeaderTest1) {
ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser(3, STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/wrong_format_header1.lab"), storm::exceptions::WrongFormatException);
ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser(3, STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/wrong_format_header1.lab"), storm::exceptions::WrongFormatException);
} }
TEST(ReadLabFileTest, WrongHeaderTest2) { TEST(ReadLabFileTest, WrongHeaderTest2) {
ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser(3, STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/wrong_format_header2.lab"), storm::exceptions::WrongFormatException);
ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser(3, STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/wrong_format_header2.lab"), storm::exceptions::WrongFormatException);
} }
TEST(ReadLabFileTest, WrongPropositionTest) { TEST(ReadLabFileTest, WrongPropositionTest) {
ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser(3, STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/wrong_format_proposition.lab"), storm::exceptions::WrongFormatException);
ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser(3, STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/wrong_format_proposition.lab"), storm::exceptions::WrongFormatException);
} }

8
test/functional/parser/ReadTraFileTest.cpp
View File

@ -21,7 +21,7 @@ TEST(ReadTraFileTest, NonExistingFileTest) {
*/ */
TEST(ReadTraFileTest, ParseFileTest1) { TEST(ReadTraFileTest, ParseFileTest1) {
storm::parser::DeterministicSparseTransitionParser* parser = nullptr; storm::parser::DeterministicSparseTransitionParser* parser = nullptr;
ASSERT_NO_THROW(parser = new storm::parser::DeterministicSparseTransitionParser(STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/csl_general_input_01.tra"));
ASSERT_NO_THROW(parser = new storm::parser::DeterministicSparseTransitionParser(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/csl_general_input_01.tra"));
std::shared_ptr<storm::storage::SparseMatrix<double>> result = parser->getMatrix(); std::shared_ptr<storm::storage::SparseMatrix<double>> result = parser->getMatrix();
if (result != nullptr) { if (result != nullptr) {
@ -73,13 +73,13 @@ TEST(ReadTraFileTest, ParseFileTest1) {
} }
TEST(ReadTraFileTest, WrongFormatTestHeader1) { TEST(ReadTraFileTest, WrongFormatTestHeader1) {
ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser(STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/wrong_format_header1.tra"), storm::exceptions::WrongFormatException);
ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/wrong_format_header1.tra"), storm::exceptions::WrongFormatException);
} }
TEST(ReadTraFileTest, WrongFormatTestHeader2) { TEST(ReadTraFileTest, WrongFormatTestHeader2) {
ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser(STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/wrong_format_header2.tra"), storm::exceptions::WrongFormatException);
ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/wrong_format_header2.tra"), storm::exceptions::WrongFormatException);
} }
TEST(ReadTraFileTest, WrongFormatTestTransition) { TEST(ReadTraFileTest, WrongFormatTestTransition) {
ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser(STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/wrong_format_transition.tra"), storm::exceptions::WrongFormatException);
ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/wrong_format_transition.tra"), storm::exceptions::WrongFormatException);
} }

4
test/functional/storm-functional-tests.cpp
View File

@ -15,7 +15,7 @@ log4cplus::Logger logger;
* Initializes the logging framework. * Initializes the logging framework.
*/ */
void setUpLogging() { void setUpLogging() {
log4cplus::SharedAppenderPtr fileLogAppender(new log4cplus::FileAppender("storm-tests.log"));
log4cplus::SharedAppenderPtr fileLogAppender(new log4cplus::FileAppender("storm-functional-tests.log"));
fileLogAppender->setName("mainFileAppender"); fileLogAppender->setName("mainFileAppender");
fileLogAppender->setLayout(std::auto_ptr<log4cplus::Layout>(new log4cplus::PatternLayout("%-5p - %D{%H:%M} (%r ms) - %F:%L : %m%n"))); fileLogAppender->setLayout(std::auto_ptr<log4cplus::Layout>(new log4cplus::PatternLayout("%-5p - %D{%H:%M} (%r ms) - %F:%L : %m%n")));
logger = log4cplus::Logger::getInstance("mainLogger"); logger = log4cplus::Logger::getInstance("mainLogger");
@ -58,7 +58,7 @@ int main(int argc, char* argv[]) {
if (!parseOptions(argc, argv)) { if (!parseOptions(argc, argv)) {
return 0; return 0;
} }
std::cout << "STORM Testing Suite" << std::endl;
std::cout << "StoRM (Functional) Testing Suite" << std::endl;
testing::InitGoogleTest(&argc, argv); testing::InitGoogleTest(&argc, argv);

Write Preview
Loading…
Cancel
Save