sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
8714 Commits
1 Branch
0 Tags
187 MiB
 
 
 
 
Tree: a9868fd501
Branches Tags
${ item.name }
Create tag ${ searchTerm }
Create branch ${ searchTerm }
from 'a9868fd501'
${ noResults }
tempest/src/storm/solver/EigenLinearEquationSolver.cpp

282 lines
16 KiB
Raw Blame History

#include "storm/solver/EigenLinearEquationSolver.h"
#include "storm/adapters/EigenAdapter.h"
#include "storm/environment/solver/EigenSolverEnvironment.h"
#include "storm/utility/vector.h"
#include "storm/utility/macros.h"
#include "storm/exceptions/InvalidSettingsException.h"
namespace storm {
namespace solver {
template<typename ValueType>
EigenLinearEquationSolver<ValueType>::EigenLinearEquationSolver() {
// Intentionally left empty.
}
template<typename ValueType>
EigenLinearEquationSolver<ValueType>::EigenLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A) {
this->setMatrix(A);
}
template<typename ValueType>
EigenLinearEquationSolver<ValueType>::EigenLinearEquationSolver(storm::storage::SparseMatrix<ValueType>&& A) {
this->setMatrix(std::move(A));
}
template<typename ValueType>
void EigenLinearEquationSolver<ValueType>::setMatrix(storm::storage::SparseMatrix<ValueType> const& A) {
eigenA = storm::adapters::EigenAdapter::toEigenSparseMatrix<ValueType>(A);
this->clearCache();
}
template<typename ValueType>
void EigenLinearEquationSolver<ValueType>::setMatrix(storm::storage::SparseMatrix<ValueType>&& A) {
// Take ownership of the matrix so it is destroyed after we have translated it to Eigen's format.
storm::storage::SparseMatrix<ValueType> localA(std::move(A));
this->setMatrix(localA);
this->clearCache();
}
template<typename ValueType>
EigenLinearEquationSolverMethod EigenLinearEquationSolver<ValueType>::getMethod(Environment const& env, bool isExactMode) const {
// Adjust the method if none was specified and we are using rational numbers.
auto method = env.solver().eigen().getMethod();
if (isExactMode && method != EigenLinearEquationSolverMethod::SparseLU) {
if (env.solver().eigen().isMethodSetFromDefault()) {
STORM_LOG_INFO("Selecting 'SparseLU' as the solution technique to guarantee exact results.");
} else {
STORM_LOG_WARN("The selected solution method does not guarantee exact results. Falling back to SparseLU.");
}
method = EigenLinearEquationSolverMethod::SparseLU;
} else if (env.solver().isForceSoundness() && method != EigenLinearEquationSolverMethod::SparseLU) {
if (env.solver().eigen().isMethodSetFromDefault()) {
STORM_LOG_INFO("Selecting 'SparseLU' as the solution technique to guarantee sound results. If you want to override this, please explicitly specify a different method.");
method = EigenLinearEquationSolverMethod::SparseLU;
} else {
STORM_LOG_WARN("The selected solution method does not guarantee sound results.");
}
}
return method;
}
#ifdef STORM_HAVE_CARL
// Specialization for storm::RationalNumber
template<>
bool EigenLinearEquationSolver<storm::RationalNumber>::internalSolveEquations(Environment const& env, std::vector<storm::RationalNumber>& x, std::vector<storm::RationalNumber> const& b) const {
auto solutionMethod = getMethod(env, true);
STORM_LOG_WARN_COND(solutionMethod == EigenLinearEquationSolverMethod::SparseLU, "Switching method to SparseLU.");
STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with with rational numbers using LU factorization (Eigen library).");
// Map the input vectors to Eigen's format.
auto eigenX = Eigen::Matrix<storm::RationalNumber, Eigen::Dynamic, 1>::Map(x.data(), x.size());
auto eigenB = Eigen::Matrix<storm::RationalNumber, Eigen::Dynamic, 1>::Map(b.data(), b.size());
Eigen::SparseLU<Eigen::SparseMatrix<storm::RationalNumber>, Eigen::COLAMDOrdering<int>> solver;
solver.compute(*eigenA);
solver._solve_impl(eigenB, eigenX);
return solver.info() == Eigen::ComputationInfo::Success;
}
// Specialization for storm::RationalFunction
template<>
bool EigenLinearEquationSolver<storm::RationalFunction>::internalSolveEquations(Environment const& env, std::vector<storm::RationalFunction>& x, std::vector<storm::RationalFunction> const& b) const {
auto solutionMethod = getMethod(env, true);
STORM_LOG_WARN_COND(solutionMethod == EigenLinearEquationSolverMethod::SparseLU, "Switching method to SparseLU.");
STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with rational functions using LU factorization (Eigen library).");
// Map the input vectors to Eigen's format.
auto eigenX = Eigen::Matrix<storm::RationalFunction, Eigen::Dynamic, 1>::Map(x.data(), x.size());
auto eigenB = Eigen::Matrix<storm::RationalFunction, Eigen::Dynamic, 1>::Map(b.data(), b.size());
Eigen::SparseLU<Eigen::SparseMatrix<storm::RationalFunction>, Eigen::COLAMDOrdering<int>> solver;
solver.compute(*eigenA);
solver._solve_impl(eigenB, eigenX);
return solver.info() == Eigen::ComputationInfo::Success;
}
#endif
template<typename ValueType>
bool EigenLinearEquationSolver<ValueType>::internalSolveEquations(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
// Map the input vectors to Eigen's format.
auto eigenX = Eigen::Matrix<ValueType, Eigen::Dynamic, 1>::Map(x.data(), x.size());
auto eigenB = Eigen::Matrix<ValueType, Eigen::Dynamic, 1>::Map(b.data(), b.size());
auto solutionMethod = getMethod(env, env.solver().isForceExact());
if (solutionMethod == EigenLinearEquationSolverMethod::SparseLU) {
STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with sparse LU factorization (Eigen library).");
Eigen::SparseLU<Eigen::SparseMatrix<ValueType>, Eigen::COLAMDOrdering<int>> solver;
solver.compute(*this->eigenA);
solver._solve_impl(eigenB, eigenX);
} else {
bool converged = false;
uint64_t numberOfIterations = 0;
Eigen::Index maxIter = std::numeric_limits<Eigen::Index>::max();
if (env.solver().eigen().getMaximalNumberOfIterations() < static_cast<uint64_t>(maxIter)) {
maxIter = env.solver().eigen().getMaximalNumberOfIterations();
}
uint64_t restartThreshold = env.solver().eigen().getRestartThreshold();
ValueType precision = storm::utility::convertNumber<ValueType>(env.solver().eigen().getPrecision());
EigenLinearEquationSolverPreconditioner preconditioner = env.solver().eigen().getPreconditioner();
if (solutionMethod == EigenLinearEquationSolverMethod::Bicgstab) {
if (preconditioner == EigenLinearEquationSolverPreconditioner::Ilu) {
STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with BiCGSTAB with Ilu preconditioner (Eigen library).");
Eigen::BiCGSTAB<Eigen::SparseMatrix<ValueType>, Eigen::IncompleteLUT<ValueType>> solver;
solver.compute(*this->eigenA);
solver.setTolerance(precision);
solver.setMaxIterations(maxIter);
eigenX = solver.solveWithGuess(eigenB, eigenX);
converged = solver.info() == Eigen::ComputationInfo::Success;
numberOfIterations = solver.iterations();
} else if (preconditioner == EigenLinearEquationSolverPreconditioner::Diagonal) {
STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with BiCGSTAB with Diagonal preconditioner (Eigen library).");
Eigen::BiCGSTAB<Eigen::SparseMatrix<ValueType>, Eigen::DiagonalPreconditioner<ValueType>> solver;
solver.setTolerance(precision);
solver.setMaxIterations(maxIter);
solver.compute(*this->eigenA);
eigenX = solver.solveWithGuess(eigenB, eigenX);
converged = solver.info() == Eigen::ComputationInfo::Success;
numberOfIterations = solver.iterations();
} else {
STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with BiCGSTAB with identity preconditioner (Eigen library).");
Eigen::BiCGSTAB<Eigen::SparseMatrix<ValueType>, Eigen::IdentityPreconditioner> solver;
solver.setTolerance(precision);
solver.setMaxIterations(maxIter);
solver.compute(*this->eigenA);
eigenX = solver.solveWithGuess(eigenB, eigenX);
numberOfIterations = solver.iterations();
converged = solver.info() == Eigen::ComputationInfo::Success;
}
} else if (solutionMethod == EigenLinearEquationSolverMethod::DGmres) {
if (preconditioner == EigenLinearEquationSolverPreconditioner::Ilu) {
STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with DGMRES with Ilu preconditioner (Eigen library).");
Eigen::DGMRES<Eigen::SparseMatrix<ValueType>, Eigen::IncompleteLUT<ValueType>> solver;
solver.setTolerance(precision);
solver.setMaxIterations(maxIter);
solver.set_restart(restartThreshold);
solver.compute(*this->eigenA);
eigenX = solver.solveWithGuess(eigenB, eigenX);
converged = solver.info() == Eigen::ComputationInfo::Success;
numberOfIterations = solver.iterations();
} else if (preconditioner == EigenLinearEquationSolverPreconditioner::Diagonal) {
STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with DGMRES with Diagonal preconditioner (Eigen library).");
Eigen::DGMRES<Eigen::SparseMatrix<ValueType>, Eigen::DiagonalPreconditioner<ValueType>> solver;
solver.setTolerance(precision);
solver.setMaxIterations(maxIter);
solver.set_restart(restartThreshold);
solver.compute(*this->eigenA);
eigenX = solver.solveWithGuess(eigenB, eigenX);
converged = solver.info() == Eigen::ComputationInfo::Success;
numberOfIterations = solver.iterations();
} else {
STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with DGMRES with identity preconditioner (Eigen library).");
Eigen::DGMRES<Eigen::SparseMatrix<ValueType>, Eigen::IdentityPreconditioner> solver;
solver.setTolerance(precision);
solver.setMaxIterations(maxIter);
solver.set_restart(restartThreshold);
solver.compute(*this->eigenA);
eigenX = solver.solveWithGuess(eigenB, eigenX);
converged = solver.info() == Eigen::ComputationInfo::Success;
numberOfIterations = solver.iterations();
}
} else if (solutionMethod == EigenLinearEquationSolverMethod::Gmres) {
if (preconditioner == EigenLinearEquationSolverPreconditioner::Ilu) {
STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with GMRES with Ilu preconditioner (Eigen library).");
Eigen::GMRES<Eigen::SparseMatrix<ValueType>, Eigen::IncompleteLUT<ValueType>> solver;
solver.setTolerance(precision);
solver.setMaxIterations(maxIter) sp/tempestpy - lib/stormpy/examples/files.py at 028c94262503abc0d0e07d9738558243a3b0197a - tempestpy - Gitea: Git with a cup of tea
sp
/
tempestpy
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
883 Commits
1 Branch
0 Tags
2.1 MiB
 
 
 
 
 
 
Tree: 028c942625
Branches Tags
${ item.name }
Create tag ${ searchTerm }
Create branch ${ searchTerm }
from '028c942625'
${ noResults }
tempestpy/lib/stormpy/examples/files.py

66 lines
2.4 KiB
Raw Blame History

import os
testfile_dir = os.path.join(os.path.dirname(os.path.abspath(__file__)), "files")
def _path(folder, file):
"""
Internal method for simpler listing of examples.
:param folder: Folder.
:param file: Example file.
:return: Complete path to example file.
"""
return os.path.join(testfile_dir, folder, file)
prism_dtmc_die = _path("dtmc", "die.pm")
"""Knuth Yao Die Example"""
prism_pdtmc_die = _path("pdtmc", "parametric_die.pm")
"""Knuth Yao Die -- 2 unfair coins Example"""
prism_dtmc_brp = _path("dtmc", "brp-16-2.pm")
"""Bounded Retransmission Protocol"""
prism_ma_simple = _path("ma", "simple.ma")
"""Prism file for a simple Markov automaton"""
drn_ctmc_dft = _path("ctmc", "dft.drn")
"""DRN format for a CTMC from a DFT"""
drn_pdtmc_die = _path("pdtmc", "die.drn")
"""DRN format for a pDTMC for the KY-Die"""
jani_dtmc_die = _path("dtmc", "die.jani")
"""Jani Version of Knuth Yao Die Example"""
prism_pdtmc_brp = _path("pdtmc", "brp16_2.pm")
"""Bounded retransmission protocol with parameters"""
prism_mdp_coin_2_2 = _path("mdp", "coin2-2.nm")
"""Prism example for coin MDP"""
prism_pmdp_coin_two_dice = _path("pmdp", "two_dice.nm")
"""Prism example for parametric two dice"""
prism_mdp_maze = _path("mdp", "maze_2.nm")
"""Prism example for the maze MDP"""
drn_pomdp_maze = _path("pomdp", "maze.drn")
"""DRN example for the maze POMDP"""
prism_pomdp_maze = _path("pomdp", "maze_2.prism")
"""Prism example for the maze POMDP"""
prism_par_pomdp_maze = _path("pomdp", "maze_2_par.prism")
"""Prism example for the parametric POMDP"""
dft_galileo_hecs = _path("dft", "hecs.dft")
"""DFT example for HECS (Galileo format)"""
dft_json_and = _path("dft", "and.json")
"""DFT example for AND gate (JSON format)"""
gspn_pnpro_simple = _path("gspn", "gspn_simple.pnpro")
"""GSPN example (PNPRO format)"""
gspn_pnml_simple = _path("gspn", "gspn_simple.pnml")
"""GSPN example (PNML format)"""
"""Shield Example 1"""
prism_mdp_lava_simple = _path("mdp", "simple.prism")
prism_mdp_cliff_walking = _path("mdp", "CliffZigZag.prism")
"""Optimal Shield Example 1"""
prism_smg_lights = _path("smg", "lights.prism")
"""Optimal Shield Example 2"""
prism_smg_robot = _path("smg", "robotics_planning.prism")
"""Optimal Controller Example"""
prism_smg_controller = _path("smg", "robot_controller.prism")
"""Safety Shield Synthesis"""
prism_smg_shield_synth = _path("smg", "safety_shield_robot.prism")
0 HTTP/1.0 200 OK Content-Type: text/html; charset=UTF-8 Set-Cookie: i_like_gitea=8516f11c059ca0a7; Path=/; HttpOnly; SameSite=Lax Set-Cookie: _csrf=uK0sfshQJJopTlh6TzjxBzot_-I6MTczNzU4MzAwNjAxNzc5OTc5Nw; Path=/; Expires=Thu, 23 Jan 2025 21:56:46 GMT; HttpOnly; SameSite=Lax Set-Cookie: macaron_flash=; Path=/; Max-Age=0; HttpOnly; SameSite=Lax X-Frame-Options: SAMEORIGIN Date: Wed, 22 Jan 2025 21:56:50 GMT sp/tempest - tempest - Gitea: Git with a cup of tea
sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
8739 Commits
1 Branch
0 Tags
187 MiB
Tree: 2f5a53196c
Branches Tags
${ item.name }
Create tag ${ searchTerm }
Create branch ${ searchTerm }
from '2f5a53196c'
${ noResults }
Commit Graph

164 Commits (2f5a53196c5165703d197ed5a67f1d4e314e7d35)

Author SHA1 Message Date
Tim Quatmann fb112ab191 Added support for modulo operators when building symbolic models in exact mode.
4 years ago
Tim Quatmann 5a76128e3f Removed DdType::None because there is no use for this anymore.
4 years ago
Tim Quatmann d49210ac2e Added DdType::None to encode that an explicit representation should be used.
5 years ago
Sebastian Junges d6bfcb4818 refactoring: moving some code out of the util folder
5 years ago
Daniel Basgöze 7076a54dfb Add error checking to C style io
5 years ago
Daniel Basgöze b7c53c080b Remove trailing whitespace
5 years ago
Daniel Basgöze 002d9e1925 Add error checking to C style io
5 years ago
Daniel Basgöze 1ee87a876a Remove trailing whitespace
5 years ago
Matthias Volk 41199ea5c7 Append in dot output for DDs
5 years ago
TimQu 5d8419336f InternalAdds: Added a comment related to GitHub issue #64
5 years ago
TimQu 36c410875c Revert "InternalAdds: Making the different splitIntoGroups implementations more consistent to each other (in the sense that the Dd is traversed in the same order)."
5 years ago
Tim Quatmann 5d530bb532 Improved compatibility of the dd-to-sparse engine (can now handle reward models with state action rewards)
5 years ago
Tim Quatmann cefe43f2bf InternalAdds: Making the different splitIntoGroups implementations more consistent to each other (in the sense that the Dd is traversed in the same order).
5 years ago
Tim Quatmann a99f0905e2 dd/bisimulation: Added argument to "getQuotient" which allows to set the quotient type (dd / sparse)
5 years ago
Matthias Volk 7a8b32399c Issue warning if max memory of Sylvan is ignored
6 years ago
Sebastian Junges d295f6e777 export of bdds into dot and text format
6 years ago
Matthias Volk 685b5c6b27 Throw exceptions after switch/case to silence compiler warnings about not returning anything
6 years ago
Matthias Volk b2ea3993ef Fixed assertion in symbolic bisimulation
6 years ago
dehnert 2768d15f4f fixing minor issue in symboiic bisimulation relation pointed out by Tim
6 years ago
dehnert 8c96548566 more work on game-based abstraction
7 years ago
dehnert 692587495f fixed bug in quotient extraction
7 years ago
dehnert 3ad85ba0e6 fixes and improvements for game-based abstraction
7 years ago
dehnert c2e646b887 working towards predicate synthesis from explicit (qualitative) result for game-based abstraction
7 years ago
dehnert c6a5d5a74d started on refining menu games based on explicit results
7 years ago
dehnert edbe3b1952 more work on explicit game solving
7 years ago
dehnert cedae194e3 towards labeling generation in dd to sparse conversion
7 years ago
dehnert 733bec60bd started on hybrid solution of abstraction
7 years ago
dehnert 316412c5d3 fixed a bug related to closing symbolic Markov automata
7 years ago
dehnert 09866e4577 enabling changing value type in quotient extraction of dd-bisimulation
7 years ago
dehnert 2e15674580 fixed an issue in state-act reward refinement for nondet models
7 years ago
dehnert 207b608e20 using sylvan way of computing cache/table sizes given a memory bound
7 years ago
dehnert ea21aca117 second attempt at fixing issue when not reusing blocks
7 years ago
dehnert 6638984b8e fixed an issue in sylvan refiner when not reusing block numbers
7 years ago
dehnert d6f2261ca9 enable representatives in quotient extraction also for MDP/MA
7 years ago
dehnert 66e08f9cd7 more time output in dd-based bisimulation
7 years ago
dehnert 34b6593ed8 overhauled output of dd-based bisimulation for benchmarking
7 years ago
dehnert 27d6e48dad workaround for quotient extraction using the original variables
7 years ago
dehnert 10f8ddc343 started on quotient extraction using the original variables, debugging CUDD...
7 years ago
dehnert 8482063a16 made symbolic bisimulation work with MA and support of sparse quotient extraction for MA
7 years ago
dehnert 9e5e1980dd first working version of symbolic Markov automaton bisimulation
7 years ago
dehnert 2a209d18e1 fixing some bisimulation issues
7 years ago
dehnert cd34e3d67e fixed issue in rational search preventing convergence in many cases
7 years ago
TimQu 68ec4ca0ce Various fixes for the case STORM_USE_CLN_EA=ON
7 years ago
TimQu fe95a4e4a7 fixed some number conversions that did not work for CLN numbers
7 years ago
Joachim Klein f56076aacf Add virtual destructors to classes having virtual functions.
7 years ago
dehnert eaee9bb2c2 removed parallel flag for bisimulation as this is now governed by sylvan:threads already, fixed bug in DD traversal
7 years ago
dehnert 0d5a4ef242 more work on sigrefmc integration
7 years ago
dehnert 99f45fea3c started integrating parallelism implementation of sigrefmc by Tom van Dijk
7 years ago
dehnert 1d1b17a707 fix some multi-threading issues
7 years ago
dehnert 05f2f241cb fixed some recently introduced issues
7 years ago