Vojtech Forejt
|
4562006bb0
|
fixed multiobjective lp bug where the reward objective function was not set if there were no PCTL targets.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11065 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
10 years ago |
Dave Parker
|
619b7d53c5
|
Re-enable disabled convergence check in multi-objective value iteration since it can give the wrong answer. Better fix follows.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10890 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
11 years ago |
Dave Parker
|
5ab01f26b8
|
Refactoring + tidying in multi-objective value iteration.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10885 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
11 years ago |
Dave Parker
|
d52576a6dd
|
Refactoring + tidying in multi-objective value iteration.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10884 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
11 years ago |
Dave Parker
|
91c8af3aac
|
Refactoring + tidying in multi-objective value iteration.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10883 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
11 years ago |
Dave Parker
|
1493a0c6c5
|
Refactoring in multi-objective value iteration: move check for step-bounded with GS.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10882 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
11 years ago |
Dave Parker
|
3afca48506
|
More info printed out by multi-objective value iteration + more efficient vector access.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10880 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
11 years ago |
Dave Parker
|
a64997f903
|
Bugfixes in sparse engine adversary generation (cumulative reward and multi-objective): remove second stat line.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10831 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
11 years ago |
Dave Parker
|
91d984cce8
|
Add some adversary generation for multi-objective value iteration (just exports one adv for each separated weighted objective).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10829 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
11 years ago |
Dave Parker
|
ff05caf158
|
Code tidy.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10815 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
11 years ago |
Dave Parker
|
cd859b45db
|
Multi-objective value iteration: generate (but do not yet export) adversaries for each weighted query.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10814 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
11 years ago |
Dave Parker
|
655cfb3550
|
Some tidying in multi-objective code.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10813 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
11 years ago |
Dave Parker
|
09bebccb52
|
Some tidying in multi-objective code.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10812 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
11 years ago |
Dave Parker
|
2806712f80
|
Some tidying in multi-objective code.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10811 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
11 years ago |
Dave Parker
|
412ac91a61
|
Bug fix in multi-objective value iteration: non-convergence when one objective has weight 0.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10806 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
11 years ago |
Dave Parker
|
1eb73ab127
|
Update sparse engine adversary generation to include number of transitions in the tra file.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10092 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
11 years ago |
Dave Parker
|
7eef2a266c
|
Fix a few compiler warnings.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10059 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
11 years ago |
Dave Parker
|
913f80a8e9
|
Minor refactoring and alignment between PS_NondetMultiReach.cc and PS_NondetMultiReach1.cc.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9528 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
11 years ago |
Dave Parker
|
9589a14c14
|
Compile fix for previous commit.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9526 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
11 years ago |
Dave Parker
|
1d09274252
|
Add adversary export to reward-based multi-objective model checking (sparse engine) - not sure why it was not there.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9524 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
11 years ago |
Dave Parker
|
1dc1e484b7
|
Tidy up JNI wrapper around NDSparseMatrix and push action index storage inside the data structure.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7609 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
0e9b9c38e7
|
Makefile fixes: stop javah-created headers showing as modified in Cygwin svn due to line endings.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7550 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
9b2d57fccd
|
Missing file from last commit.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7509 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
edcac4a4a2
|
Added R[C<=k] operator for MDPs (sparse, explicit).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7508 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
80ddd4be4b
|
Some additions to Strategy classes + better integration of symbolic strategy generation.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7169 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
2837f71036
|
First (partial) connection of sparse adversary generation to Strategy classes and -exportstrat.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7119 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
026359ea2f
|
Undo last commit
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7075 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
2c5a9de4f8
|
Code tidy: imports.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7074 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
d1046f553b
|
Typos (fix from Gaston Ingaramo).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6818 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Dave Parker
|
96992ff1c9
|
Make error_message vars static in sparse/hybrid/mtbdd engines - reportedly causes crashes otherwise (fix from Gaston Ingaramo).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6817 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
13 years ago |
Vojtech Forejt
|
772767fcd7
|
* maximal number of iteration was changed in C++ code which influenced subsequent runs
* when step bounded was run in GS, a segfault took place before an error could be shown
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6257 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Vojtech Forejt
|
f2b3b9bd7b
|
disabling ignored weights due to a numerical problem (multi(Pmax=?[F s1=7&s2=7&d1+d2=7],Pmax=?[F s1=7&s2=7&d1+d2=8]) with two-dice.nm)
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6256 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
5f7ff4e762
|
Compile fix (for Windows).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6248 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
9074396fc1
|
Compile fix (for Windows).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6247 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 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
|
14 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
|
14 years ago |
Dave Parker
|
7725e3b89c
|
Add intermittent progress updates to numerical solution (sparse engine).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5263 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
07bf18a2f4
|
Fix makefiles with easier setup of classpath using * for jars.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4889 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Vojtech Forejt
|
e3f6e64e7a
|
package-info.java is ignored in makefiles
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4380 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
14 years ago |
Dave Parker
|
3e4c617a81
|
Move most native code options from engine shared libraries to prism library.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4277 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
ab6d2bbbef
|
Remove use of -lm linking under Cygwin.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4253 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
f344411a3c
|
Fixes in C-code warning message functions.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4180 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 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
|
15 years ago |
Dave Parker
|
f61753b14e
|
Slight changes to exporttransdot format (to match explicit): boxes bot circles for states (works better when there are state labels) and larger dots for mdp transitions.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3283 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
b102e6aaf7
|
Missing error messages (in GUI) about unsupported numerical methods.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2932 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Vojtech Forejt
|
abda1ed33a
|
additional changes re setting mainlog and techlog in native calls
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2577 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Vojtech Forejt
|
6e3b126188
|
corrected a problem with setting mainlog and techlog in native calls
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2576 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
35f377ab3e
|
Improved documentation (JavaDoc mostly).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2436 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
15 years ago |
Dave Parker
|
52e3d712e7
|
Added -exportadvmdp switch.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2154 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
16 years ago |
Dave Parker
|
48a2e4bcc8
|
Undo last commit.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2151 bbc10eb1-c90d-0410-af57-cb519fbb1720
|
16 years ago |