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
Joachim Klein
ec590ec1ee
JDD: remove 'import PrismException' introduced in last commit, not needed
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10454 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
fbf968e060
JDD: add PrintMinterms methods for debugging
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10453 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
987f46dafc
StateValuesMTBDD: add static print(log, dd, model, description) method (useful for debugging)
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10452 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
5688846c0e
StateValuesMTBDD.print(log): does not throw PrismException
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10451 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
365f6559ec
JDDVars: add fromCubeSet() constructor and toCubeSet converter
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10450 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
e59d93a530
AcceptanceStreettDD: StreettPair -> StreettPairDD
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10449 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
8976cf9ace
set default file type for -exportpropaut
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10448 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
99e5420e4c
ProbModelChecker.clear(): deref complete var arrays, fix StateModelChecker constructor
Before, if varNum did not match the array length, some varDDRowVars/varDDColVars
would not be dereferenced.
Now, deref all variables in the arrays if they are non-null.
In the StateModelChecker constructor for the dummy model, we can now
pass the correct number of variables and a copy of the varDDRowVars array.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10447 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
572aaacb3a
StateModelChecker: use allDDRowVars.copy() instead of refAll
Plus reformatting
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10446 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
c92f73a141
JDDVars: derefAllArray
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10445 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
264ee2c080
prism-auto: revert previous commit, can not pass arguments to python when using env
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10444 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
a0f45900be
prism-auto: use -u switch to set stdout/stderr to unbuffered
As a side-effect, this sets stdout/stderr to 'binary', which might
make a difference on Windows...
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10442 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
b0a93691b6
..2MTBDD: from refAll to JDDVars.copyFrom()
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10441 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
9bb4d9b912
LTLModelChecker(product MDP): replace module var refAll with array copy, non-det vars with copy
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10440 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
5b29bd5433
LTLModelChecker(product MDP): replace second batch of refAlls with copies (for newAllDDVars)
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10439 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
f6536e356f
LTLModelChecker(product MDP): replace first batch of daDDVars refAll with copies
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10438 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
cfeece223f
LTLModelChecker(product MDP): simplify handling of daDDVarsCopy parameters
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10437 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
fbd2142654
LTLModelChecker(product DTMC): replace module var refAll with array copy
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10436 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
27e1c1e2eb
LTLModelChecker(product DTMC): replace second batch of refAlls with copies (for newAllDDVars)
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10435 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
c9c313e796
LTLModelChecker(product DTMC): replace first batch of daDDVars refAll with copies
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10434 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
249f45118c
LTLModelChecker(product DTMC): simplify handling of daDDVarsCopy parameters
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10433 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
d4887298d5
JDDVars: add 'static JDDVars[] copyArray(JDDVars[] vararray)'
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10431 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
795899dcd5
JDDVars: add methods 'JDDVars copy()' and 'void copyVarsFrom(JDDVars other)'
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10430 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
e4bf8aa21d
JDDVars: make JDDVars Iterable<JDDNode>
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10429 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
08b35e422a
JDDVars: add JavaDoc comments
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10428 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
5b05021d06
JDDVars: switch from Vector to Vector<JDDNode>
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10427 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
b4f94e36a5
Add method 'JDDNode JDDNode.copy()'
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10426 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Dave Parker
4050c50235
Support <<>> and [[]] operators for MDP (only * or empty), all engines.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10421 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Dave Parker
6afda907f6
Check <<>> operator for MDPs in explicit engine.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10420 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Dave Parker
a6003f8216
Allow <<>> operator for MDPs (but not checked properly yet).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10419 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Dave Parker
fa9b601faf
Update parser to allow proper <<>> or [[]] syntax.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10418 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Dave Parker
d07055efa6
Copy updated Coalition class from prism-games.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10417 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Dave Parker
f99bb9ebc2
Tidying GUI code.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10409 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago