From 2cf040f9240143a29b3f55ce415dc0ffb2f3cd94 Mon Sep 17 00:00:00 2001
From: Ludovic Apvrille <ludovic.apvrille@telecom-paris.fr>
Date: Tue, 23 Apr 2024 17:29:48 +0200
Subject: [PATCH] Adding check for signal use in Avatar
---
.../java/avatartranslator/AvatarBlock.java | 86 +++++----
.../java/avatartranslator/AvatarError.java | 13 +-
.../java/avatartranslator/AvatarSignal.java | 7 +
.../avatartranslator/AvatarSpecification.java | 16 ++
.../avatartranslator/AvatarStateMachine.java | 11 ++
.../avatartranslator/AvatarSyntaxChecker.java | 179 ++++++++++++++++++
src/main/java/ui/TAttribute.java | 3 +-
7 files changed, 275 insertions(+), 40 deletions(-)
diff --git a/src/main/java/avatartranslator/AvatarBlock.java b/src/main/java/avatartranslator/AvatarBlock.java
index 92bed46d2d..4409415bd4 100644
--- a/src/main/java/avatartranslator/AvatarBlock.java
+++ b/src/main/java/avatartranslator/AvatarBlock.java
@@ -607,49 +607,63 @@ public class AvatarBlock extends AvatarElement implements AvatarStateMachineOwne
// Add new timer signals
+ int nbOfTimers = 0;
for (AvatarAttribute aa : attributes) {
if (aa.getType() == AvatarType.TIMER) {
- name = findUniqueSignalName("set_" + aa.getName());
- asSet = new AvatarSignal(name, AvatarSignal.OUT, aa.getReferenceObject());
- value = new AvatarAttribute("timerValue", AvatarType.INTEGER, this, aa.getReferenceObject());
- asSet.addParameter(value);
- addSignal(asSet);
- sets.put(aa.getName(), asSet);
- name = findUniqueSignalName("reset_" + aa.getName());
- asReset = new AvatarSignal(name, AvatarSignal.OUT, aa.getReferenceObject());
- addSignal(asReset);
- resets.put(aa.getName(), asReset);
- name = findUniqueSignalName("expire_" + aa.getName());
- asExpire = new AvatarSignal(name, AvatarSignal.IN, aa.getReferenceObject());
- addSignal(asExpire);
- expires.put(aa.getName(), asExpire);
-
- // Create a timer block, and connect signals
- String blockName = "Timer_" + aa.getName() + "_" + getName();
- while (_spec.getBlockWithName(blockName) != null) {
- blockName += "0";
+
+ // Check if timer is really used
+ boolean toBeRemoved = false;
+ if (asm != null) {
+ toBeRemoved = asm.hasTimeoperatorWithAttribute(aa);
+ }
+
+ if (toBeRemoved) {
+ nbOfTimers ++;
+
+ name = findUniqueSignalName("set_" + aa.getName());
+ asSet = new AvatarSignal(name, AvatarSignal.OUT, aa.getReferenceObject());
+ value = new AvatarAttribute("timerValue", AvatarType.INTEGER, this, aa.getReferenceObject());
+ asSet.addParameter(value);
+ addSignal(asSet);
+ sets.put(aa.getName(), asSet);
+ name = findUniqueSignalName("reset_" + aa.getName());
+ asReset = new AvatarSignal(name, AvatarSignal.OUT, aa.getReferenceObject());
+ addSignal(asReset);
+ resets.put(aa.getName(), asReset);
+ name = findUniqueSignalName("expire_" + aa.getName());
+ asExpire = new AvatarSignal(name, AvatarSignal.IN, aa.getReferenceObject());
+ addSignal(asExpire);
+ expires.put(aa.getName(), asExpire);
+
+ // Create a timer block, and connect signals
+ String blockName = "Timer_" + aa.getName() + "_" + getName();
+ while (_spec.getBlockWithName(blockName) != null) {
+ blockName += "0";
+ }
+ AvatarBlock ab = AvatarBlockTemplate.getTimerBlock(blockName, _spec, getReferenceObject(), null, null, null);
+ _addedBlocks.add(ab);
+
+ AvatarRelation ar;
+ ar = new AvatarRelation("timerRelation", this, ab, getReferenceObject());
+ ar.addSignals(getAvatarSignalWithName(asSet.getSignalName()), ab.getAvatarSignalWithName("set"));
+ ar.addSignals(getAvatarSignalWithName(asReset.getSignalName()), ab.getAvatarSignalWithName("reset"));
+ ar.addSignals(getAvatarSignalWithName(asExpire.getSignalName()), ab.getAvatarSignalWithName("expire"));
+ _spec.addRelation(ar);
}
- AvatarBlock ab = AvatarBlockTemplate.getTimerBlock(blockName, _spec, getReferenceObject(), null, null, null);
- _addedBlocks.add(ab);
-
- AvatarRelation ar;
- ar = new AvatarRelation("timerRelation", this, ab, getReferenceObject());
- ar.addSignals(getAvatarSignalWithName(asSet.getSignalName()), ab.getAvatarSignalWithName("set"));
- ar.addSignals(getAvatarSignalWithName(asReset.getSignalName()), ab.getAvatarSignalWithName("reset"));
- ar.addSignals(getAvatarSignalWithName(asExpire.getSignalName()), ab.getAvatarSignalWithName("expire"));
- _spec.addRelation(ar);
}
}
- name = findUniqueAttributeName("timerValue_");
- value = new AvatarAttribute(name, AvatarType.INTEGER, this, getReferenceObject());
- addAttribute(value);
+ if(nbOfTimers > 0) {
+ name = findUniqueAttributeName("timerValue_");
+ value = new AvatarAttribute(name, AvatarType.INTEGER, this, getReferenceObject());
+ addAttribute(value);
- // Modify the state machine
- if (asm.removeTimers(name, sets, resets, expires)) {
- // Add an attribute for the timer value
- //value = new AvatarAttribute("__timerValue", AvatarType.INTEGER, this, getReferenceObject());
- //addAttribute(value);
+ // Modify the state machine
+ if (asm.removeTimers(name, sets, resets, expires)) {
+ // Add an attribute for the timer value
+ //value = new AvatarAttribute("__timerValue", AvatarType.INTEGER, this, getReferenceObject());
+ //addAttribute(value);
+ }
}
// Remove Timer attribute
diff --git a/src/main/java/avatartranslator/AvatarError.java b/src/main/java/avatartranslator/AvatarError.java
index 9ef6d0e2ff..c4cc8d85a5 100644
--- a/src/main/java/avatartranslator/AvatarError.java
+++ b/src/main/java/avatartranslator/AvatarError.java
@@ -54,15 +54,22 @@ public class AvatarError {
"Signals are connected but there are not compatible because they are both OUT signals",
"Signals are connected but there have non compatible parameters",
"Missing block1 declaration in relation",
- "Missing block2 declaration in relation", //5
+ /*5*/"Missing block2 declaration in relation", //5
"No signal of that name in block",
"State machine must terminate with a (stop) state",
"ASM operator has not next operator",
"Empty state machine",
- "Unused elements in state machine",
+ /*10*/"Unused elements in state machine",
"The name should start with an upper case letter",
"The name should start with a lower case letter",
- "Invalid \"else\" guard"
+ "Invalid \"else\" guard",
+ "Invalid Timer attribute in signal",
+ /*15*/"Invalid Timer attribute in method",
+ "Invalid number of parameters in action on signal",
+ "Invalid attribute in action on signal",
+ "Invalid type in signal definition",
+ "Invalid int expression in action on signal",
+ /*20*/"Invalid bool expression in action on signal"
};
diff --git a/src/main/java/avatartranslator/AvatarSignal.java b/src/main/java/avatartranslator/AvatarSignal.java
index 7232b7bb44..c212838295 100644
--- a/src/main/java/avatartranslator/AvatarSignal.java
+++ b/src/main/java/avatartranslator/AvatarSignal.java
@@ -247,6 +247,10 @@ public class AvatarSignal extends AvatarMethod {
tmp = Conversion.replaceAllString(tmp, ", ", ",");
tmp = Conversion.replaceAllChar(tmp, ' ', ",");
+ if (tmp.compareTo("Timer") == 0) {
+ return null;
+ }
+
if (tmp.compareTo("int") == 0) {
AvatarAttribute aa = new AvatarAttribute("value", AvatarType.INTEGER, _block, null);
as.addParameter(aa);
@@ -295,6 +299,9 @@ public class AvatarSignal extends AvatarMethod {
two = tmp;
}
+ if (one.compareTo("Timer") == 0) {
+ return null;
+ }
if (!isAValidId(one, false, false, false, true)) {
TraceManager.addDev("Invalid type: " + one);
diff --git a/src/main/java/avatartranslator/AvatarSpecification.java b/src/main/java/avatartranslator/AvatarSpecification.java
index 1edc4a6ca9..0f50fcade2 100644
--- a/src/main/java/avatartranslator/AvatarSpecification.java
+++ b/src/main/java/avatartranslator/AvatarSpecification.java
@@ -59,6 +59,8 @@ import java.util.*;
*/
public class AvatarSpecification extends AvatarElement implements IBSParamSpec {
+ private static String keywords[] = {"BOOL", "INT", "TIMER", "SIGNAL", "METHOD", "STATE", "BLOCK", "CLASS"};
+
public final static int UPPAAL_MAX_INT = 32767;
public static String[] ops = {">", "<", "+", "-", "*", "/", "[", "]", "(", ")", ":", "=", "==", ",", "!", "?", "{", "}", "|", "&"};
@@ -1673,4 +1675,18 @@ public class AvatarSpecification extends AvatarElement implements IBSParamSpec {
return ret;
}
+ public static boolean checkKeywords(String _id) {
+ String id = _id.toUpperCase();
+ for (int i = 0; i < keywords.length; i++) {
+ if (id.compareTo(keywords[i]) == 0) {
+ return false;
+ }
+ }
+ return true;
+ }
+
+ public static boolean isAKeyword(String _id) {
+ return !checkKeywords(_id);
+ }
+
}
diff --git a/src/main/java/avatartranslator/AvatarStateMachine.java b/src/main/java/avatartranslator/AvatarStateMachine.java
index a486951fa3..3c809afbcd 100644
--- a/src/main/java/avatartranslator/AvatarStateMachine.java
+++ b/src/main/java/avatartranslator/AvatarStateMachine.java
@@ -266,6 +266,17 @@ public class AvatarStateMachine extends AvatarElement {
}
}
+ public boolean hasTimeoperatorWithAttribute(AvatarAttribute aa) {
+ for(AvatarStateMachineElement asme: elements) {
+ if (asme instanceof AvatarTimerOperator) {
+ if ( ((AvatarTimerOperator)(asme)).getTimer() == aa) {
+ return true;
+ }
+ }
+ }
+ return false;
+ }
+
public int stateNb() {
if (states == null) {
makeStates();
diff --git a/src/main/java/avatartranslator/AvatarSyntaxChecker.java b/src/main/java/avatartranslator/AvatarSyntaxChecker.java
index 12e906b310..0884006619 100644
--- a/src/main/java/avatartranslator/AvatarSyntaxChecker.java
+++ b/src/main/java/avatartranslator/AvatarSyntaxChecker.java
@@ -48,6 +48,7 @@ import myutil.Conversion;
import myutil.IntExpressionEvaluator;
import myutil.NameChecker;
import myutil.TraceManager;
+import myutil.intboolsolver.IBSExpressions;
import java.io.StringReader;
import java.util.ArrayList;
@@ -78,10 +79,15 @@ public class AvatarSyntaxChecker {
ArrayList<AvatarError> errors = new ArrayList<>();
errors.addAll(checkNextASMSpec(avspec));
+ errors.addAll(checkMethodTypes(avspec));
+ errors.addAll(checkSignalTypes(avspec));
errors.addAll(checkSignalRelations(avspec));
+ errors.addAll(checkActionOnSignals(avspec));
+ errors.addAll(checkActions(avspec));
errors.addAll(checkASMLibraryFunctions(avspec));
errors.addAll(checkElseInGuards(avspec));
+
return errors;
}
@@ -258,6 +264,75 @@ public class AvatarSyntaxChecker {
}
+ public static ArrayList<AvatarError> checkMethodTypes(AvatarSpecification avspec) {
+ ArrayList<AvatarError> errors = new ArrayList<>();
+
+ for (AvatarBlock block : avspec.getListOfBlocks()) {
+
+ for(AvatarMethod am: block.getMethods()) {
+ AvatarError err = checkMethodTypes(avspec, block, am);
+ if (err != null) {
+ errors.add(err);
+ }
+ }
+ }
+
+ return errors;
+
+ }
+
+ public static AvatarError checkMethodTypes(AvatarSpecification avspec, AvatarBlock ab, AvatarMethod am) {
+ for(AvatarAttribute aa: am.getListOfAttributes()) {
+ if (aa.getType() == AvatarType.TIMER) {
+ AvatarError err = new AvatarError(avspec);
+ err.error = 15;
+ err.block = ab;
+ err.firstAvatarElement = am;
+ return err;
+ }
+ }
+ return null;
+ }
+
+ public static ArrayList<AvatarError> checkSignalTypes(AvatarSpecification avspec) {
+ ArrayList<AvatarError> errors = new ArrayList<>();
+
+ List<AvatarSignal> signals1, signals2;
+
+ for (AvatarRelation relation : avspec.getRelations()) {
+ signals1 = relation.getSignals1();
+ signals2 = relation.getSignals2();
+
+ List<AvatarSignal> list = new ArrayList<>();
+ list.addAll(signals1);
+ list.addAll(signals2);
+
+ for(AvatarSignal sig: list) {
+ AvatarError err = checkSignalTypes(avspec, sig);
+ if (err != null) {
+ errors.add(err);
+ }
+ }
+ }
+
+ return errors;
+
+ }
+
+ public static AvatarError checkSignalTypes(AvatarSpecification avspec, AvatarSignal sig) {
+ for(AvatarAttribute aa: sig.getListOfAttributes()) {
+ if (aa.getType() == AvatarType.TIMER) {
+ AvatarError err = new AvatarError(avspec);
+ err.error = 14;
+ err.firstAvatarElement = sig;
+ return err;
+ }
+ }
+ return null;
+ }
+
+
+
public static ArrayList<AvatarError> checkSignalRelations(AvatarSpecification avspec) {
ArrayList<AvatarError> errors = new ArrayList<>();
@@ -358,6 +433,110 @@ public class AvatarSyntaxChecker {
return errors;
}
+ public static ArrayList<AvatarError> checkActionOnSignals(AvatarSpecification avspec) {
+ ArrayList<AvatarError> errors = new ArrayList<>();
+
+ for (AvatarBlock block : avspec.getListOfBlocks()) {
+ AvatarStateMachine asm = block.getStateMachine();
+ if (asm != null) {
+ for(AvatarStateMachineElement asme: asm.getListOfElements()) {
+ if (asme instanceof AvatarActionOnSignal) {
+ AvatarActionOnSignal aaos = (AvatarActionOnSignal)asme;
+ AvatarSignal sig = aaos.getSignal();
+ if (aaos.getValues().size() != sig.getListOfAttributes().size()) {
+ AvatarError error = new AvatarError(avspec);
+ error.block = block;
+ error.firstAvatarElement = aaos;
+ error.error = 16;
+ errors.add(error);
+ } else {
+ for(int i=0; i<sig.getListOfAttributes().size(); i++) {
+ // Check that value correspond to the expected type
+ // If sig is in then only variables are expected
+ String value = aaos.getValues().get(i);
+ AvatarAttribute param = sig.getListOfAttributes().get(i);
+
+ // We expect a variable only
+ if (param.getType() == AvatarType.TIMER) {
+ AvatarError error = new AvatarError(avspec);
+ error.block = block;
+ error.firstAvatarElement = aaos;
+ error.error = 14;
+ errors.add(error);
+ } else if (sig.isIn() || param.getType() == AvatarType.UNDEFINED) {
+ AvatarAttribute aa = block.getAvatarAttributeWithName(value);
+ if (aa == null) {
+ AvatarError error = new AvatarError(avspec);
+ error.block = block;
+ error.firstAvatarElement = aaos;
+ error.error = 17;
+ errors.add(error);
+ } else {
+ // We check the type of the two is equivalent
+ if (aa.getType() != param.getType()) {
+ AvatarError error = new AvatarError(avspec);
+ error.block = block;
+ error.firstAvatarElement = aaos;
+ error.error = 17;
+ errors.add(error);
+ }
+ }
+ } else {
+ // int or boot expr
+ if (param.getType() == AvatarType.INTEGER) {
+ AvatarIBSExpressions.IExpr e1 = AvatarIBSolver.parseInt(block,value);
+ if (e1 == null) {
+ AvatarError error = new AvatarError(avspec);
+ error.block = block;
+ error.firstAvatarElement = aaos;
+ error.error = 19;
+ errors.add(error);
+ }
+ } else if (param.getType() == AvatarType.BOOLEAN) {
+ IBSExpressions.BExpr e1 = AvatarIBSolver.parseBool(block,value);
+ if (e1 == null) {
+ AvatarError error = new AvatarError(avspec);
+ error.block = block;
+ error.firstAvatarElement = aaos;
+ error.error = 20;
+ errors.add(error);
+ }
+ } else {
+ AvatarError error = new AvatarError(avspec);
+ error.block = block;
+ error.firstAvatarElement = aaos;
+ error.error = 18;
+ errors.add(error);
+ }
+ }
+
+
+ }
+ }
+ }
+ }
+ }
+
+ }
+ return errors;
+ }
+
+ public static ArrayList<AvatarError> checkActions(AvatarSpecification avspec) {
+ ArrayList<AvatarError> errors = new ArrayList<>();
+
+ for (AvatarBlock block : avspec.getListOfBlocks()) {
+ AvatarStateMachine asm = block.getStateMachine();
+ if (asm != null) {
+ for (AvatarStateMachineElement asme : asm.getListOfElements()) {
+ if (asme instanceof AvatarTransition) {
+
+ }
+ }
+ }
+ }
+ return errors;
+ }
+
public static int isAValidGuard(AvatarSpecification _as, AvatarStateMachineOwner _ab, String _guard) {
//TraceManager.addDev("Evaluating (non modified) guard:" + _guard);
diff --git a/src/main/java/ui/TAttribute.java b/src/main/java/ui/TAttribute.java
index e141d62cf1..6c379b93cd 100644
--- a/src/main/java/ui/TAttribute.java
+++ b/src/main/java/ui/TAttribute.java
@@ -39,6 +39,7 @@
package ui;
+import avatartranslator.AvatarSpecification;
import myutil.NameChecker;
import tmltranslator.TMLArchiTextSpecification;
import tmltranslator.TMLMappingTextSpecification;
@@ -260,7 +261,7 @@ public class TAttribute implements NameChecker.NamedElement, NameChecker.NameSta
b1 = (id.substring(0, 1)).matches("[a-zA-Z]");
b2 = id.matches("\\w*");
if (checkKeyword) {
- b3 = !RTLOTOSKeyword.isAKeyword(lowerid);
+ b3 = !RTLOTOSKeyword.isAKeyword(lowerid) && !AvatarSpecification.isAKeyword(lowerid);
} else {
b3 = true;
}
--
GitLab