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
Previously, model build failures skipped the tests and the corresponding
errors would not appear when running prism-auto in test mode.
Now, we just call doResultTest with the Result containing
the build exception for all the properties.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11637 bbc10eb1-c90d-0410-af57-cb519fbb1720
If-then-else expressions:
The if-expression can not refer to a parametric constant.
Other functions (min, max, floor, ...):
Arguments can not refer to parametric constants and evaluating
the function exactly has to be supported.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11615 bbc10eb1-c90d-0410-af57-cb519fbb1720
The recently added catch-all, last resort Exception handling clashes
with the nailgun exception that is used to signal a System.exit to
the nailgun process. So, we catch this kind of exception and re-throw it.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11603 bbc10eb1-c90d-0410-af57-cb519fbb1720
Normally, this should not matter, but in case closeDown is called multiple times
(e.g., due to some nailgun stuff), this should avoid multiple CUDD shutdowns,
which would probably lead to hard crashes.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11602 bbc10eb1-c90d-0410-af57-cb519fbb1720
constValues.getValueOf() throws an Exception if the constant value
does not exist. This may happen, e.g., for parametric model checking,
where the parametric constants will have no values.
So, we first check if the constant value exists. If this is not the
case then the RESULT line is clearly no match.
In the future, it might make sense to handle parametric constants
differently than non-existent constants, e.g., to provide a warning
for a nonsensical RESULT line in the latter case.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11601 bbc10eb1-c90d-0410-af57-cb519fbb1720
ParamModelChecker already has a mainLog by being a PrismComponent,
inheriting the log from the parent component.
In particular, this allows redirection of the log output via the
-mainlog parameter (as used by prism-auto).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11600 bbc10eb1-c90d-0410-af57-cb519fbb1720
PRISM recognizes the filename 'stdout' as special and exports
to standard output, so prepending a directory by prism-auto
does not make sense.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11592 bbc10eb1-c90d-0410-af57-cb519fbb1720
Instead of before, where only
// RESULT: integer
or
// RESULT: numerator/denominator
were allowed for result expressions, we now support arbitrary expressions
over the model/property parameters, e.g.,
// RESULT: 4.3*floor(q*3)
Caveat: Currently, there can be no whitespace in the expression...
Additionally, when model checking in exact mode, the expected value is
also computed using Expression.evaluateExact.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11557 bbc10eb1-c90d-0410-af57-cb519fbb1720
Dave Parker