From e14fa4a02c13f0aeb0eb017ea82255f9d4e481c1 Mon Sep 17 00:00:00 2001
From: Ludovic Apvrille <ludovic.apvrille@telecom-paris.fr>
Date: Thu, 6 Jan 2022 17:09:07 +0100
Subject: [PATCH] Resolving bug on channel artifact edition, and adding static
values to fiels of proverif dialog window
---
src/main/java/ui/GTMLModeling.java | 16 +++++-
.../tmldd/TMLArchiCommunicationArtifact.java | 4 ++
.../java/ui/tmldd/TMLArchiDiagramToolBar.java | 2 +-
.../java/ui/tmldd/TMLArchiEventArtifact.java | 8 ---
.../window/JDialogCommunicationArtifact.java | 11 ++---
.../window/JDialogProverifVerification.java | 49 ++++++++++++++-----
6 files changed, 60 insertions(+), 30 deletions(-)
diff --git a/src/main/java/ui/GTMLModeling.java b/src/main/java/ui/GTMLModeling.java
index ce198fd41f..37ae2e2bd1 100644
--- a/src/main/java/ui/GTMLModeling.java
+++ b/src/main/java/ui/GTMLModeling.java
@@ -3868,9 +3868,11 @@ public class GTMLModeling {
// Other nodes (memory, bridge, bus, VGMN, crossbar)
//}
- if ((tgc instanceof TMLArchiBUSNode) || (tgc instanceof TMLArchiVGMNNode) || (tgc instanceof TMLArchiCrossbarNode) || (tgc instanceof TMLArchiBridgeNode) || (tgc instanceof TMLArchiMemoryNode) || (tgc instanceof TMLArchiDMANode) || (tgc instanceof TMLArchiFirewallNode)) {
+ if ((tgc instanceof TMLArchiBUSNode) || (tgc instanceof TMLArchiVGMNNode) || (tgc instanceof TMLArchiCrossbarNode)
+ || (tgc instanceof TMLArchiBridgeNode) || (tgc instanceof TMLArchiMemoryNode) || (tgc instanceof TMLArchiDMANode)
+ || (tgc instanceof TMLArchiFirewallNode)) {
node = archi.getHwNodeByName(tgc.getName());
- if ((node != null) && (node instanceof HwCommunicationNode)) {
+ if (node instanceof HwCommunicationNode) {
if (tgc instanceof TMLArchiFirewallNode) {
map.firewall = true;
}
@@ -3895,10 +3897,20 @@ public class GTMLModeling {
if (elt instanceof TMLChannel) {
//TraceManager.addDev("Setting priority of " + elt + " to " + artifact.getPriority() );
((TMLChannel) (elt)).setPriority(artifact.getPriority());
+
}
if (elt != null) {
//TraceManager.addDev( "Adding communication " + s + " to Hardware Communication Node " + node.getName() );
map.addCommToHwCommNode(elt, (HwCommunicationNode) node);
+
+ // Map to other referenced comm of the artifact
+ for(String nn: artifact.getOtherCommunicationNames()) {
+ HwNode oNode = archi.getHwNodeByName(nn);
+ if (oNode instanceof HwCommunicationNode) {
+ TraceManager.addDev("Found another node for allocation of " + s + ": " + nn);
+ map.addCommToHwCommNode(elt, (HwCommunicationNode) oNode);
+ }
+ }
} else {
//TraceManager.addDev("Null mapping: no element named: " + s );
}
diff --git a/src/main/java/ui/tmldd/TMLArchiCommunicationArtifact.java b/src/main/java/ui/tmldd/TMLArchiCommunicationArtifact.java
index bf03b461cb..a6ba9b8dd1 100755
--- a/src/main/java/ui/tmldd/TMLArchiCommunicationArtifact.java
+++ b/src/main/java/ui/tmldd/TMLArchiCommunicationArtifact.java
@@ -352,6 +352,10 @@ public class TMLArchiCommunicationArtifact extends TGCWithoutInternalComponent i
return communicationName;
}
+ public ArrayList<String> getOtherCommunicationNames() {
+ return mappedElements;
+ }
+
public String getFullValue() {
String tmp = getValue();
tmp += " (" + getTypeName() + ")";
diff --git a/src/main/java/ui/tmldd/TMLArchiDiagramToolBar.java b/src/main/java/ui/tmldd/TMLArchiDiagramToolBar.java
index 7d5b4c60b6..47ecb223c9 100755
--- a/src/main/java/ui/tmldd/TMLArchiDiagramToolBar.java
+++ b/src/main/java/ui/tmldd/TMLArchiDiagramToolBar.java
@@ -88,7 +88,7 @@ public class TMLArchiDiagramToolBar extends TToolBar implements ActionListener {
mgui.actions[TGUIAction.TMLARCHI_KEY].setEnabled(b);
mgui.actions[TGUIAction.TMLARCHI_FIREWALL].setEnabled(b);
mgui.actions[TGUIAction.TMLARCHI_PORT_ARTIFACT].setEnabled(b);
- mgui.actions[TGUIAction.TMLARCHI_EVENT_ARTIFACT].setEnabled(b);
+ //mgui.actions[TGUIAction.TMLARCHI_EVENT_ARTIFACT].setEnabled(b);
mgui.actions[TGUIAction.TMLARCHI_MEMORYNODE].setEnabled(b);
mgui.actions[TGUIAction.TMLARCHI_DMANODE].setEnabled(b);
mgui.actions[TGUIAction.ACT_TOGGLE_ATTR].setEnabled(b);
diff --git a/src/main/java/ui/tmldd/TMLArchiEventArtifact.java b/src/main/java/ui/tmldd/TMLArchiEventArtifact.java
index 022a37866c..4ca1529387 100755
--- a/src/main/java/ui/tmldd/TMLArchiEventArtifact.java
+++ b/src/main/java/ui/tmldd/TMLArchiEventArtifact.java
@@ -64,14 +64,6 @@ public class TMLArchiEventArtifact extends TGCWithoutInternalComponent implement
private static final int CRAN = 5;
private static final int FILE_X = 20;
private static final int FILE_Y = 25;
-// protected int lineLength = 5;
-// protected int textX = 5;
-// protected int textY = 15;
-// protected int textY2 = 35;
-// protected int space = 5;
-// protected int fileX = 20;
-// protected int fileY = 25;
-// protected int cran = 5;
protected String oldValue = "";
protected String referenceEventName = "TMLEvent";
diff --git a/src/main/java/ui/window/JDialogCommunicationArtifact.java b/src/main/java/ui/window/JDialogCommunicationArtifact.java
index 3a74e5480d..f7b52c45f2 100644
--- a/src/main/java/ui/window/JDialogCommunicationArtifact.java
+++ b/src/main/java/ui/window/JDialogCommunicationArtifact.java
@@ -153,12 +153,10 @@ public class JDialogCommunicationArtifact extends JDialogBase implements ActionL
list.add("No communication to map");
emptyList = true;
} else {
-
- index = indexOf(list, artifact.getFullValue());
- //
+ index = indexOf(list, artifact.getValue());
}
- TraceManager.addDev("Got communications");
+ TraceManager.addDev("Got communications. Index=" + index);
referenceCommunicationName = new JComboBox<>(list);
referenceCommunicationName.setSelectedIndex(index);
@@ -201,7 +199,7 @@ public class JDialogCommunicationArtifact extends JDialogBase implements ActionL
c3.fill = GridBagConstraints.HORIZONTAL;
panel3.add(new JLabel("Memories and buses:"), c3);
Vector<String> memAndBuses = makeListOfMappableArchUnits(mappedUnits);
- TraceManager.addDev("Size of jlist:" + memAndBuses.size());
+ //TraceManager.addDev("Size of jlist:" + memAndBuses.size());
mappableElementsModel = new DefaultListModel<>();
for (String s: memAndBuses) {
mappableElementsModel.addElement(s);
@@ -430,6 +428,7 @@ public class JDialogCommunicationArtifact extends JDialogBase implements ActionL
public int indexOf(Vector<String> _list, String name) {
+ //TraceManager.addDev("Computing index with name=" + name + "\n");
int i = 0;
for (String s : _list) {
if (s.equals(name)) {
@@ -452,7 +451,7 @@ public class JDialogCommunicationArtifact extends JDialogBase implements ActionL
for (TGComponent tgc : componentList) {
if (tgc instanceof TMLArchiCommunicationNode) {
if (!(alreadyMapped.contains(tgc.getName()))) {
- TraceManager.addDev("Adding component: " + tgc.getName());
+ //TraceManager.addDev("Adding component: " + tgc.getName());
list.add(tgc.getName());
}
}
diff --git a/src/main/java/ui/window/JDialogProverifVerification.java b/src/main/java/ui/window/JDialogProverifVerification.java
index 6e0234fa5b..70bb34aaee 100644
--- a/src/main/java/ui/window/JDialogProverifVerification.java
+++ b/src/main/java/ui/window/JDialogProverifVerification.java
@@ -126,6 +126,17 @@ public class JDialogProverifVerification extends JDialog implements ActionListen
private static final Insets insets = new Insets(0, 0, 0, 0);
private static final Insets WEST_INSETS = new Insets(0, 0, 0, 0);
+ public final static int REACHABILITY_ALL = 1;
+ public final static int REACHABILITY_SELECTED = 2;
+ public final static int REACHABILITY_NONE = 3;
+
+ private static String CODE_PATH = null;
+ private static String EXECUTE_PATH = null;
+ private static int REACHABILITY_OPTION = REACHABILITY_ALL;
+ private static boolean MSG_DUPLICATION = true;
+ private static boolean PI_CALCULUS = true;
+ private static int LOOP_ITERATION = 1;
+
protected MainGUI mgui;
private AvatarDesignPanel adp;
@@ -137,9 +148,7 @@ public class JDialogProverifVerification extends JDialog implements ActionListen
protected final static int STARTED = 2;
protected final static int STOPPED = 3;
- public final static int REACHABILITY_ALL = 1;
- public final static int REACHABILITY_SELECTED = 2;
- public final static int REACHABILITY_NONE = 3;
+
TURTLEPanel currPanel;
@@ -248,10 +257,8 @@ public class JDialogProverifVerification extends JDialog implements ActionListen
this.pvoa = null;
this.limit = lim;
- pathCode = _pathCode;
-
- if (pathExecute == null)
- pathExecute = _pathExecute;
+ pathCode = ((CODE_PATH == null) ? _pathCode : CODE_PATH);
+ pathExecute = ((EXECUTE_PATH == null) ? _pathExecute : EXECUTE_PATH);
hostProVerif = _hostProVerif;
@@ -515,7 +522,9 @@ public class JDialogProverifVerification extends JDialog implements ActionListen
stateReachabilityGroup.add(stateReachabilityAll);
stateReachabilityGroup.add(stateReachabilitySelected);
stateReachabilityGroup.add(stateReachabilityNone);
- stateReachabilityAll.setSelected(true);
+ stateReachabilityAll.setSelected(REACHABILITY_OPTION == REACHABILITY_ALL);
+ stateReachabilitySelected.setSelected(REACHABILITY_OPTION == REACHABILITY_SELECTED);
+ stateReachabilityNone.setSelected(REACHABILITY_OPTION == REACHABILITY_NONE);
curY++;
addComponent(jp01, new JLabel("Allow message duplication in private channels: "), 0, curY, 2,
@@ -529,14 +538,15 @@ public class JDialogProverifVerification extends JDialog implements ActionListen
privateChannelGroup.add(privateChannelNoDup);
// TODO: change that
// privateChannelNoDup.setSelected(true);
- privateChannelDup.setSelected(true);
+ privateChannelDup.setSelected(MSG_DUPLICATION);
+ privateChannelNoDup.setSelected(!MSG_DUPLICATION);
curY++;
typedLanguage = new JCheckBox("Generate typed Pi calculus");
- typedLanguage.setSelected(true);
+ typedLanguage.setSelected(PI_CALCULUS);
addComponent(jp01, typedLanguage, 0, curY, 1, GridBagConstraints.CENTER, GridBagConstraints.BOTH);
curY++;
- loopLimit = new JTextField("1", 3);
+ loopLimit = new JTextField(""+LOOP_ITERATION, 3);
if (limit) {
addComponent(jp01, new JLabel("Limit on loop iterations:"), 0, curY, 1, GridBagConstraints.CENTER, GridBagConstraints.BOTH);
addComponent(jp01, loopLimit, 1, curY, 2, GridBagConstraints.CENTER, GridBagConstraints.BOTH);
@@ -550,8 +560,6 @@ public class JDialogProverifVerification extends JDialog implements ActionListen
-
-
jta = new JPanel();
jta.setLayout(new GridBagLayout());
jta.setBorder(new javax.swing.border.TitledBorder("Results"));
@@ -768,6 +776,21 @@ public class JDialogProverifVerification extends JDialog implements ActionListen
if (mode == STARTED) {
stopProcess();
}
+ CODE_PATH = code1.getText();
+ EXECUTE_PATH = exe2.getText();
+ if (stateReachabilityAll.isSelected()) {
+ REACHABILITY_OPTION = REACHABILITY_ALL;
+ } else if (stateReachabilitySelected.isSelected()) {
+ REACHABILITY_OPTION = REACHABILITY_SELECTED;
+ } else {
+ REACHABILITY_OPTION = REACHABILITY_NONE;
+ }
+ MSG_DUPLICATION = privateChannelDup.isSelected();
+ PI_CALCULUS = typedLanguage.isSelected();
+ try {
+ LOOP_ITERATION = Integer.decode(loopLimit.getText());
+ } catch (Exception e) {}
+
dispose();
}
--
GitLab