sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Faster compilation and topological failing test failed 

Former-commit-id: 55c816594f
tempestpy_adaptions
sjunges 9 years ago
parent
31ed578e2c
commit
e3122e5ede
13 changed files with 56 additions and 32 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 1
      src/modelchecker/csl/SparseCtmcCslModelChecker.cpp
  2. 4
      src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp
  3. 1
      src/modelchecker/csl/helper/SparseCtmcCslHelper.h
  4. 1
      src/modelchecker/prctl/HybridMdpPrctlModelChecker.h
  5. 3
      src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp
  6. 3
      src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp
  7. 2
      src/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp
  8. 2
      src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp
  9. 14
      src/solver/NativeLinearEquationSolver.cpp
  10. 15
      src/solver/NativeLinearEquationSolver.h
  11. 12
      src/utility/solver.cpp
  12. 20
      src/utility/solver.h
  13. 10
      test/functional/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp

1
src/modelchecker/csl/SparseCtmcCslModelChecker.cpp
View File

@ -15,6 +15,7 @@
#include "src/exceptions/InvalidPropertyException.h"
#include "src/exceptions/NotImplementedException.h"
namespace storm {
namespace modelchecker {
template <typename SparseCtmcModelType>

4
src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp
View File

@ -5,17 +5,19 @@
#include "src/settings/SettingsManager.h"
#include "src/settings/modules/GeneralSettings.h"
#include "src/solver/LinearEquationSolver.h"
#include "src/storage/StronglyConnectedComponentDecomposition.h"
#include "src/utility/macros.h"
#include "src/utility/vector.h"
#include "src/utility/graph.h"
#include "src/utility/numerical.h"
#include "src/exceptions/InvalidStateException.h"
#include "src/exceptions/InvalidPropertyException.h"
namespace storm {
namespace modelchecker {
namespace helper {

1
src/modelchecker/csl/helper/SparseCtmcCslHelper.h
View File

@ -7,6 +7,7 @@
#include "src/utility/solver.h"
namespace storm {
namespace modelchecker {
namespace helper {

1
src/modelchecker/prctl/HybridMdpPrctlModelChecker.h
View File

@ -6,6 +6,7 @@
#include "src/utility/solver.h"
#include "src/storage/dd/DdType.h"
namespace storm {
namespace models {
namespace symbolic {

3
src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp
View File

@ -1,5 +1,8 @@
#include "src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.h"
#include "src/solver/LinearEquationSolver.h"
#include "src/storage/dd/CuddDdManager.h"
#include "src/storage/dd/CuddAdd.h"
#include "src/storage/dd/CuddBdd.h"

3
src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp
View File

@ -6,6 +6,9 @@
#include "src/utility/vector.h"
#include "src/utility/graph.h"
#include "src/solver/LinearEquationSolver.h"
#include "src/exceptions/InvalidStateException.h"
#include "src/exceptions/InvalidPropertyException.h"

2
src/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp
View File

@ -6,6 +6,8 @@
#include "src/storage/dd/CuddBdd.h"
#include "src/storage/dd/CuddOdd.h"
#include "src/solver/SymbolicLinearEquationSolver.h"
#include "src/models/symbolic/StandardRewardModel.h"
#include "src/utility/graph.h"

2
src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp
View File

@ -1,5 +1,7 @@
#include "src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.h"
#include "src/solver/SymbolicMinMaxLinearEquationSolver.h"
#include "src/storage/dd/CuddDdManager.h"
#include "src/storage/dd/CuddAdd.h"
#include "src/storage/dd/CuddBdd.h"

14
src/solver/NativeLinearEquationSolver.cpp
View File

@ -12,12 +12,12 @@ namespace storm {
namespace solver {
template<typename ValueType>
NativeLinearEquationSolver<ValueType>::NativeLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, SolutionMethod method, double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : A(A), method(method), precision(precision), relative(relative), maximalNumberOfIterations(maximalNumberOfIterations) {
NativeLinearEquationSolver<ValueType>::NativeLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, NativeLinearEquationSolverSolutionMethod method, double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : A(A), method(method), precision(precision), relative(relative), maximalNumberOfIterations(maximalNumberOfIterations) {
// Intentionally left empty.
}
template<typename ValueType>
NativeLinearEquationSolver<ValueType>::NativeLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, SolutionMethod method) : A(A), method(method) {
NativeLinearEquationSolver<ValueType>::NativeLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, NativeLinearEquationSolverSolutionMethod method) : A(A), method(method) {
// Get the settings object to customize linear solving.
storm::settings::modules::NativeEquationSolverSettings const& settings = storm::settings::nativeEquationSolverSettings();
@ -29,9 +29,9 @@ namespace storm {
template<typename ValueType>
void NativeLinearEquationSolver<ValueType>::solveEquationSystem(std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult) const {
if (method == SolutionMethod::SOR || method == SolutionMethod::GaussSeidel) {
if (method == NativeLinearEquationSolverSolutionMethod::SOR || method == NativeLinearEquationSolverSolutionMethod::GaussSeidel) {
// Define the omega used for SOR.
ValueType omega = method == SolutionMethod::SOR ? storm::settings::nativeEquationSolverSettings().getOmega() : storm::utility::one<ValueType>();
ValueType omega = method == NativeLinearEquationSolverSolutionMethod::SOR ? storm::settings::nativeEquationSolverSettings().getOmega() : storm::utility::one<ValueType>();
// To avoid copying the contents of the vector in the loop, we create a temporary x to swap with.
bool tmpXProvided = true;
@ -157,9 +157,9 @@ namespace storm {
template<typename ValueType>
std::string NativeLinearEquationSolver<ValueType>::methodToString() const {
switch (method) {
case SolutionMethod::Jacobi: return "jacobi";
case SolutionMethod::GaussSeidel: return "gauss-seidel";
case SolutionMethod::SOR: return "sor";
case NativeLinearEquationSolverSolutionMethod::Jacobi: return "jacobi";
case NativeLinearEquationSolverSolutionMethod::GaussSeidel: return "gauss-seidel";
case NativeLinearEquationSolverSolutionMethod::SOR: return "sor";
default: return "invalid";
}
}

15
src/solver/NativeLinearEquationSolver.h
View File

@ -6,16 +6,17 @@
namespace storm {
namespace solver {
// An enumeration specifying the available solution methods.
enum class NativeLinearEquationSolverSolutionMethod {
Jacobi, GaussSeidel, SOR
};
/*!
* A class that uses StoRM's native matrix operations to implement the LinearEquationSolver interface.
*/
template<typename ValueType>
class NativeLinearEquationSolver : public LinearEquationSolver<ValueType> {
public:
// An enumeration specifying the available solution methods.
enum class SolutionMethod {
Jacobi, GaussSeidel, SOR
};
/*!
* Constructs a linear equation solver with parameters being set according to the settings object.
@ -23,7 +24,7 @@ namespace storm {
* @param A The matrix defining the coefficients of the linear equation system.
* @param method The method to use for solving linear equations.
*/
NativeLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, SolutionMethod method = SolutionMethod::Jacobi);
NativeLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, NativeLinearEquationSolverSolutionMethod method = NativeLinearEquationSolverSolutionMethod::Jacobi);
/*!
* Constructs a linear equation solver with the given parameters.
@ -35,7 +36,7 @@ namespace storm {
* @param relative If set, the relative error rather than the absolute error is considered for convergence
* detection.
*/
NativeLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, SolutionMethod method, double precision, uint_fast64_t maximalNumberOfIterations, bool relative = true);
NativeLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, NativeLinearEquationSolverSolutionMethod method, double precision, uint_fast64_t maximalNumberOfIterations, bool relative = true);
virtual void solveEquationSystem(std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult = nullptr) const override;
@ -53,7 +54,7 @@ namespace storm {
storm::storage::SparseMatrix<ValueType> const& A;
// The method to use for solving linear equation systems.
SolutionMethod method;
NativeLinearEquationSolverSolutionMethod method;
// The required precision for the iterative methods.
double precision;

12
src/utility/solver.cpp
View File

@ -2,8 +2,10 @@
#include "src/solver/SymbolicGameSolver.h"
#include <vector>
#include "src/solver/SymbolicLinearEquationSolver.h"
#include "src/solver/SymbolicMinMaxLinearEquationSolver.h"
#include "src/solver/NativeLinearEquationSolver.h"
#include "src/solver/GmmxxLinearEquationSolver.h"
@ -60,18 +62,18 @@ namespace storm {
NativeLinearEquationSolverFactory<ValueType>::NativeLinearEquationSolverFactory() {
switch (storm::settings::nativeEquationSolverSettings().getLinearEquationSystemMethod()) {
case settings::modules::NativeEquationSolverSettings::LinearEquationMethod::Jacobi:
this->method = storm::solver::NativeLinearEquationSolver<ValueType>::SolutionMethod::Jacobi;
this->method = storm::solver::NativeLinearEquationSolverSolutionMethod::Jacobi;
break;
case settings::modules::NativeEquationSolverSettings::LinearEquationMethod::GaussSeidel:
this->method = storm::solver::NativeLinearEquationSolver<ValueType>::SolutionMethod::GaussSeidel;
this->method = storm::solver::NativeLinearEquationSolverSolutionMethod::GaussSeidel;
case settings::modules::NativeEquationSolverSettings::LinearEquationMethod::SOR:
this->method = storm::solver::NativeLinearEquationSolver<ValueType>::SolutionMethod::SOR;
this->method = storm::solver::NativeLinearEquationSolverSolutionMethod::SOR;
}
omega = storm::settings::nativeEquationSolverSettings().getOmega();
}
template<typename ValueType>
NativeLinearEquationSolverFactory<ValueType>::NativeLinearEquationSolverFactory(typename storm::solver::NativeLinearEquationSolver<ValueType>::SolutionMethod method, ValueType omega) : method(method), omega(omega) {
NativeLinearEquationSolverFactory<ValueType>::NativeLinearEquationSolverFactory(typename storm::solver::NativeLinearEquationSolverSolutionMethod method, ValueType omega) : method(method), omega(omega) {
// Intentionally left empty.
}
@ -83,8 +85,8 @@ namespace storm {
template<typename ValueType>
MinMaxLinearEquationSolverFactory<ValueType>::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection solver)
{
setSolverType(solver);
prefTech = storm::solver::MinMaxTechniqueSelection::FROMSETTINGS;
setSolverType(solver);
}
template<typename ValueType>

20
src/utility/solver.h
View File

@ -1,11 +1,9 @@
#ifndef STORM_UTILITY_SOLVER_H_
#define STORM_UTILITY_SOLVER_H_
#include "src/solver/SymbolicGameSolver.h"
#include "src/solver/SymbolicMinMaxLinearEquationSolver.h"
#include "src/solver/SymbolicLinearEquationSolver.h"
#include "src/solver/LinearEquationSolver.h"
#include "src/solver/NativeLinearEquationSolver.h"
#include <set>
#include <vector>
#include "src/storage/dd/DdType.h"
#include "src/solver/SolverSelectionOptions.h"
@ -13,10 +11,18 @@ namespace storm {
namespace solver {
template<storm::dd::DdType T> class SymbolicGameSolver;
template<storm::dd::DdType T, typename V> class SymbolicLinearEquationSolver;
template<storm::dd::DdType T, typename V> class SymbolicMinMaxLinearEquationSolver;
template<typename V> class LinearEquationSolver;
template<typename V> class MinMaxLinearEquationSolver;
class LpSolver;
template<typename ValueType> class NativeLinearEquationSolver;
enum class NativeLinearEquationSolverSolutionMethod;
}
namespace storage {
template<typename V> class SparseMatrix;
}
namespace dd {
template<storm::dd::DdType T> class Add;
template<storm::dd::DdType T> class Bdd;
@ -62,12 +68,12 @@ namespace storm {
class NativeLinearEquationSolverFactory : public LinearEquationSolverFactory<ValueType> {
public:
NativeLinearEquationSolverFactory();
NativeLinearEquationSolverFactory(typename storm::solver::NativeLinearEquationSolver<ValueType>::SolutionMethod method, ValueType omega);
NativeLinearEquationSolverFactory(typename storm::solver::NativeLinearEquationSolverSolutionMethod method, ValueType omega);
virtual std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> create(storm::storage::SparseMatrix<ValueType> const& matrix) const override;
private:
typename storm::solver::NativeLinearEquationSolver<ValueType>::SolutionMethod method;
typename storm::solver::NativeLinearEquationSolverSolutionMethod method;
ValueType omega;
};

10
test/functional/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp
View File

@ -9,7 +9,7 @@
#include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "src/settings/SettingsManager.h"
#include "src/solver/NativeLinearEquationSolver.h"
#include "src/settings/modules/GeneralSettings.h"
#include "src/settings/modules/NativeEquationSolverSettings.h"
@ -153,7 +153,7 @@ TEST(SparseDtmcPrctlModelCheckerTest, LRASingleBscc) {
dtmc.reset(new storm::models::sparse::Dtmc<double>(transitionMatrix, ap));
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>(storm::solver::NativeLinearEquationSolver<double>::SolutionMethod::SOR, 0.9)));
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>(storm::solver::NativeLinearEquationSolverSolutionMethod::SOR, 0.9)));
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]");
@ -177,7 +177,7 @@ TEST(SparseDtmcPrctlModelCheckerTest, LRASingleBscc) {
dtmc.reset(new storm::models::sparse::Dtmc<double>(transitionMatrix, ap));
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>(storm::solver::NativeLinearEquationSolver<double>::SolutionMethod::SOR, 0.9)));
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>(storm::solver::NativeLinearEquationSolverSolutionMethod::SOR, 0.9)));
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]");
@ -201,7 +201,7 @@ TEST(SparseDtmcPrctlModelCheckerTest, LRASingleBscc) {
dtmc.reset(new storm::models::sparse::Dtmc<double>(transitionMatrix, ap));
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>(storm::solver::NativeLinearEquationSolver<double>::SolutionMethod::SOR, 0.9)));
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>(storm::solver::NativeLinearEquationSolverSolutionMethod::SOR, 0.9)));
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]");
@ -264,7 +264,7 @@ TEST(SparseDtmcPrctlModelCheckerTest, LRA) {
mdp.reset(new storm::models::sparse::Dtmc<double>(transitionMatrix, ap));
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>(storm::solver::NativeLinearEquationSolver<double>::SolutionMethod::SOR, 0.9)));
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>(storm::solver::NativeLinearEquationSolverSolutionMethod::SOR, 0.9)));
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]");

Write Preview
Loading…
Cancel
Save