From 8482218d13cef2cdea40cc624722613e3679b1cd Mon Sep 17 00:00:00 2001
From: Ludovic Apvrille <ludovic.apvrille@telecom-paris.fr>
Date: Wed, 29 May 2024 17:11:32 +0200
Subject: [PATCH] Enhancing syntax checking with duplicate attribute detection
---
.../java/avatartranslator/AvatarBlock.java | 10 ++
.../java/avatartranslator/AvatarError.java | 1 +
.../avatartranslator/AvatarSyntaxChecker.java | 102 ++++++++++++-
src/main/java/cli/Action.java | 2 +-
.../AvatarSpecificationSyntaxCheckerTest.java | 138 ++++++++++++++++++
5 files changed, 251 insertions(+), 2 deletions(-)
create mode 100644 ttool/src/test/java/avatartranslator/AvatarSpecificationSyntaxCheckerTest.java
diff --git a/src/main/java/avatartranslator/AvatarBlock.java b/src/main/java/avatartranslator/AvatarBlock.java
index 8ca4eea5dc..1fadb331cf 100644
--- a/src/main/java/avatartranslator/AvatarBlock.java
+++ b/src/main/java/avatartranslator/AvatarBlock.java
@@ -296,6 +296,16 @@ public class AvatarBlock extends AvatarElement implements AvatarStateMachineOwne
return null;
}
+ public AvatarMethod getMethodByName(String _name) {
+ for (AvatarMethod m : methods) {
+ if (m.getName().compareTo(_name) == 0) {
+ return m;
+ }
+ }
+
+ return null;
+ }
+
public int getNbOfASMGraphicalElements() {
if (asm == null) {
return 0;
diff --git a/src/main/java/avatartranslator/AvatarError.java b/src/main/java/avatartranslator/AvatarError.java
index 40d139617a..a7ae4704ec 100644
--- a/src/main/java/avatartranslator/AvatarError.java
+++ b/src/main/java/avatartranslator/AvatarError.java
@@ -80,6 +80,7 @@ public class AvatarError {
"Incompatible types in expression",
"Invalid integer expression",
/*30*/"Invalid boolean expression",
+ "Duplicate identifier"
};
diff --git a/src/main/java/avatartranslator/AvatarSyntaxChecker.java b/src/main/java/avatartranslator/AvatarSyntaxChecker.java
index ebd50cf469..06b0e42dfd 100644
--- a/src/main/java/avatartranslator/AvatarSyntaxChecker.java
+++ b/src/main/java/avatartranslator/AvatarSyntaxChecker.java
@@ -65,11 +65,11 @@ import java.util.List;
public class AvatarSyntaxChecker {
// Errors are defined in AvatarError
-
private final static int UNUSED_ELEMENT = 10;
private final static int FIRST_UPPER_CASE = 11;
private final static int FIRST_LOWER_CASE = 12;
private final static int ERROR_IN_ELSE_GUARD = 13;
+ private final static int DUPLICATE_IDENTIFIER = 31;
public AvatarSyntaxChecker() {
}
@@ -79,6 +79,7 @@ public class AvatarSyntaxChecker {
ArrayList<AvatarError> errors = new ArrayList<>();
errors.addAll(checkNextASMSpec(avspec));
+ errors.addAll(checkDuplicateIdentifiers(avspec));
errors.addAll(checkMethodTypes(avspec));
errors.addAll(checkSignalTypes(avspec));
errors.addAll(checkSignalRelations(avspec));
@@ -145,6 +146,105 @@ public class AvatarSyntaxChecker {
return warnings;
}
+ public static ArrayList<AvatarError> checkDuplicateIdentifiers(AvatarSpecification _avspec) {
+ //TraceManager.addDev("Checking duplicate identifiers");
+
+ ArrayList<AvatarError> errors = new ArrayList<>();
+
+ for (AvatarBlock ab : _avspec.getListOfBlocks()) {
+ errors.addAll(checkDuplicateIdentifiersOfBlock(_avspec, ab));
+ }
+
+ return errors;
+ }
+
+ public static ArrayList<AvatarError> checkDuplicateIdentifiersOfBlock(AvatarSpecification _avspec, AvatarBlock _ab) {
+ ArrayList<AvatarError> errors = new ArrayList<>();
+ //TraceManager.addDev("Checking duplicate identifiers of block " + _ab.getName());
+
+ // Check that no attribute has the same identifier of a method or of a signal
+ for(AvatarAttribute aa: _ab.getAttributes()) {
+ if (_ab.getMethodByName(aa.getName()) != null) {
+ AvatarError error = new AvatarError(_avspec);
+ error.firstAvatarElement = _ab;
+ error.secondAvatarElement = aa;
+ error.error = DUPLICATE_IDENTIFIER;
+ errors.add(error);
+ }
+ if (_ab.getSignalByName(aa.getName()) != null) {
+ AvatarError error = new AvatarError(_avspec);
+ error.firstAvatarElement = _ab;
+ error.secondAvatarElement = aa;
+ error.error = DUPLICATE_IDENTIFIER;
+ errors.add(error);
+ }
+ }
+
+ // Check that no method has the same identifier as a signal
+ for(AvatarMethod m: _ab.getMethods()) {
+ if (_ab.getSignalByName(m.getName()) != null) {
+ AvatarError error = new AvatarError(_avspec);
+ error.firstAvatarElement = _ab;
+ error.secondAvatarElement = m;
+ error.error = DUPLICATE_IDENTIFIER;
+ errors.add(error);
+ }
+ }
+
+ // Check that two attributes, two methods, or two signals don't have the same identifier
+ List<AvatarAttribute> l = _ab.getAttributes();
+ for(int i=0; i<l.size(); i++) {
+ //TraceManager.addDev("i=" + i);
+ for(int j=i+1; j<l.size(); j++) {
+ AvatarAttribute a1, a2;
+ a1 = l.get(i);
+ a2 = l.get(j);
+ //TraceManager.addDev("Testing a1=" + a1 + " a2=" + a2);
+ if (a1.getName().compareTo(a2.getName()) == 0) {
+ AvatarError error = new AvatarError(_avspec);
+ error.firstAvatarElement = _ab;
+ error.secondAvatarElement = a1;
+ error.error = DUPLICATE_IDENTIFIER;
+ errors.add(error);
+ }
+ }
+ }
+
+ List<AvatarMethod> lm = _ab.getMethods();
+ for(int i=0; i<lm.size(); i++) {
+ for(int j=i+1; j<lm.size(); j++) {
+ AvatarMethod m1, m2;
+ m1 = lm.get(i);
+ m2 = lm.get(j);
+ if (m1.getName().compareTo(m2.getName()) == 0) {
+ AvatarError error = new AvatarError(_avspec);
+ error.firstAvatarElement = _ab;
+ error.secondAvatarElement = m1;
+ error.error = DUPLICATE_IDENTIFIER;
+ errors.add(error);
+ }
+ }
+ }
+
+ List<AvatarSignal> ls = _ab.getSignals();
+ for(int i=0; i<ls.size(); i++) {
+ for(int j=i+1; j<ls.size(); j++) {
+ AvatarSignal s1, s2;
+ s1 = ls.get(i);
+ s2 = ls.get(j);
+ if (s1.getName().compareTo(s2.getName()) == 0) {
+ AvatarError error = new AvatarError(_avspec);
+ error.firstAvatarElement = _ab;
+ error.secondAvatarElement = s1;
+ error.error = DUPLICATE_IDENTIFIER;
+ errors.add(error);
+ }
+ }
+ }
+
+ return errors;
+ }
+
public static ArrayList<AvatarError> checkNames(AvatarSpecification _avspec, NameChecker.NamedElement _ne) {
ArrayList<AvatarError> warnings = new ArrayList<>();
diff --git a/src/main/java/cli/Action.java b/src/main/java/cli/Action.java
index b2bda28d0f..ef740c7e2d 100644
--- a/src/main/java/cli/Action.java
+++ b/src/main/java/cli/Action.java
@@ -1562,7 +1562,7 @@ public class Action extends Command implements ProVerifOutputListener {
public String executeCommand(String command, Interpreter interpreter) {
-
+
AvatarSpecification spec = as;
if (spec == null) {
if (!interpreter.isTToolStarted()) {
diff --git a/ttool/src/test/java/avatartranslator/AvatarSpecificationSyntaxCheckerTest.java b/ttool/src/test/java/avatartranslator/AvatarSpecificationSyntaxCheckerTest.java
new file mode 100644
index 0000000000..5db75ec98d
--- /dev/null
+++ b/ttool/src/test/java/avatartranslator/AvatarSpecificationSyntaxCheckerTest.java
@@ -0,0 +1,138 @@
+/**Copyright or (C) or Copr. GET / ENST, Telecom-Paris, Ludovic Apvrille
+ *
+ * ludovic.apvrille AT enst.fr
+ *
+ * This software is a computer program whose purpose is to allow the
+ * edition of TURTLE analysis, design and deployment diagrams, to
+ * allow the generation of RT-LOTOS or Java code from this diagram,
+ * and at last to allow the analysis of formal validation traces
+ * obtained from external tools, e.g. RTL from LAAS-CNRS and CADP
+ * from INRIA Rhone-Alpes.
+ *
+ * This software is governed by the CeCILL license under French law and
+ * abiding by the rules of distribution of free software. You can use,
+ * modify and/ or redistribute the software under the terms of the CeCILL
+ * license as circulated by CEA, CNRS and INRIA at the following URL
+ * "http://www.cecill.info".
+ *
+ * As a counterpart to the access to the source code and rights to copy,
+ * modify and redistribute granted by the license, users are provided only
+ * with a limited warranty and the software's author, the holder of the
+ * economic rights, and the successive licensors have only limited
+ * liability.
+ *
+ * In this respect, the user's attention is drawn to the risks associated
+ * with loading, using, modifying and/or developing or reproducing the
+ * software by the user in light of its specific status of free software,
+ * that may mean that it is complicated to manipulate, and that also
+ * therefore means that it is reserved for developers and experienced
+ * professionals having in-depth computer knowledge. Users are therefore
+ * encouraged to load and test the software's suitability as regards their
+ * requirements in conditions enabling the security of their systems and/or
+ * data to be ensured and, more generally, to use and operate it in the
+ * same conditions as regards security.
+ *
+ * The fact that you are presently reading this means that you have had
+ * knowledge of the CeCILL license and that you accept its terms.
+ *
+ * /**
+ * Class AvatarExpressionTest
+ * Creation: 29/04/2020
+ * @version 1.0 29/04/2020
+ * @author Alessandro TEMPIA CALVINO
+ * @see
+ */
+
+
+package avatartranslator;
+
+import static org.junit.Assert.*;
+import static org.junit.Assert.assertTrue;
+
+import myutil.TraceManager;
+import org.junit.Before;
+import org.junit.Test;
+
+import avatartranslator.modelchecker.SpecificationBlock;
+import avatartranslator.modelchecker.SpecificationState;
+
+import java.util.ArrayList;
+
+public class AvatarSpecificationSyntaxCheckerTest {
+
+ public AvatarSpecificationSyntaxCheckerTest() {
+ }
+
+ @Before
+ public void test () {
+
+ }
+
+ @Test
+ public void testDuplicateAttribute() {
+
+ AvatarSpecification as = new AvatarSpecification("avatarspecification", null);
+ AvatarBlock block1 = new AvatarBlock("block1", as, null);
+ as.addBlock(block1);
+
+ AvatarAttribute a1 = new AvatarAttribute("a1", AvatarType.INTEGER, block1, null);
+ block1.addAttribute(a1);
+ AvatarAttribute a2 = new AvatarAttribute("a1", AvatarType.INTEGER, block1, null);
+ block1.addAttribute(a2);
+
+ TraceManager.addDev("Number of attributes in block1:" + block1.getAttributes().size());
+ assertEquals(block1.getAttributes().size(), 1);
+ block1.getAttributes().add(a2);
+ TraceManager.addDev("Number of attributes in block1:" + block1.getAttributes().size());
+ assertEquals(block1.getAttributes().size(), 2);
+
+
+ ArrayList<AvatarError> myErrors = AvatarSyntaxChecker.checkSyntaxErrors(as);
+ assertEquals(myErrors.size(), 1);
+
+ AvatarAttribute a3 = new AvatarAttribute("a3", AvatarType.INTEGER, block1, null);
+ block1.addAttribute(a3);
+ AvatarAttribute a4 = new AvatarAttribute("a4", AvatarType.INTEGER, block1, null);
+ block1.addAttribute(a4);
+
+ assertEquals(block1.getAttributes().size(), 4);
+ myErrors = AvatarSyntaxChecker.checkSyntaxErrors(as);
+ assertEquals(myErrors.size(), 1);
+
+ block1.getAttributes().add(a2);
+ assertEquals(block1.getAttributes().size(), 5);
+ myErrors = AvatarSyntaxChecker.checkSyntaxErrors(as);
+ assertEquals(myErrors.size(), 3);
+
+ AvatarMethod am1 = new AvatarMethod("myLovelyMethod1", null);
+ block1.addMethod(am1);
+ myErrors = AvatarSyntaxChecker.checkSyntaxErrors(as);
+ assertEquals(myErrors.size(), 3);
+
+ block1.getMethods().add(am1);
+ myErrors = AvatarSyntaxChecker.checkSyntaxErrors(as);
+ assertEquals(myErrors.size(), 4);
+
+ AvatarMethod am2 = new AvatarMethod("a1", null);
+ block1.addMethod(am2);
+ myErrors = AvatarSyntaxChecker.checkSyntaxErrors(as);
+ assertEquals(myErrors.size(), 7);
+
+ AvatarSignal as1 = new AvatarSignal("myLovelySignal1", ui.AvatarSignal.IN, null);
+ block1.addSignal(as1);
+ myErrors = AvatarSyntaxChecker.checkSyntaxErrors(as);
+ assertEquals(myErrors.size(), 7);
+
+ block1.getMethods().add(as1);
+ myErrors = AvatarSyntaxChecker.checkSyntaxErrors(as);
+ assertEquals(myErrors.size(), 8);
+
+ AvatarSignal as2 = new AvatarSignal("myLovelyMethod1", ui.AvatarSignal.IN,null);
+ block1.addSignal(as2);
+ myErrors = AvatarSyntaxChecker.checkSyntaxErrors(as);
+ assertEquals(myErrors.size(), 10);
+
+
+
+ }
+}
--
GitLab