sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
2070 Commits
2 Branches
0 Tags
187 MiB
Tree: 30fc452623
Branches Tags
${ item.name }
Create tag ${ searchTerm }
Create branch ${ searchTerm }
from '30fc452623'
${ noResults }
Commit Graph

349 Commits (30fc45262317abab49410dea711a86d9f7019d5d)

Author SHA1 Message Date
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 5d849018de Some minor fixes to GraphAnalyzer and model checkers.
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
dehnert c02271a36a Fixed typo in CTMC class. Moved GraphAnalyzer to utility.
13 years ago
gereon 5bb71a28e9 added more interfaces to AbstractModelChecker.
13 years ago
Lanchid afce8c9d12 Fixed some doxygen warnings
13 years ago
gereon 47cb1aa4d9 renamed BoundOperator to PathBoundOperator (StateBoundOperator is coming soon...)
13 years ago