dehnert
11 years ago
73 changed files with 832 additions and 487 deletions
-
1src/counterexamples/MILPMinimalLabelSetGenerator.h
-
6src/modelchecker/AbstractModelChecker.cpp
-
6src/modelchecker/csl/helper/HybridCtmcCslHelper.cpp
-
8src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp
-
1src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
-
9src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp
-
1src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp
-
2src/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp
-
5src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
-
2src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
-
20src/settings/modules/GeneralSettings.cpp
-
20src/settings/modules/GeneralSettings.h
-
3src/settings/modules/GlpkSettings.cpp
-
3src/settings/modules/GmmxxEquationSolverSettings.cpp
-
4src/settings/modules/GurobiSettings.cpp
-
4src/settings/modules/NativeEquationSolverSettings.cpp
-
3src/settings/modules/TopologicalValueIterationEquationSolverSettings.cpp
-
55src/solver/GmmxxMinMaxLinearEquationSolver.cpp
-
18src/solver/GmmxxMinMaxLinearEquationSolver.h
-
5src/solver/LinearEquationSolver.h
-
27src/solver/MinMaxLinearEquationSolver.cpp
-
53src/solver/MinMaxLinearEquationSolver.h
-
72src/solver/NativeMinMaxLinearEquationSolver.cpp
-
19src/solver/NativeMinMaxLinearEquationSolver.h
-
32src/solver/SolverSelectionOptions.cpp
-
20src/solver/SolverSelectionOptions.h
-
19src/solver/TopologicalMinMaxLinearEquationSolver.cpp
-
4src/solver/TopologicalMinMaxLinearEquationSolver.h
-
5src/storage/BitVector.cpp
-
5src/storage/BitVector.h
-
16src/storage/SparseMatrix.cpp
-
12src/storage/SparseMatrix.h
-
15src/storage/prism/Assignment.cpp
-
7src/storage/prism/Assignment.h
-
16src/storage/prism/Command.cpp
-
8src/storage/prism/Command.h
-
12src/storage/prism/Program.cpp
-
11src/storage/prism/Update.cpp
-
6src/storage/prism/Update.h
-
53src/utility/ConstantsComparator.cpp
-
5src/utility/ConstantsComparator.h
-
28src/utility/ExtendSettingEnumWithSelectionField.h
-
2src/utility/cli.cpp
-
63src/utility/constants.cpp
-
9src/utility/constants.h
-
28src/utility/solver.cpp
-
23src/utility/solver.h
-
36src/utility/vector.h
-
2test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp
-
103test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp
-
2test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp
-
63test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp
-
3test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp
-
2test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
-
2test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp
-
98test/functional/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp
-
2test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp
-
63test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp
-
2test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp
-
2test/functional/modelchecker/NativeMdpPrctlModelCheckerTest.cpp
-
77test/functional/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp
-
63test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp
-
2test/functional/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp
-
1test/functional/solver/FullySymbolicGameSolverTest.cpp
-
2test/functional/solver/GmmxxMinMaxLinearEquationSolverTest.cpp
-
11test/functional/solver/MinMaxTechniqueSelectionTest.cpp
-
2test/functional/solver/NativeMinMaxLinearEquationSolverTest.cpp
-
15test/functional/storage/BitVectorTest.cpp
-
14test/functional/utility/VectorTest.cpp
-
1test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp
-
1test/performance/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
-
2test/performance/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp
-
2test/performance/modelchecker/NativeMdpPrctlModelCheckerTest.cpp
@ -0,0 +1,27 @@ |
|||
#include "MinMaxLinearEquationSolver.h"
|
|||
#include "src/settings/SettingsManager.h"
|
|||
#include "src/settings/modules/GeneralSettings.h"
|
|||
|
|||
#include "src/utility/macros.h"
|
|||
#include "src/exceptions/NotImplementedException.h"
|
|||
#include <cstdint>
|
|||
|
|||
namespace storm { |
|||
namespace solver { |
|||
AbstractMinMaxLinearEquationSolver::AbstractMinMaxLinearEquationSolver(double precision, bool relativeError, uint_fast64_t maximalIterations, bool trackPolicy, MinMaxTechniqueSelection prefTech) : |
|||
precision(precision), relative(relativeError), maximalNumberOfIterations(maximalIterations), trackPolicy(trackPolicy) |
|||
{ |
|||
|
|||
if(prefTech == MinMaxTechniqueSelection::FROMSETTINGS) { |
|||
useValueIteration = (storm::settings::generalSettings().getMinMaxEquationSolvingTechnique() == storm::solver::MinMaxTechnique::ValueIteration); |
|||
} else { |
|||
useValueIteration = (prefTech == MinMaxTechniqueSelection::ValueIteration); |
|||
} |
|||
} |
|||
|
|||
std::vector<storm::storage::sparse::state_type> AbstractMinMaxLinearEquationSolver::getPolicy() const { |
|||
STORM_LOG_THROW(!useValueIteration, storm::exceptions::NotImplementedException, "Getting policies after value iteration is not yet supported!"); |
|||
return policy; |
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,32 @@ |
|||
#include "src/solver/SolverSelectionOptions.h"
|
|||
|
|||
namespace storm { |
|||
namespace solver { |
|||
std::string toString(MinMaxTechnique m) { |
|||
switch(m) { |
|||
case MinMaxTechnique::PolicyIteration: |
|||
return "policy"; |
|||
case MinMaxTechnique::ValueIteration: |
|||
return "value"; |
|||
} |
|||
|
|||
} |
|||
std::string toString(LpSolverType t) { |
|||
switch(t) { |
|||
case LpSolverType::Gurobi: |
|||
return "Gurobi"; |
|||
case LpSolverType::Glpk: |
|||
return "Glpk"; |
|||
} |
|||
} |
|||
|
|||
std::string toString(EquationSolverType t) { |
|||
switch(t) { |
|||
case EquationSolverType::Native: |
|||
return "Native"; |
|||
case EquationSolverType::Gmmxx: |
|||
return "Gmmxx"; |
|||
} |
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,20 @@ |
|||
|
|||
#ifndef SOLVERSELECTIONOPTIONS_H |
|||
#define SOLVERSELECTIONOPTIONS_H |
|||
|
|||
|
|||
#include "src/utility/ExtendSettingEnumWithSelectionField.h" |
|||
|
|||
namespace storm { |
|||
namespace solver { |
|||
ExtendEnumsWithSelectionField(MinMaxTechnique, PolicyIteration, ValueIteration) |
|||
|
|||
|
|||
ExtendEnumsWithSelectionField(LpSolverType, Gurobi, Glpk) |
|||
ExtendEnumsWithSelectionField(EquationSolverType, Native, Gmmxx) |
|||
|
|||
} |
|||
} |
|||
|
|||
#endif |
|||
|
|||
@ -0,0 +1,28 @@ |
|||
#ifndef EXTENDSETTINGENUMWITHSELECTIONFIELD_H |
|||
#define EXTENDSETTINGENUMWITHSELECTIONFIELD_H |
|||
|
|||
|
|||
|
|||
#include <string> |
|||
#include <cassert> |
|||
|
|||
|
|||
#define ExtendEnumsWithSelectionField( NAME, ...) \ |
|||
enum class NAME : int { __VA_ARGS__ }; \ |
|||
enum class NAME##Selection : int { __VA_ARGS__, FROMSETTINGS }; \ |
|||
std::string toString(NAME); \ |
|||
inline NAME convert(NAME##Selection e) { \ |
|||
assert(e != NAME##Selection::FROMSETTINGS); \ |
|||
return static_cast< NAME >(e); \ |
|||
} \ |
|||
inline std::string toString(NAME##Selection e) { \ |
|||
if(e == NAME##Selection::FROMSETTINGS) { \ |
|||
return "[from settings]"; \ |
|||
}\ |
|||
else { \ |
|||
return toString(convert(e)); \ |
|||
} \ |
|||
} |
|||
|
|||
#endif /* EXTENDSETTINGENUMWITHSELECTIONFIELD_H */ |
|||
|
|||
@ -0,0 +1,11 @@ |
|||
#include "gtest/gtest.h"
|
|||
|
|||
#include "src/solver/MinMaxLinearEquationSolver.h"
|
|||
|
|||
TEST( MinMaxTechnique, Simple ) { |
|||
storm::solver::MinMaxTechniqueSelection ts = storm::solver::MinMaxTechniqueSelection::PolicyIteration; |
|||
storm::solver::MinMaxTechnique t = storm::solver::MinMaxTechnique::PolicyIteration; |
|||
ASSERT_EQ(convert(ts), t); |
|||
|
|||
|
|||
} |
|||
@ -0,0 +1,14 @@ |
|||
#include "gtest/gtest.h"
|
|||
#include "storm-config.h"
|
|||
#include "src/storage/BitVector.h"
|
|||
#include "src/utility/vector.h"
|
|||
|
|||
TEST(VectorTest, sum_if) { |
|||
std::vector<double> a = {1.0, 2.0, 4.0, 8.0, 16.0}; |
|||
storm::storage::BitVector f1(5, {2,4}); |
|||
storm::storage::BitVector f2(5, {3,4}); |
|||
|
|||
ASSERT_EQ(20.0, storm::utility::vector::sum_if(a, f1)); |
|||
ASSERT_EQ(24.0, storm::utility::vector::sum_if(a, f2)); |
|||
|
|||
} |
|||
Write
Preview
Loading…
Cancel
Save
Reference in new issue