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

Fixed errors because of changed API. 

Former-commit-id: 7f771dc576
main
PBerger 9 years ago
parent
2de905fd5f
commit
81311690ab
3 changed files with 32 additions and 32 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 52
      test/functional/abstraction/PrismMenuGameTest.cpp
  2. 4
      test/functional/storage/PrismProgramTest.cpp
  3. 8
      test/functional/utility/GraphTest.cpp

52
test/functional/abstraction/PrismMenuGameTest.cpp
View File

@ -26,7 +26,7 @@ TEST(PrismMenuGame, DieAbstractionTest_Cudd) {
initialPredicates.push_back(manager.getVariableExpression("s") < manager.integer(3));
storm::abstraction::prism::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
storm::abstraction::prism::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
storm::abstraction::MenuGame<storm::dd::DdType::CUDD, double> game = abstractProgram.getAbstractGame();
@ -43,7 +43,7 @@ TEST(PrismMenuGame, DieAbstractionTest_Sylvan) {
initialPredicates.push_back(manager.getVariableExpression("s") < manager.integer(3));
storm::abstraction::prism::AbstractProgram<storm::dd::DdType::Sylvan, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
storm::abstraction::prism::AbstractProgram<storm::dd::DdType::Sylvan, double> abstractProgram(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
storm::abstraction::MenuGame<storm::dd::DdType::Sylvan, double> game = abstractProgram.getAbstractGame();
@ -61,7 +61,7 @@ TEST(PrismMenuGame, DieAbstractionTest_SylvanWithRationalFunction) {
initialPredicates.push_back(manager.getVariableExpression("s") < manager.integer(3));
storm::abstraction::prism::AbstractProgram<storm::dd::DdType::Sylvan, storm::RationalFunction> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
storm::abstraction::prism::AbstractProgram<storm::dd::DdType::Sylvan, storm::RationalFunction> abstractProgram(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
storm::abstraction::MenuGame<storm::dd::DdType::Sylvan, storm::RationalFunction> game = abstractProgram.getAbstractGame();
@ -79,7 +79,7 @@ TEST(PrismMenuGame, DieAbstractionAndRefinementTest_Cudd) {
initialPredicates.push_back(manager.getVariableExpression("s") < manager.integer(3));
storm::abstraction::prism::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
storm::abstraction::prism::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
ASSERT_NO_THROW(abstractProgram.refine({manager.getVariableExpression("s") == manager.integer(7)}));
@ -98,7 +98,7 @@ TEST(PrismMenuGame, DieAbstractionAndRefinementTest_Sylvan) {
initialPredicates.push_back(manager.getVariableExpression("s") < manager.integer(3));
storm::abstraction::prism::AbstractProgram<storm::dd::DdType::Sylvan, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
storm::abstraction::prism::AbstractProgram<storm::dd::DdType::Sylvan, double> abstractProgram(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
ASSERT_NO_THROW(abstractProgram.refine({manager.getVariableExpression("s") == manager.integer(7)}));
@ -132,7 +132,7 @@ TEST(PrismMenuGame, DieFullAbstractionTest_Cudd) {
initialPredicates.push_back(manager.getVariableExpression("d") == manager.integer(5));
initialPredicates.push_back(manager.getVariableExpression("d") == manager.integer(6));
storm::abstraction::prism::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
storm::abstraction::prism::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
storm::abstraction::MenuGame<storm::dd::DdType::CUDD, double> game = abstractProgram.getAbstractGame();
@ -164,7 +164,7 @@ TEST(PrismMenuGame, DieFullAbstractionTest_Sylvan) {
initialPredicates.push_back(manager.getVariableExpression("d") == manager.integer(5));
initialPredicates.push_back(manager.getVariableExpression("d") == manager.integer(6));
storm::abstraction::prism::AbstractProgram<storm::dd::DdType::Sylvan, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
storm::abstraction::prism::AbstractProgram<storm::dd::DdType::Sylvan, double> abstractProgram(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
storm::abstraction::MenuGame<storm::dd::DdType::Sylvan, double> game = abstractProgram.getAbstractGame();
@ -182,7 +182,7 @@ TEST(PrismMenuGame, CrowdsAbstractionTest_Cudd) {
initialPredicates.push_back(manager.getVariableExpression("phase") < manager.integer(3));
storm::abstraction::prism::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
storm::abstraction::prism::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
storm::abstraction::MenuGame<storm::dd::DdType::CUDD, double> game = abstractProgram.getAbstractGame();
@ -200,7 +200,7 @@ TEST(PrismMenuGame, CrowdsAbstractionTest_Sylvan) {
initialPredicates.push_back(manager.getVariableExpression("phase") < manager.integer(3));
storm::abstraction::prism::AbstractProgram<storm::dd::DdType::Sylvan, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
storm::abstraction::prism::AbstractProgram<storm::dd::DdType::Sylvan, double> abstractProgram(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
storm::abstraction::MenuGame<storm::dd::DdType::Sylvan, double> game = abstractProgram.getAbstractGame();
@ -218,7 +218,7 @@ TEST(PrismMenuGame, CrowdsAbstractionAndRefinementTest_Cudd) {
initialPredicates.push_back(manager.getVariableExpression("phase") < manager.integer(3));
storm::abstraction::prism::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
storm::abstraction::prism::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
ASSERT_NO_THROW(abstractProgram.refine({manager.getVariableExpression("observe0") + manager.getVariableExpression("observe1") + manager.getVariableExpression("observe2") + manager.getVariableExpression("observe3") + manager.getVariableExpression("observe4") <= manager.getVariableExpression("runCount")}));
@ -238,7 +238,7 @@ TEST(PrismMenuGame, CrowdsAbstractionAndRefinementTest_Sylvan) {
initialPredicates.push_back(manager.getVariableExpression("phase") < manager.integer(3));
storm::abstraction::prism::AbstractProgram<storm::dd::DdType::Sylvan, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
storm::abstraction::prism::AbstractProgram<storm::dd::DdType::Sylvan, double> abstractProgram(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
ASSERT_NO_THROW(abstractProgram.refine({manager.getVariableExpression("observe0") + manager.getVariableExpression("observe1") + manager.getVariableExpression("observe2") + manager.getVariableExpression("observe3") + manager.getVariableExpression("observe4") <= manager.getVariableExpression("runCount")}));
@ -312,7 +312,7 @@ TEST(PrismMenuGame, CrowdsFullAbstractionTest_Cudd) {
initialPredicates.push_back(manager.getVariableExpression("lastSeen") == manager.integer(3));
initialPredicates.push_back(manager.getVariableExpression("lastSeen") == manager.integer(4));
storm::abstraction::prism::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
storm::abstraction::prism::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
storm::abstraction::MenuGame<storm::dd::DdType::CUDD, double> game = abstractProgram.getAbstractGame();
@ -384,7 +384,7 @@ TEST(PrismMenuGame, CrowdsFullAbstractionTest_Sylvan) {
initialPredicates.push_back(manager.getVariableExpression("lastSeen") == manager.integer(3));
initialPredicates.push_back(manager.getVariableExpression("lastSeen") == manager.integer(4));
storm::abstraction::prism::AbstractProgram<storm::dd::DdType::Sylvan, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
storm::abstraction::prism::AbstractProgram<storm::dd::DdType::Sylvan, double> abstractProgram(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
storm::abstraction::MenuGame<storm::dd::DdType::Sylvan, double> game = abstractProgram.getAbstractGame();
@ -404,7 +404,7 @@ TEST(PrismMenuGame, TwoDiceAbstractionTest_Cudd) {
initialPredicates.push_back(manager.getVariableExpression("s1") < manager.integer(3));
initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(0));
storm::abstraction::prism::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
storm::abstraction::prism::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
storm::abstraction::MenuGame<storm::dd::DdType::CUDD, double> game = abstractProgram.getAbstractGame();
@ -424,7 +424,7 @@ TEST(PrismMenuGame, TwoDiceAbstractionTest_Sylvan) {
initialPredicates.push_back(manager.getVariableExpression("s1") < manager.integer(3));
initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(0));
storm::abstraction::prism::AbstractProgram<storm::dd::DdType::Sylvan, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
storm::abstraction::prism::AbstractProgram<storm::dd::DdType::Sylvan, double> abstractProgram(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
storm::abstraction::MenuGame<storm::dd::DdType::Sylvan, double> game = abstractProgram.getAbstractGame();
@ -444,7 +444,7 @@ TEST(PrismMenuGame, TwoDiceAbstractionAndRefinementTest_Cudd) {
initialPredicates.push_back(manager.getVariableExpression("s1") < manager.integer(3));
initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(0));
storm::abstraction::prism::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
storm::abstraction::prism::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
ASSERT_NO_THROW(abstractProgram.refine({manager.getVariableExpression("d1") + manager.getVariableExpression("d2") == manager.integer(7)}));
@ -466,7 +466,7 @@ TEST(PrismMenuGame, TwoDiceAbstractionAndRefinementTest_Sylvan) {
initialPredicates.push_back(manager.getVariableExpression("s1") < manager.integer(3));
initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(0));
storm::abstraction::prism::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
storm::abstraction::prism::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
ASSERT_NO_THROW(abstractProgram.refine({manager.getVariableExpression("d1") + manager.getVariableExpression("d2") == manager.integer(7)}));
@ -519,7 +519,7 @@ TEST(PrismMenuGame, TwoDiceFullAbstractionTest_Cudd) {
initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(5));
initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(6));
storm::abstraction::prism::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
storm::abstraction::prism::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
storm::abstraction::MenuGame<storm::dd::DdType::CUDD, double> game = abstractProgram.getAbstractGame();
@ -570,7 +570,7 @@ TEST(PrismMenuGame, TwoDiceFullAbstractionTest_Sylvan) {
initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(5));
initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(6));
storm::abstraction::prism::AbstractProgram<storm::dd::DdType::Sylvan, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
storm::abstraction::prism::AbstractProgram<storm::dd::DdType::Sylvan, double> abstractProgram(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
storm::abstraction::MenuGame<storm::dd::DdType::Sylvan, double> game = abstractProgram.getAbstractGame();
@ -591,7 +591,7 @@ TEST(PrismMenuGame, WlanAbstractionTest_Cudd) {
initialPredicates.push_back(manager.getVariableExpression("bc1") == manager.integer(0));
initialPredicates.push_back(manager.getVariableExpression("c1") == manager.getVariableExpression("c2"));
storm::abstraction::prism::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
storm::abstraction::prism::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
storm::abstraction::MenuGame<storm::dd::DdType::CUDD, double> game = abstractProgram.getAbstractGame();
@ -612,7 +612,7 @@ TEST(PrismMenuGame, WlanAbstractionTest_Sylvan) {
initialPredicates.push_back(manager.getVariableExpression("bc1") == manager.integer(0));
initialPredicates.push_back(manager.getVariableExpression("c1") == manager.getVariableExpression("c2"));
storm::abstraction::prism::AbstractProgram<storm::dd::DdType::Sylvan, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
storm::abstraction::prism::AbstractProgram<storm::dd::DdType::Sylvan, double> abstractProgram(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
storm::abstraction::MenuGame<storm::dd::DdType::Sylvan, double> game = abstractProgram.getAbstractGame();
@ -633,7 +633,7 @@ TEST(PrismMenuGame, WlanAbstractionAndRefinementTest_Cudd) {
initialPredicates.push_back(manager.getVariableExpression("bc1") == manager.integer(0));
initialPredicates.push_back(manager.getVariableExpression("c1") == manager.getVariableExpression("c2"));
storm::abstraction::prism::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
storm::abstraction::prism::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
ASSERT_NO_THROW(abstractProgram.refine({manager.getVariableExpression("backoff1") < manager.integer(7)}));
@ -656,7 +656,7 @@ TEST(PrismMenuGame, WlanAbstractionAndRefinementTest_Sylvan) {
initialPredicates.push_back(manager.getVariableExpression("bc1") == manager.integer(0));
initialPredicates.push_back(manager.getVariableExpression("c1") == manager.getVariableExpression("c2"));
storm::abstraction::prism::AbstractProgram<storm::dd::DdType::Sylvan, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
storm::abstraction::prism::AbstractProgram<storm::dd::DdType::Sylvan, double> abstractProgram(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
ASSERT_NO_THROW(abstractProgram.refine({manager.getVariableExpression("backoff1") < manager.integer(7)}));
@ -777,7 +777,7 @@ TEST(PrismMenuGame, WlanFullAbstractionTest_Cudd) {
initialPredicates.push_back(manager.getVariableExpression("bc2") == manager.integer(0));
initialPredicates.push_back(manager.getVariableExpression("bc2") == manager.integer(1));
storm::abstraction::prism::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
storm::abstraction::prism::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
storm::abstraction::MenuGame<storm::dd::DdType::CUDD, double> game = abstractProgram.getAbstractGame();
@ -896,7 +896,7 @@ TEST(PrismMenuGame, WlanFullAbstractionTest_Sylvan) {
initialPredicates.push_back(manager.getVariableExpression("bc2") == manager.integer(0));
initialPredicates.push_back(manager.getVariableExpression("bc2") == manager.integer(1));
storm::abstraction::prism::AbstractProgram<storm::dd::DdType::Sylvan, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
storm::abstraction::prism::AbstractProgram<storm::dd::DdType::Sylvan, double> abstractProgram(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
storm::abstraction::MenuGame<storm::dd::DdType::Sylvan, double> game = abstractProgram.getAbstractGame();
@ -905,4 +905,4 @@ TEST(PrismMenuGame, WlanFullAbstractionTest_Sylvan) {
EXPECT_EQ(0, game.getBottomStates().getNonZeroCount());
}
#endif
#endif

4
test/functional/storage/PrismProgramTest.cpp
View File

@ -11,7 +11,7 @@ TEST(PrismProgramTest, FlattenModules) {
storm::prism::Program result;
ASSERT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/leader3.nm"));
std::unique_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory(new storm::utility::solver::MathsatSmtSolverFactory());
std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory(new storm::utility::solver::MathsatSmtSolverFactory());
ASSERT_NO_THROW(result = result.flattenModules(smtSolverFactory));
EXPECT_EQ(1, result.getNumberOfModules());
@ -46,4 +46,4 @@ TEST(PrismProgramTest, ConvertToJani) {
ASSERT_NO_THROW(prismProgram = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm"));
ASSERT_NO_THROW(janiModel = prismProgram.toJani());
}
}

8
test/functional/utility/GraphTest.cpp
View File

@ -207,7 +207,7 @@ TEST(GraphTest, SymbolicProb01StochasticGameDieSmall) {
initialPredicates.push_back(manager.getVariableExpression("s") < manager.integer(3));
storm::abstraction::prism::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
storm::abstraction::prism::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
storm::abstraction::MenuGame<storm::dd::DdType::CUDD, double> game = abstractProgram.getAbstractGame();
@ -343,7 +343,7 @@ TEST(GraphTest, SymbolicProb01StochasticGameTwoDice) {
initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(5));
initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(6));
storm::abstraction::prism::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
storm::abstraction::prism::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
storm::abstraction::MenuGame<storm::dd::DdType::CUDD, double> game = abstractProgram.getAbstractGame();
@ -512,7 +512,7 @@ TEST(GraphTest, SymbolicProb01StochasticGameWlan) {
initialPredicates.push_back(manager.getVariableExpression("bc2") == manager.integer(0));
initialPredicates.push_back(manager.getVariableExpression("bc2") == manager.integer(1));
storm::abstraction::prism::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
storm::abstraction::prism::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program, initialPredicates, std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), false);
storm::abstraction::MenuGame<storm::dd::DdType::CUDD, double> game = abstractProgram.getAbstractGame();
@ -644,4 +644,4 @@ TEST(GraphTest, ExplicitProb01MinMax) {
ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->as<storm::models::sparse::Mdp<double>>(), storm::storage::BitVector(model->getNumberOfStates(), true), model->getStates("collision_max_backoff")));
EXPECT_EQ(993ul, statesWithProbability01.first.getNumberOfSetBits());
EXPECT_EQ(16ul, statesWithProbability01.second.getNumberOfSetBits());
}
}
Write Preview
Loading…
Cancel
Save