From 766e80558f9cb44422de81984f5c7af96bb33db8 Mon Sep 17 00:00:00 2001
From: Letitia Li <letitia.li@telecom-paristech.fr>
Date: Fri, 17 Nov 2017 15:01:19 +0100
Subject: [PATCH] UPPAAL Pragma fixes
---
.../java/ui/AvatarDesignPanelTranslator.java | 19 +++++++++--
src/main/java/ui/avatarbd/AvatarBDPragma.java | 6 ++--
.../ui/avatarbd/AvatarBDSafetyPragma.java | 5 +--
.../java/ui/window/JDialogSafetyPragma.java | 32 ++++++++++++++++---
4 files changed, 51 insertions(+), 11 deletions(-)
diff --git a/src/main/java/ui/AvatarDesignPanelTranslator.java b/src/main/java/ui/AvatarDesignPanelTranslator.java
index e768a7bbbc..9e1b261ad3 100644
--- a/src/main/java/ui/AvatarDesignPanelTranslator.java
+++ b/src/main/java/ui/AvatarDesignPanelTranslator.java
@@ -205,6 +205,9 @@ public class AvatarDesignPanelTranslator {
//TraceManager.addDev("Adding pragma:" + tmp);
}
}
+ else {
+ tgcn.syntaxErrors.add(values[i]);
+ }
}
}
if (tgc instanceof AvatarBDSafetyPragma) {
@@ -435,6 +438,10 @@ public class AvatarDesignPanelTranslator {
}
String block1 = state1.split("\\.",2)[0];
String attr1 = state1.split("\\.",2)[1];
+ if (attr1.contains(".")){
+ TraceManager.addDev("Complex UPPAAL Pragma attribute " + attr1 + " must contain __ and not .");
+ return false;
+ }
attr1 = attr1.replace(".","__");
AvatarType p1Type= AvatarType.UNDEFINED;
@@ -458,7 +465,11 @@ public class AvatarDesignPanelTranslator {
if (state2.contains(".")){
String block2 = state2.split("\\.",2)[0];
String attr2= state2.split("\\.",2)[1];
- attr2 = attr2.replace(".","__");
+ if (attr2.contains(".")){
+ TraceManager.addDev("Complex UPPAAL Pragma attribute " + attr2 + " must contain __ and not .");
+ return false;
+ }
+
AvatarBlock bl2 = as.getBlockWithName(block2);
if (bl2!=null){
if (bl2.getIndexOfAvatarAttributeWithName(attr2)==-1){
@@ -501,8 +512,10 @@ public class AvatarDesignPanelTranslator {
}
String block1 = state.split("\\.",2)[0];
String attr1 = state.split("\\.",2)[1];
- // System.out.println("ATTR " + attr1);
- attr1 = attr1.replace(".", "__");
+ if (attr1.contains(".")){
+ TraceManager.addDev("Complex UPPAAL Pragma attribute " + attr1 + " must contain __ and not .");
+ return false;
+ }
AvatarBlock bl1 = as.getBlockWithName(block1);
if (bl1 !=null){
AvatarStateMachine asm = bl1.getStateMachine();
diff --git a/src/main/java/ui/avatarbd/AvatarBDPragma.java b/src/main/java/ui/avatarbd/AvatarBDPragma.java
index 7fa37939d0..fb6d3c5b25 100755
--- a/src/main/java/ui/avatarbd/AvatarBDPragma.java
+++ b/src/main/java/ui/avatarbd/AvatarBDPragma.java
@@ -292,9 +292,11 @@ public class AvatarBDPragma extends TGCScalableWithoutInternalComponent {
properties.add(s);
}
else {
+ //Pretend it's a model pragma
+ models.add(s);
//Warning Message
- JOptionPane.showMessageDialog(null, s + " is not a valid pragma.", "Invalid Pragma",
- JOptionPane.INFORMATION_MESSAGE);
+ //Do not show this: //JOptionPane.showMessageDialog(null, s + " is not a valid pragma.", "Invalid Pragma",
+ // JOptionPane.INFORMATION_MESSAGE);
}
}
//checkMySize();
diff --git a/src/main/java/ui/avatarbd/AvatarBDSafetyPragma.java b/src/main/java/ui/avatarbd/AvatarBDSafetyPragma.java
index 08cef3c8e0..2691caeff5 100644
--- a/src/main/java/ui/avatarbd/AvatarBDSafetyPragma.java
+++ b/src/main/java/ui/avatarbd/AvatarBDSafetyPragma.java
@@ -240,9 +240,10 @@ public class AvatarBDSafetyPragma extends TGCScalableWithoutInternalComponent {
properties.add(s);
}
else {
+ properties.add(s);
//Warning Message
- JOptionPane.showMessageDialog(null, s + " is not a valid pragma.", "Invalid Pragma",
- JOptionPane.INFORMATION_MESSAGE);
+ //Never show this: JOptionPane.showMessageDialog(null, s + " is not a valid pragma.", "Invalid Pragma",
+ // JOptionPane.INFORMATION_MESSAGE);
}
}
//checkMySize();
diff --git a/src/main/java/ui/window/JDialogSafetyPragma.java b/src/main/java/ui/window/JDialogSafetyPragma.java
index 0cfdb4202e..209de4e7d0 100644
--- a/src/main/java/ui/window/JDialogSafetyPragma.java
+++ b/src/main/java/ui/window/JDialogSafetyPragma.java
@@ -263,6 +263,7 @@ public class JDialogSafetyPragma extends JDialogBase implements ActionListener {
protected void initComponents() {
+
Container c = getContentPane();
Font f = new Font("Helvetica", Font.PLAIN, 14);
setFont(f);
@@ -271,13 +272,36 @@ public class JDialogSafetyPragma extends JDialogBase implements ActionListener {
helpPopup = new JPopupMenu();
//JTextArea jft = new JTextArea("UPPAAL pragmas");
//helpPopup.add(jft);
- helpPopup.add(new JLabel("UPPAAL safety queries determine if the behavior of a system. They must appear in one of the following formats."));
- helpPopup.add(new JLabel(IconManager.imgic7002));
+ helpPopup.add(new JLabel("UPPAAL safety queries determine if the behavior of a system."));
+ helpPopup.add(new JLabel("They must appear in one of the following formats:"));
+ /*JLabel row1 = new JLabel();
+ row1.setLayout(new BoxLayout(row1, BoxLayout.X_AXIS));
+ row1.add(
+ row1.add(new JLabel(IconManager.imgic7003));
+ */
+ helpPopup.add(new JLabel(IconManager.imgic7002));
helpPopup.add(new JLabel(IconManager.imgic7003));
+ /*JLabel row2 = new JLabel();
+ row2.setLayout(new BoxLayout(row2, BoxLayout.X_AXIS));
+ row2.add(new JLabel(IconManager.imgic7004));
+ row2.add(new JLabel(IconManager.imgic7005));
+ helpPopup.add(row2);*/
helpPopup.add(new JLabel(IconManager.imgic7004));
- helpPopup.add(new JLabel(IconManager.imgic7005));
+ helpPopup.add(new JLabel(IconManager.imgic7005));
helpPopup.add(new JLabel(IconManager.imgic7006));
- helpPopup.setPreferredSize(new Dimension(150,650));
+ helpPopup.add(new JLabel("An expression 'p' or 'q' may take the following forms:"));
+ helpPopup.add(new JLabel("Expressions on a state in a state machine:"));
+ helpPopup.add(new JLabel(" Block.state : ie 'System.running'"));
+ helpPopup.add(new JLabel("Expressions on boolean or integer attribute:"));
+ helpPopup.add(new JLabel(" Block.attribute==value : ie 'System.error==false or System.value==1'"));
+ helpPopup.add(new JLabel(" Block.attribute==Block2.attribute2 : ie 'System.running==Sensor.isActive'"));
+ helpPopup.add(new JLabel("Complex user-defined attributes must be written in the form attr__a:"));
+ helpPopup.add(new JLabel("ie 'System.complexAttribute__subAttribute1'"));
+
+ helpPopup.add(new JLabel("Valid expressions may be combined with the and/or operators '&&' or '||' respectively "));
+ helpPopup.add(new JLabel(" ie 'System.running || System.value==1'"));
+
+ helpPopup.setPreferredSize(new Dimension(600,830));
textarea = new JTextArea();
textarea.setEditable(true);
--
GitLab