diff --git a/build.txt b/build.txt
index 8d615eed3a175de51e1a6c4002f8b17d7d23877a..2b5ca6b5d414ec8805225eba6d78e389e37dd921 100644
--- a/build.txt
+++ b/build.txt
@@ -1 +1 @@
-12244
\ No newline at end of file
+12248
\ No newline at end of file
diff --git a/src/avatartranslator/AvatarPragma.java b/src/avatartranslator/AvatarPragma.java
index 81258520b711992d47515f2d66ca46544ff61186..ebb5856f83059d5781adb0ed6ccba775dc07c27b 100644
--- a/src/avatartranslator/AvatarPragma.java
+++ b/src/avatartranslator/AvatarPragma.java
@@ -51,7 +51,7 @@ import ui.avatarbd.AvatarBDPragma;
import java.util.*;
-public abstract class AvatarPragma extends AvatarElement {
+public abstract class AvatarPragma extends AvatarElement implements Comparable<AvatarPragma> {
public static final String[] PRAGMAS = {"Confidentiality", "Secret", "SecrecyAssumption", "InitialSystemKnowledge", "InitialSessionKnowledge", "Authenticity", "PrivatePublicKeys", "Public", "PublicConstant", "PrivateConstant"};
public static final String[] PRAGMAS_TRANSLATION = {"Secret", "Secret", "SecrecyAssumption", "InitialSystemKnowledge", "InitialSessionKnowledge", "Authenticity", "PrivatePublicKeys", "Public", "PublicConstant", "PrivateConstant"};
@@ -423,4 +423,10 @@ public abstract class AvatarPragma extends AvatarElement {
* @return A full clone of the pragma.
*/
public abstract AvatarPragma advancedClone(AvatarSpecification avspec);
+
+ @Override
+ public int compareTo(AvatarPragma b)
+ {
+ return this.toString().compareTo(b.toString());
+ }
}
diff --git a/src/launcher/ExecutionThread.java b/src/launcher/ExecutionThread.java
index 0539ded983944d7eaedb12701256cdbc06a79039..729bd96c2052cd891844496faf258e03e46e3101 100755
--- a/src/launcher/ExecutionThread.java
+++ b/src/launcher/ExecutionThread.java
@@ -311,13 +311,13 @@ class ExecutionThread extends Thread {
return;
}
- TraceManager.addDev("Going to start command " + cmd + "..." );
+ // TraceManager.addDev("Going to start command " + cmd + "..." );
final PrintStream out = new PrintStream( s.getOutputStream(), true );
proc = Runtime.getRuntime().exec(cmd);
if ( parentExecThread != null ) {
- TraceManager.addDev( "Giving my pipe to the other..." );
+ // TraceManager.addDev( "Giving my pipe to the other..." );
parentExecThread.setMyPipe( proc.getOutputStream() );
}
@@ -326,7 +326,7 @@ class ExecutionThread extends Thread {
//TraceManager.addDev("Reading the output stream of the process " + cmd);
while ( go && ( str = proc_in.readLine() ) != null ) {
- TraceManager.addDev( "Sending " + str + " from " + port + " to client..." );
+ // TraceManager.addDev( "Sending " + str + " from " + port + " to client..." );
respond( out, ResponseCode.PROCESS_OUTPUT, str );
}
diff --git a/src/launcher/RshClient.java b/src/launcher/RshClient.java
index 940342710b258a3721945c128d7981ccf36e7b2e..5435952982163248dd87ced7e62acf91f2732c89 100755
--- a/src/launcher/RshClient.java
+++ b/src/launcher/RshClient.java
@@ -318,6 +318,15 @@ public class RshClient {
}
}
+ public RshClientReader getDataReaderFromProcess() throws LauncherException {
+ Socket socket = connect(portString);
+ try {
+ return new RshClientReader(socket);
+ } catch(IOException e) {
+ throw new LauncherException(IO_ERROR, e);
+ }
+ }
+
public void writeCommandMessages( final Writer output )
throws LauncherException {
diff --git a/src/launcher/RshClientReader.java b/src/launcher/RshClientReader.java
new file mode 100755
index 0000000000000000000000000000000000000000..d4c1785ba4689b05f36853f9668817467c738163
--- /dev/null
+++ b/src/launcher/RshClientReader.java
@@ -0,0 +1,178 @@
+/* Copyright or (C) or Copr. GET / ENST, Telecom-Paris, Ludovic Apvrille
+ *
+ * ludovic.apvrille AT enst.fr
+ *
+ * This software is a computer program whose purpose is to allow the
+ * edition of TURTLE analysis, design and deployment diagrams, to
+ * allow the generation of RT-LOTOS or Java code from this diagram,
+ * and at last to allow the analysis of formal validation traces
+ * obtained from external tools, e.g. RTL from LAAS-CNRS and CADP
+ * from INRIA Rhone-Alpes.
+ *
+ * This software is governed by the CeCILL license under French law and
+ * abiding by the rules of distribution of free software. You can use,
+ * modify and/ or redistribute the software under the terms of the CeCILL
+ * license as circulated by CEA, CNRS and INRIA at the following URL
+ * "http://www.cecill.info".
+ *
+ * As a counterpart to the access to the source code and rights to copy,
+ * modify and redistribute granted by the license, users are provided only
+ * with a limited warranty and the software's author, the holder of the
+ * economic rights, and the successive licensors have only limited
+ * liability.
+ *
+ * In this respect, the user's attention is drawn to the risks associated
+ * with loading, using, modifying and/or developing or reproducing the
+ * software by the user in light of its specific status of free software,
+ * that may mean that it is complicated to manipulate, and that also
+ * therefore means that it is reserved for developers and experienced
+ * professionals having in-depth computer knowledge. Users are therefore
+ * encouraged to load and test the software's suitability as regards their
+ * requirements in conditions enabling the security of their systems and/or
+ * data to be ensured and, more generally, to use and operate it in the
+ * same conditions as regards security.
+ *
+ * The fact that you are presently reading this means that you have had
+ * knowledge of the CeCILL license and that you accept its terms.
+ */
+
+package launcher;
+
+import java.io.Reader;
+import java.io.PipedInputStream;
+import java.io.PipedOutputStream;
+import java.io.InputStreamReader;
+import java.io.IOException;
+
+import java.net.Socket;
+import java.net.SocketTimeoutException;
+
+/**
+ * Class RshClientReader
+ * Creation: 03/06/2017
+ * @version 1 03/06/2017
+ * @author Florian LUGOU
+ */
+public class RshClientReader extends Reader implements Runnable {
+
+ private PipedOutputStream pos;
+ private InputStreamReader pis;
+ private Socket clientSocket;
+
+ private Thread forwardingThread;
+ private boolean go = true;
+ private StringBuilder builder;
+ private boolean isNewLine = true;
+
+ public RshClientReader(Socket clientSocket) throws IOException {
+ this.clientSocket = clientSocket;
+ this.pos = new PipedOutputStream();
+ this.pis = new InputStreamReader(new PipedInputStream(pos));
+ this.forwardingThread = new Thread(this);
+ try {
+ this.forwardingThread.start();
+ } catch (IllegalThreadStateException e) {}
+ }
+
+ private void consumeOldLine(String s) throws IOException
+ {
+ int n = s.indexOf('\n');
+ if (n >= 0) {
+ this.pos.write(s.substring(0, n+1).getBytes());
+ this.pos.flush();
+ isNewLine = true;
+ this.consumeNewLine(s.substring(n+1));
+ } else {
+ this.pos.write(s.getBytes());
+ this.pos.flush();
+ }
+ }
+
+ private void consumeNewLine(String s) throws IOException
+ {
+ ResponseCode code = SocketComHelper.responseCode(s);
+
+ if (code == ResponseCode.PROCESS_END) {
+ this.go = false;
+ }
+
+ else if (code == null) {
+ this.builder.append(s);
+ }
+
+ else {
+ s = SocketComHelper.message(code, s);
+
+ this.isNewLine = false;
+ this.consumeOldLine(s);
+ }
+ }
+
+ @Override
+ public void run()
+ {
+ this.builder = new StringBuilder();
+ try {
+ this.clientSocket.setSoTimeout(100);
+ InputStreamReader socketReader = new InputStreamReader(this.clientSocket.getInputStream());
+ try {
+ while(this.go)
+ {
+ char[] cbuf = new char[50];
+ int n = 0;
+ try {
+ n = socketReader.read(cbuf);
+ if (n < 0)
+ break;
+ } catch(SocketTimeoutException e) {
+ if (n > 0)
+ this.builder.append(cbuf, 0, n);
+ continue;
+ }
+
+ this.builder.append(cbuf, 0, n);
+ String s = this.builder.toString();
+ this.builder = new StringBuilder();
+ if (isNewLine)
+ {
+ this.consumeNewLine(s);
+ }
+ else
+ {
+ this.consumeOldLine(s);
+ }
+ }
+ } catch(IOException e) {
+ } finally {
+ try {
+ socketReader.close();
+ } catch(IOException e) {}
+ try {
+ this.pos.close();
+ } catch(IOException e) {}
+ }
+ } catch(IOException e) {
+ } finally {
+ try {
+ this.clientSocket.close();
+ } catch(IOException e) {}
+ }
+ }
+
+ @Override
+ public int read(char[] cbuf, int off, int len) throws IOException
+ {
+ int n = this.pis.read(cbuf, off, len);
+ return n;
+ }
+
+ @Override
+ public void close() throws IOException
+ {
+ this.go = false;
+
+ try {
+ this.pis.close();
+ } catch(IOException e) {}
+ }
+}
diff --git a/src/proverifspec/ProVerifOutputAnalyzer.java b/src/proverifspec/ProVerifOutputAnalyzer.java
index 70c0eb9dcd8c639c80c74c40ed21f274ec1f8327..b988bdf830e7b9bbc0636675a2151ee45edff2c1 100644
--- a/src/proverifspec/ProVerifOutputAnalyzer.java
+++ b/src/proverifspec/ProVerifOutputAnalyzer.java
@@ -48,10 +48,12 @@ package proverifspec;
import avatartranslator.*;
import avatartranslator.toproverif.AVATAR2ProVerif;
+import java.io.Reader;
import java.io.BufferedReader;
import java.io.IOException;
-import java.io.StringReader;
import java.util.HashMap;
+import java.util.Map;
+import java.util.concurrent.ConcurrentHashMap;
import java.util.LinkedList;
import java.util.List;
import java.util.regex.Matcher;
@@ -80,19 +82,38 @@ public class ProVerifOutputAnalyzer {
private final static String untypedAuthSplit = "==> evinj:authenticity" + AVATAR2ProVerif.ATTR_DELIM;
private final static String untypedWeakAuthSplit = "==> ev:authenticity" + AVATAR2ProVerif.ATTR_DELIM;
- private HashMap<AvatarPragma, ProVerifQueryResult> results;
+ private ConcurrentHashMap<AvatarPragma, ProVerifQueryResult> results;
private LinkedList<String> errors;
+ private LinkedList<ProVerifOutputListener> listeners;
+
private AVATAR2ProVerif avatar2proverif;
public ProVerifOutputAnalyzer(AVATAR2ProVerif avatar2proverif) {
this.avatar2proverif = avatar2proverif;
this.errors = null;
this.results = null;
+ this.listeners = new LinkedList<>();
+ }
+
+ public void addListener(ProVerifOutputListener listener)
+ {
+ this.listeners.add(listener);
+ }
+
+ public void removeListener(ProVerifOutputListener listener)
+ {
+ this.listeners.remove(listener);
+ }
+
+ private void notifyListeners()
+ {
+ for (ProVerifOutputListener listener: this.listeners)
+ listener.proVerifOutputChanged();
}
- public void analyzeOutput(String _s, boolean isTyped) {
- BufferedReader reader = new BufferedReader(new StringReader(_s));
+ public void analyzeOutput(Reader reader, boolean isTyped) {
+ BufferedReader bReader = new BufferedReader(reader);
List<AvatarPragma> pragmas = this.avatar2proverif.getAvatarSpecification().getPragmas();
String previous = null;
String str;
@@ -101,7 +122,7 @@ public class ProVerifOutputAnalyzer {
ProVerifResultTrace resultTrace = new ProVerifResultTrace(proverifProcess);
boolean isInTrace = false;
- this.results = new HashMap<AvatarPragma, ProVerifQueryResult> ();
+ this.results = new ConcurrentHashMap<AvatarPragma, ProVerifQueryResult> ();
this.errors = new LinkedList<String>();
Pattern procPattern = Pattern.compile(" *\\{\\d+\\}(.*)");
@@ -109,7 +130,7 @@ public class ProVerifOutputAnalyzer {
try {
// Loop through every line in the output
- while ((str = reader.readLine()) != null)
+ while ((str = bReader.readLine()) != null)
{
if (str.isEmpty())
continue;
@@ -194,6 +215,7 @@ public class ProVerifOutputAnalyzer {
if (reachabilityPragma != null)
{
this.results.put(reachabilityPragma, result);
+ this.notifyListeners();
}
}
@@ -226,6 +248,7 @@ public class ProVerifOutputAnalyzer {
if (trueName != null && trueName.equals(attributeName))
{
this.results.put(pragma, result);
+ this.notifyListeners();
}
}
}
@@ -306,6 +329,7 @@ public class ProVerifOutputAnalyzer {
&& pragmaAuth.getAttrB().getAttribute() == attribute1)
{
this.results.put(pragma, result);
+ this.notifyListeners();
break;
}
}
@@ -320,6 +344,7 @@ public class ProVerifOutputAnalyzer {
if (previousAuthPragma != null)
{
previousAuthPragma.setWeakSatisfied(true);
+ this.notifyListeners();
}
previousAuthPragma = null;
}
@@ -331,6 +356,7 @@ public class ProVerifOutputAnalyzer {
if (previousAuthPragma != null)
{
previousAuthPragma.setWeakSatisfied(false);
+ this.notifyListeners();
}
previousAuthPragma = null;
}
@@ -341,7 +367,9 @@ public class ProVerifOutputAnalyzer {
// Found an error
else if (str.contains("Error:"))
{
- this.errors.add(str + ": " + previous);
+ synchronized(errors) {
+ this.errors.add(str + ": " + previous);
+ }
}
previous = str;
@@ -398,7 +426,7 @@ public class ProVerifOutputAnalyzer {
return state;
}
- public HashMap<AvatarPragma, ProVerifQueryResult> getResults()
+ public Map<AvatarPragma, ProVerifQueryResult> getResults()
{
return this.results;
}
@@ -458,6 +486,8 @@ public class ProVerifOutputAnalyzer {
}
public LinkedList<String> getErrors() {
- return errors;
+ synchronized(errors) {
+ return errors;
+ }
}
}
diff --git a/src/proverifspec/ProVerifOutputListener.java b/src/proverifspec/ProVerifOutputListener.java
new file mode 100644
index 0000000000000000000000000000000000000000..044c89b6013531d4a4580c79a76f03fde13093c6
--- /dev/null
+++ b/src/proverifspec/ProVerifOutputListener.java
@@ -0,0 +1,50 @@
+/**Copyright or (C) or Copr. GET / ENST, Telecom-Paris, Ludovic Apvrille
+ *
+ * ludovic.apvrille AT enst.fr
+ *
+ * This software is a computer program whose purpose is to allow the
+ * edition of TURTLE analysis, design and deployment diagrams, to
+ * allow the generation of RT-LOTOS or Java code from this diagram,
+ * and at last to allow the analysis of formal validation traces
+ * obtained from external tools, e.g. RTL from LAAS-CNRS and CADP
+ * from INRIA Rhone-Alpes.
+ *
+ * This software is governed by the CeCILL license under French law and
+ * abiding by the rules of distribution of free software. You can use,
+ * modify and/ or redistribute the software under the terms of the CeCILL
+ * license as circulated by CEA, CNRS and INRIA at the following URL
+ * "http://www.cecill.info".
+ *
+ * As a counterpart to the access to the source code and rights to copy,
+ * modify and redistribute granted by the license, users are provided only
+ * with a limited warranty and the software's author, the holder of the
+ * economic rights, and the successive licensors have only limited
+ * liability.
+ *
+ * In this respect, the user's attention is drawn to the risks associated
+ * with loading, using, modifying and/or developing or reproducing the
+ * software by the user in light of its specific status of free software,
+ * that may mean that it is complicated to manipulate, and that also
+ * therefore means that it is reserved for developers and experienced
+ * professionals having in-depth computer knowledge. Users are therefore
+ * encouraged to load and test the software's suitability as regards their
+ * requirements in conditions enabling the security of their systems and/or
+ * data to be ensured and, more generally, to use and operate it in the
+ * same conditions as regards security.
+ *
+ * The fact that you are presently reading this means that you have had
+ * knowledge of the CeCILL license and that you accept its terms.
+ *
+ * /**
+ * Class ProVerifOutputListener
+ * Creation: 02/06/2017
+ * @version 1.0 02/06/2017
+ * @author Florian LUGOU
+ * @see
+ */
+
+package proverifspec;
+
+public interface ProVerifOutputListener {
+ public void proVerifOutputChanged();
+}
diff --git a/src/ui/DefaultText.java b/src/ui/DefaultText.java
index b6bee2206dd1954ab86e3185535067d68a8d831c..428f2341080ba832592a961895dff0b33476957c 100755
--- a/src/ui/DefaultText.java
+++ b/src/ui/DefaultText.java
@@ -49,8 +49,8 @@ package ui;
public class DefaultText {
- public static String BUILD = "12243";
- public static String DATE = "2017/06/02 02:01:04 CET";
+ public static String BUILD = "12247";
+ public static String DATE = "2017/06/06 02:01:02 CET";
public static StringBuffer sbAbout = makeAbout();
diff --git a/src/ui/GTURTLEModeling.java b/src/ui/GTURTLEModeling.java
index 87311199f6d523724c4ba8bfe1f600ee98589ef9..f3031db81851fae1f77f7f74097081bf9d542aca 100755
--- a/src/ui/GTURTLEModeling.java
+++ b/src/ui/GTURTLEModeling.java
@@ -1990,7 +1990,7 @@ public class GTURTLEModeling {
rshc.setCmd(ConfigurationTTool.ProVerifVerifierPath + " -in pitype pvspec");
rshc.sendExecuteCommandRequest();
- String data = rshc.getDataFromProcess();
+ Reader data = rshc.getDataReaderFromProcess();
ProVerifOutputAnalyzer pvoa = getProVerifOutputAnalyzer ();
pvoa.analyzeOutput(data, true);
diff --git a/src/ui/interactivesimulation/JFrameSimulationSDPanel.java b/src/ui/interactivesimulation/JFrameSimulationSDPanel.java
index 90bce05ea7803e0bfb47844d454f16a085506588..c201b7e59a0ab1d262b0cfd52661b4f847ae4a70 100755
--- a/src/ui/interactivesimulation/JFrameSimulationSDPanel.java
+++ b/src/ui/interactivesimulation/JFrameSimulationSDPanel.java
@@ -55,6 +55,8 @@ import javax.swing.*;
import java.awt.*;
import java.awt.event.ActionEvent;
import java.awt.event.ActionListener;
+import java.awt.event.ComponentAdapter;
+import java.awt.event.ComponentEvent;
import java.io.BufferedReader;
//import javax.swing.event.*;
@@ -105,6 +107,14 @@ public class JFrameSimulationSDPanel extends JFrame implements ActionListener {
initActions();
makeComponents();
//setComponents();
+ this.addComponentListener(new ComponentAdapter() {
+ @Override
+ public void componentResized(ComponentEvent e)
+ {
+ if (JFrameSimulationSDPanel.this.sdpanel != null)
+ JFrameSimulationSDPanel.this.sdpanel.resized();
+ }
+ });
}
private JLabel createStatusBar() {
diff --git a/src/ui/interactivesimulation/JSimulationSDPanel.java b/src/ui/interactivesimulation/JSimulationSDPanel.java
index 694836a0ad2e653d36882727f0af6d3e0b31b643..d6e6ebb74ef9543a31533ea31ad2d2c807eab451 100644
--- a/src/ui/interactivesimulation/JSimulationSDPanel.java
+++ b/src/ui/interactivesimulation/JSimulationSDPanel.java
@@ -176,6 +176,11 @@ public class JSimulationSDPanel extends JPanel implements MouseMotionListener, R
public void setMyScrollPanel(JScrollPane _jsp) {
jsp = _jsp;
}
+
+ public void resized() {
+ this.spaceBetweenLifeLinesComputed = false;
+ this.repaint();
+ }
protected void paintComponent(Graphics g) {
super.paintComponent(g);
diff --git a/src/ui/window/JDialogProverifVerification.java b/src/ui/window/JDialogProverifVerification.java
index e15c8aba148dedbfb2075a3d40d0b0fe83e9460c..527bbd2d191d23eab63947296f9e6b645a8173f9 100644
--- a/src/ui/window/JDialogProverifVerification.java
+++ b/src/ui/window/JDialogProverifVerification.java
@@ -52,6 +52,7 @@ import avatartranslator.AvatarPragmaReachability;
import avatartranslator.AvatarPragmaSecret;
import launcher.LauncherException;
import launcher.RshClient;
+import launcher.RshClientReader;
import myutil.GraphicLib;
import myutil.MasterProcessInterface;
import myutil.TraceManager;
@@ -59,6 +60,7 @@ import proverifspec.ProVerifOutputAnalyzer;
import proverifspec.ProVerifQueryAuthResult;
import proverifspec.ProVerifQueryResult;
import proverifspec.ProVerifResultTraceStep;
+import proverifspec.ProVerifOutputListener;
import ui.AvatarDesignPanel;
import ui.IconManager;
import ui.MainGUI;
@@ -73,11 +75,12 @@ import java.awt.event.ActionListener;
import java.awt.event.MouseEvent;
import java.awt.event.MouseListener;
import java.io.*;
-import java.util.HashMap;
+import java.util.Map;
import java.util.LinkedList;
+import java.util.Collections;
-public class JDialogProverifVerification extends javax.swing.JDialog implements ActionListener, ListSelectionListener, MouseListener, Runnable, MasterProcessInterface {
+public class JDialogProverifVerification extends javax.swing.JDialog implements ActionListener, ListSelectionListener, MouseListener, Runnable, MasterProcessInterface, ProVerifOutputListener {
private static final Insets insets = new Insets(0, 0, 0, 0);
private static final Insets WEST_INSETS = new Insets(0, 0, 0, 0);
@@ -103,6 +106,8 @@ public class JDialogProverifVerification extends javax.swing.JDialog implements
int mode;
+ private ProVerifOutputAnalyzer pvoa;
+
//components
protected JPanel jta;
protected JButton start;
@@ -141,7 +146,7 @@ public class JDialogProverifVerification extends javax.swing.JDialog implements
private JList<AvatarPragma> satisfiedWeakAuthList;
private JList<AvatarPragma> nonSatisfiedAuthList;
private JList<AvatarPragma> nonProvedList;
- private HashMap<AvatarPragma, ProVerifQueryResult> results;
+ private Map<AvatarPragma, ProVerifQueryResult> results;
private Thread t;
private boolean go = false;
@@ -172,6 +177,7 @@ public class JDialogProverifVerification extends javax.swing.JDialog implements
mgui = _mgui;
this.adp = adp;
+ this.pvoa = null;
if (pathCode == null) {
pathCode = _pathCode;
@@ -356,6 +362,9 @@ public class JDialogProverifVerification extends javax.swing.JDialog implements
}
public void closeDialog() {
+ if (this.pvoa != null) {
+ this.pvoa.removeListener(this);
+ }
if (mode == STARTED) {
stopProcess();
}
@@ -409,7 +418,6 @@ public class JDialogProverifVerification extends javax.swing.JDialog implements
hasError = false;
TraceManager.addDev("Thread started");
- this.jta.removeAll();
File testFile;
try {
@@ -473,120 +481,16 @@ public class JDialogProverifVerification extends javax.swing.JDialog implements
//jta.append("" + mgui.gtm.getCheckingWarnings().size() + " warning(s)\n");
testGo();
- rshc = new RshClient(hostProVerif);
- rshc.setCmd(cmd);
- rshc.sendExecuteCommandRequest();
- String data = rshc.getDataFromProcess();
-
- ProVerifOutputAnalyzer pvoa = mgui.gtm.getProVerifOutputAnalyzer ();
- pvoa.analyzeOutput(data, typedLanguage.isSelected());
-
- if (pvoa.getErrors().size() != 0) {
- int y = 0;
+ this.rshc = new RshClient(hostProVerif);
+ this.rshc.setCmd(cmd);
+ this.rshc.sendExecuteCommandRequest();
+ RshClientReader reader = this.rshc.getDataReaderFromProcess();
- JLabel label = new JLabel("Errors found in the generated code:");
- label.setAlignmentX(Component.LEFT_ALIGNMENT);
- this.jta.add(label, this.createGbc(0, y++));
- label = new JLabel("----------------");
- label.setAlignmentX(Component.LEFT_ALIGNMENT);
- this.jta.add(label, this.createGbc(0, y++));
- this.jta.add(Box.createRigidArea(new Dimension(0,5)), this.createGbc(0, y++));
- for(String error: pvoa.getErrors()) {
- label = new JLabel(error);
- label.setAlignmentX(Component.LEFT_ALIGNMENT);
- this.jta.add(label,this.createGbc(0, y++));
- }
- } else {
- LinkedList<AvatarPragma> reachableEvents = new LinkedList<AvatarPragma> ();
- LinkedList<AvatarPragma> nonReachableEvents = new LinkedList<AvatarPragma> ();
- LinkedList<AvatarPragma> secretTerms = new LinkedList<AvatarPragma> ();
- LinkedList<AvatarPragma> nonSecretTerms = new LinkedList<AvatarPragma> ();
- LinkedList<AvatarPragma> satisfiedStrongAuth = new LinkedList<AvatarPragma> ();
- LinkedList<AvatarPragma> satisfiedWeakAuth = new LinkedList<AvatarPragma> ();
- LinkedList<AvatarPragma> nonSatisfiedAuth = new LinkedList<AvatarPragma> ();
- LinkedList<AvatarPragma> nonProved = new LinkedList<AvatarPragma> ();
-
- this.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);
- }
- }
- }
-
- LinkedList<ProVerifResultSection> sectionsList = new LinkedList<ProVerifResultSection> ();
- sectionsList.add(new ProVerifResultSection("Reachable states:", reachableEvents, this.reachableEventsList));
- sectionsList.add(new ProVerifResultSection("Non reachable states:", nonReachableEvents, this.nonReachableEventsList));
- sectionsList.add(new ProVerifResultSection("Confidential Data:", secretTerms, this.secretTermsList));
- sectionsList.add(new ProVerifResultSection("Non confidential Data:", nonSecretTerms, this.nonSecretTermsList));
- sectionsList.add(new ProVerifResultSection("Satisfied Strong Authenticity:", satisfiedStrongAuth, this.satisfiedStrongAuthList));
- sectionsList.add(new ProVerifResultSection("Satisfied Weak Authenticity:", satisfiedWeakAuth, this.satisfiedWeakAuthList));
- sectionsList.add(new ProVerifResultSection("Non Satisfied Authenticity:", nonSatisfiedAuth, this.nonSatisfiedAuthList));
- sectionsList.add(new ProVerifResultSection("Not Proved Queries:", nonProved, this.nonProvedList));
-
- int y = 0;
-
- for (ProVerifResultSection section: sectionsList)
- {
- if (!section.results.isEmpty())
- {
- JLabel label = new JLabel(section.title);
- label.setAlignmentX(Component.LEFT_ALIGNMENT);
- this.jta.add(label, this.createGbc(0, y++));
- this.jta.add(Box.createRigidArea(new Dimension(0,5)), this.createGbc(0, y++));
- section.jlist = new JList<AvatarPragma> (section.results.toArray (new AvatarPragma[0]));
- section.jlist.setSelectionMode(ListSelectionModel.SINGLE_SELECTION);
- section.jlist.addMouseListener(this);
- section.jlist.setAlignmentX(Component.LEFT_ALIGNMENT);
- this.jta.add(section.jlist, this.createGbc(0, y++));
- this.jta.add(Box.createRigidArea(new Dimension(0,10)), this.createGbc(0, y++));
- }
- }
+ if (this.pvoa == null) {
+ this.pvoa = mgui.gtm.getProVerifOutputAnalyzer ();
+ this.pvoa.addListener(this);
}
+ this.pvoa.analyzeOutput(reader, typedLanguage.isSelected());
mgui.modelBacktracingProVerif(pvoa);
@@ -702,4 +606,129 @@ public class JDialogProverifVerification extends javax.swing.JDialog implements
{
// TODO: unselect the other lists
}
+
+ @Override
+ public void proVerifOutputChanged()
+ {
+ JLabel label;
+ this.jta.removeAll();
+
+ if (pvoa.getErrors().size() != 0) {
+ int y = 0;
+
+ label = new JLabel("Errors found in the generated code:");
+ label.setAlignmentX(Component.LEFT_ALIGNMENT);
+ this.jta.add(label, this.createGbc(0, y++));
+ label = new JLabel("----------------");
+ label.setAlignmentX(Component.LEFT_ALIGNMENT);
+ this.jta.add(label, this.createGbc(0, y++));
+ this.jta.add(Box.createRigidArea(new Dimension(0,5)), this.createGbc(0, y++));
+ for(String error: pvoa.getErrors()) {
+ label = new JLabel(error);
+ label.setAlignmentX(Component.LEFT_ALIGNMENT);
+ this.jta.add(label,this.createGbc(0, y++));
+ }
+ } else {
+ LinkedList<AvatarPragma> reachableEvents = new LinkedList<AvatarPragma> ();
+ LinkedList<AvatarPragma> nonReachableEvents = new LinkedList<AvatarPragma> ();
+ LinkedList<AvatarPragma> secretTerms = new LinkedList<AvatarPragma> ();
+ LinkedList<AvatarPragma> nonSecretTerms = new LinkedList<AvatarPragma> ();
+ LinkedList<AvatarPragma> satisfiedStrongAuth = new LinkedList<AvatarPragma> ();
+ LinkedList<AvatarPragma> satisfiedWeakAuth = new LinkedList<AvatarPragma> ();
+ LinkedList<AvatarPragma> nonSatisfiedAuth = new LinkedList<AvatarPragma> ();
+ LinkedList<AvatarPragma> nonProved = new LinkedList<AvatarPragma> ();
+
+ this.results = this.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);
+ }
+ }
+ }
+
+ LinkedList<ProVerifResultSection> sectionsList = new LinkedList<ProVerifResultSection> ();
+ 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 ProVerifResultSection("Reachable states:", reachableEvents, this.reachableEventsList));
+ sectionsList.add(new ProVerifResultSection("Non reachable states:", nonReachableEvents, this.nonReachableEventsList));
+ sectionsList.add(new ProVerifResultSection("Confidential Data:", secretTerms, this.secretTermsList));
+ sectionsList.add(new ProVerifResultSection("Non confidential Data:", nonSecretTerms, this.nonSecretTermsList));
+ sectionsList.add(new ProVerifResultSection("Satisfied Strong Authenticity:", satisfiedStrongAuth, this.satisfiedStrongAuthList));
+ sectionsList.add(new ProVerifResultSection("Satisfied Weak Authenticity:", satisfiedWeakAuth, this.satisfiedWeakAuthList));
+ sectionsList.add(new ProVerifResultSection("Non Satisfied Authenticity:", nonSatisfiedAuth, this.nonSatisfiedAuthList));
+ sectionsList.add(new ProVerifResultSection("Not Proved Queries:", nonProved, this.nonProvedList));
+
+ int y = 0;
+
+ for (ProVerifResultSection section: sectionsList)
+ {
+ if (!section.results.isEmpty())
+ {
+ label = new JLabel(section.title);
+ label.setAlignmentX(Component.LEFT_ALIGNMENT);
+ this.jta.add(label, this.createGbc(0, y++));
+ this.jta.add(Box.createRigidArea(new Dimension(0,5)), this.createGbc(0, y++));
+ section.jlist = new JList<AvatarPragma> (section.results.toArray (new AvatarPragma[0]));
+ section.jlist.setSelectionMode(ListSelectionModel.SINGLE_SELECTION);
+ section.jlist.addMouseListener(this);
+ section.jlist.setAlignmentX(Component.LEFT_ALIGNMENT);
+ this.jta.add(section.jlist, this.createGbc(0, y++));
+ this.jta.add(Box.createRigidArea(new Dimension(0,10)), this.createGbc(0, y++));
+ }
+ }
+ }
+
+ this.repaint();
+ this.revalidate();
+ }
}