From 2a880164691140b7f95151ef656f9782cc42f949 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 21 Nov 2016 22:13:34 +0100 Subject: [PATCH] some fixes to tests --- .../modelchecker/GameBasedDtmcModelCheckerTest.cpp | 14 +++++++------- src/test/storage/PrismProgramTest.cpp | 6 +++--- src/test/storage/SylvanDdTest.cpp | 14 +------------- 3 files changed, 11 insertions(+), 23 deletions(-) diff --git a/src/test/modelchecker/GameBasedDtmcModelCheckerTest.cpp b/src/test/modelchecker/GameBasedDtmcModelCheckerTest.cpp index c7589eb3e..546f8fe09 100644 --- a/src/test/modelchecker/GameBasedDtmcModelCheckerTest.cpp +++ b/src/test/modelchecker/GameBasedDtmcModelCheckerTest.cpp @@ -8,7 +8,7 @@ #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "storm/parser/PrismParser.h" -#include "storm/builder/DdPrismModelBuilder.h" +#include "storm/dtmc/DdPrismModelBuilder.h" #include "storm/models/symbolic/StandardRewardModel.h" #include "storm/models/symbolic/Dtmc.h" #include "storm/settings/SettingsManager.h" @@ -18,7 +18,7 @@ #include "storm/settings/modules/GeneralSettings.h" TEST(GameBasedDtmcModelCheckerTest, Die_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"); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -67,7 +67,7 @@ TEST(GameBasedDtmcModelCheckerTest, Die_Cudd) { } TEST(GameBasedDtmcModelCheckerTest, Die_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"); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -116,7 +116,7 @@ TEST(GameBasedDtmcModelCheckerTest, Die_Sylvan) { } TEST(GameBasedDtmcModelCheckerTest, Crowds_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"); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -159,7 +159,7 @@ TEST(GameBasedDtmcModelCheckerTest, Crowds_Cudd) { } TEST(GameBasedDtmcModelCheckerTest, Crowds_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"); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -205,7 +205,7 @@ TEST(GameBasedDtmcModelCheckerTest, Crowds_Sylvan) { } TEST(GameBasedDtmcModelCheckerTest, SynchronousLeader_Cudd) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/leader-3-5.pm"); + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/leader-3-5.pm"); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -245,7 +245,7 @@ TEST(GameBasedDtmcModelCheckerTest, SynchronousLeader_Cudd) { } TEST(GameBasedDtmcModelCheckerTest, SynchronousLeader_Sylvan) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/builder/leader-3-5.pm"); + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/leader-3-5.pm"); // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; diff --git a/src/test/storage/PrismProgramTest.cpp b/src/test/storage/PrismProgramTest.cpp index b5df85050..ba4beb5bf 100644 --- a/src/test/storage/PrismProgramTest.cpp +++ b/src/test/storage/PrismProgramTest.cpp @@ -8,8 +8,8 @@ #ifdef STORM_HAVE_MSAT TEST(PrismProgramTest, FlattenModules) { - storm::prism::Program result; - ASSERT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/leader3.nm")); + storm::prism::Program program; + ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/leader3.nm")); std::shared_ptr smtSolverFactory = std::make_shared(); @@ -77,7 +77,7 @@ TEST(PrismProgramTest, FlattenModules_Dice_Mathsat) { #ifdef STORM_HAVE_Z3 TEST(PrismProgramTest, FlattenModules_Leader_Z3) { storm::prism::Program program; - ASSERT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/leader3.nm")); + ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/leader3.nm")); std::shared_ptr smtSolverFactory = std::make_shared(); diff --git a/src/test/storage/SylvanDdTest.cpp b/src/test/storage/SylvanDdTest.cpp index 6ce20bf41..f32f3be1a 100644 --- a/src/test/storage/SylvanDdTest.cpp +++ b/src/test/storage/SylvanDdTest.cpp @@ -1,22 +1,13 @@ #include "gtest/gtest.h" #include "storm-config.h" -<<<<<<< HEAD:test/functional/storage/SylvanDdTest.cpp -#include "src/adapters/CarlAdapter.h" -#include "src/exceptions/InvalidArgumentException.h" -#include "src/storage/dd/DdManager.h" -#include "src/storage/dd/Add.h" -#include "src/storage/dd/Odd.h" -#include "src/storage/dd/DdMetaVariable.h" -#include "src/settings/SettingsManager.h" -======= +#include "storm/adapters/CarlAdapter.h" #include "storm/exceptions/InvalidArgumentException.h" #include "storm/storage/dd/DdManager.h" #include "storm/storage/dd/Add.h" #include "storm/storage/dd/Odd.h" #include "storm/storage/dd/DdMetaVariable.h" #include "storm/settings/SettingsManager.h" ->>>>>>> master:src/test/storage/SylvanDdTest.cpp #include "storm/storage/SparseMatrix.h" @@ -1052,7 +1043,6 @@ TEST(SylvanDd, BddOddTest) { EXPECT_EQ(9ul, matrix.getColumnCount()); EXPECT_EQ(106ul, matrix.getNonzeroEntryCount()); } -<<<<<<< HEAD:test/functional/storage/SylvanDdTest.cpp TEST(SylvanDd, BddToExpressionTest) { std::shared_ptr> ddManager(new storm::dd::DdManager()); @@ -1069,5 +1059,3 @@ TEST(SylvanDd, BddToExpressionTest) { auto result = bdd.toExpression(*manager); } -======= ->>>>>>> master:src/test/storage/SylvanDdTest.cpp