06d78967df
Fixed MDP Parser, removed parsing of STATES/TRANSITIONS, see #10
Refactored the Sparse Adapters, see #17
12 years ago
8c248c05c5
Renamed NonDeterministic to Nondeterministic in all places. Fixed (hopefully) all occurrences of these names. Implemented Prob0A algorithm.
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
b5fcc7e590
Also, deleted the output.dot file...
12 years ago
96a833d605
Added /test/parser/output.dot to gitignore (output file is automatically
generated by ParseDtmcTest and should not be in the repository)
12 years ago
718608622f
added Ctmdp model, changed MdpParser to NonDetModelParser
12 years ago
f6196c7429
Some error messages on "unparsable" formulas
PrctlParser now throws an error in all cases a formula could not be
parsed successfully.
12 years ago
47cb1aa4d9
renamed BoundOperator to PathBoundOperator (StateBoundOperator is coming soon...)
renamed modelChecker to modelchecker
12 years ago
bb34e94eac
Changed the output function of the formulae to produce a string in the
same format as the input
12 years ago
ab4174183b
Changed PrctlParser to directly parse the input string as formula, and
added PrctlFileParser to parse formulae from a file
12 years ago
e829e613c0
Changed grammar such that brackets are not necessary around each binary
operator, and changed some test cases to check that it works
12 years ago
e2f6b4b265
Extended parseComplexFormulaTest to use nested path formulas
12 years ago
10e25fbd61
fixed warnings in ParseMdpTest
12 years ago
3833c8af41
Some more test cases for PRCTL formula parsing
12 years ago
e52379bb54
Added XCode stuff to .gitignore. Fixed a few tests to compile with clang under -Werror.
12 years ago
b66e1a34db
Some fixes in formulas
Additional test case for reward formulas
12 years ago
02528f2bd9
Test cases for Prctl parser
12 years ago
7e87f35e95
First test case for prctl parser, and some necessary modifications for
the code
12 years ago
a598d3751c
The DeterministicSparseTransitionParser.cpp was still broken, rewrote it in a simpler and more convenient way.
All Deterministic Tests complete now.
12 years ago
c2669ccec4
"Creating" DeterministicModelParser
this new parser is actually the old DtmcParser.
It can now also create Ctmc models...
12 years ago
7800132684
Added Mdp Class, Parser and support in the AutoParser.
Added Test for MdpParser
12 years ago
557461a77d
Renamed SquareSparseMatrix to SparseMatrix
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
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 ;)
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
64784d4e92
Renamed LabParser to AtomicPropositionLabelingParser
12 years ago
b0b8c98f6b
Renamed TraParser to DeterministicSparseTransitionParser
12 years ago
08f87d545c
Some more refactoring, renaming, adding #ifndef guards...
Fixed a warning in SquareSparseMatrix.h regarding a conversion from uint64 to uint
12 years ago
cce8391e44
Refactored everything to match naming scheme.
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
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.
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
f960e20e53
porting LabParser and TraParser from c-style API to class API
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
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
7eaedbfe9b
changing names of parsers
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
b7618fd91a
Refactoring of labeling classes.
12 years ago
c33dfac505
Renamed classes for atomic proposition labeling storage.
Added some methods to DTMC class stub.
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
f3a600550a
(not much)
12 years ago
8b1d5804c9
Edited the test cases from the parsers, added a missing FAIL() in the dead branches.
12 years ago
1643901c5a
Big bunch of fixes, including memory leaks, bad code pathes, insufficent error reporting, uninitialized variables, etc, etc.
Edited sparse/static_sparse_matrix.h, added an internal state enum to represent errors and the like.
12 years ago
87f768ca41
Edited src/parser/read_lab_file.cpp, fixed String tokenization in WIN32
Edited MRMCConfig.h.in to include the base path for Test/ Directory
Refactored the test files to use the new test/ base path macro
With credits to Thomas ;)
12 years ago
65763c29f1
Restructured labeling class (map does not directly point to the
Atomic_proposition objects any longer)
Adapted labeling parser to work with declaration lines longer
than BUFFER_SIZE bytes.
With credits to Philipp :-)
12 years ago
765689c40a
Changed name of class "Labelling" to "Labeling".
12 years ago
8e460897f0
Minor corrections (Memory initialization in AtomicProposition) and
more
test
cases
12 years ago
a0e07c2022
Parser for labelling files including new data structure managing
different atomic propositions.
(Works now as node_array attribute of class Atomic_proposition is now
always instantiated with 0)
12 years ago
PBerger
dehnert
Lanchid
gereon