As discussed in bug #2810797 the RodinDB doesn't save the name of an extended event for INITIALISATION events because it would be redundant information. Anyhow it is possible for a plug-in to set a refines clause for an INITIALISATION event which is extended. The RodinDB doesn't report an error/warning here.
How to reproduce:
Execute the following lines for an INITIALISATION event:
IRefinesEvent refinesEvent = rodinEvent.getRefinesClause(getNewName());
refinesEvent.create(null, monitor);
refinesEvent.setAbstractEventLabel("some_name", monitor);
Expected behaviour:
Error or warning marker on resource
Seen behaviour:
No problem reported
This is correctly reported by the static checker as a warning marker: "Initialisation must not refine explicitly".
Note: you need to save the machine and have the builder enable for the static checker to run.
Ah, sorry, my mistake... ;-)
Maybe the error message could be improved for the case when 'extends' is set.
'extends' doesn't change anything. The refinement is still there. Extension is just a decoration of the refinement relation.
No need to change the message.