Browse Source

better subenvironments

tempestpy_adaptions
TimQu 7 years ago
parent
commit
42cea9c688
  1. 2
      src/storm/api/counterexamples.cpp
  2. 14
      src/storm/environment/Environment.cpp
  3. 9
      src/storm/environment/Environment.h
  4. 38
      src/storm/environment/SubEnvironment.h
  5. 6
      src/storm/environment/environments.h
  6. 2
      src/storm/environment/solver/MinMaxSolverEnvironment.h
  7. 22
      src/storm/environment/solver/SolverEnvironment.cpp
  8. 6
      src/storm/environment/solver/SolverEnvironment.h
  9. 2
      src/storm/modelchecker/AbstractModelChecker.cpp
  10. 2
      src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp
  11. 2
      src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
  12. 2
      src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp
  13. 2
      src/storm/solver/LpMinMaxLinearEquationSolver.cpp
  14. 2
      src/storm/solver/MinMaxLinearEquationSolver.cpp
  15. 2
      src/storm/solver/StandardMinMaxLinearEquationSolver.cpp
  16. 2
      src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp
  17. 2
      src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp

2
src/storm/api/counterexamples.cpp

@ -1,6 +1,6 @@
#include "storm/api/counterexamples.h"
#include "storm/environment/environments.h"
#include "storm/environment/Environment.h"
namespace storm {
namespace api {

14
src/storm/environment/Environment.cpp

@ -1,28 +1,22 @@
#include "storm/environment/Environment.h"
#include "storm/environment/SubEnvironment.h"
#include "storm/environment/solver/SolverEnvironment.h"
#include "storm/environment/solver/MinMaxSolverEnvironment.h"
namespace storm {
Environment::Environment() : solverEnvironment(std::make_unique<SolverEnvironment>()) {
Environment::Environment() {
// Intentionally left empty.
}
Environment::Environment(Environment const& other) :
solverEnvironment(new SolverEnvironment(*other.solverEnvironment)) {
// Intentionally left empty.
}
Environment::~Environment() {
// Intentionally left empty.
}
SolverEnvironment& Environment::solver() {
return *solverEnvironment;
return solverEnvironment.get();
}
SolverEnvironment const& Environment::solver() const {
return *solverEnvironment;
return solverEnvironment.get();
}
}

9
src/storm/environment/Environment.h

@ -1,10 +1,9 @@
#pragma once
#include<memory>
#include "storm/environment/SubEnvironment.h"
namespace storm {
// Forward declare sub-environments
class SolverEnvironment;
@ -12,8 +11,6 @@ namespace storm {
public:
Environment();
Environment(Environment const& other);
virtual ~Environment();
SolverEnvironment& solver();
@ -21,9 +18,7 @@ namespace storm {
private:
std::unique_ptr<SolverEnvironment> solverEnvironment;
SubEnvironment<SolverEnvironment> solverEnvironment;
};
}

38
src/storm/environment/SubEnvironment.h

@ -0,0 +1,38 @@
#pragma once
#include<memory>
namespace storm {
template<typename EnvironmentType>
class SubEnvironment {
public:
SubEnvironment() : subEnv(std::make_unique<EnvironmentType>()) {
// Intentionally left empty
}
SubEnvironment(SubEnvironment const& other) : subEnv(new EnvironmentType(*other.subEnv)) {
// Intentionally left empty
}
SubEnvironment<EnvironmentType>& operator=(SubEnvironment const& other) {
subEnv = std::make_unique<EnvironmentType>(*other.subEnv);
return *this;
}
EnvironmentType const& get() const {
return *subEnv;
}
EnvironmentType& get() {
return *subEnv;
}
private:
std::unique_ptr<EnvironmentType> subEnv;
};
}

6
src/storm/environment/environments.h

@ -1,6 +0,0 @@
#pragma once
#include "storm/environment/Environment.h"
//#include "storm/environment/solver/SolverEnvironment.h"
//#include "storm/environment/solver/MinMaxSolverEnvironment.h"

2
src/storm/environment/solver/MinMaxSolverEnvironment.h

@ -1,5 +1,7 @@
#pragma once
#include "storm/environment/solver/SolverEnvironment.h"
#include "storm/adapters/RationalNumberAdapter.h"
#include "storm/solver/SolverSelectionOptions.h"
#include "storm/solver/MultiplicationStyle.h"

22
src/storm/environment/solver/SolverEnvironment.cpp

@ -1,19 +1,13 @@
#include "storm/environment/solver/SolverEnvironment.h"
#include "storm/environment/solver/MinMaxSolverEnvironment.h"
#include "storm/settings/SettingsManager.h"
#include "storm/settings/modules/GeneralSettings.h"
namespace storm {
SolverEnvironment::SolverEnvironment() :
// eigenSolverEnvironment(std::make_unique<EigenSolverEnvironment>()),
// gmmxxSolverEnvironment(std::make_unique<GmmxxSolverEnvironment>()),
minMaxSolverEnvironment(std::make_unique<MinMaxSolverEnvironment>()) //,
// nativeSolverEnvironment(std::make_unique<NativeSolverEnvironment>()) {
{ }
SolverEnvironment::SolverEnvironment(SolverEnvironment const& other) :
minMaxSolverEnvironment(new MinMaxSolverEnvironment(*other.minMaxSolverEnvironment)),
forceSoundness(other.forceSoundness) {
// Intentionally left empty
SolverEnvironment::SolverEnvironment() {
forceSoundness = storm::settings::getModule<storm::settings::modules::GeneralSettings>().isSoundSet();
}
SolverEnvironment::~SolverEnvironment() {
@ -21,11 +15,11 @@ namespace storm {
}
MinMaxSolverEnvironment& SolverEnvironment::minMax() {
return *minMaxSolverEnvironment;
return minMaxSolverEnvironment.get();
}
MinMaxSolverEnvironment const& SolverEnvironment::minMax() const{
return *minMaxSolverEnvironment;
MinMaxSolverEnvironment const& SolverEnvironment::minMax() const {
return minMaxSolverEnvironment.get();
}
bool SolverEnvironment::isForceSoundness() const {

6
src/storm/environment/solver/SolverEnvironment.h

@ -2,6 +2,9 @@
#include<memory>
#include "storm/environment/Environment.h"
#include "storm/environment/SubEnvironment.h"
namespace storm {
// Forward declare subenvironments
@ -14,7 +17,6 @@ namespace storm {
public:
SolverEnvironment();
SolverEnvironment(SolverEnvironment const& other);
~SolverEnvironment();
// EigenSolverEnvironment& eigen();
@ -32,7 +34,7 @@ namespace storm {
private:
// std::unique_ptr<EigenSolverEnvironment> eigenSolverEnvironment;
// std::unique_ptr<GmmxxSolverEnvironment> gmmxxSolverEnvironment;
std::unique_ptr<MinMaxSolverEnvironment> minMaxSolverEnvironment;
SubEnvironment<MinMaxSolverEnvironment> minMaxSolverEnvironment;
// std::unique_ptr<NativeSolverEnvironment> nativeSolverEnvironment;
bool forceSoundness;

2
src/storm/modelchecker/AbstractModelChecker.cpp

@ -9,7 +9,7 @@
#include "storm/exceptions/InvalidArgumentException.h"
#include "storm/exceptions/InternalTypeErrorException.h"
#include "storm/environment/environments.h"
#include "storm/environment/Environment.h"
#include "storm/models/sparse/Dtmc.h"
#include "storm/models/sparse/Ctmc.h"

2
src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp

@ -10,8 +10,6 @@
#include "storm/solver/MinMaxLinearEquationSolver.h"
#include "storm/solver/LinearEquationSolver.h"
#include "storm/environment/Environment.h"
#include "storm/environment/solver/SolverEnvironment.h"
#include "storm/environment/solver/MinMaxSolverEnvironment.h"
#include "storm/settings/SettingsManager.h"

2
src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp

@ -33,8 +33,6 @@
#include "storm/utility/ProgressMeasurement.h"
#include "storm/utility/export.h"
#include "storm/environment/Environment.h"
#include "storm/environment/solver/SolverEnvironment.h"
#include "storm/environment/solver/MinMaxSolverEnvironment.h"
#include "storm/exceptions/InvalidStateException.h"

2
src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp

@ -2,8 +2,6 @@
#include "storm/utility/ConstantsComparator.h"
#include "storm/environment/Environment.h"
#include "storm/environment/solver/SolverEnvironment.h"
#include "storm/environment/solver/MinMaxSolverEnvironment.h"
#include "storm/utility/KwekMehlhorn.h"

2
src/storm/solver/LpMinMaxLinearEquationSolver.cpp

@ -1,7 +1,5 @@
#include "storm/solver/LpMinMaxLinearEquationSolver.h"
#include "storm/environment/Environment.h"
#include "storm/environment/solver/SolverEnvironment.h"
#include "storm/environment/solver/MinMaxSolverEnvironment.h"
#include "storm/utility/vector.h"
#include "storm/utility/macros.h"

2
src/storm/solver/MinMaxLinearEquationSolver.cpp

@ -7,8 +7,6 @@
#include "storm/solver/TopologicalMinMaxLinearEquationSolver.h"
#include "storm/solver/LpMinMaxLinearEquationSolver.h"
#include "storm/environment/Environment.h"
#include "storm/environment/solver/SolverEnvironment.h"
#include "storm/environment/solver/MinMaxSolverEnvironment.h"
#include "storm/utility/macros.h"

2
src/storm/solver/StandardMinMaxLinearEquationSolver.cpp

@ -6,8 +6,6 @@
#include "storm/solver/NativeLinearEquationSolver.h"
#include "storm/solver/EliminationLinearEquationSolver.h"
#include "storm/environment/Environment.h"
#include "storm/environment/solver/SolverEnvironment.h"
#include "storm/environment/solver/MinMaxSolverEnvironment.h"
#include "storm/utility/vector.h"

2
src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp

@ -7,8 +7,6 @@
#include "storm/utility/constants.h"
#include "storm/environment/Environment.h"
#include "storm/environment/solver/SolverEnvironment.h"
#include "storm/environment/solver/MinMaxSolverEnvironment.h"
#include "storm/utility/dd.h"

2
src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp

@ -7,8 +7,6 @@
#include "storm/exceptions/InvalidStateException.h"
#include "storm/exceptions/InvalidEnvironmentException.h"
#include "storm/environment/Environment.h"
#include "storm/environment/solver/SolverEnvironment.h"
#include "storm/environment/solver/MinMaxSolverEnvironment.h"
#include "storm/settings/SettingsManager.h"

Loading…
Cancel
Save