If the ProbModelTransformationOperator does not modify the non-row / non-column
variables in the transformation of the transition function, it can also be used
for MDPs (modifying the successor state only depending on the originating state).
This can be useful in standard product transformations that are agnostic of
the non-deterministic choice.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11947 bbc10eb1-c90d-0410-af57-cb519fbb1720
By specifying a NondetModelTransformationOperator, we can easily transform
a given symbolic NondetModel (MDP) to a transformed model. The necessary
handling of the meta-information is done in NondetModelModel.getTransformed.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11946 bbc10eb1-c90d-0410-af57-cb519fbb1720
By specifying a ProbModelTransformationOperator, we can easily transform
a given symbolic ProbModel (DTMC/CTMC) to a transformed model. The necessary
handling of the meta-information is done in ProbModel.getTransformed.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11945 bbc10eb1-c90d-0410-af57-cb519fbb1720
The -ddextrastatevars setting allows to change the number of state variable pairs that are preallocated
before the actual model state variables. Previously, 20 state variable pairs were allocated for the
product construction (LTL). From now on, this is the default, but the amount can be changed, e.g., to
0 to force all automaton states to be allocated at the bottom of the MTBDD.
From now on, additionally, we also preallocate 20 action variables at the top of the MTBDD,
which will provide extra action / non-deterministic choice bits for symbolic model transformations
that require additional non-deterministic choices, e.g., additional special actions, etc.
The number of preallocated action variables is configurable by the -ddextraactionvars setting.
Adding the additional variables should not have a performance impact, as they are "don't cares"
in the normal MTBDD encoding of the models.
For the sparse and hybrid engine, allocating the nondeterministic choice variables at the top
makes sense for performance reasons (the submatrix for each choice is a sub-MTBDD), so we currently
only support extra action variables at the top.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11944 bbc10eb1-c90d-0410-af57-cb519fbb1720
The current behaviour for the -o2 (MTBDD) variable order (no
pre-allocation of state variables before the model variables) is there
since the initial support for LTL in PRISM. We need some benchmarks
to see if it's a good idea to use preallocation as for the -o1 order.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11943 bbc10eb1-c90d-0410-af57-cb519fbb1720
Sometimes, we have additional knowledge which states of the model
(apart from the initial states) are guaranteed to be reachable.
The added method then provides a way to start the reachability computation
with those states as the seed, which can speed up the computation as less
unknown states have to be discovered.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11938 bbc10eb1-c90d-0410-af57-cb519fbb1720
The previously used filecmp.cmp opens the files to be compared in 'rb'
mode, i.e., it will tell us that two files that differ only in the
line-ending encoding (CRLF vs LF) are not equivalent. However, we'd
like to get the export tests to succeed on Windows, regardless of the
line endings. So, we provide our own file comparison method that opens
the file in 'rU' mode (universal newline mode), which converts all the
newline encodings to '\n' transparently.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11880 bbc10eb1-c90d-0410-af57-cb519fbb1720
Somehow, PRISM can not open a NamedTemporaryFile created on Windows
(see issue prismmodelchecker/prism#11) when passed the filename via
the -mainlog parameter.
So, on Windows, we fall back on the old method of capturing stdout
directly via the Popen call. As this does not work with nailgun (the
C printfs go to the nailgun server stdout), we currently don't allow
nailgun use on Windows.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11879 bbc10eb1-c90d-0410-af57-cb519fbb1720
We want to strip trailing zeros (after the .) as well. This commit, together with the
previous one should provide the previous functionality, but fixing the issue with trailing
zeros for integers.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11860 bbc10eb1-c90d-0410-af57-cb519fbb1720
The regular expression for identifying the trailing .0* part of the string
did not require the . to actually occur, which would also strip the zeros from
integers ending with zeros.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11859 bbc10eb1-c90d-0410-af57-cb519fbb1720
These methods work for the case where the generic acceptance condition
has the required structure or can be easily padded to have the required
structure for Rabin / Streett.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11827 bbc10eb1-c90d-0410-af57-cb519fbb1720
Generally, as soon as clearBuiltModel is called, the models should not be
touched anymore. In doBuildModel, keep the null assignments for the
model storage variable for the unused engine.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11825 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
Joachim Klein