Browse Source

And more includes on the right spot.

Former-commit-id: 72bb348687
tempestpy_adaptions
sjunges 9 years ago
parent
commit
5e428a795a
  1. 1
      src/counterexamples/MILPMinimalLabelSetGenerator.h
  2. 1
      src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp
  3. 1
      src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp
  4. 8
      src/utility/solver.cpp
  5. 25
      src/utility/solver.h
  6. 2
      test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp
  7. 1
      test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp
  8. 2
      test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp
  9. 2
      test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp
  10. 4
      test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp
  11. 2
      test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
  12. 2
      test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp
  13. 2
      test/functional/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp
  14. 2
      test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp
  15. 2
      test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp
  16. 2
      test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp
  17. 2
      test/functional/modelchecker/NativeMdpPrctlModelCheckerTest.cpp
  18. 2
      test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp
  19. 1
      test/functional/solver/FullySymbolicGameSolverTest.cpp
  20. 1
      test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp
  21. 1
      test/performance/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
  22. 2
      test/performance/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp
  23. 2
      test/performance/modelchecker/NativeMdpPrctlModelCheckerTest.cpp

1
src/counterexamples/MILPMinimalLabelSetGenerator.h

@ -17,6 +17,7 @@
#include "src/utility/graph.h"
#include "src/utility/counterexamples.h"
#include "src/utility/solver.h"
#include "src/solver/LpSolver.h"
#include "src/settings/SettingsManager.h"
#include "src/settings/modules/GeneralSettings.h"

1
src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp

@ -10,6 +10,7 @@
#include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h"
#include "src/modelchecker/results/HybridQuantitativeCheckResult.h"
#include "src/solver/MinMaxLinearEquationSolver.h"
#include "src/settings/modules/GeneralSettings.h"

1
src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp

@ -10,6 +10,7 @@
#include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h"
#include "src/modelchecker/results/HybridQuantitativeCheckResult.h"
#include "src/solver/SymbolicLinearEquationSolver.h"
#include "src/settings/modules/GeneralSettings.h"

8
src/utility/solver.cpp

@ -1,9 +1,9 @@
#include "src/utility/solver.h"
#include "src/settings/SettingsManager.h"
#include "src/solver/SymbolicGameSolver.h"
#include "src/solver/SymbolicLinearEquationSolver.h"
#include "src/solver/NativeLinearEquationSolver.h"
#include "src/solver/GmmxxLinearEquationSolver.h"
@ -16,6 +16,10 @@
#include "src/settings/SettingsManager.h"
#include "src/settings/modules/GeneralSettings.h"
#include "src/settings/modules/NativeEquationSolverSettings.h"
#include "src/exceptions/InvalidSettingsException.h"
namespace storm {
namespace utility {

25
src/utility/solver.h

@ -1,20 +1,25 @@
#ifndef STORM_UTILITY_SOLVER_H_
#define STORM_UTILITY_SOLVER_H_
#include "src/solver/SymbolicGameSolver.h"
#include "src/solver/SymbolicLinearEquationSolver.h"
#include "src/solver/LinearEquationSolver.h"
#include "src/solver/NativeLinearEquationSolver.h"
#include "src/solver/MinMaxLinearEquationSolver.h"
#include "src/solver/LpSolver.h"
#include "src/storage/dd/DdType.h"
#include "src/settings/modules/NativeEquationSolverSettings.h"
#include "src/exceptions/InvalidSettingsException.h"
namespace storm {
namespace solver {
template<storm::dd::DdType T> class SymbolicGameSolver;
template<storm::dd::DdType T, typename V> class SymbolicLinearEquationSolver;
template<typename V> class LinearEquationSolver;
template<typename V> class MinMaxLinearEquationSolver;
class LpSolver;
}
namespace dd {
template<storm::dd::DdType T> class Add;
template<storm::dd::DdType T> class Bdd;
}
namespace expressions {
class Variable;
}
namespace utility {
namespace solver {
template<storm::dd::DdType Type, typename ValueType>

2
test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp

@ -12,6 +12,8 @@
#include "src/settings/SettingsManager.h"
#include "src/settings/modules/GeneralSettings.h"
#include "src/settings/modules/NativeEquationSolverSettings.h"
#include "src/settings/modules/GmmxxEquationSolverSettings.h"
TEST(GmmxxCtmcCslModelCheckerTest, Cluster) {

1
test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp

@ -8,6 +8,7 @@
#include "src/settings/SettingsManager.h"
#include "src/settings/modules/GeneralSettings.h"
#include "src/settings/modules/GmmxxEquationSolverSettings.h"
#include "src/settings/modules/NativeEquationSolverSettings.h"
#include "src/settings/SettingMemento.h"
#include "src/parser/AutoParser.h"

2
test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp

@ -17,6 +17,8 @@
#include "src/settings/modules/GeneralSettings.h"
#include "src/settings/modules/GmmxxEquationSolverSettings.h"
#include "src/settings/modules/NativeEquationSolverSettings.h"
TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster) {
// Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableGeneralSettings().overridePrismCompatibilityMode(true);

2
test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp

@ -14,6 +14,8 @@
#include "src/settings/modules/GeneralSettings.h"
#include "src/settings/modules/GmmxxEquationSolverSettings.h"
#include "src/settings/modules/NativeEquationSolverSettings.h"
TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Die) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");

4
test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp

@ -10,10 +10,10 @@
#include "src/parser/PrismParser.h"
#include "src/builder/DdPrismModelBuilder.h"
#include "src/models/symbolic/Dtmc.h"
#include "src/settings/SettingsManager.h"
#include "src/settings/SettingsManager.h"
#include "src/settings/modules/GeneralSettings.h"
#include "src/settings/modules/NativeEquationSolverSettings.h"
#include "src/settings/modules/GmmxxEquationSolverSettings.h"
TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice) {

2
test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp

@ -9,6 +9,8 @@
#include "src/settings/modules/GeneralSettings.h"
#include "src/settings/modules/GmmxxEquationSolverSettings.h"
#include "src/settings/modules/NativeEquationSolverSettings.h"
#include "src/parser/AutoParser.h"
TEST(GmmxxMdpPrctlModelCheckerTest, Dice) {

2
test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp

@ -14,6 +14,8 @@
#include "src/settings/modules/GeneralSettings.h"
#include "src/settings/modules/NativeEquationSolverSettings.h"
TEST(SparseCtmcCslModelCheckerTest, Cluster) {
// Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableGeneralSettings().overridePrismCompatibilityMode(true);

2
test/functional/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp

@ -9,6 +9,8 @@
#include "src/settings/SettingsManager.h"
#include "src/settings/modules/GeneralSettings.h"
#include "src/settings/modules/NativeEquationSolverSettings.h"
#include "src/settings/SettingMemento.h"
#include "src/parser/AutoParser.h"

2
test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp

@ -16,6 +16,8 @@
#include "src/settings/SettingsManager.h"
#include "src/settings/modules/GeneralSettings.h"
#include "src/settings/modules/NativeEquationSolverSettings.h"
TEST(NativeHybridCtmcCslModelCheckerTest, Cluster) {
// Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableGeneralSettings().overridePrismCompatibilityMode(true);

2
test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp

@ -15,6 +15,8 @@
#include "src/settings/modules/GmmxxEquationSolverSettings.h"
#include "src/settings/modules/NativeEquationSolverSettings.h"
TEST(NativeHybridDtmcPrctlModelCheckerTest, Die) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");

2
test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp

@ -14,6 +14,8 @@
#include "src/settings/modules/GeneralSettings.h"
#include "src/settings/modules/NativeEquationSolverSettings.h"
TEST(NativeHybridMdpPrctlModelCheckerTest, Dice) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");

2
test/functional/modelchecker/NativeMdpPrctlModelCheckerTest.cpp

@ -8,6 +8,8 @@
#include "src/settings/SettingsManager.h"
#include "src/settings/modules/GeneralSettings.h"
#include "src/settings/modules/NativeEquationSolverSettings.h"
#include "src/parser/AutoParser.h"
TEST(SparseMdpPrctlModelCheckerTest, Dice) {

2
test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp

@ -11,6 +11,8 @@
#include "src/models/symbolic/Dtmc.h"
#include "src/settings/SettingsManager.h"
#include "src/settings/modules/NativeEquationSolverSettings.h"
#include "src/settings/modules/GeneralSettings.h"
TEST(SymbolicDtmcPrctlModelCheckerTest, Die) {

1
test/functional/solver/FullySymbolicGameSolverTest.cpp

@ -7,6 +7,7 @@
#include "src/utility/solver.h"
#include "src/settings/SettingsManager.h"
#include "src/solver/SymbolicGameSolver.h"
#include "src/settings/modules/NativeEquationSolverSettings.h"

1
test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp

@ -2,6 +2,7 @@
#include "storm-config.h"
#include "src/settings/SettingsManager.h"
#include "src/settings/modules/GmmxxEquationSolverSettings.h"
#include "src/settings/modules/NativeEquationSolverSettings.h"
#include "src/settings/SettingMemento.h"
#include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"

1
test/performance/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp

@ -2,6 +2,7 @@
#include "storm-config.h"
#include "src/settings/SettingsManager.h"
#include "src/settings/modules/NativeEquationSolverSettings.h"
#include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "src/utility/solver.h"

2
test/performance/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp

@ -2,6 +2,8 @@
#include "storm-config.h"
#include "src/settings/SettingsManager.h"
#include "src/settings/modules/GmmxxEquationSolverSettings.h"
#include "src/settings/modules/NativeEquationSolverSettings.h"
#include "src/settings/SettingMemento.h"
#include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"

2
test/performance/modelchecker/NativeMdpPrctlModelCheckerTest.cpp

@ -4,6 +4,8 @@
#include "src/settings/SettingsManager.h"
#include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "src/settings/modules/NativeEquationSolverSettings.h"
#include "src/utility/solver.h"
#include "src/parser/AutoParser.h"

Loading…
Cancel
Save