sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
2271 Commits
2 Branches
0 Tags
187 MiB
Tree: 10e93d7cbb
Branches Tags
${ item.name }
Create tag ${ searchTerm }
Create branch ${ searchTerm }
from '10e93d7cbb'
${ noResults }
Commit Graph

189 Commits (10e93d7cbb579ef528187a7fe0ba150925f03f80)

Author SHA1 Message Date
PBerger 73ddba5b29 Merged master, applied fixes.
11 years ago
dehnert aecd0e3cb8 Made Storm compile again without Z3: guarded some header inclusions and function definitions/implementations. Also guarded the tests that require certain libraries (like Gurobi, glpk, Z3), so that tests do not fail any more when the libraries are not available.
11 years ago
dehnert 40c698af90 Some fixes to make new SMT framework compile with clang under Mac OS (includes fixes to some initializiation ordering warnings). Bugfix for PRISM parser to correctly handle formulas.
11 years ago
David_Korzeniewski 3887cb57aa Fix for temporaries and non const references
11 years ago
David_Korzeniewski 52d3d91060 Implemented Unsat Core/Assumtions & simple test
11 years ago
PBerger d2f4c85711 Made changes to comply with new SparseMatrix Interface (YUCK).
11 years ago
David_Korzeniewski a815a6f425 Implemented allSat with z3 and test
11 years ago
David_Korzeniewski 93c03fff3f Fixed order of checks in Z3ExpressionAdapter, fixed missing override of isVariable in VariableExpression, removed unnecessary exception in Z3SmtSolver model generation
11 years ago
PBerger b7ad4398e2 Fixed an error in the interface of the LpSolvers.
11 years ago
David_Korzeniewski a0319cb6e7 Model Generation and Tests for translating from z3 to storm
11 years ago
David_Korzeniewski 9a7b4f69ef More tests and some small bugfixes for Z3SmtSolver
11 years ago
David_Korzeniewski 45bc8ea665 Conditional compilation for all parts using z3 by checking STORM_HAVE_Z3
11 years ago
David_Korzeniewski 37ef3feebb Fixed return type of addBinaryVariable
11 years ago
David_Korzeniewski 4e6c9b7d6b Implemented translating z3 expressions to storm expressions
11 years ago
dehnert 66d6fa3bb4 Fixed wrong type.
11 years ago
dehnert 9e746549a8 Fully adapted MILP-based counterexample generator to new LP solver interface.
11 years ago
dehnert 29d8111991 Adapted Gurobi and glpk LP solvers to expression-based interface. Adapted tests and made them work again.
11 years ago
dehnert d5c2f9248f Finished linear coefficient visitor and adapted glpk solver to new expression-based LP solver interface.
11 years ago
dehnert 3158d19123 Started working on adapting LP solver interface to new expressions.
11 years ago
David_Korzeniewski 29083cc89c Implemented asserting expressions and checking satisfiability with z3
11 years ago
David_Korzeniewski 98f87a5e6d Adapted Z3ExpressionAdapter for new expressions
11 years ago
David_Korzeniewski f69b79593c initial interface for smt solver wrappers
11 years ago
dehnert 33cce28df8 Fixed minor bug MILP-based minimal command set generator. GurobiLpSolver is now able to deal with constraints involving several instances of the same variable.
11 years ago
sjunges 0eb13c6415 fixed a lot of unused variable warnings
11 years ago
PBerger a4a17de4fc Added timing for PRCTL formula checking.
11 years ago
PBerger 26500ff4a8 Refactored the CUDA Kernel to once again use the "hacked" combination of column indices and values with a bit of reinterpret_cast magic.
11 years ago
PBerger 0922921b24 Updated cudaForStorm/CMakeLists.txt to make use of the new GIT based version schema.
11 years ago
PBerger 05814f5d73 Fixed a bug in the equalModuloPrecision function of the CUDA Kernel
11 years ago
PBerger d3f513b0a0 Added debug output to CUDA Kernel.
11 years ago
PBerger c0a7e42486 Implemented a basic but complete kernel for value iteration in CUDA.
11 years ago
dehnert 12743e0a7e Moved from additional row grouping to the one embedded in the matrix itself.
11 years ago
PBerger 68a6e533be Added error handling in GurobiLpSolver.cpp
11 years ago
PBerger a6e7e6b4e0 Edited GurobiLpSolver.cpp, added the error code to the messages.
11 years ago
PBerger af650b6666 Removed debug outputs from the TopologicalValueIterationNondeterministicLinearEquationSolver
11 years ago
PBerger a4ae226e57 Removed debug output from our debugging session
11 years ago
dehnert f049a9f0af Bugfix for topological equation solver.
11 years ago
PBerger 98b0bcf187 Reimplemented the TopologicalValueIterationNondeterministicLinearEquationSolver with splitting into submatrices.
11 years ago
dehnert 17d9df1ac7 Some fixes to make the branch compile with clang.
11 years ago
PBerger 4eef3b0d57 Added an example for SCC related testing which will change soon
11 years ago
PBerger 57b6208eee Added a pseudo model which can be constructed from only a matrix to look and behave like a model for use in Decomposition classes
11 years ago
PBerger 64891af785 Trying to refurbish the TopologicalValueIterationMdpPrctlModelChecker
11 years ago
PBerger 9d1e53cff9 Added a missing include for uint_fast64_t to be recognized as a type
11 years ago
dehnert 486e99d6ae Added signal handler for SIGTERM. Introduced delayed update for LP solvers to reduce overhead.
11 years ago
dehnert 42708a6d21 Added utility header for all parts that use std::swap.
11 years ago
dehnert 36fb44e206 Added functional tests for nondeterministic linear equation solvers. Added functional tests for LPs in addition to the existing MILP tests.
11 years ago
dehnert 514aace4fd Added function tests for both glpk- and Gurobi-based LP solver implementations. Found and fixed some bugs while doing this.
11 years ago
dehnert c5985be437 Minor fixes for GlpkLpSolver.
11 years ago
dehnert 8ebd924ca6 Further work on refactoring solvers: cleaned LP solver interface a bit and adapted glpk- and Gurobi-based implementations of the interface.
11 years ago
dehnert 588a4b60b6 Refactored linear equation solvers and nondeterministic linear equation solvers. Added functional tests for both.
11 years ago
dehnert 79730379e4 Started refactoring the linear equation system solvers.
11 years ago