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

1552 Commits (a51157e11afda37e8cd30e5e2b2af66b3a9e6a7e)
 

Author SHA1 Message Date
Dave Parker 83acce9758 Extract MDP GS setting from -gs (to stop DTMC GS setting getting overridden in explicit engine).
14 years ago
Dave Parker 4a1163a86d Added ability to disable precomputation algs independently (switches -noprob0 and -noprob1).
14 years ago
Dave Parker 5dab19e7dc Add check for trying val iter from above for max probs - does not work.
14 years ago
Vojtech Forejt 879eac6d76 bash completion for property names
14 years ago
Vojtech Forejt 16215e79b0 syntax highlighting for Vim
14 years ago
Dave Parker f749ab8f24 Prism exits with code 1 if failed due to existence of deadlocks.
14 years ago
Dave Parker a066e5db8e Bugfix in handling of init/deadlock labels during constant processing - e.g. P=?[F "deadlock"&x=i] failed if i was a constant.
14 years ago
Dave Parker 94cc80b19e Missing committed file from earlier JDD-debug functionality.
14 years ago
Dave Parker 7173ca6244 CHANGELOG.
14 years ago
Vojtech Forejt 496ae010fc fixed a bug in bash completion (syntax error if last word contained a space)
14 years ago
Vojtech Forejt dc6037d047 PrintWarningToMainLog method that gives access to Java printWarning method.
14 years ago
Vojtech Forejt 1e49dd0197 Verification/simulation in GUI now shows number of warnings in the result window (if it's nonzero)
14 years ago
Vojtech Forejt acd646d02c * PrismLog now has a "printWarning" method that can be used to print warnings.
14 years ago
Vojtech Forejt 0f52647368 changed bash completion script so that it does not print full paths when completing file names
14 years ago
Vojtech Forejt bccfecbefa First version of Bash programmable completion script for PRISM
14 years ago
Vojtech Forejt 8f89f4e4b1 Verbosity level in PrismLog. Untested yet.
14 years ago
Vojtech Forejt cd1b3dcfed Fixed a problem where transition rewards were not being set for unnamed actions
14 years ago
Dave Parker 3bfb5929bb Explicit bug fig (from qar/Anvesh) - can now reset rewards in MDPRewardsSimple to 0.
14 years ago
Dave Parker ef5f6db0ad Re-instate .dev version suffix
14 years ago
Dave Parker 50d08cde90 Un-needed file
14 years ago
Dave Parker e9a1859339 Add binary operators to StateValues class and use in explicit model checking.
14 years ago
Dave Parker bf59e25a49 Fixed a bug in getAllUndefinedConstantsRecursively. Showed up when running auto in embedded example. Bug found by Janne Kauttio.
14 years ago
Dave Parker 9e7ff7c43b Makefile fix. Package parser.type may not get built in some scenarios.
14 years ago
Dave Parker be5c6ea92a Added PrismTest class to illustrate programmatic use of PRISM.
14 years ago
Dave Parker a19cd352f1 Makefile dist_bin target automatically builds "all" too first.
14 years ago
Dave Parker 3a85f6e277 Make binary distribution names architecture-dependent (32 vs 64 bit).
14 years ago
Dave Parker aae6d1c39e Compile fix - oops.
14 years ago
Dave Parker 7f1b6beb4c Version num: 4.0.2
14 years ago
Dave Parker fadb7858ab CHANGELOG.
14 years ago
Dave Parker aca617849b Some optimisations for approximate model checking on models with deadlocks (could do other operators too).
14 years ago
Dave Parker f578bbb893 Approximate model checking ignores "max path length" setting when verifying time-bounded properties.
14 years ago
Dave Parker 905a57fcf3 Test commit
14 years ago
Dave Parker a41137906a Test commit
14 years ago
Dave Parker e6e29e6c7a Test commit
14 years ago
Dave Parker 1867f1e5e3 Small changes to reading in of init distributions (to align with new explicit version).
14 years ago
Dave Parker 755295f9b4 Explicit engine handles transient with imported init distribition.
14 years ago
Dave Parker c072eb0bd3 More methods in explicit StateValues.
14 years ago
Dave Parker 9707b6bf10 Added -exportstates for explicit engine.
14 years ago
Dave Parker 30c0c09569 Small fixes in explicit StateValues class.
14 years ago
Dave Parker 355032b5e3 Code tidy
14 years ago
Dave Parker 9ba97fe1fc Add MDPExplicit class to capture shared from MDPSimple/MDPSparse (also a few fixes to same thing done previously for DTMCs).
14 years ago
Dave Parker 6a046b4431 Tidy/improve passing of settings to explicit model checkers.
14 years ago
Dave Parker d54e92533c Another fix for adv gen in explicit engine: min probs should not be treated as for max probs.
14 years ago
Dave Parker e24ee33442 Bug fix in explicit MDPs: actions added as 0.0 instead of null.
14 years ago
Dave Parker 0bb97718c1 Adv gen for rewards in explicit engine (from prism-games).
14 years ago
Dave Parker 0debba1332 New JDD debugging code from Vojta (disabled by default).
14 years ago
Dave Parker f49ce60f1b Fixes in explicit MDP adversary generation (min case can give wrong answer).
14 years ago
Dave Parker 1076e70f9f Bug fix in explicit-state MDP adversary generation (MDPSparse).
14 years ago
Dave Parker 89580b450d Makefile bugfix: better alignment of CUDD and PRISM compile flags.
14 years ago
Dave Parker 76119e3a08 Fix bug in experiments (introduced in recent const improvements) (schoolboy error).
14 years ago