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
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
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
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
6e41ee360d
Fixes to several problems with gcc.
Former-commit-id: f7908fdc6f
11 years ago
0ac3efb082
Finished merge of CMakeLists.txt
Former-commit-id: c4f903e8c5
11 years ago
ef850b213b
Added the option -ftemplate-depth=1024 for Clang
Former-commit-id: 063b420dea
11 years ago
b79fde1a42
Added a definition for GTest to build with MSVC on Windows
Former-commit-id: 5ccb773886
11 years ago
11198c648c
Fixed include pathes for CUDD in CMakeLists.txt
Added a variadic macro for MSVC since the PrismGrammar makes use of emplace magic
Patched log4cplus to disable unicode from a parent project
"Patched" various serious issues in CUDD, where size_t <-> int problems and forced int to bool conversions piss of the compiler. And me.
Former-commit-id: eb27e77ddd
11 years ago
659df778dd
Refactored all in-repository includes to make use of CMakes great features
Former-commit-id: 2b1ec4649a
11 years ago
735cd2013f
Further work on minimal label set generator. Intermediate commit.
Former-commit-id: 0f123ae3c4
11 years ago
85e674266d
Added support for linking against Gurobi to CMakeLists.txt. Prepared work on the generator of minimal label sets.
Former-commit-id: a7a87edcfe
11 years ago
edeedd2bed
Added ConversionHelper.h to single out the needed no-strict-aliasing target
Replaced a few "auto" variables as GCC4.7 fails to infer the correct type
Former-commit-id: 09a0c8dac9
11 years ago
82053c4822
Fixed missing suffix for static library of log4cplus.
Former-commit-id: 013a34bf58
11 years ago
df21fbbbde
Added new version of Log4CPlus, updated from v1.1.0 to v.1.1.2-rc2
Updated CMakeLists.txt, included new Log4Cplus
Former-commit-id: 55cc5a74d3
11 years ago
e69c9f1962
Added all options from StoRM
Rewrote all calls to the Settings instance with the new Syntax
Implemented new ArgumentValidators.h
Former-commit-id: b4ab63f8f2
11 years ago
bde10b750e
Added my initial implementation of Settings
Former-commit-id: 5da4b7604f
11 years ago
6af5ce4860
Another container for which gcc does not support emplace yet...
Former-commit-id: 3914bf9737
12 years ago
abf6f85b63
Intermediate commit to switch workplace.
Former-commit-id: 11932e19d7
12 years ago
42b9072cbf
Implemented TBB Parallelization Support into SparseMatrix.h
Re-factored Includes in CMake for TBB
Former-commit-id: b5ebf4153a
12 years ago
4b68cb7bbf
Removed all references to LTL2DStar in Master branch
12 years ago
30e69ee4d4
Corrected CMakeLists.txt (from merge)
12 years ago
a96380259a
Added ltl2ba and ltl2dstar to ressources
12 years ago
ec91dcbe2e
Merge branch master into LTLParser
12 years ago
d3c80dca16
Updated CMakeLists.txt
- Added more sub-folders in the source-structure
- Added an option for MSVC to use /bigobj with the Compiler as PrismParser.cpp bloats the object instance count
- Edited CUDD Link Targets for MSVC
Edited SymbolicModelAdapter.h, added an alternative implementation for log2 (NOT part of C90, not of Cxx!)
Edited Program.cpp, promoted vars from int to uint to conquer warnings related to loss of precision
Likewise in DeterministicSparseTransitionParser.cpp, IntegerConstantExpression.h
Edited storm.cpp, reimplemented Usage-Query for non-Unix platforms.
Edited CuddUtility.h, added an include for int Type definitions as they do not fall from the sky
Edited ErrorHandling.h. reimplemented ErrorHandling for non-Unix platforms. Backtraces can not yet be provided.
12 years ago
b5baae5861
Added 3 missing example files for synchronous leader election protocol. Set release optimization level for clang to O3.
12 years ago
6ba1cf25c8
Added new variable for base bath for project root. Changed test input files to the files from example folder. Added leader4.lab to asynchronous leader election example.
12 years ago
3851377064
Introduced executable storm-functional-tests and storm-performance-tests. While the former contains the previous tests, the latter is currently empty, but will hold performance tests in the future.
12 years ago
27de566228
Moved current tests to the functional test suite in an attempt to introduce performance tests.
12 years ago
5f27a932a9
Moved SCC decomposition to AbstractModel class, which was possible due to virtual iterator facilities in model classes.
12 years ago
4c0d7f6d95
adding cudd linker options for storm-tests
12 years ago
1642c5f66c
Added missing functions to CUDDs cpp interface
12 years ago
cfb721a66e
Turn off Cotire by default (because it triggers internal compilation errors not only in clang, but also in gcc 4.7). Signed-off-by: dehnert.
12 years ago
e2f95e065f
Modified CmakeLists.txt to actually also link the libraries of TBB if requested. Included custom build of TBB for Mac OS using Apple clang 4.2 (based on clang 3.2).
12 years ago
2a8920aeef
Updated CMakeLists.txt, added an option for Intel TBB
Edited gmm_blas.h, reordered includes
12 years ago
f5910e8da1
Added Intel TBB 4.1 Update 3 with Binaries for Windows, Linux and Mac OSX.
Updated CMakeLists.txt to include default paths.
12 years ago
7dc36875ae
Added file groups in CMakeLists.txt such that files are now grouped in IDEs, like, e.g., Xcode.
12 years ago
2b4d26023a
Fixed one of the remaining bugs introduced by refactoring.
12 years ago
5cdfba685e
Added resources for Usage of Intels Thread Building Blocks
Implemented multithreading using TBB inside of GMM for usage in Sparse Matrix Multiplication against Dense Vectors
Usage: #define GMM_USE_TBB to enable TBB, additionally define GMM_USE_TBB_FOR_INNER to enable multithreading for EACH row (only feasible of the number of NNZ per Row is large - as in near dense)
12 years ago
490f037259
Kind of undoing the previous commit.
gcc can only link, if -lobj is the first cudd lib to be linked...
Now, all the object files can be removed from libobj.a
12 years ago
f5ab82c163
As I was a bit puzzled: make CMake print out the used compiler
12 years ago
5315fa5f9e
undoing previous commit. Just ignore those...
12 years ago
0c9f84a5c6
Building with DEBUG totally breaks everything in g++.
12 years ago
7d95a45633
Fixed bug in AbstractModelChecker: it does now correctly inherit from a lot more interface classes. NOTE: checking a formula on a model checker that does not support it failed silently. This should NOT be the case. Re-enabled DEBUG option for cmake. NOTE: why was this disabled anyway? Introduced another layer AbstractDeterministicModel and AbstractNonDeterministicModel in model hierarchy to allow for easily distinguishing these classes. Made necessary adaptions in (hopefully) all classes. Move the graph analyzer to utility folder.
12 years ago
dbd6c02f6a
Updated CMakeLists.txt, Cotire Usage is now restricted to Linux/Windows and deactivated on APPLE systems.
12 years ago
7f956b0d35
Added Cotire to Storm to build PCH on all plattforms.
Edited the ConstTemplates.h as the new compilation order breaks because of some min/max macros.
12 years ago
21e0ecd9f0
Change in CmakeLists.txt: When building debug, add -g as CXX flag (For
clang)
12 years ago
726569d5f1
Fixed bug in parser that inserted 0-entries on the diagonal at the wrong places. Enabled link-time-optimizations for Release-Build when using clang. Fixed bug in base exception: what() returned a pointer to a char array belonging to a local variable, which got deallocated and thus invalidates the char array content.
12 years ago
edd3a9a20e
Added possibility to evaluate expressions without concrete variables. Fixed some minor things in CUDD Makefiles. Renamed IR adapter.
12 years ago
3a73e0838c
make memcheck targets call the binaries with -v and --fix-deadlocks
12 years ago
dehnert
PBerger
Lanchid
gereon
david