Browse Source

Merge branch 'master' of https://sselab.de/lab9/private/git/storm

Former-commit-id: 2a52b2a93f
main
dehnert 10 years ago
parent
commit
4e8538e282
  1. 12
      CMakeLists.txt
  2. 11
      src/cli/cli.cpp
  3. 29
      src/cli/cli.h
  4. 1
      src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp
  5. 9
      src/modelchecker/prctl/HybridMdpPrctlModelChecker.h
  6. 1
      src/modelchecker/propositional/SparsePropositionalModelChecker.h
  7. 10
      src/modelchecker/propositional/SymbolicPropositionalModelChecker.h
  8. 1
      src/models/ModelBase.h
  9. 1
      src/models/sparse/Dtmc.h
  10. 5
      src/models/sparse/Model.h
  11. 1
      src/models/symbolic/Model.cpp
  12. 54
      src/solver/AllowEarlyTerminationCondition.cpp
  13. 54
      src/solver/AllowEarlyTerminationCondition.h
  14. 4
      src/solver/GmmxxMinMaxLinearEquationSolver.cpp
  15. 4
      src/solver/MinMaxLinearEquationSolver.cpp
  16. 9
      src/solver/MinMaxLinearEquationSolver.h
  17. 4
      src/solver/NativeMinMaxLinearEquationSolver.cpp
  18. 3
      src/solver/SolverSelectionOptions.h
  19. 1
      src/storage/DeterministicModelBisimulationDecomposition.h
  20. 10
      src/storm.cpp
  21. 62
      src/utility/solver.cpp
  22. 34
      src/utility/solver.h
  23. 36
      src/utility/storm.h
  24. 5
      test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp
  25. 8
      test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
  26. 5
      test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp
  27. 18
      test/functional/modelchecker/NativeMdpPrctlModelCheckerTest.cpp
  28. 8
      test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp
  29. 29
      test/functional/solver/GmmxxMinMaxLinearEquationSolverTest.cpp
  30. 4
      test/performance/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
  31. 4
      test/performance/modelchecker/NativeMdpPrctlModelCheckerTest.cpp
  32. 4
      test/performance/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp

12
CMakeLists.txt

@ -371,10 +371,11 @@ endif()
#############################################################
file(GLOB_RECURSE STORM_HEADERS ${PROJECT_SOURCE_DIR}/src/*.h)
file(GLOB_RECURSE STORM_SOURCES_WITHOUT_MAIN ${PROJECT_SOURCE_DIR}/src/*/*.cpp)
file(GLOB_RECURSE STORM_SOURCES_CLI ${PROJECT_SOURCE_DIR}/src/cli/*.cpp)
file(GLOB_RECURSE STORM_MAIN_FILE ${PROJECT_SOURCE_DIR}/src/storm.cpp)
set(STORM_SOURCES "${STORM_SOURCES_WITHOUT_MAIN};${STORM_MAIN_FILE};")
file(GLOB_RECURSE STORM_ADAPTERS_FILES ${PROJECT_SOURCE_DIR}/src/adapters/*.h ${PROJECT_SOURCE_DIR}/src/adapters/*.cpp)
file(GLOB_RECURSE STORM_BUILDER_FILES ${PROJECT_SOURCE_DIR}/src/builder/*.h ${PROJECT_SOURCE_DIR}/src/builder/*.cpp)
file(GLOB_RECURSE STORM_CLI_FILES ${PROJECT_SOURCE_DIR}/src/cli/*.h ${PROJECT_SOURCE_DIR}/src/cli/*.cpp)
file(GLOB_RECURSE STORM_EXCEPTIONS_FILES ${PROJECT_SOURCE_DIR}/src/exceptions/*.h ${PROJECT_SOURCE_DIR}/src/exceptions/*.cpp)
file(GLOB_RECURSE STORM_LOGIC_FILES ${PROJECT_SOURCE_DIR}/src/logic/*.h ${PROJECT_SOURCE_DIR}/src/logic/*.cpp)
file(GLOB STORM_MODELCHECKER_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/*.cpp)
@ -410,10 +411,15 @@ file(GLOB_RECURSE STORM_PERFORMANCE_TEST_FILES ${STORM_CPP_TESTS_BASE_PATH}/perf
# Additional include files like the storm-config.h
file(GLOB_RECURSE STORM_BUILD_HEADERS ${PROJECT_BINARY_DIR}/include/*.h)
set(STORM_LIB_SOURCES ${STORM_SOURCES_WITHOUT_MAIN})
list(REMOVE_ITEM STORM_LIB_SOURCES ${STORM_SOURCES_CLI})
set(STORM_MAIN_SOURCES ${STORM_SOURCES_CLI} ${STORM_MAIN_FILE})
# Group the headers and sources
source_group(main FILES ${STORM_MAIN_FILE})
source_group(adapters FILES ${STORM_ADAPTERS_FILES})
source_group(builder FILES ${STORM_BUILDER_FILES})
source_group(cli FILES ${STORM_CLI_FILES})
source_group(exceptions FILES ${STORM_EXCEPTIONS_FILES})
source_group(logic FILES ${STORM_LOGIC_FILES})
source_group(generated FILES ${STORM_BUILD_HEADERS} ${STORM_BUILD_SOURCES})
@ -492,8 +498,8 @@ endif()
## All link_directories() calls MUST be made before this point #
## #
###############################################################################
add_library(storm ${STORM_SOURCES_WITHOUT_MAIN} ${STORM_HEADERS})
add_executable(storm-main ${STORM_MAIN_FILE})
add_library(storm ${STORM_LIB_SOURCES})
add_executable(storm-main ${STORM_MAIN_SOURCES})
target_link_libraries(storm-main storm)
set_target_properties(storm-main PROPERTIES OUTPUT_NAME "storm")
add_executable(storm-functional-tests ${STORM_FUNCTIONAL_TEST_MAIN_FILE} ${STORM_FUNCTIONAL_TEST_FILES})

11
src/utility/cli.cpp → src/cli/cli.cpp

@ -1,9 +1,12 @@
#include "cli.h"
#include "../utility/storm.h"
#include "src/settings/modules/DebugSettings.h"
#include "src/exceptions/OptionParserException.h"
#include "src/utility/storm-version.h"
// Includes for the linked libraries and versions header.
#ifdef STORM_HAVE_INTELTBB
# include "tbb/tbb_stddef.h"
@ -30,7 +33,6 @@
#endif
namespace storm {
namespace utility {
namespace cli {
std::string getCurrentWorkingDirectory() {
char temp[512];
@ -196,14 +198,14 @@ namespace storm {
LOG4CPLUS_INFO(logger, "Enabled trace mode, log output gets printed to console.");
}
if (storm::settings::debugSettings().isLogfileSet()) {
initializeFileLogging();
storm::utility::initializeFileLogging();
}
return true;
}
void processOptions() {
if (storm::settings::debugSettings().isLogfileSet()) {
initializeFileLogging();
storm::utility::initializeFileLogging();
}
storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings();
@ -253,5 +255,4 @@ namespace storm {
}
}
}
}
}

29
src/cli/cli.h

@ -0,0 +1,29 @@
#ifndef STORM_UTILITY_CLI_H_
#define STORM_UTILITY_CLI_H_
#include <string>
namespace storm {
namespace cli {
std::string getCurrentWorkingDirectory();
void printHeader(const int argc, const char* argv[]);
void printUsage();
/*!
* Parses the given command line arguments.
*
* @param argc The argc argument of main().
* @param argv The argv argument of main().
* @return True iff the program should continue to run after parsing the options.
*/
bool parseOptions(const int argc, const char* argv[]);
void processOptions();
}
}
#endif

1
src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp

@ -4,6 +4,7 @@
#include "src/storage/dd/CuddOdd.h"
#include "src/models/symbolic/Mdp.h"
#include "src/models/symbolic/StandardRewardModel.h"
#include "src/modelchecker/results/SymbolicQualitativeCheckResult.h"

9
src/modelchecker/prctl/HybridMdpPrctlModelChecker.h

@ -3,11 +3,16 @@
#include "src/modelchecker/propositional/SymbolicPropositionalModelChecker.h"
#include "src/models/symbolic/Mdp.h"
#include "src/utility/solver.h"
#include "src/storage/dd/DdType.h"
namespace storm {
namespace models {
namespace symbolic {
template<storm::dd::DdType T> class Mdp;
}
}
namespace modelchecker {
template<storm::dd::DdType DdType, typename ValueType>
class HybridMdpPrctlModelChecker : public SymbolicPropositionalModelChecker<DdType> {

1
src/modelchecker/propositional/SparsePropositionalModelChecker.h

@ -3,7 +3,6 @@
#include "src/modelchecker/AbstractModelChecker.h"
#include "src/models/sparse/Model.h"
namespace storm {
namespace modelchecker {

10
src/modelchecker/propositional/SymbolicPropositionalModelChecker.h

@ -2,11 +2,19 @@
#define STORM_MODELCHECKER_SYMBOLICPROPOSITIONALMODELCHECKER_H_
#include "src/modelchecker/AbstractModelChecker.h"
#include "src/models/symbolic/Model.h"
#include "src/storage/dd/DdType.h"
namespace storm {
namespace models {
namespace symbolic {
template<storm::dd::DdType Type> class Model;
}
}
namespace modelchecker {
template<storm::dd::DdType Type>
class SymbolicPropositionalModelChecker : public AbstractModelChecker {
public:

1
src/models/ModelBase.h

@ -5,7 +5,6 @@
#include "src/models/ModelType.h"
#include "src/utility/macros.h"
#include "src/exceptions/InvalidOperationException.h"
namespace storm {
namespace models {

1
src/models/sparse/Dtmc.h

@ -4,7 +4,6 @@
#include "src/models/sparse/DeterministicModel.h"
#include "src/utility/OsDetection.h"
#include "src/utility/constants.h"
#include "src/adapters/CarlAdapter.h"
namespace storm {

5
src/models/sparse/Model.h

@ -9,11 +9,14 @@
#include "src/models/ModelBase.h"
#include "src/models/sparse/StateLabeling.h"
#include "src/storage/sparse/StateType.h"
#include "src/storage/BitVector.h"
#include "src/storage/SparseMatrix.h"
#include "src/utility/OsDetection.h"
namespace storm {
namespace storage {
class BitVector;
}
namespace models {
namespace sparse {

1
src/models/symbolic/Model.cpp

@ -3,6 +3,7 @@
#include <boost/algorithm/string/join.hpp>
#include "src/exceptions/IllegalArgumentException.h"
#include "src/exceptions/InvalidOperationException.h"
#include "src/adapters/AddExpressionAdapter.h"

54
src/solver/AllowEarlyTerminationCondition.cpp

@ -0,0 +1,54 @@
#include "AllowEarlyTerminationCondition.h"
#include "src/utility/vector.h"
namespace storm {
namespace solver {
template<typename ValueType>
TerminateAfterFilteredSumPassesThresholdValue<ValueType>::TerminateAfterFilteredSumPassesThresholdValue(storm::storage::BitVector const& filter, ValueType threshold, bool terminateIfAbove) :
terminationThreshold(threshold), filter(filter), terminateIfAboveThreshold(terminateIfAbove)
{
// Intentionally left empty.
}
template<typename ValueType>
bool TerminateAfterFilteredSumPassesThresholdValue<ValueType>::terminateNow(const std::vector<ValueType>& currentValues) const {
assert(currentValues.size() >= filter.size());
ValueType currentThreshold = storm::utility::vector::sum_if(currentValues, filter);
if(this->terminateIfAboveThreshold) {
return currentThreshold >= this->terminationThreshold;
} else {
return currentThreshold <= this->terminationThreshold;
}
}
template<typename ValueType>
TerminateAfterFilteredExtremumPassesThresholdValue<ValueType>::TerminateAfterFilteredExtremumPassesThresholdValue(storm::storage::BitVector const& filter, ValueType threshold, bool terminateIfAbove, bool useMinimum) :
terminationThreshold(threshold), filter(filter), terminateIfAboveThreshold(terminateIfAbove), useMinimumAsExtremum(useMinimum)
{
// Intentionally left empty.
}
template<typename ValueType>
bool TerminateAfterFilteredExtremumPassesThresholdValue<ValueType>::terminateNow(const std::vector<ValueType>& currentValues) const {
assert(currentValues.size() >= filter.size());
ValueType initVal = terminateIfAboveThreshold ? terminationThreshold - 1 : terminationThreshold + 1;
ValueType currentThreshold = useMinimumAsExtremum ? storm::utility::vector::max_if(currentValues, filter, initVal) : storm::utility::vector::max_if(currentValues, filter, initVal);
if(this->terminateIfAboveThreshold) {
return currentThreshold >= this->terminationThreshold;
} else {
return currentThreshold <= this->terminationThreshold;
}
}
template class TerminateAfterFilteredExtremumPassesThresholdValue<double>;
template class TerminateAfterFilteredSumPassesThresholdValue<double>;
}
}

54
src/solver/AllowEarlyTerminationCondition.h

@ -0,0 +1,54 @@
#ifndef ALLOWEARLYTERMINATIONCONDITION_H
#define ALLOWEARLYTERMINATIONCONDITION_H
#include <vector>
#include "src/storage/BitVector.h"
namespace storm {
namespace solver {
template<typename ValueType>
class AllowEarlyTerminationCondition {
public:
virtual bool terminateNow(std::vector<ValueType> const& currentValues) const = 0;
};
template<typename ValueType>
class NoEarlyTerminationCondition : public AllowEarlyTerminationCondition<ValueType> {
public:
bool terminateNow(std::vector<ValueType> const& currentValues) const { return false; }
};
template<typename ValueType>
class TerminateAfterFilteredSumPassesThresholdValue : public AllowEarlyTerminationCondition<ValueType> {
public:
TerminateAfterFilteredSumPassesThresholdValue(storm::storage::BitVector const& filter, ValueType threshold, bool terminateAbove);
bool terminateNow(std::vector<ValueType> const& currentValues) const;
protected:
ValueType terminationThreshold;
storm::storage::BitVector filter;
bool terminateIfAboveThreshold;
};
template<typename ValueType>
class TerminateAfterFilteredExtremumPassesThresholdValue : public AllowEarlyTerminationCondition<ValueType>{
public:
TerminateAfterFilteredExtremumPassesThresholdValue(storm::storage::BitVector const& filter, ValueType threshold, bool terminateAbove, bool useMinimum);
bool terminateNow(std::vector<ValueType> const& currentValue) const;
protected:
ValueType terminationThreshold;
storm::storage::BitVector filter;
bool terminateIfAboveThreshold;
bool useMinimumAsExtremum;
};
}
}
#endif /* ALLOWEARLYTERMINATIONCONDITION_H */

4
src/solver/GmmxxMinMaxLinearEquationSolver.cpp

@ -53,7 +53,7 @@ namespace storm {
// Proceed with the iterations as long as the method did not converge or reach the user-specified maximum number
// of iterations.
while (!converged && iterations < this->maximalNumberOfIterations) {
while (!converged && iterations < this->maximalNumberOfIterations && !this->earlyTermination->terminateNow(*currentX)) {
// Compute x' = A*x + b.
gmm::mult(*gmmxxMatrix, *currentX, *multiplyResult);
gmm::add(b, *multiplyResult);
@ -119,7 +119,7 @@ namespace storm {
// Proceed with the iterations as long as the method did not converge or reach the user-specified maximum number
// of iterations.
while (!converged && iterations < this->maximalNumberOfIterations) {
while (!converged && iterations < this->maximalNumberOfIterations && !this->earlyTermination->terminateNow(*currentX)) {
// Take the sub-matrix according to the current choices
storm::storage::SparseMatrix<ValueType> submatrix = this->A.selectRowsFromRowGroups(this->policy, true);
submatrix.convertToEquationSystem();

4
src/solver/MinMaxLinearEquationSolver.cpp

@ -19,6 +19,10 @@ namespace storm {
}
}
void AbstractMinMaxLinearEquationSolver::setPolicyTracking(bool setToTrue) {
trackPolicy = setToTrue;
}
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;

9
src/solver/MinMaxLinearEquationSolver.h

@ -5,6 +5,7 @@
#include <cstdint>
#include "SolverSelectionOptions.h"
#include "src/storage/sparse/StateType.h"
#include "AllowEarlyTerminationCondition.h"
namespace storm {
namespace storage {
@ -55,7 +56,7 @@ namespace storm {
protected:
MinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& matrix, double precision, bool relativeError, uint_fast64_t maxNrIterations, bool trackPolicy, MinMaxTechniqueSelection prefTech) :
AbstractMinMaxLinearEquationSolver(precision, relativeError, maxNrIterations, trackPolicy, prefTech),
A(matrix) {
A(matrix), earlyTermination(new NoEarlyTerminationCondition<ValueType>()) {
// Intentionally left empty.
}
@ -101,7 +102,13 @@ namespace storm {
*/
virtual void performMatrixVectorMultiplication(bool minimize, std::vector<ValueType>& x, std::vector<ValueType>* b = nullptr, uint_fast64_t n = 1, std::vector<ValueType>* multiplyResult = nullptr) const = 0;
void setEarlyTerminationCondition(std::unique_ptr<AllowEarlyTerminationCondition<ValueType>> v) {
earlyTermination = std::move(v);
}
protected:
std::unique_ptr<AllowEarlyTerminationCondition<ValueType>> earlyTermination;
storm::storage::SparseMatrix<ValueType> const& A;
};

4
src/solver/NativeMinMaxLinearEquationSolver.cpp

@ -53,7 +53,7 @@ namespace storm {
// Proceed with the iterations as long as the method did not converge or reach the
// user-specified maximum number of iterations.
while (!converged && iterations < this->maximalNumberOfIterations) {
while (!converged && iterations < this->maximalNumberOfIterations && !this->earlyTermination->terminateNow(*currentX)) {
// Compute x' = A*x + b.
this->A.multiplyWithVector(*currentX, *multiplyResult);
storm::utility::vector::addVectors(*multiplyResult, b, *multiplyResult);
@ -121,7 +121,7 @@ namespace storm {
// Proceed with the iterations as long as the method did not converge or reach the user-specified maximum number
// of iterations.
while (!converged && iterations < this->maximalNumberOfIterations) {
while (!converged && iterations < this->maximalNumberOfIterations && !this->earlyTermination->terminateNow(*currentX)) {
// Take the sub-matrix according to the current choices
storm::storage::SparseMatrix<ValueType> submatrix = this->A.selectRowsFromRowGroups(this->policy, true);
submatrix.convertToEquationSystem();

3
src/solver/SolverSelectionOptions.h

@ -11,7 +11,8 @@ namespace storm {
ExtendEnumsWithSelectionField(LpSolverType, Gurobi, Glpk)
ExtendEnumsWithSelectionField(EquationSolverType, Native, Gmmxx)
ExtendEnumsWithSelectionField(EquationSolverType, Native, Gmmxx, Topological)
}
}

1
src/storage/DeterministicModelBisimulationDecomposition.h

@ -13,6 +13,7 @@
#include "src/storage/Distribution.h"
#include "src/utility/constants.h"
#include "src/utility/OsDetection.h"
#include "src/exceptions/InvalidOperationException.h"
namespace storm {
namespace utility {

10
src/storm.cpp

@ -1,22 +1,22 @@
// Include other headers.
#include "src/exceptions/BaseException.h"
#include "src/utility/macros.h"
#include "src/utility/cli.h"
#include "src/cli/cli.h"
#include "src/utility/initialize.h"
/*!
* Main entry point of the executable storm.
*/
int main(const int argc, const char** argv) {
try {
storm::utility::setUp();
storm::utility::cli::printHeader(argc, argv);
bool optionsCorrect = storm::utility::cli::parseOptions(argc, argv);
storm::cli::printHeader(argc, argv);
bool optionsCorrect = storm::cli::parseOptions(argc, argv);
if (!optionsCorrect) {
return -1;
}
// From this point on we are ready to carry out the actual computations.
storm::utility::cli::processOptions();
storm::cli::processOptions();
// All operations have now been performed, so we clean up everything and terminate.
storm::utility::cleanUp();

62
src/utility/solver.cpp

@ -81,30 +81,56 @@ namespace storm {
}
template<typename ValueType>
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> MinMaxLinearEquationSolverFactory<ValueType>::create(storm::storage::SparseMatrix<ValueType> const& matrix) const {
storm::solver::EquationSolverType equationSolver = storm::settings::generalSettings().getEquationSolver();
switch (equationSolver) {
case storm::solver::EquationSolverType::Gmmxx: return std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>>(new storm::solver::GmmxxMinMaxLinearEquationSolver<ValueType>(matrix));
case storm::solver::EquationSolverType::Native: return std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>>(new storm::solver::NativeMinMaxLinearEquationSolver<ValueType>(matrix));
default: return std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>>(new storm::solver::GmmxxMinMaxLinearEquationSolver<ValueType>(matrix));
}
MinMaxLinearEquationSolverFactory<ValueType>::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection solver)
{
setSolverType(solver);
prefTech = storm::solver::MinMaxTechniqueSelection::FROMSETTINGS;
}
template<typename ValueType>
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> GmmxxMinMaxLinearEquationSolverFactory<ValueType>::create(storm::storage::SparseMatrix<ValueType> const& matrix) const {
return std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>>(new storm::solver::GmmxxMinMaxLinearEquationSolver<ValueType>(matrix));
void MinMaxLinearEquationSolverFactory<ValueType>::setSolverType(storm::solver::EquationSolverTypeSelection solverTypeSel) {
if(solverTypeSel == storm::solver::EquationSolverTypeSelection::FROMSETTINGS) {
this->solverType = storm::settings::generalSettings().getEquationSolver();
} else {
this->solverType = storm::solver::convert(solverTypeSel);
}
}
template<typename ValueType>
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> NativeMinMaxLinearEquationSolverFactory<ValueType>::create(storm::storage::SparseMatrix<ValueType> const& matrix) const {
return std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>>(new storm::solver::NativeMinMaxLinearEquationSolver<ValueType>(matrix));
}
void MinMaxLinearEquationSolverFactory<ValueType>::setPreferredTechnique(storm::solver::MinMaxTechniqueSelection preferredTech) {
this->prefTech = preferredTech;
}
template<typename ValueType>
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> TopologicalMinMaxLinearEquationSolverFactory<ValueType>::create(storm::storage::SparseMatrix<ValueType> const& matrix) const {
return std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>>(new storm::solver::TopologicalMinMaxLinearEquationSolver<ValueType>(matrix));
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> MinMaxLinearEquationSolverFactory<ValueType>::create(storm::storage::SparseMatrix<ValueType> const& matrix, bool trackPolicy) const {
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> p1;
switch (solverType) {
case storm::solver::EquationSolverType::Gmmxx:
{
p1.reset(new storm::solver::GmmxxMinMaxLinearEquationSolver<ValueType>(matrix, this->prefTech));
break;
}
case storm::solver::EquationSolverType::Native:
{
p1.reset(new storm::solver::NativeMinMaxLinearEquationSolver<ValueType>(matrix, this->prefTech));
break;
}
case storm::solver::EquationSolverType::Topological:
{
STORM_LOG_THROW(prefTech == storm::solver::MinMaxTechniqueSelection::PolicyIteration, storm::exceptions::NotImplementedException, "Policy iteration for topological solver is not supported.");
p1.reset(new storm::solver::TopologicalMinMaxLinearEquationSolver<ValueType>(matrix));
break;
}
}
p1->setPolicyTracking(trackPolicy);
return p1;
}
std::unique_ptr<storm::solver::LpSolver> LpSolverFactory::create(std::string const& name) const {
storm::solver::LpSolverType lpSolver = storm::settings::generalSettings().getLpSolver();
switch (lpSolver) {
@ -134,9 +160,7 @@ namespace storm {
template class GmmxxLinearEquationSolverFactory<double>;
template class NativeLinearEquationSolverFactory<double>;
template class MinMaxLinearEquationSolverFactory<double>;
template class GmmxxMinMaxLinearEquationSolverFactory<double>;
template class NativeMinMaxLinearEquationSolverFactory<double>;
template class TopologicalMinMaxLinearEquationSolverFactory<double>;
}
}
}

34
src/utility/solver.h

@ -7,7 +7,7 @@
#include "src/solver/LinearEquationSolver.h"
#include "src/solver/NativeLinearEquationSolver.h"
#include "src/storage/dd/DdType.h"
#include "src/utility/ExtendSettingEnumWithSelectionField.h"
#include "src/solver/SolverSelectionOptions.h"
namespace storm {
namespace solver {
@ -80,30 +80,22 @@ namespace storm {
template<typename ValueType>
class MinMaxLinearEquationSolverFactory {
public:
MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection solverType = storm::solver::EquationSolverTypeSelection::FROMSETTINGS);
/*!
* Creates a new nondeterministic linear equation solver instance with the given matrix.
*/
virtual std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> create(storm::storage::SparseMatrix<ValueType> const& matrix) const;
};
template<typename ValueType>
class NativeMinMaxLinearEquationSolverFactory : public MinMaxLinearEquationSolverFactory<ValueType> {
public:
virtual std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> create(storm::storage::SparseMatrix<ValueType> const& matrix) const override;
};
template<typename ValueType>
class GmmxxMinMaxLinearEquationSolverFactory : public MinMaxLinearEquationSolverFactory<ValueType> {
public:
virtual std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> create(storm::storage::SparseMatrix<ValueType> const& matrix) const override;
};
template<typename ValueType>
class TopologicalMinMaxLinearEquationSolverFactory : public MinMaxLinearEquationSolverFactory<ValueType> {
public:
virtual std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> create(storm::storage::SparseMatrix<ValueType> const& matrix) const override;
virtual std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> create(storm::storage::SparseMatrix<ValueType> const& matrix, bool trackPolicy = false) const;
void setSolverType(storm::solver::EquationSolverTypeSelection solverType);
void setPreferredTechnique(storm::solver::MinMaxTechniqueSelection);
protected:
/// The type of solver which should be created.
storm::solver::EquationSolverType solverType;
/// The preferred technique to be used by the solver.
/// Notice that we save the selection enum here, which allows different solvers to use different techniques.
storm::solver::MinMaxTechniqueSelection prefTech;
};
class LpSolverFactory {
public:
/*!

36
src/utility/cli.h → src/utility/storm.h

@ -1,5 +1,6 @@
#ifndef STORM_UTILITY_CLI_H_
#define STORM_UTILITY_CLI_H_
#ifndef STORM_H
#define STORM_H
#include <iostream>
#include <iomanip>
@ -15,8 +16,6 @@
// Headers that provide auxiliary functionality.
#include "src/utility/storm-version.h"
#include "src/utility/OsDetection.h"
#include "src/settings/SettingsManager.h"
@ -72,25 +71,9 @@
#include "src/exceptions/NotImplementedException.h"
namespace storm {
namespace utility {
namespace cli {
std::string getCurrentWorkingDirectory();
void printHeader(const int argc, const char* argv[]);
void printUsage();
/*!
* Parses the given command line arguments.
*
* @param argc The argc argument of main().
* @param argv The argv argument of main().
* @return True iff the program should continue to run after parsing the options.
*/
bool parseOptions(const int argc, const char* argv[]);
template<typename ValueType>
template<typename ValueType>
std::shared_ptr<storm::models::sparse::Model<ValueType>> buildExplicitModel(std::string const& transitionsFile, std::string const& labelingFile, boost::optional<std::string> const& stateRewardsFile = boost::optional<std::string>(), boost::optional<std::string> const& transitionRewardsFile = boost::optional<std::string>()) {
return storm::parser::AutoParser::parseModel(transitionsFile, labelingFile, stateRewardsFile ? stateRewardsFile.get() : "", transitionRewardsFile ? transitionRewardsFile.get() : "");
}
@ -411,9 +394,8 @@ namespace storm {
}
}
void processOptions();
}
}
}
#endif
#endif /* STORM_H */

5
test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp

@ -11,6 +11,7 @@
#include "src/parser/FormulaParser.h"
#include "src/builder/DdPrismModelBuilder.h"
#include "src/models/symbolic/Dtmc.h"
#include "src/models/symbolic/Mdp.h"
#include "src/models/symbolic/StandardRewardModel.h"
#include "src/settings/SettingsManager.h"
@ -41,7 +42,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice) {
std::shared_ptr<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>> mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>();
storm::modelchecker::HybridMdpPrctlModelChecker<storm::dd::DdType::CUDD, double> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory<double>()));
storm::modelchecker::HybridMdpPrctlModelChecker<storm::dd::DdType::CUDD, double> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Gmmxx)));
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]");
@ -138,7 +139,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader) {
std::shared_ptr<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>> mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>();
storm::modelchecker::HybridMdpPrctlModelChecker<storm::dd::DdType::CUDD, double> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory<double>()));
storm::modelchecker::HybridMdpPrctlModelChecker<storm::dd::DdType::CUDD, double> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Gmmxx)));
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]");

8
test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp

@ -28,7 +28,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) {
ASSERT_EQ(mdp->getNumberOfStates(), 169ull);
ASSERT_EQ(mdp->getNumberOfTransitions(), 436ull);
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory<double>()));
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Gmmxx)));
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]");
@ -92,7 +92,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) {
std::shared_ptr<storm::models::sparse::Mdp<double>> stateRewardMdp = abstractModel->as<storm::models::sparse::Mdp<double>>();
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> stateRewardModelChecker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory<double>()));
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> stateRewardModelChecker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Gmmxx)));
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]");
@ -114,7 +114,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) {
std::shared_ptr<storm::models::sparse::Mdp<double>> stateAndTransitionRewardMdp = abstractModel->as<storm::models::sparse::Mdp<double>>();
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory<double>()));
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Gmmxx)));
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]");
@ -144,7 +144,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, AsynchronousLeader) {
ASSERT_EQ(3172ull, mdp->getNumberOfStates());
ASSERT_EQ(7144ull, mdp->getNumberOfTransitions());
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory<double>()));
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Gmmxx)));
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]");

5
test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp

@ -40,8 +40,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice) {
std::shared_ptr<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>> mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>();
storm::modelchecker::HybridMdpPrctlModelChecker<storm::dd::DdType::CUDD, double> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory<double>()));
storm::modelchecker::HybridMdpPrctlModelChecker<storm::dd::DdType::CUDD, double> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Native)));
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
@ -137,7 +136,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader) {
std::shared_ptr<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>> mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>();
storm::modelchecker::HybridMdpPrctlModelChecker<storm::dd::DdType::CUDD, double> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory<double>()));
storm::modelchecker::HybridMdpPrctlModelChecker<storm::dd::DdType::CUDD, double> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Native)));
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]");

18
test/functional/modelchecker/NativeMdpPrctlModelCheckerTest.cpp

@ -27,7 +27,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) {
ASSERT_EQ(mdp->getNumberOfStates(), 169ull);
ASSERT_EQ(mdp->getNumberOfTransitions(), 436ull);
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory<double>()));
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Native)));
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]");
@ -91,7 +91,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) {
std::shared_ptr<storm::models::sparse::Mdp<double>> stateRewardMdp = abstractModel->as<storm::models::sparse::Mdp<double>>();
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> stateRewardModelChecker(*stateRewardMdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory<double>()));
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> stateRewardModelChecker(*stateRewardMdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Native)));
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]");
@ -113,7 +113,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) {
std::shared_ptr<storm::models::sparse::Mdp<double>> stateAndTransitionRewardMdp = abstractModel->as<storm::models::sparse::Mdp<double>>();
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory<double>()));
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Native)));
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]");
@ -143,7 +143,7 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) {
ASSERT_EQ(3172ull, mdp->getNumberOfStates());
ASSERT_EQ(7144ull, mdp->getNumberOfTransitions());
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory<double>()));
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Native)));
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]");
@ -207,7 +207,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) {
mdp.reset(new storm::models::sparse::Mdp<double>(transitionMatrix, ap));
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory<double>()));
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Native)));
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]");
@ -239,7 +239,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) {
mdp.reset(new storm::models::sparse::Mdp<double>(transitionMatrix, ap));
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory<double>()));
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Native)));
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]");
@ -280,7 +280,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) {
mdp.reset(new storm::models::sparse::Mdp<double>(transitionMatrix, ap));
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory<double>()));
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Native)));
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]");
@ -366,7 +366,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA) {
mdp.reset(new storm::models::sparse::Mdp<double>(transitionMatrix, ap));
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory<double>()));
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Native)));
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]");
@ -488,7 +488,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA) {
mdp.reset(new storm::models::sparse::Mdp<double>(transitionMatrix, ap));
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory<double>()));
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Native)));
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]");

8
test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp

@ -26,7 +26,7 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Dice) {
ASSERT_EQ(mdp->getNumberOfStates(), 169ull);
ASSERT_EQ(mdp->getNumberOfTransitions(), 436ull);
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> mc(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::TopologicalMinMaxLinearEquationSolverFactory<double>()));
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> mc(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Topological)));
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]");
@ -87,7 +87,7 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Dice) {
// ------------- state rewards --------------
std::shared_ptr<storm::models::sparse::Mdp<double>> stateRewardMdp = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.state.rew", "")->as<storm::models::sparse::Mdp<double>>();
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> stateRewardModelChecker(*stateRewardMdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::TopologicalMinMaxLinearEquationSolverFactory<double>()));
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> stateRewardModelChecker(*stateRewardMdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Topological)));
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]");
@ -112,7 +112,7 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Dice) {
// -------------------------------- state and transition reward ------------------------
std::shared_ptr<storm::models::sparse::Mdp<double>> stateAndTransitionRewardMdp = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.state.rew", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.trans.rew")->as<storm::models::sparse::Mdp<double>>();
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::TopologicalMinMaxLinearEquationSolverFactory<double>()));
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Topological)));
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]");
@ -143,7 +143,7 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, AsynchronousLeader) {
ASSERT_EQ(mdp->getNumberOfStates(), 3172ull);
ASSERT_EQ(mdp->getNumberOfTransitions(), 7144ull);
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> mc(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::TopologicalMinMaxLinearEquationSolverFactory<double>()));
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> mc(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Topological)));
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]");

29
test/functional/solver/GmmxxMinMaxLinearEquationSolverTest.cpp

@ -25,6 +25,35 @@ TEST(GmmxxMinMaxLinearEquationSolver, SolveWithStandardOptions) {
ASSERT_LT(std::abs(x[0] - 0.989991), storm::settings::gmmxxEquationSolverSettings().getPrecision());
}
// TODO add better tests here.
TEST(GmmxxMinMaxLinearEquationSolver, SolveWithStandardOptionsAndEarlyTermination) {
storm::storage::SparseMatrixBuilder<double> builder(0, 0, 0, false, true);
ASSERT_NO_THROW(builder.newRowGroup(0));
ASSERT_NO_THROW(builder.addNextValue(0, 0, 0.9));
storm::storage::SparseMatrix<double> A;
ASSERT_NO_THROW(A = builder.build(2));
std::vector<double> x(1);
std::vector<double> b = {0.099, 0.5};
double bound = 0.8;
storm::solver::GmmxxMinMaxLinearEquationSolver<double> solver(A);
solver.setEarlyTerminationCondition(std::unique_ptr<storm::solver::AllowEarlyTerminationCondition<double>>(new storm::solver::TerminateAfterFilteredExtremumPassesThresholdValue<double>(storm::storage::BitVector(1, true), bound, true, true)));
ASSERT_NO_THROW(solver.solveEquationSystem(true, x, b));
ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::gmmxxEquationSolverSettings().getPrecision());
ASSERT_NO_THROW(solver.solveEquationSystem(false, x, b));
ASSERT_LT(std::abs(x[0] - 0.989991), 0.989991 - bound - storm::settings::gmmxxEquationSolverSettings().getPrecision());
bound = 0.6;
solver.setEarlyTerminationCondition(std::unique_ptr<storm::solver::AllowEarlyTerminationCondition<double>>(new storm::solver::TerminateAfterFilteredExtremumPassesThresholdValue<double>(storm::storage::BitVector(1, true), bound, true, true)));
ASSERT_NO_THROW(solver.solveEquationSystem(false, x, b));
ASSERT_LT(std::abs(x[0] - 0.989991), 0.989991 - bound - storm::settings::gmmxxEquationSolverSettings().getPrecision());
}
TEST(GmmxxMinMaxLinearEquationSolver, MatrixVectorMultiplication) {
storm::storage::SparseMatrixBuilder<double> builder(0, 0, 0, false, true);
ASSERT_NO_THROW(builder.newRowGroup(0));

4
test/performance/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp

@ -24,7 +24,7 @@ TEST(GmxxMdpPrctlModelCheckerTest, AsynchronousLeader) {
ASSERT_EQ(2095783ull, mdp->getNumberOfStates());
ASSERT_EQ(7714385ull, mdp->getNumberOfTransitions());
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory<double>()));
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Gmmxx)));
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]");
@ -82,7 +82,7 @@ TEST(GmxxMdpPrctlModelCheckerTest, Consensus) {
ASSERT_EQ(63616ull, mdp->getNumberOfStates());
ASSERT_EQ(213472ull, mdp->getNumberOfTransitions());
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory<double>()));
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Gmmxx)));
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"finished\"]");

4
test/performance/modelchecker/NativeMdpPrctlModelCheckerTest.cpp

@ -25,7 +25,7 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) {
ASSERT_EQ(2095783ull, mdp->getNumberOfStates());
ASSERT_EQ(7714385ull, mdp->getNumberOfTransitions());
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory<double>()));
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Native)));
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]");
@ -83,7 +83,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Consensus) {
ASSERT_EQ(63616ull, mdp->getNumberOfStates());
ASSERT_EQ(213472ull, mdp->getNumberOfTransitions());
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory<double>()));
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Native)));
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"finished\"]");

4
test/performance/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp

@ -20,7 +20,7 @@ TEST(DISABLED_TopologicalValueIterationMdpPrctlModelCheckerTest, AsynchronousLea
ASSERT_EQ(mdp->getNumberOfStates(), 2095783ull);
ASSERT_EQ(mdp->getNumberOfTransitions(), 7714385ull);
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::TopologicalMinMaxLinearEquationSolverFactory<double>()));
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Topological)));
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]");
@ -67,7 +67,7 @@ TEST(DISABLED_TopologicalValueIterationMdpPrctlModelCheckerTest, Consensus) {
ASSERT_EQ(mdp->getNumberOfStates(), 63616ull);
ASSERT_EQ(mdp->getNumberOfTransitions(), 213472ull);
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::TopologicalMinMaxLinearEquationSolverFactory<double>()));
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Topological)));
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"finished\"]");

|||||||
100:0
Loading…
Cancel
Save