6143 Commits (cf478b2984c26fe8b845e71f1c86fb47660826d3)
 

Author SHA1 Message Date
dehnert 90cb987357 intermediate commit to switch workplace 7 years ago
TimQu 419fcd1b43 Fixed test 7 years ago
TimQu c9beea4f33 better lower/upper result bounds 7 years ago
TimQu 746a58ff12 better statistics output 7 years ago
TimQu 86253fe88a moved multidimensional unfolding implementation from multiobjective into helper namespace 7 years ago
TimQu 17d6835477 removed acyclic minmax method as it is not much better then gauss-seidel style multiplications 7 years ago
TimQu d85a845b7d Fixed cases where a solver guarantee was not established although it was needed by the termination condition 7 years ago
TimQu 117d1b5c99 clean up single objective reward bounded case 7 years ago
Matthias Volk c4c6c9cbce Test compiler configurations within cmake 7 years ago
dehnert 5fd7878791 added option to refine over states whose signatures changed in dd-based bisimulation 7 years ago
TimQu 016fedd58e Better progress info 7 years ago
TimQu 199d12a2c2 Merge remote-tracking branch 'origin/master' into reward-bounded-multi-objective 7 years ago
TimQu f2d837dc42 Merge remote-tracking branch 'origin/master' into reward-bounded-multi-objective 7 years ago
dehnert 518773f18f commit missing version file 7 years ago
dehnert e6f61fb441 fixed bug in hybrid engine when using interval iteration 7 years ago
TimQu 9859f60db0 Fixed solver tests 7 years ago
TimQu f44ce8801c "fixed" the tests that failed because of unsound value iteration 7 years ago
TimQu 3571f0ddca Respected that the solution is unique when doing value iteration 7 years ago
TimQu 33585c811f MinMax Solver requirements now respect whether the solution is known to be unique or not. 7 years ago
dehnert 7dcb450aad started on computing changed states in one shot 7 years ago
dehnert c85e30dfd0 added distance-aware initial partition to dd-based bisimulation 7 years ago
dehnert 9498705c95 more reuse of values in bisimulation-based abstraction refinement 7 years ago
dehnert 4fad33b5e8 started on optimizing bisimulation-based abstraction-refinement 7 years ago
dehnert 669940ccd3 only supporting reuse of nothing or of block numbers 7 years ago
dehnert 4e4526182f adding information about which technique is used to symbolic native linear equation solver 7 years ago
dehnert a19c2fe59b work on variations which data is reused in dd-based bisimulation 7 years ago
dehnert b8120ed73a Markov automaton model checker now clearing basic requirements 7 years ago
dehnert 41828ca27d more work on bisimulation-based abstraction-refinement 7 years ago
dehnert b415c12c25 further preparation of partial bisimulation model checker 7 years ago
TimQu 3215f25513 upper result bounds for cumulative reward formulas to enable interval iteration 7 years ago
TimQu d91d979d90 changed some output 7 years ago
dehnert 9c685f3bdb started on partial bisimulation model checker 7 years ago
dehnert ea507a0b13 added dd-based partial quotient extraction for DTMCs 7 years ago
dehnert ab12e4ff3d started on partial quotient extraction in symbolic bisimulation 7 years ago
dehnert d90c507431 fixed bug in sparse bisimulation quotient extraction related to rewards 7 years ago
TimQu 70dc9ce7ac Bypassing requirements check to make value iteration without a lower result bound work 7 years ago
Matthias Volk 58c8531d34 Use Carl 17.10 7 years ago
TimQu 26efa18d32 Merge remote-tracking branch 'origin/master' into reward-bounded-multi-objective 7 years ago
TimQu e3a506ecc6 Property information output 7 years ago
dehnert 34485836b8 fixed some convertNumber applications 7 years ago
Matthias Volk f47e40d363 Fixed removed variable 7 years ago
dehnert 4d7770aea6 fixed issue in hybrid reachability reward computation that caused empty row groups 7 years ago
dehnert 3185719fe5 fix for linking issue under linux, adding missing l3pp dependency l3pp_ext 7 years ago
dehnert c0f07557ed simplified state signature computation in dd-based bisimulation 7 years ago
TimQu c66175c5e0 Merge remote-tracking branch 'origin/master' into reward-bounded-multi-objective 7 years ago
dehnert 29b915ccbf fix out-of-index write in bisimulation quotienting 7 years ago
TimQu 4cadc61f19 less searches for epoch solutions 7 years ago
dehnert 0ef06fd31b re-add time output to storm output and make iterative minmax solver respect linear equation solver format for policy iteration 7 years ago
TimQu b56cd07d0e Consider only a submap of all epochsolutions for faster search 7 years ago
TimQu 5c1de03d14 fixed min prob computation for single objective case 7 years ago