Skip to content
Snippets Groups Projects
Commit 6d331493 authored by Michael Leuschel's avatar Michael Leuschel
Browse files

support invariants whose source is not a machine


e.g., generated by plugins

Signed-off-by: default avatarMichael Leuschel <leuschel@uni-duesseldorf.de>
parent 2b3184da
Branches
No related tags found
No related merge requests found
Pipeline #157490 passed
...@@ -609,8 +609,10 @@ public class ModelTranslator extends AbstractComponentTranslator { ...@@ -609,8 +609,10 @@ public class ModelTranslator extends AbstractComponentTranslator {
final String srcName = src.getRodinFile().getBareName(); final String srcName = src.getRodinFile().getBareName();
result = currentName.equals(srcName); result = currentName.equals(srcName);
} else { } else {
throw new TranslationFailedException("Machine " + currentName, // Some plugins virtually add new invariants (e.g., FOLLOWED_BY for events)
"Source of invariant is not a machine"); Logger.notifyUser("Source of invariant in " + currentName + " is not a machine. Invariant may be added multiple times.");
// TODO: check if this source is local or not
result = false; // assume it is local so that it is added in the translation
} }
return result; return result;
} }
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment