diff --git a/src/avatartranslator/toproverif/AVATAR2ProVerif.java b/src/avatartranslator/toproverif/AVATAR2ProVerif.java
index 709ca3ce8d67cbd70735c3ad8a60db7bd38c1f44..0c912ef84f2e981a36db144ea643c5371d9dbdb3 100755
--- a/src/avatartranslator/toproverif/AVATAR2ProVerif.java
+++ b/src/avatartranslator/toproverif/AVATAR2ProVerif.java
@@ -55,7 +55,7 @@ import javax.swing.*;
import ui.ConfigurationTTool;
import ui.CheckingError;
import ui.AvatarDesignPanel;
-import ui.window.JDialogProVerifGeneration;
+import ui.window.JDialogProverifVerification;
import ui.TGComponent;
import proverifspec.*;
import myutil.*;
@@ -551,8 +551,8 @@ public class AVATAR2ProVerif implements AvatarTranslator {
}
// Queries for states
- TraceManager.addDev ("Queries Event (" + (this.stateReachability == JDialogProVerifGeneration.REACHABILITY_ALL ? "ALL" : this.stateReachability == JDialogProVerifGeneration.REACHABILITY_SELECTED ? "SELECTED" : "NONE") + ")");
- if (this.stateReachability != JDialogProVerifGeneration.REACHABILITY_NONE) {
+ TraceManager.addDev ("Queries Event (" + (this.stateReachability == JDialogProverifVerification.REACHABILITY_ALL ? "ALL" : this.stateReachability == JDialogProverifVerification.REACHABILITY_SELECTED ? "SELECTED" : "NONE") + ")");
+ if (this.stateReachability != JDialogProverifVerification.REACHABILITY_NONE) {
this.spec.addDeclaration (new ProVerifComment ("Queries Event"));
for (AvatarBlock block: this.avspec.getListOfBlocks ()) {
HashSet<AvatarStateMachineElement> visited = new HashSet<AvatarStateMachineElement> ();
@@ -564,7 +564,7 @@ public class AVATAR2ProVerif implements AvatarTranslator {
continue;
visited.add (asme);
- if (asme instanceof AvatarState && (this.stateReachability == JDialogProVerifGeneration.REACHABILITY_ALL || ((AvatarState) asme).isCheckable ())) {
+ if (asme instanceof AvatarState && (this.stateReachability == JDialogProverifVerification.REACHABILITY_ALL || ((AvatarState) asme).isCheckable ())) {
this.spec.addDeclaration (new ProVerifQueryEv (new ProVerifVar[] {}, "enteringState__" + block.getName() + "__" + asme.getName()));
this.spec.addDeclaration (new ProVerifEvDecl ("enteringState__" + block.getName() + "__" + asme.getName(), new String[] {}));
TraceManager.addDev("| event (enteringState__" + block.getName() + "__" + asme.getName() + ")");
@@ -1293,8 +1293,8 @@ public class AVATAR2ProVerif implements AvatarTranslator {
ProVerifTranslatorParameter arg = (ProVerifTranslatorParameter) _arg;
ProVerifProcInstr _lastInstr = arg.lastInstr;
- if (this.stateReachability == JDialogProVerifGeneration.REACHABILITY_ALL ||
- (this.stateReachability == JDialogProVerifGeneration.REACHABILITY_SELECTED && _asme.isCheckable ()))
+ if (this.stateReachability == JDialogProverifVerification.REACHABILITY_ALL ||
+ (this.stateReachability == JDialogProverifVerification.REACHABILITY_SELECTED && _asme.isCheckable ()))
// Adding an event for reachability of the state
_lastInstr = _lastInstr.setNextInstr (new ProVerifProcRaw ("event enteringState__" + arg.block.getName() + "__" + _asme.getName() + "()", true));
diff --git a/src/ui/ActionPerformer.java b/src/ui/ActionPerformer.java
index 878aedb46322d205f0ff92eb012e775f38d98a8f..f24cf00472befea686896f86b2f2925106927958 100755
--- a/src/ui/ActionPerformer.java
+++ b/src/ui/ActionPerformer.java
@@ -157,8 +157,6 @@ public class ActionPerformer {
mgui.generateAUTS();
} else if (command.equals(mgui.actions[TGUIAction.ACT_GEN_UPPAAL].getActionCommand())) {
mgui.generateUPPAAL();
- } else if (command.equals(mgui.actions[TGUIAction.ACT_GEN_PROVERIF].getActionCommand())) {
- mgui.generateProVerif();
} else if (command.equals(mgui.actions[TGUIAction.ACT_DSE].getActionCommand())) {
mgui.dse();
} else if (command.equals(mgui.actions[TGUIAction.ACT_AVATAR_MODEL_CHECKER].getActionCommand())) {
diff --git a/src/ui/GTURTLEModeling.java b/src/ui/GTURTLEModeling.java
index 54a1a8ba219dc4d28125573f8dd8ecba79d629e0..5ffe6b313d6f78479305a959a9eb67a1b4e33121 100755
--- a/src/ui/GTURTLEModeling.java
+++ b/src/ui/GTURTLEModeling.java
@@ -2920,7 +2920,6 @@ public class GTURTLEModeling {
warnings = avatar2proverif.getWarnings();
languageID = PROVERIF;
mgui.setMode(MainGUI.EDIT_PROVERIF_OK);
- //mgui.setMode(MainGUI.MODEL_PROVERIF_OK);
//uppaalTable = tml2uppaal.getRelationTIFUPPAAL(_debug);
try {
if (avatar2proverif.saveInFile(_path)){
@@ -2951,8 +2950,6 @@ public class GTURTLEModeling {
languageID = TPN;
- mgui.setMode(MainGUI.EDIT_PROVERIF_OK);
- //mgui.setMode(MainGUI.MODEL_PROVERIF_OK);
//uppaalTable = tml2uppaal.getRelationTIFUPPAAL(_debug);
return true;
/*try {
diff --git a/src/ui/JToolBarMainTurtle.java b/src/ui/JToolBarMainTurtle.java
index 9dfa8c39c0c95c83ae812301a809ad237bb566ee..6446dceb0efef4a8745a4e9878f4809b984e345d 100755
--- a/src/ui/JToolBarMainTurtle.java
+++ b/src/ui/JToolBarMainTurtle.java
@@ -198,11 +198,6 @@ public class JToolBarMainTurtle extends JToolBar implements ActionListener
genlotos.addMouseListener(mgui.mouseHandler);
}
- /*if (MainGUI.proverifOn) {
- button = add(mgui.actions[TGUIAction.ACT_GEN_PROVERIF]);
- button.addMouseListener(mgui.mouseHandler);
- }*/
-
addSeparator();
checkcode = add(mgui.actions[TGUIAction.ACT_CHECKCODE]);
diff --git a/src/ui/MainGUI.java b/src/ui/MainGUI.java
index 69b058ad7534cf0eaf48968d8bbd214acc68b4b1..437664cda1f1bbc895e65bf5c378e237995d6152 100644
--- a/src/ui/MainGUI.java
+++ b/src/ui/MainGUI.java
@@ -270,7 +270,6 @@ public class MainGUI implements ActionListener, WindowListener, KeyListener, Pe
public final static byte UPPAAL_OK = 42;
public final static byte NC_OK = 43;
public final static byte MODEL_UPPAAL_OK = 44;
- public final static byte MODEL_PROVERIF_OK = 45;
public final static byte EDIT_PROVERIF_OK = 46;
public final static byte AVATAR_SYNTAXCHECKING_OK = 47;
public final static byte PANEL_CHANGED = 48;
@@ -3102,7 +3101,6 @@ public class MainGUI implements ActionListener, WindowListener, KeyListener, Pe
if (b) {
ret = true;
setMode(MainGUI.AVATAR_SYNTAXCHECKING_OK);
- //setMode(MainGUI.MODEL_PROVERIF_OK);
//setMode(MainGUI.GEN_DESIGN_OK);
/*
if (!automatic) {
@@ -3161,7 +3159,6 @@ public class MainGUI implements ActionListener, WindowListener, KeyListener, Pe
if (b) {
ret = true;
setMode(MainGUI.AVATAR_SYNTAXCHECKING_OK);
- //setMode(MainGUI.MODEL_PROVERIF_OK);
//setMode(MainGUI.GEN_DESIGN_OK);
/*
if (!automatic) {
@@ -3951,7 +3948,6 @@ public class MainGUI implements ActionListener, WindowListener, KeyListener, Pe
public void avatarProVerifVerification() {
TraceManager.addDev("Avatar proverif fv");
- //JDialogProVerifGeneration jgen = new JDialogProVerifGeneration(frame, this, "ProVerif: code generation and verification", ConfigurationTTool.ProVerifVerifierHost, ConfigurationTTool.ProVerifCodeDirectory, ConfigurationTTool.ProVerifVerifierPath);
JDialogProverifVerification jgen = new JDialogProverifVerification(frame, this, "Security verification with ProVerif", ConfigurationTTool.ProVerifVerifierHost, ConfigurationTTool.ProVerifCodeDirectory, ConfigurationTTool.ProVerifVerifierPath);
// jgen.setSize(500, 450);
GraphicLib.centerOnParent(jgen, 500, 450);
@@ -4088,33 +4084,6 @@ public class MainGUI implements ActionListener, WindowListener, KeyListener, Pe
}
- public void generateProVerif() {
- TraceManager.addDev("Generate ProVerif!");
-
- JDialogProVerifGeneration jgen = new JDialogProVerifGeneration(frame, this, "ProVerif: code generation and verification", ConfigurationTTool.ProVerifVerifierHost, ConfigurationTTool.ProVerifCodeDirectory, ConfigurationTTool.ProVerifVerifierPath);
- //jgen.setSize(500, 450);
- GraphicLib.centerOnParent(jgen, 500, 450);
- jgen.setVisible(true);
- dtree.toBeUpdated();
-
- // Generate from AVATAR
- /*if (gtm.getTURTLEModelingState() == 3) {
- boolean result = gtm.generateProVerifFromAVATAR(ConfigurationTTool.ProVerifCodeDirectory);
- if (result) {
- JOptionPane.showMessageDialog(frame,
- "0 error, " + getCheckingWarnings().size() + " warning(s). ProVerif specification generated",
- "Successful translation from the Avatar to a ProVerif specification",
- JOptionPane.INFORMATION_MESSAGE);
- } else {
- JOptionPane.showMessageDialog(frame,
- "" + getCheckingErrors().size() + " errors, " +getCheckingWarnings().size() + " warning(s). ProVerif specification could NOT be generated",
- "ERROR during translation from AVATAR to UPPAAL",
- JOptionPane.INFORMATION_MESSAGE);
- }
- }*/
- }
-
-
public List<String> generateAllAUT(String path) {
return gtm.generateAUT(path);
}
diff --git a/src/ui/ModeManager.java b/src/ui/ModeManager.java
index 58c72430aba0e5ef8e8bba6484adcdc0416135c8..26f007941d770e4b2cfed7a8bbb84155f819a6c7 100755
--- a/src/ui/ModeManager.java
+++ b/src/ui/ModeManager.java
@@ -151,10 +151,6 @@ public class ModeManager {
//actions[TGUIAction.ACT_SIMU_JAVA].setEnabled(true);
//actions[TGUIAction.ACT_GEN_RTLOTOS].setEnabled(true);
//actions[TGUIAction.ACT_PROJECTION].setEnabled(false);
- break;
- case MainGUI.MODEL_PROVERIF_OK:
- actions[TGUIAction.ACT_GEN_PROVERIF].setEnabled(true);
-
break;
case MainGUI.EDIT_PROVERIF_OK:
actions[TGUIAction.ACT_VIEW_RTLOTOS].setEnabled(true);
@@ -218,7 +214,6 @@ public class ModeManager {
actions[TGUIAction.ACT_GEN_AUT].setEnabled(false);
actions[TGUIAction.ACT_GEN_AUTS].setEnabled(false);
actions[TGUIAction.ACT_GEN_UPPAAL].setEnabled(false);
- actions[TGUIAction.ACT_GEN_PROVERIF].setEnabled(false);
actions[TGUIAction.ACT_AVATAR_MODEL_CHECKER].setEnabled(false);
actions[TGUIAction.ACT_CHECKCODE].setEnabled(false);
actions[TGUIAction.ACT_SIMULATION].setEnabled(false);
@@ -244,7 +239,6 @@ public class ModeManager {
actions[TGUIAction.ACT_GEN_TMLTXT].setEnabled(false);
actions[TGUIAction.ACT_GEN_CCODE].setEnabled(false);
actions[TGUIAction.ACT_GEN_UPPAAL].setEnabled(false);
- actions[TGUIAction.ACT_GEN_PROVERIF].setEnabled(false);
//actions[TGUIAction.ACT_AVATAR_MODEL_CHECKER].setEnabled(false);
actions[TGUIAction.ACT_GEN_AUT].setEnabled(false);
actions[TGUIAction.ACT_GEN_AUTS].setEnabled(false);
@@ -264,7 +258,6 @@ public class ModeManager {
actions[TGUIAction.ACT_GEN_AUT].setEnabled(false);
actions[TGUIAction.ACT_GEN_AUTS].setEnabled(false);
actions[TGUIAction.ACT_GEN_UPPAAL].setEnabled(false);
- actions[TGUIAction.ACT_GEN_PROVERIF].setEnabled(false);
actions[TGUIAction.ACT_AVATAR_MODEL_CHECKER].setEnabled(false);
actions[TGUIAction.ACT_CHECKCODE].setEnabled(false);
actions[TGUIAction.ACT_SIMULATION].setEnabled(false);
diff --git a/src/ui/TGUIAction.java b/src/ui/TGUIAction.java
index 7a8cac6e18506af4468dfe7e01c08852925a2ef4..6f43ca38bac6e5120bec50eda363fa4860fc8a32 100755
--- a/src/ui/TGUIAction.java
+++ b/src/ui/TGUIAction.java
@@ -474,7 +474,6 @@ public class TGUIAction extends AbstractAction {
public static final int ACT_GEN_RTLOTOS = 27;
public static final int ACT_GEN_LOTOS = 155;
public static final int ACT_GEN_UPPAAL = 204;
- public static final int ACT_GEN_PROVERIF = 331;
public static final int ACT_AVATAR_MODEL_CHECKER = 433;
public static final int ACT_GEN_JAVA = 112;
public static final int ACT_SIMU_JAVA = 167;
@@ -710,7 +709,6 @@ public class TGUIAction extends AbstractAction {
actions[ACT_ONECLICK_LOTOS_RG] = new TAction("gen_rglotos-command", "One-click LOTOS-based verification", IconManager.imgic342, IconManager.imgic342, "One-click LOTOS-based verification", "Generates a LOTOS-based RG from TTool diagrams", '0');
actions[ACT_ONECLICK_RTLOTOS_RG] = new TAction("gen_rgrtlotos-command", "Generate RT-LOTOS-based RG", IconManager.imgic342, IconManager.imgic342, "Generate RT-LOTOS-based RG ", "Generates an RT-LOTOS-based RG from TTool diagrams", '0');
actions[ACT_GEN_UPPAAL] = new TAction("gen_uppaal-command", "Safety formal verification with UPPAAL", IconManager.imgic86, IconManager.imgic86, "Generate UPPAAL specification", "Generates a UPPAAL specification from TTool diagrams", '0');
- actions[ACT_GEN_PROVERIF] = new TAction("gen_proverif-command", "Generate ProVerif Code", IconManager.imgic34, IconManager.imgic35, "Generate ProVerif specification", "Generates a ProVerif specification from AVATAR diagrams", '0');
actions[ACT_AVATAR_MODEL_CHECKER] = new TAction("avatar-model-checker", "Avatar model checker", IconManager.imgic140, IconManager.imgic140, "Avatar model checker", "Executes the AVATAR model checker from an AVATAR design", '0');
actions[ACT_GEN_JAVA] = new TAction("gen_java-command", "Generate JAVA", IconManager.imgic38, IconManager.imgic39, "Generate JAVA", "Generates Java code from TURTLE diagrams", 0);
actions[ACT_SIMU_JAVA] = new TAction("gen_simujava-command", "Java-based simulation", IconManager.imgic38, IconManager.imgic39, "JAVA-based simualtion", "Simulate diagrams using Java language", 0);
diff --git a/src/ui/window/JDialogDSE.java b/src/ui/window/JDialogDSE.java
index 4508a378fb6d1ac2e6a59e46fd2f293e14028bbd..77110e6e21dab80434b00ea1053b63784946fa1f 100644
--- a/src/ui/window/JDialogDSE.java
+++ b/src/ui/window/JDialogDSE.java
@@ -36,7 +36,7 @@
* knowledge of the CeCILL license and that you accept its terms.
*
* /**
- * Class JDialogProVerifGeneration
+ * Class JDialogDSE
* Dialog for managing the generation of ProVerif code and execution of
* ProVerif
* Creation: 10/09/2010
diff --git a/src/ui/window/JDialogProVerifGeneration.java b/src/ui/window/JDialogProVerifGeneration.java
deleted file mode 100644
index 48ccc201ec4a7c9d3155f2c248d073293138bebb..0000000000000000000000000000000000000000
--- a/src/ui/window/JDialogProVerifGeneration.java
+++ /dev/null
@@ -1,548 +0,0 @@
-/**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 JDialogProVerifGeneration
- * Dialog for managing the generation of ProVerif code and execution of
- * ProVerif
- * Creation: 10/09/2010
- * @version 1.1 10/09/2010
- * @author Ludovic APVRILLE
- * @see
- */
-
-package ui.window;
-
-import java.awt.*;
-import java.awt.event.*;
-import javax.swing.*;
-import java.io.*;
-
-import myutil.*;
-import avatartranslator.*;
-import proverifspec.*;
-import ui.*;
-
-import launcher.*;
-
-
-public class JDialogProVerifGeneration extends javax.swing.JDialog implements ActionListener, Runnable, MasterProcessInterface {
-
- protected MainGUI mgui;
-
- private String textC1 = "Generate ProVerif code in";
- private String textC2 = "Execute ProVerif as";
-
- protected static String pathCode;
- protected static String pathExecute;
-
-
- protected final static int NOT_STARTED = 1;
- 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;
-
- int mode;
-
- //components
- protected JTextArea jta;
- protected JButton start;
- protected JButton stop;
- protected JButton close;
-
- protected JRadioButton exe, exeint;
- protected ButtonGroup exegroup;
- protected JLabel gen, comp;
- protected JTextField code1, code2, unitcycle, compiler1, exe1, exe2, exe3, exe2int, loopLimit;
- protected JTabbedPane jp1;
- protected JScrollPane jsp;
- protected JCheckBox outputOfProVerif, typedLanguage;
- protected JRadioButton stateReachabilityAll, stateReachabilitySelected, stateReachabilityNone;
- protected ButtonGroup stateReachabilityGroup;
- protected JComboBox<String> versionSimulator;
-
- private Thread t;
- private boolean go = false;
- private boolean hasError = false;
- //protected boolean startProcess = false;
-
- private String hostProVerif;
-
- protected RshClient rshc;
-
-
- /** Creates new form */
- public JDialogProVerifGeneration(Frame f, MainGUI _mgui, String title, String _hostProVerif, String _pathCode, String _pathExecute) {
- super(f, title, true);
-
- mgui = _mgui;
-
- if (pathCode == null) {
- pathCode = _pathCode;
- }
-
- if (pathExecute == null)
- pathExecute = _pathExecute;
-
-
- hostProVerif = _hostProVerif;
-
- initComponents();
- myInitComponents();
- pack();
-
- //getGlassPane().addMouseListener( new MouseAdapter() {});
- getGlassPane().setCursor(Cursor.getPredefinedCursor(Cursor.WAIT_CURSOR));
- }
-
- protected void myInitComponents() {
- mode = NOT_STARTED;
- setButtons();
- }
-
- protected void initComponents() {
-
- Container c = getContentPane();
- setFont(new Font("Helvetica", Font.PLAIN, 14));
- c.setLayout(new BorderLayout());
- //setDefaultCloseOperation(JFrame.DISPOSE_ON_CLOSE);
-
- // Issue #41 Ordering of tabbed panes
- jp1 = GraphicLib.createTabbedPane();//new JTabbedPane();
-
- JPanel jp01 = new JPanel();
- GridBagLayout gridbag01 = new GridBagLayout();
- GridBagConstraints c01 = new GridBagConstraints();
- jp01.setLayout(gridbag01);
- jp01.setBorder(new javax.swing.border.TitledBorder("Code generation"));
-
- JPanel jp03 = new JPanel();
- GridBagLayout gridbag03 = new GridBagLayout();
- GridBagConstraints c03 = new GridBagConstraints();
- jp03.setLayout(gridbag03);
- jp03.setBorder(new javax.swing.border.TitledBorder("Execution"));
-
-
- c01.weighty = 1.0;
- c01.weightx = 1.0;
- c01.gridwidth = GridBagConstraints.REMAINDER; //end row
- c01.fill = GridBagConstraints.BOTH;
- c01.gridheight = 1;
-
- gen = new JLabel(textC1);
- //genJava.addActionListener(this);
- jp01.add(gen, c01);
-
- code1 = new JTextField(pathCode, 100);
- jp01.add(code1, c01);
-
- jp01.add(new JLabel(" "), c01);
- c01.gridwidth = GridBagConstraints.REMAINDER; //end row
-
-
- c01.gridx = 0;
- c01.gridy = 3;
- c01.gridwidth = 1;
- jp01.add(new JLabel("Compute state reachability: "), c01);
-
- stateReachabilityGroup = new ButtonGroup ();
-
- c01.gridx = 1;
- stateReachabilityAll = new JRadioButton("all");
- jp01.add(stateReachabilityAll, c01);
-
- c01.gridx = 2;
- stateReachabilitySelected = new JRadioButton("selected");
- jp01.add(stateReachabilitySelected, c01);
-
- c01.gridx = 3;
- c01.gridwidth = GridBagConstraints.REMAINDER; //end row
- stateReachabilityNone = new JRadioButton("none");
- jp01.add(stateReachabilityNone, c01);
-
- stateReachabilityGroup.add (stateReachabilityAll);
- stateReachabilityGroup.add (stateReachabilitySelected);
- stateReachabilityGroup.add (stateReachabilityNone);
- stateReachabilityAll.setSelected(true);
-
- c01.gridx = GridBagConstraints.RELATIVE;
- c01.gridy = GridBagConstraints.RELATIVE;
- typedLanguage = new JCheckBox("Generate typed Pi calculus");
- typedLanguage.setSelected(true);
- jp01.add(typedLanguage, c01);
- jp01.add(new JLabel("Limit on loop iterations"));
- c01.gridwidth= GridBagConstraints.REMAINDER;
- loopLimit = new JTextField("1", 3);
- jp01.add(loopLimit,c01);
- /*optimizemode = new JCheckBox("Optimize code");
- optimizemode.setSelected(optimizeModeSelected);
- jp01.add(optimizemode, c01);
-
- jp01.add(new JLabel("Simulator used:"), c01);
-
- versionSimulator = new JComboBox(simus);
- versionSimulator.setSelectedIndex(selectedItem);
- versionSimulator.addActionListener(this);
- jp01.add(versionSimulator, c01);
- //System.out.println("selectedItem=" + selectedItem);
-
- //devmode = new JCheckBox("Development version of the simulator");
- //devmode.setSelected(true);
- //jp01.add(devmode, c01);*/
-
- jp01.add(new JLabel(" "), c01);
-
- jp1.add("Generate code", jp01);
-
-
- // Panel 03
- c03.gridheight = 1;
- c03.weighty = 1.0;
- c03.weightx = 1.0;
- c03.gridwidth = GridBagConstraints.REMAINDER; //end row
- c03.fill = GridBagConstraints.BOTH;
- c03.gridheight = 1;
-
- exegroup = new ButtonGroup();
- exe = new JRadioButton(textC2, true);
- exe.addActionListener(this);
- exegroup.add(exe);
- //exeJava.addActionListener(this);
- jp03.add(exe, c03);
-
- exe2 = new JTextField(pathExecute + " -in pi ", 100);
- jp03.add(exe2, c03);
-
- jp03.add(new JLabel(" "), c03);
-
- outputOfProVerif = new JCheckBox("Show output of ProVerif");
- outputOfProVerif.setSelected(false);
- jp03.add(outputOfProVerif, c03);
-
-
- jp1.add("Execute", jp03);
-
- c.add(jp1, BorderLayout.NORTH);
-
-
- jta = new ScrolledJTextArea();
- jta.setEditable(false);
- jta.setMargin(new Insets(10, 10, 10, 10));
- jta.setTabSize(3);
- jta.append("Select options and then, click on 'start' to launch ProVerif code generation / compilation\n");
- Font f = new Font("Courrier", Font.BOLD, 12);
- jta.setFont(f);
- jsp = new JScrollPane(jta, JScrollPane.VERTICAL_SCROLLBAR_ALWAYS, JScrollPane.HORIZONTAL_SCROLLBAR_ALWAYS);
- jsp.setPreferredSize(new Dimension(300,300));
- c.add(jsp, BorderLayout.CENTER);
-
- start = new JButton("Start", IconManager.imgic53);
- stop = new JButton("Stop", IconManager.imgic55);
- close = new JButton("Close", IconManager.imgic27);
-
- start.setPreferredSize(new Dimension(100, 30));
- stop.setPreferredSize(new Dimension(100, 30));
- close.setPreferredSize(new Dimension(120, 30));
-
- start.addActionListener(this);
- stop.addActionListener(this);
- close.addActionListener(this);
-
- JPanel jp2 = new JPanel();
- jp2.add(start);
- jp2.add(stop);
- jp2.add(close);
-
- c.add(jp2, BorderLayout.SOUTH);
-
- }
-
- public void actionPerformed(ActionEvent evt) {
- String command = evt.getActionCommand();
-
- if (command.equals("Start")) {
- startProcess();
- } else if (command.equals("Stop")) {
- stopProcess();
- } else if (command.equals("Close")) {
- closeDialog();
- }
- }
-
- public void closeDialog() {
- if (mode == STARTED) {
- stopProcess();
- }
- dispose();
- }
-
- public void stopProcess() {
- if (rshc != null ){
- try {
- rshc.stopCommand();
- } catch (LauncherException le) {
- }
- }
- rshc = null;
- mode = STOPPED;
- setButtons();
- go = false;
- }
-
- public void startProcess() {
- t = new Thread(this);
- mode = STARTED;
- setButtons();
- go = true;
- t.start();
- }
-
- private void testGo() throws InterruptedException {
- if (go == false) {
- throw new InterruptedException("Stopped by user");
- }
- }
-
- public void run() {
- String cmd;
- String /*list,*/ data;
- // int cycle = 0;
-
- hasError = false;
-
- TraceManager.addDev("Thread started");
- File testFile;
- try {
- // Code generation
- if (jp1.getSelectedIndex() == 0) {
- jta.append("Generating ProVerif code\n");
-
- testGo();
- pathCode = code1.getText().trim ();
-
- if (pathCode.isEmpty()){
- pathCode="pvspec";
- }
-
- testFile = new File(pathCode);
-
- if (testFile.isDirectory()){
- if (!pathCode.endsWith (File.separator)){
- pathCode += File.separator;
- }
- pathCode += "pvspec";
- testFile = new File(pathCode);
- }
-
- if (testFile.exists()){
- // FIXME Raise error
- System.out.println("FILE EXISTS!!!");
- }
- if (mgui.gtm.generateProVerifFromAVATAR(pathCode, stateReachabilityAll.isSelected () ? REACHABILITY_ALL : stateReachabilitySelected.isSelected () ? REACHABILITY_SELECTED : REACHABILITY_NONE, typedLanguage.isSelected(), loopLimit.getText())) {
- jta.append("ProVerif code generation done\n");
- } else {
- setError();
- jta.append("Could not generate proverif code\n");
- }
-
- if (typedLanguage.isSelected()){
- exe2.setText(pathExecute + " -in pitype ");
- }
- else {
- exe2.setText(pathExecute + " -in pi ");
- }
- exe2.setText(exe2.getText()+pathCode);
- //if (mgui.gtm.getCheckingWarnings().size() > 0) {
- jta.append("" + mgui.gtm.getCheckingWarnings().size() + " warning(s)\n");
- //}
- }
- testGo();
- // Execute
- if (jp1.getSelectedIndex() == 1) {
- try {
-
- cmd = exe2.getText();
-
- jta.append("Executing ProVerif code with command: \n" + cmd + "\n");
-
- rshc = new RshClient(hostProVerif);
- // Assuma data are on the remote host
- // Command
-
- data = processCmd(cmd);
-
-
- if (outputOfProVerif.isSelected()) {
- jta.append(data);
- }
-
- ProVerifOutputAnalyzer pvoa = mgui.gtm.getProVerifOutputAnalyzer ();
- pvoa.analyzeOutput(data, typedLanguage.isSelected());
-
- if (pvoa.getErrors().size() != 0) {
- jta.append("\nErrors found in the generated code:\n----------------\n");
- for(String error: pvoa.getErrors()) {
- jta.append(error+"\n");
- }
-
- } else {
-
- jta.append("\nReachable states:\n----------------\n");
- for(String re: pvoa.getReachableEvents()) {
- jta.append(re+"\n");
- }
-
- jta.append("\nNon reachable states:\n----------------\n");
- for(String re: pvoa.getNonReachableEvents()) {
- jta.append(re+"\n");
- }
-
- jta.append("\nConfidential Data:\n----------------\n");
- for(AvatarAttribute attr: pvoa.getSecretTerms()) {
- jta.append(attr.getBlock ().getName () + "." + attr.getName () + "\n");
- }
-
- jta.append("\nNon Confidential Data:\n----------------\n");
- for(AvatarAttribute attr: pvoa.getNonSecretTerms()) {
- jta.append(attr.getBlock ().getName () + "." + attr.getName () + "\n");
- }
-
- jta.append("\nSatisfied Strong Authenticity:\n----------------\n");
- for(String re: pvoa.getSatisfiedAuthenticity()) {
- jta.append(re+"\n");
- }
-
- jta.append("\nSatisfied Weak Authenticity:\n----------------\n");
- for(String re: pvoa.getSatisfiedWeakAuthenticity()) {
- jta.append(re+"\n");
- }
-
- jta.append("\nNon Satisfied Strong Authenticity:\n----------------\n");
- for(String re: pvoa.getNonSatisfiedAuthenticity()) {
- jta.append(re+"\n");
- }
-
- jta.append("\nNon proved queries:\n----------------\n");
- for(String re: pvoa.getNotProved()) {
- jta.append(re+"\n");
- }
- }
-
- mgui.modelBacktracingProVerif(pvoa);
-
- jta.append("\nAll done\n");
- } catch (LauncherException le) {
- jta.append("Error: " + le.getMessage() + "\n");
- mode = STOPPED;
- setButtons();
- return;
- } catch (Exception e) {
- mode = STOPPED;
- setButtons();
- return;
- }
- }
-
- if ((hasError == false) && (jp1.getSelectedIndex() < 1)) {
- jp1.setSelectedIndex(jp1.getSelectedIndex() + 1);
- }
-
- } catch (InterruptedException ie) {
- jta.append("Interrupted\n");
- }
-
- jta.append("\n\nReady to process next command\n");
-
- checkMode();
- setButtons();
-
- //System.out.println("Selected item=" + selectedItem);
- }
-
- protected String processCmd(String cmd) throws LauncherException {
- rshc.setCmd(cmd);
- String s = null;
- rshc.sendExecuteCommandRequest();
- s = rshc.getDataFromProcess();
- return s;
- }
-
- protected void checkMode() {
- mode = NOT_STARTED;
- }
-
- protected void setButtons() {
- switch(mode) {
- case NOT_STARTED:
- start.setEnabled(true);
- stop.setEnabled(false);
- close.setEnabled(true);
- //setCursor(Cursor.getPredefinedCursor(Cursor.DEFAULT_CURSOR));
- getGlassPane().setVisible(false);
- break;
- case STARTED:
- start.setEnabled(false);
- stop.setEnabled(true);
- close.setEnabled(false);
- getGlassPane().setVisible(true);
- //setCursor(Cursor.getPredefinedCursor(Cursor.WAIT_CURSOR));
- break;
- case STOPPED:
- default:
- start.setEnabled(false);
- stop.setEnabled(false);
- close.setEnabled(true);
- getGlassPane().setVisible(false);
- break;
- }
- }
-
- public boolean hasToContinue() {
- return (go == true);
- }
-
- public void appendOut(String s) {
- jta.append(s);
- }
-
- public void setError() {
- hasError = true;
- }
-}
diff --git a/src/ui/window/JDialogProverifVerification.java b/src/ui/window/JDialogProverifVerification.java
index 4c28cd41768b78175ab1af3454b4092b20b9c91e..f16e53df6a58df7995af35c2aac35c7700566c16 100644
--- a/src/ui/window/JDialogProverifVerification.java
+++ b/src/ui/window/JDialogProverifVerification.java
@@ -381,43 +381,44 @@ public class JDialogProverifVerification extends javax.swing.JDialog implements
testGo();
pathCode = code1.getText().trim ();
- if (pathCode.isEmpty()){
- pathCode="pvspec";
- } /*else {
-
- if (!FileUtils.checkPath(pathCode)) {
- jta.append("Error: invalid directory: " + pathCode + "\n");
- mode = STOPPED;
- setButtons();
- return;
- }
- }*/
+ if (pathCode.isEmpty() || pathCode.endsWith(File.separator)) {
+ pathCode += "pvspec";
+ }
testFile = new File(pathCode);
- File dir = testFile.getParentFile();
- if (!dir.exists()) {
- jta.append("Error: invalid directory: " + pathCode + "\n");
- mode = STOPPED;
- setButtons();
- return;
- }
-
-
-
- if (testFile.isDirectory()){
- if (!pathCode.endsWith (File.separator)){
- pathCode += File.separator;
- }
+ if (testFile != null && testFile.isDirectory()){
+ pathCode += File.separator;
pathCode += "pvspec";
testFile = new File(pathCode);
}
+
+ File dir = null;
+ if (testFile != null)
+ {
+ dir = testFile.getParentFile();
+ }
+
+ if (testFile == null || dir == null || !dir.exists()) {
+ jta.append("Error: invalid file: " + pathCode + "\n");
+ mode = STOPPED;
+ setButtons();
+ return;
+ }
+
if (testFile.exists()){
// FIXME Raise error
System.out.println("FILE EXISTS!!!");
}
- if (mgui.gtm.generateProVerifFromAVATAR(pathCode, stateReachabilityAll.isSelected () ? REACHABILITY_ALL : stateReachabilitySelected.isSelected () ? REACHABILITY_SELECTED : REACHABILITY_NONE, typedLanguage.isSelected(), loopLimit.getText())) {
+
+ if (
+ mgui.gtm.generateProVerifFromAVATAR(
+ pathCode,
+ stateReachabilityAll.isSelected () ? REACHABILITY_ALL : stateReachabilitySelected.isSelected () ? REACHABILITY_SELECTED : REACHABILITY_NONE,
+ typedLanguage.isSelected(),
+ loopLimit.getText())
+ ) {
jta.append("ProVerif code generation done\n");
} else {
setError();
@@ -430,6 +431,7 @@ public class JDialogProverifVerification extends javax.swing.JDialog implements
else {
exe2.setText(pathExecute + " -in pi ");
}
+
exe2.setText(exe2.getText()+pathCode);
//if (mgui.gtm.getCheckingWarnings().size() > 0) {
jta.append("" + mgui.gtm.getCheckingWarnings().size() + " warning(s)\n");