- Fixed one problem marked FIXME in the transpose function. The need for a "sentinel" element was created by an off by one in the prior loop.
- Changed all occurences of SparseMatrix<bool> to SparseMatrix<T>. Now the only two types for which SparseMatrix is instantiated are double and int.
- Compiles again.
|-> Compile time seems to be roughly the same for clean; make all. For incremental builds I haven't tested yet.
Former-commit-id: 6d829e0903
- Also handled the case of a missing --prctl while using the counterexample generation.
- Remark: Some documentation for the VectorSet would have been nice.
Former-commit-id: c687b67454
- Fixed the infinite loop bug that occured when giving a filepath pointing to a directory instead of a file.
- The BitVector to Dtmc subsystem converter now supports an optional choice labeling.
- The output of the modelchecker to the log file is now suppressed while doing a counterexample generation.
- It is now possible to add more atomic propositions to the AtomicPropositionLabeling than previously declared (at the cost of one reserve per added ap beyond the maximum).
The maximum is then increased accordingly.
|-> As a result the state added for the Dtmc subsystem has now its own label.
Next up: Merge.)
Former-commit-id: 74c92aaea1
Remark: I don't quite get the optional choice labeling in Dtmcs.
Whats its purpose?
Why is it undocumented in the Dtmc constructor, not supported by the parser but needed nevertheless?
Next up: Pretty up counterexample generation output.
Former-commit-id: c04063b608
-Had to add a addState function to AtomicPropositionLabeling to be able to throw out the unneeded states using the substates constructor while at the end adding the absorbing state and its label.
An alternative for that would be to provide a constructor taking the mapping and the single labelings vector as well as a getter for the single labelings.
-The --counterexample command now only uses the pctl file given as argument to it and therefore it is now superflous to give the --prctl command in that case.
-Also fixed a bug in the filter constructor of the BitVector.
Now it copies all bit values specified by the filter to the correct index of new instance instead of all to index 0.
Next up: Handle the optionals of the Dtmc when creating the sub-Dtmc.
Former-commit-id: b45ee94cb2
* included small consensus example
* made backward-transition generation more beautiful and versatile
* included Dijkstra search for most probable paths
* included first rough scheduler-guessing (there's room for improvement though)
Former-commit-id: db795fa1bf
dehnert
masawei
PBerger