9775f7ae7e
Added CTMC model, doing c&p from dtmc.
I have no idea, if this is what we actually want... :-)
12 years ago
b26a731383
Added reward parsing:
* Transition-based rewards are parsed using the existing (Deterministic)SparseTransitionsParser.
* State-based rewards are parsed using a new SparseStateRewardParser that parses lines consisting of a state and an associated reward.
* The Dtmc class now stores the two reward models.
* The DtmcParser class now parses up to one transition-based and one state-based reward file. They may, however, be omitted in which case the respective reward model is set to null.
12 years ago
37f6337fa5
using new iterator for checking matrix
SquareSparseMatrix now has a new iterator over elements in a row.
Dtmc uses this iterator to check the probability matrix.
12 years ago
4d4219991c
renaming sanity check, fix brackets
12 years ago
afb0373358
Added DtmcParser class that parses a whole DTMC, making use of the
labeling and transitions parser.
Removed the parseDtmc function from IoUtility, as it became obsolete
with the DtmcParser class, fitted test cases accordingly.
12 years ago
5cc8e8bb2d
modified sanity check to use internal data structures...
12 years ago
83e660ac3d
check is sums of each row is one (or zero for "imaginary" states)
12 years ago
fe95c2225b
Added missing contructors to all exceptions.
12 years ago
96c7dd9a79
Added the (default) external build path /build to git ignore.
Added, fixed, refactored Include Guards in ALL Files, should be consistent now.
12 years ago
cce8391e44
Refactored everything to match naming scheme.
12 years ago
1f36724cc2
Refactored StringOutput to use std::to_string
Fixed Reference/Pointer bugs in all formulas.
Implemented EigenDtmcPrctlModelChecker
Replaced uses of int32 with 64bits
12 years ago
4095e87282
changing pointer to std::shared_ptr
parsers return some kind of object and it is not clear who owns this object,
i.e. who is responsible to delete it.
12 years ago
3b8e2a488b
Fix for ticket 21.
Fixed the map of the AtomicPropositionsLabeling class to
std::unordered_map.
12 years ago
b726a07b3f
Small bugfix for the dot output
12 years ago
f5d2205352
- Removed enum to infer the correct formula (sub-)class, instead used
"check" which calls the correct check function in the model checker.
- The dot output was modified to work with the refactored names
- Also, it uses now filestreams instead of C style output
- and the iterators from the matrix class
- Included new (stub) test case for output (and general parsing)
12 years ago
2bf01bfea3
Added graph search algorithms for determining the set of states that have no possibility of going to a non-target state. Enhanced bit vector class.
12 years ago
05eaab7816
Removed invocations of memcpy in favour of std::copy as compilers will take care of optimizations.
12 years ago
c634ff6d0b
Removed debug output.
12 years ago
e632fc1bb6
fixing error & warning...
12 years ago
8857655b56
Refactored names according to guidelines.
12 years ago
464fe97578
Fixed initialization order in constructor.
12 years ago
70bf39b634
Fixed includes for graph transitions class. Added index iteration functionality to the bit vector class.
12 years ago
d871aca351
Renamed the backward transitions class to GraphTransitions and generalized it to be able to store the forward or backward graph structure of a given system.
12 years ago
1ed29262ff
Renamed dtmc.h to Dtmc.h and backward_transitions.h to BackwardTransitions.h.
12 years ago
378fe3f532
Renamed and refactored atomic propositions labeling.
12 years ago
8911b0b71a
Fixed wrong namespace for bit vector and square sparse matrix classes.
12 years ago
8806dc6592
Performed renaming of static_sparse_matrix.h to SquareSparseMatrix.h, renamed the class accordingly and adapted the tests and includes.
12 years ago
bdfb9b7d72
Further refactoring of the bit vector class, now including logging output. Renamed it according to the new naming scheme.
12 years ago
876154e6f0
Removed logging output from all classes. Added log4cplus as 3rdparty library. Refactored CMakeLists.txt to always use libraries that are in the repository. Changed executable file to mrmc/mrmc-tests. Added case distinction in gtest to compile with clang.
12 years ago
5a8c2a8d0e
Added iterator functionality to bit vector. Minor cosmetics here and there.
12 years ago
ee081fd570
Fixed a lot of memory access violations, memory leaks, warnings. Enabled -Werror for gcc, as there are currently no warnings.
12 years ago
3560d10481
Added comment for destructor.
12 years ago
d5919f2fdf
Removed unnecessary lines.
12 years ago
eeddadc096
The columns of non-zero elements of a single row in a sparse matrix can now be iterated using an iterator. These iterator functionality is now used by the computation of the backwards transitions.
12 years ago
3c5dbb8483
Changed all indexing to 0-bound. From now on, the available states always start with 0 and end with the state with the highest index used.
Adapted the test cases.
Added comments in the sparse matrix class.
12 years ago
12e6a945df
Included new (smaller) test model. Bugfixes and improvements to BackwardTransitions class. Removed performance test code from main() function in favor for creating a simple DTMC from the input parameters.
12 years ago
bd594e2fae
Added backwards transitions class. Small refactorings. Had to comment out some parts in utility.cpp and read_tra_file_test.cpp because they do not compile and seem to not be compliant with the current version in the repository.
12 years ago
107ea1e498
Fixed minor typo in comment.
12 years ago
b7618fd91a
Refactoring of labeling classes.
12 years ago
44fbef62bd
Added capability to compute model size in bytes and corresponding functions in several classes. Added model info output to DTMC class. Added atomic proposition information output to atomic propositions labeling class.
12 years ago
0ec2369459
Added support for 1-based indices for atomic proposition labeling. Fixed some whitespace typos.
12 years ago
c33dfac505
Renamed classes for atomic proposition labeling storage.
Added some methods to DTMC class stub.
12 years ago
88101ef238
Fixed comment typo.
12 years ago
b7eaeab11f
Renamed dtmc folder to models, corrected namespace in contained classes and fixed includes in affected files.
Added DTMC class stub.
12 years ago
gereon
dehnert
Lanchid
PBerger