s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
3623 Commits
5 Branches
0 Tags
31 MiB
Tree: 615d3c2147
Branches Tags
${ item.name }
Create tag ${ searchTerm }
Create branch ${ searchTerm }
from '615d3c2147'
${ noResults }
Commit Graph

693 Commits (615d3c21474e9f1135293c702a6844cb79414348)

Author SHA1 Message Date
Dave Parker 80c8dcd09d Refactor explicit engine product construction.
11 years ago
Dave Parker e893970d22 Add some (already implemented) methods to ModelSimple interface.
11 years ago
Dave Parker 0603e4a9b5 Some refactoring in explicit model checking engines: create new child model checkers, rather than inheriting their functionality as a subclass(e.g. DTMCModelChecker from CTMCModelChecker) - avoids problems where some methods are not implemented in the subclass.
11 years ago
Dave Parker 6e89edfedb Co-safe reward model checking for CTMCs.
11 years ago
Dave Parker bfeb0d0b69 Implement lifting to product for STPG rewards.
11 years ago
Dave Parker 1762db4d34 Bugfix in lifting rewards to product.
11 years ago
Dave Parker 21d663816a Push lifting of (explicit) reward structures into Reward classes.
11 years ago
Dave Parker df63c6e9a1 Refactoring: StateRewardsArray extends StateRewards.
11 years ago
Dave Parker 87bce928b1 Code tidy
11 years ago
Dave Parker 303d31be14 Better error message for non-co-safe properties in R operators.
11 years ago
Dave Parker a76b3c73bd Remove (most) usage of R_F in temporal operators.
11 years ago
Dave Parker 17a946783d Disallow properties of the form R[F<=k].
11 years ago
Dave Parker 8a9701e7ec Code tidy
11 years ago
Dave Parker 69c8b2ce1f Bug fix: better detection of R[F] when seeing if it is cosafe.
11 years ago
Dave Parker fee3972b20 Bug fix in explicit co-ssafe reward computation.
11 years ago
Dave Parker 54bf906cc3 Missing -exporttarget case.
11 years ago
Dave Parker 957148215e Support (symbolic/explicit) for expected reward to satisfy a co-safe LTL formula.
11 years ago
Dave Parker c8e181ffda explicit.ProbModelChecker: Add statesOfInterest to a few more functions (for merging purposes).
11 years ago
Dave Parker 9e434ad9ea Merge in explicit engine detection of end components for Streett acceptance. [from Joachim Klein]
11 years ago
Dave Parker c8f60a622f Fix some comments.
11 years ago
Dave Parker 4f6f28541a Move some STPG stuff from prism-games back to the trunk.
11 years ago
Dave Parker 777e295513 Performance improvement for SubNondetModel (and thus explicit engine end-component detection) + a bugfix. [from Marcus Daum]
11 years ago
Joachim Klein fe95ece342 Deterministic automata: Better checking of atomic propositions
11 years ago
Joachim Klein 83ad513dc4 explicit.LTLModelChecker: catch missing edges in the DA for increased robustness
11 years ago
Dave Parker af7a1e7902 Bug fix (non-crucial) in explicit expected total cost.
11 years ago
Dave Parker 4bb807cb8e Code rearrange: move automata stuff to a separate "automata" package.
11 years ago
Dave Parker 22bb6dea1c Merge prism-hoaf branch back into trunk.
11 years ago
Dave Parker bc29c96cbc Cache the embedded DTMC inside CTMCSimple. This preserves the cached PredecessorRelation in the DTMC, allowing subsequent properties to be checked more efficiently. [from Joachim Klein]
11 years ago
Dave Parker 4da481df18 Remove debug output.
11 years ago
Dave Parker 2dc4ef9a4a Fix JavaDoc bugs.
11 years ago
Dave Parker 852398415b Add R[C] model checking for explicit DTMC model checker too (not really testeed much yet).
11 years ago
Dave Parker 88eb9ae71a Re-rename new predecessor option (-nocachepre to -noprerel, etc.)
11 years ago
Dave Parker 01aaf56ca3 explicit.DTMCModelChecker: Implements predecessor-based versions of prob0 / prob1. [from Joachim Klein]
11 years ago
Dave Parker 5570bbe256 Change -nobackward option to -nocachepre.
11 years ago
Dave Parker c7dbacf85f Add option -nobackward to PrismSettings (disables computations relying on the predecessor relation). [from Joachim Klein]
11 years ago
Dave Parker f4ab03013f Add methods to the explicit.Model interface to get a (cached) PredecessorRelation. [from Joachim Klein]
11 years ago
Dave Parker 9babbf4bf1 Add explicit.PredecessorRelation class for computing / storing predecessor relation of models. [from Joachim Klein]
11 years ago
Dave Parker 4cc09fbc6c Bigfix in CTMC model checking, due to recent BSCC code reorganisation. [from Joachim Klein]
11 years ago
Dave Parker 9c407486c8 Bug fix in export of product states in explicit DTMC model checker.
11 years ago
Dave Parker a6a371ee77 Remove debug output.
11 years ago
Dave Parker f82a7c84ad Clean up output when avg time is shown as NaN. [from Joachim Klein; and the last commit]
11 years ago
Dave Parker 9a6bb057cf Allow initial states list to be cleared in ModelExplicit.
11 years ago
Dave Parker fae4eb38d7 Add support for -exporttarget to explicit engine.
11 years ago
Dave Parker 4a33c0398c Add some more (hidden) settings to explicit StateModelChecker inheritSettings().
11 years ago
Dave Parker 897ca7c4c1 Code re-arrange.
11 years ago
Dave Parker bb1d0dcd5b Add label export functionality to explicit engine
11 years ago
Dave Parker 56f48fa2d2 Remove debug output
11 years ago
Dave Parker 53c24c5abb Add exportTarget settings to explicit model checkers (not used yet).
11 years ago
Dave Parker 0984820760 Add support for -exportprodtrans and -exportprodstates switches to explicit engine.
11 years ago
Dave Parker 5173aab053 Bug fix in explicit.SCCComputerTarjan (from Joachim Klein).
11 years ago