dehnert
97e302a78c
guarded timeouts in z3 by ifdef-guards
Former-commit-id: 1bf463686a
9 years ago
sjunges
703013b97c
program, vector, gurobi
Former-commit-id: 6cfaf78d59
9 years ago
dehnert
59501dd347
removed some object files of xerces. started working on smt-based permissive schedulers
Former-commit-id: de95333225
9 years ago
sjunges
14639525b6
Revert "xerces on gitignore fix"
This reverts commit 82f2927500
[formerly c2cc388ce7
].
Former-commit-id: 9e76890660
9 years ago
dehnert
82f2927500
xerces on gitignore fix
Former-commit-id: c2cc388ce7
9 years ago
sjunges
e9b4aa5de4
xerces 2nd part
Former-commit-id: bcd783c277
9 years ago
sjunges
73073d2fff
Added Xerces
Former-commit-id: 9e5eeb3b86
9 years ago
sjunges
288f34b083
Added Xerces
Former-commit-id: 42a3347ab6
9 years ago
sjunges
e8408cdc7b
gurobi 6.05 for mac os support - second try
Former-commit-id: 1dc5be581a
9 years ago
sjunges
4425368e0c
gurobi 6.05 for mac os support
Former-commit-id: 29afa71b2d
9 years ago
sjunges
bdb105ce85
cmake: marked several variables as advanced
Former-commit-id: 8f6c063472
9 years ago
sjunges
0a061274b6
support for downloaded version of z3
Former-commit-id: d8dc5e03d9
9 years ago
sjunges
7722165256
Support for gurobi 602
Former-commit-id: 915d3a48dd
9 years ago
dehnert
f9f5a4e206
reincluded tbb in gmm. fixed missing header. extended formula parser to return multiple formulas
Former-commit-id: a2849d6534
9 years ago
sjunges
c7becb3c60
improved cmake for z3 and gurobi
Former-commit-id: d85982abd2
9 years ago
dehnert
bb7d4c3b0e
update for gmm++: 4.2 to 5.0
Former-commit-id: 542b048470
9 years ago
David_Korzeniewski
7521be7408
Fixed some problems on windows.
Former-commit-id: 0fe6f3593d
9 years ago
dehnert
d7f1012509
got rid of more warnings
Former-commit-id: 514624a4b1
9 years ago
dehnert
56b4f53ce7
got rid of more warnings
Former-commit-id: 5c39f63c69
9 years ago
sjunges
1bb4d2c0ae
silenced glpk warnings for clang on OSX
Former-commit-id: 824def99bf
9 years ago
dehnert
21627fbab4
Started to get rid of some warnings. In particular this means making the compiler more silent for third-party stuff.
Former-commit-id: 2b6ca07d06
9 years ago
sjunges
9c0b5b028c
Finding z3 in system, cleaned some cmakelists.
Former-commit-id: 67ab9f7a0c
9 years ago
PBerger
3bb0346407
Fixed missing typenames and member initialization reordering.
Former-commit-id: bdf24399d6
10 years ago
David_Korzeniewski
d4f051c4f0
Fixed Windows build
Former-commit-id: 53c99736de
10 years ago
dehnert
d787b80fec
CTMC examples now build properly using the DD-based model generator.
Former-commit-id: ac97b005e3
10 years ago
dehnert
913aa83dbc
Removed ltl2dstar.
Former-commit-id: 2045babf36
10 years ago
David_Korzeniewski
95d5ebbb7d
Updated build instructions with list of tested compilers and some new dependencies, but it still looks partially outdated.
Former-commit-id: 1931f71cf9
10 years ago
David_Korzeniewski
8ebc0e4640
Final touches on cuda nondeterministic linear equation solver & modelchecker
Former-commit-id: c549ae0401
10 years ago
PBerger
f7adf54be3
Added A FindGurobi file for CMake.
Adapted build process to use the new file to support all version of the library (upgrading to 6.0 breaks everything).
Former-commit-id: 820ad02968
10 years ago
dehnert
f5f2a2dd4c
Added expression evaluation (header-only) library exprtk and a corresponding evaluator class.
Former-commit-id: 950d1af6e0
10 years ago
David_Korzeniewski
5299ed5172
Adapted FindCusp to fail silently if cusp is not found. Now configuring fails with a meaningful error message instead of syntax errors.
Former-commit-id: e77388a186
10 years ago
David_Korzeniewski
2e92d66bf3
Cmake scripts for linking mathsat and gmp or mpir which is required by mathsat
Former-commit-id: b13b68115a
10 years ago
PBerger
ed3df5f155
Last push :)
Former-commit-id: 72c4b69cb2
10 years ago
PBerger
493f93a94b
Added __restrict__ keyword to CUDA kernel. This should enhance compiler optimization.
Refactored TopologicalValueIterationNondeterministicLinearEquationSolver to support "down-casting" to float.
Added better timing output.
Former-commit-id: 688c40decb
10 years ago
PBerger
ea427fcde1
Fixed include directories for CUDA Plugin in CMakeLists.txt
Refactored all code related to the SPMV kernels to work with float.
Wrote a test that determines whether the compiler uses 64bit boundary alignments on std::pairs of uint64 and float.
Introduced functions that allow for conversions between different ValueTypes (e.g. from float to double and backwards).
Former-commit-id: 830d24064f
10 years ago
PBerger
73ddba5b29
Merged master, applied fixes.
Added feedback from the cuda plugin and return of iteration count.
Former-commit-id: 711ca3d9ec
10 years ago
PBerger
d2f4c85711
Made changes to comply with new SparseMatrix Interface (YUCK).
Fixed tests, all that stuff.
Former-commit-id: c78de5f8ce
11 years ago
dehnert
6078e07476
First version of DD iterator; small test included.
Former-commit-id: 2ec2323886
11 years ago
PBerger
f2383ccfb5
Added missing definitions required for CUDD to compile under 64bit architectures.
Former-commit-id: 4e40ea7ee3
11 years ago
dehnert
5fe7ffe51a
Added missing function declaration in CUDD'c C++ interface. Started on an iterator for DD valuations.
Former-commit-id: a97ccdec3d
11 years ago
dehnert
61d4bb956c
Added functionality to compare two ADDs up to a given precision. Added logical operator overloads to DD interface. Added tests for all new features.
Former-commit-id: 738ad49d62
11 years ago
dehnert
5a4730ae22
When exporting DDs to the dot format, edges leading to the zero node are now suppressed. Also, nodes in the dot file are now labeled with variable names (+ the number of the bit).
Former-commit-id: 410d61d333
11 years ago
PBerger
94b25c02ca
Fixed bugs in some files.
Made LTL a little better to compile under WIN32.
Former-commit-id: 71377f0672
11 years ago
dehnert
88d9f36ef4
Added min/max abstract over DD variables to CUDD (actual code taken from PRISM). Added more tests for DD layer. Fixed some bugs in the DD layer.
Former-commit-id: a4b7810137
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.
Refactored the CUDA-SCC grouping algorithm as is took 80x longer to calculate the groups than it took to calculate the entire solution.
Former-commit-id: 5a5ffabe38
11 years ago
PBerger
0922921b24
Updated cudaForStorm/CMakeLists.txt to make use of the new GIT based version schema.
Added version functions to the Cuda Plugin.
Edited storm.cpp to show version infos for the CUDA Plugin.
Fixed a critical error in basicValueIteration.cu which causes random SEGFAULTs... :P
Streamlined the TopologicalValueIterationNondeterministicLinearEquationSolver.cpp. The SCC group optimizer now returns flat_sets instead of a vector as the sets are ordered, which is required for the Solver to work.
This is now a stable version of StoRM containing a fully wor
Former-commit-id: 47d5c2825c
11 years ago
PBerger
05814f5d73
Fixed a bug in the equalModuloPrecision function of the CUDA Kernel
Added more debug output to the CUDA handler functions
Added a function for grouping of SCCs for better performance
Added functionality and accessors to the SparseMatrix
Former-commit-id: 770aec1b09
11 years ago
PBerger
d3f513b0a0
Added debug output to CUDA Kernel.
Added a performance test for the CUDA stuff.
Former-commit-id: 9953befdea
11 years ago
PBerger
b63a6179d8
Fixed a possible bug in the equalModuloPrecision comparison of vectors.
Same for the CUDA Kernel, but there all hell broke free.
Former-commit-id: 6cb21c3919
11 years ago
PBerger
208005e68b
Added Tests to the Cuda Plugin.
Refactored kernel for SpMV to use two vectors for column indexes and values.
Former-commit-id: 3560d3cc9a
11 years ago