3c32eec8e1
Made the prob0/1 algorithms for MDPs share a common backward transition object.
12 years ago
fbe1f41213
Removed GraphTransition class, which is now replaced by SparseMatrix in the instances where it was used before. Changed GraphAnalyzer accordingly and adapted tests.
12 years ago
ed4c6c8429
Fixed SCC decomposition functions. Added performance tests for GraphAnalyzer.
12 years ago
69395face2
Moved creation of SCC-dependency graph into abstract model class. Added functionality to sparse matrix class to not give the number of nonzeros upfront, but to to grow on demand.
12 years ago
b28b827362
All methods of GraphAnalyzer:
* commented,
* return values instead of passing result variables by reference.
12 years ago
5495456991
Added new log level "trace"
Fixed bug in ExplicitModelAdapter
12 years ago
ab11d3c207
Further refactoring of GraphAnalyzer class. Some comments are still missing and GraphAnalyzer should be made a namespace instead of a class with static methods only.
12 years ago
fc67cf4e3f
Further refactoring of GraphAnalyzer class.
12 years ago
cc7230abb1
Started to refactor graph analyzing to include less pointers and the like. Currently this breaks two tests.
12 years ago
5279466644
- Removed "test-prctl" option
- Some restructuring in storm.cpp
12 years ago
d4f791e80d
Removed default values for prctl, csl and ltl settings and added
test formulas for the "die" test as prctl file
12 years ago
5d3b9e5cc1
Basic structure for central model checking method in storm.cpp
12 years ago
d266d9effe
Fixed another bug in sparse matrix. Fixed bug in test.
12 years ago
00b4797948
Further refactoring. Other classes are now adapted to the changes in the sparse matrix class.
12 years ago
9ae177c9b5
Further refactoring. In particular of the matrix class.
12 years ago
43f11ccc5f
Refactoring of modelchecker folder.
12 years ago
102f38322d
Fixed several bugs in several modules (bit vector, parser, etc.). Topological value iteration now works for the consensus protocol and the two dice example.
12 years ago
1f3b172c83
Added a simple module that handles segfaults: print a message and provide a backtrace.
I grew tired of always starting gdb when it would've sufficed to know the function.
This routine will demangle C++ symbols, so you can see in which function we crashed.
12 years ago
bdf173c315
GraphTransition objects can now be build from the SCC decomposition of a system.
12 years ago
a73ae7aed4
Added new option --debug.
12 years ago
f52d4eb7a8
Added new option --debug.
12 years ago
af1aa4e1e5
Added native matrix-vector multiplication for our matrix format (as fast as gmm++). Fixed bug in bit vector. Fixed some issues in SCC decomposition. MDP model checkers now have the solving methods by default (native ones) and may override them with their own ones, if desired. Added some aux stuff, like vector helper methods.
12 years ago
aee63dcf31
Made the SCC generation during decomposition optional.
12 years ago
961909877a
Added iterative version of Tarjan's algorithm for performing SCC decomposition of state-based models.
12 years ago
01779c9e83
Incomplete version of SCC decomposition of nondeterministic models.
12 years ago
34b85b956e
Moved model checking of DTMCs to superclass. Now, each DTMC model checker only needs to implement matrix-vector multiplication and linear equation solving to be able to fully model check DTMCs. Added subset/disjoint functionality to bit vector. Changed tests for MDP and DTMC model checking a bit.
12 years ago
cf772688f0
added setter for options in Settings class.
12 years ago
d38e7eeeb8
Implemented new utility functions and improved existing ones.
12 years ago
bc4eb661ba
Fixed some memory leaks. Fixed bug in vector utility. Fixed bug in sparse matrix printing. Fixed bug in DTMC model checker (computing reachability rewards). Included full reward model checking for MDPs.
12 years ago
5b57728d7e
Merge branch master into PrctlParser
12 years ago
d4cf812c5e
Added until-model checking for MDPs. Implemented Prob1A algorithm. Added asynchronous leader example.
12 years ago
48dea0199e
Started implementing the model checker for MDPs. Added reduce functionality to vector utility. Moved min/max capability to NoBoundOperator.
12 years ago
7d7edc5a05
Implemented Prob1E algorithm for nondeterministic models. Added comparison operator to bit vector.
12 years ago
7ceb1ed9b2
Added logging for errors in labeling class. Corrected wrong labeling of MDP in examples. Extended test checking for first MDP example in main.
12 years ago
8a9d766c73
Changed input format for non-deterministic models to PRISMs output format. Added min/max capability to probabilistic operator without bounds. Implemented Prob0E. Added a simple MDP model to example suite.
12 years ago
8c248c05c5
Renamed NonDeterministic to Nondeterministic in all places. Fixed (hopefully) all occurrences of these names. Implemented Prob0A algorithm.
12 years ago
19cbe13691
Prepared methods for performing reachability searches for non-deterministic models. Removed storage of backward transition relation: it is now (re-)created on demand in the model checkers.
12 years ago
5d849018de
Some minor fixes to GraphAnalyzer and model checkers.
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
c02271a36a
Fixed typo in CTMC class. Moved GraphAnalyzer to utility.
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
7e87f35e95
First test case for prctl parser, and some necessary modifications for
the code
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
9a9cd968d9
Added a test to verify the RowSum Function in the Sparse Matrix.
Added an option to the settings for auto-fixing missing no-selfloop states. Kind of a super-option above fix-nodeadlocks, perhaps some Cleanup later on.
Modified tra Files to comply with formats...
12 years ago
5f57cbb12a
Now able to build the BDD for the die example, including the reachability analysis! Booyah
12 years ago
4d813999e3
Backup commit. On my way of buidling appropriate BDDs.
12 years ago
c4af78b859
Added singleton utility class for CUDD-based things. Added some first methods to expression classes to generate ADDs, but this should be moved to a separate class implementing the expression visitor pattern.
12 years ago
f9923bac95
Fixed memory leaks involving Settings class
Settings (being a singleton) will now free it's instance itself upon program termination.
12 years ago
facec2b040
experimented with custom style checker, fixed a few minor issues
12 years ago
062960b94c
Some cleanups, removing memleaks
12 years ago
dehnert
gereon
Lanchid
PBerger