To check that, for all parameter valuations in a region,
(1) some threshold property holds or (2) that a given
scheduler is optimal, a set of constraints is checked.
Currently, only heuristic checking is implemented, i.e., determining
via sampling if the constraints hold. This can produce false positives
in the region computations, i.e., a region is not sufficiently split.
We add a warning if the region computation relied on the heuristic
constraint check and thus can be imprecise.
In particular, align output format with other engines and treat exact mode
specially (print rational numbers instead of functions, approximate values)
For parametric, output results per region.
Print not only the state index, but also the variable valuations for that state
(similar to the other engines).
Example for exact:
prism prism-examples/dice/dice.pm -pf 'filter(print, P=?[ F d=1])' --exact
=== Previously ===
Results (non-zero only) for filter true:
([0.0,1.0])0:={ 1 | 6 }1:={ 1 | 3 }2:={ 0 }3:={ 2 | 3 }4:={ 0 }5:={ 0 }6:={ 0 }7:={ 1 }8:={ 0 }9:={ 0 }10:={ 0 }11:={ 0 }12:={ 0 }
==================
=== Now ==========
Results (non-zero only) for filter true:
0:(0,0)=1/6 (~0.16666666666666666)
1:(1,0)=1/3 (~0.33333333333333337)
3:(3,0)=2/3 (~0.6666666666666666)
7:(7,1)=1 (1.0)
==================
Example for parametric:
=== Previously ===
Results (non-zero only) for filter true:
([0.0,0.5])0:={ ( -1 ) p + 1 }1:={ 1 }2:={ 0 }([0.5,1.0])0:={ p }1:={ 1 }2:={ 0 }
==================
=== Now ==========
Results (non-zero only) for filter true:
([0.0,0.5]):
0:(0)={ ( -1 ) p + 1 }
1:(1)={ 1 }
([0.5,1.0]):
0:(0)={ p }
1:(1)={ 1 }
==================
To ensure that the policy iteration (performed on an MDP where parameters have been replaced
by a parameter valuation) converges and converges on the right result in the presence of
zero-reward end components, we initialise the policy iteration for Rmin[F] with a
proper scheduler, i.e., that reaches the goal with probability one (see [BertsekasTsitsiklis91]).
Together with the previous commit, this fixes#4 and #15.
In the state eliminator, i.e., solving for a DTMC, a state that has probability
zero of reaching the target states (i.e., that can not reach the target state)
should get infinite reward.
Previously, the check for this looked at the returned set of collectStatesBackward(),
which always returns the whole state space (used for backward elimination order).
Now, we use the variant of collectStatesBackward() that only returns the states
that can reach the target set.
Additionally, we now compute the set of infinity states for Rmin/Rmax using
prob0a / prob0e, respectively, and ensure that they get value infinity.
As well, remove getNumTotalChoices() in favour of the getNumChoices() method
as used in the explicit models.
This will allow using the explicit model checkers prob0/prob1 methods.
Sometimes, we want to use the prob0/1... methods to generate schedulers instead of doing
the standard precomputations and don't want to have the normal log output.
Not inherited using inheritSettings()
In Java 9, there is a new system class java.lang.Module that is implicitly imported
everywhere and which clashes with the parser.ast.Module class, resulting in
compilation errors, as javac is not able to disambiguate between the two
automatically.
We are therefore more specific when referencing the PRISM parser's 'Module' class,
by using the full 'parser.ast.Module' name.
Switching between max and min when removing the negation was missing for MDPs.
Test case:
prism functionality/verify/mdps/ltl/simple_ltl.nm functionality/verify/mdps/ltl/simple_ltl.nm.props -exact -prop 3
from prism-tests.
Sometimes, if the prism-auto scripts gets interrupted, an existing
nailgun server is not properly shut down and might break a subsequent
prism-auto run.
When using an iteration method with two alternating solution vectors (power, jacobi),
we did not copy the result to the second vector when we have detected convergence in
an SCC (for topological interval iteration). Subsequently, as the values for finished
SCCs will never be updated anymore, the values for this states will oscillate between
the final value and the value from the iteration step before, potentially preventing
convergence. This will be mitigated if we enfore convergence from below / above, but
at least from below enforcing convergence should not be necessary.
An example would be
prism prism-examples/dice/two_dice.nm -pf 'Rmin=?[ F s1=7]' -explicit -topological -ii:nomonotonicbelow
where oscillation between 0 and 1 inhibits convergence.
To fix, we tell the iteration method when we are done with an SCC so that we can
copy the results. For singleton SCCs, we already copied the results to both vectors.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12204 bbc10eb1-c90d-0410-af57-cb519fbb1720
For CTMCs, only the state rewards, but not the transition rewards
are scaled by the rates.
Failing tests e.g.
functionality/verify/ctmcs/rewards/ctmc_rewards.sm
(14) R{"a"}=? [ F s=1 ]
from functionality/verify/ctmcs/rewards/ctmc_rewards.sm.props
in the test suite with --exact mode
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12203 bbc10eb1-c90d-0410-af57-cb519fbb1720
Currently, building PRISM with parallel building does not work,
as there are dependencies between targets that are not fully
encoded in the Makefiles. Building with -j n flag would lead to error.
Now, we add the .NOTPARALLEL target to most of the Makefiles,
which tell GNU make to ignore the -j flag. Note that this
only inhibits parallel builds for the current Makefile, we
thus have to specify it for all sub-Makefiles as well
(see https://www.gnu.org/software/make/manual/html_node/Parallel.html)
For the external libraries, CUDD and LPSolve don't seem to mind building
in parallel, so we don't inhibit there and can get some minor compile time
speed-up by using multiple cores if the -j option is specified.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12202 bbc10eb1-c90d-0410-af57-cb519fbb1720
Consistently include cstdio instead of stdio.h, etc. For MinGW,
the default underlying stdio implementation (Microsoft DLL based vs
POSIX MinGW implementation) differs between C++ and C code, so
format string warnings pop up if we include the C header...
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12192 bbc10eb1-c90d-0410-af57-cb519fbb1720
There is currently no portable format string argument for std::size_t,
so we simply convert to a string via std::to_string() ourselves.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12191 bbc10eb1-c90d-0410-af57-cb519fbb1720
On Win32, jints are actually long ints, so printf would need %ld instead of %d.
As jints are 32bit, we simply cast to an int to silence format string compiler
warning.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12190 bbc10eb1-c90d-0410-af57-cb519fbb1720
Joachim Klein