|
@ -19,7 +19,7 @@ |
|
|
#include "storm/adapters/CarlAdapter.h"
|
|
|
#include "storm/adapters/CarlAdapter.h"
|
|
|
|
|
|
|
|
|
TEST(PrismMenuGame, DieAbstractionTest_Cudd) { |
|
|
TEST(PrismMenuGame, DieAbstractionTest_Cudd) { |
|
|
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/die.pm"); |
|
|
|
|
|
|
|
|
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm"); |
|
|
|
|
|
|
|
|
std::vector<storm::expressions::Expression> initialPredicates; |
|
|
std::vector<storm::expressions::Expression> initialPredicates; |
|
|
storm::expressions::ExpressionManager& manager = program.getManager(); |
|
|
storm::expressions::ExpressionManager& manager = program.getManager(); |
|
@ -36,7 +36,7 @@ TEST(PrismMenuGame, DieAbstractionTest_Cudd) { |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
TEST(PrismMenuGame, DieAbstractionTest_Sylvan) { |
|
|
TEST(PrismMenuGame, DieAbstractionTest_Sylvan) { |
|
|
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/die.pm"); |
|
|
|
|
|
|
|
|
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm"); |
|
|
|
|
|
|
|
|
std::vector<storm::expressions::Expression> initialPredicates; |
|
|
std::vector<storm::expressions::Expression> initialPredicates; |
|
|
storm::expressions::ExpressionManager& manager = program.getManager(); |
|
|
storm::expressions::ExpressionManager& manager = program.getManager(); |
|
@ -54,7 +54,7 @@ TEST(PrismMenuGame, DieAbstractionTest_Sylvan) { |
|
|
|
|
|
|
|
|
#ifdef STORM_HAVE_CARL
|
|
|
#ifdef STORM_HAVE_CARL
|
|
|
TEST(PrismMenuGame, DieAbstractionTest_SylvanWithRationalFunction) { |
|
|
TEST(PrismMenuGame, DieAbstractionTest_SylvanWithRationalFunction) { |
|
|
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/die.pm"); |
|
|
|
|
|
|
|
|
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm"); |
|
|
|
|
|
|
|
|
std::vector<storm::expressions::Expression> initialPredicates; |
|
|
std::vector<storm::expressions::Expression> initialPredicates; |
|
|
storm::expressions::ExpressionManager& manager = program.getManager(); |
|
|
storm::expressions::ExpressionManager& manager = program.getManager(); |
|
@ -72,7 +72,7 @@ TEST(PrismMenuGame, DieAbstractionTest_SylvanWithRationalFunction) { |
|
|
#endif
|
|
|
#endif
|
|
|
|
|
|
|
|
|
TEST(PrismMenuGame, DieAbstractionAndRefinementTest_Cudd) { |
|
|
TEST(PrismMenuGame, DieAbstractionAndRefinementTest_Cudd) { |
|
|
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/die.pm"); |
|
|
|
|
|
|
|
|
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm"); |
|
|
|
|
|
|
|
|
std::vector<storm::expressions::Expression> initialPredicates; |
|
|
std::vector<storm::expressions::Expression> initialPredicates; |
|
|
storm::expressions::ExpressionManager& manager = program.getManager(); |
|
|
storm::expressions::ExpressionManager& manager = program.getManager(); |
|
@ -91,7 +91,7 @@ TEST(PrismMenuGame, DieAbstractionAndRefinementTest_Cudd) { |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
TEST(PrismMenuGame, DieAbstractionAndRefinementTest_Sylvan) { |
|
|
TEST(PrismMenuGame, DieAbstractionAndRefinementTest_Sylvan) { |
|
|
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/die.pm"); |
|
|
|
|
|
|
|
|
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm"); |
|
|
|
|
|
|
|
|
std::vector<storm::expressions::Expression> initialPredicates; |
|
|
std::vector<storm::expressions::Expression> initialPredicates; |
|
|
storm::expressions::ExpressionManager& manager = program.getManager(); |
|
|
storm::expressions::ExpressionManager& manager = program.getManager(); |
|
@ -110,7 +110,7 @@ TEST(PrismMenuGame, DieAbstractionAndRefinementTest_Sylvan) { |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
TEST(PrismMenuGame, DieFullAbstractionTest_Cudd) { |
|
|
TEST(PrismMenuGame, DieFullAbstractionTest_Cudd) { |
|
|
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/die.pm"); |
|
|
|
|
|
|
|
|
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm"); |
|
|
|
|
|
|
|
|
std::vector<storm::expressions::Expression> initialPredicates; |
|
|
std::vector<storm::expressions::Expression> initialPredicates; |
|
|
storm::expressions::ExpressionManager& manager = program.getManager(); |
|
|
storm::expressions::ExpressionManager& manager = program.getManager(); |
|
@ -142,7 +142,7 @@ TEST(PrismMenuGame, DieFullAbstractionTest_Cudd) { |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
TEST(PrismMenuGame, DieFullAbstractionTest_Sylvan) { |
|
|
TEST(PrismMenuGame, DieFullAbstractionTest_Sylvan) { |
|
|
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/die.pm"); |
|
|
|
|
|
|
|
|
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm"); |
|
|
|
|
|
|
|
|
std::vector<storm::expressions::Expression> initialPredicates; |
|
|
std::vector<storm::expressions::Expression> initialPredicates; |
|
|
storm::expressions::ExpressionManager& manager = program.getManager(); |
|
|
storm::expressions::ExpressionManager& manager = program.getManager(); |
|
@ -174,7 +174,7 @@ TEST(PrismMenuGame, DieFullAbstractionTest_Sylvan) { |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
TEST(PrismMenuGame, CrowdsAbstractionTest_Cudd) { |
|
|
TEST(PrismMenuGame, CrowdsAbstractionTest_Cudd) { |
|
|
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/crowds-5-5.pm"); |
|
|
|
|
|
|
|
|
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.pm"); |
|
|
program = program.substituteConstants(); |
|
|
program = program.substituteConstants(); |
|
|
|
|
|
|
|
|
std::vector<storm::expressions::Expression> initialPredicates; |
|
|
std::vector<storm::expressions::Expression> initialPredicates; |
|
@ -192,7 +192,7 @@ TEST(PrismMenuGame, CrowdsAbstractionTest_Cudd) { |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
TEST(PrismMenuGame, CrowdsAbstractionTest_Sylvan) { |
|
|
TEST(PrismMenuGame, CrowdsAbstractionTest_Sylvan) { |
|
|
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/crowds-5-5.pm"); |
|
|
|
|
|
|
|
|
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.pm"); |
|
|
program = program.substituteConstants(); |
|
|
program = program.substituteConstants(); |
|
|
|
|
|
|
|
|
std::vector<storm::expressions::Expression> initialPredicates; |
|
|
std::vector<storm::expressions::Expression> initialPredicates; |
|
@ -210,7 +210,7 @@ TEST(PrismMenuGame, CrowdsAbstractionTest_Sylvan) { |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
TEST(PrismMenuGame, CrowdsAbstractionAndRefinementTest_Cudd) { |
|
|
TEST(PrismMenuGame, CrowdsAbstractionAndRefinementTest_Cudd) { |
|
|
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/crowds-5-5.pm"); |
|
|
|
|
|
|
|
|
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.pm"); |
|
|
program = program.substituteConstants(); |
|
|
program = program.substituteConstants(); |
|
|
|
|
|
|
|
|
std::vector<storm::expressions::Expression> initialPredicates; |
|
|
std::vector<storm::expressions::Expression> initialPredicates; |
|
@ -230,7 +230,7 @@ TEST(PrismMenuGame, CrowdsAbstractionAndRefinementTest_Cudd) { |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
TEST(PrismMenuGame, CrowdsAbstractionAndRefinementTest_Sylvan) { |
|
|
TEST(PrismMenuGame, CrowdsAbstractionAndRefinementTest_Sylvan) { |
|
|
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/crowds-5-5.pm"); |
|
|
|
|
|
|
|
|
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.pm"); |
|
|
program = program.substituteConstants(); |
|
|
program = program.substituteConstants(); |
|
|
|
|
|
|
|
|
std::vector<storm::expressions::Expression> initialPredicates; |
|
|
std::vector<storm::expressions::Expression> initialPredicates; |
|
@ -250,7 +250,7 @@ TEST(PrismMenuGame, CrowdsAbstractionAndRefinementTest_Sylvan) { |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
TEST(PrismMenuGame, CrowdsFullAbstractionTest_Cudd) { |
|
|
TEST(PrismMenuGame, CrowdsFullAbstractionTest_Cudd) { |
|
|
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/crowds-5-5.pm"); |
|
|
|
|
|
|
|
|
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.pm"); |
|
|
program = program.substituteConstants(); |
|
|
program = program.substituteConstants(); |
|
|
|
|
|
|
|
|
std::vector<storm::expressions::Expression> initialPredicates; |
|
|
std::vector<storm::expressions::Expression> initialPredicates; |
|
@ -322,7 +322,7 @@ TEST(PrismMenuGame, CrowdsFullAbstractionTest_Cudd) { |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
TEST(PrismMenuGame, CrowdsFullAbstractionTest_Sylvan) { |
|
|
TEST(PrismMenuGame, CrowdsFullAbstractionTest_Sylvan) { |
|
|
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/crowds-5-5.pm"); |
|
|
|
|
|
|
|
|
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.pm"); |
|
|
program = program.substituteConstants(); |
|
|
program = program.substituteConstants(); |
|
|
|
|
|
|
|
|
std::vector<storm::expressions::Expression> initialPredicates; |
|
|
std::vector<storm::expressions::Expression> initialPredicates; |
|
@ -394,7 +394,7 @@ TEST(PrismMenuGame, CrowdsFullAbstractionTest_Sylvan) { |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
TEST(PrismMenuGame, TwoDiceAbstractionTest_Cudd) { |
|
|
TEST(PrismMenuGame, TwoDiceAbstractionTest_Cudd) { |
|
|
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/two_dice.nm"); |
|
|
|
|
|
|
|
|
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm"); |
|
|
program = program.substituteConstants(); |
|
|
program = program.substituteConstants(); |
|
|
program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>()); |
|
|
program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>()); |
|
|
|
|
|
|
|
@ -414,7 +414,7 @@ TEST(PrismMenuGame, TwoDiceAbstractionTest_Cudd) { |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
TEST(PrismMenuGame, TwoDiceAbstractionTest_Sylvan) { |
|
|
TEST(PrismMenuGame, TwoDiceAbstractionTest_Sylvan) { |
|
|
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/two_dice.nm"); |
|
|
|
|
|
|
|
|
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm"); |
|
|
program = program.substituteConstants(); |
|
|
program = program.substituteConstants(); |
|
|
program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>()); |
|
|
program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>()); |
|
|
|
|
|
|
|
@ -434,7 +434,7 @@ TEST(PrismMenuGame, TwoDiceAbstractionTest_Sylvan) { |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
TEST(PrismMenuGame, TwoDiceAbstractionAndRefinementTest_Cudd) { |
|
|
TEST(PrismMenuGame, TwoDiceAbstractionAndRefinementTest_Cudd) { |
|
|
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/two_dice.nm"); |
|
|
|
|
|
|
|
|
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/builder/two_dice.nm"); |
|
|
program = program.substituteConstants(); |
|
|
program = program.substituteConstants(); |
|
|
program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>()); |
|
|
program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>()); |
|
|
|
|
|
|
|
@ -456,7 +456,7 @@ TEST(PrismMenuGame, TwoDiceAbstractionAndRefinementTest_Cudd) { |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
TEST(PrismMenuGame, TwoDiceAbstractionAndRefinementTest_Sylvan) { |
|
|
TEST(PrismMenuGame, TwoDiceAbstractionAndRefinementTest_Sylvan) { |
|
|
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/two_dice.nm"); |
|
|
|
|
|
|
|
|
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/builder/two_dice.nm"); |
|
|
program = program.substituteConstants(); |
|
|
program = program.substituteConstants(); |
|
|
program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>()); |
|
|
program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>()); |
|
|
|
|
|
|
|
@ -478,7 +478,7 @@ TEST(PrismMenuGame, TwoDiceAbstractionAndRefinementTest_Sylvan) { |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
TEST(PrismMenuGame, TwoDiceFullAbstractionTest_Cudd) { |
|
|
TEST(PrismMenuGame, TwoDiceFullAbstractionTest_Cudd) { |
|
|
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/two_dice.nm"); |
|
|
|
|
|
|
|
|
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm"); |
|
|
program = program.substituteConstants(); |
|
|
program = program.substituteConstants(); |
|
|
program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>()); |
|
|
program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>()); |
|
|
|
|
|
|
|
@ -529,7 +529,7 @@ TEST(PrismMenuGame, TwoDiceFullAbstractionTest_Cudd) { |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
TEST(PrismMenuGame, TwoDiceFullAbstractionTest_Sylvan) { |
|
|
TEST(PrismMenuGame, TwoDiceFullAbstractionTest_Sylvan) { |
|
|
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/two_dice.nm"); |
|
|
|
|
|
|
|
|
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm"); |
|
|
program = program.substituteConstants(); |
|
|
program = program.substituteConstants(); |
|
|
program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>()); |
|
|
program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>()); |
|
|
|
|
|
|
|
@ -580,7 +580,7 @@ TEST(PrismMenuGame, TwoDiceFullAbstractionTest_Sylvan) { |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
TEST(PrismMenuGame, WlanAbstractionTest_Cudd) { |
|
|
TEST(PrismMenuGame, WlanAbstractionTest_Cudd) { |
|
|
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/wlan0-2-4.nm"); |
|
|
|
|
|
|
|
|
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/wlan0-2-4.nm"); |
|
|
program = program.substituteConstants(); |
|
|
program = program.substituteConstants(); |
|
|
program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>()); |
|
|
program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>()); |
|
|
|
|
|
|
|
@ -601,7 +601,7 @@ TEST(PrismMenuGame, WlanAbstractionTest_Cudd) { |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
TEST(PrismMenuGame, WlanAbstractionTest_Sylvan) { |
|
|
TEST(PrismMenuGame, WlanAbstractionTest_Sylvan) { |
|
|
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/wlan0-2-4.nm"); |
|
|
|
|
|
|
|
|
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/wlan0-2-4.nm"); |
|
|
program = program.substituteConstants(); |
|
|
program = program.substituteConstants(); |
|
|
program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>()); |
|
|
program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>()); |
|
|
|
|
|
|
|
@ -622,7 +622,7 @@ TEST(PrismMenuGame, WlanAbstractionTest_Sylvan) { |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
TEST(PrismMenuGame, WlanAbstractionAndRefinementTest_Cudd) { |
|
|
TEST(PrismMenuGame, WlanAbstractionAndRefinementTest_Cudd) { |
|
|
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/wlan0-2-4.nm"); |
|
|
|
|
|
|
|
|
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/wlan0-2-4.nm"); |
|
|
program = program.substituteConstants(); |
|
|
program = program.substituteConstants(); |
|
|
program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>()); |
|
|
program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>()); |
|
|
|
|
|
|
|
@ -645,7 +645,7 @@ TEST(PrismMenuGame, WlanAbstractionAndRefinementTest_Cudd) { |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
TEST(PrismMenuGame, WlanAbstractionAndRefinementTest_Sylvan) { |
|
|
TEST(PrismMenuGame, WlanAbstractionAndRefinementTest_Sylvan) { |
|
|
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/wlan0-2-4.nm"); |
|
|
|
|
|
|
|
|
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/wlan0-2-4.nm"); |
|
|
program = program.substituteConstants(); |
|
|
program = program.substituteConstants(); |
|
|
program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>()); |
|
|
program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>()); |
|
|
|
|
|
|
|
@ -668,7 +668,7 @@ TEST(PrismMenuGame, WlanAbstractionAndRefinementTest_Sylvan) { |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
TEST(PrismMenuGame, WlanFullAbstractionTest_Cudd) { |
|
|
TEST(PrismMenuGame, WlanFullAbstractionTest_Cudd) { |
|
|
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/wlan0-2-4.nm"); |
|
|
|
|
|
|
|
|
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/wlan0-2-4.nm"); |
|
|
program = program.substituteConstants(); |
|
|
program = program.substituteConstants(); |
|
|
program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>()); |
|
|
program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>()); |
|
|
|
|
|
|
|
@ -787,7 +787,7 @@ TEST(PrismMenuGame, WlanFullAbstractionTest_Cudd) { |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
TEST(PrismMenuGame, WlanFullAbstractionTest_Sylvan) { |
|
|
TEST(PrismMenuGame, WlanFullAbstractionTest_Sylvan) { |
|
|
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/wlan0-2-4.nm"); |
|
|
|
|
|
|
|
|
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/wlan0-2-4.nm"); |
|
|
program = program.substituteConstants(); |
|
|
program = program.substituteConstants(); |
|
|
program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>()); |
|
|
program = program.flattenModules(std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>()); |
|
|
|
|
|
|
|
|