Dave Parker
|
ff893c6cdc
|
CHANGELOG.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4108 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Vojtech Forejt
|
561bcf9c6d
|
Added switches -noprob0 and -noprob1 to the bash completion script
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4107 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
83acce9758
|
Extract MDP GS setting from -gs (to stop DTMC GS setting getting overridden in explicit engine).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4106 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
4a1163a86d
|
Added ability to disable precomputation algs independently (switches -noprob0 and -noprob1).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4103 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
5dab19e7dc
|
Add check for trying val iter from above for max probs - does not work.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4101 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Vojtech Forejt
|
879eac6d76
|
bash completion for property names
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4098 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Vojtech Forejt
|
16215e79b0
|
syntax highlighting for Vim
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4095 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
f749ab8f24
|
Prism exits with code 1 if failed due to existence of deadlocks.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4086 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
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.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4085 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
94cc80b19e
|
Missing committed file from earlier JDD-debug functionality.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4080 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
7173ca6244
|
CHANGELOG.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4079 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Vojtech Forejt
|
496ae010fc
|
fixed a bug in bash completion (syntax error if last word contained a space)
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4074 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Vojtech Forejt
|
dc6037d047
|
PrintWarningToMainLog method that gives access to Java printWarning method.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4073 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Vojtech Forejt
|
1e49dd0197
|
Verification/simulation in GUI now shows number of warnings in the result window (if it's nonzero)
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4072 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Vojtech Forejt
|
acd646d02c
|
* PrismLog now has a "printWarning" method that can be used to print warnings.
* In the end of computation PrismCL prints a message if there were some warnings.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4069 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Vojtech Forejt
|
0f52647368
|
changed bash completion script so that it does not print full paths when completing file names
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4059 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Vojtech Forejt
|
bccfecbefa
|
First version of Bash programmable completion script for PRISM
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4057 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Vojtech Forejt
|
8f89f4e4b1
|
Verbosity level in PrismLog. Untested yet.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4056 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Vojtech Forejt
|
cd1b3dcfed
|
Fixed a problem where transition rewards were not being set for unnamed actions
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4050 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
3bfb5929bb
|
Explicit bug fig (from qar/Anvesh) - can now reset rewards in MDPRewardsSimple to 0.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4046 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
ef5f6db0ad
|
Re-instate .dev version suffix
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3999 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
50d08cde90
|
Un-needed file
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3997 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
e9a1859339
|
Add binary operators to StateValues class and use in explicit model checking.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3996 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
bf59e25a49
|
Fixed a bug in getAllUndefinedConstantsRecursively. Showed up when running auto in embedded example. Bug found by Janne Kauttio.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3983 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
9e7ff7c43b
|
Makefile fix. Package parser.type may not get built in some scenarios.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3969 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
be5c6ea92a
|
Added PrismTest class to illustrate programmatic use of PRISM.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3966 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
a19cd352f1
|
Makefile dist_bin target automatically builds "all" too first.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3948 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
3a85f6e277
|
Make binary distribution names architecture-dependent (32 vs 64 bit).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3947 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
aae6d1c39e
|
Compile fix - oops.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3882 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
7f1b6beb4c
|
Version num: 4.0.2
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3880 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
fadb7858ab
|
CHANGELOG.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3879 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
aca617849b
|
Some optimisations for approximate model checking on models with deadlocks (could do other operators too).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3876 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
f578bbb893
|
Approximate model checking ignores "max path length" setting when verifying time-bounded properties.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3855 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
905a57fcf3
|
Test commit
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3787 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
a41137906a
|
Test commit
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3786 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
e6e29e6c7a
|
Test commit
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3783 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
1867f1e5e3
|
Small changes to reading in of init distributions (to align with new explicit version).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3735 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
755295f9b4
|
Explicit engine handles transient with imported init distribition.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3734 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
c072eb0bd3
|
More methods in explicit StateValues.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3733 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
9707b6bf10
|
Added -exportstates for explicit engine.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3722 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
30c0c09569
|
Small fixes in explicit StateValues class.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3721 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
355032b5e3
|
Code tidy
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3711 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
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).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3709 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
6a046b4431
|
Tidy/improve passing of settings to explicit model checkers.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3708 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
d54e92533c
|
Another fix for adv gen in explicit engine: min probs should not be treated as for max probs.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3691 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
e24ee33442
|
Bug fix in explicit MDPs: actions added as 0.0 instead of null.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3646 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
0bb97718c1
|
Adv gen for rewards in explicit engine (from prism-games).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3641 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
0debba1332
|
New JDD debugging code from Vojta (disabled by default).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3639 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
f49ce60f1b
|
Fixes in explicit MDP adversary generation (min case can give wrong answer).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3629 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
1076e70f9f
|
Bug fix in explicit-state MDP adversary generation (MDPSparse).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3627 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |