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

2986 Commits (a8a3639ee7eec9625105c97df5a1495092eb187b)
 

Author SHA1 Message Date
Joachim Klein a8a3639ee7 NondetModelChecker: use more PrismNotSupportedExceptions instead of PrismExceptions
10 years ago
Joachim Klein 1621fb31c7 mtbdd/PM_NondetInstReward.cc: comment typo
10 years ago
Joachim Klein 7f48229dc1 Prism.modelCheckExact: Properly handle boolean results
10 years ago
Joachim Klein 0632eb656a PrismCL: Catch unhandled Exceptions instead of delegating to default Java handling
10 years ago
Joachim Klein eb017f950c prism.SCCComputer: SanityJDD checks
10 years ago
Joachim Klein 36f4e3f81f prism.ECComputer: SanityJDD checks
10 years ago
Joachim Klein 296f589631 JDD.isSingleton: fix broken computation
10 years ago
Dave Parker 4626d529a5 Code tidy
10 years ago
Dave Parker 09c5b11a74 Bug fix in ConstructModel - do not call attachLabels in justReach mode.
10 years ago
Joachim Klein 0e57919d0e explicit engine: Properly signal "not supported" for MDP total reward computations
10 years ago
Dave Parker bd9f2f255d Add slightly more efficient implementation of getChoiceAction for PRISM models.
10 years ago
Dave Parker 41f4b886ce Minor code tidy
10 years ago
Dave Parker 50e13bca29 Add new getChoiceAction method to ModelGenerator interface, which is basically an alias for getTransitionAction(i, 0).
10 years ago
Dave Parker f76e72827e Correct error in documentation for ModelGenerator interface.
10 years ago
Dave Parker 9fb9d0ae26 Bug fix in StateListMTBDD.getIndexOfState.
10 years ago
Dave Parker 9eff92431e Bug fix in computation (and therefore display) of progress percentage during statistical model checking.
10 years ago
Joachim Klein e5b7f3297b Symbolic engines: Clear ODD when clearing the model (fix memory leak)
10 years ago
Joachim Klein 123734eeab Infrastructure for deallocating ODDs
10 years ago
Dave Parker fba209b7f3 New getIndexOfState method in prism.StateList (not tested yet).
10 years ago
Dave Parker 8e38d2b7dd Some tidying + documentation in prism.StateList classes.
10 years ago
Joachim Klein 4cca315ef2 Add JDD.FindMinPositive (minimal positive terminal constant of an MTBDD)
10 years ago
Joachim Klein abb2b4a403 ProbModel: add resetStateRewards (analogous to resetTransRewards)
10 years ago
Joachim Klein 71975abdf7 JavaDoc: improve documentation of ProbModel.resetTrans and ProbModel.resetTransRewards
10 years ago
Joachim Klein 95e3e532ba SanityJDD: allow check methods to be called without having to globally enable sanity checks
10 years ago
Joachim Klein 888d62633d DebugJDD: Move JNI methods to JDD class
10 years ago
Joachim Klein 723c9123c8 mtbdd.PrismMTBDD: JavaDoc for reachability, prob precomputation methods, add sanity checks
10 years ago
Joachim Klein 338d76503c jdd.JDD: add sanity checks (SanityJDD framework)
10 years ago
Joachim Klein 803ac5b64c PrismSettings: add -ddsanity option
10 years ago
Joachim Klein f81f447ba3 Add SanityJDD: Framework for performing basic sanity checks on the symbolic MTBDD operations
10 years ago
Joachim Klein a7f0aff6e4 JDD: add JDD.IsZeroOneMTBDD() method for checking if an MTBDD is a 0/1-MTBDD
10 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
Joachim Klein c70922c329 GUISimulator, path formulae view: For P[ phi ] properties, display only the inner path formula phi
10 years ago
Joachim Klein 4f165146b1 GUISimulator: reactivate the display of path formulae in the corresponding simulator tab [reported by Steffen Märcker]
10 years ago
Dave Parker 29b9286be3 Add some missing methods to DTMCFromMDPAndMDStrategy.
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 95c3f7db43 Add a missing method in DTMCFromMDPAndMDStrategy.
10 years ago
Dave Parker d309f8c748 Comment fix.
10 years ago
Dave Parker 2398010959 Small fix in OpRelOpBound toString method.
10 years ago
Joachim Klein fd6aa0814d NondetModelChecker.checkRewardCoSafeLTL: We have to intersect the goal states (AcceptanceReach) with model.getReach()
10 years ago
Joachim Klein c9f30162c7 JDD: fix typos in comment for JDD.isSingleton
10 years ago
Joachim Klein 7ee83e31ba DebugJDD: update (generated) DebugJDD.h with the information about light-weight nodes
10 years ago
Joachim Klein 6ca3e63d85 DebugJDD: add test cases for getThen(), getElse() and getValue() calls
10 years ago
Joachim Klein eda77943df DebugJDD: add SuppressWarning("unused") to some of the test cases
10 years ago
Joachim Klein 238785213a DebugJDD: Improved handling of JDDNode.getThen(), JDDNode.getElse(); allow copy() on such nodes
10 years ago
Joachim Klein ef2d15c256 JDDNode.getThen() / getElse(): reintroduce sanity check against asking constant nodes for then/else
10 years ago
Joachim Klein 71f2bb389f DebugJDD: fix variable name typo
10 years ago
Joachim Klein 3729d85d37 DebugJDD: Improve source formatting
10 years ago
Joachim Klein 146dbe8ade DebugJDD: main() to run small test cases
10 years ago
Joachim Klein 23e61ea93a DebugJDD: Improve tracing for "Copied from" case
10 years ago