diff --git a/src/avatartranslator/toproverif/AVATAR2ProVerif.java b/src/avatartranslator/toproverif/AVATAR2ProVerif.java
index 5ff611b2defd378675094db0e1c94423748b2954..8b2ea53896a3c78c5f5758e85c422cdc4cb4d7d3 100755
--- a/src/avatartranslator/toproverif/AVATAR2ProVerif.java
+++ b/src/avatartranslator/toproverif/AVATAR2ProVerif.java
@@ -83,14 +83,14 @@ public class AVATAR2ProVerif {
- public ProVerifSpec generateProVerif(boolean _debug, boolean _optimize) {
+ public ProVerifSpec generateProVerif(boolean _debug, boolean _optimize, boolean _stateReachability) {
warnings = new Vector();
spec = new ProVerifSpec();
avspec.removeCompositeStates();
avspec.removeTimers();
- makeHeader();
+ makeHeader(_stateReachability);
makeBlocks();
@@ -122,7 +122,7 @@ public class AVATAR2ProVerif {
return spec;
}
- public void makeHeader() {
+ public void makeHeader(boolean _stateReachability) {
spec.addToGlobalSpecification(DATA_HEADER + "\n");
spec.addToGlobalSpecification(PK_HEADER + "\n");
@@ -155,7 +155,17 @@ public class AVATAR2ProVerif {
spec.addToGlobalSpecification("query attacker:" + attribute.getName() + ".\n\n");
}
}
+ // Queries for states
+ if (_stateReachability) {
+ for(AvatarStateMachineElement asme: block.getStateMachine().getListOfElements()) {
+ if (asme instanceof AvatarState) {
+ spec.addToGlobalSpecification("query ev:" + "enteringState__" + block.getName() + "__" + asme.getName() + "().\n");
+ }
+ }
+ }
}
+
+
}
public boolean hasSecretPragmaWithAttribute(String _blockName, String attributeName) {
@@ -413,7 +423,7 @@ public class AVATAR2ProVerif {
spec.addProcess(p);
_processes.add(p);
_states.add((AvatarState)_asme);
- addLine(p, "event enteringState__" + _asme.getName() + "()");
+ addLine(p, "event enteringState__" + _block.getName() + "__" + _asme.getName() + "()");
// Calling the new process from the old one
addLine(_p, p.processName);
diff --git a/src/proverifspec/ProVerifOutputAnalyzer.java b/src/proverifspec/ProVerifOutputAnalyzer.java
new file mode 100644
index 0000000000000000000000000000000000000000..2a955f51de47186e180b342dfcfb247c5b084d89
--- /dev/null
+++ b/src/proverifspec/ProVerifOutputAnalyzer.java
@@ -0,0 +1,124 @@
+/**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 ProVerifOutputAnalyzer
+* Creation: 16/09/2010
+* @version 1.0 16/09/2010
+* @author Ludovic APVRILLE
+* @see
+*/
+
+package proverifspec;
+
+import java.util.*;
+
+import myutil.*;
+import java.io.*;
+
+
+public class ProVerifOutputAnalyzer {
+
+
+ private LinkedList<String> reachableEvents;
+ private LinkedList<String> nonReachableEvents;
+ private LinkedList<String> secretTerms;
+ private LinkedList<String> nonSecretTerms;
+
+
+
+ public ProVerifOutputAnalyzer() {
+ reachableEvents = new LinkedList<String>();
+ nonReachableEvents = new LinkedList<String>();
+ secretTerms = new LinkedList<String>();
+ nonSecretTerms = new LinkedList<String>();
+ }
+
+ public void analyzeOutput(String _s) {
+ String str;
+ int index0, index1;
+
+ BufferedReader reader = new BufferedReader(new StringReader(_s));
+
+ try {
+ while ((str = reader.readLine()) != null) {
+ index0 = str.indexOf("RESULT not ev:");
+ index1 = str.indexOf("() is false");
+ if ((index0 < index1) && (index0 != -1) && (index1 != -1)) {
+ reachableEvents.add(str.substring(index0+14, index1));
+ }
+ index0 = str.indexOf("RESULT not ev:");
+ index1 = str.indexOf("() is true");
+ if ((index0 < index1) && (index0 != -1) && (index1 != -1)) {
+ nonReachableEvents.add(str.substring(index0+14, index1));
+ }
+ index0 = str.indexOf("RESULT not attacker:");
+ index1 = str.indexOf("[] is true");
+ if ((index0 < index1) && (index0 != -1) && (index1 != -1)) {
+ secretTerms.add(str.substring(index0+20, index1));
+ }
+ index0 = str.indexOf("RESULT not attacker:");
+ index1 = str.indexOf("[] is false");
+ if ((index0 < index1) && (index0 != -1) && (index1 != -1)) {
+ nonSecretTerms.add(str.substring(index0+20, index1));
+ }
+
+ }
+
+ } catch(IOException e) {
+ e.printStackTrace();
+ }
+
+ }
+
+ public LinkedList<String> getReachableEvents() {
+ return reachableEvents;
+ }
+
+ public LinkedList<String> getNonReachableEvents() {
+ return nonReachableEvents;
+ }
+
+ public LinkedList<String> getSecretTerms() {
+ return secretTerms;
+ }
+
+ public LinkedList<String> getNonSecretTerms() {
+ return nonSecretTerms;
+ }
+
+}
\ No newline at end of file
diff --git a/src/ui/GTURTLEModeling.java b/src/ui/GTURTLEModeling.java
index 9f53198f92f6aa8ced73e05f3cd026e1d98e6338..c8612f0e5e3874dad8953bc727f4b74385e55659 100755
--- a/src/ui/GTURTLEModeling.java
+++ b/src/ui/GTURTLEModeling.java
@@ -442,11 +442,11 @@ public class GTURTLEModeling {
}
}
- public boolean generateProVerifFromAVATAR(String _path) {
+ public boolean generateProVerifFromAVATAR(String _path, boolean _stateReachability) {
avatar2proverif = new AVATAR2ProVerif(avatarspec);
//tml2uppaal.setChoiceDeterministic(choices);
//tml2uppaal.setSizeInfiniteFIFO(_size);
- proverif = avatar2proverif.generateProVerif(true, true);
+ proverif = avatar2proverif.generateProVerif(true, true, _stateReachability);
languageID = PROVERIF;
//mgui.setMode(MainGUI.MODEL_PROVERIF_OK);
//uppaalTable = tml2uppaal.getRelationTIFUPPAAL(_debug);
diff --git a/src/ui/window/JDialogProVerifGeneration.java b/src/ui/window/JDialogProVerifGeneration.java
index 9055fe87f6a9c175f3eb2981b60da3c3d9c0b75a..82f0f3679a1fc2897f6d0292ff68ee8205fea65e 100644
--- a/src/ui/window/JDialogProVerifGeneration.java
+++ b/src/ui/window/JDialogProVerifGeneration.java
@@ -56,6 +56,7 @@ import java.util.*;
import myutil.*;
import avatartranslator.toproverif.*;
import avatartranslator.*;
+import proverifspec.*;
import ui.*;
import launcher.*;
@@ -90,7 +91,7 @@ public class JDialogProVerifGeneration extends javax.swing.JDialog implements Ac
protected JTextField code1, code2, unitcycle, compiler1, exe1, exe2, exe3, exe2int;
protected JTabbedPane jp1;
protected JScrollPane jsp;
- protected JCheckBox removeCppFiles, removeXFiles, debugmode, optimizemode;
+ protected JCheckBox stateReachability, outputOfProVerif;
protected JComboBox versionSimulator;
private Thread t;
@@ -171,11 +172,14 @@ public class JDialogProVerifGeneration extends javax.swing.JDialog implements Ac
jp01.add(new JLabel(" "), c01);
c01.gridwidth = GridBagConstraints.REMAINDER; //end row
- /*debugmode = new JCheckBox("Put debug information in code");
- debugmode.setSelected(false);
- jp01.add(debugmode, c01);
+ stateReachability = new JCheckBox("Compute state reachability");
+ stateReachability.setSelected(true);
+ jp01.add(stateReachability, c01);
- optimizemode = new JCheckBox("Optimize code");
+
+
+
+ /*optimizemode = new JCheckBox("Optimize code");
optimizemode.setSelected(optimizeModeSelected);
jp01.add(optimizemode, c01);
@@ -215,11 +219,17 @@ public class JDialogProVerifGeneration extends javax.swing.JDialog implements Ac
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));
@@ -314,7 +324,7 @@ public class JDialogProVerifGeneration extends javax.swing.JDialog implements Ac
testGo();
- if (mgui.gtm.generateProVerifFromAVATAR(pathCode)) {
+ if (mgui.gtm.generateProVerifFromAVATAR(pathCode, stateReachability.isSelected())) {
jta.append("ProVerif code generation done\n");
} else {
jta.append("Could not generate SystemC file\n");
@@ -336,8 +346,34 @@ public class JDialogProVerifGeneration extends javax.swing.JDialog implements Ac
// Command
data = processCmd(cmd);
- jta.append(data);
- jta.append("Execution done\n");
+ if (outputOfProVerif.isSelected()) {
+ jta.append(data);
+ }
+
+ ProVerifOutputAnalyzer pvoa = new ProVerifOutputAnalyzer();
+ pvoa.analyzeOutput(data);
+
+ 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(String re: pvoa.getSecretTerms()) {
+ jta.append(re+"\n");
+ }
+
+ jta.append("\nNon confidential data:\n----------------\n");
+ for(String re: pvoa.getNonSecretTerms()) {
+ jta.append(re+"\n");
+ }
+
+ jta.append("\nAll done\n");
} catch (LauncherException le) {
jta.append("Error: " + le.getMessage() + "\n");
mode = STOPPED;