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

Moved main testfiles into tests/storm/ and the storm-pars testfiles into tests/storm-pars

main
TimQu 9 years ago
parent
62d50b336b
commit
4191d17f1e
92 changed files with 719 additions and 721 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. 25
      src/test/CMakeLists.txt
  2. 385
      src/test/modelchecker/SparseDtmcParameterLiftingTest.cpp
  3. 313
      src/test/modelchecker/SparseMdpParameterLiftingTest.cpp
  4. 23
      src/test/storm-pars/CMakeLists.txt
  5. 362
      src/test/storm-pars/modelchecker/SparseDtmcParameterLiftingTest.cpp
  6. 301
      src/test/storm-pars/modelchecker/SparseMdpParameterLiftingTest.cpp
  7. 8
      src/test/storm-pars/storm-test.cpp
  8. 23
      src/test/storm/CMakeLists.txt
  9. 0
      src/test/storm/abstraction/PrismMenuGameTest.cpp
  10. 0
      src/test/storm/adapter/MathsatExpressionAdapterTest.cpp
  11. 0
      src/test/storm/adapter/Z3ExpressionAdapterTest.cpp
  12. 0
      src/test/storm/builder/DdJaniModelBuilderTest.cpp
  13. 0
      src/test/storm/builder/DdPrismModelBuilderTest.cpp
  14. 0
      src/test/storm/builder/ExplicitJaniModelBuilderTest.cpp
  15. 0
      src/test/storm/builder/ExplicitJitJaniModelBuilderTest.cpp
  16. 0
      src/test/storm/builder/ExplicitPrismModelBuilderTest.cpp
  17. 0
      src/test/storm/logic/FragmentCheckerTest.cpp
  18. 0
      src/test/storm/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp
  19. 0
      src/test/storm/modelchecker/GameBasedDtmcModelCheckerTest.cpp
  20. 0
      src/test/storm/modelchecker/GameBasedMdpModelCheckerTest.cpp
  21. 0
      src/test/storm/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp
  22. 0
      src/test/storm/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp
  23. 0
      src/test/storm/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp
  24. 0
      src/test/storm/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp
  25. 0
      src/test/storm/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp
  26. 0
      src/test/storm/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
  27. 0
      src/test/storm/modelchecker/NativeCtmcCslModelCheckerTest.cpp
  28. 0
      src/test/storm/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp
  29. 0
      src/test/storm/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp
  30. 0
      src/test/storm/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp
  31. 0
      src/test/storm/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp
  32. 0
      src/test/storm/modelchecker/NativeMdpPrctlModelCheckerTest.cpp
  33. 0
      src/test/storm/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp
  34. 0
      src/test/storm/modelchecker/SparseExplorationModelCheckerTest.cpp
  35. 0
      src/test/storm/modelchecker/SparseMaCbMultiObjectiveModelCheckerTest.cpp
  36. 0
      src/test/storm/modelchecker/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp
  37. 0
      src/test/storm/modelchecker/SparseMdpCbMultiObjectiveModelCheckerTest.cpp
  38. 0
      src/test/storm/modelchecker/SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp
  39. 0
      src/test/storm/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp
  40. 0
      src/test/storm/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp
  41. 0
      src/test/storm/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp
  42. 0
      src/test/storm/parser/.gitignore
  43. 0
      src/test/storm/parser/AutoParserTest.cpp
  44. 0
      src/test/storm/parser/DeterministicModelParserTest.cpp
  45. 0
      src/test/storm/parser/DeterministicSparseTransitionParserTest.cpp
  46. 0
      src/test/storm/parser/DirectEncodingParserTest.cpp
  47. 0
      src/test/storm/parser/FormulaParserTest.cpp
  48. 0
      src/test/storm/parser/MappedFileTest.cpp
  49. 0
      src/test/storm/parser/MarkovAutomatonParserTest.cpp
  50. 0
      src/test/storm/parser/MarkovAutomatonSparseTransitionParserTest.cpp
  51. 0
      src/test/storm/parser/NondeterministicModelParserTest.cpp
  52. 0
      src/test/storm/parser/NondeterministicSparseTransitionParserTest.cpp
  53. 0
      src/test/storm/parser/PrismParserTest.cpp
  54. 0
      src/test/storm/parser/SparseItemLabelingParserTest.cpp
  55. 0
      src/test/storm/parser/SparseStateRewardParserTest.cpp
  56. 0
      src/test/storm/permissiveschedulers/MilpPermissiveSchedulerTest.cpp
  57. 0
      src/test/storm/permissiveschedulers/SmtPermissiveSchedulerTest.cpp
  58. 0
      src/test/storm/solver/CudaPluginTest.cpp
  59. 0
      src/test/storm/solver/EigenLinearEquationSolverTest.cpp
  60. 0
      src/test/storm/solver/EliminationLinearEquationSolverTest.cpp
  61. 0
      src/test/storm/solver/FullySymbolicGameSolverTest.cpp
  62. 0
      src/test/storm/solver/GameSolverTest.cpp
  63. 0
      src/test/storm/solver/GlpkLpSolverTest.cpp
  64. 0
      src/test/storm/solver/GmmxxLinearEquationSolverTest.cpp
  65. 0
      src/test/storm/solver/GmmxxMinMaxLinearEquationSolverTest.cpp
  66. 0
      src/test/storm/solver/GurobiLpSolverTest.cpp
  67. 0
      src/test/storm/solver/MathsatSmtSolverTest.cpp
  68. 0
      src/test/storm/solver/MinMaxTechniqueSelectionTest.cpp
  69. 0
      src/test/storm/solver/NativeLinearEquationSolverTest.cpp
  70. 0
      src/test/storm/solver/NativeMinMaxLinearEquationSolverTest.cpp
  71. 0
      src/test/storm/solver/Z3LpSolverTest.cpp
  72. 0
      src/test/storm/solver/Z3SmtSolverTest.cpp
  73. 0
      src/test/storm/storage/BitVectorHashMapTest.cpp
  74. 0
      src/test/storm/storage/BitVectorTest.cpp
  75. 0
      src/test/storm/storage/CuddDdTest.cpp
  76. 0
      src/test/storm/storage/DeterministicModelBisimulationDecompositionTest.cpp
  77. 0
      src/test/storm/storage/ExpressionEvalutionTest.cpp
  78. 0
      src/test/storm/storage/ExpressionTest.cpp
  79. 0
      src/test/storm/storage/JaniModelTest.cpp
  80. 0
      src/test/storm/storage/MaximalEndComponentDecompositionTest.cpp
  81. 0
      src/test/storm/storage/NondeterministicModelBisimulationDecompositionTest.cpp
  82. 0
      src/test/storm/storage/PrismProgramTest.cpp
  83. 0
      src/test/storm/storage/SchedulerTest.cpp
  84. 0
      src/test/storm/storage/SparseMatrixTest.cpp
  85. 0
      src/test/storm/storage/StronglyConnectedComponentDecompositionTest.cpp
  86. 0
      src/test/storm/storage/SylvanDdTest.cpp
  87. 0
      src/test/storm/storm-test.cpp
  88. 0
      src/test/storm/transformer/EndComponentEliminatorTest.cpp
  89. 0
      src/test/storm/utility/GraphTest.cpp
  90. 0
      src/test/storm/utility/KSPTest.cpp
  91. 0
      src/test/storm/utility/ModelInstantiatorTest.cpp
  92. 0
      src/test/storm/utility/VectorTest.cpp

25
src/test/CMakeLists.txt
View File

@ -1,23 +1,2 @@
# Base path for test files
set(STORM_TESTS_BASE_PATH "${PROJECT_SOURCE_DIR}/src/test")
# Test Sources
file(GLOB_RECURSE ALL_FILES ${STORM_TESTS_BASE_PATH}/*.h ${STORM_TESTS_BASE_PATH}/*.cpp)
register_source_groups_from_filestructure("${ALL_FILES}" test)
# Note that the tests also need the source files, except for the main file
include_directories(${GTEST_INCLUDE_DIR})
foreach (testsuite abstraction adapter builder logic modelchecker parser permissiveschedulers solver storage transformer utility)
file(GLOB_RECURSE TEST_${testsuite}_FILES ${STORM_TESTS_BASE_PATH}/${testsuite}/*.h ${STORM_TESTS_BASE_PATH}/${testsuite}/*.cpp)
add_executable (test-${testsuite} ${TEST_${testsuite}_FILES} ${STORM_TESTS_BASE_PATH}/storm-test.cpp)
target_link_libraries(test-${testsuite} storm)
target_link_libraries(test-${testsuite} ${STORM_TEST_LINK_LIBRARIES})
add_dependencies(test-${testsuite} test-resources)
add_test(NAME run-test-${testsuite} COMMAND $<TARGET_FILE:test-${testsuite}>)
add_dependencies(tests test-${testsuite})
endforeach ()
add_subdirectory(storm)
add_subdirectory(storm-pars)

385
src/test/modelchecker/SparseDtmcParameterLiftingTest.cpp
View File

@ -1,385 +0,0 @@
#include "gtest/gtest.h"
#include "storm-config.h"
#ifdef STORM_HAVE_CARL
#include "storm/adapters/RationalFunctionAdapter.h"
#include "storm/modelchecker/parametric/SparseDtmcRegionChecker.h"
#include "storm/storage/ParameterRegion.h"
#include "storm/api/storm.h"
TEST(SparseDtmcParameterLiftingTest, Brp_Prob) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm";
std::string formulaAsString = "P<=0.84 [F s=5 ]";
std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5
// Program and formula
storm::prism::Program program = storm::api::parseProgram(programFile);
program = storm::utility::prism::preprocess(program, constantsAsString);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
storm::modelchecker::parametric::SparseDtmcRegionChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double, storm::RationalNumber> regionChecker(*model);
regionChecker.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
//start testing
auto allSatRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.7<=pL<=0.9,0.75<=pK<=0.95", modelParameters);
auto exBothRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.4<=pL<=0.65,0.75<=pK<=0.95", modelParameters);
auto allVioRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.1<=pL<=0.73,0.2<=pK<=0.715", modelParameters);
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, regionChecker.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, regionChecker.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, regionChecker.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
TEST(SparseDtmcParameterLiftingTest, Brp_Rew) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp_rewards16_2.pm";
std::string formulaAsString = "R>2.5 [F ((s=5) | (s=0&srep=3)) ]";
std::string constantsAsString = "pL=0.9,TOAck=0.5";
carl::VariablePool::getInstance().clear();
storm::prism::Program program = storm::api::parseProgram(programFile);
program = storm::utility::prism::preprocess(program, constantsAsString);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
storm::modelchecker::parametric::SparseDtmcRegionChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double, storm::RationalNumber> regionChecker(*model);
regionChecker.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
//start testing
auto allSatRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.7<=pK<=0.875,0.75<=TOMsg<=0.95", modelParameters);
auto exBothRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters);
auto allVioRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.1<=pK<=0.3,0.2<=TOMsg<=0.3", modelParameters);
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, regionChecker.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, regionChecker.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, regionChecker.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
TEST(SparseDtmcParameterLiftingTest, Brp_Rew_Bounded) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp_rewards16_2.pm";
std::string formulaAsString = "R>2.5 [ C<=300]";
std::string constantsAsString = "pL=0.9,TOAck=0.5";
carl::VariablePool::getInstance().clear();
storm::prism::Program program = storm::api::parseProgram(programFile);
program = storm::utility::prism::preprocess(program, constantsAsString);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
storm::modelchecker::parametric::SparseDtmcRegionChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double, storm::RationalNumber> regionChecker(*model);
regionChecker.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
//start testing
auto allSatRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.7<=pK<=0.875,0.75<=TOMsg<=0.95", modelParameters);
auto exBothRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters);
auto allVioRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.1<=pK<=0.3,0.2<=TOMsg<=0.3", modelParameters);
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, regionChecker.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, regionChecker.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, regionChecker.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
TEST(SparseDtmcParameterLiftingTest, Brp_Prob_exactValidation) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm";
std::string formulaAsString = "P<=0.84 [F s=5 ]";
std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5
// Program and formula
storm::prism::Program program = storm::api::parseProgram(programFile);
program = storm::utility::prism::preprocess(program, constantsAsString);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
storm::modelchecker::parametric::SparseDtmcRegionChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double, storm::RationalNumber> regionChecker(*model);
auto settings = regionChecker.getSettings();
settings.applyExactValidation = true;
regionChecker.setSettings(settings);
regionChecker.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
//start testing
auto allSatRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.7<=pL<=0.9,0.75<=pK<=0.95", modelParameters);
auto exBothRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.4<=pL<=0.65,0.75<=pK<=0.95", modelParameters);
auto allVioRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.1<=pL<=0.73,0.2<=pK<=0.715", modelParameters);
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, regionChecker.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, regionChecker.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, regionChecker.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
TEST(SparseDtmcParameterLiftingTest, Brp_Rew_exactValidation) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp_rewards16_2.pm";
std::string formulaAsString = "R>2.5 [F ((s=5) | (s=0&srep=3)) ]";
std::string constantsAsString = "pL=0.9,TOAck=0.5";
carl::VariablePool::getInstance().clear();
storm::prism::Program program = storm::api::parseProgram(programFile);
program = storm::utility::prism::preprocess(program, constantsAsString);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
storm::modelchecker::parametric::SparseDtmcRegionChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double, storm::RationalNumber> regionChecker(*model);
auto settings = regionChecker.getSettings();
settings.applyExactValidation = true;
regionChecker.setSettings(settings);
regionChecker.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
//start testing
auto allSatRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.7<=pK<=0.875,0.75<=TOMsg<=0.95", modelParameters);
auto exBothRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters);
auto allVioRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.1<=pK<=0.3,0.2<=TOMsg<=0.3", modelParameters);
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, regionChecker.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, regionChecker.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, regionChecker.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
TEST(SparseDtmcParameterLiftingTest, Brp_Rew_Bounded_exactValidation) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp_rewards16_2.pm";
std::string formulaAsString = "R>2.5 [ C<=300]";
std::string constantsAsString = "pL=0.9,TOAck=0.5";
carl::VariablePool::getInstance().clear();
storm::prism::Program program = storm::api::parseProgram(programFile);
program = storm::utility::prism::preprocess(program, constantsAsString);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
storm::modelchecker::parametric::SparseDtmcRegionChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double, storm::RationalNumber> regionChecker(*model);
auto settings = regionChecker.getSettings();
settings.applyExactValidation = true;
regionChecker.setSettings(settings);
regionChecker.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
//start testing
auto allSatRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.7<=pK<=0.875,0.75<=TOMsg<=0.95", modelParameters);
auto exBothRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters);
auto allVioRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.1<=pK<=0.3,0.2<=TOMsg<=0.3", modelParameters);
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, regionChecker.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, regionChecker.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, regionChecker.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
TEST(SparseDtmcParameterLiftingTest, Brp_Rew_Infty) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp_rewards16_2.pm";
std::string formulaAsString = "R>2.5 [F (s=0&srep=3) ]";
std::string constantsAsString = "";
carl::VariablePool::getInstance().clear();
storm::prism::Program program = storm::api::parseProgram(programFile);
program = storm::utility::prism::preprocess(program, constantsAsString);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
storm::modelchecker::parametric::SparseDtmcRegionChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double, storm::RationalNumber> regionChecker(*model);
regionChecker.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
//start testing
auto allSatRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.7<=pK<=0.9,0.6<=pL<=0.85,0.9<=TOMsg<=0.95,0.85<=TOAck<=0.9", modelParameters);
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, regionChecker.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
TEST(SparseDtmcParameterLiftingTest, Brp_Rew_4Par) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp_rewards16_2.pm";
std::string formulaAsString = "R>2.5 [F ((s=5) | (s=0&srep=3)) ]";
std::string constantsAsString = ""; //!! this model will have 4 parameters
carl::VariablePool::getInstance().clear();
storm::prism::Program program = storm::api::parseProgram(programFile);
program = storm::utility::prism::preprocess(program, constantsAsString);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
storm::modelchecker::parametric::SparseDtmcRegionChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double, storm::RationalNumber> regionChecker(*model);
regionChecker.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
//start testing
auto allSatRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.7<=pK<=0.9,0.6<=pL<=0.85,0.9<=TOMsg<=0.95,0.85<=TOAck<=0.9", modelParameters);
auto exBothRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.1<=pK<=0.7,0.2<=pL<=0.8,0.15<=TOMsg<=0.65,0.3<=TOAck<=0.9", modelParameters);
auto allVioRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.1<=pK<=0.4,0.2<=pL<=0.3,0.15<=TOMsg<=0.3,0.1<=TOAck<=0.2", modelParameters);
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, regionChecker.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, regionChecker.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, regionChecker.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
TEST(SparseDtmcParameterLiftingTest, Crowds_Prob) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/crowds3_5.pm";
std::string formulaAsString = "P<0.5 [F \"observe0Greater1\" ]";
std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5
carl::VariablePool::getInstance().clear();
storm::prism::Program program = storm::api::parseProgram(programFile);
program = storm::utility::prism::preprocess(program, constantsAsString);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
storm::modelchecker::parametric::SparseDtmcRegionChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double, storm::RationalNumber> regionChecker(*model);
regionChecker.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
//start testing
auto allSatRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.1<=PF<=0.75,0.15<=badC<=0.2", modelParameters);
auto exBothRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.75<=PF<=0.8,0.2<=badC<=0.3", modelParameters);
auto allVioRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.2", modelParameters);
auto allVioHardRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.9", modelParameters);
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, regionChecker.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, regionChecker.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, regionChecker.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::CenterViolated, regionChecker.analyzeRegion(allVioHardRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
TEST(SparseDtmcParameterLiftingTest, Crowds_Prob_stepBounded) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/crowds3_5.pm";
std::string formulaAsString = "P<0.5 [F<=300 \"observe0Greater1\" ]";
std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5
carl::VariablePool::getInstance().clear();
storm::prism::Program program = storm::api::parseProgram(programFile);
program = storm::utility::prism::preprocess(program, constantsAsString);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
storm::modelchecker::parametric::SparseDtmcRegionChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double, storm::RationalNumber> regionChecker(*model);
regionChecker.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
//start testing
auto allSatRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.1<=PF<=0.75,0.15<=badC<=0.2", modelParameters);
auto exBothRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.75<=PF<=0.8,0.2<=badC<=0.3", modelParameters);
auto allVioRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.2", modelParameters);
auto allVioHardRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.9", modelParameters);
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, regionChecker.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, regionChecker.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, regionChecker.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::CenterViolated, regionChecker.analyzeRegion(allVioHardRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
TEST(SparseDtmcParameterLiftingTest, Crowds_Prob_1Par) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/crowds3_5.pm";
std::string formulaAsString = "P>0.75 [F \"observe0Greater1\" ]";
std::string constantsAsString = "badC=0.3"; //e.g. pL=0.9,TOACK=0.5
carl::VariablePool::getInstance().clear();
storm::prism::Program program = storm::api::parseProgram(programFile);
program = storm::utility::prism::preprocess(program, constantsAsString);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
storm::modelchecker::parametric::SparseDtmcRegionChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double, storm::RationalNumber> regionChecker(*model);
regionChecker.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
//start testing
auto allSatRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.9<=PF<=0.99", modelParameters);
auto exBothRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.8<=PF<=0.9", modelParameters);
auto allVioRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.01<=PF<=0.8", modelParameters);
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, regionChecker.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, regionChecker.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, regionChecker.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
TEST(SparseDtmcParameterLiftingTest, Crowds_Prob_Const) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/crowds3_5.pm";
std::string formulaAsString = "P>0.6 [F \"observe0Greater1\" ]";
std::string constantsAsString = "PF=0.9,badC=0.2";
carl::VariablePool::getInstance().clear();
storm::prism::Program program = storm::api::parseProgram(programFile);
program = storm::utility::prism::preprocess(program, constantsAsString);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
storm::modelchecker::parametric::SparseDtmcRegionChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double, storm::RationalNumber> regionChecker(*model);
regionChecker.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
//start testing
auto allSatRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("", modelParameters);
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, regionChecker.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
#endif

313
src/test/modelchecker/SparseMdpParameterLiftingTest.cpp
View File

@ -1,313 +0,0 @@
#include "gtest/gtest.h"
#include "storm-config.h"
#ifdef STORM_HAVE_CARL
#include "storm/adapters/RationalFunctionAdapter.h"
#include "storm/modelchecker/parametric/SparseMdpRegionChecker.h"
#include "storm/storage/ParameterRegion.h"
#include "storm/api/storm.h"
TEST(SparseMdpParameterLiftingTest, two_dice_Prob) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/two_dice.nm";
std::string formulaFile = "P<=0.17 [ F \"doubles\" ]";
carl::VariablePool::getInstance().clear();
storm::prism::Program program = storm::api::parseProgram(programFile);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaFile, program));
std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
storm::modelchecker::parametric::SparseMdpRegionChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double, storm::RationalNumber> regionChecker(*model);
regionChecker.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
auto allSatRegion = storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.495<=p1<=0.5,0.5<=p2<=0.505", modelParameters);
auto exBothRegion = storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.45<=p1<=0.55,0.45<=p2<=0.55", modelParameters);
auto allVioRegion = storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.6<=p1<=0.7,0.6<=p2<=0.6", modelParameters);
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, regionChecker.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, regionChecker.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, regionChecker.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
TEST(SparseMdpParameterLiftingTest, two_dice_Prob_bounded) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/two_dice.nm";
std::string formulaFile = "P<=0.17 [ F<100 \"doubles\" ]";
carl::VariablePool::getInstance().clear();
storm::prism::Program program = storm::api::parseProgram(programFile);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaFile, program));
std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
storm::modelchecker::parametric::SparseMdpRegionChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double, storm::RationalNumber> regionChecker(*model);
regionChecker.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
auto allSatRegion = storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.495<=p1<=0.5,0.5<=p2<=0.505", modelParameters);
auto exBothRegion = storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.45<=p1<=0.55,0.45<=p2<=0.55", modelParameters);
auto allVioRegion = storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.6<=p1<=0.7,0.6<=p2<=0.6", modelParameters);
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, regionChecker.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, regionChecker.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, regionChecker.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
TEST(SparseMdpParameterLiftingTest, two_dice_Prob_exactValidation) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/two_dice.nm";
std::string formulaFile = "P<=0.17 [ F \"doubles\" ]";
carl::VariablePool::getInstance().clear();
storm::prism::Program program = storm::api::parseProgram(programFile);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaFile, program));
std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
storm::modelchecker::parametric::SparseMdpRegionChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double, storm::RationalNumber> regionChecker(*model);
regionChecker.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
auto allSatRegion = storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.495<=p1<=0.5,0.5<=p2<=0.505", modelParameters);
auto exBothRegion = storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.45<=p1<=0.55,0.45<=p2<=0.55", modelParameters);
auto allVioRegion = storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.6<=p1<=0.7,0.6<=p2<=0.6", modelParameters);
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, regionChecker.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, regionChecker.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, regionChecker.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
TEST(SparseMdpParameterLiftingTest, two_dice_Prob_bounded_exactValidation) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/two_dice.nm";
std::string formulaFile = "P<=0.17 [ F<100 \"doubles\" ]";
carl::VariablePool::getInstance().clear();
storm::prism::Program program = storm::api::parseProgram(programFile);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaFile, program));
std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
storm::modelchecker::parametric::SparseMdpRegionChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double, storm::RationalNumber> regionChecker(*model);
regionChecker.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
auto allSatRegion = storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.495<=p1<=0.5,0.5<=p2<=0.505", modelParameters);
auto exBothRegion = storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.45<=p1<=0.55,0.45<=p2<=0.55", modelParameters);
auto allVioRegion = storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.6<=p1<=0.7,0.6<=p2<=0.6", modelParameters);
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, regionChecker.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, regionChecker.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, regionChecker.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
TEST(SparseMdpParameterLiftingTest, coin_Prob) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/coin2_2.nm";
std::string formulaAsString = "P>0.25 [F \"finished\"&\"all_coins_equal_1\" ]";
storm::prism::Program program = storm::api::parseProgram(programFile);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
storm::modelchecker::parametric::SparseMdpRegionChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double, storm::RationalNumber> regionChecker(*model);
regionChecker.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
//start testing
auto allSatRegion = storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.3<=p1<=0.45,0.2<=p2<=0.54", modelParameters);
auto exBothRegion = storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.4<=p1<=0.65,0.5<=p2<=0.7", modelParameters);
auto allVioRegion = storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.4<=p1<=0.7,0.55<=p2<=0.6", modelParameters);
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, regionChecker.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, regionChecker.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, regionChecker.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
TEST(SparseMdpParameterLiftingTest, brp_Prop) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/brp16_2.nm";
std::string formulaAsString = "P<=0.84 [ F (s=5 & T) ]";
std::string constantsAsString = "TOMsg=0.0,TOAck=0.0";
storm::prism::Program program = storm::api::parseProgram(programFile);
program = storm::utility::prism::preprocess(program, constantsAsString);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
storm::modelchecker::parametric::SparseMdpRegionChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double, storm::RationalNumber> regionChecker(*model);
regionChecker.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
//start testing
auto allSatRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.7<=pL<=0.9,0.75<=pK<=0.95", modelParameters);
auto exBothRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.4<=pL<=0.65,0.75<=pK<=0.95", modelParameters);
auto allVioRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.1<=pL<=0.73,0.2<=pK<=0.715", modelParameters);
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, regionChecker.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, regionChecker.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, regionChecker.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
TEST(SparseMdpParameterLiftingTest, brp_Rew) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/brp16_2.nm";
std::string formulaAsString = "R>2.5 [F ((s=5) | (s=0&srep=3)) ]";
std::string constantsAsString = "pL=0.9,TOAck=0.5";
storm::prism::Program program = storm::api::parseProgram(programFile);
program = storm::utility::prism::preprocess(program, constantsAsString);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
storm::modelchecker::parametric::SparseMdpRegionChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double, storm::RationalNumber> regionChecker(*model);
regionChecker.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
//start testing
auto allSatRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.7<=pK<=0.875,0.75<=TOMsg<=0.95", modelParameters);
auto exBothRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters);
auto allVioRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.1<=pK<=0.3,0.2<=TOMsg<=0.3", modelParameters);
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, regionChecker.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, regionChecker.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, regionChecker.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
TEST(SparseMdpParameterLiftingTest, brp_Rew_bounded) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/brp16_2.nm";
std::string formulaAsString = "R>2.5 [ C<=300 ]";
std::string constantsAsString = "pL=0.9,TOAck=0.5";
storm::prism::Program program = storm::api::parseProgram(programFile);
program = storm::utility::prism::preprocess(program, constantsAsString);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
storm::modelchecker::parametric::SparseMdpRegionChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double, storm::RationalNumber> regionChecker(*model);
regionChecker.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
//start testing
auto allSatRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.7<=pK<=0.875,0.75<=TOMsg<=0.95", modelParameters);
auto exBothRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters);
auto allVioRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.1<=pK<=0.3,0.2<=TOMsg<=0.3", modelParameters);
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, regionChecker.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, regionChecker.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, regionChecker.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
TEST(SparseMdpParameterLiftingTest, Brp_Rew_Infty) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/brp16_2.nm";
std::string formulaAsString = "R>2.5 [F (s=0&srep=3) ]";
std::string constantsAsString = "";
carl::VariablePool::getInstance().clear();
storm::prism::Program program = storm::api::parseProgram(programFile);
program = storm::utility::prism::preprocess(program, constantsAsString);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
storm::modelchecker::parametric::SparseMdpRegionChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double, storm::RationalNumber> regionChecker(*model);
regionChecker.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
//start testing
auto allSatRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.7<=pK<=0.9,0.6<=pL<=0.85,0.9<=TOMsg<=0.95,0.85<=TOAck<=0.9", modelParameters);
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, regionChecker.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
TEST(SparseMdpParameterLiftingTest, Brp_Rew_4Par) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/brp16_2.nm";
std::string formulaAsString = "R>2.5 [F ((s=5) | (s=0&srep=3)) ]";
std::string constantsAsString = ""; //!! this model will have 4 parameters
carl::VariablePool::getInstance().clear();
storm::prism::Program program = storm::api::parseProgram(programFile);
program = storm::utility::prism::preprocess(program, constantsAsString);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
storm::modelchecker::parametric::SparseMdpRegionChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double, storm::RationalNumber> regionChecker(*model);
regionChecker.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
//start testing
auto allSatRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.7<=pK<=0.9,0.6<=pL<=0.85,0.9<=TOMsg<=0.95,0.85<=TOAck<=0.9", modelParameters);
auto exBothRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.1<=pK<=0.7,0.2<=pL<=0.8,0.15<=TOMsg<=0.65,0.3<=TOAck<=0.9", modelParameters);
auto allVioRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.1<=pK<=0.4,0.2<=pL<=0.3,0.15<=TOMsg<=0.3,0.1<=TOAck<=0.2", modelParameters);
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, regionChecker.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, regionChecker.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, regionChecker.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
#endif

23
src/test/storm-pars/CMakeLists.txt
View File

@ -0,0 +1,23 @@
# Base path for test files
set(STORM_TESTS_BASE_PATH "${PROJECT_SOURCE_DIR}/src/test/storm-pars")
# Test Sources
file(GLOB_RECURSE ALL_FILES ${STORM_TESTS_BASE_PATH}/*.h ${STORM_TESTS_BASE_PATH}/*.cpp)
register_source_groups_from_filestructure("${ALL_FILES}" test)
# Note that the tests also need the source files, except for the main file
include_directories(${GTEST_INCLUDE_DIR})
foreach (testsuite modelchecker)
file(GLOB_RECURSE TEST_${testsuite}_FILES ${STORM_TESTS_BASE_PATH}/${testsuite}/*.h ${STORM_TESTS_BASE_PATH}/${testsuite}/*.cpp)
add_executable (test-pars-${testsuite} ${TEST_${testsuite}_FILES} ${STORM_TESTS_BASE_PATH}/storm-test.cpp)
target_link_libraries(test-pars-${testsuite} storm-pars)
target_link_libraries(test-pars-${testsuite} ${STORM_TEST_LINK_LIBRARIES})
add_dependencies(test-pars-${testsuite} test-resources)
add_test(NAME run-test-pars-${testsuite} COMMAND $<TARGET_FILE:test-pars-${testsuite}>)
add_dependencies(tests test-pars-${testsuite})
endforeach ()

362
src/test/storm-pars/modelchecker/SparseDtmcParameterLiftingTest.cpp
View File

@ -0,0 +1,362 @@
#include "gtest/gtest.h"
#include "storm-config.h"
#ifdef STORM_HAVE_CARL
#include "storm/adapters/RationalFunctionAdapter.h"
#include "storm-pars/api/storm-pars.h"
#include "storm/api/storm.h"
TEST(SparseDtmcParameterLiftingTest, Brp_Prob) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm";
std::string formulaAsString = "P<=0.84 [F s=5 ]";
std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5
// Program and formula
storm::prism::Program program = storm::api::parseProgram(programFile);
program = storm::utility::prism::preprocess(program, constantsAsString);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker<storm::RationalFunction, double>(model, storm::api::createTask<storm::RationalFunction>(formulas[0], true));
//start testing
auto allSatRegion=storm::api::parseRegion<storm::RationalFunction>("0.7<=pL<=0.9,0.75<=pK<=0.95", modelParameters);
auto exBothRegion=storm::api::parseRegion<storm::RationalFunction>("0.4<=pL<=0.65,0.75<=pK<=0.95", modelParameters);
auto allVioRegion=storm::api::parseRegion<storm::RationalFunction>("0.1<=pL<=0.73,0.2<=pK<=0.715", modelParameters);
EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
TEST(SparseDtmcParameterLiftingTest, Brp_Rew) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp_rewards16_2.pm";
std::string formulaAsString = "R>2.5 [F ((s=5) | (s=0&srep=3)) ]";
std::string constantsAsString = "pL=0.9,TOAck=0.5";
carl::VariablePool::getInstance().clear();
storm::prism::Program program = storm::api::parseProgram(programFile);
program = storm::utility::prism::preprocess(program, constantsAsString);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker<storm::RationalFunction, double>(model, storm::api::createTask<storm::RationalFunction>(formulas[0], true));
//start testing
auto allSatRegion=storm::api::parseRegion<storm::RationalFunction>("0.7<=pK<=0.875,0.75<=TOMsg<=0.95", modelParameters);
auto exBothRegion=storm::api::parseRegion<storm::RationalFunction>("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters);
auto allVioRegion=storm::api::parseRegion<storm::RationalFunction>("0.1<=pK<=0.3,0.2<=TOMsg<=0.3", modelParameters);
EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
TEST(SparseDtmcParameterLiftingTest, Brp_Rew_Bounded) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp_rewards16_2.pm";
std::string formulaAsString = "R>2.5 [ C<=300]";
std::string constantsAsString = "pL=0.9,TOAck=0.5";
carl::VariablePool::getInstance().clear();
storm::prism::Program program = storm::api::parseProgram(programFile);
program = storm::utility::prism::preprocess(program, constantsAsString);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker<storm::RationalFunction, double>(model, storm::api::createTask<storm::RationalFunction>(formulas[0], true));
//start testing
auto allSatRegion=storm::api::parseRegion<storm::RationalFunction>("0.7<=pK<=0.875,0.75<=TOMsg<=0.95", modelParameters);
auto exBothRegion=storm::api::parseRegion<storm::RationalFunction>("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters);
auto allVioRegion=storm::api::parseRegion<storm::RationalFunction>("0.1<=pK<=0.3,0.2<=TOMsg<=0.3", modelParameters);
EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
TEST(SparseDtmcParameterLiftingTest, Brp_Prob_exactValidation) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm";
std::string formulaAsString = "P<=0.84 [F s=5 ]";
std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5
// Program and formula
storm::prism::Program program = storm::api::parseProgram(programFile);
program = storm::utility::prism::preprocess(program, constantsAsString);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
auto regionChecker = storm::api::initializeValidatingRegionModelChecker<storm::RationalFunction, double, storm::RationalNumber>(model, storm::api::createTask<storm::RationalFunction>(formulas[0], true));
auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
//start testing
auto allSatRegion=storm::api::parseRegion<storm::RationalFunction>("0.7<=pL<=0.9,0.75<=pK<=0.95", modelParameters);
auto exBothRegion=storm::api::parseRegion<storm::RationalFunction>("0.4<=pL<=0.65,0.75<=pK<=0.95", modelParameters);
auto allVioRegion=storm::api::parseRegion<storm::RationalFunction>("0.1<=pL<=0.73,0.2<=pK<=0.715", modelParameters);
EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
TEST(SparseDtmcParameterLiftingTest, Brp_Rew_exactValidation) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp_rewards16_2.pm";
std::string formulaAsString = "R>2.5 [F ((s=5) | (s=0&srep=3)) ]";
std::string constantsAsString = "pL=0.9,TOAck=0.5";
carl::VariablePool::getInstance().clear();
storm::prism::Program program = storm::api::parseProgram(programFile);
program = storm::utility::prism::preprocess(program, constantsAsString);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
auto regionChecker = storm::api::initializeValidatingRegionModelChecker<storm::RationalFunction, double, storm::RationalNumber>(model, storm::api::createTask<storm::RationalFunction>(formulas[0], true));
//start testing
auto allSatRegion=storm::api::parseRegion<storm::RationalFunction>("0.7<=pK<=0.875,0.75<=TOMsg<=0.95", modelParameters);
auto exBothRegion=storm::api::parseRegion<storm::RationalFunction>("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters);
auto allVioRegion=storm::api::parseRegion<storm::RationalFunction>("0.1<=pK<=0.3,0.2<=TOMsg<=0.3", modelParameters);
EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
TEST(SparseDtmcParameterLiftingTest, Brp_Rew_Bounded_exactValidation) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp_rewards16_2.pm";
std::string formulaAsString = "R>2.5 [ C<=300]";
std::string constantsAsString = "pL=0.9,TOAck=0.5";
carl::VariablePool::getInstance().clear();
storm::prism::Program program = storm::api::parseProgram(programFile);
program = storm::utility::prism::preprocess(program, constantsAsString);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
auto regionChecker = storm::api::initializeValidatingRegionModelChecker<storm::RationalFunction, double, storm::RationalNumber>(model, storm::api::createTask<storm::RationalFunction>(formulas[0], true));
//start testing
auto allSatRegion=storm::api::parseRegion<storm::RationalFunction>("0.7<=pK<=0.875,0.75<=TOMsg<=0.95", modelParameters);
auto exBothRegion=storm::api::parseRegion<storm::RationalFunction>("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters);
auto allVioRegion=storm::api::parseRegion<storm::RationalFunction>("0.1<=pK<=0.3,0.2<=TOMsg<=0.3", modelParameters);
EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
TEST(SparseDtmcParameterLiftingTest, Brp_Rew_Infty) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp_rewards16_2.pm";
std::string formulaAsString = "R>2.5 [F (s=0&srep=3) ]";
std::string constantsAsString = "";
carl::VariablePool::getInstance().clear();
storm::prism::Program program = storm::api::parseProgram(programFile);
program = storm::utility::prism::preprocess(program, constantsAsString);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker<storm::RationalFunction, double>(model, storm::api::createTask<storm::RationalFunction>(formulas[0], true));
//start testing
auto allSatRegion=storm::api::parseRegion<storm::RationalFunction>("0.7<=pK<=0.9,0.6<=pL<=0.85,0.9<=TOMsg<=0.95,0.85<=TOAck<=0.9", modelParameters);
EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
TEST(SparseDtmcParameterLiftingTest, Brp_Rew_4Par) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp_rewards16_2.pm";
std::string formulaAsString = "R>2.5 [F ((s=5) | (s=0&srep=3)) ]";
std::string constantsAsString = ""; //!! this model will have 4 parameters
carl::VariablePool::getInstance().clear();
storm::prism::Program program = storm::api::parseProgram(programFile);
program = storm::utility::prism::preprocess(program, constantsAsString);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker<storm::RationalFunction, double>(model, storm::api::createTask<storm::RationalFunction>(formulas[0], true));
//start testing
auto allSatRegion=storm::api::parseRegion<storm::RationalFunction>("0.7<=pK<=0.9,0.6<=pL<=0.85,0.9<=TOMsg<=0.95,0.85<=TOAck<=0.9", modelParameters);
auto exBothRegion=storm::api::parseRegion<storm::RationalFunction>("0.1<=pK<=0.7,0.2<=pL<=0.8,0.15<=TOMsg<=0.65,0.3<=TOAck<=0.9", modelParameters);
auto allVioRegion=storm::api::parseRegion<storm::RationalFunction>("0.1<=pK<=0.4,0.2<=pL<=0.3,0.15<=TOMsg<=0.3,0.1<=TOAck<=0.2", modelParameters);
EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
TEST(SparseDtmcParameterLiftingTest, Crowds_Prob) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/crowds3_5.pm";
std::string formulaAsString = "P<0.5 [F \"observe0Greater1\" ]";
std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5
carl::VariablePool::getInstance().clear();
storm::prism::Program program = storm::api::parseProgram(programFile);
program = storm::utility::prism::preprocess(program, constantsAsString);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker<storm::RationalFunction, double>(model, storm::api::createTask<storm::RationalFunction>(formulas[0], true));
//start testing
auto allSatRegion=storm::api::parseRegion<storm::RationalFunction>("0.1<=PF<=0.75,0.15<=badC<=0.2", modelParameters);
auto exBothRegion=storm::api::parseRegion<storm::RationalFunction>("0.75<=PF<=0.8,0.2<=badC<=0.3", modelParameters);
auto allVioRegion=storm::api::parseRegion<storm::RationalFunction>("0.8<=PF<=0.95,0.2<=badC<=0.2", modelParameters);
auto allVioHardRegion=storm::api::parseRegion<storm::RationalFunction>("0.8<=PF<=0.95,0.2<=badC<=0.9", modelParameters);
EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::RegionResult::CenterViolated, regionChecker->analyzeRegion(allVioHardRegion, storm::modelchecker::RegionResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
TEST(SparseDtmcParameterLiftingTest, Crowds_Prob_stepBounded) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/crowds3_5.pm";
std::string formulaAsString = "P<0.5 [F<=300 \"observe0Greater1\" ]";
std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5
carl::VariablePool::getInstance().clear();
storm::prism::Program program = storm::api::parseProgram(programFile);
program = storm::utility::prism::preprocess(program, constantsAsString);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker<storm::RationalFunction, double>(model, storm::api::createTask<storm::RationalFunction>(formulas[0], true));
//start testing
auto allSatRegion=storm::api::parseRegion<storm::RationalFunction>("0.1<=PF<=0.75,0.15<=badC<=0.2", modelParameters);
auto exBothRegion=storm::api::parseRegion<storm::RationalFunction>("0.75<=PF<=0.8,0.2<=badC<=0.3", modelParameters);
auto allVioRegion=storm::api::parseRegion<storm::RationalFunction>("0.8<=PF<=0.95,0.2<=badC<=0.2", modelParameters);
auto allVioHardRegion=storm::api::parseRegion<storm::RationalFunction>("0.8<=PF<=0.95,0.2<=badC<=0.9", modelParameters);
EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::RegionResult::CenterViolated, regionChecker->analyzeRegion(allVioHardRegion, storm::modelchecker::RegionResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
TEST(SparseDtmcParameterLiftingTest, Crowds_Prob_1Par) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/crowds3_5.pm";
std::string formulaAsString = "P>0.75 [F \"observe0Greater1\" ]";
std::string constantsAsString = "badC=0.3"; //e.g. pL=0.9,TOACK=0.5
carl::VariablePool::getInstance().clear();
storm::prism::Program program = storm::api::parseProgram(programFile);
program = storm::utility::prism::preprocess(program, constantsAsString);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker<storm::RationalFunction, double>(model, storm::api::createTask<storm::RationalFunction>(formulas[0], true));
//start testing
auto allSatRegion=storm::api::parseRegion<storm::RationalFunction>("0.9<=PF<=0.99", modelParameters);
auto exBothRegion=storm::api::parseRegion<storm::RationalFunction>("0.8<=PF<=0.9", modelParameters);
auto allVioRegion=storm::api::parseRegion<storm::RationalFunction>("0.01<=PF<=0.8", modelParameters);
EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
TEST(SparseDtmcParameterLiftingTest, Crowds_Prob_Const) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/crowds3_5.pm";
std::string formulaAsString = "P>0.6 [F \"observe0Greater1\" ]";
std::string constantsAsString = "PF=0.9,badC=0.2";
carl::VariablePool::getInstance().clear();
storm::prism::Program program = storm::api::parseProgram(programFile);
program = storm::utility::prism::preprocess(program, constantsAsString);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker<storm::RationalFunction, double>(model, storm::api::createTask<storm::RationalFunction>(formulas[0], true));
//start testing
auto allSatRegion=storm::api::parseRegion<storm::RationalFunction>("", modelParameters);
EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
#endif

301
src/test/storm-pars/modelchecker/SparseMdpParameterLiftingTest.cpp
View File

@ -0,0 +1,301 @@
#include "gtest/gtest.h"
#include "storm-config.h"
#ifdef STORM_HAVE_CARL
#include "storm/adapters/RationalFunctionAdapter.h"
#include "storm-pars/api/storm-pars.h"
#include "storm/api/storm.h"
TEST(SparseMdpParameterLiftingTest, two_dice_Prob) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/two_dice.nm";
std::string formulaFile = "P<=0.17 [ F \"doubles\" ]";
carl::VariablePool::getInstance().clear();
storm::prism::Program program = storm::api::parseProgram(programFile);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaFile, program));
std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker<storm::RationalFunction, double>(model, storm::api::createTask<storm::RationalFunction>(formulas[0], true));
auto allSatRegion = storm::api::parseRegion<storm::RationalFunction>("0.495<=p1<=0.5,0.5<=p2<=0.505", modelParameters);
auto exBothRegion = storm::api::parseRegion<storm::RationalFunction>("0.45<=p1<=0.55,0.45<=p2<=0.55", modelParameters);
auto allVioRegion = storm::api::parseRegion<storm::RationalFunction>("0.6<=p1<=0.7,0.6<=p2<=0.6", modelParameters);
EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
TEST(SparseMdpParameterLiftingTest, two_dice_Prob_bounded) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/two_dice.nm";
std::string formulaFile = "P<=0.17 [ F<100 \"doubles\" ]";
carl::VariablePool::getInstance().clear();
storm::prism::Program program = storm::api::parseProgram(programFile);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaFile, program));
std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker<storm::RationalFunction, double>(model, storm::api::createTask<storm::RationalFunction>(formulas[0], true));
auto allSatRegion = storm::api::parseRegion<storm::RationalFunction>("0.495<=p1<=0.5,0.5<=p2<=0.505", modelParameters);
auto exBothRegion = storm::api::parseRegion<storm::RationalFunction>("0.45<=p1<=0.55,0.45<=p2<=0.55", modelParameters);
auto allVioRegion = storm::api::parseRegion<storm::RationalFunction>("0.6<=p1<=0.7,0.6<=p2<=0.6", modelParameters);
EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
TEST(SparseMdpParameterLiftingTest, two_dice_Prob_exactValidation) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/two_dice.nm";
std::string formulaFile = "P<=0.17 [ F \"doubles\" ]";
carl::VariablePool::getInstance().clear();
storm::prism::Program program = storm::api::parseProgram(programFile);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaFile, program));
std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
auto regionChecker = storm::api::initializeValidatingRegionModelChecker<storm::RationalFunction, double, storm::RationalNumber>(model, storm::api::createTask<storm::RationalFunction>(formulas[0], true));
auto allSatRegion = storm::api::parseRegion<storm::RationalFunction>("0.495<=p1<=0.5,0.5<=p2<=0.505", modelParameters);
auto exBothRegion = storm::api::parseRegion<storm::RationalFunction>("0.45<=p1<=0.55,0.45<=p2<=0.55", modelParameters);
auto allVioRegion = storm::api::parseRegion<storm::RationalFunction>("0.6<=p1<=0.7,0.6<=p2<=0.6", modelParameters);
EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
TEST(SparseMdpParameterLiftingTest, two_dice_Prob_bounded_exactValidation) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/two_dice.nm";
std::string formulaFile = "P<=0.17 [ F<100 \"doubles\" ]";
carl::VariablePool::getInstance().clear();
storm::prism::Program program = storm::api::parseProgram(programFile);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaFile, program));
std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
auto regionChecker = storm::api::initializeValidatingRegionModelChecker<storm::RationalFunction, double, storm::RationalNumber>(model, storm::api::createTask<storm::RationalFunction>(formulas[0], true));
auto allSatRegion = storm::api::parseRegion<storm::RationalFunction>("0.495<=p1<=0.5,0.5<=p2<=0.505", modelParameters);
auto exBothRegion = storm::api::parseRegion<storm::RationalFunction>("0.45<=p1<=0.55,0.45<=p2<=0.55", modelParameters);
auto allVioRegion = storm::api::parseRegion<storm::RationalFunction>("0.6<=p1<=0.7,0.6<=p2<=0.6", modelParameters);
EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
TEST(SparseMdpParameterLiftingTest, coin_Prob) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/coin2_2.nm";
std::string formulaAsString = "P>0.25 [F \"finished\"&\"all_coins_equal_1\" ]";
storm::prism::Program program = storm::api::parseProgram(programFile);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker<storm::RationalFunction, double>(model, storm::api::createTask<storm::RationalFunction>(formulas[0], true));
//start testing
auto allSatRegion = storm::api::parseRegion<storm::RationalFunction>("0.3<=p1<=0.45,0.2<=p2<=0.54", modelParameters);
auto exBothRegion = storm::api::parseRegion<storm::RationalFunction>("0.4<=p1<=0.65,0.5<=p2<=0.7", modelParameters);
auto allVioRegion = storm::api::parseRegion<storm::RationalFunction>("0.4<=p1<=0.7,0.55<=p2<=0.6", modelParameters);
EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
TEST(SparseMdpParameterLiftingTest, brp_Prop) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/brp16_2.nm";
std::string formulaAsString = "P<=0.84 [ F (s=5 & T) ]";
std::string constantsAsString = "TOMsg=0.0,TOAck=0.0";
storm::prism::Program program = storm::api::parseProgram(programFile);
program = storm::utility::prism::preprocess(program, constantsAsString);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker<storm::RationalFunction, double>(model, storm::api::createTask<storm::RationalFunction>(formulas[0], true));
//start testing
auto allSatRegion=storm::api::parseRegion<storm::RationalFunction>("0.7<=pL<=0.9,0.75<=pK<=0.95", modelParameters);
auto exBothRegion=storm::api::parseRegion<storm::RationalFunction>("0.4<=pL<=0.65,0.75<=pK<=0.95", modelParameters);
auto allVioRegion=storm::api::parseRegion<storm::RationalFunction>("0.1<=pL<=0.73,0.2<=pK<=0.715", modelParameters);
EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
TEST(SparseMdpParameterLiftingTest, brp_Rew) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/brp16_2.nm";
std::string formulaAsString = "R>2.5 [F ((s=5) | (s=0&srep=3)) ]";
std::string constantsAsString = "pL=0.9,TOAck=0.5";
storm::prism::Program program = storm::api::parseProgram(programFile);
program = storm::utility::prism::preprocess(program, constantsAsString);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker<storm::RationalFunction, double>(model, storm::api::createTask<storm::RationalFunction>(formulas[0], true));
//start testing
auto allSatRegion=storm::api::parseRegion<storm::RationalFunction>("0.7<=pK<=0.875,0.75<=TOMsg<=0.95", modelParameters);
auto exBothRegion=storm::api::parseRegion<storm::RationalFunction>("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters);
auto allVioRegion=storm::api::parseRegion<storm::RationalFunction>("0.1<=pK<=0.3,0.2<=TOMsg<=0.3", modelParameters);
EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
TEST(SparseMdpParameterLiftingTest, brp_Rew_bounded) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/brp16_2.nm";
std::string formulaAsString = "R>2.5 [ C<=300 ]";
std::string constantsAsString = "pL=0.9,TOAck=0.5";
storm::prism::Program program = storm::api::parseProgram(programFile);
program = storm::utility::prism::preprocess(program, constantsAsString);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker<storm::RationalFunction, double>(model, storm::api::createTask<storm::RationalFunction>(formulas[0], true));
//start testing
auto allSatRegion=storm::api::parseRegion<storm::RationalFunction>("0.7<=pK<=0.875,0.75<=TOMsg<=0.95", modelParameters);
auto exBothRegion=storm::api::parseRegion<storm::RationalFunction>("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters);
auto allVioRegion=storm::api::parseRegion<storm::RationalFunction>("0.1<=pK<=0.3,0.2<=TOMsg<=0.3", modelParameters);
EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
TEST(SparseMdpParameterLiftingTest, Brp_Rew_Infty) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/brp16_2.nm";
std::string formulaAsString = "R>2.5 [F (s=0&srep=3) ]";
std::string constantsAsString = "";
carl::VariablePool::getInstance().clear();
storm::prism::Program program = storm::api::parseProgram(programFile);
program = storm::utility::prism::preprocess(program, constantsAsString);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker<storm::RationalFunction, double>(model, storm::api::createTask<storm::RationalFunction>(formulas[0], true));
//start testing
auto allSatRegion=storm::api::parseRegion<storm::RationalFunction>("0.7<=pK<=0.9,0.6<=pL<=0.85,0.9<=TOMsg<=0.95,0.85<=TOAck<=0.9", modelParameters);
EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
TEST(SparseMdpParameterLiftingTest, Brp_Rew_4Par) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/brp16_2.nm";
std::string formulaAsString = "R>2.5 [F ((s=5) | (s=0&srep=3)) ]";
std::string constantsAsString = ""; //!! this model will have 4 parameters
carl::VariablePool::getInstance().clear();
storm::prism::Program program = storm::api::parseProgram(programFile);
program = storm::utility::prism::preprocess(program, constantsAsString);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
auto rewParameters = storm::models::sparse::getRewardParameters(*model);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker<storm::RationalFunction, double>(model, storm::api::createTask<storm::RationalFunction>(formulas[0], true));
//start testing
auto allSatRegion=storm::api::parseRegion<storm::RationalFunction>("0.7<=pK<=0.9,0.6<=pL<=0.85,0.9<=TOMsg<=0.95,0.85<=TOAck<=0.9", modelParameters);
auto exBothRegion=storm::api::parseRegion<storm::RationalFunction>("0.1<=pK<=0.7,0.2<=pL<=0.8,0.15<=TOMsg<=0.65,0.3<=TOAck<=0.9", modelParameters);
auto allVioRegion=storm::api::parseRegion<storm::RationalFunction>("0.1<=pK<=0.4,0.2<=pL<=0.3,0.15<=TOMsg<=0.3,0.1<=TOAck<=0.2", modelParameters);
EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
#endif

8
src/test/storm-pars/storm-test.cpp
View File

@ -0,0 +1,8 @@
#include "gtest/gtest.h"
#include "storm/settings/SettingsManager.h"
int main(int argc, char **argv) {
storm::settings::initializeAll("Storm-pars (Functional) Testing Suite", "test-pars");
::testing::InitGoogleTest(&argc, argv);
return RUN_ALL_TESTS();
}

23
src/test/storm/CMakeLists.txt
View File

@ -0,0 +1,23 @@
# Base path for test files
set(STORM_TESTS_BASE_PATH "${PROJECT_SOURCE_DIR}/src/test/storm")
# Test Sources
file(GLOB_RECURSE ALL_FILES ${STORM_TESTS_BASE_PATH}/*.h ${STORM_TESTS_BASE_PATH}/*.cpp)
register_source_groups_from_filestructure("${ALL_FILES}" test)
# Note that the tests also need the source files, except for the main file
include_directories(${GTEST_INCLUDE_DIR})
foreach (testsuite abstraction adapter builder logic modelchecker parser permissiveschedulers solver storage transformer utility)
file(GLOB_RECURSE TEST_${testsuite}_FILES ${STORM_TESTS_BASE_PATH}/${testsuite}/*.h ${STORM_TESTS_BASE_PATH}/${testsuite}/*.cpp)
add_executable (test-${testsuite} ${TEST_${testsuite}_FILES} ${STORM_TESTS_BASE_PATH}/storm-test.cpp)
target_link_libraries(test-${testsuite} storm)
target_link_libraries(test-${testsuite} ${STORM_TEST_LINK_LIBRARIES})
add_dependencies(test-${testsuite} test-resources)
add_test(NAME run-test-${testsuite} COMMAND $<TARGET_FILE:test-${testsuite}>)
add_dependencies(tests test-${testsuite})
endforeach ()

0
src/test/abstraction/PrismMenuGameTest.cpp → src/test/storm/abstraction/PrismMenuGameTest.cpp
View File

0
src/test/adapter/MathsatExpressionAdapterTest.cpp → src/test/storm/adapter/MathsatExpressionAdapterTest.cpp
View File

0
src/test/adapter/Z3ExpressionAdapterTest.cpp → src/test/storm/adapter/Z3ExpressionAdapterTest.cpp
View File

0
src/test/builder/DdJaniModelBuilderTest.cpp → src/test/storm/builder/DdJaniModelBuilderTest.cpp
View File

0
src/test/builder/DdPrismModelBuilderTest.cpp → src/test/storm/builder/DdPrismModelBuilderTest.cpp
View File

0
src/test/builder/ExplicitJaniModelBuilderTest.cpp → src/test/storm/builder/ExplicitJaniModelBuilderTest.cpp
View File

0
src/test/builder/ExplicitJitJaniModelBuilderTest.cpp → src/test/storm/builder/ExplicitJitJaniModelBuilderTest.cpp
View File

0
src/test/builder/ExplicitPrismModelBuilderTest.cpp → src/test/storm/builder/ExplicitPrismModelBuilderTest.cpp
View File

0
src/test/logic/FragmentCheckerTest.cpp → src/test/storm/logic/FragmentCheckerTest.cpp
View File

0
src/test/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp → src/test/storm/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp
View File

0
src/test/modelchecker/GameBasedDtmcModelCheckerTest.cpp → src/test/storm/modelchecker/GameBasedDtmcModelCheckerTest.cpp
View File

0
src/test/modelchecker/GameBasedMdpModelCheckerTest.cpp → src/test/storm/modelchecker/GameBasedMdpModelCheckerTest.cpp
View File

0
src/test/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp → src/test/storm/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp
View File

0
src/test/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp → src/test/storm/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp
View File

0
src/test/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp → src/test/storm/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp
View File

0
src/test/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp → src/test/storm/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp
View File

0
src/test/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp → src/test/storm/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp
View File

0
src/test/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp → src/test/storm/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
View File

0
src/test/modelchecker/NativeCtmcCslModelCheckerTest.cpp → src/test/storm/modelchecker/NativeCtmcCslModelCheckerTest.cpp
View File

0
src/test/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp → src/test/storm/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp
View File

0
src/test/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp → src/test/storm/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp
View File

0
src/test/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp → src/test/storm/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp
View File

0
src/test/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp → src/test/storm/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp
View File

0
src/test/modelchecker/NativeMdpPrctlModelCheckerTest.cpp → src/test/storm/modelchecker/NativeMdpPrctlModelCheckerTest.cpp
View File

0
src/test/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp → src/test/storm/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp
View File

0
src/test/modelchecker/SparseExplorationModelCheckerTest.cpp → src/test/storm/modelchecker/SparseExplorationModelCheckerTest.cpp
View File

0
src/test/modelchecker/SparseMaCbMultiObjectiveModelCheckerTest.cpp → src/test/storm/modelchecker/SparseMaCbMultiObjectiveModelCheckerTest.cpp
View File

0
src/test/modelchecker/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp → src/test/storm/modelchecker/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp
View File

0
src/test/modelchecker/SparseMdpCbMultiObjectiveModelCheckerTest.cpp → src/test/storm/modelchecker/SparseMdpCbMultiObjectiveModelCheckerTest.cpp
View File

0
src/test/modelchecker/SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp → src/test/storm/modelchecker/SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp
View File

0
src/test/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp → src/test/storm/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp
View File

0
src/test/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp → src/test/storm/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp
View File

0
src/test/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp → src/test/storm/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp
View File

0
src/test/parser/.gitignore → src/test/storm/parser/.gitignore
View File

0
src/test/parser/AutoParserTest.cpp → src/test/storm/parser/AutoParserTest.cpp
View File

0
src/test/parser/DeterministicModelParserTest.cpp → src/test/storm/parser/DeterministicModelParserTest.cpp
View File

0
src/test/parser/DeterministicSparseTransitionParserTest.cpp → src/test/storm/parser/DeterministicSparseTransitionParserTest.cpp
View File

0
src/test/parser/DirectEncodingParserTest.cpp → src/test/storm/parser/DirectEncodingParserTest.cpp
View File

0
src/test/parser/FormulaParserTest.cpp → src/test/storm/parser/FormulaParserTest.cpp
View File

0
src/test/parser/MappedFileTest.cpp → src/test/storm/parser/MappedFileTest.cpp
View File

0
src/test/parser/MarkovAutomatonParserTest.cpp → src/test/storm/parser/MarkovAutomatonParserTest.cpp
View File

0
src/test/parser/MarkovAutomatonSparseTransitionParserTest.cpp → src/test/storm/parser/MarkovAutomatonSparseTransitionParserTest.cpp
View File

0
src/test/parser/NondeterministicModelParserTest.cpp → src/test/storm/parser/NondeterministicModelParserTest.cpp
View File

0
src/test/parser/NondeterministicSparseTransitionParserTest.cpp → src/test/storm/parser/NondeterministicSparseTransitionParserTest.cpp
View File

0
src/test/parser/PrismParserTest.cpp → src/test/storm/parser/PrismParserTest.cpp
View File

0
src/test/parser/SparseItemLabelingParserTest.cpp → src/test/storm/parser/SparseItemLabelingParserTest.cpp
View File

0
src/test/parser/SparseStateRewardParserTest.cpp → src/test/storm/parser/SparseStateRewardParserTest.cpp
View File

0
src/test/permissiveschedulers/MilpPermissiveSchedulerTest.cpp → src/test/storm/permissiveschedulers/MilpPermissiveSchedulerTest.cpp
View File

0
src/test/permissiveschedulers/SmtPermissiveSchedulerTest.cpp → src/test/storm/permissiveschedulers/SmtPermissiveSchedulerTest.cpp
View File

0
src/test/solver/CudaPluginTest.cpp → src/test/storm/solver/CudaPluginTest.cpp
View File

0
src/test/solver/EigenLinearEquationSolverTest.cpp → src/test/storm/solver/EigenLinearEquationSolverTest.cpp
View File

0
src/test/solver/EliminationLinearEquationSolverTest.cpp → src/test/storm/solver/EliminationLinearEquationSolverTest.cpp
View File

0
src/test/solver/FullySymbolicGameSolverTest.cpp → src/test/storm/solver/FullySymbolicGameSolverTest.cpp
View File

0
src/test/solver/GameSolverTest.cpp → src/test/storm/solver/GameSolverTest.cpp
View File

0
src/test/solver/GlpkLpSolverTest.cpp → src/test/storm/solver/GlpkLpSolverTest.cpp
View File

0
src/test/solver/GmmxxLinearEquationSolverTest.cpp → src/test/storm/solver/GmmxxLinearEquationSolverTest.cpp
View File

0
src/test/solver/GmmxxMinMaxLinearEquationSolverTest.cpp → src/test/storm/solver/GmmxxMinMaxLinearEquationSolverTest.cpp
View File

0
src/test/solver/GurobiLpSolverTest.cpp → src/test/storm/solver/GurobiLpSolverTest.cpp
View File

0
src/test/solver/MathsatSmtSolverTest.cpp → src/test/storm/solver/MathsatSmtSolverTest.cpp
View File

0
src/test/solver/MinMaxTechniqueSelectionTest.cpp → src/test/storm/solver/MinMaxTechniqueSelectionTest.cpp
View File

0
src/test/solver/NativeLinearEquationSolverTest.cpp → src/test/storm/solver/NativeLinearEquationSolverTest.cpp
View File

0
src/test/solver/NativeMinMaxLinearEquationSolverTest.cpp → src/test/storm/solver/NativeMinMaxLinearEquationSolverTest.cpp
View File

0
src/test/solver/Z3LpSolverTest.cpp → src/test/storm/solver/Z3LpSolverTest.cpp
View File

0
src/test/solver/Z3SmtSolverTest.cpp → src/test/storm/solver/Z3SmtSolverTest.cpp
View File

0
src/test/storage/BitVectorHashMapTest.cpp → src/test/storm/storage/BitVectorHashMapTest.cpp
View File

0
src/test/storage/BitVectorTest.cpp → src/test/storm/storage/BitVectorTest.cpp
View File

0
src/test/storage/CuddDdTest.cpp → src/test/storm/storage/CuddDdTest.cpp
View File

0
src/test/storage/DeterministicModelBisimulationDecompositionTest.cpp → src/test/storm/storage/DeterministicModelBisimulationDecompositionTest.cpp
View File

0
src/test/storage/ExpressionEvalutionTest.cpp → src/test/storm/storage/ExpressionEvalutionTest.cpp
View File

0
src/test/storage/ExpressionTest.cpp → src/test/storm/storage/ExpressionTest.cpp
View File

0
src/test/storage/JaniModelTest.cpp → src/test/storm/storage/JaniModelTest.cpp
View File

0
src/test/storage/MaximalEndComponentDecompositionTest.cpp → src/test/storm/storage/MaximalEndComponentDecompositionTest.cpp
View File

0
src/test/storage/NondeterministicModelBisimulationDecompositionTest.cpp → src/test/storm/storage/NondeterministicModelBisimulationDecompositionTest.cpp
View File

0
src/test/storage/PrismProgramTest.cpp → src/test/storm/storage/PrismProgramTest.cpp
View File

0
src/test/storage/SchedulerTest.cpp → src/test/storm/storage/SchedulerTest.cpp
View File

0
src/test/storage/SparseMatrixTest.cpp → src/test/storm/storage/SparseMatrixTest.cpp
View File

0
src/test/storage/StronglyConnectedComponentDecompositionTest.cpp → src/test/storm/storage/StronglyConnectedComponentDecompositionTest.cpp
View File

0
src/test/storage/SylvanDdTest.cpp → src/test/storm/storage/SylvanDdTest.cpp
View File

0
src/test/storm-test.cpp → src/test/storm/storm-test.cpp
View File

0
src/test/transformer/EndComponentEliminatorTest.cpp → src/test/storm/transformer/EndComponentEliminatorTest.cpp
View File

0
src/test/utility/GraphTest.cpp → src/test/storm/utility/GraphTest.cpp
View File

0
src/test/utility/KSPTest.cpp → src/test/storm/utility/KSPTest.cpp
View File

0
src/test/utility/ModelInstantiatorTest.cpp → src/test/storm/utility/ModelInstantiatorTest.cpp
View File

0
src/test/utility/VectorTest.cpp → src/test/storm/utility/VectorTest.cpp
View File

Write Preview
Loading…
Cancel
Save