Joachim Klein
fd46caec64
Add Jltl2dstarCmdLine command-line interface for LTL -> DRA functionality (for testing)
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10535 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Joachim Klein
449b06ef8f
Add Jltl2baCmdLine command-line interface for LTL -> NBA functionality (for testing)
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10534 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Joachim Klein
b1863bb528
automata.DA: printHOA()
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10533 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Joachim Klein
f449803020
Acceptance: add outputHOAHeader()
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10532 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Joachim Klein
4bd03ef854
Acceptance: add getSignatureForStateHOA()
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10531 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Joachim Klein
5cafc40cb9
AcceptanceGeneric: add missing getSignatureForState() functionality
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10530 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Joachim Klein
1a17950deb
AcceptanceGeneric: add getLoafNodes() helper
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10529 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Joachim Klein
96600e7a2f
jltl2dstar.DA: printHOA
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10528 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Joachim Klein
490642291d
jltl2dstar.DA: fix print (ltl2dstar format output)
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10527 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Joachim Klein
80a78f9ec5
jltl2dstar.NBA: printing in LBTT and HOA format
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10526 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Joachim Klein
6d3bfff9a6
jltl2ba.APElement: printing in LBTT / HOA format
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10525 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Joachim Klein
5d3adc211c
jltl2ba.APSet: add print_hoa()
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10524 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Joachim Klein
ca47143da5
SimpleLTL: add parsing functionality for LBT(T) formulas (prefix format)
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10523 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Dave Parker
9b039439c2
Bug fix in export of simulation path (to a file): file should be closed on completion.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10520 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Joachim Klein
2b07700f5f
StateValues: new method filter(dd, double), sets values not in filter to d
Adapt DoubleVector to make value for filter user-definable.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10516 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
af3af9dc8d
StateValues: Consolidate documentation, add REF/DEREF information
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10515 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
5d30703654
StateValues: small rename for consistency
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10514 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
85ed9b8f17
DoubleVector: Document ref/deref
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10513 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
4300731de6
Add JDD.Times: Syntactic sugar for multi-operand JDD.Apply(TIMES, ...)
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10512 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
941e45affd
Add JDD.isSingleton
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10511 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
9fc0e5b07a
symbolic StateModelChecker: deref filter if the recursive checkExpression call throws an exception
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10510 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
9a814f226b
symbolic ProbModelChecker: Fix JDDNode reference issues for total reward computation
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10509 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
ab136ae5e2
JDDNode.getThen() and getElse(): Protect against calls for a constant node, which is invalid.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10508 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
c26c995957
Add -dddebug and -ddtrace command-line arguments to PrismCL
-dddebug activates the DebugJDD mechanism, while -ddtrace id will
trace refs/derefs of the JDDNode with the given ID. -ddtrace implies
-dddebug. Due to the additional efforts spent to keep track of the
information, DebugJDD mode can slow-down model checking and increase
memory usage.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10507 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
19f422a472
Refactor DebugJDD handling, add node tracing.
The DebugJDD class provides Java-side reference counting for
JDDNodes and tries to detect problems with the reference counting,
such as to many derefs (can lead to crashes during garbage collection)
or too few derefs (leads to memory leakage and a warning when exiting
PRISM).
When debugging is enabled, each JDDNode is assigned a unique, sequential
ID that should be stable across runs of PRISM with the same command-line
arguments, in contrast to the underlying CUDD DDNode pointers, which can
and do change with each invokation.
A tracing mechanism allows to print all the ref/deref events for a particular
JDDNode.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10506 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
ea8a7c6ba9
Add DebugJDD_GetExternalRefCounts
Analyze the BDD and return the implied number of external references per node
in a map (node -> count). Only return nodes with non-zero external references.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10505 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
54b5c42121
JDDNode: make DDN_ JNI functions protected and static
This way, they can be accessed by other classes in the jdd package.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10504 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Dave Parker
ec47bf753a
Remove "KB" from "CUDD max. memory" option description.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10503 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Dave Parker
cbafeeecbf
Tweak CUDD out-of-memory error output in GUI.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10502 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Dave Parker
63812e59a5
Auto-format (for merging purposes).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10497 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
0d00e9097e
AcceptanceRabinDD, AcceptanceStreettDD: add complement and and(), or() methods
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10495 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
555e5ae69a
Acceptance: add complement functionality, some more comments
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10494 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
96caf197ab
dd_matrix.cc: fix recently introduced error handling
+ some whitespace cleanup
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10493 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Dave Parker
f930d8e60f
Tweak CUDD out-of-memory error output.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10492 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Dave Parker
f601843c59
prism-auto bug fix (crashes when run on a single model in build mode).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10491 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Dave Parker
4258503c80
Make DD_MatrixMultiply deal with memout in the same was other DD functions.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10490 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Dave Parker
bfecd70db9
Small code fix in DD_MatrixMultiply.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10489 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Dave Parker
3abbac6491
Fix: Allow -javamaxmem to be passed to the GUI (xprism) too.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10488 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
4dfcd39fd1
dd_*.cc: Argument checking, if any DdNode is NULL return NULL
This allows nesting of DD_ functions in the presence of CUDD memory errors.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10487 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
f559e0adb8
Return NaN for DD_FindMin / DD_FindMax on CUDD out of memory
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10486 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
eecc87786a
CuDD is actually called CUDD
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10485 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Dave Parker
5ad8ef2269
Small typos
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10484 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
68e0a80b98
GUI computation threads: Catch more errors (e.g. CuddOutOfMemoryException) and use the new error(Exception) handling
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10483 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
a9630648b0
GUIComputationThread: Add method for logging generic Exceptions
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10482 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
9ed1674013
PrismCL: Catch CuddOutOfMemoryException and print helpful message
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10481 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
91cb0f7e36
JDD: Use checkForCuddError() for DD functions that don't return a node
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10480 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
e9897b4838
dd_matrix.cc: Add NULL checks for the return values of DD functions
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10479 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
efe6fe0ef9
dd_vars.cc: Add NULL checks for the return values of DD functions
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10478 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
90326ecfaf
dd_term.cc: Add NULL checks for the return values of DD functions
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10477 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
62bc1cc1d0
dd_basics.cc: Add NULL checks for the return values of DD functions
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10476 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago