6227 Commits (c5e356bc40956c22c2e2c3b41d2bd1a0e1a055d9)
 

Author SHA1 Message Date
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
dehnert 8204c03c0b fixed a ton of warnings 7 years ago
dehnert bb890cb91f Merge branch 'master' into rationalsearch 7 years ago
TimQu 5071df5c82 made sound value iteration work and respect the correct precision 7 years ago
Sebastian Junges ccfb1a292c drn parser and exporter use reward names 7 years ago
Sebastian Junges 2ce145745a parameters from rewards are now also collected in wellformedness analysis 7 years ago
Sebastian Junges 6832fc805c parser improvements in changelog 7 years ago
Sebastian Junges 378e2ee40f Better error message if expression parser fails 7 years ago
dehnert 02c23865da reworked memory leak solution in sylvan according to Tom van Dijks hints 7 years ago
TimQu 9140c1dc0e statistics and empty-epoch-matrix optimization also for single objective case 7 years ago
TimQu 108e8e69e8 Changed statistics output a little. Optimized the case where the transition matrix of the epoch model is empty 7 years ago
dehnert 8adb1b75bd Merge branch 'master' of https://srv-i2.informatik.rwth-aachen.de/scm/git/storm 7 years ago
dehnert 72d58b6155 fix for sylvan workers not releasing mmap'ed memory 7 years ago
Matthias Volk dc78ea9c9e Merge branch 'dft-refactor' 7 years ago
Matthias Volk 4c19c60fb5 Merge branch 'master' of https://srv-i2.informatik.rwth-aachen.de/scm/git/storm 7 years ago
Matthias Volk 0913388cd3 Renamed ExplicitDFTModelBuilderApprox to ExplicitDFTModelBuilder 7 years ago
dehnert 8f95032d34 not logging exceeding precision in Kwek-Mehlhorn 7 years ago