Invarants occurr multiple times in the translated model
Description
Environment
relates to
Gliffy Diagrams
Activity

Jenkins Build Server March 18, 2014 at 7:27 AM
FAILURE: Integrated in

Jenkins Build Server February 11, 2014 at 5:10 PM
SUCCESS: Integrated in
ProB_eclipse_develop #1337
PROBPLUGIN-97: Fixed code to check whether an invariant is defined in the current machine or an abstract one. (plagge: rev 110417081c7a97ffec1e074fbbc8000b32da3026)
de.prob.core/src/de/prob/eventb/translator/internal/ModelTranslator.java

Jens Bendisposto February 11, 2014 at 7:28 AMEdited
Yes, but we should check that it works. I've added a ticket

Daniel Plagge February 10, 2014 at 1:31 PM
@Jens: Is it possible that the bug does not affect ProB2, because ProB2 works directly on the bare Rodin files?

Daniel Plagge February 10, 2014 at 1:30 PM
Fixed the bug: To check whether an invariant has been defined in an abstract machine, the translation iterated through all abstract machines and checked if the source of the predicate was equal to one of them. The problem was (I assume) that the list of abstract machines has at most one entry. Thus if M2 refines M1 and M3 refines M2, the list of abstract machines of M3 is [M2], not [M1,M2].
Now we just determine the name of the current machine and check if the name of the predicate's source is equal to that.
Details
Details
Assignee

Reporter
