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

30 Commits (4e939c529babb0978dd7aef4ea549671ab113769)

Author SHA1 Message Date
Joachim Klein 16f63dd580 imported patch rewardcounter-reward-bound-checks.patch
8 years ago
Joachim Klein 3757da3fa0 imported patch rewardcounter-TemporalOperatorBounds-use.patch
8 years ago
Joachim Klein 7345668608 imported patch rewardcounter-TemporalOperatorBound-use.patch
8 years ago
Joachim Klein 57b68f6f9d Statistical MC: Fix infinite sampling for lower bounded P[F]/P[U]
8 years ago
Joachim Klein 37fad8894e SamplerBoundedUntilDisc: tweak handling of absent upper bound
8 years ago
Joachim Klein 367a2bd717 Statistical MC: Check bounds for CTMC bounded until
8 years ago
Joachim Klein 2261b32586 SamplerRewardReach: minor cleanup in constructor
9 years ago
Joachim Klein f518d66c6c Sampler: fix logic for rejecting co-safety path formulas in reward samplers (fixes previous commit)
10 years ago
Joachim Klein a325400ba2 Sampler.createSampler: For reward properties, catch the new case of a co-safety path formula properly
10 years ago
Dave Parker 48147aa4ad Improvements to the SamplerDouble class: revised approach to variance estimation for better numerical stability (contributed by Marcin Copik), plus some further tidying/documentation.
10 years ago
Dave Parker a76b3c73bd Remove (most) usage of R_F in temporal operators.
11 years ago
Dave Parker caf5a0e50b Bugfix: statistical model checking of discrete-time bounded untils with strict bounds (from Joachim Klein).
12 years ago
Dave Parker 8e2bc361cd Improve simulation Sampler classes to handle deadlocks (in some cases). Deadlocks still not properly handled by the simulator.
12 years ago
Dave Parker 02c26dbf53 Update simulator to allow path lengths over 2^31.
13 years ago
Dave Parker db928a3402 Tweak/move error messages for non-supported R[C] operator.
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.
14 years ago
Dave Parker 0245cf77b4 Bug fix: crash on invalid integer reward struct indices.
14 years ago
Dave Parker aca617849b Some optimisations for approximate model checking on models with deadlocks (could do other operators too).
15 years ago
Dave Parker f578bbb893 Approximate model checking ignores "max path length" setting when verifying time-bounded properties.
15 years ago
Dave Parker 45da0e31ae Bugfix: exception when checking R[I] properties with simulator.
15 years ago
Dave Parker e4d1d0c10c Bugfix in simulator: Wrong answers for R=?[C<=t] properties on CTMCs.
15 years ago
Dave Parker 35f377ab3e Improved documentation (JavaDoc mostly).
15 years ago
Dave Parker 53a5274cb3 Addition of new statistical model checking stuff (patch difference between trunk and prism-statmc branch at this revision).
16 years ago
Dave Parker fcf236acd3 Added (self-loop) deterministic loop detection to simulator.
16 years ago
Dave Parker bcd6110358 Simulator updates: fixed display of transitions in GUI, added (some) detection of deadlocks/self-loops. (And some tidying.)
16 years ago
Dave Parker a0db106a88 Tweaks to Sampler design + non-compilation bugfix.
16 years ago
Dave Parker bb2615b43b Further work on simulator.
16 years ago
Dave Parker 6dc06b42b7 Fixes and tidies to the simulator.
16 years ago
Dave Parker 7039eb385c Further work on simulator, including sampling.
16 years ago
Dave Parker 4ee4fb211a Further work on simulator, including sampling.
16 years ago