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

131 Commits (038ed779ff56cae96d13016ed9986e3ca60541d5)

Author SHA1 Message Date
Joachim Klein 038ed779ff ExportIterations: Log the file name when exporting iterations (2)
8 years ago
Joachim Klein 7edb481d76 Hybrid/sparse: Add check against state index overflow also to interval iteration methods
9 years ago
Joachim Klein 5adb550043 Makefiles: inhibit parallel building (-j n mode)
9 years ago
Joachim Klein 83e6c291b0 (native) switch includes from .h to C++ header wrappers
9 years ago
Joachim Klein 7c5eb10d37 PH,PM,PS: cast jints to int in printf
9 years ago
Joachim Klein 7d874df348 PrismMTBDD, PrismSparse export_string: Pass via "%s" to log
9 years ago
Joachim Klein 6b856bce86 PH, PS: log errors via "%s"
9 years ago
Joachim Klein a8b8daaf71 PS: cleanup warning message printing
9 years ago
Joachim Klein 2bb7a217f2 PS: cleanup format strings
9 years ago
Joachim Klein 14ad1d32af fix compilation issue: cmath / isinf
9 years ago
Joachim Klein c1efd5233b (interval iteration, symbolic) interval iteration variants for the computation methods of MTBDD, Hybrid and Sparse
9 years ago
Joachim Klein 7c612640da PS iteration methods: use MeasureSupNorm. MultiObjective remains todo.
9 years ago
Joachim Klein 3c2a2232e1 (export-iterations) Sparse engine: If enabled, export iterations to HTML file
9 years ago
Joachim Klein 30f7def86c (export-iterations) introduce --exportiterations option, ExportIterations helper classes for C and Java
9 years ago
Joachim Klein cc90e7a20c Sparse engine: Error if number of reachable states is too large
9 years ago
Joachim Klein 732d224bd7 Win64 cleanup, sparse_adv.cc: avoid pointer-to-integer casts
9 years ago
Joachim Klein 4c134da06d Win64 cleanup, PS_NondetMulti*: avoid pointer-to-integer casts
9 years ago
Joachim Klein 9850ae3c71 sparse engine: consistently use delete[] when destroying solution vectors
10 years ago
Dave Parker 3b68b5e0a9 Bug fix: respect disable_selfloop setting during adversary generation in LP-based multi-objective model checking.
10 years ago
Vojtech Forejt 4562006bb0 fixed multiobjective lp bug where the reward objective function was not set if there were no PCTL targets.
11 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.
11 years ago
Dave Parker 5ab01f26b8 Refactoring + tidying in multi-objective value iteration.
11 years ago
Dave Parker d52576a6dd Refactoring + tidying in multi-objective value iteration.
11 years ago
Dave Parker 91c8af3aac Refactoring + tidying in multi-objective value iteration.
11 years ago
Dave Parker 1493a0c6c5 Refactoring in multi-objective value iteration: move check for step-bounded with GS.
11 years ago
Dave Parker 3afca48506 More info printed out by multi-objective value iteration + more efficient vector access.
11 years ago
Dave Parker a64997f903 Bugfixes in sparse engine adversary generation (cumulative reward and multi-objective): remove second stat line.
11 years ago
Dave Parker 91d984cce8 Add some adversary generation for multi-objective value iteration (just exports one adv for each separated weighted objective).
11 years ago
Dave Parker ff05caf158 Code tidy.
11 years ago
Dave Parker cd859b45db Multi-objective value iteration: generate (but do not yet export) adversaries for each weighted query.
11 years ago
Dave Parker 655cfb3550 Some tidying in multi-objective code.
11 years ago
Dave Parker 09bebccb52 Some tidying in multi-objective code.
11 years ago
Dave Parker 2806712f80 Some tidying in multi-objective code.
11 years ago
Dave Parker 412ac91a61 Bug fix in multi-objective value iteration: non-convergence when one objective has weight 0.
11 years ago
Dave Parker 1eb73ab127 Update sparse engine adversary generation to include number of transitions in the tra file.
11 years ago
Dave Parker 7eef2a266c Fix a few compiler warnings.
11 years ago
Dave Parker 913f80a8e9 Minor refactoring and alignment between PS_NondetMultiReach.cc and PS_NondetMultiReach1.cc.
12 years ago
Dave Parker 9589a14c14 Compile fix for previous commit.
12 years ago
Dave Parker 1d09274252 Add adversary export to reward-based multi-objective model checking (sparse engine) - not sure why it was not there.
12 years ago
Dave Parker 1dc1e484b7 Tidy up JNI wrapper around NDSparseMatrix and push action index storage inside the data structure.
13 years ago
Dave Parker 0e9b9c38e7 Makefile fixes: stop javah-created headers showing as modified in Cygwin svn due to line endings.
13 years ago
Dave Parker 9b2d57fccd Missing file from last commit.
13 years ago
Dave Parker edcac4a4a2 Added R[C<=k] operator for MDPs (sparse, explicit).
13 years ago
Dave Parker 80ddd4be4b Some additions to Strategy classes + better integration of symbolic strategy generation.
13 years ago
Dave Parker 2837f71036 First (partial) connection of sparse adversary generation to Strategy classes and -exportstrat.
13 years ago
Dave Parker 026359ea2f Undo last commit
13 years ago
Dave Parker 2c5a9de4f8 Code tidy: imports.
13 years ago
Dave Parker d1046f553b Typos (fix from Gaston Ingaramo).
13 years ago
Dave Parker 96992ff1c9 Make error_message vars static in sparse/hybrid/mtbdd engines - reportedly causes crashes otherwise (fix from Gaston Ingaramo).
13 years ago
Vojtech Forejt 772767fcd7 * maximal number of iteration was changed in C++ code which influenced subsequent runs
14 years ago