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.
Previously, constants that are defined via an expression
were evaluated using standard (integer or floating point) arithmetic,
even in parametric or exact model checking mode.
This commit provides the infrastructure for requesting that constant
expressions are evaluated using exact arithmetic.
To keep the API backward compatible, we introduce additional methods that
offer an 'exact' flag, but keep the old methods as well. Those default to
normal arithmetic.
TypeDouble constants are kept as rational numbers, while int and boolean
constants are converted to Java data types. For int, an exception is raised
if the value can't be exactly represented by Java int.
Support matching of constants in RESULT strings for the case
that constants in the model are exact rational
numbers (implemented in subsequent commits).
This allows storage of BigRational values in StateValues / Values vectors, e.g.,
to store constants that have been evaluated exactly.
TypeDouble.castValueTo now returns a Number instead of a Double, requiring the use
of the doubleValue() method in several places where the value is evaluated using
double arithmetic.
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.
For numerical results, support e.g.
// RESULT: ~0.1244123
to indicate that the result is known to be imprecise.
For the exact engine, provide better error reports:
- If result is not exactly as expected, check if it's numerically close
- If the expected result is marked as imprecise, don't consider as an error
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.
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
Only filter(state, ...) has special handling for TypeVoid results (special
results such as e.g. pareto results from multi-objective model checking).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12034 bbc10eb1-c90d-0410-af57-cb519fbb1720
During reward construction in the explicit engine using the new ModelGenerator
functionality (see SVN 11772), the check for transition rewards was missing
(he explicit engine currently does not support transition rewards for DTMCs and CTMCs).
This commit adds functionality to ModelInfo to determine whether a reward structure
defines transition rewards and adds a corresponding check during reward construction.
Example: prism-examples/dice/dice.pm with R=?[ F s=7 ] and -explicit returns 0 instead
of an error message.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11802 bbc10eb1-c90d-0410-af57-cb519fbb1720
- Extended functionality available through the prism.Prism API when using ModelGenerators
- Improvements to ModelGenerator interface wrt handling of rewards (and also labels)
- Explicit engine model checkers now build rewards from a ModelGenerator, not a RewardStruct.
This is now (optionally) attached with the setModulesFileAndPropertiesFile method.
- New code to generate symbolic models from ModelGenerators (useful, if not super efficient)
- Move createVarList() method from ModelGenerator up to ModelInfo
- Some code tidying in LabelList
Code was previously at https://github.com/prismmodelchecker/prism-svn/tree/model-generator
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11772 bbc10eb1-c90d-0410-af57-cb519fbb1720
To be able to reference labels that are loaded from a .lab file and stored in the model,
they have to appear in the ModulesFile. This method stores
label "labelName" = false;
definitions. As the actual state set information is directly stored in the model,
evaluating the label will result in the correct state set.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11740 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
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
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
Steffen Märcker