Dave Parker
|
e4af9297b6
|
Missing package-info.java.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6982 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
a72a2d6e4b
|
Upgrade CUDD to version 5.0.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6964 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
2cedd3daf2
|
Update main Makefile to pass variables correctly to new cudd-5.0 Makefile.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6963 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
8361366efb
|
Code comment
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6962 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
5a373672bb
|
Some example code in explicit.DTMCModelChecker.java.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6959 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
ada9f0e3c7
|
Misc code tidy and warning removal.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6936 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
5a1186c177
|
Strategy synthesis for reach rewards in the explicit engine: choices for inf states and do export.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6933 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
65a6464b32
|
Strategy synthesis for reach rewards in the explicit engine (no precomputation yet).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6932 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
fe4cd9560c
|
Allow unbounded integer variables in model (but forbid for symbolic model construction).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6929 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
2573445470
|
Typo.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6928 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
9673f00c6a
|
Miscellaneous code tidying + warning fixes.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6927 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
d081fdae7d
|
Remove debug output.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6922 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
7805084dc6
|
Fix strategy generation for Prob1 (explicit): do an extra inner fixed point loop at the end, to avoid problems of generating surplus strategy info during early outer iterations.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6921 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
ec7a5b9511
|
Javadoc.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6920 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
48fd9e7bdd
|
Log output tweaks.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6917 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
f404f8e8d1
|
Remove debug output.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6914 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
22b6e4f5ba
|
Bug fix in previous commit.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6913 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
b8969df87e
|
MDP reachability in explicit engine: do not do numerical solution unless needed.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6912 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
fee5b70ac1
|
Connect policy iteration algs (explicit engine) to strategy generation. Also, only export DTMC to adversary file (currently).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6911 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
3ff7df7b0a
|
Attach strategy generation for MDP Gauss-Seidel (explicit).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6909 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
8b6d5d17a8
|
Improvements to strategy generation for MDP reachability in explicit engine, notably algorithms for precomputation. Also split Prob1 into Prob1A and Prob1E for efficiency reasons.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6907 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
d30e52c2a4
|
DTMCFromMDPMemorylessAdversary class treats a choice of -1 as "do nothing".
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6906 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
70b1ac94f9
|
Bug fix and implemente dmissing methods in DTMCFromMDPMemorylessAdversary.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6905 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
51bf20f1f6
|
Add strategy generation to MDP Gauss-Seidel (explicit).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6902 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
c02983ea26
|
Small code tidies.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6901 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
064356d11f
|
Rename adversary to strategy in explicit MDP model checking + align with prism-games.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6899 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
7e61583c17
|
Added multiplePlayers() method to ModelType.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6891 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
5d1fcbbfdd
|
CHANGELOG.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6887 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
aa807d3ab3
|
Small improvements to usability of the GUI simulator transition table.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6886 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
95995f66c9
|
Pepa Makefile bugfix - copied form prism-games.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6884 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
3f56c6668f
|
Miscellaneous code changes/tidies - trying to align with prism-games a bit.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6881 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
c5fa220048
|
Miscellaneous code changes/tidies - trying to align with prism-games a bit.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6880 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
018c8c89d5
|
Miscellaneous code changes/tidies - trying to align with prism-games a bit.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6878 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
726c84eedd
|
Aligning with prism-games a bit (explicit reward stuff).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6875 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
1539fc766c
|
Aligning with prism-games a bit (explicit reward stuff).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6873 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
4ee9ed825e
|
Miscellaneous code changes/tidies - trying to align with prism-games a bit.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6871 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
6df7dbf140
|
Some code auto-formatting (for branch purposes).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6869 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
8784323e6e
|
Some code auto-formatting (for branch purposes).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6865 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
021b512512
|
Bugfix: error in recent additions to S operator type checking.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6855 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
0c229d3a39
|
CHANGELOG.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6854 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
aed65159ca
|
Import auto-tidy
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6840 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
18b4d0daa3
|
Change -exportresults to use notation <file[:<options>] not <file[,<options>]> by default.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6838 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
26c27d3af5
|
CHANGELOG.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6837 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
54a724c3cd
|
Document -exportmodel and -import model in -help.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6836 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
b899db642e
|
Revised notation for -exportmodel and -importmodel (following discussions with Hubert).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6835 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
6a218a9e6f
|
Tweak to message output when exporting labels.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6834 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
9a658794b1
|
Additional -help xxx messages.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6833 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
3ec332e2d0
|
Tweak -help.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6832 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
24f7ac5a01
|
CHANGELOG.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6830 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
f33fde1d60
|
A few -help message tweaks, and some new '-help xxx' switches (currently just for const and exportresults).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6829 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |