rethink bounds check design
This information is written here because here it would be available to anyone wanting to change the specification of bounds check.
We use NuSMV to check the bounds. Outputs of a component map to “DEFINE”
in NuSMV which is just a name for an expression, i.e., it is not a
variable. This “DEFINE” can not be used in a property
specification because of language limitations in NuSMV.
So, as a result we generate the following specification for each
transition t:
“actions in t do not violate the bound”
This approach generates too many specifications but there is no other way out.
(from redmine: issue id 3411, created on 2018-05-17)
- Relations:
- relates #3024 (closed)
- relates #3412 (closed)