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

3062 Commits (2a38cf110bb4928530bf9415237747073efbc066)
 

Author SHA1 Message Date
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
Joachim Klein c3ce49be34 DebugJDD: fix Copy() case, directly use JDD.DD_Deref to avoid misleading tracing output
10 years ago
Joachim Klein 36ca47cfd8 Multi-objective LTL: Improve reference counting handling
10 years ago
Joachim Klein 45e8894f12 DebugJDD: reset tracking data when CUDD is shutdown
10 years ago
Joachim Klein 861883963c DebugJDD: Improved ref count debugging for JDD, new options
10 years ago
Joachim Klein b2e4a120be JDD: Change scope of DD_Ref and DD_Deref to "package" (to allow calls from DebugJDD)
10 years ago
Dave Parker 67616712b0 Author list - used for svn-git mirroring.
10 years ago
Dave Parker 4b1fbe2ba0 CHANGELOG.
10 years ago
Dave Parker ec0428f084 Update parser files to version 6.0 of JavaCC.
10 years ago
Dave Parker 1aa8a3eb71 CHANGELOG update.
10 years ago
Dave Parker 09a9693138 Change location of documentation sources in Makefile.
10 years ago
Dave Parker 2226e6eb91 Version num 4.3 -> 4.3.1 (keep in sync with minor change to public release).
10 years ago
Dave Parker 26a73e3248 Fix Cygwin launch scripts to handle paths with spaces in.
10 years ago
Dave Parker cd4e8cba19 Fix for Mac launch scripts - find right Java executable to avoid DYLD_LIBRARY_PATH problems.
10 years ago
Dave Parker 4a9c6cb7a8 Make sure automata package is rebuilt when needed from Makefile.
10 years ago
Dave Parker b76fe0e8b1 Add -exportprodvector switch, which exports solution vector over product model after checking LTL-based properties. Currently, supported in explicit engine, or symbolic engines where the result ends up being a vector of doubles (not an MTBDD).
10 years ago
Joachim Klein 73a4ccf44f SimulatorEngine: fix broken display of updates a path (GUI, regression) [with Linda Leuschner]
10 years ago
Joachim Klein 7ddf026889 APSet: add asList() convenience method
10 years ago
Joachim Klein c32cf2c94c jltl2ba.APSet: source format, tidy up comments
10 years ago
Joachim Klein 32ffab4e94 jltl2ba.APSet: comments, add Iterable<APElement> elements() method
10 years ago
Joachim Klein ae4b8c929e MDP model checking: allow Büchi acceptance
10 years ago
Joachim Klein 204f972abb LTLModelChecker: add support for EC computations against Büchi acceptance
10 years ago
Joachim Klein 32cee09a72 HOAF2DA: Handle Buchi acceptance in HOA automata
10 years ago
Joachim Klein 85a96b0ee9 HOAF2DA: Handle Streett acceptance in HOA automata
10 years ago
Joachim Klein 9611929efc prism/LTLModelChecker: add remark to TODO
10 years ago