From cab9e55b46423faaefa4e28f855c1f7e3d5e8250 Mon Sep 17 00:00:00 2001
From: Ludovic Apvrille <ludovic.apvrille@telecom-paris.fr>
Date: Fri, 7 Jul 2023 15:30:59 +0200
Subject: [PATCH] Resolving bug on main diagram in reset proverif backtracing
---
src/main/java/ai/AIBlock.java | 4 +---
src/main/java/ai/AIStateMachine.java | 21 +++++++++++++++++----
src/main/java/myutil/AIInterface.java | 10 +++++-----
src/main/java/ui/AvatarDesignPanel.java | 7 ++++++-
src/main/java/ui/MainGUI.java | 1 +
src/main/java/ui/window/JFrameAI.java | 20 +++++++++++++++++++-
6 files changed, 49 insertions(+), 14 deletions(-)
diff --git a/src/main/java/ai/AIBlock.java b/src/main/java/ai/AIBlock.java
index 6c23d28356..5780fd4e33 100644
--- a/src/main/java/ai/AIBlock.java
+++ b/src/main/java/ai/AIBlock.java
@@ -73,7 +73,7 @@ public class AIBlock extends AIInteract {
"#Respect: Two connected signals must have " +
"the same list of attributes, even if they are " +
"defined in two different blocks. One of them must be output, the other one must be input" +
- "#Respect: all input signals must have exactly one corresponding output signal, i.e. an ouput signal with the same name" +
+ "#Respect: all input signals must have exactly one corresponding output signal, i.e., an ouput signal with the same name" +
"#Respect: two signals with the same name must be defined in different blocks";
/*"and after " +
"the blocks, add the " +
@@ -90,8 +90,6 @@ public class AIBlock extends AIInteract {
"# A signal must be involved in one connection exactly";*/
-
-
public static String[] KNOWLEDGE_STAGES = {KNOWLEDGE_ON_JSON_FOR_BLOCKS_AND_ATTRIBUTES, KNOWLEDGE_ON_JSON_FOR_BLOCKS_AND_CONNECTIONS};
AvatarSpecification specification;
private String[] QUESTION_IDENTIFY_SYSTEM_BLOCKS = {"From the following system specification, using the specified JSON format, identify the " +
diff --git a/src/main/java/ai/AIStateMachine.java b/src/main/java/ai/AIStateMachine.java
index 12915fa042..cf608d7a3d 100644
--- a/src/main/java/ai/AIStateMachine.java
+++ b/src/main/java/ai/AIStateMachine.java
@@ -44,6 +44,7 @@ import avatartranslator.AvatarBlock;
import avatartranslator.AvatarSpecification;
import avatartranslator.tosysmlv2.AVATAR2SysMLV2;
import myutil.TraceManager;
+import org.apache.batik.anim.timing.Trace;
import java.util.ArrayList;
@@ -125,18 +126,22 @@ public class AIStateMachine extends AIInteract implements AISysMLV2DiagramConten
for(String blockName: blockNames) {
TraceManager.addDev("Handling block: " + blockName);
done = false; cpt = 0;
+ int max = 3;
+
+
questionT = QUESTION_IDENTIFY_STATE_MACHINE[0] + blockName;
- while (!done && cpt < 3) {
+ while (!done && cpt < max) {
done = true;
boolean ok = makeQuestion(questionT);
if (!ok) {
TraceManager.addDev("Make question failed");
}
- if (specification != null) {
+ if (ok && specification != null) {
AvatarBlock b = specification.getBlockWithName(blockName);
if (b != null) {
- ArrayList<String> errors = b.makeStateMachineFromJSON(extractJSON(), cpt == 2);
+ TraceManager.addDev("Making the state machine of " + blockName);
+ ArrayList<String> errors = b.makeStateMachineFromJSON(extractJSON(), cpt == (max - 1));
if ((errors != null) && (errors.size() > 0)) {
done = false;
questionT = "Your answer was not correct because of the following errors:";
@@ -150,9 +155,11 @@ public class AIStateMachine extends AIInteract implements AISysMLV2DiagramConten
} else {
TraceManager.addDev("ERROR: no block named " + blockName);
}
+ } else {
+ TraceManager.addDev("Null specification");
}
- waitIfConditionTrue(!done && cpt < 3);
+ waitIfConditionTrue(!done && cpt < max);
cpt ++;
}
@@ -167,6 +174,12 @@ public class AIStateMachine extends AIInteract implements AISysMLV2DiagramConten
}
public Object applyAnswer(Object input) {
+ TraceManager.addDev("Apply answer in AIState Machine");
+ if (specification == null) {
+ TraceManager.addDev("Null spec");
+ } else {
+ TraceManager.addDev("Non null spec");
+ }
if (input == null) {
return specification;
}
diff --git a/src/main/java/myutil/AIInterface.java b/src/main/java/myutil/AIInterface.java
index 9d162891d7..fc0e46f420 100644
--- a/src/main/java/myutil/AIInterface.java
+++ b/src/main/java/myutil/AIInterface.java
@@ -117,9 +117,9 @@ public class AIInterface {
try {
if (connection == null) {
- TraceManager.addDev("Connecting to " + urlText);
+ //TraceManager.addDev("Connecting to " + urlText);
connection = (HttpURLConnection) new URL(urlText).openConnection();
- TraceManager.addDev("Connection to " + urlText + " is opened");
+ //TraceManager.addDev("Connection to " + urlText + " is opened");
connection.setRequestMethod("POST");
//connection.setRequestProperty("Content-Type", "application/json");
connection.setRequestProperty("Content-Type", "application/json; charset=UTF-8");
@@ -131,7 +131,7 @@ public class AIInterface {
disconnect();
throw new AIInterfaceException(CONNECTION_PB);
}
- TraceManager.addDev("Connection done with key: " + key);
+ //TraceManager.addDev("Connection done with key: " + key);
}
private void disconnect() throws AIInterfaceException {
@@ -157,11 +157,11 @@ public class AIInterface {
for(AIKnowledge aik: knowledge) {
sub = new org.json.JSONObject();
sub.put("role", "user");
- TraceManager.addDev("Putting user knowledge: " + aik.userKnowledge);
+ //TraceManager.addDev("Putting user knowledge: " + aik.userKnowledge);
sub.put("content", aik.userKnowledge);
array.put(sub);
sub = new org.json.JSONObject();
- TraceManager.addDev("Putting assistant knowledge: " + aik.assistantKnowledge);
+ //TraceManager.addDev("Putting assistant knowledge: " + aik.assistantKnowledge);
sub.put("role", "assistant");
sub.put("content", aik.assistantKnowledge);
array.put(sub);
diff --git a/src/main/java/ui/AvatarDesignPanel.java b/src/main/java/ui/AvatarDesignPanel.java
index 9ea54f3eff..d93d369a46 100644
--- a/src/main/java/ui/AvatarDesignPanel.java
+++ b/src/main/java/ui/AvatarDesignPanel.java
@@ -78,6 +78,7 @@ public class AvatarDesignPanel extends TURTLEPanel {
if (_mgui == null) {
//for unit testing only
abdp = new AvatarBDPanel(null, null);
+ tdp = abdp;
return;
}
// Issue #41 Ordering of tabbed panes
@@ -299,7 +300,7 @@ public class AvatarDesignPanel extends TURTLEPanel {
public TGComponent hasCheckableMasterMutex() {
TGComponent tgc, tgctmp;
for (int i = 0; i < panels.size(); i++) {
- tdp = panels.get(i);
+ TDiagramPanel tdp = panels.get(i);
if (tdp instanceof AvatarSMDPanel) {
Iterator<TGComponent> iterator = panels.get(i).getComponentList().listIterator();
while (iterator.hasNext()) {
@@ -318,6 +319,7 @@ public class AvatarDesignPanel extends TURTLEPanel {
public void removeAllMutualExclusionWithMasterMutex() {
TGComponent tgc;
+ TDiagramPanel tdp;
for (int i = 0; i < panels.size(); i++) {
tdp = panels.get(i);
if (tdp instanceof AvatarSMDPanel) {
@@ -332,6 +334,7 @@ public class AvatarDesignPanel extends TURTLEPanel {
public void reinitMutualExclusionStates() {
TGComponent tgc;
+ TDiagramPanel tdp;
for (int i = 0; i < panels.size(); i++) {
tdp = panels.get(i);
if (tdp instanceof AvatarSMDPanel) {
@@ -373,6 +376,7 @@ public class AvatarDesignPanel extends TURTLEPanel {
}
public void resetModelBacktracingProVerif() {
+ TDiagramPanel tdp;
if (abdp == null) {
return;
}
@@ -454,6 +458,7 @@ public class AvatarDesignPanel extends TURTLEPanel {
}
public void modelBacktracingProVerif(ProVerifOutputAnalyzer pvoa) {
+ TDiagramPanel tdp;
if (abdp == null) {
return;
diff --git a/src/main/java/ui/MainGUI.java b/src/main/java/ui/MainGUI.java
index bebaf52c27..8cdba52409 100644
--- a/src/main/java/ui/MainGUI.java
+++ b/src/main/java/ui/MainGUI.java
@@ -8299,6 +8299,7 @@ public class MainGUI implements ActionListener, WindowListener, KeyListener, Per
}
public TDiagramPanel getCurrentMainTDiagramPanel() {
+ TraceManager.addDev("Main selected index:" + mainTabbedPane.getSelectedIndex());
return tabs.elementAt(mainTabbedPane.getSelectedIndex()).tdp;
}
diff --git a/src/main/java/ui/window/JFrameAI.java b/src/main/java/ui/window/JFrameAI.java
index c5a5b1648b..f61d3ed792 100644
--- a/src/main/java/ui/window/JFrameAI.java
+++ b/src/main/java/ui/window/JFrameAI.java
@@ -119,6 +119,8 @@ public class JFrameAI extends JFrame implements ActionListener {
chats = new ArrayList<>();
makeComponents();
+ TraceManager.addDev("Selected TDP = " + mgui.getCurrentMainTDiagramPanel().getClass());
+
}
public void setIcon(ChatData _data, Icon newIcon) {
@@ -144,7 +146,8 @@ public class JFrameAI extends JFrame implements ActionListener {
help();
}
});
- helpPopup.getInputMap(JComponent.WHEN_IN_FOCUSED_WINDOW).put(KeyStroke.getKeyStroke("ESCAPE"), "closeJlabel");
+ helpPopup.getInputMap(JComponent.WHEN_IN_FOCUSED_WINDOW).put(KeyStroke.getKeyStroke("ESCAPE"),
+ "closeJlabel");
helpPopup.getActionMap().put("closeJlabel", new AbstractAction() {
@Override
public void actionPerformed(ActionEvent e) {
@@ -305,6 +308,7 @@ public class JFrameAI extends JFrame implements ActionListener {
}
private void start() {
+ TraceManager.addDev("Start in JFrameAI");
currentChatIndex = answerPane.getSelectedIndex();
ChatData selected = selectedChat();
@@ -315,7 +319,9 @@ public class JFrameAI extends JFrame implements ActionListener {
}
if (chatDataMade) {
+ TraceManager.addDev("chatDataMade in JFameAI");
String selectedClass = AIInteractClass[listOfPossibleActions.getSelectedIndex()];
+ TraceManager.addDev("SelectedClass: " + selectedClass);
selected.aiInteract = ai.AIInteract.getInstance("ai." + selectedClass, selected.aiChatData);
@@ -324,7 +330,10 @@ public class JFrameAI extends JFrame implements ActionListener {
return;
}
+ TraceManager.addDev("Selected aiinteract: " + selected.aiInteract.getClass());
+
if (selected.aiInteract instanceof AIAvatarSpecificationRequired) {
+ TraceManager.addDev("****** AIAvatarSpecificationRequired identified *****");
TDiagramPanel tdp = mgui.getCurrentMainTDiagramPanel();
boolean found = false;
if (tdp instanceof AvatarBDPanel) {
@@ -332,14 +341,22 @@ public class JFrameAI extends JFrame implements ActionListener {
}
if (found) {
+ TraceManager.addDev("BD panel: ok");
boolean ret = mgui.checkModelingSyntax(true);
if (ret) {
+ TraceManager.addDev("****** Syntax checking OK *****");
((AIAvatarSpecificationRequired) (selected.aiInteract)).setAvatarSpecification(mgui.gtm.getAvatarSpecification());
+ } else {
+ TraceManager.addDev("\n\n*****Syntax checking failed: no avatar spec***\n\n");
}
+ } else {
+ TraceManager.addDev("Selected panel is not correct. tdp=" + tdp.getClass());
+ return;
}
}
if (selected.aiInteract instanceof AISysMLV2DiagramContent) {
+ TraceManager.addDev("****** AISysMLV2DiagramContent identified *****");
TDiagramPanel tdp = mgui.getCurrentTDiagramPanel();
String[] validDiagrams = ((AISysMLV2DiagramContent)(selected.aiInteract)).getValidDiagrams();
String className = tdp.getClass().getName();
@@ -413,6 +430,7 @@ public class JFrameAI extends JFrame implements ActionListener {
} else if (selectedChat.aiInteract instanceof ai.AIDesignPropertyIdentification) {
// nothing up to now :-)
} else if (selectedChat.aiInteract instanceof ai.AIStateMachine) {
+ TraceManager.addDev("Applying state machines");
applyIdentifyStateMachines(selectedChat.aiInteract.applyAnswer(null));
} else if (selectedChat.aiInteract instanceof ai.AIAmulet) {
applyMutations();
--
GitLab