dehnert
a4fec9f080
Started writing functional tests for DD abstraction layer and fixed some bugs on the way.
Former-commit-id: 8a2fc118be
11 years ago
dehnert
2fcb12e875
Fixed some backslashes in includes to slashes and changed indentation of some code.
Former-commit-id: 0e4828e368
11 years ago
dbohlender
39aac5857b
Merge branch 'master' of https://sselab.de/lab9/private/git/storm
Former-commit-id: 9c473ea499
11 years ago
dehnert
dd15e60193
Removed faulty deletion of cudd utility (is obsolete now anyway).
Former-commit-id: 743c59ceca
11 years ago
dbohlender
7ea7ce93e2
Fixed MSVC incompabilities
Former-commit-id: 67749daab8
11 years ago
dehnert
386fac3935
Removed faulty deletion of cudd utility (is obsolete now anyway).
Former-commit-id: c4dca6c50f
11 years ago
dehnert
d6ff967ef0
Added missing algorithm header inclusion.
Former-commit-id: 32231ecb8d
11 years ago
dehnert
cb35b3315d
Added matrix-matrix multiplication to DD interface. (This includes matrix-vector multiplication as a special case).
Former-commit-id: d5d8fef738
11 years ago
dehnert
ac355a66eb
Further work on DD layer.
Former-commit-id: 061b428763
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
sjunges
32ad2ae1a0
minimal changes to make sparse matrices with polynomials work
Former-commit-id: 6688ebc9fd
11 years ago
dehnert
dea56e1bd4
Added some missing includes and some stubs for additional functionality of DD abstraction layer.
Former-commit-id: d90d525993
11 years ago
dehnert
52cd48c247
Fixed bug in restriction of a program to certain commands. Also, modules may now have an action without actually having a command labeled with the action and the explicit model adapter now handles this correctly.
Former-commit-id: 6bbb4b807c
11 years ago
dehnert
c2c353f6b9
Readded missing file.
Former-commit-id: acc68213d4
11 years ago
dehnert
a63cda69f5
Added function to retrieve range DD for meta variable.
Former-commit-id: 32ef6715f4
11 years ago
dehnert
874fc8a864
Alpha version of DD abstraction layer.
Former-commit-id: 98cc5f3aa7
11 years ago
dehnert
97e4e01250
Further step towards finalizing the abstraction layer for DDs.
Former-commit-id: efd5822b67
11 years ago
dehnert
70fc3ec29a
Further work on abstraction layer for DDs.
Former-commit-id: 245986076b
11 years ago
PBerger
a4a17de4fc
Added timing for PRCTL formula checking.
Replaced std::sort with std::inplace_merge, saving another factor 2.
Former-commit-id: 961c31bb68
11 years ago
dehnert
de44a1562c
Started writing the DD abstraction layer.
Former-commit-id: 8720a38b17
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
Sebastian Junges
e56e8bf71b
boost hash support for multivariate polynommials from carl, typedefs for polynomials when using parametric systems
Former-commit-id: 074758fa36
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
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
masawei
2ed6be853b
Fixed two minor bugs.
- First one concerning the MappedFileTest in which I neglected to consider that the number of characters used to signal a new line differs between Linux (\n -> 1) and Windows (\r\n -> 2) which caused the test to fail on all OS using two characters (hence not on Linux, where I ran the tests).
- Second bug concerned the case that a transition reward file contained more states than the corresponding transition file.
In that case the parser tried to acces the entry of the rowGroupIndices vector behind the last actual entry, which caused an exception to be thrown.
Now there is a check whether the highest state index found by the parser does exceed the highest state index of the model.
Former-commit-id: bc83267f3c
11 years ago
PBerger
24ae4e4ae3
Merge branch 'master_working' into philippTopologicalRevival
Conflicts:
src/modelchecker/prctl/TopologicalValueIterationMdpPrctlModelChecker.h
src/solver/NondeterministicLinearEquationSolver.h
src/storage/SparseMatrix.h
src/storm.cpp
src/utility/vector.h
Former-commit-id: a4c707fe76
11 years ago
PBerger
cd46a6b0c6
Fixed a bug in the equalModuloPrecision function.
Former-commit-id: 465d90b4a7
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
masawei
db1bb8b70e
Merge branch 'master' of https://sselab.de/lab9/private/git/storm
Former-commit-id: b639e5a703
11 years ago
masawei
8f171c7dc5
Finished initial remerge.
- Fixed comments.
- It seems to be ASSERT_EQ(expected, actual);
|-> Switched arguments of nearly all ASSERT_EQs to correctly use this macro in the parser tests.
Former-commit-id: e5059709f2
11 years ago
PBerger
e45fa5a82c
Added a Test for the CUDA Plugin.
Added accessors for the SparseMatrix as I need access to the internal vectors.
Added a pure SPMV Kernel interface to check the kernel for errors.
Former-commit-id: 46e1449eeb
11 years ago
masawei
28910462ec
Necessary changes to the nondeterministic parses to compensate for the change in the way the mapping between states of the model and the rows of the transition matrix are handled.
- All tests are green.
- Some comments are now a bit wrong.
Next up: Correct comments.
Former-commit-id: 610c0282b2
11 years ago
PBerger
c0a7e42486
Implemented a basic but complete kernel for value iteration in CUDA.
It doesnt work :(
Former-commit-id: 6a3a7aa505
11 years ago
PBerger
71e077f420
Compiles with CUSP :)
Former-commit-id: 78555303bf
11 years ago
PBerger
a964846e2d
Added cusplibrary as a git submodule.
Former-commit-id: 152764c8f3
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
masawei
08168f5511
Merge branch 'refactureParsers'
Conflicts:
src/parser/MarkovAutomatonParser.cpp
src/parser/MarkovAutomatonSparseTransitionParser.cpp
src/parser/MarkovAutomatonSparseTransitionParser.h
src/parser/NondeterministicModelParser.cpp
src/parser/NondeterministicModelParser.h
src/parser/NondeterministicSparseTransitionParser.cpp
test/functional/storage/MaximalEndComponentDecompositionTest.cpp
Former-commit-id: db4aea7faa
11 years ago
masawei
6444fc5197
Last fixes and changes.
- Some renaming (among others unmatched -> mismatched).
- Added checks and tests for doubled or skipped lines as well as lines concerning the same transition.
Next up: Remerge.)
Former-commit-id: 05efcbf91c
11 years ago
masawei
ff1ba43940
Lots of renames.
Former-commit-id: 1fb2726396
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
63933637ac
Fixed a bug in the SparseMatrix.cpp. When using TBB the typename is not permitted.
Former-commit-id: e191c14e1d
11 years ago
PBerger
84a794164c
Updated the BUILD.txt file with current information.
Former-commit-id: efa4d0b2e4
11 years ago