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

2731 Commits (c143d3870743ff3399f47996019c32f479ab70de)
 

Author SHA1 Message Date
Dave Parker 7da07f7b99 Small refactor in positive normal form conversion.
10 years ago
Dave Parker 0c2e16ec32 Add conversion to positive normal form for LTL as well as boolean expressions.
10 years ago
Joachim Klein 6f8b090ef0 Settings: remove debug output for -ltl2datool argument
10 years ago
Dave Parker e140741c0a Remove unused method from BooleanUtils.
10 years ago
Joachim Klein f1aa7edc01 dv.cc/iv.cc: When converting from an MTBDD, check that we don't write outside of the DoubleVector/IntegerVector
10 years ago
Dave Parker d791bce62f Add some more options to LTL2DA program
10 years ago
Dave Parker 6e5a62eb42 Add some more options to LTL2DA program
10 years ago
Dave Parker 7f6c068e8b Add a simple command-line test program (LBT->HOA) to LTL2DA.
10 years ago
Dave Parker 5145992646 Bug fix in Expression.isPositiveNormalFormLTL: do not assume type checking has already been done.
10 years ago
Dave Parker 81f73d19d7 Bugfix in new SimpleLTL-to-Expression method.
10 years ago
Dave Parker fe305344df Utility function to create an Expression from an LTL formula represented as a jltl2ba SimpleLTL object (i.e., the reverse of Expression.convertForJltl2ba()).
10 years ago
Dave Parker ad238d314c Allow -exportpropaut to export DA in HOA format, e.g.: prism dice.pm -pf "P=?[X X d=6]" -exportpropaut:hoa da.hoa
10 years ago
Joachim Klein c79a27b218 HOAF2DA: add main() method to provide command-line interface for testing deterministic HOA parsing.
10 years ago
Joachim Klein fd46caec64 Add Jltl2dstarCmdLine command-line interface for LTL -> DRA functionality (for testing)
10 years ago
Joachim Klein 449b06ef8f Add Jltl2baCmdLine command-line interface for LTL -> NBA functionality (for testing)
10 years ago
Joachim Klein b1863bb528 automata.DA: printHOA()
10 years ago
Joachim Klein f449803020 Acceptance: add outputHOAHeader()
10 years ago
Joachim Klein 4bd03ef854 Acceptance: add getSignatureForStateHOA()
10 years ago
Joachim Klein 5cafc40cb9 AcceptanceGeneric: add missing getSignatureForState() functionality
10 years ago
Joachim Klein 1a17950deb AcceptanceGeneric: add getLoafNodes() helper
10 years ago
Joachim Klein 96600e7a2f jltl2dstar.DA: printHOA
10 years ago
Joachim Klein 490642291d jltl2dstar.DA: fix print (ltl2dstar format output)
10 years ago
Joachim Klein 80a78f9ec5 jltl2dstar.NBA: printing in LBTT and HOA format
10 years ago
Joachim Klein 6d3bfff9a6 jltl2ba.APElement: printing in LBTT / HOA format
10 years ago
Joachim Klein 5d3adc211c jltl2ba.APSet: add print_hoa()
10 years ago
Joachim Klein ca47143da5 SimpleLTL: add parsing functionality for LBT(T) formulas (prefix format)
10 years ago
Dave Parker 9b039439c2 Bug fix in export of simulation path (to a file): file should be closed on completion.
10 years ago
Joachim Klein 2b07700f5f StateValues: new method filter(dd, double), sets values not in filter to d
11 years ago
Joachim Klein af3af9dc8d StateValues: Consolidate documentation, add REF/DEREF information
11 years ago
Joachim Klein 5d30703654 StateValues: small rename for consistency
11 years ago
Joachim Klein 85ed9b8f17 DoubleVector: Document ref/deref
11 years ago
Joachim Klein 4300731de6 Add JDD.Times: Syntactic sugar for multi-operand JDD.Apply(TIMES, ...)
11 years ago
Joachim Klein 941e45affd Add JDD.isSingleton
11 years ago
Joachim Klein 9fc0e5b07a symbolic StateModelChecker: deref filter if the recursive checkExpression call throws an exception
11 years ago
Joachim Klein 9a814f226b symbolic ProbModelChecker: Fix JDDNode reference issues for total reward computation
11 years ago
Joachim Klein ab136ae5e2 JDDNode.getThen() and getElse(): Protect against calls for a constant node, which is invalid.
11 years ago
Joachim Klein c26c995957 Add -dddebug and -ddtrace command-line arguments to PrismCL
11 years ago
Joachim Klein 19f422a472 Refactor DebugJDD handling, add node tracing.
11 years ago
Joachim Klein ea8a7c6ba9 Add DebugJDD_GetExternalRefCounts
11 years ago
Joachim Klein 54b5c42121 JDDNode: make DDN_ JNI functions protected and static
11 years ago
Dave Parker ec47bf753a Remove "KB" from "CUDD max. memory" option description.
11 years ago
Dave Parker cbafeeecbf Tweak CUDD out-of-memory error output in GUI.
11 years ago
Dave Parker 63812e59a5 Auto-format (for merging purposes).
11 years ago
Joachim Klein 0d00e9097e AcceptanceRabinDD, AcceptanceStreettDD: add complement and and(), or() methods
11 years ago
Joachim Klein 555e5ae69a Acceptance: add complement functionality, some more comments
11 years ago
Joachim Klein 96caf197ab dd_matrix.cc: fix recently introduced error handling
11 years ago
Dave Parker f930d8e60f Tweak CUDD out-of-memory error output.
11 years ago
Dave Parker f601843c59 prism-auto bug fix (crashes when run on a single model in build mode).
11 years ago
Dave Parker 4258503c80 Make DD_MatrixMultiply deal with memout in the same was other DD functions.
11 years ago
Dave Parker bfecd70db9 Small code fix in DD_MatrixMultiply.
11 years ago