tempest

Author	SHA1	Message	Date
Lanchid	0e0b5ff688	Added methods to check whether child nodes are set (necessary, as sub classes have no direct access to the pointer)	13 years ago
Lanchid	195c58e60f	Small change of plans: Abstract formulas now use a template parameter for subformulas, so it can be determined later which kind formulas they accept as subformulas.	13 years ago
Lanchid	f1383964f0	Adapted abstract formulas to new structure	13 years ago
Lanchid	38652f44e4	Restructuring formula classes, part I Sorted formulas into respective folders, depending on which logic they belong to (or if they are abstract). The Code is NOTadapted to the new structure yet.	13 years ago
dehnert	43f11ccc5f	Refactoring of modelchecker folder.	13 years ago
Lanchid	5b57728d7e	Merge branch master into PrctlParser	13 years ago
dehnert	73623ff3f6	Added boolean parameter qualitative to all path formulas, i.e. to the checking and the callback methods.	13 years ago
gereon	5bb71a28e9	added more interfaces to AbstractModelChecker.	13 years ago
Lanchid	afce8c9d12	Fixed some doxygen warnings (Remaining warnings all appear because of undocumented function parameters)	13 years ago
gereon	47cb1aa4d9	renamed BoundOperator to PathBoundOperator (StateBoundOperator is coming soon...) renamed modelChecker to modelchecker	13 years ago
gereon	d7a288d05a	fixed "copy" constructor	13 years ago
gereon	55c2d5c03f	implemented clone for BoundedNaryUntil	13 years ago
gereon	43b56fce62	first version of BoundedNaryUntil. clone() does not work yet...	13 years ago
gereon	3716dedc78	first half of documentation.	13 years ago
gereon	8449c5ee11	implemented formula checker	13 years ago
gereon	9d65bdeef3	next iteration on formulas... removed AbstractFormula::cast() in favor of AbstractModelChecker::as() changed all formulas to use this new one actually implement ::check(AbstractModelChecker) for all formulas	13 years ago
gereon	8a719bed22	some more form on formulas. seems to work for formula objects changed yet...	13 years ago
gereon	df91728da0	first "kind of working" version.	13 years ago
dehnert	86c7ae3f5c	Added BoundedEventually as a convenience operator. Included check for illegal atomic propositions. Added exception class to be raised in case a property is invalid for the respective model.	13 years ago
dehnert	58cf8118fe	Initial version of reward model checking for DTMCs. Added two convenience operators to PCTL (Eventually and Globally) and added missing reward formulas.	13 years ago
PBerger	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
PBerger	9e5b69b211	Further naming scheme enforcement.	13 years ago
PBerger	96c7dd9a79	Added the (default) external build path /build to git ignore. Added, fixed, refactored Include Guards in ALL Files, should be consistent now.	13 years ago
PBerger	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
dehnert	091a7740a2	Added a lot of consts to all methods provided by formula classes.	13 years ago
Lanchid	bb9aa0dfe2	Changed check function in formula classes to use a reference of the model checker instead of a pointer.	13 years ago
Lanchid	6b4945e55c	Changed getter for child nodes to reference style	13 years ago
Lanchid	350f1a0990	Code style for formula classes	13 years ago
Lanchid	a1854b26a5	Documentation of ModelChecker (new) and improved doc of formula classes	13 years ago
Lanchid	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)	13 years ago
PBerger	4f7cbd450a	Fixed bugs in the Windows Part of the parser, refactored includes to meet Windows Requirements. Deleted a #warning	13 years ago
Lanchid	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

4 Commits (0e0b5ff6881ae02b370c7271feebbe80fbfe49e1)