Menu
▾
▴
#236 "Inherited" overwrites "convergent".
I just figured out the following unexpected behavior.
Maybe it has already been fixed in V0.9.
1. I define an event "foo" in the abstract model. "foo" is anticipated.
2. I refine the abstract model.
3. I select "true" (= inherited) and "convergent" in the concrete version of "foo". I also declare a variant.
4. From the generated POs, I derive that the concrete version of "foo" is still anticipated.
I would expect that "inherited" only affects parameters, guards, and actions, but not the "convergence value".
By the way: what happens if the abstract event has a witness, and the concrete event is inherited. Will the witness be copied?
In 0.9.x, "inherited" has been replaced by "extended". An extended event inherits parameters, guards and actions from its abstraction event, and nothing else. In particular, the convergence of the concrete event is declared locally in the concrete event and not inherited from its abstraction.
I've checked that your example does produce the expected proof obligations with the latest release from CVS.