diff --git a/src/main/java/avatartranslator/AvatarGuard.java b/src/main/java/avatartranslator/AvatarGuard.java
index f6cf4f8e735e746d88a417745cbed712314cb0bb..08523583e6caada473472f0711615465cdf3b99a 100644
--- a/src/main/java/avatartranslator/AvatarGuard.java
+++ b/src/main/java/avatartranslator/AvatarGuard.java
@@ -72,10 +72,11 @@ public abstract class AvatarGuard {
return new AvatarGuardEmpty();
String sane = AvatarGuard.sanitizeString(_guard);
+
if (sane.isEmpty())
return new AvatarGuardEmpty();
- if (sane.toLowerCase().equals("else"))
+ if (sane.equalsIgnoreCase("else"))
return new AvatarGuardElse();
int indexRParen = 0;
@@ -120,14 +121,16 @@ public abstract class AvatarGuard {
} else {
int indexLParen = sane.indexOf("(", indexRParen);
if (indexLParen == -1)
- indexLParen = indexRParen;
+ indexLParen = sane.length();
for (String delim: new String[]{"and", "or", "&&", "||"}) {
-
+ TraceManager.addDev("Working on delim: " + delim);
int indexBinaryOp = sane.substring(0, indexLParen).indexOf(delim, indexRParen + 1);
if (indexBinaryOp != -1) {
+ TraceManager.addDev("Found delim!");
first = AvatarGuard.createFromString(block, sane.substring(0, indexBinaryOp));
AvatarGuard second = AvatarGuard.createFromString(block, sane.substring(indexBinaryOp + delim.length()));
+ TraceManager.addDev("First=" + first + "\nSecond=" + second);
if (first instanceof AvatarComposedGuard && second instanceof AvatarComposedGuard)
return new AvatarBinaryGuard((AvatarComposedGuard) first, (AvatarComposedGuard) second, delim);
TraceManager.addDev("Binary guard " + sane + "does not contain 2 guards");
@@ -207,12 +210,12 @@ public abstract class AvatarGuard {
return new AvatarGuardEmpty();
}
- private static String sanitizeString(String s) {
+ public static String sanitizeString(String s) {
String result = Conversion.replaceAllChar(s, ' ', "").trim();
result = Conversion.replaceAllChar(result, '[', "");
result = Conversion.replaceAllChar(result, ']', "");
- return result;
+ return result.trim();
}
public static AvatarGuard addGuard(AvatarGuard _guard, AvatarGuard _g, String _binaryOp) {
diff --git a/src/main/java/avatartranslator/AvatarSyntaxChecker.java b/src/main/java/avatartranslator/AvatarSyntaxChecker.java
index 7ee7aad53b38df992711208626723dadfde0dcb4..d52671a2ff0fa499ca45ffa86cd446279d331169 100644
--- a/src/main/java/avatartranslator/AvatarSyntaxChecker.java
+++ b/src/main/java/avatartranslator/AvatarSyntaxChecker.java
@@ -210,7 +210,7 @@ public class AvatarSyntaxChecker {
public static int isAValidGuard(AvatarSpecification _as, AvatarStateMachineOwner _ab, String _guard) {
//TraceManager.addDev("Evaluating (non modified) guard:" + _guard);
- String tmp = _guard.replaceAll(" ", "").trim();
+ String tmp = _guard.replaceAll(" ", "");
if (tmp.compareTo("[]") == 0) {
return 0;
}
@@ -225,13 +225,23 @@ public class AvatarSyntaxChecker {
act = Conversion.putVariableValueInString(AvatarSpecification.ops, act, aa.getName(), aa.getDefaultInitialValue());
}
+ TraceManager.addDev("Testing guard expr=" + act);
+
AvatarExpressionSolver e1 = new AvatarExpressionSolver(act);
if (e1.buildExpression()) {
- return 1;
+ TraceManager.addDev("Build ok. guard expr=" + act);
+
+ TraceManager.addDev("Testing evaluation. guard expr=" + act);
+
+ if (e1.getReturnType() != AvatarExpressionSolver.IMMEDIATE_BOOL) {
+ return -1;
+ }
+
+ return 0;
}
- return 0;
+ return -1;
/*BoolExpressionEvaluator bee = new BoolExpressionEvaluator();
diff --git a/src/main/java/ui/AvatarDesignPanelTranslator.java b/src/main/java/ui/AvatarDesignPanelTranslator.java
index 9d643c04801298331768ce825fbc6ba76c0ff606..cf6d29cae03181bef0335a041b3c6c69b2fb6893 100644
--- a/src/main/java/ui/AvatarDesignPanelTranslator.java
+++ b/src/main/java/ui/AvatarDesignPanelTranslator.java
@@ -2330,24 +2330,31 @@ public class AvatarDesignPanelTranslator {
private void createGuard(final AvatarTransition transition,
final AvatarSMDConnector connector) {
+
+
final AvatarStateMachineOwner block = transition.getBlock();
- final String guardStr = modifyString(connector.getEffectiveGuard());
- //TraceManager.addDev("Effective guard:" + guardStr);
- final AvatarGuard guard = AvatarGuard.createFromString(block, guardStr);
- //TraceManager.addDev("Avatarguard:" + guard);
+ String toCheck = modifyString(connector.getEffectiveGuard());
+ toCheck = toCheck.replaceAll(" ", "");
final int error;
- if (guard.isElseGuard()) {
+ if ( (toCheck.equalsIgnoreCase("[]")) ||
+ (toCheck.equalsIgnoreCase("")) ||
+ (toCheck.equalsIgnoreCase("[else]"))
+ || (toCheck.equalsIgnoreCase("else"))) {
error = 0;
} else {
- error = AvatarSyntaxChecker.isAValidGuard(block.getAvatarSpecification(), block, guardStr);
+ TraceManager.addDev("Testing valid guard: " + toCheck);
+ error = AvatarSyntaxChecker.isAValidGuard(block.getAvatarSpecification(), block, toCheck);
+ TraceManager.addDev("guard Error? " + error);
}
if (error < 0) {
- makeError(error, connector.tdp, block, connector, "transition guard", guardStr);
+ makeError(error, connector.tdp, block, connector, "transition guard", toCheck);
} else {
+ final AvatarGuard guard = AvatarGuard.createFromString(block, toCheck);
transition.setGuard(guard);
}
+
}
private void createAfterDelay(final AvatarTransition transition,
diff --git a/src/main/java/ui/TGComboBoxWithHelp.java b/src/main/java/ui/TGComboBoxWithHelp.java
index 8c54a7b6dda366824fcab561c90d14d932a8209d..d9ecd6d0ef4dd85204899e847fe262efb3e2f4f8 100644
--- a/src/main/java/ui/TGComboBoxWithHelp.java
+++ b/src/main/java/ui/TGComboBoxWithHelp.java
@@ -61,7 +61,7 @@ import java.util.Vector;
* @author Ludovic APVRILLE
*/
public class TGComboBoxWithHelp<E> extends JComboBox<E> {
- public TGHelpButton myButton;
+ private TGHelpButton myButton;
public TGComboBoxWithHelp() {
super();
diff --git a/src/main/java/ui/TGHelpButton.java b/src/main/java/ui/TGHelpButton.java
index 67dc8800ae5389a6c403667813591260d0d6abe5..36dc6b99b5d353313060a82045b20b363c42ed0a 100644
--- a/src/main/java/ui/TGHelpButton.java
+++ b/src/main/java/ui/TGHelpButton.java
@@ -72,6 +72,13 @@ public class TGHelpButton extends JButton {
makeHelpConfiguration(helpWord, mgui, hm);
}
+ public TGHelpButton(String text, Icon icon, String helpWord, MainGUI mgui, HelpManager hm) {
+ super(text, icon);
+ this.mgui = mgui;
+ setGeneralConfiguration();
+ makeHelpConfiguration(helpWord, mgui, hm);
+ }
+
private void setGeneralConfiguration() {
setOpaque(false);
setFocusPainted(false);
@@ -90,6 +97,8 @@ public class TGHelpButton extends JButton {
}
if (he == null) {
TraceManager.addDev("NULL HE");
+ } else {
+ buttonClick(this, he, mgui);
}
}
}
@@ -104,7 +113,7 @@ public class TGHelpButton extends JButton {
c.weightx = 0.5;
c.gridwidth = GridBagConstraints.REMAINDER;
- buttonClick(this, he, mgui);
+
panel.add(this, c);
}
@@ -112,7 +121,7 @@ public class TGHelpButton extends JButton {
if (he == null) {
return;
}
- buttonClick(this, he, mgui);
+ //buttonClick(this, he, mgui);
panel.add(this);
}
@@ -120,10 +129,12 @@ public class TGHelpButton extends JButton {
- private void buttonClick(JButton but, HelpEntry he, MainGUI mgui) {
+ public void buttonClick(JButton but, HelpEntry he, MainGUI mgui) {
+ //TraceManager.addDev("ADding action listener");
but.addActionListener(new ActionListener() {
@Override
public void actionPerformed(ActionEvent e) {
+ //TraceManager.addDev("Action performed on help button!");
if(helpDialog == null) {
helpDialog = new JDialogTGComponentHelp(mgui, he);
helpDialog.setLocationHelpWindow(but);
diff --git a/src/main/java/ui/window/JDialogProverifVerification.java b/src/main/java/ui/window/JDialogProverifVerification.java
index 5172c9638c1aa3911ffca0f0ed495c08d2812a70..6e0234fa5bfa44f57fb5bbf394aacdfed544c029 100644
--- a/src/main/java/ui/window/JDialogProverifVerification.java
+++ b/src/main/java/ui/window/JDialogProverifVerification.java
@@ -107,10 +107,7 @@ import proverifspec.ProVerifQueryAuthResult;
import proverifspec.ProVerifQueryResult;
import proverifspec.ProVerifResultTraceStep;
import tmltranslator.TMLMapping;
-import ui.AvatarDesignPanel;
-import ui.MainGUI;
-import ui.TMLArchiPanel;
-import ui.TURTLEPanel;
+import ui.*;
import ui.interactivesimulation.JFrameSimulationSDPanel;
import ui.util.IconManager;
@@ -182,6 +179,9 @@ public class JDialogProverifVerification extends JDialog implements ActionListen
protected JCheckBox removeForkAndJoin;
+ public TGHelpButton myButton;
+ public static String helpString = "securityverification.html";
+
private Map<JCheckBox, List<JCheckBox>> cpuTaskObjs = new HashMap<JCheckBox, List<JCheckBox>>();
private class MyMenuItem extends JMenuItem {
@@ -483,6 +483,11 @@ public class JDialogProverifVerification extends JDialog implements ActionListen
jp01.setLayout(gridbag01);
jp01.setBorder(new javax.swing.border.TitledBorder("Verification options"));
+ myButton = new TGHelpButton("Help me!", IconManager.imgic32, helpString, mgui, mgui.getHelpManager());
+ jp01.add(myButton, new GridBagConstraints(3, curY, 1, 1, 1.0, 1.0, GridBagConstraints.EAST,
+ GridBagConstraints.BOTH, insets, 0, 0));
+ curY++;
+
JLabel gen = new JLabel("Generate ProVerif code in: ");
addComponent(jp01, gen, 0, curY, 1, GridBagConstraints.CENTER, GridBagConstraints.BOTH);
@@ -513,7 +518,8 @@ public class JDialogProverifVerification extends JDialog implements ActionListen
stateReachabilityAll.setSelected(true);
curY++;
- addComponent(jp01, new JLabel("Allow message duplication in private channels: "), 0, 3, 2, GridBagConstraints.CENTER, GridBagConstraints.BOTH);
+ addComponent(jp01, new JLabel("Allow message duplication in private channels: "), 0, curY, 2,
+ GridBagConstraints.CENTER, GridBagConstraints.BOTH);
ButtonGroup privateChannelGroup = new ButtonGroup();
privateChannelDup = new JRadioButton("Yes");
JRadioButton privateChannelNoDup = new JRadioButton("No");
@@ -538,7 +544,13 @@ public class JDialogProverifVerification extends JDialog implements ActionListen
}
JLabel empty = new JLabel("");
- jp01.add(empty, new GridBagConstraints(0, curY, 3, 1, 1.0, 1.0, GridBagConstraints.CENTER, GridBagConstraints.BOTH, insets, 0, 0));
+ jp01.add(empty, new GridBagConstraints(0, curY, 3, 1, 1.0, 1.0, GridBagConstraints.CENTER,
+ GridBagConstraints.BOTH, insets, 0, 0));
+
+
+
+
+
jta = new JPanel();
jta.setLayout(new GridBagLayout());
diff --git a/src/main/resources/help/securityverification.html b/src/main/resources/help/securityverification.html
index e100c42e06be15579540f2bd40223e45b37fb665..5130fe314800edc9ada4dcf68df6f593201c6a54 100644
--- a/src/main/resources/help/securityverification.html
+++ b/src/main/resources/help/securityverification.html
@@ -26,7 +26,7 @@
<h2 id="proverif-installation-and-configuration">ProVerif installation and configuration</h2>
<p>We advice to install the latest version of ProVerif on your computer. We usually install ProVerif using <em>opam</em>:</p>
<pre><code>$ opam install proverif</code></pre>
-<p>Once proverif has been installed, TTool must be configured. TTool relies on a .xml configuration file (bu defautl: config.xml). Open this configuration file and configure:</p>
+<p>Once proverif has been installed, TTool must be configured. TTool relies on a .xml configuration file (by default: config.xml). Open this configuration file and configure:</p>
<p>The directory in which TTool generated ProVerif specifications. For instance:</p>
<pre><code><ProVerifCodeDirectory data="/home/foo/TTool/proverif/" /></code></pre>
<p>The path to the ProVerif executable. For instance:</p>
@@ -34,7 +34,5 @@
<h2 id="security-properties">Security properties</h2>
<h2 id="investigating-verification-results">Investigating verification results</h2>
<h2 id="advanced-concepts">Advanced concepts</h2>
-<p>If the syntax is correct, then you can go on for verification or code generation.</p>
-<p>On the contrary, errors are listed in the tree on the left of the main panel. Similarly, warnings are listed in this tree.</p>
</body>
</html>
diff --git a/ttool/src/test/java/avatartranslator/AvatarExpressionTest.java b/ttool/src/test/java/avatartranslator/AvatarExpressionTest.java
index 88ff6e423f398981c5379817ef08494d11cb576f..7acbc61fb4c0a6cbcf13d51e8376cdb67aaa3b08 100644
--- a/ttool/src/test/java/avatartranslator/AvatarExpressionTest.java
+++ b/ttool/src/test/java/avatartranslator/AvatarExpressionTest.java
@@ -110,6 +110,10 @@ public class AvatarExpressionTest {
assertTrue(e1.buildExpression());
assertTrue(e1.getReturnType() == AvatarExpressionSolver.IMMEDIATE_BOOL);
+ AvatarExpressionSolver e1bis = new AvatarExpressionSolver("not( ( 0>10 ) and true)");
+ assertTrue(e1bis.buildExpression());
+ assertTrue(e1bis.getReturnType() == AvatarExpressionSolver.IMMEDIATE_BOOL);
+
AvatarExpressionSolver e2 = new AvatarExpressionSolver("-10 / 2 - 15 * 2 + 1 == -30 -4");
assertTrue(e2.buildExpression());
assertTrue(e2.getReturnType() == AvatarExpressionSolver.IMMEDIATE_BOOL);
diff --git a/ttool/src/test/java/avatartranslator/AvatarGuardTests.java b/ttool/src/test/java/avatartranslator/AvatarGuardTests.java
index 2796d5d0046dd6d27c4e5af4aac12ef13a6094c4..ec07c63fa304433cd9a029bcf3af71b378ea8c39 100644
--- a/ttool/src/test/java/avatartranslator/AvatarGuardTests.java
+++ b/ttool/src/test/java/avatartranslator/AvatarGuardTests.java
@@ -206,7 +206,7 @@ public class AvatarGuardTests {
assertTrue(res instanceof AvatarUnaryGuard);
res= AvatarGuard.createFromString(B, "not(m__a==key2)");
assertTrue(res instanceof AvatarUnaryGuard);
- res= AvatarGuard.createFromString(B, "not(m__a==m__b)");
+ res= AvatarGuard.createFromString(B, "not (m__a == m__b ) ");
assertTrue(res instanceof AvatarUnaryGuard);
}