[Analyses] ASSIGN construct can not deduce viability of assignments
NuSMV files contain ASSIGN blocks of the form “next(var) = case
_next_t = t1 : var = dvar_t;”. If var is of a range type, NuSMV cant
properly decide bound violations as it can not deduce the Invariants and
Guard constraints for the transition.
My guess is, this happens because the bound-checking is something rather
spartanical that was never supposed to regard the kinds of dependencies
we are using. The bound-checking seems to be a separate step before
integrating the assign statement into the transition predicate; since
the invalid actions which would be forced by an assign block, once
translated to a Trans constraint, would simply not be regarded as they
would lead into an invalid state.
Solution 1: use TRANS constraint to encode the actions instead of ASSIGN
blocks.
This guarantees that NuSMV will not fail because of wrongly resolved
bounds. The downside: NuSMV will just not take any bound-violating
transitions even though the model could specify them but that would
require an unchecked model which is forbidden.
Solution 2: add Guard-Expressions to the ASSIGN conditions.
This would rely on the guard-expressions to be sufficiently expressive
for NuSMV to check the bounds. Unresolvable problems could be reported
back to the user who would have to refine the guard. Though this is a
more Contract focused approach, it would probably clutter the guard as
well as the generated NuSMV code. Also, we would probably have to
introduce a whole structure of State-invariances to prove more complex
bound violations do not appear (e.g. replace v1 < 4 with v1 < 200
in solution2.smv, model is ok but NuSMV is complaining)
(from redmine: issue id 2716, created on 2016-10-14, closed on 2016-11-07)
- Uploads: