For the non-fair case, the restriction is indeed done
by the ECComputer, but for the fair case, the restriction
of candidateStates to states_Li_not is required.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11243 bbc10eb1-c90d-0410-af57-cb519fbb1720
Parsing a HOA automaton, if a state has an acceptance signature that
contains an acceptance set that is not actually referenced in the
acceptance condition, we simply skip these entries, as they are not
relevant for acceptance.
This commit fixes the handling for this situation:
Acceptance: 2 Inf(0)
...
State: 1 {1}
I.e., when the acceptance set index is valid but larger than the
largest used one. Previously, would throw an IndexOutOfBoundsException
trying to access a non-existant set.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11218 bbc10eb1-c90d-0410-af57-cb519fbb1720
The compilation wrapper 'ccc' of lpsolve tries to determine
whether the isnan macro is defined. The test program calls
isnan(0), i.e., with an integer argument. On current Arch Linux,
GCC uses _builtin_isnan, which leads to an error due to the integer
argument and the 'ccc' wrapper assumes that isnan is not defined.
This leads to compilation issues later on.
The fix replaces the isnan(0) test call with isnan(0.0).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11216 bbc10eb1-c90d-0410-af57-cb519fbb1720
When translating the module state variables to locations, probabilities in
commands were not translated. If the probability expression contains a reference
to the state variables, e.g.,
(s=0 ? 0.5 : 0.75)
then the variable reference persists, which leads to an exception when
updating variable information of the module later on, as the state variable
is no longer defined in the translated module.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11215 bbc10eb1-c90d-0410-af57-cb519fbb1720
Add handling for ExpressionITE to Simplify.
Incidentally, this fixes a bug in PTA handling, where guards with an
ITE operation where not properly simplified and thus unsupported, e.g.,
s=0 ? true : false
as guard.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11214 bbc10eb1-c90d-0410-af57-cb519fbb1720
The routines in LTL2RabinLibrary for generating DA for
simple path formulas with time bounds have been adapted
to deal with negated labels. This makes the special
preprocessing for such formulas unnecessary and we remove it.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11199 bbc10eb1-c90d-0410-af57-cb519fbb1720
Without formula simplifications, jltl2ba will produce an APSet L0, L1, ...
With formula simplifications (upcoming commit), some APs can be missing
in the NBA (when irrelevant) or reordered (due to formula simplification).
We handle edge label construction as elsewhere in PRISM for DA, to take
this into account.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11186 bbc10eb1-c90d-0410-af57-cb519fbb1720
This is currently caught elsewhere as well, but provides defense-in-depth
for the situation that time bounds in LTL are supported later on.
Bounds on temporal operators don't have the same semantics in CTMCs
as for discrete-time models.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11178 bbc10eb1-c90d-0410-af57-cb519fbb1720
If the expected result specified via // RESULT
is an error, we treat a PrismNotSupportedException just
as any other ordinary exception. This allows verifying
the content of a PrismNotSupportedException error message.
Otherwise, we do the usual special handling as before.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11173 bbc10eb1-c90d-0410-af57-cb519fbb1720
There's actually JDK library functionality for a hash map that
uses object identity instead of .equals(), making PlainObjectReference
unnecessary. Use IdentityHashMap instead.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11169 bbc10eb1-c90d-0410-af57-cb519fbb1720
Previously, subformulas were computed by a DTMCModelChecker
in the embedded DTMC, yielding wrong results. Now, maximal
state subformulas are checked via the CTMCModelChecker and
replaced by labels before calling the LTL model checking
routine on the embedded DTMC.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11168 bbc10eb1-c90d-0410-af57-cb519fbb1720
The labels encode the satisfaction sets of the subformulas. This method can be
used to do the standard PCTL* recursion step, i.e., computing Sat(phi) and replacing
phi with an atomic proposition a_phi in the formula.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11167 bbc10eb1-c90d-0410-af57-cb519fbb1720
When building a model from the GUI with the explicit engine, constant were sometimes not
updated correctly:
(1) Open xprism, switch to explicit engine
(2) Load a model with undefined constants, e.g., brp.pm
(3) Build the model, setting constants (e.g., 2 and 3)
(4) Build the model again, setting *other* constants (e.g., 22 and 3)
In step (4), the log file reflects the changed constants,
but the generated model has the same number of states as
in step (3) and is fact built with the constants of step (3).
The cause:
If the PRISM file is not reloaded, then the currentModelGenerator
remains the same. In ModulesFileModelGenerator.initialise(), called
from setSomeUndefinedConstants() in step (3), the modulesFile is
overwritten with the modulesFile where the constants set in step (3)
have been replaced in the AST with the concrete values.
In step (4), there are no more AST-elements with undefined constants
and hence the modules file does not reflect the changed constants when
the constants in the constant list are changed.
The fix is to keep a copy of the original modules file in the
ModulesFileModelGenerator which is freshly deepCopyied and
processed in the subsequent calls to initialise().
Regression introduced in SVN r10996 when switching to the
ModulesFileModelGenerator infrastructure.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11159 bbc10eb1-c90d-0410-af57-cb519fbb1720
Joachim Klein