From dbe1a4e14fb690a6ee74881122757b0235b87610 Mon Sep 17 00:00:00 2001
From: tempiaa <tempiaa@eurecom.fr>
Date: Fri, 24 Jul 2020 15:56:43 +0200
Subject: [PATCH] Fix in syntax checker errors display, fix in true false
pragma expected value
---
.../modelchecker/SafetyProperty.java | 8 +++---
.../ModelCheckerValidator.java | 4 +--
.../java/ui/AvatarDesignPanelTranslator.java | 26 ++++++++++++-------
.../ui/window/JDialogUPPAALValidation.java | 8 +++---
4 files changed, 27 insertions(+), 19 deletions(-)
diff --git a/src/main/java/avatartranslator/modelchecker/SafetyProperty.java b/src/main/java/avatartranslator/modelchecker/SafetyProperty.java
index 7085d1bda9..967836ba91 100644
--- a/src/main/java/avatartranslator/modelchecker/SafetyProperty.java
+++ b/src/main/java/avatartranslator/modelchecker/SafetyProperty.java
@@ -269,12 +269,12 @@ public class SafetyProperty {
}
private String checkExpectedResult(String tmpP) {
- if (tmpP.startsWith("T") || tmpP.startsWith("t")) {
+ if (tmpP.startsWith("T ") || tmpP.startsWith("t ")) {
expectedResult = true;
- return tmpP.substring(1).trim();
- } else if (tmpP.startsWith("F") || tmpP.startsWith("f")) {
+ return tmpP.substring(2).trim();
+ } else if (tmpP.startsWith("F ") || tmpP.startsWith("f ")) {
expectedResult = false;
- return tmpP.substring(1).trim();
+ return tmpP.substring(2).trim();
}
return tmpP;
diff --git a/src/main/java/avatartranslator/modelcheckervalidator/ModelCheckerValidator.java b/src/main/java/avatartranslator/modelcheckervalidator/ModelCheckerValidator.java
index 23618c6f40..af80169f45 100644
--- a/src/main/java/avatartranslator/modelcheckervalidator/ModelCheckerValidator.java
+++ b/src/main/java/avatartranslator/modelcheckervalidator/ModelCheckerValidator.java
@@ -286,8 +286,8 @@ public class ModelCheckerValidator {
private static String removeExpectedResult(String query) {
- if (query.matches("^[TtFf].*")) {
- return query.substring(1).trim();
+ if (query.matches("^[TtFf]\\s.*")) {
+ return query.substring(2).trim();
} else {
return query;
}
diff --git a/src/main/java/ui/AvatarDesignPanelTranslator.java b/src/main/java/ui/AvatarDesignPanelTranslator.java
index 47567278d2..a873c0f27d 100644
--- a/src/main/java/ui/AvatarDesignPanelTranslator.java
+++ b/src/main/java/ui/AvatarDesignPanelTranslator.java
@@ -425,8 +425,8 @@ public class AvatarDesignPanelTranslator {
_pragma = _pragma.trim();
//remove expected result letter from the start if present
- if (_pragma.matches("^[TtFf].*")) {
- _pragma = _pragma.substring(1).trim();
+ if (_pragma.matches("^[TtFf]\\s.*")) {
+ _pragma = _pragma.substring(2).trim();
}
if (_pragma.contains("=") && !(_pragma.contains("==") || _pragma.contains("<=") || _pragma.contains(">=") || _pragma.contains("!="))) {
@@ -460,10 +460,10 @@ public class AvatarDesignPanelTranslator {
String state1 = _pragma.split("-->")[0];
String state2 = _pragma.split("-->")[1];
// System.out.println("checking... " + state1 + " " + state2);
- if (!state1.contains(".") || !state2.contains(".")) {
- TraceManager.addDev("Safety Pragma " + _pragma + " cannot be parsed: missing '.'");
- return false;
- }
+// if (!state1.contains(".") || !state2.contains(".")) {
+// TraceManager.addDev("Safety Pragma " + _pragma + " cannot be parsed: missing '.'");
+// return false;
+// }
if (!statementParser(state1, as, _pragma, tgc)) {
return false;
}
@@ -482,6 +482,10 @@ public class AvatarDesignPanelTranslator {
} else {
+ UICheckingError ce = new UICheckingError(CheckingError.STRUCTURE_ERROR, "Pragma " + _pragma + " cannot be parsed: wrong or missing CTL header");
+ ce.setTDiagramPanel(adp.getAvatarBDPanel());
+ ce.setTGComponent(tgc);
+ addWarning(ce);
TraceManager.addDev("Safety Pragma " + _pragma + " cannot be parsed");
return false;
}
@@ -501,16 +505,19 @@ public class AvatarDesignPanelTranslator {
}
state = replaceOperators(state);
- if (statementParserRec(state, as, _pragma, tgc) == 1) {
+ int returnVal = statementParserRec(state, as, _pragma, tgc);
+ if (returnVal == 1) {
UICheckingError ce = new UICheckingError(CheckingError.STRUCTURE_ERROR, "Safety Pragma " + _pragma + " has invalid return type");
ce.setTDiagramPanel(adp.getAvatarBDPanel());
ce.setTGComponent(tgc);
addWarning(ce);
TraceManager.addDev("UPPAAL Pragma " + _pragma + " improperly formatted");
return false;
+ } else if (returnVal == -1) {
+ return false;
+ } else {
+ return true;
}
-
- return true;
//Divide into simple statements
@@ -698,6 +705,7 @@ public class AvatarDesignPanelTranslator {
}
private int statementParserRec(String state, AvatarSpecification as, String _pragma, TGComponent tgc) {
+ //returns -1 for errors, 0 for boolean result type, and 1 for int result type
boolean isNot = false;
boolean isNegated = false;
diff --git a/src/main/java/ui/window/JDialogUPPAALValidation.java b/src/main/java/ui/window/JDialogUPPAALValidation.java
index baa855e6e5..ff6a351031 100644
--- a/src/main/java/ui/window/JDialogUPPAALValidation.java
+++ b/src/main/java/ui/window/JDialogUPPAALValidation.java
@@ -869,11 +869,11 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti
query = query.trim();
expectedResult = true;
- if (query.startsWith("T") || query.startsWith("t")) {
- return query.substring(1).trim();
- } else if (query.startsWith("F") || query.startsWith("f")) {
+ if (query.startsWith("T ") || query.startsWith("t ")) {
+ return query.substring(2).trim();
+ } else if (query.startsWith("F ") || query.startsWith("f ")) {
expectedResult = false;
- return query.substring(1).trim();
+ return query.substring(2).trim();
}
return query;
--
GitLab