diff --git a/src/main/java/cli/Action.java b/src/main/java/cli/Action.java
index d7fcebc2df6b6e94bbfb0153d141039bfd30cedb..2733c8b00c8d2a013e7c9729792cc2c3ff9d6ee5 100644
--- a/src/main/java/cli/Action.java
+++ b/src/main/java/cli/Action.java
@@ -39,7 +39,7 @@
package cli;
-import avatartranslator.AvatarSpecification;
+import avatartranslator.*;
import avatartranslator.directsimulation.AvatarSpecificationSimulation;
import avatartranslator.modelchecker.AvatarModelChecker;
import avatartranslator.modelchecker.CounterexampleQueryReport;
@@ -52,10 +52,16 @@ import common.ConfigurationTTool;
import common.SpecConfigTTool;
import graph.RG;
import launcher.RTLLauncher;
+import launcher.RshClient;
+import launcher.RshClientReader;
import myutil.Conversion;
import myutil.FileUtils;
import myutil.PluginManager;
import myutil.TraceManager;
+import proverifspec.ProVerifOutputAnalyzer;
+import proverifspec.ProVerifOutputListener;
+import proverifspec.ProVerifQueryAuthResult;
+import proverifspec.ProVerifQueryResult;
import tmltranslator.TMLMapping;
import tmltranslator.TMLMappingTextSpecification;
import tmltranslator.TMLModeling;
@@ -64,6 +70,7 @@ import ui.MainGUI;
import ui.avatarinteractivesimulation.AvatarInteractiveSimulationActions;
import ui.avatarinteractivesimulation.JFrameAvatarInteractiveSimulation;
import ui.util.IconManager;
+import ui.window.JDialogProverifVerification;
import ui.window.JDialogSystemCGeneration;
import ui.*;
@@ -86,7 +93,7 @@ import java.util.List;
*
* @author Ludovic APVRILLE
*/
-public class Action extends Command {
+public class Action extends Command implements ProVerifOutputListener {
// Action commands
private final static String NEW = "new";
private final static String OPEN = "open";
@@ -114,6 +121,7 @@ public class Action extends Command {
private final static String DIPLO_LOAD_TMAP = "diplodocus-load-tmap";
private final static String DIPLO_DRAW_TML = "diplodocus-draw-tml";
private final static String DIPLO_DRAW_TMAP = "diplodocus-draw-tmap";
+ private final static String DIPLO_SEC_PROOF = "diplodocus-sec-proof";
private final static String NAVIGATE_PANEL_TO_LEFT = "move-current-panel-to-left";
@@ -138,6 +146,11 @@ public class Action extends Command {
private TMLModeling tmlm;
private TMLMapping tmap;
+ private Map<AvatarPragma, ProVerifQueryResult> results;
+ private ProVerifQueryResult result;
+ private StringBuffer buffer;
+ private ProVerifOutputAnalyzer pvoa;
+
public Action() {
}
@@ -999,6 +1012,82 @@ public class Action extends Command {
}
};
+ // Diplodocus security verfication proverif
+ Command diplodocusSecProof = new Command() {
+ public String getCommand() {
+ return DIPLO_SEC_PROOF;
+ }
+
+ public String getShortCommand() {
+ return "dsp";
+ }
+
+ public String getDescription() {
+ return "Perform security verification over a TMAP specification";
+ }
+
+ public String executeCommand(String command, Interpreter interpreter) {
+
+ String[] commands = command.split(" ");
+ if (commands.length < 1) {
+ return Interpreter.BAD;
+ }
+
+ if (tmap == null) {
+ if (tmlm == null) {
+ return interpreter.TML_NO_SPEC;
+ } else {
+ interpreter.mgui.gtm.setTMLModeling(tmlm);
+ }
+ } else {
+ interpreter.mgui.gtm.setTMLMapping(tmap);
+ }
+
+ try {
+ String pathCode = SpecConfigTTool.ProVerifCodeDirectory;
+ SpecConfigTTool.checkAndCreateProverifDir(pathCode);
+ pathCode += "pvspec";
+ File testFile = new File(pathCode);
+ File dir = testFile.getParentFile();
+
+ if (dir == null || !dir.exists()) {
+ return Interpreter.BAD_DIRECTORY + ": " + pathCode;
+ }
+
+ if (!interpreter.mgui.gtm.generateProVerifFromAVATAR(
+ pathCode,
+ JDialogProverifVerification.REACHABILITY_NONE,
+ false,
+ false,
+ ""+JDialogProverifVerification.LOOP_ITERATION)
+ ) {
+ return interpreter.GEN_FAILED;
+ }
+
+ TraceManager.addDev("Generation ok. Starting ProVerif");
+
+ String cmd = ConfigurationTTool.ProVerifVerifierPath + " in pitype " + pathCode;
+ RshClient rshc = new RshClient("localhost");
+ rshc.setCmd(cmd);
+ rshc.sendExecuteCommandRequest();
+ TraceManager.addDev("Execute command started");
+ RshClientReader reader = rshc.getDataReaderFromProcess();
+
+ pvoa = interpreter.mgui.gtm.getProVerifOutputAnalyzer();
+ TraceManager.addDev("Getting analyzer");
+ pvoa.analyzeOutput(reader, true);
+ buffer = new StringBuffer();
+ pvoa.addListener(Action.this);
+
+ } catch (Exception e) {
+ TraceManager.addDev("Exception during security proof / " + e.getClass() + " / " + e.getMessage());
+ return e.getMessage();
+ }
+
+ return null;
+ }
+ };
+
// PANEL manipulation
@@ -1924,6 +2013,7 @@ public class Action extends Command {
addAndSortSubcommand(diplodocusLoadTMAP);
addAndSortSubcommand(diplodocusDrawTML);
addAndSortSubcommand(diplodocusDrawTMAP);
+ addAndSortSubcommand(diplodocusSecProof);
addAndSortSubcommand(movePanelToTheLeftPanel);
addAndSortSubcommand(movePanelToTheRightPanel);
addAndSortSubcommand(selectPanel);
@@ -1942,4 +2032,113 @@ public class Action extends Command {
}
+ private class ProVerifResultSection {
+ String title;
+ List<AvatarPragma> results;
+ JList<AvatarPragma> jlist;
+
+ ProVerifResultSection(String title, List<AvatarPragma> results) {
+ this.title = title;
+ this.results = results;
+ }
+ }
+
+ @Override
+ public void proVerifOutputChanged() {
+
+ //TraceManager.addDev("Proverif output changed");
+
+ JLabel label;
+ buffer = new StringBuffer();
+
+ if (pvoa.getErrors().size() != 0) {
+ buffer.append("Errors:\n" );
+ for (String error: pvoa.getErrors()) {
+ buffer.append("\tError: " + error);
+
+ }
+ } else {
+ LinkedList<AvatarPragma> reachableEvents = new LinkedList<>();
+ LinkedList<AvatarPragma> nonReachableEvents = new LinkedList<>();
+ LinkedList<AvatarPragma> secretTerms = new LinkedList<>();
+ LinkedList<AvatarPragma> nonSecretTerms = new LinkedList<>();
+ LinkedList<AvatarPragma> satisfiedStrongAuth = new LinkedList<>();
+ LinkedList<AvatarPragma> satisfiedWeakAuth = new LinkedList<>();
+ LinkedList<AvatarPragma> nonSatisfiedAuth = new LinkedList<>();
+ LinkedList<AvatarPragma> nonProved = new LinkedList<>();
+
+ results = pvoa.getResults();
+
+ //
+
+ for (AvatarPragma pragma : this.results.keySet()) {
+ if (pragma instanceof AvatarPragmaReachability) {
+ ProVerifQueryResult r = this.results.get(pragma);
+ if (r.isProved()) {
+ if (r.isSatisfied())
+ reachableEvents.add(pragma);
+ else
+ nonReachableEvents.add(pragma);
+ } else
+ nonProved.add(pragma);
+ } else if (pragma instanceof AvatarPragmaSecret) {
+ ProVerifQueryResult r = this.results.get(pragma);
+ if (r.isProved()) {
+ if (r.isSatisfied())
+ secretTerms.add(pragma);
+ else
+ nonSecretTerms.add(pragma);
+ } else
+ nonProved.add(pragma);
+ } else if (pragma instanceof AvatarPragmaAuthenticity) {
+ ProVerifQueryAuthResult r = (ProVerifQueryAuthResult) this.results.get(pragma);
+ if (!r.isWeakProved()) {
+ nonProved.add(pragma);
+ } else {
+ if (!r.isProved())
+ nonProved.add(pragma);
+ if (r.isProved() && r.isSatisfied())
+ satisfiedStrongAuth.add(pragma);
+ else if (r.isWeakSatisfied())
+ satisfiedWeakAuth.add(pragma);
+ else
+ nonSatisfiedAuth.add(pragma);
+ }
+ }
+ }
+
+ Collection<Action.ProVerifResultSection> sectionsList = new LinkedList<>();
+ Collections.sort(reachableEvents);
+ Collections.sort(nonReachableEvents);
+ Collections.sort(secretTerms);
+ Collections.sort(nonSecretTerms);
+ Collections.sort(satisfiedStrongAuth);
+ Collections.sort(satisfiedWeakAuth);
+ Collections.sort(nonSatisfiedAuth);
+ Collections.sort(nonProved);
+ sectionsList.add(new Action.ProVerifResultSection("Reachable states:", reachableEvents));
+ sectionsList.add(new Action.ProVerifResultSection("Non reachable states:", nonReachableEvents));
+ sectionsList.add(new Action.ProVerifResultSection("Confidential Data:", secretTerms));
+ sectionsList.add(new Action.ProVerifResultSection("Non confidential Data:", nonSecretTerms));
+ sectionsList.add(new Action.ProVerifResultSection("Satisfied Strong Authenticity:", satisfiedStrongAuth));
+ sectionsList.add(new Action.ProVerifResultSection("Satisfied Weak Authenticity:", satisfiedWeakAuth));
+ sectionsList.add(new Action.ProVerifResultSection("Non Satisfied Authenticity:", nonSatisfiedAuth));
+ sectionsList.add(new Action.ProVerifResultSection("Not Proved Queries:", nonProved));
+
+ int y = 0;
+
+ for (Action.ProVerifResultSection section : sectionsList) {
+ if (!section.results.isEmpty()) {
+ buffer.append(section.title + "\n");
+ section.jlist = new JList<>(section.results.toArray(new AvatarPragma[0]));
+ section.jlist.setSelectionMode(ListSelectionModel.SINGLE_SELECTION);
+ section.jlist.setAlignmentX(Component.LEFT_ALIGNMENT);
+ buffer.append("\n" + section.jlist);
+ }
+ }
+ }
+
+ System.out.println(buffer);
+ }
+
}
diff --git a/src/main/java/cli/Interpreter.java b/src/main/java/cli/Interpreter.java
index fbd181963e7a12cc6381b3a48eaeaa5514fb197e..1a34f12185a35da7fa6d68c50520c461fb50d6ba 100644
--- a/src/main/java/cli/Interpreter.java
+++ b/src/main/java/cli/Interpreter.java
@@ -74,11 +74,13 @@ public class Interpreter implements Runnable, TerminalProviderInterface {
public final static String BAD_COMMAND_NAME = "The provided command is invalid";
public final static String ROBOT_EXCEPTION = "Robot could not be started";
public final static String BAD_FILE_NAME = "Unvalid file identifier";
+ public final static String BAD_DIRECTORY = "Unvalid directory identifier";
public final static String BAD_FILE = "Badly formatted file";
public final static String AVATAR_NO_SPEC = "No Avatar specification";
public final static String TML_NO_SPEC = "No TML specification";
public final static String TMAP_NO_SPEC = "No TMAP specification";
public final static String NO_WINDOW = "The targeted window does not exist";
+ public final static String GEN_FAILED = "code generation failed";
private String script;
diff --git a/src/main/java/ui/AvatarDesignPanel.java b/src/main/java/ui/AvatarDesignPanel.java
index 151c5b306d6d2cf4326e955939724c27a47e3a8b..9ea54f3effd984f0d616d6f74609ff9c1357e09f 100644
--- a/src/main/java/ui/AvatarDesignPanel.java
+++ b/src/main/java/ui/AvatarDesignPanel.java
@@ -40,6 +40,7 @@ package ui;
import avatartranslator.*;
import myutil.GraphicLib;
+import myutil.TraceManager;
import proverifspec.ProVerifOutputAnalyzer;
import proverifspec.ProVerifQueryAuthResult;
import proverifspec.ProVerifQueryResult;
@@ -222,6 +223,7 @@ public class AvatarDesignPanel extends TURTLEPanel {
}
public List<TAttribute> getAllAttributes(String _name) {
+ TraceManager.addDev("Getting all attributes of " + _name);
return abdp.getAllAttributesOfBlock(_name);
}
diff --git a/src/main/java/ui/GTURTLEModeling.java b/src/main/java/ui/GTURTLEModeling.java
index 83a96fe95b5c94f5415ad288a8c12910ec5f2a8c..9c46ed3a6a43b78c0e42bca991e5e5dd112f0573 100644
--- a/src/main/java/ui/GTURTLEModeling.java
+++ b/src/main/java/ui/GTURTLEModeling.java
@@ -2706,8 +2706,13 @@ public class GTURTLEModeling {
}
@SuppressWarnings("unchecked")
- public void setTMLMapping(TMLMapping tmap) {
- this.tmap = tmap;
+ public void setTMLMapping(TMLMapping _tmap) {
+ this.tmap = _tmap;
+ }
+
+ @SuppressWarnings("unchecked")
+ public void setTMLModeling(TMLModeling _tmlm) {
+ this.tmlm = _tmlm;
}
public UPPAALSpec getLastUPPAALSpecification() {
@@ -5506,18 +5511,22 @@ public class GTURTLEModeling {
node = diagramNl.item(j);
if (node.getNodeType() == Node.ELEMENT_NODE) {
elt = (Element) node;
- if (elt.getTagName().compareTo("AVATARBlockDiagramPanel") == 0)
- // Class diagram
+ if (elt.getTagName().compareTo("AVATARBlockDiagramPanel") == 0) {
+ // Block diagram
+ TraceManager.addDev("Load avatar bd panel");
loadAvatarBD(elt, indexDesign, keepUUID);
+ }
}
}
for (int j = 0; j < diagramNl.getLength(); j++) {
node = diagramNl.item(j);
if (node.getNodeType() == Node.ELEMENT_NODE) {
elt = (Element) node;
- if (elt.getTagName().compareTo("AVATARStateMachineDiagramPanel") == 0)
+ if (elt.getTagName().compareTo("AVATARStateMachineDiagramPanel") == 0) {
// Managing activity diagrams
+ TraceManager.addDev("Load avatar smd panel");
loadAvatarSMD(elt, indexDesign, keepUUID);
+ }
}
}
@@ -7159,8 +7168,8 @@ public class GTURTLEModeling {
}
}
- public void loadAvatarSMD(TDiagramPanel tdp, String oldValue, String newValue, boolean keepUUID) throws MalformedModelingException {
- TraceManager.addDev("---> Load activity diagram of old=" + oldValue + " new=" + newValue);
+ public void loadAvatarSMD(TDiagramPanel tdp, String oldValue, String newValue, boolean keepUUID, TGComponent originComponent) throws MalformedModelingException {
+ TraceManager.addDev("---> Load SMD of old=" + oldValue + " new=" + newValue);
try {
NodeList smdNl = docCopy.getElementsByTagName("AVATARStateMachineDiagramPanel");
@@ -7224,7 +7233,7 @@ public class GTURTLEModeling {
connectConnectorsToRealPoints(asmdp);
asmdp.structureChanged();
//TraceManager.addDev("Activity diagram : " + tadp.getName() + " post loading");
- makePostLoading(asmdp, 0);
+ makePostLoading(asmdp, 0, originComponent);
}
}
}
@@ -7315,8 +7324,11 @@ public class GTURTLEModeling {
throw new MalformedModelingException();
}
}
-
public void makePostLoading(TDiagramPanel tdp, int beginIndex) throws MalformedModelingException {
+ makePostLoading(tdp, beginIndex, null);
+ }
+
+ public void makePostLoading(TDiagramPanel tdp, int beginIndex, TGComponent originComponent) throws MalformedModelingException {
TGComponent tgc;
//TraceManager.addDev("Post loading of diagram " + tdp.toString());
@@ -7327,7 +7339,7 @@ public class GTURTLEModeling {
tgc = list.get(i);
//TraceManager.addDev(tgc.getName());
//TraceManager.addDev(tgc.getValue());
- tgc.makePostLoading(decId);
+ tgc.makePostLoading(decId, originComponent);
}
// Order components
@@ -7396,6 +7408,7 @@ public class GTURTLEModeling {
//TraceManager.addDev("Component added to diagram tgc=" + tgc);
tdp.addBuiltComponent(tgc);
list.add(tgc);
+
/*if ((zoomV != 1) && (tgc instanceof TGScalableComponent)){
((TGScalableComponent)tgc).forceScale(zoomV);
TraceManager.addDev("myX after =" + tgc.getX());
@@ -7622,6 +7635,7 @@ public class GTURTLEModeling {
tgc = father.getInternalTGComponent(fatherNum);
if (tgc == null) {
+
// To be added to its father -> swallow component
if (father instanceof SwallowTGComponent) {
//TraceManager.addDev("1 Must add the component to its father:");
@@ -7664,8 +7678,12 @@ public class GTURTLEModeling {
throw new MalformedModelingException();
}
+
+
tgc.setIndexU(index);
+ //TraceManager.addDev("Going to set name");
+
if (myName != null) {
tgc.setName(myName);
}
@@ -7692,12 +7710,15 @@ public class GTURTLEModeling {
}
}
+ //TraceManager.addDev("Set enable");
tgc.setEnabled(enable);
/*if (tgc instanceof TCDTObject) {
TraceManager.addDev("Loading " + myValue);
}*/
+
+
String oldClassName = myValue;
//TraceManager.addDev("Old class name=" + oldClassName);
//Added by Solange
@@ -7727,6 +7748,13 @@ public class GTURTLEModeling {
}
}
+ if ((tgc instanceof AvatarBDLibraryFunction) && (decId > 0)) {
+ TraceManager.addDev("Library func");
+ if (tdp.isAlreadyAnAvatarBDBlockName(myValue)) {
+ myValue = tdp.findAvatarBDBlockName(myValue + "_");
+ }
+ }
+
if ((tgc instanceof TMLCPrimitiveComponent) && (decId > 0)) {
if (tdp.isAlreadyATMLPrimitiveComponentName(myValue)) {
myValue = tdp.findTMLPrimitiveComponentName(myValue + "_");
@@ -7739,17 +7767,14 @@ public class GTURTLEModeling {
}
}
//TraceManager.addDev("myValue=" + myValue);
+
tgc.setValueWithChange(myValue);
+
//TraceManager.addDev("value done");
if ((tgc instanceof TCDTClass) && (decId > 0)) {
loadActivityDiagram(tdp, oldClassName, myValue, keepUUID);
}
- if ((tgc instanceof AvatarBDBlock) && (decId > 0)) {
- //TraceManager.addDev("Going to load ad of task " + oldClassName + " myValue=" + myValue);
- loadAvatarSMD(tdp, oldClassName, myValue, keepUUID);
- }
-
if ((tgc instanceof TMLTaskOperator) && (decId > 0)) {
//TraceManager.addDev("Going to load ad of task " + oldClassName + " myValue=" + myValue);
loadTMLActivityDiagram(tdp, oldClassName, myValue, keepUUID);
@@ -7759,11 +7784,20 @@ public class GTURTLEModeling {
//TraceManager.addDev("Going to load ad of component " + oldClassName + " myValue=" + myValue);
loadTMLActivityDiagram(tdp, oldClassName, myValue, keepUUID);
}
+
+
+ if ((tgc instanceof AvatarBDBlock) && (decId > 0)) {
+ TraceManager.addDev("Going to load smd of block " + tgc + " myValue=" + tgc.getValue());
+ loadAvatarSMD(tdp, oldClassName, myValue, keepUUID, tgc);
+ }
+
+
}
//TraceManager.addDev("Laoding component with id="+ myId);
tgc.forceId(myId);
+
if ((uid != null) && (keepUUID)) {
//TraceManager.addDev("Forcing UUID");
tgc.forceUUID(uid);
@@ -7772,6 +7806,20 @@ public class GTURTLEModeling {
tgc.makeUUID();
}
+ //extra param
+ //TraceManager.addDev("Extra params" + tgc.getClass() + " value: " + tgc.getValue());
+ //TraceManager.addDev("My value = " + tgc.getValue());
+ tgc.loadExtraParam(elt1.getElementsByTagName("extraparam"), decX, decY, decId);
+ //TraceManager.addDev("Extra param ok");
+
+ if ((myValue != null) && (!myValue.equals(null))) {
+ if ((tgc instanceof AvatarBDBlock) && (decId > 0)) {
+ TraceManager.addDev("Going to load smd of block " + tgc + " myValue=" + tgc.getValue());
+ loadAvatarSMD(tdp, oldClassName, myValue, keepUUID, tgc);
+ }
+ }
+
+
tgc.setLoaded(true);
tgc.setInternalLoaded(false);
tgc.setMinSize(myMinWidth, myMinHeight);
@@ -7817,11 +7865,7 @@ public class GTURTLEModeling {
tgc.setBreakpoint(breakpoint);
}
- //extra param
- // TraceManager.addDev("Extra params" + tgc.getClass());
- //TraceManager.addDev("My value = " + tgc.getValue());
- tgc.loadExtraParam(elt1.getElementsByTagName("extraparam"), decX, decY, decId);
- //TraceManager.addDev("Extra param ok");
+
//#issue 82
if ((myValue != null) && (!myValue.equals("null"))) {
@@ -7868,6 +7912,9 @@ public class GTURTLEModeling {
TraceManager.addDev("getValue " + tgc.getValue());
}*/
+ //TraceManager.addDev("All done for component " + tgc.getClass().toString());
+
+
} catch (Exception e) {
TraceManager.addError("Exception XML Component " + e.getMessage() + "trace=" + e.getStackTrace());
throw new MalformedModelingException(e);
diff --git a/src/main/java/ui/MainGUI.java b/src/main/java/ui/MainGUI.java
index bb8f0979be24676aaba75d86ec4282a449649869..390805d324afb6178b6fa1df99a2a22308e8efb0 100644
--- a/src/main/java/ui/MainGUI.java
+++ b/src/main/java/ui/MainGUI.java
@@ -4450,10 +4450,12 @@ public class MainGUI implements ActionListener, WindowListener, KeyListener, Per
public List<TAttribute> getAllAttributes(TURTLEPanel tp, String name) {
if (tp == null) {
+ TraceManager.addDev("Null tp");
return null;
}
if (!(tp instanceof AvatarDesignPanel)) {
+ TraceManager.addDev("Not an AVATAR Design panel");
return null;
}
AvatarDesignPanel adp = (AvatarDesignPanel) tp;
diff --git a/src/main/java/ui/TDiagramPanel.java b/src/main/java/ui/TDiagramPanel.java
index ee73157364ae72b98e4af5e72c3273260aaab4a0..cd81a71912f4d8354b05e336f1475facd4022d0a 100644
--- a/src/main/java/ui/TDiagramPanel.java
+++ b/src/main/java/ui/TDiagramPanel.java
@@ -4308,6 +4308,8 @@ public abstract class TDiagramPanel extends JPanel implements GenericTree {
tgc.searchForText(text, elements);
}
+
+
public MainGUI getMainGUI() { //Ajout CD pour creation d'un panel depuis un block
return mgui;
}
diff --git a/src/main/java/ui/TGComponent.java b/src/main/java/ui/TGComponent.java
index ccaeff929e44c144de8940fbd7695ab3ef73bf7f..d7569bb5fb0d28296791f3850eb9439652b48a44 100644
--- a/src/main/java/ui/TGComponent.java
+++ b/src/main/java/ui/TGComponent.java
@@ -3551,15 +3551,19 @@ public abstract class TGComponent extends AbstractCDElement implements /*CDEleme
return;
}
- public final void makePostLoading(int decId) throws MalformedModelingException {
+ public final void makePostLoading(int decId, TGComponent originComponent) throws MalformedModelingException {
//TraceManager.addDev("Make post loading of " + getName());
- postLoading(decId);
+ postLoading(decId, originComponent);
for (int i = 0; i < nbInternalTGComponent; i++) {
- tgcomponent[i].postLoading(decId);
+ tgcomponent[i].postLoading(decId, originComponent);
}
}
- public void postLoading(int decId) throws MalformedModelingException {
+ public final void makePostLoading(int decId) throws MalformedModelingException {
+ makePostLoading(decId, null);
+ }
+
+ public void postLoading(int decId, TGComponent originComponent) throws MalformedModelingException {
}
public void resetVerificationResults() {
diff --git a/src/main/java/ui/avatarbd/AvatarBDBlock.java b/src/main/java/ui/avatarbd/AvatarBDBlock.java
index 149dcc36be253d996f5f6b3b788f1a7ae9b662cb..f44fa7ee988ce28e2c5815d65fb66aa82b5da841 100644
--- a/src/main/java/ui/avatarbd/AvatarBDBlock.java
+++ b/src/main/java/ui/avatarbd/AvatarBDBlock.java
@@ -1177,6 +1177,8 @@ public class AvatarBDBlock extends TGCScalableWithInternalComponent implements S
String s;
String tmpGlobalCode = "";
+ TraceManager.addDev("Loading attributes of block " + getBlockName());
+
try {
NodeList nli;
Node n1, n2;
diff --git a/src/main/java/ui/avatarbd/AvatarBDInterface.java b/src/main/java/ui/avatarbd/AvatarBDInterface.java
index 0d73c3ef0ab52230dffa8a698064ea0ffa51a6d3..0521ef9db9f58de1b656c415bf5db66d98a3c98a 100644
--- a/src/main/java/ui/avatarbd/AvatarBDInterface.java
+++ b/src/main/java/ui/avatarbd/AvatarBDInterface.java
@@ -69,7 +69,8 @@ import java.util.List;
* @author Ludovic APVRILLE
* @version 1.1 06/04/2010
*/
-public class AvatarBDInterface extends TGCScalableWithInternalComponent implements SwallowTGComponent, SwallowedTGComponent, GenericTree, AvatarBDStateMachineOwner, WithAttributes {
+public class AvatarBDInterface extends TGCScalableWithInternalComponent implements SwallowTGComponent, SwallowedTGComponent, GenericTree,
+ AvatarBDStateMachineOwner, WithAttributes {
private static String GLOBAL_CODE_INFO = "(block code)";
@@ -974,6 +975,22 @@ public class AvatarBDInterface extends TGCScalableWithInternalComponent implemen
return true;
}
+ public boolean hasInternalBlockWithName(String name) {
+ if (getValue().equals(name)) {
+ return true;
+ }
+ TGComponent tgc;
+ for(int i=0; i<getNbInternalTGComponent(); i++) {
+ tgc = getInternalTGComponent(i);
+ if (tgc instanceof AvatarBDStateMachineOwner) {
+ boolean b = ((AvatarBDStateMachineOwner)tgc).hasInternalBlockWithName(name);
+ if (b)
+ return b;
+ }
+ }
+ return false;
+ }
+
protected void setJDialogOptions(JDialogAvatarInterface _jdab) {
//jda.addAccess(TAttribute.getStringAccess(TAttribute.PUBLIC));
_jdab.addAccess(TAttribute.getStringAccess(TAttribute.PRIVATE));
diff --git a/src/main/java/ui/avatarbd/AvatarBDLibraryFunction.java b/src/main/java/ui/avatarbd/AvatarBDLibraryFunction.java
index 668803a51ac3b897e3a3aef85b47a9d478d90af3..025dc1d87e2d335f41f963a5053ec10b210a28b0 100644
--- a/src/main/java/ui/avatarbd/AvatarBDLibraryFunction.java
+++ b/src/main/java/ui/avatarbd/AvatarBDLibraryFunction.java
@@ -61,7 +61,8 @@ import java.util.LinkedList;
* @author Florian LUGOU
* @version 1.0 04.08.2016
*/
-public class AvatarBDLibraryFunction extends TGCScalableWithoutInternalComponent implements SwallowedTGComponent, AvatarBDStateMachineOwner, Comparable<AvatarBDLibraryFunction> {
+public class AvatarBDLibraryFunction extends TGCScalableWithoutInternalComponent implements SwallowedTGComponent, AvatarBDStateMachineOwner,
+ Comparable<AvatarBDLibraryFunction> {
/**
* Stereotype for standard library function.
@@ -192,8 +193,12 @@ public class AvatarBDLibraryFunction extends TGCScalableWithoutInternalComponent
this.removable = true;
this.userResizable = true;
+
+ name = tdp.findAvatarBDBlockName("LibraryFunction");
+ setValue(name);
+
// Find a new unused name
- int i;
+ /*int i;
for (i = 0; i < 100; i++) {
String tmpName = "LibraryFunction" + i;
if (this.tdp.isAvatarBlockNameUnique(tmpName) &&
@@ -205,7 +210,7 @@ public class AvatarBDLibraryFunction extends TGCScalableWithoutInternalComponent
}
if (i == 100) {
// TODO: throw exception
- }
+ }*/
this.oldScaleFactor = this.tdp.getZoom();
this.currentFontSize = (int) (AvatarBDLibraryFunction.maxFontSize * this.oldScaleFactor);
@@ -929,6 +934,10 @@ public class AvatarBDLibraryFunction extends TGCScalableWithoutInternalComponent
return ((AvatarDesignPanel) (this.tdp.tp)).getAvatarSMDPanel(this.value);
}
+ public boolean hasInternalBlockWithName(String name) {
+ return false;
+ }
+
/**
* Removes the cryptographic primitives from the list of methods.
*/
diff --git a/src/main/java/ui/avatarbd/AvatarBDPanel.java b/src/main/java/ui/avatarbd/AvatarBDPanel.java
index a46582f4c1eaf1eb7f419819f35a90c962045bc7..d387d5bc55de699b466f5d43fcc1e0b18fa165a0 100644
--- a/src/main/java/ui/avatarbd/AvatarBDPanel.java
+++ b/src/main/java/ui/avatarbd/AvatarBDPanel.java
@@ -530,7 +530,7 @@ public class AvatarBDPanel extends TDiagramPanel {
return v;
}
- //ajoute DG 27.02.: Interfcae signals treated as block signals to avoid too many case distinctions - is this possible ?
+ //ajoute DG 27.02.: Interface signals treated as block signals to avoid too many case distinctions - is this possible ?
public List<AvatarSignal> getListOfAvailableSignals(AvatarBDInterface _block) {
List<AvatarSignal> v = new LinkedList<AvatarSignal> ();
diff --git a/src/main/java/ui/avatarbd/AvatarBDStateMachineOwner.java b/src/main/java/ui/avatarbd/AvatarBDStateMachineOwner.java
index 13b68cefd465fb4d00b24ab12f72c5be5aacfb45..58cb93e2627ca3d4061e4de42c8fd51d4d270581 100755
--- a/src/main/java/ui/avatarbd/AvatarBDStateMachineOwner.java
+++ b/src/main/java/ui/avatarbd/AvatarBDStateMachineOwner.java
@@ -66,4 +66,8 @@ public interface AvatarBDStateMachineOwner {
String getOwnerName();
AvatarSMDPanel getAvatarSMDPanel();
+
+ String getValue();
+ boolean hasInternalBlockWithName(String name);
+
}
diff --git a/src/main/java/ui/avatarsmd/AvatarSMDLibraryFunctionCall.java b/src/main/java/ui/avatarsmd/AvatarSMDLibraryFunctionCall.java
index b54ebd5aa2f38536d5b9434fb3e9a7903230d4bc..6f67c533367389b6c247e85b2c95aed7252a7224 100644
--- a/src/main/java/ui/avatarsmd/AvatarSMDLibraryFunctionCall.java
+++ b/src/main/java/ui/avatarsmd/AvatarSMDLibraryFunctionCall.java
@@ -39,11 +39,14 @@
package ui.avatarsmd;
import myutil.GraphicLib;
+import myutil.TraceManager;
import org.w3c.dom.Element;
import org.w3c.dom.Node;
import org.w3c.dom.NodeList;
import ui.*;
+import ui.avatarbd.AvatarBDBlock;
import ui.avatarbd.AvatarBDLibraryFunction;
+import ui.avatarbd.AvatarBDStateMachineOwner;
import ui.util.IconManager;
import ui.window.JDialogSMDLibraryFunctionCall;
@@ -61,12 +64,16 @@ import java.util.List;
public class AvatarSMDLibraryFunctionCall extends AvatarSMDBasicCanBeDisabledComponent /* Issue #69 TGCScalableWithoutInternalComponent*/ implements BasicErrorHighlight {
private List<TAttribute> parameters;
+ private List<String> parametersS;
private List<AvatarSignal> signals;
+ private List<String> signalsS;
private List<TAttribute> returnAttributes;
+ private List<String>returnAttributesS;
private AvatarBDLibraryFunction libraryFunction;
+ private String libraryFunctionS;
private static int lineLength = 5;
private static int paddingHorizontal = 5;
@@ -330,6 +337,12 @@ public class AvatarSMDLibraryFunctionCall extends AvatarSMDBasicCanBeDisabledCom
@Override
public void loadExtraParam (NodeList nl, int decX, int decY, int decId) throws MalformedModelingException {
+ parametersS = new LinkedList<>();
+ returnAttributesS = new LinkedList<>();
+ signals = new LinkedList<>();
+ libraryFunctionS = null;
+
+
try {
for(int i=0; i<nl.getLength(); i++) {
Node n1 = nl.item(i);
@@ -354,55 +367,65 @@ public class AvatarSMDLibraryFunctionCall extends AvatarSMDBasicCanBeDisabledCom
switch (elt.getTagName ()) {
case "LibraryFunction": {
+
if (this.libraryFunction != null) {
throw new MalformedModelingException ();
}
- String name = elt.getAttribute ("name");
- if (name.equals ("null"))
+ String nameOfLib = elt.getAttribute ("name");
+ TraceManager.addDev("Library function: " + nameOfLib);
+ if (nameOfLib.equals ("null"))
break;
- for (AvatarBDLibraryFunction func: mgui.getAllLibraryFunctions (tp, tdpName))
- if (func.getFullyQualifiedName ().equals (name)) {
+ libraryFunctionS = nameOfLib;
+
+ /*for (AvatarBDLibraryFunction func: mgui.getAllLibraryFunctions (tp, tdpName))
+ if (func.getFullyQualifiedName ().equals (nameOfLib)) {
this.libraryFunction = func;
break;
}
if (this.libraryFunction == null) {
+ TraceManager.addDev("No library function named: " + nameOfLib);
throw new MalformedModelingException ();
- }
+ }*/
break;
}
case "Parameter": {
String name = elt.getAttribute ("id");
if (name.equals ("null")) {
- this.parameters.add (null);
break;
+ } else {
+ this.parametersS.add(name);
}
- boolean found = false;
- for (TAttribute attr: mgui.getAllAttributes (tp, tdpName))
- if (attr.getId ().equals (name)) {
- this.parameters.add (attr);
+ /*boolean found = false;
+ for (TAttribute attr: mgui.getAllAttributes (tp, tdpName)) {
+ TraceManager.addDev("Parameter: " + attr.getId());
+ if (attr.getId().equals(name)) {
+ this.parameters.add(attr);
found = true;
break;
}
+ }
if (!found) {
+ TraceManager.addDev("Parameter " + name + " not found in library function ");
throw new MalformedModelingException ();
- }
+ }*/
break;
}
case "Signal": {
String value = elt.getAttribute ("value");
if (value.equals ("null")) {
- this.signals.add (null);
break;
+ } else {
+ signalsS.add(value);
}
- boolean found = false;
+ /*boolean found = false;
for (AvatarSignal signal: mgui.getAllSignals (tp, tdpName))
if (signal.toString ().equals (value)) {
this.signals.add (signal);
@@ -412,18 +435,19 @@ public class AvatarSMDLibraryFunctionCall extends AvatarSMDBasicCanBeDisabledCom
if (!found) {
throw new MalformedModelingException ();
- }
+ }*/
break;
}
case "ReturnAttribute": {
String name = elt.getAttribute ("id");
if (name.equals ("null")) {
- this.returnAttributes.add (null);
break;
+ } else {
+ this.returnAttributesS.add(name);
}
- boolean found = false;
+ /*boolean found = false;
for (TAttribute attr: mgui.getAllAttributes (tp, tdpName))
if (attr.getId ().equals (name)) {
this.returnAttributes.add (attr);
@@ -432,8 +456,9 @@ public class AvatarSMDLibraryFunctionCall extends AvatarSMDBasicCanBeDisabledCom
}
if (!found) {
+ TraceManager.addDev("Return attribute " + name + " not found in library function ");
throw new MalformedModelingException ();
- }
+ }*/
break;
}
}
@@ -455,6 +480,131 @@ public class AvatarSMDLibraryFunctionCall extends AvatarSMDBasicCanBeDisabledCom
}
+ @Override
+ public void postLoading(int decId, TGComponent originComponent) throws MalformedModelingException {
+
+ TraceManager.addDev("Post loading of AvatarSMDLibraryFunctionCall");
+
+
+ MainGUI mgui = this.tdp.getMGUI ();
+ TURTLEPanel tp = mgui.getCurrentTURTLEPanel ();
+ String tdpName = this.tdp.getName ();
+
+ boolean error = false ;
+
+ for(String s: parametersS) {
+ TraceManager.addDev("Handling parameterS: " + s);
+ boolean found = false;
+ List<TAttribute> listOfAttributes;
+ if ( (originComponent != null) && (originComponent instanceof AvatarBDStateMachineOwner)) {
+ listOfAttributes = ((AvatarBDStateMachineOwner)originComponent).getAttributeList();
+ } else {
+ listOfAttributes = mgui.getAllAttributes (tp, tdpName);
+ }
+
+ for (TAttribute attr : listOfAttributes) {
+ //TraceManager.addDev("Parameter: " + attr.getId());
+ if (attr.getId().equals(s)) {
+ this.parameters.add(attr);
+ found = true;
+ break;
+ }
+ }
+
+ if (!found) {
+ TraceManager.addDev("ERROR. Parameter " + s + " not found");
+ error = true;
+ }
+ }
+ parametersS = null;
+
+ for(String s: returnAttributesS) {
+ TraceManager.addDev("Handling returnAttributesS: " + s);
+ boolean found = false;
+ List<TAttribute> listOfAttributes;
+ if ( (originComponent != null) && (originComponent instanceof AvatarBDStateMachineOwner)) {
+ listOfAttributes = ((AvatarBDStateMachineOwner)originComponent).getAttributeList();
+ } else {
+ listOfAttributes = mgui.getAllAttributes (tp, tdpName);
+ }
+ for (TAttribute attr : listOfAttributes) {
+ //TraceManager.addDev("Parameter: " + attr.getId());
+ if (attr.getId().equals(s)) {
+ this.returnAttributes.add(attr);
+ found = true;
+ break;
+ }
+ }
+ if (!found) {
+ TraceManager.addDev("ERROR. Return parameter " + s + " not found");
+ error = true;
+ }
+
+ }
+
+ returnAttributesS = null;
+ TraceManager.addDev("returnAttributesS nullified ");
+
+ if (signalsS != null) {
+ for (String s : signalsS) {
+ TraceManager.addDev("Handling signalsS: " + s);
+ boolean found = false;
+ List<AvatarSignal> listOfSignals;
+ if ( (originComponent != null) && (originComponent instanceof AvatarBDStateMachineOwner)) {
+ listOfSignals = ((AvatarBDStateMachineOwner)originComponent).getAllSignalList();
+ } else {
+ listOfSignals = mgui.getAllSignals (tp, tdpName);
+ }
+ for (AvatarSignal signal: listOfSignals) {
+ TraceManager.addDev("Signal: " + signal.getId());
+ if (signal.toString().equals(s)) {
+ this.signals.add(signal);
+ found = true;
+ break;
+ }
+ }
+ if (!found) {
+ TraceManager.addDev("ERROR. Signal " + s + " not found");
+ error = true;
+ }
+ }
+ }
+
+ signalsS = null;
+ TraceManager.addDev("signalsS nullified ");
+
+ if (libraryFunctionS != null) {
+ TraceManager.addDev("Handling AvatarBDLibraryFunction: " + libraryFunctionS);
+ for (AvatarBDLibraryFunction func : mgui.getAllLibraryFunctions(tp, tdpName)) {
+ TraceManager.addDev("comparing " + func.getFullyQualifiedName() + " with " + libraryFunctionS);
+ if (func.getFullyQualifiedName().equals(libraryFunctionS)) {
+ this.libraryFunction = func;
+ break;
+ }
+ }
+
+ if (this.libraryFunction == null) {
+ TraceManager.addDev("ERROR. No library function named: " + libraryFunctionS);
+ error = true;
+ } else {
+ TraceManager.addDev("Library function found: " + libraryFunctionS);
+ }
+ } else {
+ TraceManager.addDev("ERROR. No library function defined");
+ error = true;
+ }
+
+ libraryFunctionS = null;
+ TraceManager.addDev("libraryFunctionS nullified ");
+
+
+ if (error) {
+ TraceManager.addDev("Error found in postloading of AvatarSMDLibraryFunctionCall");
+ // throw new MalformedModelingException ();
+ }
+
+ }
+
@Override
public int getType() {
return TGComponentManager.AVATARSMD_LIBRARY_FUNCTION_CALL;
diff --git a/src/main/java/ui/window/JDialogProverifVerification.java b/src/main/java/ui/window/JDialogProverifVerification.java
index 9a172e77e9f86f64a5ab6dbdd75399e901e38cdc..fa536e55905f38783b5d6b02b54d85820a532c0b 100644
--- a/src/main/java/ui/window/JDialogProverifVerification.java
+++ b/src/main/java/ui/window/JDialogProverifVerification.java
@@ -136,7 +136,7 @@ public class JDialogProverifVerification extends JDialog implements ActionListen
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;
+ public static int LOOP_ITERATION = 1;
private static boolean DRAW_AVATAR = false;
@@ -932,8 +932,6 @@ public class JDialogProverifVerification extends JDialog implements ActionListen
}
-
-
String cmd = exe2.getText().trim();
if (this.typedLanguage.isSelected()) {