diff --git a/test/functional/abstraction/PrismMenuGameTest.cpp b/test/functional/abstraction/PrismMenuGameTest.cpp index 70624a1ff..038ea6eb8 100644 --- a/test/functional/abstraction/PrismMenuGameTest.cpp +++ b/test/functional/abstraction/PrismMenuGameTest.cpp @@ -26,7 +26,7 @@ TEST(PrismMenuGame, DieAbstractionTest_Cudd) { initialPredicates.push_back(manager.getVariableExpression("s") < manager.integer(3)); - storm::abstraction::prism::AbstractProgram abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); + storm::abstraction::prism::AbstractProgram abstractProgram(program, initialPredicates, std::make_shared(), false); storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); @@ -43,7 +43,7 @@ TEST(PrismMenuGame, DieAbstractionTest_Sylvan) { initialPredicates.push_back(manager.getVariableExpression("s") < manager.integer(3)); - storm::abstraction::prism::AbstractProgram abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); + storm::abstraction::prism::AbstractProgram abstractProgram(program, initialPredicates, std::make_shared(), false); storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); @@ -61,7 +61,7 @@ TEST(PrismMenuGame, DieAbstractionTest_SylvanWithRationalFunction) { initialPredicates.push_back(manager.getVariableExpression("s") < manager.integer(3)); - storm::abstraction::prism::AbstractProgram abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); + storm::abstraction::prism::AbstractProgram abstractProgram(program, initialPredicates, std::make_shared(), false); storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); @@ -79,7 +79,7 @@ TEST(PrismMenuGame, DieAbstractionAndRefinementTest_Cudd) { initialPredicates.push_back(manager.getVariableExpression("s") < manager.integer(3)); - storm::abstraction::prism::AbstractProgram abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); + storm::abstraction::prism::AbstractProgram abstractProgram(program, initialPredicates, std::make_shared(), 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 abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); + storm::abstraction::prism::AbstractProgram abstractProgram(program, initialPredicates, std::make_shared(), 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 abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); + storm::abstraction::prism::AbstractProgram abstractProgram(program, initialPredicates, std::make_shared(), false); storm::abstraction::MenuGame 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 abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); + storm::abstraction::prism::AbstractProgram abstractProgram(program, initialPredicates, std::make_shared(), false); storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); @@ -182,7 +182,7 @@ TEST(PrismMenuGame, CrowdsAbstractionTest_Cudd) { initialPredicates.push_back(manager.getVariableExpression("phase") < manager.integer(3)); - storm::abstraction::prism::AbstractProgram abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); + storm::abstraction::prism::AbstractProgram abstractProgram(program, initialPredicates, std::make_shared(), false); storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); @@ -200,7 +200,7 @@ TEST(PrismMenuGame, CrowdsAbstractionTest_Sylvan) { initialPredicates.push_back(manager.getVariableExpression("phase") < manager.integer(3)); - storm::abstraction::prism::AbstractProgram abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); + storm::abstraction::prism::AbstractProgram abstractProgram(program, initialPredicates, std::make_shared(), false); storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); @@ -218,7 +218,7 @@ TEST(PrismMenuGame, CrowdsAbstractionAndRefinementTest_Cudd) { initialPredicates.push_back(manager.getVariableExpression("phase") < manager.integer(3)); - storm::abstraction::prism::AbstractProgram abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); + storm::abstraction::prism::AbstractProgram abstractProgram(program, initialPredicates, std::make_shared(), 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 abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); + storm::abstraction::prism::AbstractProgram abstractProgram(program, initialPredicates, std::make_shared(), 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 abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); + storm::abstraction::prism::AbstractProgram abstractProgram(program, initialPredicates, std::make_shared(), false); storm::abstraction::MenuGame 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 abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); + storm::abstraction::prism::AbstractProgram abstractProgram(program, initialPredicates, std::make_shared(), false); storm::abstraction::MenuGame 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 abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); + storm::abstraction::prism::AbstractProgram abstractProgram(program, initialPredicates, std::make_shared(), false); storm::abstraction::MenuGame 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 abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); + storm::abstraction::prism::AbstractProgram abstractProgram(program, initialPredicates, std::make_shared(), false); storm::abstraction::MenuGame 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 abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); + storm::abstraction::prism::AbstractProgram abstractProgram(program, initialPredicates, std::make_shared(), 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 abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); + storm::abstraction::prism::AbstractProgram abstractProgram(program, initialPredicates, std::make_shared(), 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 abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); + storm::abstraction::prism::AbstractProgram abstractProgram(program, initialPredicates, std::make_shared(), false); storm::abstraction::MenuGame 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 abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); + storm::abstraction::prism::AbstractProgram abstractProgram(program, initialPredicates, std::make_shared(), false); storm::abstraction::MenuGame 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 abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); + storm::abstraction::prism::AbstractProgram abstractProgram(program, initialPredicates, std::make_shared(), false); storm::abstraction::MenuGame 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 abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); + storm::abstraction::prism::AbstractProgram abstractProgram(program, initialPredicates, std::make_shared(), false); storm::abstraction::MenuGame 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 abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); + storm::abstraction::prism::AbstractProgram abstractProgram(program, initialPredicates, std::make_shared(), 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 abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); + storm::abstraction::prism::AbstractProgram abstractProgram(program, initialPredicates, std::make_shared(), 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 abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); + storm::abstraction::prism::AbstractProgram abstractProgram(program, initialPredicates, std::make_shared(), false); storm::abstraction::MenuGame 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 abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); + storm::abstraction::prism::AbstractProgram abstractProgram(program, initialPredicates, std::make_shared(), false); storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); @@ -905,4 +905,4 @@ TEST(PrismMenuGame, WlanFullAbstractionTest_Sylvan) { EXPECT_EQ(0, game.getBottomStates().getNonZeroCount()); } -#endif \ No newline at end of file +#endif diff --git a/test/functional/storage/PrismProgramTest.cpp b/test/functional/storage/PrismProgramTest.cpp index 1ae7c4f32..281d981c0 100644 --- a/test/functional/storage/PrismProgramTest.cpp +++ b/test/functional/storage/PrismProgramTest.cpp @@ -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 smtSolverFactory(new storm::utility::solver::MathsatSmtSolverFactory()); + std::shared_ptr 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()); -} \ No newline at end of file +} diff --git a/test/functional/utility/GraphTest.cpp b/test/functional/utility/GraphTest.cpp index 8f88c696a..62c52b0f9 100644 --- a/test/functional/utility/GraphTest.cpp +++ b/test/functional/utility/GraphTest.cpp @@ -207,7 +207,7 @@ TEST(GraphTest, SymbolicProb01StochasticGameDieSmall) { initialPredicates.push_back(manager.getVariableExpression("s") < manager.integer(3)); - storm::abstraction::prism::AbstractProgram abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); + storm::abstraction::prism::AbstractProgram abstractProgram(program, initialPredicates, std::make_shared(), false); storm::abstraction::MenuGame 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 abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); + storm::abstraction::prism::AbstractProgram abstractProgram(program, initialPredicates, std::make_shared(), false); storm::abstraction::MenuGame 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 abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); + storm::abstraction::prism::AbstractProgram abstractProgram(program, initialPredicates, std::make_shared(), false); storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); @@ -644,4 +644,4 @@ TEST(GraphTest, ExplicitProb01MinMax) { ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->as>(), storm::storage::BitVector(model->getNumberOfStates(), true), model->getStates("collision_max_backoff"))); EXPECT_EQ(993ul, statesWithProbability01.first.getNumberOfSetBits()); EXPECT_EQ(16ul, statesWithProbability01.second.getNumberOfSetBits()); -} \ No newline at end of file +}