tempest

Author	SHA1	Message	Date
Lanchid	4cddd9ad78	Changing AbstractFormulaChecker and PrctlFormulaChecker to completely work with the new structure of formulas.	13 years ago
Lanchid	01b1efc12d	Some improvements/corrections to the LTL parser and some test cases for it	13 years ago
Lanchid	834cb269a6	Minor corrections in code	13 years ago
Lanchid	fb50665564	Documentation of formula classes	13 years ago
Lanchid	ccfd1ccc6a	Documentation for CSL and PRCTL classes	13 years ago
Lanchid	0a2725d79c	Documentation of abstract formulas.	13 years ago
Lanchid	535ae933b0	Compiling implementation of LTL parser	13 years ago
Lanchid	9e3ec6c403	Added LTL	13 years ago
Lanchid	00286b2f01	Added formula classes for CSL	13 years ago
Lanchid	45867c33c1	Prctl works now.	13 years ago
Lanchid	f513e49084	Almost finished restruction of PRCTL formulas; adapted code (including test cases) to work correctly with the new structure	13 years ago
Lanchid	3e554514cb	Correct formulas	13 years ago
Lanchid	ba4a3807dc	New header file for all PRCTL formulas	13 years ago
Lanchid	b64fd7c351	Adapted PRCTL formulas to the new structure	13 years ago
Lanchid	7e4d09cb01	Added abstract reward operators.	13 years ago
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	a1ec7a5d54	Derived PRCTL formula classes from abstract ones	13 years ago
Lanchid	adf16e5f9e	Added abstract reward formulas	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
Lanchid	f996829836	Some minor changes in output of formulas	13 years ago
Lanchid	39ff3240d3	More convenient syntax for time bounded formulas, and respective test cases.	13 years ago
Lanchid	96fa125fe4	Added time bounded operators for CSL.	13 years ago
Lanchid	bfd2178ca3	Corrected define guards in some header files	13 years ago
Lanchid	7e91d5b01e	Test cases for CSL parser	13 years ago
Lanchid	509c1a2b47	Added support for SteadyStateNoBoundOperator into the CSL parser.	13 years ago
Lanchid	2470c31cb0	Added SteadyStateNoBoundOperator	13 years ago
Lanchid	08815b8c13	Changed "NoBoundOperator" to "PathNoBoundOperator", as I will implement a "StateNoBoundOperator" now...	13 years ago
Lanchid	6ff25321d4	First version of CSL parser TODO: - Correct path formulas - Time bounded until - Steady state operator without bounds	13 years ago
Lanchid	c7afcecf4a	Minor changes (mainly improving comments)	13 years ago
Lanchid	895c2b6aad	Convenient file parser for PRCTL, and correct reward formula parsing (together with some necessary code for that)	13 years ago
dehnert	43f11ccc5f	Refactoring of modelchecker folder.	13 years ago
gereon	836bdb3f1c	Created new base class OptimizingOperator. Inheriting from this class where appropriate, added constructors accepting minimumOperator argument.	13 years ago
gereon	a5ad38a46b	Added options for optimizing max/min operator to BoundOperators.	13 years ago
dehnert	f787044ece	Fixed bug in cloning of negated formulas.	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
dehnert	5ba7f63bc2	Splitted RewardBoundOperator and ProbabilisticBoundOperator checking methods for model checkers (needed for enabling qualititative model checking for P operator with bounds 0/1). Moved some methods of DtmcModelChecker one level up to AbstractModelChecker. TODO: this should be done for other methods as well, but there are more changes needed for that to work.	13 years ago
dehnert	d4cf812c5e	Added until-model checking for MDPs. Implemented Prob1A algorithm. Added asynchronous leader example.	13 years ago
dehnert	48dea0199e	Started implementing the model checker for MDPs. Added reduce functionality to vector utility. Moved min/max capability to NoBoundOperator.	13 years ago
dehnert	8a9d766c73	Changed input format for non-deterministic models to PRISMs output format. Added min/max capability to probabilistic operator without bounds. Implemented Prob0E. Added a simple MDP model to example suite.	13 years ago
dehnert	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.	13 years ago
gereon	5bb71a28e9	added more interfaces to AbstractModelChecker.	13 years ago
gereon	4389f6ba5b	finished PrctlFormulaChecker. I hope it checks the correct set of operators now...	13 years ago
Lanchid	afce8c9d12	Fixed some doxygen warnings (Remaining warnings all appear because of undocumented function parameters)	13 years ago
Lanchid	bfce1a5655	Removed brackets in output of until formulas	13 years ago
gereon	cc9b11d7e4	added StateBoundOperator and SteadyStateOperator	13 years ago
gereon	47cb1aa4d9	renamed BoundOperator to PathBoundOperator (StateBoundOperator is coming soon...) renamed modelChecker to modelchecker	13 years ago
Lanchid	bb34e94eac	Changed the output function of the formulae to produce a string in the same format as the input	13 years ago

1 2

96 Commits (4cddd9ad78b5afdcc576bc176196f452a61203e1)