sjunges
|
a129983ae9
|
cleaning includes for better compilation times
Former-commit-id: e2878ae043
|
10 years ago |
dehnert
|
507331d8a9
|
more debug output
Former-commit-id: acb7f9ea2f
|
10 years ago |
dehnert
|
13514c9da8
|
hybrid CTMC model checker can now do lra as well
Former-commit-id: 6e898a2a6d
|
10 years ago |
dehnert
|
6c4162fae4
|
more work towards steady state for CTMCs
Former-commit-id: c3e17d1fc0
|
10 years ago |
dehnert
|
dd399c5f85
|
Finalized hybrid MDP model checker. It passes its tests now.
Former-commit-id: 47de0b9433
|
10 years ago |
dehnert
|
2bf7eafb4b
|
Further work on hybrid MDP model checker.
Former-commit-id: 3192a13f55
|
10 years ago |
dehnert
|
e3320ee086
|
Started working on hybrid MDP model checker.
Former-commit-id: 63a8efb93c
|
10 years ago |
dehnert
|
869f8c50c9
|
Fixed some minor CTMC-related bugs.
Former-commit-id: 3abb948542
|
10 years ago |
dehnert
|
76b99a5515
|
Commit to switch workplace.
Former-commit-id: e80da5e90b
|
10 years ago |
dehnert
|
c1917ce6d9
|
Finalized hybrid DTMC model checker. It now passes its tests.
Former-commit-id: 99d79e1bc6
|
10 years ago |
dehnert
|
72166bed37
|
Created new class for storing hybrid check results (symbolic as well as explicit parts) and the surrounding functionality.
Former-commit-id: d4ad6da5a1
|
10 years ago |
dehnert
|
3b4dca1a03
|
Improved Jacobi method a bit.
Former-commit-id: f4affeebf6
|
10 years ago |
dehnert
|
06bfc17ec6
|
Started making hybrid (dd/sparse) model checking work.
Former-commit-id: 23fac3a672
|
10 years ago |
dehnert
|
907e3512c0
|
Fixed a potential bug in the ODD generation and it now uses hash maps instead of regular maps.
Former-commit-id: f8e5fb3018
|
10 years ago |
dehnert
|
e83d191be3
|
ODDs can now also be constructed from BDDs directly (without a transformation step to ADDs).
Former-commit-id: d19bbc3ff5
|
10 years ago |
dehnert
|
c8d8f75a10
|
Working on ODD generation for BDDs (not yet working).
Former-commit-id: 5665dd1f24
|
10 years ago |
dehnert
|
d787b80fec
|
CTMC examples now build properly using the DD-based model generator.
Former-commit-id: ac97b005e3
|
10 years ago |
dehnert
|
60701cebdb
|
ADDs and BDDs are no longer mixed in the abstraction layer.
Former-commit-id: 3c31063ea6
|
10 years ago |
dehnert
|
5bd6ca606f
|
Started refactoring DD abstraction layer.
Former-commit-id: 60f7713c24
|
10 years ago |
dehnert
|
c70d93f4d3
|
Qualitative modelchecking algorithms for MDPs using BDDs. Not yet bugfixed.
Former-commit-id: 3215a38c44
|
10 years ago |
dehnert
|
c8007876ae
|
Symbolic models can now be built from the command line.
Former-commit-id: 2c239df754
|
10 years ago |
dehnert
|
706ea56963
|
Now DDs are either MTBDDs or BDDs. This makes it possible to use BDDs where possible, which is faster.
Former-commit-id: 07ffb5882d
|
10 years ago |
dehnert
|
e58d38fadf
|
More work on integrating DD-based model building.
Former-commit-id: 84f5a5c603
|
10 years ago |
dehnert
|
6347e19da8
|
Intermediate commit: integrating MTBDD model generation/model checking to main tool.
Former-commit-id: a312d3a425
|
10 years ago |
dehnert
|
b37e009168
|
Further steps to new expressions.
Former-commit-id: 4396857eff
|
10 years ago |
dehnert
|
8e71081f1e
|
Functional tests now work again.
Former-commit-id: 46d964ad22
|
10 years ago |
dehnert
|
ed74392f0d
|
Another intermediate commit.
Former-commit-id: 37585dbfa0
|
10 years ago |
dehnert
|
99d9a9710d
|
Further steps to make everything work again.
Former-commit-id: 3f45a49dab
|
10 years ago |
dehnert
|
7ec3e8b214
|
Further fixes for new variable handling. libstorm now compiles again, yay.
Former-commit-id: a9ac5c0356
|
10 years ago |
dehnert
|
7ea6ec3644
|
Further refactoring.
Former-commit-id: 7769132a68
|
10 years ago |
dehnert
|
e49814d391
|
Modified pctl/csl/ltl options to now take formulas instead of files. Prefixed the macros with STORM_. Moved these macros into a file in the utilities. Modified architecture of the exception classes slightly. Threw away all the contents of main(). This will now be build from scratch.
Former-commit-id: 89d94f7957
|
11 years ago |
dehnert
|
1cd01e3f28
|
Adapted all places that are accessing the settings to the new interface. It now compiles again with a lot of linker errors (because of method bodies that are not yet present).
Former-commit-id: 01a33e479d
|
11 years ago |
dehnert
|
9ad12616e2
|
Renamed files in settings module a bit. Started on the pseudo-modular module-settings.
Former-commit-id: b3162aa86b
|
11 years ago |
dehnert
|
96e1f8faf9
|
Renamed Settings class to SettingsManager.
Former-commit-id: 2b33f4c8d0
|
11 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
|
11 years ago |
dehnert
|
ab58103555
|
Started to pimp matrix. First step: added proper methods setColumn/setValue that operate on a matrix entry and removed the non-const versions of getColumn/getValue. Added a typedef for the index type in the matrix so that it becomes possible to have matrices with a different index type (e.g. 32-bit values).
Former-commit-id: 3cc0fdf9ee
|
11 years ago |
dehnert
|
671797738a
|
Now the parameter that is set for dynamic reordering actually gets passed to CUDD.
Former-commit-id: 46676dc9d1
|
11 years ago |
dehnert
|
caf96c04e0
|
Extended DD interface by methods to generate explicit row-grouped matrices from DDs.
Former-commit-id: 1945d7be6d
|
11 years ago |
dehnert
|
8587f68eb1
|
Fixed toMatrix conversion using ODDs. The next step is to generate non-deterministic matrices, i.e., matrices with row groups.
Former-commit-id: e4a9c5f0ed
|
11 years ago |
dehnert
|
236e7fa290
|
Another step towards generating explicit data structures from DDs using ODDs.
Former-commit-id: 5b7e3e8680
|
11 years ago |
dehnert
|
f12ff82baf
|
Added getNodeCount for ODD and fixed a bug concerning boolean meta variables.
Former-commit-id: 79eb69226b
|
11 years ago |
dehnert
|
5d53c6efa5
|
Added ODD-concept to easily convert between DD-based and explicit formats.
Former-commit-id: f2a2a002b7
|
11 years ago |
PBerger
|
7ab2a84c0f
|
Small beauty fixes to the Cudd Interface
Former-commit-id: 631d5a20bd
|
11 years ago |
dehnert
|
63f55b38f0
|
Removed debug output that was - of course - never there. (You saw nothing!)
Former-commit-id: 9249928f54
|
11 years ago |
dehnert
|
7b2def2b11
|
Added function to retrieve the minterms of a DD as an expression and added corresponding test.
Former-commit-id: afaf1f02a3
|
11 years ago |
dehnert
|
e79fa50999
|
Changed naming of DD variables belonging to one meta variable slightly: only integer-valued meta variables now get a '.i' suffix to denote their i-th bit.
Former-commit-id: 771312ac31
|
11 years ago |
dehnert
|
60b2145461
|
Added function to DD interface that creates a nested if-then-else expression that represents the very same function as the DD. Added a test for this functionality. Added some methods offereded by Cudd to simplify DDs.
Former-commit-id: 4fc816f64b
|
11 years ago |
dehnert
|
1513241985
|
Added functions for more efficiently retrieving the DD for 'greater than constant', 'greater or equal than constant' and 'notZero'.
Former-commit-id: 9d80c29f27
|
11 years ago |
dehnert
|
b1f22c1747
|
Added shortcut DD interface to compute \'greaterZero\' on a DD.
Former-commit-id: 65585533fd
|
11 years ago |
dehnert
|
9e506f40bc
|
Some fixes for MSVC. :P
Former-commit-id: 1429e54f73
|
11 years ago |