The formula may have bounds attached to the temporal operators, so we
strive to preserve them.
Dualizing the operators does not change the bounds, so we can just
attach them (see ExpressionTemporal.convertToUntilForm()) to the new
temporal operator.
It looks like the value of col_offset is never actually used
during the recursion steps. For the moment, we just initialise with 0
(can not be worse than starting with uninitialised value) and mark
as candidate for refactoring after thorough inspections of
the various code paths.
(via linting)
In test mode, we'd like to have proper 'not supported' handling during the tests,
so we don't exit immediately when encountering an engine / iteration method that
is incompatible, as that would count as a failure.
Due to a typo, the upper iteration uses `updateValueFromBelow` instead of `updateValueFromAbove`
to update the value vector. When the flag for monotonicity enforcement from above is active (default),
all values are thus forced to be above the upper bound, preventing convergence.
Example:
prism functionality/verify/mdps/reach/mdp_simple.nm functionality/verify/mdps/reach/mdp_simple.nm.props -sparse -intervaliter
+ test case
Previously, a transition reward with [] would match the self loop
transition added for fixing deadlocks in the explicit engine.
Fixes#29 and adds test case.
If we are solving the transposed equation system, the solution vector
is over the column vars, not the row vars. This has to be taken into
account when exporting the iterations using -exportiterations.
install.sh attempts to replace PRISM_DIR=... with the actual PRISM directory
in the startup scripts contained in bin/ using a call to sed.
On MacOS, the system sed fails with 'RE error: illegal byte sequence' for binary
files, such as the .DS_Store files created by the Finder.
So, we exclude all files starting with a dot (.*) as well. Additionally,
we use `-iname` instead of `-name` in the find command for the matches
against '*.bat' and 'ngprism' to match insensitive to the case of the filename.
[adapted by @kleinj from PR #59]
In attachLabels(), avoid unnecessarily exploring the state space again
when the ModelGenerator indicates that labels aren't used (i.e. when
getNumLabels() == 0).
As noted in #48, DTMCUniformisedSimple does not implement the full range of ModelExplicit methods. Trying to use it outside of the areas where it's currently used in PRISM can then lead to NullPointerExceptions etc.
We add here accessors for the deadlock states, passing through the method calls to the underlying CTMC.
Additionally, point to the fully-featured uniformised DTMC object / construction method.
The location of the PRISM configuration file is now OS-dependent. On UNIX-like systems, following the XDG base directory specification, it is prism.settings in ~/.config (or in $XDG_CONFIG_HOME if that overrides it). On OS X, it is prism.settings in ~/Library/Preferences. On anything else it remains in ~/.prism.
If an existing configuration file exists in ~/.prism, that file is still used regardless of the OS.
Closes#38.
Joachim Klein