There is no explicit model type keyword added to the parser.
Instead, LTSs are auto-detected by the absence of probabilities.
ConstructModel is extended to build LTSs. Model checking (CTL+LTL)
can be done out of the box using the existing NonProbModelChecker class.
A few MDP regression tests are clarified to make it clear that the
models are MDPs, not LTSs.
Both types of engine now disallow negative/infinite/NaN rewards.
Symbolic engines will mostly still not detect the presence of NaN
due to the way that CUDD deals with this.
Regression tests also added.
Code is split into different methods for each type of test.
It is also mostly relocated to a new class prism.ResultTesting,
since it should not really be tied to the Property object.
The result for testing can now be passed as a Result object,
as well as Double, Integer, etc., with the former being preferred.
This will allow info attached to the Result object to be used
for the correctness, notably accuracy/error info.
Also add a new testing regression test - just some constants,
including border cases - infinity, NaN, etc.
Was previously being parsed as a PRISM expression as a fallback,
but the parser currently does not handle big integers.
Test case added. And these tests moved to a new "testing" directory.
The statesOfInterest variables was wrongly not reset to 'reach'.
Not usually caught because the statesOfInterest optimisation is
currently used in very few places. The attached bugfix test shows
an example of where it does go wrong.
This uses a new type of ExpressionFilter with op type "store",
rather than setting a boolean flag on existing filter objects.
Includes two test-cases showing examples where the old code failed.
This cleans up and refactors the iteration over state variable
valuation/value pairs via StateValues. In particular StateValuesMTBDD
learns how to do non-sparse printing.
Furthermore, it
* introduces generic "iterate" and "iterateFiltered"
methods for iterating over the state/values, calling a
StateAndValueConsumer object
* provides a StateAndValueConsumer implementation (StateAndValuePrinter)
that supports printing in the various output styles supported by PRISM
* cleans up the convenience "print" method using default methods in StateValues
* activates the MTBDD engine for one -exportvector based test
Note: Previously, in the StateValuesMTBDD iteration steps, the int[]
array with the current values represented the increments to be added
to the low values of state variables, with the addition
value = low + a[i]
happening on output. Now, we initialise the array with low, i.e.,
the values in the array correspond to the actual variable values.
Exports the value of a model checked property for all states as a vector.
If <file> is "stdout", this is displayed to the log instead of a file.
Currently, only works for a single property: if there is more than one,
then the file gets overwritten each time a property is checked.
Also fixes a bug in the underlying mechanism for storing results vectors
in the explicit engine (within Results objects).
When converting an MTBDD to an integer vector (as is done to prepare the storage for the computed strategy for Pmax-Until using the sparse engine), the MTBDD has to be zero for non-reachable states, as that could lead to out-of-bounds writes to the array during conversion.
This commit adds the required restriction to reach in prism.NondetModelChecker.
+ test case
+ fixes deref of 'yes' during initialization
When DOT graphs of a model are exported, their maximum permitted size is
hardcoded to 8 inches wide by 5 inches high, which is too small for the
rendered drawing to be useful (e.g. during debugging) for all but the
simplest of models. Remove the maximum size restriction, allowing tools
to render the drawing with its natural dimensions.
'testsfull' runs the test cases from prism-tests against all the
different engines (explicit, hybrid, sparse, mtbdd, exact), with and
without interval iteration and topological ordering, where appropriate.
Tweak the result strings for the CTL with step bounds cases (currently
computation is not supported with any engine). Previously, an error was
expected, but the properties are not actually erroneous. Additonally, the
error message was not uniform between the different engines, leading to
spurious failures against the exact engine.
Some of the result values for the test cases were floating-point approximations,
which results in 'close but inaccurate' errors when running the test cases against
the exact engine.
We replace those results either with the exact values or mark the approximated
results with ~... (mostly for a few CTMC properties, where the exact results
are a bit unwieldly).
During model exploration of a CTMC, when using fast adaptive uniformisation,
only the last part of an update (rate & successor state) is used, as the
indexing of the outgoing transitions is buggy.
We now store all outgoing transitions and handle the case of multiple
choices/enabled commands in the CTMC.
+ two test cases
Expressions are now evaluated exactly in parametric / exact model checking mode for:
- state updates
- command guards
- the if part of if-then-else expressions
- reward guards
- reward values
- Boolean expressions in RESULTS in property files
Add various test cases to check that it is now handled properly.
Using the infrastructure from the previous commit, we request exact evaluation
of constants in exact and parametric model checking mode.
Additionally, note where we deliberately choose non-exact evaluation mode.
Add corresponding test cases.
The action object attached to a transition can be null (internal action), leading to a null pointer
exception when trying to call the toString method.
+ test case
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.
Dave Parker