diff --git a/src/avatartranslator/AvatarStateMachineElement.java b/src/avatartranslator/AvatarStateMachineElement.java
index 0facd74778edf7f10aa38fb69782eac776e1e055..77bb32d7a5dd43da43cd53f0030d3d78cbaa2965 100644
--- a/src/avatartranslator/AvatarStateMachineElement.java
+++ b/src/avatartranslator/AvatarStateMachineElement.java
@@ -47,6 +47,8 @@ package avatartranslator;
import java.util.*;
+import myutil.*;
+
public abstract class AvatarStateMachineElement extends AvatarElement {
@@ -182,5 +184,64 @@ public abstract class AvatarStateMachineElement extends AvatarElement {
public abstract AvatarStateMachineElement basicCloneMe();
+
+ // Guard with an id and not(id)
+ public boolean hasElseChoiceType1() {
+ if (nexts.size() != 2) {
+ return false;
+ }
+
+ AvatarStateMachineElement elt1, elt2;
+
+ elt1 = getNext(0);
+ elt2 = getNext(1);
+
+ if ( (!(elt1 instanceof AvatarTransition)) || (!(elt2 instanceof AvatarTransition))) {
+ return false;
+ }
+
+ AvatarTransition at1, at2;
+
+ at1 = (AvatarTransition)elt1;
+ at2 = (AvatarTransition)elt2;
+
+ if ((!(at1.isGuarded())) || (!(at2.isGuarded()))) {
+ return false;
+ }
+
+ String g1, g2;
+ g1 = at1.getGuard();
+ g2 = at2.getGuard();
+
+ g1 = Conversion.replaceAllString(g1, "[", "");
+ g1 = Conversion.replaceAllString(g1, "]", "").trim();
+ g1 = Conversion.replaceAllString(g1, " ", "");
+
+ g2 = Conversion.replaceAllString(g2, "[", "");
+ g2 = Conversion.replaceAllString(g2, "]", "").trim();
+ g2 = Conversion.replaceAllString(g2, " ", "");
+
+ String g, n;
+
+ if (g1.startsWith("not(")) {
+ n = g1;
+ g = g2;
+ } else {
+ g = g1;
+ n = g2;
+ }
+
+ if (!AvatarAttribute.isAValidAttributeName(g.trim())) {
+ return false;
+ }
+
+ if (n.substring(4, n.length()-1).compareTo(g) != 0) {
+ return false;
+ }
+
+
+ return true;
+ }
+
}
\ No newline at end of file
diff --git a/src/avatartranslator/toproverif/AVATAR2ProVerif.java b/src/avatartranslator/toproverif/AVATAR2ProVerif.java
index 8b2ea53896a3c78c5f5758e85c422cdc4cb4d7d3..69c5a8e5605863f5a44f2c52a7b5ea185254e59c 100755
--- a/src/avatartranslator/toproverif/AVATAR2ProVerif.java
+++ b/src/avatartranslator/toproverif/AVATAR2ProVerif.java
@@ -53,8 +53,12 @@ import myutil.*;
import avatartranslator.*;
public class AVATAR2ProVerif {
+
+ private final static String UNKNOWN = "UNKNOWN";
+
- private final static String DATA_HEADER = "(* Boolean return types *)\ndata true/0.\ndata false/0.\n";
+ private final static String BOOLEAN_DATA_HEADER = "(* Boolean return types *)\ndata true/0.\ndata false/0.\n";
+ private final static String FUNC_DATA_HEADER = "(* Functions data *)\ndata " + UNKNOWN + "/0.\n";
private final static String PK_HEADER = "(* Public key cryptography *)\nfun pk/1.\nfun encrypt/2.\nreduc decrypt(encrypt(x,pk(y)),y) = x.\n";
private final static String SK_HEADER = "(* Symmetric key cryptography *)\nfun sencrypt/2.\nreduc sdecrypt(sencrypt(x,k),k) = x.\n";
@@ -123,7 +127,8 @@ public class AVATAR2ProVerif {
}
public void makeHeader(boolean _stateReachability) {
- spec.addToGlobalSpecification(DATA_HEADER + "\n");
+ spec.addToGlobalSpecification(BOOLEAN_DATA_HEADER + "\n");
+ spec.addToGlobalSpecification(FUNC_DATA_HEADER + "\n");
spec.addToGlobalSpecification(PK_HEADER + "\n");
spec.addToGlobalSpecification(SK_HEADER + "\n");
@@ -131,6 +136,7 @@ public class AVATAR2ProVerif {
spec.addToGlobalSpecification(CONCAT_HEADER + "\n");
spec.addToGlobalSpecification("\n(* Channel *)\nfree ch.\n");
+ spec.addToGlobalSpecification("\n(* Channel *)\nprivate free chprivate.\n");
/* Parse all attributes declared by blocks and declare them as "private free" */
/*LinkedList<AvatarBlock> blocks = avatarspec.getListOfBlocks();
@@ -368,9 +374,12 @@ public class AVATAR2ProVerif {
AvatarSignal as;
AvatarActionOnSignal aaos;
AvatarTransition at;
- ProVerifProcess p;
- String tmp;
+ ProVerifProcess p, ptmp, ptmp1, ptmp2;
+ String tmp, name, value, term;
int i, j;
+ int index0, index1;
+ AvatarMethod am;
+ boolean found;
// Null element
if (_asme == null) {
@@ -439,36 +448,62 @@ public class AVATAR2ProVerif {
makeBlockProcesses(_block, _asm, _asme.getNext(0), p, _processes, _states, null);
return ;
}
+
- // Must handle the choice between several transitions
- // Must select the first transition to analyse non-deterministically
- // Make a process for all new following
- addLine(p, "new choice__" + _asme.getName());
- addLine(p, "out(ch, choice__" + _asme.getName() + ")");
-
-
- ProVerifProcess pvp[] = new ProVerifProcess[_asme.nbOfNexts()];
- tmp = "(";
- for(i=0; i<_asme.nbOfNexts(); i++) {
- if (i>0) {
- tmp += " | ";
+ if (_asme.hasElseChoiceType1()) {
+ TraceManager.addDev("Found a else choice");
+ ProVerifProcess pvp[] = new ProVerifProcess[_asme.nbOfNexts()];
+ tmp = "(";
+ for(i=0; i<_asme.nbOfNexts(); i++) {
+ if (i>0) {
+ tmp += " | ";
+ }
+ // Creating a new process
+ pvp[i] = new ProVerifProcess(_block.getName() + "__" + (_processes.size() + 1));
+ spec.addProcess(pvp[i]);
+ _processes.add(pvp[i]);
+ _states.add((AvatarState)_asme);
+ tmp += "(" + _block.getName() + "__" + (_processes.size()) + ")";
}
- // Creating a new process
- pvp[i] = new ProVerifProcess(_block.getName() + "__" + (_processes.size() + 1));
- spec.addProcess(pvp[i]);
- _processes.add(pvp[i]);
- _states.add((AvatarState)_asme);
- tmp += "(" + _block.getName() + "__" + (_processes.size()) + ")";
- }
- tmp += ")";
- addLine(p, tmp);
- for(i=0; i<_asme.nbOfNexts(); i++) {
- makeBlockProcesses(_block, _asm, _asme.getNext(i), pvp[i], _processes, _states, _asme.getName());
+ tmp += ")";
+ addLine(p, tmp);
+ for(i=0; i<_asme.nbOfNexts(); i++) {
+ makeBlockProcesses(_block, _asm, _asme.getNext(i), pvp[i], _processes, _states, null);
+ }
+ terminateProcess(p);
+
+ } else {
+
+ // Must handle the choice between several transitions
+ // Must select the first transition to analyse non-deterministically
+ // Make a process for all new following
+ addLine(p, "new choice__" + _asme.getName());
+ addLine(p, "out(chprivate, choice__" + _asme.getName() + ")");
+
+
+ ProVerifProcess pvp[] = new ProVerifProcess[_asme.nbOfNexts()];
+ tmp = "(";
+ for(i=0; i<_asme.nbOfNexts(); i++) {
+ if (i>0) {
+ tmp += " | ";
+ }
+ // Creating a new process
+ pvp[i] = new ProVerifProcess(_block.getName() + "__" + (_processes.size() + 1));
+ spec.addProcess(pvp[i]);
+ _processes.add(pvp[i]);
+ _states.add((AvatarState)_asme);
+ tmp += "(" + _block.getName() + "__" + (_processes.size()) + ")";
+ }
+ tmp += ")";
+ addLine(p, tmp);
+ for(i=0; i<_asme.nbOfNexts(); i++) {
+ makeBlockProcesses(_block, _asm, _asme.getNext(i), pvp[i], _processes, _states, _asme.getName());
+ }
+ terminateProcess(p);
}
- terminateProcess(p);
}
- // State
+ // Transition
} else if (_asme instanceof AvatarTransition) {
at = (AvatarTransition)_asme;
// Guard
@@ -483,26 +518,105 @@ public class AVATAR2ProVerif {
// Transition from a state -> this transition must be the one selected
if (_choiceInfo != null) {
- addLine(_p, "in(ch, m__)");
+ addLine(_p, "in(chprivate, m__)");
tmp = "if choice__" + _choiceInfo + " = m__ then";
addLineNoEnd(_p, tmp);
}
// Temporal operators are ignored
// Only functions are taken into account
+ p = _p;
for(i=0; i<at.getNbOfAction(); i++) {
tmp = at.getAction(i);
TraceManager.addDev("Found action: " + tmp);
if (!AvatarSpecification.isAVariableSettingString(tmp)) {
TraceManager.addDev("Found function: " + tmp);
- addLineNoEnd(_p, "let " + tmp + " in ");
+ index0 = tmp.indexOf('=');
+ index1 = tmp.indexOf('(');
+ term = tmp.substring(0, index0).trim();
+ if ((index0 == -1) || (index1 == -1) || (index0 > index1) || (term.length() == 0)) {
+ addLineNoEnd(p, "let " + tmp + " in ");
+ } else {
+ found = false;
+ name = tmp.substring(index0+1, index1).trim();
+ am = _block.getAvatarMethodWithName(name);
+ if (am != null) {
+ LinkedList<AvatarAttribute> list = am.getListOfReturnAttributes();
+ if (list.size() == 1) {
+ if (list.get(0).getType() == AvatarType.BOOLEAN) {
+ found = true;
+ }
+ }
+ }
+
+
+ if ((found) && (name.compareTo("verifyMAC") == 0)){
+ // Verify MAC!
+ index0 = tmp.indexOf(')');
+ if (index0 == -1) {
+ index0 = tmp.length();
+ }
+ value = tmp.substring(index1+1, index0).trim();
+ String[] values = value.split(",");
+ if (values.length < 3) {
+ addLineNoEnd(p, "let " + tmp + " in");
+ } else {
+ addLineNoEnd(p, "let MAC__tmp = MAC(" + values[0].trim() + " , " + values[1].trim() + ") in");
+ //addLine(p, "new choice__mac");
+ //addLine(p, "out(chprivate, choice__mac)");
+
+ ptmp1 = new ProVerifProcess(_block.getName() + "__" + (_processes.size() + 1));
+ spec.addProcess(ptmp1);
+ _processes.add(ptmp1);
+ _states.add(null);
+
+ ptmp2 = new ProVerifProcess(_block.getName() + "__" + (_processes.size() + 1));
+ spec.addProcess(ptmp2);
+ _processes.add(ptmp2);
+ _states.add(null);
+
+ addLineNoEnd(p, "((" + ptmp1.processName + ")|(" + ptmp2.processName + ")).");
+
+ ptmp = new ProVerifProcess(_block.getName() + "__" + (_processes.size() + 1));
+ spec.addProcess(ptmp);
+ _processes.add(ptmp);
+ _states.add(null);
+
+ addLineNoEnd(ptmp1, "if MAC__tmp = " + values[2].trim() + " then");
+ //addLine(ptmp1, "in(chprivate, m__)");
+ //addLineNoEnd(ptmp1, "if m__ = choice__mac then");
+ addLineNoEnd(ptmp1, "let " + term + "= true in");
+ addLineNoEnd(ptmp1, ptmp.processName + ".");
+
+ addLineNoEnd(ptmp2, "if MAC__tmp <> " + values[2].trim() + " then");
+ //addLine(ptmp2, "in(chprivate, m__)");
+ //addLineNoEnd(ptmp2, "if m__ = choice__mac then");
+ addLineNoEnd(ptmp2, "let " + term + "= false in");
+ addLineNoEnd(ptmp2, ptmp.processName + ".");
+
+ /*addLineNoEnd(p, "let MAC__tmp = MAC(" + values[0].trim() + " , " + values[1].trim() + ") in");
+ addLineNoEnd(p, "if MAC__tmp = " + values[2].trim() + " then");
+ addLineNoEnd(p, "let " + term + "= true in");
+ addLineNoEnd(p, ptmp.processName);
+ addLineNoEnd(p, "else");
+ addLineNoEnd(p, "let " + term + "= false in");
+ addLineNoEnd(p, ptmp.processName + ".");*/
+ p = ptmp;
+ }
+ } else {
+ addLineNoEnd(p, "let " + tmp + " in");
+ }
+
+
+ }
+
} else if (AvatarSpecification.isABasicVariableSettingString(tmp)) {
TraceManager.addDev("Found function: " + tmp);
- addLineNoEnd(_p, "let " + tmp + " in ");
+ addLineNoEnd(p, "let " + tmp + " in ");
}
}
- makeBlockProcesses(_block, _asm, _asme.getNext(0), _p, _processes, _states, null);
+ makeBlockProcesses(_block, _asm, _asme.getNext(0), p, _processes, _states, null);
// Ignored elements
} else {
diff --git a/src/proverifspec/ProVerifOutputAnalyzer.java b/src/proverifspec/ProVerifOutputAnalyzer.java
index 2a955f51de47186e180b342dfcfb247c5b084d89..cad09f0b6c950ec3dfb506331bc7976544869e4a 100644
--- a/src/proverifspec/ProVerifOutputAnalyzer.java
+++ b/src/proverifspec/ProVerifOutputAnalyzer.java
@@ -58,6 +58,7 @@ public class ProVerifOutputAnalyzer {
private LinkedList<String> nonReachableEvents;
private LinkedList<String> secretTerms;
private LinkedList<String> nonSecretTerms;
+ private LinkedList<String> errors;
@@ -66,10 +67,12 @@ public class ProVerifOutputAnalyzer {
nonReachableEvents = new LinkedList<String>();
secretTerms = new LinkedList<String>();
nonSecretTerms = new LinkedList<String>();
+
+ errors = new LinkedList<String>();
}
public void analyzeOutput(String _s) {
- String str;
+ String str, previous="";
int index0, index1;
BufferedReader reader = new BufferedReader(new StringReader(_s));
@@ -97,6 +100,12 @@ public class ProVerifOutputAnalyzer {
nonSecretTerms.add(str.substring(index0+20, index1));
}
+ index0 = str.indexOf("Error:");
+ if (index0 != -1) {
+ errors.add(str + ": " + previous);
+ }
+
+ previous = str;
}
} catch(IOException e) {
@@ -121,4 +130,8 @@ public class ProVerifOutputAnalyzer {
return nonSecretTerms;
}
+ public LinkedList<String> getErrors() {
+ return errors;
+ }
+
}
\ No newline at end of file
diff --git a/src/ui/GTURTLEModeling.java b/src/ui/GTURTLEModeling.java
index c8612f0e5e3874dad8953bc727f4b74385e55659..563a362bf7bc427f95fb4a539bf91196a64ee234 100755
--- a/src/ui/GTURTLEModeling.java
+++ b/src/ui/GTURTLEModeling.java
@@ -448,6 +448,7 @@ public class GTURTLEModeling {
//tml2uppaal.setSizeInfiniteFIFO(_size);
proverif = avatar2proverif.generateProVerif(true, true, _stateReachability);
languageID = PROVERIF;
+ mgui.setMode(MainGUI.EDIT_PROVERIF_OK);
//mgui.setMode(MainGUI.MODEL_PROVERIF_OK);
//uppaalTable = tml2uppaal.getRelationTIFUPPAAL(_debug);
try {
@@ -838,6 +839,14 @@ public class GTURTLEModeling {
public String getLastGraphicalRGAUTProj() {
return rgautprojdot;
}
+
+ public String getLastProVerifSpecification() {
+ if (proverif == null) {
+ return "";
+ }
+
+ return proverif.getStringSpec();
+ }
public int getNbRTLOTOS() {
return nbRTLOTOS;
diff --git a/src/ui/MainGUI.java b/src/ui/MainGUI.java
index 5a276958ca2fbf09bebf0614fd5b0862b25c2814..65ecea832cafc9b2e943c1775705c3dffe7f92dd 100755
--- a/src/ui/MainGUI.java
+++ b/src/ui/MainGUI.java
@@ -189,6 +189,7 @@ public class MainGUI implements ActionListener, WindowListener, KeyListener {
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 int INCREMENT = 10;
@@ -578,6 +579,9 @@ public class MainGUI implements ActionListener, WindowListener, KeyListener {
case MODEL_PROVERIF_OK:
actions[TGUIAction.ACT_GEN_PROVERIF].setEnabled(true);
break;
+ case EDIT_PROVERIF_OK:
+ actions[TGUIAction.ACT_VIEW_RTLOTOS].setEnabled(true);
+ break;
case GEN_DESIGN_OK:
actions[TGUIAction.ACT_GEN_DESIGN].setEnabled(true);
break;
@@ -3676,6 +3680,8 @@ public class MainGUI implements ActionListener, WindowListener, KeyListener {
showFormalSpecification("RT-LOTOS Specification #" + gtm.getNbRTLOTOS(), gtm.getLastRTLOTOSSpecification());
} else if (gtm.getLanguageID() == GTURTLEModeling.LOTOS) {
showFormalSpecification("LOTOS Specification #" + gtm.getNbRTLOTOS(), gtm.getLastRTLOTOSSpecification());
+ } else if (gtm.getLanguageID() == GTURTLEModeling.PROVERIF) {
+ showFormalSpecification("Last ProVerif Specification", gtm.getLastProVerifSpecification());
}
}
diff --git a/src/ui/window/JDialogProVerifGeneration.java b/src/ui/window/JDialogProVerifGeneration.java
index 82f0f3679a1fc2897f6d0292ff68ee8205fea65e..3b1cd7bc8ce0eb69346f7622e8a34a11505cf3f5 100644
--- a/src/ui/window/JDialogProVerifGeneration.java
+++ b/src/ui/window/JDialogProVerifGeneration.java
@@ -353,24 +353,33 @@ public class JDialogProVerifGeneration extends javax.swing.JDialog implements Ac
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");
+ 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(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");