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
masawei
175e852956
Resolved problems resulting from merge.
- gcc 4.8 (and assorted libraries) does not provide an erase(const_iterator) method for std::list but only an erase(iterator).
This is in compliance with the c++11 draft N3337, which specifies the change from iterator to const_iterator only for "set, multiset, map [and] multimap" but not list.
Therefore the constant list iterators were replaced by non constant iterators in MaximalEndComponentDecomposition and Vector set.
The locations are marked with a FIXME, such that the const_iterator can be replaced back when gcc provides it.
- Fixed (completed) the stub implementation for the GurobiLpSolver in case that Gurobi is not present.
|-> Would not compile before due to missing functions and incorrect signatures.
- Switched to c++11 for gcc. Since gcc 4.8 provides full compliance to the c++11 standard.
|-> Initially hoped that it would fix the const_iterator problem, but it did not.
- Fixed the cmake warning concerning a missing whitespace between tokens in the last line of CMakeLists.txt.
Former-commit-id: f90768375e
11 years ago
David_Korzeniewski
9e66447eb2
Add "lib" prefix for z3 only on Windows
Former-commit-id: bdfa503070
11 years ago
David_Korzeniewski
7c0dd5eaf5
Fixed build errors on Windows
Former-commit-id: 10929f075d
11 years ago
dehnert
bc94f69c0b
Resolved some ambiguities that produced problems under Linux. Added option USE_LIBCXX to CMakeLists.txt to also use libc++ under Linux.
Former-commit-id: 2e06d7adf6
11 years ago
dehnert
5cd18c1cf5
Resolved some ambiguities that produced problems under Linux. Added option USE_LIBCXX to CMakeLists.txt to also use libc++ under Linux.
Former-commit-id: f2f7bb6d80
11 years ago
dehnert
47a05fc1b0
Beautified output of option system. Enabled command line interface of counterexample generation.
Former-commit-id: cecc5e85b3
11 years ago
dehnert
2e570f6311
Merge.
Former-commit-id: 572cdb80fc
11 years ago
dehnert
a45e9423b8
Sparse matrix can now also be used without knowing the number of rows/columns/nonzeros upfront. Adapted ExplicitModelAdapter to use that capability to not explore the state space twice. Added support for Z3 to CMakeLists.txt. Added correct submatrix checks for transition rewards in MDPs. Extended a test for the ExplicitModelAdapter a bit.
Former-commit-id: 105efc5342
11 years ago
PBerger
79c40126f3
Fixed a bug in the SparseMatrix.h where the multi threaded implementation would crash sometimes
Added a new definition to CMakeLists.txt for MSVC as to undefine the MIN/MAX macros
Former-commit-id: 5a3d12e920
11 years ago
PBerger
c242dcbd97
Refactored CMakeLists.txt for better editing and overview
Refactored all Defines for Gurobi, TBB, etc into the storm-config file
Fixed a missing cast int SymbolicModelAdapter.h
Fixed changed iterator structures in SparseMatrix.h
Fixed bugs in CuddUtility.cpp where a 64bit shift was executed on a 32bit literal (1 should be 1ull)
Fixed a Type Error in graph.h
Former-commit-id: 797b4da2eb
11 years ago
PBerger
6fca000233
Removed defines.hxx from source tree
Added a new include path for storm as to include the generated out-of-source defines.hxx
Former-commit-id: 1a75f61da0
11 years ago
dehnert
6e41ee360d
Fixes to several problems with gcc.
Former-commit-id: f7908fdc6f
11 years ago
dehnert
0ac3efb082
Finished merge of CMakeLists.txt
Former-commit-id: c4f903e8c5
11 years ago
PBerger
ef850b213b
Added the option -ftemplate-depth=1024 for Clang
Former-commit-id: 063b420dea
11 years ago