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

57 Commits (8525fdc43a4c9ad8b3e48170b66f173b17c5bb43)

Author SHA1 Message Date
Dave Parker f937eaf698 Better dot output for games in A-R loop.
16 years ago
Dave Parker b6b993f030 Improved Fox-Glynn for small numbers + int overflow bugfix (Vojta).
16 years ago
Dave Parker bd0f1cb719 Explicit Prob1 bugfix.
16 years ago
Dave Parker 88c49d8d69 Uniformisation bugfix in explicit engine.
16 years ago
Dave Parker 49fb84b25d MDPModelChecker uses init state to display results.
16 years ago
Dave Parker c3ba43e358 Further work on simulator.
16 years ago
Dave Parker 7ab0f64ad0 Added option to set epsilon for A-R loop.
16 years ago
Dave Parker adfc38bbf6 Removed (old) abstraction package.
16 years ago
Dave Parker 894054debe First version of explicit model construction.
16 years ago
Dave Parker 6b992f1df6 Deadlocks and permutations for explicit.
16 years ago
Dave Parker 3321e1df7d Explicit model export has option to just do tra file.
16 years ago
Dave Parker ae4e24aa71 Explicit model export matches PRISM export better.
16 years ago
Dave Parker 45b9247462 Various additions/improvements to explicit code needed for model construction.
16 years ago
Dave Parker a1b94a59fb Missing file from previous (PRISM+explicit) commit.
16 years ago
Dave Parker d40ffd38e9 Preliminary code to attach explicit stuff to PRISM + some more Model class re-arrangements.
16 years ago
Dave Parker 57a404cc05 Fixes in explicit CTMC solving + some CTMDP stuff.
16 years ago
Dave Parker 9343644985 Updated MDPs to new model class design, added some CTMDP stuff.
16 years ago
Dave Parker 8f2748a711 Redesign/tidy of model interfaces + more CTMC model checking.
16 years ago
Dave Parker 719e186117 Code tidy.
16 years ago
Dave Parker 564a7354e6 Output typos.
16 years ago
Dave Parker acb3a9e220 Bugfix in switch to PRISM-AR.
16 years ago
Dave Parker f8cf00708e Added -exactcheck and -rebuild=immed options for PRISM-AR (plus tweaks to A-R API wrt rebuilding).
16 years ago
Dave Parker 97e845a7df Removed surplus output.
16 years ago
Dave Parker 127be3a3f3 Comments/tidy.
16 years ago
Dave Parker 2803fc45e0 Explicit-state model checker for DTMCs (not very efficient - mostly MDP-like).
16 years ago
Dave Parker f0bc960199 Code tidy.
16 years ago
Dave Parker 5f3732401d Additions to prism-ar code.
16 years ago
Dave Parker 4f3d2090e8 A-R loop output tidy + bugfix (in PRISM version).
16 years ago
Dave Parker 7400c243f6 Some code for doing full model checking to test A-R loop.
16 years ago
Dave Parker cbc80bab53 Extra explicit model checker method.
16 years ago
Dave Parker 1383ed7a99 Constructors for explicit models.
16 years ago
Dave Parker 80ee80817c Strategy generation for bounded until (MDPs).
16 years ago
Dave Parker ebd7af1d53 Code tidy.
16 years ago
Dave Parker 533d7d9425 Bugfixes: loops (esp. bounded until) in explicit mc.
16 years ago
Dave Parker 3d34b9baef Info output for explicit models.
16 years ago
Dave Parker b75bf6792a Info output for explicit models.
16 years ago
Dave Parker 08eec82b7b Added -nopre for MDP CL model checker.
16 years ago
Dave Parker afed6677e3 Bugfix: equals() in Distribution (explicit).
16 years ago
Dave Parker 1fba1a5e41 Test program for (explicit) STPG model checking.
16 years ago
Dave Parker 8472802b6b Slight tweak to (explict) output of MDP dot files (consistency with STPGs).
16 years ago
Dave Parker 664f37c731 Import/export of STPGs (explicit) + better dot output.
16 years ago
Dave Parker 8c1bd35059 Imported label files can have blank lines (explicit lib).
16 years ago
Dave Parker a9bdc74b25 MDPModelChecker improvements, including Prob0.
16 years ago
Dave Parker 92b341ccf2 Tidy,
16 years ago
Dave Parker 85bcef53d2 Improvements to import from tra files (explicit lib).
16 years ago
Dave Parker 783dcc9863 Bug fix: Blank lines allowed in labels files.
16 years ago
Dave Parker 11868e05bd Added -epsilon switch for A-R.
16 years ago
Dave Parker b760af0db3 Asbtraction of CTMC for unbounded props uses embedded DTMC.
16 years ago
Dave Parker 900c100728 DTMC transition count bugfix.
16 years ago
Dave Parker 24f7d04d70 Method to build embedded DTMC.
16 years ago