dehnert
b5f907d99d
Added propositional model checker. Put some of the new classes in new folders. Fixed an issue that prevented compilation.
Former-commit-id: 517a870d2f
10 years ago
dehnert
8a4706d9c9
A lot of work on model checker interfaces. In particular, the SCC elimination model checker is almost integrated.
Former-commit-id: bbf988c943
10 years ago
dehnert
9026aa9ac9
Adapted first model checker to the new properties.
Former-commit-id: 206d6c9858
10 years ago
dehnert
1699732dce
More work on logic classes.
Former-commit-id: 9d94e02b74
10 years ago
dehnert
320641e597
Started working on modified property classes.
Former-commit-id: cbcf84c2f6
10 years ago
dehnert
00861a7479
Loosened the restriction to always require GMP a bit.
Former-commit-id: 0537ff217a
10 years ago
dehnert
91e177028d
Started refactoring explicit model generator of PRISM models
Former-commit-id: 4ea82670d0
10 years ago
dehnert
53196f5610
Created bit vector hash map and some necessary bit vector methods.
Former-commit-id: 4a9946a743
10 years ago
dehnert
c474920fa4
Started refactoring SMT solvers. Now displaying MathSAT version in CLI.
Former-commit-id: 1736a0bb6b
10 years ago
David_Korzeniewski
b8a74c61c0
Set cuda_root variable in cmakelists to make it show up in the gui when configuring.
Former-commit-id: 29ca44312f
10 years ago
svkurowski
da3542dcec
Integrate CUDA into buildsystem and add example function
Former-commit-id: 2f5acf8dcd
10 years ago
svkurowski
00ec9a7db6
Integrate CUDA into buildsystem and add example function
Former-commit-id: 392acb148a
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
eb9c1de59b
Added Boost DECLTYPE for MSVC.
Former-commit-id: c70dfa5e63
10 years ago
dehnert
d3fc2d8fbf
Fixed small but important bug in SCC decomposition that led to wrong results when using MSVC.
Former-commit-id: 07358dc2e8
10 years ago
dehnert
ba4b71a353
Added boost define BOOST_RESULT_OF_USE_DECLTYPE for gcc.
Former-commit-id: b346362805
10 years ago
dehnert
3dfc6a7b74
Pimped bisimulation a bit.
Former-commit-id: a27ea8b996
10 years ago
sjunges
cafcb3f238
version info extended and moved to cpp, added options flag (although unclear what exactly should be displayed then)
Former-commit-id: 3c82455d24
10 years ago
sjunges
a279b06c03
reenabled parametric solving after merge
Former-commit-id: 6e81008932
10 years ago
dehnert
94902388c7
Some minor changes, still doesn't compile.
Former-commit-id: cfc613fd8e
10 years ago
dehnert
9ad12616e2
Renamed files in settings module a bit. Started on the pseudo-modular module-settings.
Former-commit-id: b3162aa86b
10 years ago
dehnert
96e1f8faf9
Renamed Settings class to SettingsManager.
Former-commit-id: 2b33f4c8d0
10 years ago
dehnert
9569426c86
Moved option registration to the settings class (so it's not deceentralized any longer). This enables to build storm as a library and on top of that build some exectuables, which saves a lot of compile time as soon as several targets have to be built or one switches between targets.
Former-commit-id: 69e0d526c7
10 years ago
dehnert
1cc930f0e4
Added proper source grouping for properties directory. Fixed one performance tests. Started on SCC-based reachability model checker.
Former-commit-id: e48c163783
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
sjunges
7ca6a4edeb
sub part for parameters, working parsing for non parametric systems into a parametric system
Former-commit-id: 7714692e32
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
6e1241211b
Started moving IR and adjusting it to the new expression classes.
Former-commit-id: 24a182701f
11 years ago
dehnert
c8a8beca2a
Started working on new easy-to-use expression classes.
Former-commit-id: 9ee1be5822
11 years ago
sjunges
a528610d98
version is now written into a seperate header file to prevent recompile of many files after a commit
Former-commit-id: a287aacefa
11 years ago
dehnert
4252a2710c
Renamed CPackConfig.cmake to StormCPackConfig.cmake and adapted reference in CMakeLists.txt accordingly. Also, CPackConfig.cmake is now ignored.
Former-commit-id: d24d731950
11 years ago
dehnert
de44a1562c
Started writing the DD abstraction layer.
Former-commit-id: 8720a38b17
11 years ago
Sebastian Junges
419f5c22c8
support for parametric systems to c++
Former-commit-id: 63ddba8832
11 years ago
Sebastian Junges
8458e75309
sets the STORM_HAVE_CARL define for c++. Requires carl for parametric builds now
Former-commit-id: 1974957484
11 years ago
Sebastian Junges
4f167e5545
extended the CMakeLists to include carl when using parametric systems
Former-commit-id: 708cfa0f78
11 years ago
PBerger
1d70331123
Fixed a bug in a Regex.
Former-commit-id: 33793efb16
11 years ago
PBerger
2ad5e57db2
Refactored version handling. Its now done via Tags in GIT.
Added CPack configuration as to build packages on the build servers.
Former-commit-id: f3d9507867
11 years ago
PBerger
9388cd158c
Implementations, implementations.
Former-commit-id: e203636fac
11 years ago
PBerger
9b70810354
Added a compiler directive for GCC to fix a bug occurring in Boost since Version 1.54 with GCC >= 4.7.0 (see https://svn.boost.org/trac/boost/ticket/8774 )
Former-commit-id: 60b0d1416e
11 years ago
PBerger
3f53a44482
Modified CMakeLists.txt, made the variable names a bit more clear. All Storm-related options should be prefixed with STORM_ so that they dont break or influence dependent builds.
Former-commit-id: 9aea43e3e2
11 years ago
PBerger
7c93109773
Updated Intel Threading Building Blocks to Version 4.2.
Edited the FindTBB script to better parse and find the libraries.
TBB now includes builds for Mac @ libc++.
Former-commit-id: 4f573ee6a2
11 years ago
PBerger
59b7ca39d9
Updated log4CPlus to latest version containing bugfixes.
Former-commit-id: 4b588bd66a
11 years ago
PBerger
da9fe04ba4
Removed the extra shell around the Cuda Plugin. Changed include pathes.
Former-commit-id: c7fec9220d
11 years ago
PBerger
f0aa54823e
Added glpk to resources.
Wrote a CMakeLists.txt file for GLPK that works with MSVC, GCC and Clang.
Former-commit-id: a9884f3736
11 years ago
PBerger
8781aa27b6
Added cudaForStorm as a dynamic library extension
Former-commit-id: 31c6be4c1c
11 years ago
dehnert
72531bcebb
Added proper TBB multi-threading to all operation relevant to model checking MDPs.
Former-commit-id: dcb4bde1d3
11 years ago
dehnert
cdc369b96a
Temporarily removed the detection of the repository version of TBB from CMakeLists.txt. Corrected TBB sparse matrix-vector multiplication. Added TBB parallel vector addition.
Former-commit-id: f90ae764c8
11 years ago
dehnert
cf2b84b281
Further work on iterators for sparse matrix.
Former-commit-id: 8e78262161
11 years ago
dehnert
e08b61b9f7
Added functional and performance tests for sparse matrix.
Former-commit-id: dd9abe1826
11 years ago
dehnert
b3601782a9
Added Lp Solver class for glpk and added it as an option in CMakeLists.txt.
Former-commit-id: e5c5215a29
11 years ago