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
756cbd4ed1
Fixed some bugs in GmmxxAdapter and added row-vector product to sparse matrix.
12 years ago
4bb76d0268
Added EigenAdapter and a Test for the Adapter.
Fixed a type in EigenDtmcPrctlModelChecker.h
Added missing transitions in one example input file
12 years ago
d4b5a24757
Fixed the Jacobi Decomposition in the Matrix, Diagonal Matrix was not inverted.
Implemented solveLinearEquationSystemWithJacobi for GMM based Solver.
12 years ago
e8fd897852
Fixed bug in copy constructor of matrix.
12 years ago
facec2b040
experimented with custom style checker, fixed a few minor issues
12 years ago
b13f1ff37f
Adding check "transitionRewards submatrix of transitions"
12 years ago
7800132684
Added Mdp Class, Parser and support in the AutoParser.
Added Test for MdpParser
12 years ago
57274b3f09
Fixed missing newline and warning about nested comments.
12 years ago
557461a77d
Renamed SquareSparseMatrix to SparseMatrix
12 years ago
36e2f5f15b
Refactored SparseMatrix, made references const.
Refactored Adapter to GMM to make use of new internal format
12 years ago
b89db58fbb
Made changes to all files that use the Sparse Matrix, as the diagonal entries are now included in the main storage. This refs #34
12 years ago
1561843cee
Minor bugfix in sparse matrix method to compute pointwise product.
Remove unnecessary small example files.
Add reward files for synchronous leader example.
Added test procedures to main (commented out by default) to check all of the three main models (crowds, die, synchronous leader).
12 years ago
58cf8118fe
Initial version of reward model checking for DTMCs. Added two convenience operators to PCTL (Eventually and Globally) and added missing reward formulas.
12 years ago
f983317b54
Renaming MRMC to STORM, see #42
Markt und Straßen stehn verlassen,
still erleuchtet jedes Haus,
Sinnend' geh ich durch die Gassen,
alles sieht so festlich aus.
An den Fenstern haben Frauen
buntes Spielzeug fromm geschmückt,
Tausend Kindlein stehn und schauen,
sind so wunderstill beglückt.
Und ich wandre aus den Mauern
Bis hinaus ins freie Feld,
Hehres Glänzen, heil'ges Schauern!
Wie so weit und still die Welt!
Sterne hoch die Kreise schlingen,
Aus des Schnees Einsamkeit
Steigt's wie wunderbares Singen-
O du gnadenreiche Zeit!
Merry Christmas commit ;)
13 years ago
a9b6e92306
Added adapters folder and GmmxxAdapter that is a friend class of the matrix class and can convert the sparse matrix to the gmm++ format. Removed this conversion from the matrix class.
13 years ago
364d8e4861
added Matrix::getRowSum()
... and using it in the DTMC check
13 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.
13 years ago
48098b596d
Removed the parameter from const templates, as types can be stated
explicitly (see documentation)
13 years ago
a04bdd9b97
Fixed a few bugs.
13 years ago
89e38fed8f
Added temporary check() method to ProbabilisticNoBoundsOperator.
Added two check() functions to DtmcPrctlModelChecker that are to be called by the "outer world" that check a given formula and print the result the standard output.
Fixed bug in GmmxxDtmcPrctlModelChecker that prevented BiCGStab using ILU preconditioning from working
Refactored mrmc.cpp to remove larger code blocks from main().
Added option to specify logging file. If no file is set and the verbose option is not set either, logging is basically disabled by setting the logging level very high. This is a workaround for the fact that at least one log appender needs to be set in the logging framework, which would not be the case if both logging facilities (file and console) are disabled.
13 years ago
a5d922c6a8
removed pointless return that produces an error (return value...)
13 years ago
08f87d545c
Some more refactoring, renaming, adding #ifndef guards...
Fixed a warning in SquareSparseMatrix.h regarding a conversion from uint64 to uint
13 years ago
cce8391e44
Refactored everything to match naming scheme.
13 years ago
95b000436b
Added a JacobiDecomposition container and conversion function. Added const where possible.
13 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
13 years ago
cbf719568a
Added correct return value computation in method MakeRowsAbsorbing of
class SquareSparseMatrix.
13 years ago
8cbb7aa7d7
fixing toEigen conversion, making test case working :-)
13 years ago
27ba61ff74
Fixed minor bugs here and there. Improved gmm++-based model checker.
13 years ago
80b53bea18
Added more example files. Removed deletes at end of main() as these pointers are deleted by the DTMC class already. Small refactoring of GraphAnalyzer according to new guidelines. Added vector utility functions to set elements of vectors. Added conversion routine from our sparse matrix format to gmm++ format. Fixed some bugs in sparse matrix class. Added prototypical implementation of GmmxxDtmcPrctlModelChecker.
13 years ago
13a2bd3057
Moved const_templates.h from "misc" to "utility" to be able to remove
the former folder.
Also, changed those templates to use references instead of pointers for
easier code.
Renamer "utility.h" and .cpp to "ioUtility.h/cpp", as utility code
providing functionality not linked with IO has been put into other
files.
13 years ago
71c824b91a
hunting for memory erros
adding make targets to call mrmc and mrmc-tests with valgrind
fixing some memory errors in SSM, SSMTest, BitVector
adding an additional check to readLabFile
13 years ago
2ca83f5f31
Added functionality to rapidly extract sub-matrix from our sparse matrix format.
13 years ago
30827b543e
Fixed off-by-one error in sparse matrix. Now the tests do not produce a segfault any longer.
13 years ago
05eaab7816
Removed invocations of memcpy in favour of std::copy as compilers will take care of optimizations.
13 years ago
8911b0b71a
Fixed wrong namespace for bit vector and square sparse matrix classes.
13 years ago
8806dc6592
Performed renaming of static_sparse_matrix.h to SquareSparseMatrix.h, renamed the class accordingly and adapted the tests and includes.
13 years ago
2d80eb39b3
Changed logging format and minor formatting fix.
13 years ago
cfe9f86ccd
Added logging with log4cplus to sparse matrix class.
13 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.
13 years ago
ee081fd570
Fixed a lot of memory access violations, memory leaks, warnings. Enabled -Werror for gcc, as there are currently no warnings.
13 years ago
bb071d829a
fixed a simple warning...
13 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.
13 years ago
ed84bfbce7
Adapted sparse matrix class to camel case notation.
13 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.
13 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.
13 years ago
8a170d3fa6
Scheisse... hab anscheinend vergessen das zu pushen
Enthalten ist:
- Unit "Utility" zum parsen und ausgeben von DTMCs
- Klasse Formula und Subclasses für PCTL-Formeln
- Interface für den Model Checker
13 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.
13 years ago
f5dce8d33a
Added a test for reported bug by CDehnert: Sparse Matrix to Eigen conversion loses the diagonal entries
Fixed static_sparse_matrix.h
13 years ago
b63d168192
1) Excluded the constant templates from the SparseMatrix class, as gcc forbids
explicit specializations of function templates inside classes.
2) Added a parameter to these templates which allows the inference of the type
of the template parameter (gcc seems to need this)
3) Added DOT file output to the SparseMatrix.
13 years ago
PBerger
dehnert
gereon
Lanchid