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
Joachim Klein
3be99a61cf
dd_abstr.cc: Add NULL checks for the return values of DD functions
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10475 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
9ce369d38e
JDD: Add a flag that can be set/checked in native code to indicate that a CuDD error has occurred.
For DD functions that return a DdNode*, errors can be reported by returning NULL.
Functions that have no return value (printing, etc) or a data value (double, etc)
should set the flag, which can be converted into an CuddOutOfMemoryException on
the PRISM side using JDD.checkForCuddError()
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10474 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
2c2533eda8
JDD: Check for NULL ptr in Ref/Deref
Normally, we should catch the construction of JDDNodes with NULL pointers
beforehand, but for robustness we make sure that we do not call Cudd_Ref
and Cudd_Deref for a NULL DdNode*, as that leads to SIGSEGV crashes.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10473 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
f23d831b32
JDD: Throw CuddOfOutMemoryException for ptrToNode(NULL)
The native DD/CuDD methods return NULL to indicate that
an out-of-memory error in CuDD has occurred. Before, we
constructed a JDDNode for this NULL ptr, which would lead
to a SIGSEGV crash the next time any operation
(ref, deref, etc) would be performed on that JDDNode.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10472 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
379918beea
JDD: Switch to JDDNode ptrToNode(long ptr) as a single point for converting from a DD long pointer to a referenced JDDNode.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10471 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Dave Parker
32e6c16015
Undo accidental part of last commit.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10465 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Dave Parker
e2d1f0af25
Bug fix in CNF conversion.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10461 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Dave Parker
795627c953
Add partial support for multi-objective queries expressed as Boolean expressions.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10456 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Dave Parker
d44e1c7ecc
Bug fix in Coalition copy constructor.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10455 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago