Skip to:

  1. Skip to Jira Navigation
  2. Skip to Side Navigation
  3. Skip to Main Content

Invarants occurr multiple times in the translated model

Description

Daniel, Jens,

Mir fällt auf, dass in der .eventb Übersetzung die gleiche Invariante auf vielen verschiedenen Ebenen auftritt.
Ich erinnere mich dunkel daran, dass wir dieses Problem schon einmal besprochen hatten.
Es ist nicht unbedingt sehr effizient wenn die gleiche Invariante mehrmals geprüft werden muss

Die Frage ist ob wir dies in der Übersetzung beheben, in bmachine_construction_eventb oder in b_ast_cleanup ?

Gruss,
Michael

Environment

None

Gliffy Diagrams

Activity

Show:

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

FAILURE: Integrated in

ProB_eclipse_develop_Rodin3 #13

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 AM
Edited

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.

Fixed

Details

Assignee

Reporter

Priority

More fields

Created February 10, 2014 at 9:43 AM
Updated March 18, 2014 at 7:27 AM
Resolved February 14, 2014 at 9:11 AM
Configure