456c7be353
ECComputerDefault: switch from numeric to graph-based computation of transitions remaining in an EC
Numeric computations (relying on sum of outgoing transitions > 1 - epsilon to detect choices that
remain in the EC) are not precise, better to just do a graph-based computation.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12028 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
3e80add2a4
symbolic ECComputer: provide helpers for graph-based computation of transititions staying in an EC
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12027 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
bf67bf7927
symbolic ECComputer: move findMaximalStableSet to ECComputer, make public
The provided functionality is useful as well when doing further
analysis on (M)ECs outside of the EC computations.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12026 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
9883fe5a1d
iv.cc: convert indexing from long to int64_t
Consistently use 64-bit index variables (to match size used for ODD offsets).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12025 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
d4bcc0db94
dv.cc: convert indexing from long to int64_t
Consistently use 64-bit index variables (to match size used for ODD offsets).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12024 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
958adc38ab
IntegerVector: Check that number of states fit into int
If the number of states is too large for the index of the vector to
fit into a Java int throw a PrismNotSupportedException.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12023 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
a7bbeb18ae
DoubleVector: Check that number of states fit into int
If the number of states is too large for the index of the vector to
fit into a Java int throw a PrismNotSupportedException.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12022 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
c246228a18
Hybrid engine: Error if number of reachable states is too large
Currently, the hybrid engine internally uses int (signed 32bit) index variables
So, if the number of states is larger than Integer.MAX_VALUE, there is a problem
and the code will most probably crash or do nonsensical things.
We check this before calling into the native hybrid engine code and
throw a PrismNotSupportedException.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12021 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
cc90e7a20c
Sparse engine: Error if number of reachable states is too large
Currently, the sparse engine internally uses int (signed 32bit) index variables
So, if the number of states is larger than Integer.MAX_VALUE, there is a problem
and the code will most probably crash or do nonsensical things.
We check this before calling into the native sparse engine code and
throw a PrismNotSupportedException.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12020 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
1d8f9fc6b9
ODD: Use int64_t for offsets everywhere, check for arithmetic overflow
Before, the ODD offsets (for indexing into the reachable states) were
stored as longs, resulting in inconsistent numbers of (symbolic)
states that can be treated. In particular, on Win64, long is 32bit.
We switch to int64_t for the ODD offsets everywhere, allowing
MTBDD computations for models with >2^31 states.
Additionally, we check for arithmetic overflow in the offset
computations. Due to the symbolic storage for the models and the
state space explosion, it's possible to construct simple model files
that reach the 2^63 states limit.
If this limit is reached, we now throw an error message. In the future
it might be worthwile to ensure that PRISM can deal with the absence
of an ODD for all the computations that don't absolutely require it
and carry on (most MTBDD engine algorithms should be fine).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12019 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
a8f26d2346
cudd, cpu_time.c: Include time.h for MINGW32 target
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12018 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
30a98ac4d0
Win64 cleanup, Makefile: remove -fpermissive flag
Not needed anymore, now that the pointer-to-integer casts are fixed.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12017 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
8c7311e417
Win64 cleanup: Backport CUDD 3.0.0 fixes for pointer-to-integer casts on Windows
As Windows 64bit uses IL32P64 data model (long is 32bit, pointers are
64bit), the various casts from pointer to long used in our version of CUDD
mangle the top-level half of pointers. On Java 8, the memory allocations
seem to generate benign pointers at first, but for larger symbolic models
this can lead to strange behaviour or crashes. For Java 9, crashes are more
immediate (https://github.com/prismmodelchecker/prism/issues/13 ).
The CUDD 3.0.0 release fixes those issues by using intptr_t and uintptr_t
for the pointer-to-integer casts. As we don't want to fully switch to 3.0.0
at the moment, this commit backports these fixes.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12016 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
79ea1d96a5
Makefile, cygwin64: Remove -fPIC
The mingw compiler issues warnings that the code is position-independent by default,
so we just drop the flag.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12015 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
732d224bd7
Win64 cleanup, sparse_adv.cc: avoid pointer-to-integer casts
Here, the casts are not needed, we can simply declare the correct pointer types.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12014 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
4c134da06d
Win64 cleanup, PS_NondetMulti*: avoid pointer-to-integer casts
Here, the casts are not needed, we can simply declare the correct pointer types.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12013 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
ce917c0248
dd_export.cc: format string %zu is not supported on Windows, use portable PRIuPTR
Windows needs %Iu for fprinting size_t / uintptr_t values, use the portable
format string macro available in C++11.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12012 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
57018c5d29
Windows: unbuffered stdout output
On Linux and OS X, we use line-buffered output for stdout.
Unfortunately, on Windows setvbuf with _IOLBF is ignored, instead
fully-buffered output is used, see
https://docs.microsoft.com/de-de/cpp/c-runtime-library/reference/setvbuf
So, we use unbuffered mode for stdout on Windows, as otherwise
long-running tasks can make it seem as if PRISM hangs.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12011 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
f21aa86be8
Makefile: C++ compiler flag --std=c++11
We would like to use C++11 features in the future, so tell the compiler
to use C++11.
The lpsolve library relies on the WIN32 macro definition to detect Windows
instead of the usual _WIN32. WIN32 seems not to be defined in mingw/gcc
when standard mode is active, so we define it ourselves.
http://nadeausoftware.com/articles/2012/01/c_c_tip_how_use_compiler_predefined_macros_detect_operating_system#WindowsCygwinnonPOSIXandMinGW
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12010 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
c38126a82e
Makefile: statically link pthread library for cygwin
In recent mingw g++ compilers from cygwin, the standard C++ library
depends on the pthreads library (libwinpthread-1.dll). As we'd like
for the prism DLLs to not depend on that library, we adapt the
linker flags to statically link the pthread library.
As we are not actually using any symbols, we also have to use the
--whole-archive flag to force linking.
https://stackoverflow.com/questions/13768515/how-to-do-static-linking-of-libwinpthread-1-dll-in-mingw/43402308#43402308
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12009 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
7f66e8b286
MTBDD Reachability computation: Gracefully handle CUDD out-of-memory
We check after each DD operation whether the returned DdNode* is NULL
and abort the computation. The NULL return value is then caught in the
JDD.ptrToNode() method, which raises a CuddOutOfMemoryException.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12008 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
453a96d80d
MTBDD Prob0/1 computations: Gracefully handle CUDD out-of-memory
We check after each DD operation whether the returned DdNode* is NULL
and abort the computation. The NULL return value is then caught in the
JDD.ptrToNode() method, which raises a CuddOutOfMemoryException.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12007 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
62f1e7d0ac
Prism.java: typo
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12006 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
7e8499dccf
prism.LTLModelChecker: comment typo
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12005 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
3dd1680c6e
prism-auto: count warnings / dd-warnings as well for statistic
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12004 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
c34d68046e
prism-auto: slight refactoring of colour printing
(1) use dedicated printColoured method, which suppresses
colouring if isColourEnabled() is false (e.g., when piping to a file)
(2) use dedicated colour (light red) for warnings, as before
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12003 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
c5eaee22f7
Auto-switch to explicit engine for non-probabilistic LTL model checking.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12002 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
c4ed300c01
Add state reward export for explicit engine; also some refactoring of reward exporting
(in particular, move logic for splitting into multiple reward files up to prism.Prism)
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12001 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
fe76535b3d
prism-auto: Add colour coding to summary table for passed/failed/etc. counts.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12000 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
a75ee46e89
FileSetting: Only create editor/render when needed, i.e., only from the GUI, not command-line.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11999 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
2261b32586
SamplerRewardReach: minor cleanup in constructor
Remove unnecessary check on valueKnown in constructor, seems
to be a copy-paste artifact.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11998 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
83e754e309
Multi-objective: convert some PrismException to PrismNotSupportedException
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11997 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
2221cb99d4
ExplicitFiles2MTBDD: fix missing JDDNode copy
When using the init label DD for the actual start state, need to copy.
Otherwise the ref count will be too low.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11996 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
5c21a80d68
prism-auto: print test statistics at the end if in test-mode
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11995 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
885ae560a7
explicit: Improve error message for unsupported multi-objective model checking
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11994 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
65dc304c17
Property.checkAgainstExpectedResultString: improve error message if there is an unexpected result type
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11993 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
a551301b5c
prism.ECComputerDefault: use JDD.isSingleton instead of GetNumMinterms to check for singleton state set
Using isSingleton should be more efficent.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11992 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
b2fbb25dd9
JDD.isSingleton: improve documentation (requires that the vars are ordered)
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11991 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
32404e1ab6
Bugfix: Model labels get exported twice when there is also a properties file due to recent ModelInfo refacetoring.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11984 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
d08a8d4c33
prism-auto fix: when checking output files in test mode, fail immediately when the first one is different.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11983 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
0ee323ea6a
explicit.MDPModelChecker: implement instantaneous reward computation (Rmax/min [I=x])
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11979 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
01a398bbc0
explicit.DTMCModelChecker.computeTotalRewards: use predecessor-relation-based computations for prob0
Previous behavior available via -noprerel switch.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11978 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
c7c8c8a7ff
explicit.DTMCModelChecker.computeReachRewards: use predecessor-relation-based computation for prob1
Previous behavior available using -noprerel switch.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11977 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
750923dfbf
(param/exact) fix handling of != in parametric/exact engine (with Linda Leuschner)
Missing case for NE operator in BoxRegion.cmpOp. This affects the check routines
for the != operator in the parametric/exact engines, e.g., for state formulas
such as s!=t
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11976 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
28b741819d
Optimise computation of expected instantaenous rewards (R[I=k]) for DTMCs when the value is only required for one state (explicit engine).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11975 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
b9a8cada88
Add DTMC transient probability computation for explicit engine.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11974 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
700a13f030
Refactoring in explicit CTMC model checker to reuse existing methods.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11973 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
751e95fa42
Small fix in prism-auto: make sure directory is passed to bench to benchmark function in "build" mode, in particular so that log names are created consisently. (Reported by Steffen Marcker).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11964 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
c0c584b589
add common.StopWatch for easily tracking computation times and printing to the PRISM log
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11952 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
cb812db4bf
symbolic: MDPQuotient transformation for computing the quotient MDP given an equivalence relation on the states
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11949 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Joachim Klein