Menu
▾
▴
#220 Model error not seen when building project
The following project contains a error which is not seen by the rodin platform after buiding the project.
In the model "m04_1" of the project one variable is missing. This variable has been added to the corresponding abstract model "m03_1" (its name is "mStopS").
Paul,
it is not an error to make a variable disappear in a refinement, as soon as the variable is not used anywhere in the refinement, except maybe in witnesses if need be (i.e., if the variable was assigned non deterministically in the abstraction).
This is actually the case in your model, so it is normal that no warning, error or unprovable PO is generated.
From a theoretical point of view, there is a notion of observable variable for which the theory ensures that it cannot disappear. However, this is not yet implemented in the current tooling. It will be implemented during the Deploy project at the same time as model decomposition.