The parametric engine works under the assumption that models
are well-defined, i.e., that parameter valuations will lead
to graph-preserving probabilities, etc.
If we encounter a point in a region where these assumptions
don't hold, we now treat this by splitting the region. Regions
with such an improper midpoint that are below the precision
threshold are considered to be undefined and further processing
is aborted.
In particular, this treatment ensures that we never perform
policy iteration on a model with parameter instantiation
that is not well defined / supported. E.g., if there
were negative rewards for such a point, policy iteration
would previously not necessarily terminate.
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.
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.
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
This commit refactors the exportToDotFile infrastructure of
the explicit engine to allow the flexible decoration of the
nodes and edges in the DOT file, e.g., for annotating rewards,
marking certain states, etc.
We provide default implementations in explicit.Model for most methods,
only exportTransitionsToDotFile needs to be provided in derived classes
to allow DOT export.
Note that the abstract method in ModelExplicit
abstract void exportTransitionsToDotFile(int i, PrismLog out);
has been removed, which will lead to errors in derived classes
where implementations of this method have been marked with the
@Override annotation.
To fix this, simply replace the signature of your implementation of
void exportTransitionsToDotFile(int i, PrismLog out);
by
void exportTransitionsToDotFile(int i, PrismLog out, Iterable<explicit.graphviz.Decorator> decorators)
(as defined in explicit.Model). You can simply ignore the decorators
parameter at first. Later on, if you want to support decoration,
have a look at the implementations of this method in DTMCExplicit
and MDPExplicit for the proper handling.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12115 bbc10eb1-c90d-0410-af57-cb519fbb1720
The getSuccessorsIterator provides an iterator over the set of successors,
i.e., deduplication is sometimes required (e.g. for MDPs).
We introduce here a SuccessorsIterator class that allows to make deduplication
optional, which may have benefits in performance. Additionally, SuccessorsIterator
implements a primitive OfInt iterator, which can avoid auto-boxing.
Subclasses of explicit.Model now have to provide an implementation for getSuccessors(int s),
getSuccessorsIterator(int s) is provided via a default method that automatically
requests deduplication.
Subclasses of explicit.NondetModel now have to provide an implementation for getSuccessors(int s, int).,
getSuccessorsIterator(int s, int i) is provided via a default method that automatically
requests deduplication.
Adapt the existing subclasses of explicit.Model.
Provides additional default methods and removes unneeded specializations in sub-classes:
boolean isSuccessor(int s1, int s2)
boolean allSuccessorsInSet(int s, BitSet set)
boolean someSuccessorsInSet(int s, BitSet set)
boolean allSuccessorsMatch(int s, IntPredicate p)
boolean someSuccessorsMatch(int s, IntPredicate p)
and for NondetModel:
boolean allSuccessorsInSet(int s, int i, BitSet set)
boolean someSuccessorsInSet(int s, int i, BitSet set)
boolean allSuccessorsMatch(int s, int i, IntPredicate p)
boolean someSuccessorsMatch(int s, int i, IntPredicate p)
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12085 bbc10eb1-c90d-0410-af57-cb519fbb1720
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
The transitions are explored twice during model construction, once
to find the reachable states and the second time to actually build
the transition structure of the model. We suppress the warning
in the first pass so that it does not appear twice.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11656 bbc10eb1-c90d-0410-af57-cb519fbb1720
Already convert the expression to a function for ChoiceListFlexi,
as this will allow filtering zero probability updates (next commit)
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11653 bbc10eb1-c90d-0410-af57-cb519fbb1720
If we can can not guarantee that the probabilties for a command sum to 1 in a DTMC or
MDP then we report an error. This is similar to what happens for the explicit and
symbolic engines and fixes issue prismmodelchecker/prism#6.
This error check can be switched off using the -noprobchecks option.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11644 bbc10eb1-c90d-0410-af57-cb519fbb1720
We wrap the RegionValues returned by ParamModelChecker in a ParamResult
object, which stores additional meta-information that allow for the
result to be tested.
In test mode, if there is only a single region, tests against the given
expected RESULT expression.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11639 bbc10eb1-c90d-0410-af57-cb519fbb1720
Joachim Klein