From 3e9f9552b1cdcf177c32803371e5aa732e224fef Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 9 Aug 2016 19:38:36 +0200 Subject: [PATCH 1/2] fixed tests: using shared_ptr instead of unique_ptr for SMT solver factory in abstraction Former-commit-id: 6159a20565d3938c32a17a3115ff227ed8bc67f3 --- .../abstraction/PrismMenuGameTest.cpp | 72 +++++++++---------- test/functional/storage/PrismProgramTest.cpp | 2 +- test/functional/utility/GraphTest.cpp | 6 +- 3 files changed, 40 insertions(+), 40 deletions(-) diff --git a/test/functional/abstraction/PrismMenuGameTest.cpp b/test/functional/abstraction/PrismMenuGameTest.cpp index 148bd6f25..ba2811a67 100644 --- a/test/functional/abstraction/PrismMenuGameTest.cpp +++ b/test/functional/abstraction/PrismMenuGameTest.cpp @@ -24,7 +24,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(); @@ -41,7 +41,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(); @@ -58,7 +58,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)})); @@ -77,7 +77,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)})); @@ -111,7 +111,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(); @@ -143,7 +143,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(); @@ -161,7 +161,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(); @@ -179,7 +179,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(); @@ -197,7 +197,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")})); @@ -217,7 +217,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")})); @@ -291,7 +291,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(); @@ -363,7 +363,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(); @@ -375,7 +375,7 @@ TEST(PrismMenuGame, CrowdsFullAbstractionTest_Sylvan) { TEST(PrismMenuGame, TwoDiceAbstractionTest_Cudd) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); program = program.substituteConstants(); - program = program.flattenModules(std::make_unique()); + program = program.flattenModules(std::make_shared()); std::vector initialPredicates; storm::expressions::ExpressionManager& manager = program.getManager(); @@ -383,7 +383,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(); @@ -395,7 +395,7 @@ TEST(PrismMenuGame, TwoDiceAbstractionTest_Cudd) { TEST(PrismMenuGame, TwoDiceAbstractionTest_Sylvan) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); program = program.substituteConstants(); - program = program.flattenModules(std::make_unique()); + program = program.flattenModules(std::make_shared()); std::vector initialPredicates; storm::expressions::ExpressionManager& manager = program.getManager(); @@ -403,7 +403,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(); @@ -415,7 +415,7 @@ TEST(PrismMenuGame, TwoDiceAbstractionTest_Sylvan) { TEST(PrismMenuGame, TwoDiceAbstractionAndRefinementTest_Cudd) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); program = program.substituteConstants(); - program = program.flattenModules(std::make_unique()); + program = program.flattenModules(std::make_shared()); std::vector initialPredicates; storm::expressions::ExpressionManager& manager = program.getManager(); @@ -423,7 +423,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)})); @@ -437,7 +437,7 @@ TEST(PrismMenuGame, TwoDiceAbstractionAndRefinementTest_Cudd) { TEST(PrismMenuGame, TwoDiceAbstractionAndRefinementTest_Sylvan) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); program = program.substituteConstants(); - program = program.flattenModules(std::make_unique()); + program = program.flattenModules(std::make_shared()); std::vector initialPredicates; storm::expressions::ExpressionManager& manager = program.getManager(); @@ -445,7 +445,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)})); @@ -459,7 +459,7 @@ TEST(PrismMenuGame, TwoDiceAbstractionAndRefinementTest_Sylvan) { TEST(PrismMenuGame, TwoDiceFullAbstractionTest_Cudd) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); program = program.substituteConstants(); - program = program.flattenModules(std::make_unique()); + program = program.flattenModules(std::make_shared()); std::vector initialPredicates; storm::expressions::ExpressionManager& manager = program.getManager(); @@ -498,7 +498,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(); @@ -510,7 +510,7 @@ TEST(PrismMenuGame, TwoDiceFullAbstractionTest_Cudd) { TEST(PrismMenuGame, TwoDiceFullAbstractionTest_Sylvan) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); program = program.substituteConstants(); - program = program.flattenModules(std::make_unique()); + program = program.flattenModules(std::make_shared()); std::vector initialPredicates; storm::expressions::ExpressionManager& manager = program.getManager(); @@ -549,7 +549,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(); @@ -561,7 +561,7 @@ TEST(PrismMenuGame, TwoDiceFullAbstractionTest_Sylvan) { TEST(PrismMenuGame, WlanAbstractionTest_Cudd) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-4.nm"); program = program.substituteConstants(); - program = program.flattenModules(std::make_unique()); + program = program.flattenModules(std::make_shared()); std::vector initialPredicates; storm::expressions::ExpressionManager& manager = program.getManager(); @@ -570,7 +570,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(); @@ -582,7 +582,7 @@ TEST(PrismMenuGame, WlanAbstractionTest_Cudd) { TEST(PrismMenuGame, WlanAbstractionTest_Sylvan) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-4.nm"); program = program.substituteConstants(); - program = program.flattenModules(std::make_unique()); + program = program.flattenModules(std::make_shared()); std::vector initialPredicates; storm::expressions::ExpressionManager& manager = program.getManager(); @@ -591,7 +591,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(); @@ -603,7 +603,7 @@ TEST(PrismMenuGame, WlanAbstractionTest_Sylvan) { TEST(PrismMenuGame, WlanAbstractionAndRefinementTest_Cudd) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-4.nm"); program = program.substituteConstants(); - program = program.flattenModules(std::make_unique()); + program = program.flattenModules(std::make_shared()); std::vector initialPredicates; storm::expressions::ExpressionManager& manager = program.getManager(); @@ -612,7 +612,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)})); @@ -626,7 +626,7 @@ TEST(PrismMenuGame, WlanAbstractionAndRefinementTest_Cudd) { TEST(PrismMenuGame, WlanAbstractionAndRefinementTest_Sylvan) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-4.nm"); program = program.substituteConstants(); - program = program.flattenModules(std::make_unique()); + program = program.flattenModules(std::make_shared()); std::vector initialPredicates; storm::expressions::ExpressionManager& manager = program.getManager(); @@ -635,7 +635,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)})); @@ -649,7 +649,7 @@ TEST(PrismMenuGame, WlanAbstractionAndRefinementTest_Sylvan) { TEST(PrismMenuGame, WlanFullAbstractionTest_Cudd) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-4.nm"); program = program.substituteConstants(); - program = program.flattenModules(std::make_unique()); + program = program.flattenModules(std::make_shared()); std::vector initialPredicates; storm::expressions::ExpressionManager& manager = program.getManager(); @@ -756,7 +756,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(); @@ -768,7 +768,7 @@ TEST(PrismMenuGame, WlanFullAbstractionTest_Cudd) { TEST(PrismMenuGame, WlanFullAbstractionTest_Sylvan) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-4.nm"); program = program.substituteConstants(); - program = program.flattenModules(std::make_unique()); + program = program.flattenModules(std::make_shared()); std::vector initialPredicates; storm::expressions::ExpressionManager& manager = program.getManager(); @@ -875,7 +875,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(); diff --git a/test/functional/storage/PrismProgramTest.cpp b/test/functional/storage/PrismProgramTest.cpp index 1ae7c4f32..b6a5d1264 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 = std::make_shared(); ASSERT_NO_THROW(result = result.flattenModules(smtSolverFactory)); EXPECT_EQ(1, result.getNumberOfModules()); diff --git a/test/functional/utility/GraphTest.cpp b/test/functional/utility/GraphTest.cpp index 8f88c696a..33c31ac5b 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(); From b14f866e01533099631bfc63622c9585952c6309 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 9 Aug 2016 22:06:59 +0200 Subject: [PATCH 2/2] added more flatten tests Former-commit-id: 7e35a90c884ff7f68930b4e3aabe1d121dfb772f --- test/functional/storage/PrismProgramTest.cpp | 42 +++++++++++++++----- 1 file changed, 33 insertions(+), 9 deletions(-) diff --git a/test/functional/storage/PrismProgramTest.cpp b/test/functional/storage/PrismProgramTest.cpp index b6a5d1264..e8ea63c98 100644 --- a/test/functional/storage/PrismProgramTest.cpp +++ b/test/functional/storage/PrismProgramTest.cpp @@ -8,20 +8,44 @@ #ifdef STORM_HAVE_MSAT 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")); + storm::prism::Program program; + ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/leader3.nm")); std::shared_ptr smtSolverFactory = std::make_shared(); - ASSERT_NO_THROW(result = result.flattenModules(smtSolverFactory)); - EXPECT_EQ(1, result.getNumberOfModules()); - EXPECT_EQ(74, result.getModule(0).getNumberOfCommands()); + ASSERT_NO_THROW(program = program.flattenModules(smtSolverFactory)); + EXPECT_EQ(1, program.getNumberOfModules()); + EXPECT_EQ(74, program.getModule(0).getNumberOfCommands()); - ASSERT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/wlan0_collide.nm")); + ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/wlan0_collide.nm")); - ASSERT_NO_THROW(result = result.flattenModules(smtSolverFactory)); - EXPECT_EQ(1, result.getNumberOfModules()); - EXPECT_EQ(180, result.getModule(0).getNumberOfCommands()); + ASSERT_NO_THROW(program = program.flattenModules(smtSolverFactory)); + EXPECT_EQ(1, program.getNumberOfModules()); + EXPECT_EQ(180, program.getModule(0).getNumberOfCommands()); + + ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/csma2_2.nm")); + + ASSERT_NO_THROW(program = program.flattenModules(smtSolverFactory)); + EXPECT_EQ(1, program.getNumberOfModules()); + EXPECT_EQ(71, program.getModule(0).getNumberOfCommands()); + + ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/firewire.nm")); + + ASSERT_NO_THROW(program = program.flattenModules(smtSolverFactory)); + EXPECT_EQ(1, program.getNumberOfModules()); + EXPECT_EQ(5026, program.getModule(0).getNumberOfCommands()); + + ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/coin2.nm")); + + ASSERT_NO_THROW(program = program.flattenModules(smtSolverFactory)); + EXPECT_EQ(1, program.getNumberOfModules()); + EXPECT_EQ(13, program.getModule(0).getNumberOfCommands()); + + ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/two_dice.nm")); + + ASSERT_NO_THROW(program = program.flattenModules(smtSolverFactory)); + EXPECT_EQ(1, program.getNumberOfModules()); + EXPECT_EQ(16, program.getModule(0).getNumberOfCommands()); } #endif