Browse Source

some fixes to tests

tempestpy_adaptions
dehnert 8 years ago
parent
commit
2a88016469
  1. 14
      src/test/modelchecker/GameBasedDtmcModelCheckerTest.cpp
  2. 6
      src/test/storage/PrismProgramTest.cpp
  3. 14
      src/test/storage/SylvanDdTest.cpp

14
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;

6
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<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
@ -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<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::Z3SmtSolverFactory>();

14
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<storm::dd::DdManager<storm::dd::DdType::Sylvan>> ddManager(new storm::dd::DdManager<storm::dd::DdType::Sylvan>());
@ -1069,5 +1059,3 @@ TEST(SylvanDd, BddToExpressionTest) {
auto result = bdd.toExpression(*manager);
}
=======
>>>>>>> master:src/test/storage/SylvanDdTest.cpp
Loading…
Cancel
Save