Dave Parker
|
01c8e4872d
|
Pareto queries return actual point list (TileList), not void.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6226 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
8a4f1815b6
|
Reformat toString for TileList.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6225 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
aa9515c339
|
Better test for lpsolve55 Makefiles being called correctly (lib prefix empty on Windows).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6224 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
4eba6c48f3
|
Code tidy
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6223 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
db928a3402
|
Tweak/move error messages for non-supported R[C] operator.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6222 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
4d9d778515
|
Comment tweak
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6221 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
10ea5d9da0
|
Add building of new ext/ directory to Makefile.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6220 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
c6fb0ffb9b
|
Copy across ext/ directory (containing lpsolve55 and lp_solve_5.5_java) from prism-multi to trunk.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6219 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
4bbe7cf75e
|
code tidy
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6218 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
47c1a13428
|
Tidy/tweak multi-objective settings, align with others.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6216 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
6850de1ab1
|
Tweak changelog.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6215 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
0abe4e8a72
|
Remove @author tag(s), for consistency.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6214 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
b13aa417ad
|
Un-needed files (since fairnesss stuff not in this branch, currently).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6213 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
702e9e5df0
|
Corrected/added headers + copyright info.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6212 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
9b5aae301f
|
Patch in current version of multi-objective model checking (from prism-multi branch). Still need to copy across etc/ directory containing lpsolve libraries. Also contains a few JDD fixes via Christian von Essen.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6211 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
f57b1da878
|
Minor polishing in prism-auto script.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6209 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
5932841ec7
|
Update version info (to 4.1.beta1).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6208 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
dfcfb6c23f
|
Start to summarise changes in upcoming 4.1 release.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6207 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
2884b8b143
|
Better error message for non-supported S operator in explicit engine.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6206 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
2ef6a3e2ee
|
Bug fix: computing next probs in explicit engine (was not converted to embedded DTMC).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6173 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
ab63021afb
|
Javadoc typo
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6028 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
1ea340dbd2
|
Author/copyright info.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6024 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
f98a0727f3
|
CHANGELOG.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6023 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
3295869453
|
Fix mvMultRewJacSingle method for DTMCEmbeddedSimple (for Hongyang).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5780 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
9373bc0b11
|
Add mvMultRewJacSingle method for DTMCEmbeddedSimple (for Hongyang).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5777 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
08b5f75aa4
|
Bug fix: LHS of until was being ignored in explicit CTMC model checking.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5760 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
c38378ad10
|
Makefile dist_bin target adds flags for javac to target Java 1.6.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5756 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
de95d5ea89
|
Slight efficiency improvement in JDD.IsContainedIn().
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5705 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
786d2ac6a8
|
Tidy: Auto-format.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5702 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
ae798a69d9
|
Fix: explicit engine did not pick up verbose setting.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5664 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
65bb3d2d9a
|
Compiler warning.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5648 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
cd250aa6d1
|
Improved selection of matching RESULT for -test: can just have a subset of const values in the RESULT spec.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5647 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
eb8c1e9abf
|
Better error msg for unavailability of R[C<=k] for MDPs.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5638 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
84f1c97413
|
Code tidy.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5635 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
3b59b8f6cd
|
Code tidy.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5633 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
da50f86281
|
Tweak comments in policy iteration.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5632 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
eb34f465a7
|
Bounded until for DTMC/MDP in explicit engine.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5631 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
433c3a3414
|
Next operator for explicit model checker.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5629 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
4413259325
|
Explicit model checker can handle negated path operators like G.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5624 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
582ddb0e43
|
Error message typos.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5623 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
1b5dc955e6
|
Few extra methods in StateValues.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5622 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
6e2b0b789b
|
DTMC S operator model checking for explicit engine.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5621 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
fd53ce813c
|
Refactor (symbolic) steady-state computation for S operator.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5620 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
5018559d3e
|
DTMC steady-state computation for explicit engine.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5617 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
387fae41f4
|
Code comments
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5616 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
e0eca95da0
|
Refactor (symbolic) steady-state computation for S operator.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5615 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
d71fde3538
|
Refactor (symbolic) steady-state computation.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5614 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
50201cfbf7
|
Refactor single-BSCC detection in (symbolic) steady-state computation.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5613 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
271f6af317
|
Temporary compile fix.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5612 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
4f09722850
|
Added IsContainedIn method to JDD.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5601 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |