diff --git a/Makefile b/Makefile
index 8a14a51b7074468372941b2304c30447c6be79cb..0e94f6e0d08105aff00dca8447d3a316e028c21c 100755
--- a/Makefile
+++ b/Makefile
@@ -15,7 +15,7 @@ GZIP = gzip -9 -f
DEBUG = -g
CLASSPATH = -classpath
SOURCEPATH = -sourcepath
-PACKAGE = avatartranslator avatartranslator/toexecutable avatartranslator/directsimulation avatartranslator/tocppsim avatartranslator/touppaal avatartranslator/toturtle avatartranslator/toproverif avatartranslator/totpn automata compiler/tmlparser vcd nc ddtranslator launcher myutil tpndescription sddescription sdtranslator tepe translator tmltranslator tmltranslator/tmlcp tmltranslator/toautomata tmltranslator/tosystemc tmltranslator/tomappingsystemc tmltranslator/tomappingsystemc2 tmltranslator/tomappingsystemc3 tmltranslator/touppaal tmltranslator/toturtle translator/tojava translator/tosimujava translator/totpn translator/touppaal ui ui/avatarbd ui/avatardd ui/avatarsmd ui/avatarrd ui/avatarpd ui/avatarcd ui/avatarad ui/ad ui/cd ui/oscd ui/osad ui/dd ui/ebrdd ui/file ui/graph ui/iod ui/ncdd ui/procsd ui/prosmdui/prosmd/util ui/tmlad ui/tmlcd ui/tmldd ui/tmlcomp ui/req ui/sd ui/tree ui/ucd ui/window tmltranslator tmltranslator/toturtle req/ebrdd tmltranslator/tosystemc tmatrix proverifspec uppaaldesc fr/inria/oasis/vercors/cttool/model remotesimulation tmltranslator/ctranslator attacktrees myutil/externalSearch
+#PACKAGE = avatartranslator avatartranslator/toexecutable avatartranslator/directsimulation avatartranslator/tocppsim avatartranslator/touppaal avatartranslator/toturtle avatartranslator/toproverif avatartranslator/totpn automata compiler/tmlparser vcd nc ddtranslator launcher myutil tpndescription sddescription sdtranslator tepe translator tmltranslator tmltranslator/tmlcp tmltranslator/toautomata tmltranslator/tosystemc tmltranslator/tomappingsystemc tmltranslator/tomappingsystemc2 tmltranslator/tomappingsystemc3 tmltranslator/touppaal tmltranslator/toturtle translator/tojava translator/tosimujava translator/totpn translator/touppaal ui ui/avatarbd ui/avatardd ui/avatarsmd ui/avatarrd ui/avatarpd ui/avatarcd ui/avatarad ui/ad ui/cd ui/oscd ui/osad ui/dd ui/ebrdd ui/file ui/graph ui/iod ui/ncdd ui/procsd ui/prosmdui/prosmd/util ui/tmlad ui/tmlcd ui/tmldd ui/tmlcomp ui/req ui/sd ui/tree ui/ucd ui/window tmltranslator tmltranslator/toturtle req/ebrdd tmltranslator/tosystemc tmatrix proverifspec uppaaldesc fr/inria/oasis/vercors/cttool/model remotesimulation tmltranslator/ctranslator attacktrees myutil/externalSearch
BUILDER = builder.jar
BUILD_INFO = build.txt
BUILD_TO_MODIFY = src/ui/DefaultText.java
@@ -72,6 +72,7 @@ TTOOL_TARGET = $(TTOOL_PATH)/TTool_install/TTool
TTOOL_TARGET_RELEASE = $(TTOOL_PATH)/TTool_install
TTOOL_PREINSTALL = $(TTOOL_PATH)/preinstallTTool
TTOOL_PREINSTALL_LINUX = $(TTOOL_PREINSTALL)/linux
+PACKAGE = $(shell cd $(TTOOL_SRC); find . -type d)
RELEASE_STD_FILES_LINUX_EXE = ttool_unix
RELEASE_STD_FILES_WINDIWS_EXE = ttool_windows.bat
@@ -299,3 +300,8 @@ clean:
rm -f $(TTOOL_SRC)/$$p/*.class $(TTOOL_SRC)/$$p/*.java~; \
done
+ultraclean: clean
+ @@for p in $(RELEASE_STD_FILES_BIN); do \
+ echo rm -f $$p;\
+ rm -f $(TTOOL_BIN)/$$p; \
+ done
diff --git a/src/avatartranslator/AvatarAction.java b/src/avatartranslator/AvatarAction.java
new file mode 100644
index 0000000000000000000000000000000000000000..abb3d37eccfcc44591fbdf7e944a97955008c0b0
--- /dev/null
+++ b/src/avatartranslator/AvatarAction.java
@@ -0,0 +1,88 @@
+/**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 AvatarAction
+ * Creation: 16/09/2015
+ * @version 1.0 16/09/2015
+ * @author Florian LUGOU
+ * @see
+ */
+
+package avatartranslator;
+
+import myutil.TraceManager;
+
+public abstract class AvatarAction {
+ String action;
+
+ public static AvatarAction createFromString (AvatarBlock block, String toParse) {
+ AvatarAction result = null;
+
+ int indexEq = toParse.indexOf("=");
+
+ if (indexEq == -1)
+ // No equal sign: this must be a function call
+ result = AvatarTermFunction.createFromString (block, toParse);
+
+ else {
+ // This should be an assignment
+ AvatarTerm leftHand = AvatarTerm.createFromString (block, toParse.substring (0, indexEq));
+ AvatarTerm rightHand = AvatarTerm.createFromString (block, toParse.substring (indexEq + 1));
+
+ if (leftHand != null && rightHand != null && leftHand.isLeftHand ())
+ result = new AvatarActionAssignment ((AvatarLeftHand) leftHand, rightHand);
+ }
+
+ if (result == null)
+ TraceManager.addDev ("Action '" + toParse + "' couldn't be parsed");
+
+ return result;
+ }
+
+ public boolean isAMethodCall () {
+ return false;
+ }
+
+ public boolean isAVariableSetting () {
+ return false;
+ }
+
+ public boolean isABasicVariableSetting () {
+ return false;
+ }
+}
diff --git a/src/avatartranslator/AvatarActionAssignment.java b/src/avatartranslator/AvatarActionAssignment.java
new file mode 100644
index 0000000000000000000000000000000000000000..a4bc98a3f286de8c443deec021ee752b7bc4774a
--- /dev/null
+++ b/src/avatartranslator/AvatarActionAssignment.java
@@ -0,0 +1,78 @@
+/**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 AvatarActionAssignment
+ * Creation: 16/09/2015
+ * @version 1.0 16/09/2015
+ * @author Florian LUGOU
+ * @see
+ */
+
+
+package avatartranslator;
+
+public class AvatarActionAssignment extends AvatarAction {
+ AvatarLeftHand leftHand;
+ AvatarTerm rightHand;
+
+ public AvatarActionAssignment (AvatarLeftHand _leftHand, AvatarTerm _rightHand) {
+ this.leftHand = _leftHand;
+ this.rightHand = _rightHand;
+ }
+
+ public boolean isAVariableSetting () {
+ return true;
+ }
+
+ public AvatarLeftHand getLeftHand () {
+ return this.leftHand;
+ }
+
+ public AvatarTerm getRightHand () {
+ return this.rightHand;
+ }
+
+ public boolean isABasicVariableSetting () {
+ return (this.leftHand instanceof AvatarLocalVar || this.leftHand instanceof AvatarAttribute) &&
+ (this.rightHand instanceof AvatarLocalVar || this.rightHand instanceof AvatarAttribute);
+ }
+
+ public String toString () {
+ return this.leftHand.toString () + " = " + this.rightHand.toString ();
+ }
+}
diff --git a/src/avatartranslator/AvatarActionOnSignal.java b/src/avatartranslator/AvatarActionOnSignal.java
index 35868951cd3df3a67ee4aa6c655dd4fe82275742..9b1455ba5d3dcde3ecb6a504e0c539adb987c111 100644
--- a/src/avatartranslator/AvatarActionOnSignal.java
+++ b/src/avatartranslator/AvatarActionOnSignal.java
@@ -116,4 +116,7 @@ public class AvatarActionOnSignal extends AvatarStateMachineElement {
}
}
+ public void translate (AvatarTranslator translator, Object arg) {
+ translator.translateActionOnSignal (this, arg);
+ }
}
diff --git a/src/avatartranslator/AvatarAttribute.java b/src/avatartranslator/AvatarAttribute.java
index 87b22968d50736d2d9589bf0c06645c96336f20e..9be6a8e0e26a88de94aec205910cd844b6701ec6 100644
--- a/src/avatartranslator/AvatarAttribute.java
+++ b/src/avatartranslator/AvatarAttribute.java
@@ -53,7 +53,7 @@ import myutil.*;
import translator.*;
import translator.tojava.*;
-public class AvatarAttribute extends AvatarElement{
+public class AvatarAttribute extends AvatarElement implements AvatarTerm,AvatarLeftHand {
// Types of parameters
private int type;
@@ -112,29 +112,6 @@ public class AvatarAttribute extends AvatarElement{
return (type == AvatarType.BOOLEAN);
}
- public static boolean isAValidAttributeName(String id) {
- if ((id == null) || (id.length() < 1)) {
- return false;
- }
-
- String lowerid = id.toLowerCase();
- boolean b1, b2, b3, b4, b5;
- b1 = (id.substring(0,1)).matches("[a-zA-Z]");
- b2 = id.matches("\\w*");
- b3 = !RTLOTOSKeyword.isAKeyword(lowerid);
- b5 = !JKeyword.isAKeyword(lowerid);
-
-
- if ((lowerid.equals(AvatarType.getStringType(0).toLowerCase())) || (lowerid.equals(AvatarType.getStringType(1).toLowerCase())) || (lowerid.equals(AvatarType.getStringType(2).toLowerCase())) || (lowerid.equals(AvatarType.getStringType(3).toLowerCase())) || (lowerid.equals(AvatarType.getStringType(4).toLowerCase()))) {
- b4 = false;
- } else {
- b4 = true;
- }
-
-
- return (b1 && b2 && b3 && b4 && b5);
- }
-
public String toString() {
String ret = AvatarType.getStringType(type) + " " + getName();
if (initialValue == null) {
@@ -152,4 +129,8 @@ public class AvatarAttribute extends AvatarElement{
return ret + " = " + initialValue;
}
+
+ public boolean isLeftHand () {
+ return true;
+ }
}
diff --git a/src/avatartranslator/AvatarBlock.java b/src/avatartranslator/AvatarBlock.java
index 9fba041a9feeeda1c887926de90e082b5d72486e..731cbaa049fa5d8fc85504f5a8aa68ff0f63cc62 100644
--- a/src/avatartranslator/AvatarBlock.java
+++ b/src/avatartranslator/AvatarBlock.java
@@ -574,7 +574,7 @@ public class AvatarBlock extends AvatarElement {
asme0 = asme.getNext(i);
if ((asme0 instanceof AvatarTransition) && (asme0 != at)) {
at0 = (AvatarTransition)asme0;
- g = at0.getGuard();
+ g = at0.getGuard().toString ();
if (g != null) {
if (at0.hasNonDeterministicGuard()) {
guard = "false";
@@ -592,7 +592,7 @@ public class AvatarBlock extends AvatarElement {
guard = Conversion.replaceAllChar(guard, '[', "(");
guard = Conversion.replaceAllChar(guard, ']', ")");
guard = "[" + guard + "]";
- at.setGuard(guard);
+ at.setGuard(new AvatarGuard (guard));
TraceManager.addDev("[ else ] replaced with :" + guard);
}
}
diff --git a/src/avatartranslator/AvatarBlockTemplate.java b/src/avatartranslator/AvatarBlockTemplate.java
index b62d207239b7d28aa4f67c14fe0c4b0aacadb565..872cd378249dd86f4cbf340c29fc311aa73ce032 100644
--- a/src/avatartranslator/AvatarBlockTemplate.java
+++ b/src/avatartranslator/AvatarBlockTemplate.java
@@ -52,93 +52,93 @@ import java.util.*;
import myutil.*;
public class AvatarBlockTemplate {
-
+
public AvatarBlockTemplate() {
}
-
- public static AvatarBlock getTimerBlock(String _name, Object _referenceBlock, Object _referenceSet, Object _referenceExpire, Object _referenceReset) {
- AvatarBlock ab = new AvatarBlock(_name, _referenceBlock);
-
- /*AvatarAttribute aa2 = new AvatarAttribute("toto", AvatarType.INTEGER, _referenceBlock);
- ab.addAttribute(aa2);*/
- AvatarAttribute aa = new AvatarAttribute("value", AvatarType.INTEGER, _referenceBlock);
- ab.addAttribute(aa);
- /*AvatarAttribute aa1 = new AvatarAttribute("__value", AvatarType.INTEGER, _referenceBlock);
- ab.addAttribute(aa1);*/
-
- AvatarSignal set = new AvatarSignal("set", AvatarSignal.IN, _referenceBlock);
- AvatarSignal reset = new AvatarSignal("reset", AvatarSignal.IN, _referenceBlock);
- AvatarSignal expire = new AvatarSignal("expire", AvatarSignal.OUT, _referenceBlock);
- AvatarAttribute val = new AvatarAttribute("value", AvatarType.INTEGER, aa.getReferenceObject());
- set.addParameter(val);
- ab.addSignal(set);
- ab.addSignal(reset);
- ab.addSignal(expire);
-
- AvatarStateMachine asm = ab.getStateMachine();
- AvatarStartState ass = new AvatarStartState("start", _referenceBlock);
-
- asm.setStartState(ass);
- asm.addElement(ass);
-
- AvatarState as1 = new AvatarState("wait4set", _referenceBlock);
- asm.addElement(as1);
-
- AvatarState as2 = new AvatarState("wait4expire", _referenceBlock);
- asm.addElement(as2);
-
- AvatarActionOnSignal aaos1 = new AvatarActionOnSignal("set1", set, _referenceSet);
- aaos1.addValue("value");
- asm.addElement(aaos1);
-
- AvatarActionOnSignal aaos2 = new AvatarActionOnSignal("set2", set, _referenceSet);
- aaos2.addValue("value");
- asm.addElement(aaos2);
-
- AvatarActionOnSignal aaos3 = new AvatarActionOnSignal("reset1", reset, _referenceReset);
- asm.addElement(aaos3);
-
- AvatarActionOnSignal aaos4 = new AvatarActionOnSignal("reset2", reset, _referenceReset);
- asm.addElement(aaos4);
-
- AvatarActionOnSignal aaos5 = new AvatarActionOnSignal("expire", expire, _referenceExpire);
- asm.addElement(aaos5);
-
- AvatarTransition at;
-
- // set
- at = makeAvatarEmptyTransitionBetween(asm, ass, as1, _referenceBlock);
- at = makeAvatarEmptyTransitionBetween(asm, as1, aaos1, _referenceBlock);
- at = makeAvatarEmptyTransitionBetween(asm, aaos1, as2, _referenceBlock);
-
- at = makeAvatarEmptyTransitionBetween(asm, as2, aaos2, _referenceBlock);
- at = makeAvatarEmptyTransitionBetween(asm, aaos2, as2, _referenceBlock);
-
- // expire
- at = makeAvatarEmptyTransitionBetween(asm, as2, aaos5, _referenceBlock);
- at.setDelays("value", "value");
- at = makeAvatarEmptyTransitionBetween(asm, aaos5, as1, _referenceBlock);
-
- // reset
- at = makeAvatarEmptyTransitionBetween(asm, as1, aaos3, _referenceBlock);
- at = makeAvatarEmptyTransitionBetween(asm, aaos3, as1, _referenceBlock);
-
- at = makeAvatarEmptyTransitionBetween(asm, as2, aaos4, _referenceBlock);
- at = makeAvatarEmptyTransitionBetween(asm, aaos4, as1, _referenceBlock);
-
-
- return ab;
-
- }
-
- public static AvatarTransition makeAvatarEmptyTransitionBetween(AvatarStateMachine _asm, AvatarStateMachineElement _elt1, AvatarStateMachineElement _elt2, Object _reference) {
- AvatarTransition at = new AvatarTransition("tr", _reference);
-
- _asm.addElement(at);
-
- _elt1.addNext(at);
- at.addNext(_elt2);
-
- return at;
- }
-}
\ No newline at end of file
+
+ public static AvatarBlock getTimerBlock(String _name, Object _referenceBlock, Object _referenceSet, Object _referenceExpire, Object _referenceReset) {
+ AvatarBlock ab = new AvatarBlock(_name, _referenceBlock);
+
+ /*AvatarAttribute aa2 = new AvatarAttribute("toto", AvatarType.INTEGER, _referenceBlock);
+ ab.addAttribute(aa2);*/
+ AvatarAttribute aa = new AvatarAttribute("value", AvatarType.INTEGER, _referenceBlock);
+ ab.addAttribute(aa);
+ /*AvatarAttribute aa1 = new AvatarAttribute("__value", AvatarType.INTEGER, _referenceBlock);
+ ab.addAttribute(aa1);*/
+
+ AvatarSignal set = new AvatarSignal("set", AvatarSignal.IN, _referenceBlock);
+ AvatarSignal reset = new AvatarSignal("reset", AvatarSignal.IN, _referenceBlock);
+ AvatarSignal expire = new AvatarSignal("expire", AvatarSignal.OUT, _referenceBlock);
+ AvatarAttribute val = new AvatarAttribute("value", AvatarType.INTEGER, aa.getReferenceObject());
+ set.addParameter(val);
+ ab.addSignal(set);
+ ab.addSignal(reset);
+ ab.addSignal(expire);
+
+ AvatarStateMachine asm = ab.getStateMachine();
+ AvatarStartState ass = new AvatarStartState("start", _referenceBlock);
+
+ asm.setStartState(ass);
+ asm.addElement(ass);
+
+ AvatarState as1 = new AvatarState("wait4set", _referenceBlock);
+ asm.addElement(as1);
+
+ AvatarState as2 = new AvatarState("wait4expire", _referenceBlock);
+ asm.addElement(as2);
+
+ AvatarActionOnSignal aaos1 = new AvatarActionOnSignal("set1", set, _referenceSet);
+ aaos1.addValue("value");
+ asm.addElement(aaos1);
+
+ AvatarActionOnSignal aaos2 = new AvatarActionOnSignal("set2", set, _referenceSet);
+ aaos2.addValue("value");
+ asm.addElement(aaos2);
+
+ AvatarActionOnSignal aaos3 = new AvatarActionOnSignal("reset1", reset, _referenceReset);
+ asm.addElement(aaos3);
+
+ AvatarActionOnSignal aaos4 = new AvatarActionOnSignal("reset2", reset, _referenceReset);
+ asm.addElement(aaos4);
+
+ AvatarActionOnSignal aaos5 = new AvatarActionOnSignal("expire", expire, _referenceExpire);
+ asm.addElement(aaos5);
+
+ AvatarTransition at;
+
+ // set
+ at = makeAvatarEmptyTransitionBetween(ab, asm, ass, as1, _referenceBlock);
+ at = makeAvatarEmptyTransitionBetween(ab, asm, as1, aaos1, _referenceBlock);
+ at = makeAvatarEmptyTransitionBetween(ab, asm, aaos1, as2, _referenceBlock);
+
+ at = makeAvatarEmptyTransitionBetween(ab, asm, as2, aaos2, _referenceBlock);
+ at = makeAvatarEmptyTransitionBetween(ab, asm, aaos2, as2, _referenceBlock);
+
+ // expire
+ at = makeAvatarEmptyTransitionBetween(ab, asm, as2, aaos5, _referenceBlock);
+ at.setDelays("value", "value");
+ at = makeAvatarEmptyTransitionBetween(ab, asm, aaos5, as1, _referenceBlock);
+
+ // reset
+ at = makeAvatarEmptyTransitionBetween(ab, asm, as1, aaos3, _referenceBlock);
+ at = makeAvatarEmptyTransitionBetween(ab, asm, aaos3, as1, _referenceBlock);
+
+ at = makeAvatarEmptyTransitionBetween(ab, asm, as2, aaos4, _referenceBlock);
+ at = makeAvatarEmptyTransitionBetween(ab, asm, aaos4, as1, _referenceBlock);
+
+
+ return ab;
+
+ }
+
+ public static AvatarTransition makeAvatarEmptyTransitionBetween(AvatarBlock _block, AvatarStateMachine _asm, AvatarStateMachineElement _elt1, AvatarStateMachineElement _elt2, Object _reference) {
+ AvatarTransition at = new AvatarTransition(_block, "tr", _reference);
+
+ _asm.addElement(at);
+
+ _elt1.addNext(at);
+ at.addNext(_elt2);
+
+ return at;
+ }
+}
diff --git a/src/avatartranslator/AvatarGuard.java b/src/avatartranslator/AvatarGuard.java
new file mode 100644
index 0000000000000000000000000000000000000000..baef0248ebca6f49e88e0adf95d9c1528b68e2e7
--- /dev/null
+++ b/src/avatartranslator/AvatarGuard.java
@@ -0,0 +1,88 @@
+/**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 AvatarGuard
+ * Creation: 16/09/2015
+ * @version 1.0 16/09/2015
+ * @author Florian LUGOU
+ * @see
+ */
+
+
+package avatartranslator;
+
+import myutil.Conversion;
+
+public class AvatarGuard {
+ String guard;
+
+ public AvatarGuard (String _guard) {
+ if (_guard == null)
+ this.guard = "[ ]";
+ else
+ this.guard = _guard;
+ }
+
+ public void addGuard(String _g) {
+ guard = "(" + guard + ") and (" + _g + ")";
+ }
+
+ public boolean isElseGuard () {
+ String _guard = Conversion.replaceAllChar(guard, ' ', "").trim();
+
+ return _guard.compareTo("[else]") == 0;
+ }
+
+ public boolean isNonDeterministicGuard () {
+ String tmp = Conversion.replaceAllChar(guard, ' ', "").trim();
+
+ return tmp.compareTo("[]") == 0;
+ }
+
+ public boolean isGuarded () {
+ if (guard.trim().length() == 0)
+ return false;
+
+ String s = Conversion.replaceAllString(guard, " ", "").trim();
+ return s.compareTo("[]") != 0;
+ }
+
+ public String toString () {
+ return this.guard;
+ }
+}
diff --git a/src/avatartranslator/AvatarLeftHand.java b/src/avatartranslator/AvatarLeftHand.java
new file mode 100644
index 0000000000000000000000000000000000000000..b7594835a155c114585a84ac1d8a111c40ff0345
--- /dev/null
+++ b/src/avatartranslator/AvatarLeftHand.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 AvatarLeftHand
+ * Creation: 16/09/2015
+ * @version 1.0 16/09/2015
+ * @author Florian LUGOU
+ * @see
+ */
+
+
+package avatartranslator;
+
+public interface AvatarLeftHand extends AvatarTerm {
+}
diff --git a/src/avatartranslator/AvatarLocalVar.java b/src/avatartranslator/AvatarLocalVar.java
new file mode 100644
index 0000000000000000000000000000000000000000..7b5e3161f2cbb74a32fafe8d3231f8b388f829c5
--- /dev/null
+++ b/src/avatartranslator/AvatarLocalVar.java
@@ -0,0 +1,67 @@
+/**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 AvatarLocalVar
+ * Creation: 16/09/2015
+ * @version 1.0 16/09/2015
+ * @author Florian LUGOU
+ * @see
+ */
+
+
+package avatartranslator;
+
+public class AvatarLocalVar implements AvatarTerm, AvatarLeftHand {
+ String name;
+
+ public AvatarLocalVar (String _name) {
+ this.name = _name;
+ }
+
+ public String getName () {
+ return this.name;
+ }
+
+ public boolean isLeftHand () {
+ return true;
+ }
+
+ public String toString () {
+ return this.name;
+ }
+}
diff --git a/src/avatartranslator/AvatarMethod.java b/src/avatartranslator/AvatarMethod.java
index 1ad60488cbdc7c4fb365fabb20b677cddab6a913..50173602b23532e02b81da451f074a908020ed9f 100644
--- a/src/avatartranslator/AvatarMethod.java
+++ b/src/avatartranslator/AvatarMethod.java
@@ -1,39 +1,39 @@
/**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.
+ 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 AvatarMethod
@@ -52,114 +52,111 @@ import java.util.*;
import myutil.*;
public class AvatarMethod extends AvatarElement{
-
- protected boolean implementationProvided;
-
- protected LinkedList<AvatarAttribute> parameters;
- protected LinkedList<AvatarAttribute> returnParameters;
-
-
+
+ protected boolean implementationProvided;
+
+ protected LinkedList<AvatarAttribute> parameters;
+ protected LinkedList<AvatarAttribute> returnParameters;
+
+
public AvatarMethod(String _name, Object _referenceObject) {
- super(_name, _referenceObject);
+ super(_name, _referenceObject);
parameters = new LinkedList<AvatarAttribute>();
- returnParameters = new LinkedList<AvatarAttribute>();
+ returnParameters = new LinkedList<AvatarAttribute>();
}
-
+
public void setImplementationProvided(boolean _imp) {
- implementationProvided = _imp;
+ implementationProvided = _imp;
}
-
+
public boolean isImplementationProvided() {
- return implementationProvided;
+ return implementationProvided;
+ }
+
+ public void addParameter(AvatarAttribute _attribute) {
+ parameters.add(_attribute);
+ }
+
+ public void addReturnParameter(AvatarAttribute _attribute) {
+ returnParameters.add(_attribute);
+ }
+
+ public LinkedList<AvatarAttribute> getListOfAttributes() {
+ return parameters;
+ }
+
+ public LinkedList<AvatarAttribute> getListOfReturnAttributes() {
+ return returnParameters;
+ }
+
+ public static boolean isAValidMethodName(String _method) {
+ return AvatarTerm.isValidName (_method);
+ }
+
+ public String toString() {
+ int cpt = 0;
+ String ret = "";
+
+ if (returnParameters.size() != 0) {
+ if (returnParameters.size() == 1) {
+ ret += AvatarType.getStringType(returnParameters.get(0).getType()) + " ";
+ } else {
+ int index = 0;
+ for(AvatarAttribute aa: returnParameters) {
+ if (index == 0) {
+ index ++;
+ } else {
+ ret = ret + ",";
+ }
+ ret += AvatarType.getStringType(aa.getType());
+ }
+ ret = "(" + ret + ") ";
+ }
+
+ }
+
+ ret += getName() + "(";
+
+ for(AvatarAttribute attribute: parameters) {
+ if (cpt != 0) {
+ ret += ",";
+ }
+ cpt ++;
+ ret += attribute.toString();
+ }
+
+ ret += ")";
+ return ret;
+ }
+
+ public boolean isCompatibleWith(AvatarMethod _am) {
+ if (parameters.size() != _am.getListOfAttributes().size()) {
+ return false;
+ }
+
+ AvatarAttribute _ama;
+ int cpt = 0;
+ for(AvatarAttribute aa: parameters) {
+ _ama = _am.getListOfAttributes().get(cpt);
+ if (_ama.getType() != aa.getType()) {
+ return false;
+ }
+ cpt ++;
+ }
+
+ if (returnParameters.size() != _am.getListOfReturnAttributes().size()) {
+ return false;
+ }
+
+ cpt = 0;
+ for(AvatarAttribute aa: returnParameters) {
+ _ama = _am.getListOfReturnAttributes().get(cpt);
+ if (_ama.getType() != aa.getType()) {
+ return false;
+ }
+ cpt ++;
+ }
+
+ return true;
}
-
- public void addParameter(AvatarAttribute _attribute) {
- parameters.add(_attribute);
- }
-
- public void addReturnParameter(AvatarAttribute _attribute) {
- returnParameters.add(_attribute);
- }
-
- public LinkedList<AvatarAttribute> getListOfAttributes() {
- return parameters;
- }
-
- public LinkedList<AvatarAttribute> getListOfReturnAttributes() {
- return returnParameters;
- }
-
- public static boolean isAValidMethodName(String _method) {
- return AvatarAttribute.isAValidAttributeName(_method);
- }
-
- public String toString() {
- int cpt = 0;
- String ret = "";
-
- if (returnParameters.size() != 0) {
- if (returnParameters.size() == 1) {
- ret += AvatarType.getStringType(returnParameters.get(0).getType()) + " ";
- } else {
- int index = 0;
- for(AvatarAttribute aa: returnParameters) {
- if (index == 0) {
- index ++;
- } else {
- ret = ret + ",";
- }
- ret += AvatarType.getStringType(aa.getType());
- }
- ret = "(" + ret + ") ";
- }
-
- }
-
- ret += getName() + "(";
-
- for(AvatarAttribute attribute: parameters) {
- if (cpt != 0) {
- ret += ",";
- }
- cpt ++;
- ret += attribute.toString();
- }
-
- ret += ")";
- return ret;
- }
-
- public boolean isCompatibleWith(AvatarMethod _am) {
- if (parameters.size() != _am.getListOfAttributes().size()) {
- return false;
- }
-
- AvatarAttribute _ama;
- int cpt = 0;
- for(AvatarAttribute aa: parameters) {
- _ama = _am.getListOfAttributes().get(cpt);
- if (_ama.getType() != aa.getType()) {
- return false;
- }
- cpt ++;
- }
-
- if (returnParameters.size() != _am.getListOfReturnAttributes().size()) {
- return false;
- }
-
- cpt = 0;
- for(AvatarAttribute aa: returnParameters) {
- _ama = _am.getListOfReturnAttributes().get(cpt);
- if (_ama.getType() != aa.getType()) {
- return false;
- }
- cpt ++;
- }
-
- return true;
- }
-
-
-
-}
\ No newline at end of file
+}
diff --git a/src/avatartranslator/AvatarRandom.java b/src/avatartranslator/AvatarRandom.java
index a9a73e5af77379964a9eddfd52356b70bc11bdbb..20f4d3904843e630013a60ebf05499dc249d330c 100644
--- a/src/avatartranslator/AvatarRandom.java
+++ b/src/avatartranslator/AvatarRandom.java
@@ -96,4 +96,7 @@ public class AvatarRandom extends AvatarStateMachineElement {
return "Random between " + minValue + " and " + maxValue + " stored in " + variable;
}
-}
\ No newline at end of file
+ public void translate (AvatarTranslator translator, Object arg) {
+ translator.translateRandom (this, arg);
+ }
+}
diff --git a/src/avatartranslator/AvatarSignal.java b/src/avatartranslator/AvatarSignal.java
index b23e3c6d70c09ab3da02b3bda9e42006f16036e2..4de3d311eae1dba9c1c4803360354527c9a9cfc2 100644
--- a/src/avatartranslator/AvatarSignal.java
+++ b/src/avatartranslator/AvatarSignal.java
@@ -82,7 +82,7 @@ public class AvatarSignal extends AvatarMethod {
}
public static boolean isAValidSignal(String _signal) {
- return AvatarAttribute.isAValidAttributeName(_signal);
+ return AvatarTerm.isValidName (_signal);
}
public String toString() {
diff --git a/src/avatartranslator/AvatarSpecification.java b/src/avatartranslator/AvatarSpecification.java
index 9d627b878597114eb33c7f13ac55101764a6fb5c..bcdbf9f804ac2e5b06715f9e447e0cacdcd925eb 100644
--- a/src/avatartranslator/AvatarSpecification.java
+++ b/src/avatartranslator/AvatarSpecification.java
@@ -245,152 +245,6 @@ public class AvatarSpecification extends AvatarElement {
return null;
}
- public static boolean isAVariableSettingString(String _action) {
- int index = _action.indexOf('=');
-
- if (index == -1) {
- return false;
- }
-
- String tmp = _action.substring(index+1, _action.length()).trim();
-
- index = tmp.indexOf('(');
-
- if (index == -1) {
- return true;
- }
-
- tmp = tmp.substring(0, index);
-
- if (AvatarAttribute.isAValidAttributeName(tmp)) {
- return false;
- }
-
- return true;
- }
-
- public static boolean isABasicVariableSettingString(String _action) {
- int index = _action.indexOf('=');
-
- if (index == -1) {
- return false;
- }
-
- String name0 = _action.substring(index+1, _action.length()).trim();
- String name1 = _action.substring(0, index).trim();
-
- if (!AvatarAttribute.isAValidAttributeName(name0)) {
- return false;
- }
-
- if (!AvatarAttribute.isAValidAttributeName(name1)) {
- return false;
- }
-
- return true;
- }
-
- public static String getMethodCallFromAction(String _action) {
- int index = _action.indexOf('=');
- if (index > -1) {
- _action = _action.substring(index+1, _action.length()).trim();
- }
-
- index = _action.indexOf('(');
- if (index == -1) {
- return _action;
- }
- return _action.substring(0, index);
- }
-
- public static int getNbOfParametersInAction(String _action) {
- int index = _action.indexOf('=');
- if (index > -1) {
- _action = _action.substring(index+1, _action.length()).trim();
- }
-
- index = _action.indexOf('(');
- if (index == -1) {
- return 0;
- }
-
- String actions = _action.substring(index+1, _action.length()).trim();
-
- index = actions.indexOf(')');
- if (index == -1) {
- return 0;
- }
-
- actions = actions.substring(0, index).trim();
-
- if (actions.length() == 0) {
- return 0;
- }
-
- int cpt = 1;
- while ((index = actions.indexOf(',')) != -1) {
- cpt ++;
- actions = actions.substring(index+1, actions.length()).trim();
- }
-
- return cpt;
- }
-
- public static int getNbOfReturnParametersInAction(String _action) {
- int index = _action.indexOf('=');
- if (index == -1) {
- return 0;
-
- }
-
- _action = _action.substring(0, index).trim();
-
- index = _action.indexOf('(');
- if (index == -1) {
- return 0;
- }
-
- String actions = _action.substring(index+1, _action.length()).trim();
-
- index = actions.indexOf(')');
- if (index == -1) {
- return 0;
- }
-
- actions = actions.substring(0, index).trim();
-
- if (actions.length() == 0) {
- return 0;
- }
-
- int cpt = 1;
- while ((index = actions.indexOf(',')) != -1) {
- cpt ++;
- actions = actions.substring(index+1, actions.length()).trim();
- }
-
- return cpt;
- }
-
- public static String getParameterInAction(String _action, int _index) {
- int nb = getNbOfParametersInAction(_action);
- if (!(_index < nb) || (_index < 0)) {
- return null;
- }
-
- int index = _action.indexOf('=');
- if (index > -1) {
- _action = _action.substring(index+1, _action.length()).trim();
- }
-
- int index1 = _action.indexOf('(');
- int index2 = _action.indexOf(')');
- String actions = _action.substring(index1+1, index2).trim();
- String actionss[] = actions.split(",");
- return actionss[_index].trim();
-
- }
-
public AvatarStateMachineElement getStateMachineElementFromReferenceObject(Object _o) {
AvatarStateMachineElement asme;
for(AvatarBlock block: blocks) {
@@ -436,27 +290,14 @@ public class AvatarSpecification extends AvatarElement {
return null;
}
- public static boolean isElseGuard(String _guard) {
- if (_guard == null) {
- return false;
- }
-
- String guard = Conversion.replaceAllChar(_guard, ' ', "").trim();
-
- return guard.compareTo("[else]") == 0;
- }
-
public boolean hasLossyChannel() {
- for(AvatarRelation relation: relations) {
- if (relation.isLossy()) {
+ for(AvatarRelation relation: relations)
+ if (relation.isLossy())
return true;
- }
- }
return false;
}
-
public void makeRobustness() {
TraceManager.addDev("Make robustness");
if (robustnessMade) {
diff --git a/src/avatartranslator/AvatarStartState.java b/src/avatartranslator/AvatarStartState.java
index 232bbcb941ed26e58acc6be50bd6a3685bf844fa..35946f6a6a0d5a1e55294ca51d27cf91dd92c00e 100644
--- a/src/avatartranslator/AvatarStartState.java
+++ b/src/avatartranslator/AvatarStartState.java
@@ -63,4 +63,7 @@ public class AvatarStartState extends AvatarStateMachineElement {
return "Start state";
}
+ public void translate (AvatarTranslator translator, Object arg) {
+ translator.translateStartState (this, arg);
+ }
}
diff --git a/src/avatartranslator/AvatarState.java b/src/avatartranslator/AvatarState.java
index 54de3c13cfd95a69d74689f57ba99183fa2b3ccd..c43343874f8f0a37a284a93124fd3114dc6f734b 100644
--- a/src/avatartranslator/AvatarState.java
+++ b/src/avatartranslator/AvatarState.java
@@ -118,4 +118,8 @@ public class AvatarState extends AvatarStateMachineElement {
}
return entryCode;
}
+
+ public void translate (AvatarTranslator translator, Object arg) {
+ translator.translateState (this, arg);
+ }
}
diff --git a/src/avatartranslator/AvatarStateMachine.java b/src/avatartranslator/AvatarStateMachine.java
index 5641ed591ea087088a37898c5158a1f15359daca..ffe9118d500b39912d8457ae0e4d43f8e6109273 100644
--- a/src/avatartranslator/AvatarStateMachine.java
+++ b/src/avatartranslator/AvatarStateMachine.java
@@ -84,6 +84,26 @@ public class AvatarStateMachine extends AvatarElement {
return elements;
}
+ private void getSimplifiedElementsAux (HashMap<AvatarStateMachineElement, Integer> simplifiedElements, HashSet<AvatarStateMachineElement> visited, AvatarStateMachineElement root) {
+ if (visited.contains (root)) {
+ Integer name = simplifiedElements.get (root);
+ if (name == null)
+ simplifiedElements.put (root, new Integer (simplifiedElements.size ()));
+ }
+ else {
+ visited.add (root);
+ for (AvatarStateMachineElement asme: root.nexts)
+ this.getSimplifiedElementsAux (simplifiedElements, visited, asme);
+ }
+ }
+
+ public HashMap<AvatarStateMachineElement, Integer> getSimplifiedElements () {
+ HashMap<AvatarStateMachineElement, Integer> simplifiedElements = new HashMap<AvatarStateMachineElement, Integer> ();
+ simplifiedElements.put (startState, new Integer (0));
+ this.getSimplifiedElementsAux (simplifiedElements, new HashSet<AvatarStateMachineElement> (), startState);
+ return simplifiedElements;
+ }
+
public String toString() {
StringBuffer sb = new StringBuffer("State machine Id=" + getID() + "\n");
@@ -303,7 +323,7 @@ public class AvatarStateMachine extends AvatarElement {
addElement(as);
as.setHidden(true);
as.setState(_currentState);
- AvatarTransition atn = new AvatarTransition("splittransition_after", null);
+ AvatarTransition atn = new AvatarTransition(_at.getBlock (), "splittransition_after", null);
addElement(atn);
element.removeNext(_at);
element.addNext(atn);
@@ -583,7 +603,7 @@ public class AvatarStateMachine extends AvatarElement {
addElement(as);
as.setHidden(true);
as.setState(_currentState);
- AvatarTransition atn = new AvatarTransition("internaltransition", null);
+ AvatarTransition atn = new AvatarTransition(_at.getBlock(), "internaltransition", null);
addElement(atn);
element.removeNext(_at);
element.addNext(atn);
@@ -612,7 +632,7 @@ public class AvatarStateMachine extends AvatarElement {
as = new AvatarState(tmp, null);
addElement(as);
as.setHidden(true);
- at = new AvatarTransition("internaltransition", null);
+ at = new AvatarTransition(_at.getBlock (), "internaltransition", null);
addElement(at);
//_element -> at -> as -> element
@@ -634,7 +654,7 @@ public class AvatarStateMachine extends AvatarElement {
as = new AvatarState(tmp, null);
addElement(as);
as.setHidden(true);
- at = new AvatarTransition("internaltransition", null);
+ at = new AvatarTransition(_at.getBlock (), "internaltransition", null);
addElement(at);
//_element -> at -> as -> element
@@ -912,8 +932,8 @@ public class AvatarStateMachine extends AvatarElement {
ast.setTimerValue(val.getName());
ast.setTimer(aa);
- newat0 = new AvatarTransition("transition_settimer_" + aa.getName(), _block.getReferenceObject());
- newat1 = new AvatarTransition("transition_settimer_" + aa.getName(), _block.getReferenceObject());
+ newat0 = new AvatarTransition(_block, "transition_settimer_" + aa.getName(), _block.getReferenceObject());
+ newat1 = new AvatarTransition(_block, "transition_settimer_" + aa.getName(), _block.getReferenceObject());
elements.add(ar);
elements.add(ast);
@@ -932,8 +952,8 @@ public class AvatarStateMachine extends AvatarElement {
// Wait for timer expiration on the transition
AvatarExpireTimer aet = new AvatarExpireTimer("expiretimer_" + aa.getName(), _block.getReferenceObject());
aet.setTimer(aa);
- newat0 = new AvatarTransition("transition0_expiretimer_" + aa.getName(), _block.getReferenceObject());
- newat1 = new AvatarTransition("transition1_expiretimer_" + aa.getName(), _block.getReferenceObject());
+ newat0 = new AvatarTransition(_block, "transition0_expiretimer_" + aa.getName(), _block.getReferenceObject());
+ newat1 = new AvatarTransition(_block, "transition1_expiretimer_" + aa.getName(), _block.getReferenceObject());
as = new AvatarState("state1_expiretimer_" + aa.getName(), _block.getReferenceObject());
addElement(aet);
addElement(newat0);
@@ -1004,7 +1024,7 @@ public class AvatarStateMachine extends AvatarElement {
AvatarState myState = new AvatarState("statefortransition__" + ID_ELT, _at.getReferenceObject());
myState.setHidden(true);
- AvatarTransition at2 = new AvatarTransition("transitionfortransition__" + ID_ELT, _at.getReferenceObject());
+ AvatarTransition at2 = new AvatarTransition(_at.getBlock (), "transitionfortransition__" + ID_ELT, _at.getReferenceObject());
ID_ELT ++;
AvatarTransition at1 = (AvatarTransition)(next.getNext(0));
@@ -1019,7 +1039,7 @@ public class AvatarStateMachine extends AvatarElement {
return;
} else {
AvatarState myState = new AvatarState("statefortransition__" + ID_ELT, _at.getReferenceObject());
- AvatarTransition at = new AvatarTransition("transitionfortransition__", _at.getReferenceObject());
+ AvatarTransition at = new AvatarTransition(_at.getBlock (), "transitionfortransition__", _at.getReferenceObject());
at.addNext(_at.getNext(0));
_at.removeAllNexts();
_at.addNext(myState);
@@ -1154,10 +1174,10 @@ public class AvatarStateMachine extends AvatarElement {
return name + id;
}
- public void handleUnfollowedStartState() {
+ public void handleUnfollowedStartState(AvatarBlock _block) {
if (startState.nbOfNexts() == 0) {
AvatarStopState stopState = new AvatarStopState("__StopState", startState.getReferenceObject());
- AvatarTransition at = new AvatarTransition("__toStop", startState.getReferenceObject());
+ AvatarTransition at = new AvatarTransition(_block, "__toStop", startState.getReferenceObject());
addElement(stopState);
addElement(at);
startState.addNext(at);
diff --git a/src/avatartranslator/AvatarStateMachineElement.java b/src/avatartranslator/AvatarStateMachineElement.java
index 2db0dc1948bdd9af1095c6a8bd2d62b7d4da0f2b..cfbb17e16b0b352d011342aa16fb3c262681f2d6 100644
--- a/src/avatartranslator/AvatarStateMachineElement.java
+++ b/src/avatartranslator/AvatarStateMachineElement.java
@@ -246,8 +246,8 @@ public abstract class AvatarStateMachineElement extends AvatarElement {
}
String g1, g2;
- g1 = at1.getGuard();
- g2 = at2.getGuard();
+ g1 = at1.getGuard().toString ();
+ g2 = at2.getGuard().toString ();
g1 = Conversion.replaceAllString(g1, "[", "");
g1 = Conversion.replaceAllString(g1, "]", "").trim();
@@ -327,5 +327,7 @@ public abstract class AvatarStateMachineElement extends AvatarElement {
public abstract String getNiceName();
+ public abstract void translate (AvatarTranslator translator, Object arg);
+
}
diff --git a/src/avatartranslator/AvatarStopState.java b/src/avatartranslator/AvatarStopState.java
index c05e03f72c03efd59b454792b00264f3fc142719..aa57c9181df3fc40499bdde95ef42742dd7996d5 100644
--- a/src/avatartranslator/AvatarStopState.java
+++ b/src/avatartranslator/AvatarStopState.java
@@ -49,18 +49,21 @@ import java.util.*;
public class AvatarStopState extends AvatarStateMachineElement {
-
-
+
+
public AvatarStopState(String _name, Object _referenceObject) {
super(_name, _referenceObject);
}
-
- public AvatarStateMachineElement basicCloneMe() {
- return new AvatarStopState(getName(), getReferenceObject());
- }
-
- public String getNiceName() {
- return "Stop state";
- }
-
+
+ public AvatarStateMachineElement basicCloneMe() {
+ return new AvatarStopState(getName(), getReferenceObject());
+ }
+
+ public String getNiceName() {
+ return "Stop state";
+ }
+
+ public void translate (AvatarTranslator translator, Object arg) {
+ translator.translateStopState (this, arg);
+ }
}
diff --git a/src/avatartranslator/AvatarTerm.java b/src/avatartranslator/AvatarTerm.java
new file mode 100644
index 0000000000000000000000000000000000000000..dd6b464182e6e36f7243f8027bca4da6171011a8
--- /dev/null
+++ b/src/avatartranslator/AvatarTerm.java
@@ -0,0 +1,95 @@
+/**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 AvatarTerm
+ * Creation: 16/09/2015
+ * @version 1.0 16/09/2015
+ * @author Florian LUGOU
+ * @see
+ */
+
+
+package avatartranslator;
+
+import myutil.TraceManager;
+import translator.RTLOTOSKeyword;
+import translator.tojava.JKeyword;
+
+public interface AvatarTerm {
+ public boolean isLeftHand ();
+ public String getName ();
+
+ public static AvatarTerm createFromString (AvatarBlock block, String toParse) {
+ AvatarTerm result = AvatarTermFunction.createFromString (block, toParse);
+ if (result != null)
+ return result;
+
+ result = AvatarTuple.createFromString (block, toParse);
+ if (result != null)
+ return result;
+
+ toParse = toParse.trim ();
+ result = block.getAvatarAttributeWithName (toParse);
+ if (result != null)
+ return result;
+ TraceManager.addDev ("AvatarAttribute '" + toParse + "' couldn't be parsed");
+
+ if (isValidName (toParse))
+ return new AvatarLocalVar (toParse);
+ TraceManager.addDev ("AvatarLocalVar '" + toParse + "' couldn't be parsed");
+
+ TraceManager.addDev ("AvatarTerm '" + toParse + "' couldn't be parsed");
+ return null;
+ }
+
+ public static boolean isValidName (String _name) {
+ String toParse = _name.trim ();
+ String lowerid = toParse.toLowerCase();
+ boolean b1, b2, b3, b4, b5;
+ b1 = (toParse.substring(0,1)).matches("[a-zA-Z]");
+ b2 = toParse.matches("\\w*");
+ b3 = !RTLOTOSKeyword.isAKeyword(lowerid);
+ b4 = true;
+ for (int i=0; i<5; i++)
+ if (lowerid.equals(AvatarType.getStringType(i).toLowerCase()))
+ b4 = false;
+ b5 = !JKeyword.isAKeyword(lowerid);
+
+ return (b1 && b2 && b3 && b4 && b5);
+ }
+}
diff --git a/src/avatartranslator/AvatarTermFunction.java b/src/avatartranslator/AvatarTermFunction.java
new file mode 100644
index 0000000000000000000000000000000000000000..6e5825a0c6f753138d99cfc6aa2ca01bd19a78a9
--- /dev/null
+++ b/src/avatartranslator/AvatarTermFunction.java
@@ -0,0 +1,113 @@
+/**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 AvatarTermFunction
+ * Creation: 16/09/2015
+ * @version 1.0 16/09/2015
+ * @author Florian LUGOU
+ * @see
+ */
+
+package avatartranslator;
+
+import java.util.LinkedList;
+import myutil.TraceManager;
+
+public class AvatarTermFunction extends AvatarAction implements AvatarTerm {
+ AvatarTuple args;
+ AvatarMethod method;
+
+ public AvatarTermFunction (AvatarMethod _method, AvatarTuple _args) {
+ this.args = _args;
+ this.method = _method;
+ }
+
+ public static AvatarTermFunction createFromString (AvatarBlock block, String toParse) {
+ int indexLParen = toParse.indexOf ("(");
+ String methodName;
+ AvatarTuple argsTuple;
+
+ if (indexLParen == -1) {
+ // No left parenthesis: this must be a 0-arity function call
+ methodName = toParse.trim ();
+ argsTuple = new AvatarTuple ();
+ }
+ else {
+ // Left parenthesis present
+ methodName = toParse.substring (0, indexLParen).trim ();
+ argsTuple = AvatarTuple.createFromString (block, toParse.substring (indexLParen));
+ }
+
+ AvatarMethod meth = block.getAvatarMethodWithName (methodName);
+ if (meth != null && argsTuple != null && meth.getListOfAttributes ().size () == argsTuple.getComponents ().size ())
+ // Method was found and the arguments provided are correct
+ return new AvatarTermFunction (meth, argsTuple);
+
+ TraceManager.addDev ("Function call '" + toParse + "' couldn't be parsed");
+
+ return null;
+ }
+
+ public AvatarMethod getMethod () {
+ return this.method;
+ }
+
+ public LinkedList<AvatarTerm> getArgs () {
+ return this.args.getComponents ();
+ }
+
+ public void addArgument (AvatarTerm term) {
+ this.args.addComponent (term);
+ }
+
+ public boolean isAMethodCall () {
+ return true;
+ }
+
+ public boolean isLeftHand () {
+ return false;
+ }
+
+ public String getName () {
+ return this.toString ();
+ }
+
+ public String toString () {
+ return this.method.getName () + " " + this.args.toString ();
+ }
+}
diff --git a/src/avatartranslator/AvatarTimerOperator.java b/src/avatartranslator/AvatarTimerOperator.java
index eb7d16d262ff1f063ac3f938a60f248eca2e707c..d625ebbc523a97731a8af9c72c6b3828ef4fdf31 100644
--- a/src/avatartranslator/AvatarTimerOperator.java
+++ b/src/avatartranslator/AvatarTimerOperator.java
@@ -70,5 +70,8 @@ public abstract class AvatarTimerOperator extends AvatarStateMachineElement {
return "";
}
-
-}
\ No newline at end of file
+
+ public void translate (AvatarTranslator translator, Object arg) {
+ translator.translateTimerOperator (this, arg);
+ }
+}
diff --git a/src/avatartranslator/AvatarTransition.java b/src/avatartranslator/AvatarTransition.java
index 7e8dc9073d5890d0368421f66d349edb2e0e9062..9018ee7bbea3c57ea67a55231b8251c2a3d05c67 100644
--- a/src/avatartranslator/AvatarTransition.java
+++ b/src/avatartranslator/AvatarTransition.java
@@ -51,41 +51,110 @@ import myutil.*;
public class AvatarTransition extends AvatarStateMachineElement {
- private String guard = "[ ]";
+ private AvatarGuard guard;
private String minDelay = "", maxDelay = "";
private String minCompute = "", maxCompute = "";
+ private AvatarBlock block;
- private LinkedList<String> actions; // actions on variable, or method call
+ private LinkedList<AvatarAction> actions; // actions on variable, or method call
- public AvatarTransition(String _name, Object _referenceObject) {
+ public AvatarTransition(AvatarBlock _block, String _name, Object _referenceObject) {
super(_name, _referenceObject);
- actions = new LinkedList<String>();
+ actions = new LinkedList<AvatarAction>();
+ this.guard = new AvatarGuard ("[ ]");
+ this.block = _block;
}
-
- public String getGuard() {
+ public AvatarGuard getGuard() {
return guard;
}
- public void setGuard(String _guard) {
- guard = _guard;
+ public void setGuard(AvatarGuard _guard) {
+ this.guard = _guard;
}
+ public void setGuard (String _guard) {
+ this.guard = new AvatarGuard (_guard);
+ }
public void addGuard(String _g) {
- guard = "(" + guard + ") and (" + _g + ")";
+ this.guard.addGuard (_g);
}
public int getNbOfAction() {
return actions.size();
}
- public String getAction(int _index) {
+ public LinkedList<AvatarAction> getActions () {
+ return this.actions;
+ }
+
+ public AvatarBlock getBlock () {
+ return this.block;
+ }
+
+ private <T extends AvatarAction> Iterable<T> getIterableForClass (Class<T> childClass) {
+ return new Iterable<T> () {
+ public Iterator<T> iterator () {
+ return new Iterator<T> () {
+ private Iterator<AvatarAction> actions = AvatarTransition.this.actions.iterator ();
+ private boolean hasCached = false;
+ private T cached;
+
+ public boolean hasNext () {
+ if (this.hasCached)
+ return true;
+ while (this.actions.hasNext ()) {
+ AvatarAction action = this.actions.next ();
+ if (childClass.isInstance (action)) {
+ this.hasCached = true;
+ this.cached = childClass.cast (action);
+ return true;
+ }
+ }
+ return false;
+ }
+
+ public T next () {
+ if (this.hasCached) {
+ this.hasCached = false;
+ return this.cached;
+ }
+
+ while (this.actions.hasNext ()) {
+ AvatarAction action = this.actions.next ();
+ if (childClass.isInstance (action))
+ return childClass.cast (action);
+ }
+
+ return null;
+ }
+ };
+ }
+ };
+ }
+
+ public Iterable<AvatarTermFunction> getFunctionCalls () {
+ return this.getIterableForClass (AvatarTermFunction.class);
+ }
+
+ public Iterable<AvatarActionAssignment> getAssignments () {
+ return this.getIterableForClass (AvatarActionAssignment.class);
+ }
+
+ public AvatarAction getAction(int _index) {
return actions.get(_index);
}
public void addAction(String _action) {
- actions.add(_action);
+ AvatarAction aa = AvatarAction.createFromString (block, _action);
+ if (aa != null)
+ actions.add(aa);
+ }
+
+ public void addAction (AvatarAction _action) {
+ if (_action != null)
+ this.actions.add (_action);
}
public void setDelays(String _minDelay, String _maxDelay) {
@@ -117,26 +186,21 @@ public class AvatarTransition extends AvatarStateMachineElement {
if (maxCompute.trim().length() ==0) {
return getMinCompute();
}
- return maxCompute;
- }
+ return maxCompute; }
public boolean hasElseGuard() {
if (guard == null) {
return false;
}
- return AvatarSpecification.isElseGuard(guard);
+ return guard.isElseGuard();
}
public boolean hasNonDeterministicGuard() {
- if (guard == null) {
+ if (guard == null)
return false;
- }
-
- String tmp = Conversion.replaceAllChar(guard, ' ', "").trim();
-
- return tmp.compareTo("[]") == 0;
+ return guard.isNonDeterministicGuard ();
}
public boolean isEmpty() {
@@ -149,7 +213,7 @@ public class AvatarTransition extends AvatarStateMachineElement {
public AvatarTransition cloneMe() {
- AvatarTransition at = new AvatarTransition(getName(), getReferenceObject());
+ AvatarTransition at = new AvatarTransition(block, getName(), getReferenceObject());
at.setGuard(getGuard());
at.setDelays(getMinDelay(), getMaxDelay());
at.setComputes(getMinCompute(), getMaxCompute());
@@ -166,7 +230,7 @@ public class AvatarTransition extends AvatarStateMachineElement {
}
public AvatarStateMachineElement basicCloneMe() {
- AvatarTransition at = new AvatarTransition(getName() + "_clone", getReferenceObject());
+ AvatarTransition at = new AvatarTransition(block, getName() + "_clone", getReferenceObject());
at.setGuard(getGuard());
@@ -183,7 +247,7 @@ public class AvatarTransition extends AvatarStateMachineElement {
if (actions.size() < 2) {
return;
}
- String action = actions.get(0);
+ AvatarAction action = actions.get(0);
actions.clear();
actions.add(action);
}
@@ -201,20 +265,10 @@ public class AvatarTransition extends AvatarStateMachineElement {
//}
public boolean isGuarded() {
- if (guard == null) {
+ if (guard == null)
return false;
- }
-
- if (guard.trim().length() == 0) {
- return false;
- }
- String s = Conversion.replaceAllString(guard, " ", "").trim();
- if (s.compareTo("[]") == 0) {
- return false;
- }
-
- return true;
+ return guard.isGuarded ();
}
public boolean hasDelay() {
@@ -237,8 +291,8 @@ public class AvatarTransition extends AvatarStateMachineElement {
return false;
}
- for(String s: actions) {
- if (s.trim().length() > 0) {
+ for(AvatarAction a: actions) {
+ if (a.toString ().trim().length() > 0) {
return true;
}
}
@@ -256,7 +310,8 @@ public class AvatarTransition extends AvatarStateMachineElement {
ret += "minCompute=" + getMinCompute() + " maxcompute=" + getMaxCompute() + "\n";
}
- for(String s: actions) {
+ for(AvatarAction a: actions) {
+ String s = a.toString ();
if (s.trim().length() > 0) {
ret += s.trim() + " / ";
}
@@ -273,40 +328,9 @@ public class AvatarTransition extends AvatarStateMachineElement {
// Assumes actions are correctly formatted
public boolean hasMethodCall() {
-
- for(String action: actions) {
- if (isAMethodCall(action)) {
- return true;
- }
- }
- return false;
-
- }
-
- public static boolean isAMethodCall(String _action) {
- int index;
- index = _action.indexOf("=");
-
- // Method of the form f(...)
- if (index == -1) {
- return true;
- }
-
- // Method of the form x = f(...)
- _action = _action.substring(index+1, _action.length()).trim();
- index = _action.indexOf("(");
- if (index != -1) {
- _action = _action.substring(0, index).trim();
- if (_action.length() == 0) {
- return false;
-
- }
- boolean b1 = (_action.substring(0,1)).matches("[a-zA-Z]");
- boolean b2 = _action.matches("\\w*");
- if (b1 && b2) {
+ for(AvatarAction action: actions)
+ if (action.isAMethodCall())
return true;
- }
- }
return false;
}
@@ -325,19 +349,7 @@ public class AvatarTransition extends AvatarStateMachineElement {
return "Empty transition";
}
- public static String getVariableInAction(String action) {
- action = action.trim();
- int index = action.indexOf("=");
- if (index == -1) {
- return action;
- }
-
- return action.substring(0, index).trim();
+ public void translate (AvatarTranslator translator, Object arg) {
+ translator.translateTransition (this, arg);
}
-
-
-
-
-
-
}
diff --git a/src/avatartranslator/AvatarTranslator.java b/src/avatartranslator/AvatarTranslator.java
new file mode 100644
index 0000000000000000000000000000000000000000..7f036d2a235c67453af38b89c1eac6172716889d
--- /dev/null
+++ b/src/avatartranslator/AvatarTranslator.java
@@ -0,0 +1,56 @@
+/**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 AvatarTranslator
+ * Creation: 16/09/2015
+ * @version 1.0 16/09/2015
+ * @author Florian LUGOU
+ * @see
+ */
+
+package avatartranslator;
+
+public interface AvatarTranslator {
+ public void translateTimerOperator (AvatarTimerOperator _asme, Object _arg);
+ public void translateActionOnSignal (AvatarActionOnSignal _asme, Object _arg);
+ public void translateTransition (AvatarTransition _asme, Object _arg);
+ public void translateStartState (AvatarStartState _asme, Object _arg);
+ public void translateState (AvatarState _asme, Object _arg);
+ public void translateRandom (AvatarRandom _asme, Object _arg);
+ public void translateStopState (AvatarStopState _asme, Object _arg);
+}
diff --git a/src/avatartranslator/AvatarTuple.java b/src/avatartranslator/AvatarTuple.java
new file mode 100644
index 0000000000000000000000000000000000000000..aa06c6ef0db7499b80dd5d3197a2ab7edee407cb
--- /dev/null
+++ b/src/avatartranslator/AvatarTuple.java
@@ -0,0 +1,125 @@
+/**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 AvatarTuple
+ * Creation: 16/09/2015
+ * @version 1.0 16/09/2015
+ * @author Florian LUGOU
+ * @see
+ */
+
+
+package avatartranslator;
+
+import java.util.LinkedList;
+import myutil.TraceManager;
+
+public class AvatarTuple implements AvatarTerm, AvatarLeftHand {
+ LinkedList<AvatarTerm> components;
+
+ public AvatarTuple () {
+ this.components = new LinkedList<AvatarTerm> ();
+ }
+
+ public static AvatarTuple createFromString (AvatarBlock block, String toParse) {
+ AvatarTuple result = null;
+
+ int indexLParen = toParse.indexOf ("(");
+ if (indexLParen != -1) {
+ int indexRParen = toParse.indexOf (")", indexLParen);
+ if (indexRParen == -1)
+ indexRParen = toParse.length ();
+ String[] components = toParse.substring (indexLParen+1, indexRParen).split (",");
+
+ boolean illFormed = false;
+ AvatarTuple argsTuple = new AvatarTuple ();
+ for (String arg: components) {
+ AvatarTerm t = AvatarTerm.createFromString (block, arg);
+ if (t == null) {
+ // Term couldn't be parsed
+ illFormed = true;
+ break;
+ }
+
+ argsTuple.addComponent (t);
+ }
+
+ if (!illFormed)
+ // Every argument was correctly parsed
+ result = argsTuple;
+ }
+
+ if (result == null)
+ TraceManager.addDev ("Tuple '" + toParse + "' couldn't be parsed");
+
+ return result;
+ }
+
+ public void addComponent (AvatarTerm term) {
+ this.components.add (term);
+ }
+
+ public LinkedList<AvatarTerm> getComponents () {
+ return this.components;
+ }
+
+ public String getName () {
+ return this.toString ();
+ }
+
+ public String toString () {
+ String result = "(";
+ boolean first = true;
+ for (AvatarTerm term: components) {
+ if (first)
+ first = false;
+ else
+ result += ", ";
+ result += term.getName ();
+ }
+
+ return result + ")";
+ }
+
+ public boolean isLeftHand () {
+ for (AvatarTerm term: this.components)
+ if (!(term instanceof AvatarLocalVar))
+ return false;
+ return true;
+ }
+}
diff --git a/src/avatartranslator/directsimulation/AvatarSimulationBlock.java b/src/avatartranslator/directsimulation/AvatarSimulationBlock.java
index 7260d21121a82a44f241651c22eb491baa0010df..6c375de514110a1697b242e6a975b070ea7e741b 100644
--- a/src/avatartranslator/directsimulation/AvatarSimulationBlock.java
+++ b/src/avatartranslator/directsimulation/AvatarSimulationBlock.java
@@ -174,7 +174,7 @@ public class AvatarSimulationBlock {
AvatarTransition at = (AvatarTransition)(asme);
if (at.isGuarded()) {
// Must evaluate the guard
- String guard = at.getGuard();
+ String guard = at.getGuard().toString ();
String s = Conversion.replaceAllString(guard, "[", "").trim();
s = Conversion.replaceAllString(s, "]", "").trim();
guardOk = evaluateBoolExpression(s, lastTransaction.attributeValues);
@@ -352,7 +352,7 @@ public class AvatarSimulationBlock {
if (at.hasActions()) {
actions = new Vector<String>();
for(i=0; i<at.getNbOfAction(); i++) {
- action = at.getAction(i);
+ action = at.getAction(i).toString ();
//TraceManager.addDev("action #" + i + " = " + action);
makeAction(action, attributeValues, actions);
}
@@ -535,7 +535,9 @@ public class AvatarSimulationBlock {
String nameOfMethod;
int ind;
- if (AvatarTransition.isAMethodCall(_action)) {
+ AvatarAction action = AvatarAction.createFromString (block, _action);
+ // TODO: use the new AvatarAction class instead of re-parsing
+ if (action.isAMethodCall ()) {
// Evaluate all elements of the method call!
ind = _action.indexOf("(");
if (ind == -1) {
diff --git a/src/avatartranslator/toexecutable/AVATAR2CPOSIX.java b/src/avatartranslator/toexecutable/AVATAR2CPOSIX.java
index ce9358f87d3914d792a903d877c48f9c868a43c4..4b2b70e00a15b9d05f623e008da214a413105874 100755
--- a/src/avatartranslator/toexecutable/AVATAR2CPOSIX.java
+++ b/src/avatartranslator/toexecutable/AVATAR2CPOSIX.java
@@ -506,7 +506,7 @@ public class AVATAR2CPOSIX {
AvatarTransition at = (AvatarTransition)_asme;
if (at.isGuarded()) {
- String g = modifyGuard(at.getGuard());
+ String g = modifyGuard(at.getGuard().toString ());
ret += "if (!" + g + ") {" + CR;
if (debug) {
@@ -654,7 +654,7 @@ public class AVATAR2CPOSIX {
aaos = (AvatarActionOnSignal)(_at.getNext(0));
if (_at.isGuarded()) {
- String g = modifyGuard(_at.getGuard());
+ String g = modifyGuard(_at.getGuard().toString ());
ret += "if (" + g + ") {" + CR;
}
@@ -734,7 +734,7 @@ public class AVATAR2CPOSIX {
private String makeImmediateAction(AvatarTransition _at, int _index) {
String ret = "";
if (_at.isGuarded()) {
- String g = modifyGuard(_at.getGuard());
+ String g = modifyGuard(_at.getGuard().toString ());
ret += "if (" + g + ") {" + CR;
}
@@ -947,33 +947,28 @@ public class AVATAR2CPOSIX {
public String makeActionsOfTransaction(AvatarBlock _block, AvatarTransition _at) {
String ret = "";
- String act;
- String var;
String type;
for(int i=0; i<_at.getNbOfAction(); i++) {
// Must know whether this is an action or a method call
- act = _at.getAction(i);
- if (_at.isAMethodCall(act)) {
- ret += modifyMethodName(_block, act) + ";" + CR;
+ AvatarAction act = _at.getAction(i);
+ if (act.isAMethodCall()) {
+ ret += modifyMethodName(_block, act.toString ()) + ";" + CR;
} else {
- ret += act + ";" + CR;
- var = _at.getVariableInAction(act);
- AvatarAttribute aa;
- aa = _block.getAvatarAttributeWithName(var);
- if (aa != null) {
- if (aa.isInt()) {
- type = "0";
- } else {
- type = "1";
- }
- //ret += "sprintf(__value, \"%d\", " + var + ");" + CR;
- ret += traceVariableModification(_block.getName(), var, type);
+ AvatarLeftHand leftHand = ((AvatarActionAssignment) act).getLeftHand ();
+ ret += act.toString () + ";" + CR;
+ if (leftHand instanceof AvatarAttribute) {
+ if (((AvatarAttribute) leftHand).isInt()) {
+ type = "0";
+ } else {
+ type = "1";
}
-
+ ret += traceVariableModification(_block.getName(), leftHand.toString (), type);
+ }
+
}
}
-
+
return ret;
}
-
-}
\ No newline at end of file
+
+}
diff --git a/src/avatartranslator/toexecutable/AVATAR2SOCLIB.java b/src/avatartranslator/toexecutable/AVATAR2SOCLIB.java
index 5f94aaf57da7257ded69130d77bba4ca0f7547c1..1d23a128191e20bd240a0827063e9966b711d6b9 100644
--- a/src/avatartranslator/toexecutable/AVATAR2SOCLIB.java
+++ b/src/avatartranslator/toexecutable/AVATAR2SOCLIB.java
@@ -608,7 +608,7 @@ public class AVATAR2SOCLIB {
AvatarTransition at = (AvatarTransition)_asme;
if (at.isGuarded()) {
- String g = modifyGuard(at.getGuard());
+ String g = modifyGuard(at.getGuard().toString ());
ret += "if (!" + g + ") {" + CR;
if (debug) {
@@ -755,7 +755,7 @@ public class AVATAR2SOCLIB {
aaos = (AvatarActionOnSignal)(_at.getNext(0));
if (_at.isGuarded()) {
- String g = modifyGuard(_at.getGuard());
+ String g = modifyGuard(_at.getGuard().toString ());
ret += "if (" + g + ") {" + CR;
}
@@ -868,7 +868,7 @@ public class AVATAR2SOCLIB {
private String makeImmediateAction(AvatarTransition _at, int _index) {
String ret = "";
if (_at.isGuarded()) {
- String g = modifyGuard(_at.getGuard());
+ String g = modifyGuard(_at.getGuard().toString ());
ret += "if (" + g + ") {" + CR;
}
@@ -1118,27 +1118,23 @@ public class AVATAR2SOCLIB {
public String makeActionsOfTransaction(AvatarBlock _block, AvatarTransition _at) {
String ret = "";
- String act;
- String var;
String type;
for(int i=0; i<_at.getNbOfAction(); i++) {
// Must know whether this is an action or a method call
- act = _at.getAction(i);
- if (_at.isAMethodCall(act)) {
- ret += modifyMethodName(_block, act) + ";" + CR;
+ AvatarAction act = _at.getAction(i);
+ if (act.isAMethodCall()) {
+ ret += modifyMethodName(_block, act.toString ()) + ";" + CR;
} else {
- ret += act + ";" + CR;
- var = _at.getVariableInAction(act);
- AvatarAttribute aa;
- aa = _block.getAvatarAttributeWithName(var);
- if (aa != null) {
- if (aa.isInt()) {
+ ret += act.toString () + ";" + CR;
+ AvatarLeftHand leftHand = ((AvatarActionAssignment) act).getLeftHand ();
+ if (leftHand instanceof AvatarAttribute) {
+ if (((AvatarAttribute) leftHand).isInt()) {
type = "0";
} else {
type = "1";
}
//ret += "sprintf(__value, \"%d\", " + var + ");" + CR;
- ret += traceVariableModification(_block.getName(), var, type);
+ ret += traceVariableModification(_block.getName(), leftHand.toString (), type);
}
}
diff --git a/src/avatartranslator/toproverif/AVATAR2ProVerif.java b/src/avatartranslator/toproverif/AVATAR2ProVerif.java
index ed2bc3d312b45220a632bda316b32687db8dee7b..b14560f0660a14a6ea0d67157beeff8f6d9f7b45 100755
--- a/src/avatartranslator/toproverif/AVATAR2ProVerif.java
+++ b/src/avatartranslator/toproverif/AVATAR2ProVerif.java
@@ -53,54 +53,66 @@ import myutil.*;
import avatartranslator.*;
import ui.*;
-public class AVATAR2ProVerif {
+public class AVATAR2ProVerif implements AvatarTranslator {
private static int GENERAL_ID = 0;
private final static String UNKNOWN = "UNKNOWN";
+ private final static String TRUE = "TRUE";
+ private final static String FALSE = "FALSE";
- 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_PK = "pk";
+ private final static String PK_ENCRYPT = "aencrypt";
+ private final static String PK_DECRYPT = "adecrypt";
+ private final static String PK_SIGN = "sign";
+ private final static String PK_VERIFYSIGN = "verifySign";
- private final static String PK_HEADER = "(* Public key cryptography *)\nfun pk/1.\nfun aencrypt/2.\nreduc adecrypt(aencrypt(x,pk(y)),y) = x.\n";
- private final static String SIG_HEADER = "fun sign/2.\nfun verifySign/3.\nequation verifySign(m, sign(m,sk), pk(sk))=true.\n";
- private final static String CERT_HEADER = "(* Certificates *)\nfun cert/2.\nfun verifyCert/2.\nequation verifyCert(cert(epk, sign(epk, sk)), pk(sk))=true.\nreduc getpk(cert(epk, sign(epk,sk))) = epk.\n";
+ private final static String CERT_CERT = "cert";
+ private final static String CERT_VERIFYCERT = "verifyCert";
+ private final static String CERT_GETPK = "getpk";
+ private final static String SK_ENCRYPT = "sencrypt";
+ private final static String SK_DECRYPT = "sdecrypt";
- private final static String SK_HEADER = "(* Symmetric key cryptography *)\nfun sencrypt/2.\nreduc sdecrypt(sencrypt(x,k),k) = x.\n";
- private final static String MAC_HEADER = "(* MAC *)\nfun MAC/2.\nreduc verifyMAC(m, k, MAC(m, k)) = true.\n";
- private final static String HASH_HEADER = "(* HASH *)\nfun hash/1.\n";
- private final static String CONCAT_HEADER = "(* CONCAT *)\nfun concat/5.\nreduc get1(concat(m1, m2, m3, m4, m5))= m1.\nreduc get2(concat(m1, m2, m3, m4, m5))= m2.\nreduc get3(concat(m1, m2, m3, m4, m5))= m3.\nreduc get4(concat(m1, m2, m3, m4, m5))= m4.\nreduc get5(concat(m1, m2, m3, m4, m5))= m5.\n";
+ private final static String MAC_MAC = "MAC";
+ private final static String MAC_VERIFYMAC = "verifyMAC";
+
+ private final static String HASH_HASH = "hash";
+
+ private final static String CH_MAINCH = "ch";
+ private final static String CH_ENCRYPT = "privChEnc";
+ private final static String CH_DECRYPT = "privChDec";
+
+ private final static String CHCTRL_CH = "chControl";
+ private final static String CHCTRL_ENCRYPT = "chControlEnc";
+ private final static String CHCTRL_DECRYPT = "chControlDec";
private ProVerifSpec spec;
private AvatarSpecification avspec;
private Hashtable<String, Integer> macs;
+ private LinkedList<ProVerifVar> sessionKnowledge;
+
protected Hashtable<String, String> declarations;
private Vector warnings;
private boolean advancedTranslation;
-
public AVATAR2ProVerif(AvatarSpecification _avspec) {
avspec = _avspec;
}
-
public void saveInFile(String path) throws FileException {
- FileUtils.saveFile(path + "pvspec", spec.makeSpec());
+ FileUtils.saveFile(path + "pvspec", spec.getStringSpec ());
}
-
public Vector getWarnings() {
return warnings;
}
-
-
- public ProVerifSpec generateProVerif(boolean _debug, boolean _optimize, boolean _stateReachability, boolean _advancedTranslation) {
+ public ProVerifSpec generateProVerif(boolean _debug, boolean _optimize, boolean _stateReachability, boolean _advancedTranslation, boolean _typed) {
advancedTranslation = _advancedTranslation;
GENERAL_ID = 0;
@@ -108,11 +120,14 @@ public class AVATAR2ProVerif {
declarations = new Hashtable<String, String>();
warnings = new Vector();
- spec = new ProVerifSpec();
+ if (_typed)
+ spec = new ProVerifSpec (new ProVerifPitypeSyntaxer ());
+ else
+ spec = new ProVerifSpec (new ProVerifPiSyntaxer ());
avspec.removeCompositeStates();
avspec.removeTimers();
- avspec.removeElseGuards();
+ avspec.removeElseGuards();
makeHeader(_stateReachability);
@@ -120,45 +135,33 @@ public class AVATAR2ProVerif {
makeBlocks();
-
- //TraceManager.addDev("-> Spec:" + avspec.toString());
-
-
- /*if (_optimize) {
- spec.optimize();
- }*/
-
-
return spec;
}
- private String makeAttrName(String _block, String _attribute) {
+ private static String makeAttrName(String _block, String _attribute) {
return _block + "__" + _attribute;
}
-
- private String makeActionFromBlockParam(String _block, String _param) {
+ private ProVerifProcInstr makeActionFromBlockParam(String _block, String _param) {
String tmp = makeAttrName(_block, _param);
String tmpH = declarations.get(tmp);
if (tmpH == null) {
declarations.put(tmp, tmp);
- tmp = "new " + tmp + ";\n";
- return tmp;
+ return new ProVerifProcNew (tmp, "bitstring");
}
- return "";
+ return null;
}
- private String makeLetActionFromBlockParam(String _block, String _param, String known) {
+ private ProVerifProcInstr makeLetActionFromBlockParam(String _block, String _param, String known) {
String tmp = makeAttrName(_block, _param);
String tmpH = declarations.get(tmp);
if (tmpH == null) {
declarations.put(tmp, tmp);
- tmp = "let " + tmp + " =" + known + " in \n";
- return tmp;
+ return new ProVerifProcLet (new ProVerifVar[] {new ProVerifVar (tmp, "bitstring")}, known);
}
- return "";
+ return null;
}
private void addDeclarationsFromList(int startIndex, String[] list, String result) {
@@ -166,554 +169,373 @@ public class AVATAR2ProVerif {
String tmp1;
int index;
- TraceManager.addDev("Add declaration list length=" + list.length);
-
for(int i=startIndex; i<list.length; i++) {
-
tmp = list[i];
- TraceManager.addDev("tmp=" + tmp);
index = tmp.indexOf('.');
if (index != -1) {
blockName = tmp.substring(0, index).trim();
- paramName = tmp.substring(index+1, tmp.length());
+ paramName = tmp.substring(index+1);
tmp1 = makeAttrName(blockName, paramName);
- if (tmp1 != null) {
+ if (tmp1 != null)
declarations.put(tmp1, result);
- TraceManager.addDev("Adding declaration: " + tmp1 + " result=" + result);
- }
}
}
-
}
public void makeHeader(boolean _stateReachability) {
- spec.addToGlobalSpecification(BOOLEAN_DATA_HEADER + "\n");
- spec.addToGlobalSpecification(FUNC_DATA_HEADER + "\n");
-
- spec.addToGlobalSpecification(PK_HEADER + "\n");
- spec.addToGlobalSpecification(SIG_HEADER + "\n");
- spec.addToGlobalSpecification(CERT_HEADER + "\n");
- spec.addToGlobalSpecification(SK_HEADER + "\n");
- spec.addToGlobalSpecification(MAC_HEADER + "\n");
- spec.addToGlobalSpecification(HASH_HEADER + "\n");
- 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();
- for(AvatarBlock block: blocks) {
- spec.addToGlobalSpecification("\n(* Block " + block.getName() + " : variables *)\n");
- for(AvatarAttribute attribute: block.getAttributes()) {
- spec.addToGlobalSpecification("private free " + attribute.getName() + ".\n");
- }
- }*/
-
-
- spec.addToGlobalSpecification("\n(* Data *)\n");
+ TraceManager.addDev("\n\n=+=+=+ Making Headers +=+=+=");
+ spec.addDeclaration (new ProVerifComment ("Boolean return types"));
+ spec.addDeclaration (new ProVerifConst (TRUE, "bitstring"));
+ spec.addDeclaration (new ProVerifConst (FALSE, "bitstring"));
+ spec.addDeclaration (new ProVerifComment ("Functions data"));
+ spec.addDeclaration (new ProVerifConst (UNKNOWN, "bitstring"));
+
+ spec.addDeclaration (new ProVerifComment ("Public key cryptography"));
+ spec.addDeclaration (new ProVerifFunc (PK_PK, new String[] {"bitstring"}, "bitstring"));
+ spec.addDeclaration (new ProVerifFunc (PK_ENCRYPT, new String[] {"bitstring", "bitstring"}, "bitstring"));
+ spec.addDeclaration (new ProVerifReduc (new ProVerifVar[] {new ProVerifVar ("x", "bitstring"), new ProVerifVar ("y", "bitstring")}, PK_DECRYPT + "(" + PK_ENCRYPT + "(x," + PK_PK + "(y)),y) = x"));
+ spec.addDeclaration (new ProVerifFunc (PK_SIGN, new String[] {"bitstring", "bitstring"}, "bitstring"));
+ spec.addDeclaration (new ProVerifReduc (new ProVerifVar[] {new ProVerifVar ("m", "bitstring"), new ProVerifVar ("sk", "bitstring")}, PK_VERIFYSIGN + "(m," + PK_SIGN + "(m,sk)," + PK_PK + "(sk))=" + TRUE));
+
+ spec.addDeclaration (new ProVerifComment ("Certificates"));
+ spec.addDeclaration (new ProVerifFunc (CERT_CERT, new String[] {"bitstring", "bitstring"}, "bitstring"));
+ spec.addDeclaration (new ProVerifReduc (new ProVerifVar[] {new ProVerifVar ("epk", "bitstring"), new ProVerifVar ("sk", "bitstring")}, CERT_VERIFYCERT + "(" + CERT_CERT + "(epk," + PK_SIGN + "(epk,sk))," + PK_PK + "(sk))=" + TRUE));
+ spec.addDeclaration (new ProVerifReduc (new ProVerifVar[] {new ProVerifVar ("epk", "bitstring"), new ProVerifVar ("sk", "bitstring")}, CERT_GETPK + "(" + CERT_CERT + "(epk," + PK_SIGN + "(epk,sk)))=epk"));
+
+ spec.addDeclaration (new ProVerifComment ("Symmetric key cryptography"));
+ spec.addDeclaration (new ProVerifFunc (SK_ENCRYPT, new String[] {"bitstring", "bitstring"}, "bitstring"));
+ spec.addDeclaration (new ProVerifReduc (new ProVerifVar[] {new ProVerifVar ("x", "bitstring"), new ProVerifVar ("k", "bitstring")}, SK_DECRYPT + "(" + SK_ENCRYPT + "(x,k),k)=x"));
+
+ spec.addDeclaration (new ProVerifComment ("MAC"));
+ spec.addDeclaration (new ProVerifFunc (MAC_MAC, new String[] {"bitstring", "bitstring"}, "bitstring"));
+ spec.addDeclaration (new ProVerifReduc (new ProVerifVar[] {new ProVerifVar ("m", "bitstring"), new ProVerifVar ("k", "bitstring")}, MAC_VERIFYMAC + "(m,k," + MAC_MAC + "(m,k))=" + TRUE));
+
+ spec.addDeclaration (new ProVerifComment ("HASH"));
+ spec.addDeclaration (new ProVerifFunc (HASH_HASH, new String[] {"bitstring"}, "bitstring"));
+
+ spec.addDeclaration (new ProVerifComment ("Channel"));
+ spec.addDeclaration (new ProVerifVar (CH_MAINCH, "channel"));
+ spec.addDeclaration (new ProVerifFunc (CH_ENCRYPT, new String[] {"bitstring"}, "bitstring", true));
+ spec.addDeclaration (new ProVerifReduc (new ProVerifVar[] {new ProVerifVar ("x", "bitstring")}, CH_DECRYPT + "(" + CH_ENCRYPT + "(x))=x", true));
+
+ spec.addDeclaration (new ProVerifComment ("Control Channel"));
+ spec.addDeclaration (new ProVerifVar (CHCTRL_CH, "channel"));
+ spec.addDeclaration (new ProVerifFunc (CHCTRL_ENCRYPT, new String[] {"bitstring"}, "bitstring", true));
+ spec.addDeclaration (new ProVerifReduc (new ProVerifVar[] {new ProVerifVar ("x", "bitstring")}, CHCTRL_DECRYPT + "(" + CHCTRL_ENCRYPT + "(x))=x", true));
+
LinkedList<AvatarBlock> blocks = avspec.getListOfBlocks();
- String[] list;
- String pragma;
+ String action = "(";
+ for(AvatarBlock block: blocks) {
+ HashMap<AvatarStateMachineElement, Integer> simplifiedElements = block.getStateMachine ().getSimplifiedElements ();
+ for (AvatarStateMachineElement asme: simplifiedElements.keySet ())
+ spec.addDeclaration (new ProVerifVar ("call__" + block.getName() + "__" + simplifiedElements.get (asme), "bitstring", true));
+ }
+ spec.addDeclaration (new ProVerifComment ("Data"));
/* Data */
+ TraceManager.addDev("Constants");
for(AvatarBlock block: blocks) {
for(AvatarAttribute attribute: block.getAttributes()) {
- pragma = hasConstantPragmaStartingWithAttribute(block.getName(), attribute.getName());
+ String pragma = hasConstantPragmaStartingWithAttribute(block.getName(), attribute.getName());
if (pragma != null) {
- spec.addToGlobalSpecification("data " + makeAttrName(block.getName(), attribute.getName()) + "/0.\n");
- declarations.put(makeAttrName(block.getName(), attribute.getName()), makeAttrName(block.getName(), attribute.getName()));
- list = getListOfBlockParams(pragma);
- addDeclarationsFromList(1, list, makeAttrName(block.getName(), attribute.getName()));
+ String constName = makeAttrName(block.getName(), attribute.getName());
+ TraceManager.addDev("| " + constName);
+ spec.addDeclaration (new ProVerifConst (constName, "bitstring"));
+ declarations.put(constName, constName);
+ String[] list = getListOfBlockParams(pragma);
+ addDeclarationsFromList(1, list, constName);
}
}
}
-
- spec.addToGlobalSpecification("\n(* Secrecy Assumptions *)\n");
/* Secrecy Assumptions */
- int index;
- String tmp, blockName, paramName, tmp1;
- for(String pr: avspec.getPragmas()) {
+ spec.addDeclaration (new ProVerifComment ("Secrecy Assumptions"));
+ TraceManager.addDev("Secrecy Assumptions");
+ for(String pr: avspec.getPragmas())
if (isSecrecyAssumptionPragma(pr)) {
- list = getListOfBlockParams(pr);
+ String[] list = getListOfBlockParams(pr);
for(int i=0; i<list.length; i++) {
- tmp = list[i];
- index = tmp.indexOf('.');
+ String tmp = list[i];
+ int index = tmp.indexOf('.');
if (index != -1) {
- blockName = tmp.substring(0, index).trim();
- paramName = tmp.substring(index+1, tmp.length());
- tmp1 = makeAttrName(blockName, paramName);
+ String blockName = tmp.substring(0, index).trim();
+ String paramName = tmp.substring(index+1);
+ String tmp1 = makeAttrName(blockName, paramName);
if (tmp1 != null) {
- spec.addToGlobalSpecification("not " + tmp1 +".\n");
+ TraceManager.addDev("| " + tmp1);
+ spec.addDeclaration (new ProVerifSecrecyAssum (tmp1));
}
}
}
}
- }
/* Queries */
/* Parse all attributes starting with "secret" and declare them as non accesible to attacker" */
- spec.addToGlobalSpecification("\n(* Queries *)\n");
+ spec.addDeclaration (new ProVerifComment ("Queries"));
+ TraceManager.addDev("Queries");
for(AvatarBlock block: blocks) {
for(AvatarAttribute attribute: block.getAttributes()) {
// Attribute is preinitialized if it is in a secret pragma
//TraceManager.addDev("Testing secret of " + block.getName() + "." + attribute.getName() + " ?");
if (hasSecretPragmaWithAttribute(block.getName(), attribute.getName())) {
//TraceManager.addDev("Secret!");
- spec.addToGlobalSpecification("private free " + makeAttrName(block.getName(), attribute.getName()) + ".\n");
- declarations.put(makeAttrName(block.getName(), attribute.getName()), makeAttrName(block.getName(), attribute.getName()));
- spec.addToGlobalSpecification("query attacker:" + makeAttrName(block.getName(), attribute.getName()) + ".\n\n");
+ String varName = makeAttrName(block.getName(), attribute.getName());
+ spec.addDeclaration (new ProVerifVar (varName, "bitstring", true));
+ declarations.put(varName, varName);
+ spec.addDeclaration (new ProVerifQueryAtt (varName));
+ TraceManager.addDev("| attacker (" + varName + ")");
}
}
+
// Queries for states
- if (_stateReachability) {
- for(AvatarStateMachineElement asme: block.getStateMachine().getListOfElements()) {
+ if (_stateReachability)
+ for(AvatarStateMachineElement asme: block.getStateMachine().getListOfElements())
if (asme instanceof AvatarState) {
- spec.addToGlobalSpecification("query ev:" + "enteringState__" + block.getName() + "__" + asme.getName() + "().\n");
+ spec.addDeclaration (new ProVerifQueryEv (new ProVerifVar[] {}, "enteringState__" + block.getName() + "__" + asme.getName()));
+ spec.addDeclaration (new ProVerifEvDecl ("enteringState__" + block.getName() + "__" + asme.getName(), new String[] {}));
+ TraceManager.addDev("| event (enteringState__" + block.getName() + "__" + asme.getName() + ")");
}
- }
- }
}
-
/* Autenticity */
makeAuthenticityPragmas();
}
public void makeAuthenticityPragmas() {
- spec.addToGlobalSpecification("\n(* Authenticity *)\n");
+ spec.addDeclaration (new ProVerifComment ("Authenticity"));
+ TraceManager.addDev("Authenticity");
+
LinkedList<String> pragmas = avspec.getPragmas();
- String tmp;
- String tmps [];
- String name1;
- String name0;
- String p0, p1;
int cpt = -1;
- int index;
for(String pragma: pragmas) {
cpt ++;
if (isAuthenticityPragma(pragma)) {
- tmp = pragma.substring(13, pragma.length()).trim();
- //tmp = Conversion.replaceAllChar(tmp, '.', "__");
-
- //TraceManager.addDev("Testing pragma: " + tmp);
+ String tmp = pragma.substring(13).trim();
if (tmp.length() != 0) {
- tmps = tmp.split(" ");
+ String[] tmps = tmp.split (" +");
if (tmps.length > 1) {
- TraceManager.addDev("0");
- index = tmps[0].indexOf(".");
- name0 = tmps[0].substring(index+1, tmps[0].length());
- index = name0.indexOf(".");
- name0 = name0.substring(index+1, name0.length());
-
- TraceManager.addDev("1");
-
- index = tmps[1].indexOf(".");
- name1 = tmps[1].substring(index+1, tmps[1].length());
- index = name1.indexOf(".");
- name1 = name1.substring(index+1, name1.length());
-
- TraceManager.addDev("2");
- p1 = Conversion.replaceAllChar(tmps[1], '.', "__");
- TraceManager.addDev("3");
- p0 = Conversion.replaceAllChar(tmps[0], '.', "__");
- TraceManager.addDev("name0" + tmps[0]);
- TraceManager.addDev("name1" + tmps[1]);
-
- try {
- //spec.addToGlobalSpecification("query evinj:authenticity__" + p1 + "__" + cpt + "(" + name1 + ") ==> evinj:authenticity__" + p0 + "__" + cpt + "(" + name0 + ").\n");
- spec.addToGlobalSpecification("query evinj:authenticity__" + p1 + "__" + cpt + "(m__93482) ==> evinj:authenticity__" + p0 + "__" + cpt + "(m__93482).\n");
- } catch (Exception e) {
- TraceManager.addDev("\n\n*** Error on pragma:" + pragma + ": " + e.getMessage());
- }
+ String p0 = Conversion.replaceAllChar(tmps[0], '.', "__");
+ String p1 = Conversion.replaceAllChar(tmps[1], '.', "__");
+
+ TraceManager.addDev("| authenticity__" + p1 + "__" + cpt + "(m__93482) ==> authenticity__" + p0 + "__" + cpt + "(m__93482)");
+ spec.addDeclaration (new ProVerifEvDecl ("authenticity__" + p1 + "__" + cpt, new String[] {"bitstring"}));
+ spec.addDeclaration (new ProVerifEvDecl ("authenticity__" + p0 + "__" + cpt, new String[] {"bitstring"}));
+ spec.addDeclaration (new ProVerifQueryEvinj (new ProVerifVar[] {new ProVerifVar ("m__93482", "bitstring")}, "authenticity__" + p1 + "__" + cpt + "(m__93482)", "authenticity__" + p0 + "__" + cpt + "(m__93482)"));
}
}
}
}
-
}
public boolean hasAuthenticityPragma(boolean isOut, String _blockName, String attributeName) {
- TraceManager.addDev("************* Searching for authenticity pragma for " + _blockName + "." + attributeName + " " + isOut);
LinkedList<String> pragmas = avspec.getPragmas();
- String tmp;
- String tmps [];
- int index;
- String name;
- for(String pragma: pragmas) {
+ for(String pragma: pragmas)
if (isAuthenticityPragma(pragma)) {
- tmp = pragma.substring(13, pragma.length()).trim();
+ String tmp = pragma.substring(13).trim();
- TraceManager.addDev("Testing prama: " + tmp);
-
- if (tmp.length() == 0) {
+ if (tmp.isEmpty ())
return false;
- }
- tmps = tmp.split(" ");
+ String[] tmps = tmp.split(" ");
if (tmps.length >1) {
- if (isOut) {
+ if (isOut)
tmp = tmps[0];
- } else {
+ else
tmp = tmps[1];
- }
- //TraceManager.addDev("Testing with: " + tmp);
- if (tmp.length() > 0) {
- index = tmp.indexOf('.');
- if (index != -1) {
- try {
- if (tmp.substring(0, index).compareTo(_blockName) == 0) {
-
- TraceManager.addDev("Testing with: " + _blockName + "." + attributeName);
- name = attributeName;
- /*index = name.indexOf("__");
- if (index != -1) {
- name = name.substring(0, index);
- }*/
- if (tmp.substring(index+1, tmp.length()).compareTo(name) == 0) {
- TraceManager.addDev("Found authenticity");
- return true;
- }
- }
- } catch (Exception e) {
- TraceManager.addDev("Error on testing pragma");
- }
- }
- }
+ int index = tmp.indexOf('.');
+ if ( index != -1
+ && tmp.substring(0, index).compareTo(_blockName) == 0
+ && tmp.substring(index+1).compareTo(attributeName) == 0)
+ return true;
}
-
}
- }
-
- TraceManager.addDev("Authenticity failed");
return false;
}
public LinkedList<String> getAuthenticityPragmas(String _blockName, String _stateName) {
- TraceManager.addDev("************* Searching for authenticity pragma for " + _blockName + "." + _stateName);
LinkedList<String> pragmas = avspec.getPragmas();
- String tmp;
- String tmps [];
- int index;
- String name;
- int cpt = -1;
LinkedList<String> ret = new LinkedList<String>();
+ int cpt = -1;
for(String pragma: pragmas) {
cpt ++;
if (isAuthenticityPragma(pragma)) {
- tmp = pragma.substring(13, pragma.length()).trim();
-
- TraceManager.addDev("Testing prama: " + tmp);
+ String tmp = pragma.substring(13).trim();
- if (tmp.length() == 0) {
+ if (tmp.isEmpty())
return ret;
- }
- tmps = tmp.split(" ");
+ String[] tmps = tmp.split(" ");
- if (tmps.length >1) {
+ if (tmps.length > 1)
for(int i=0; i<2; i++) {
- if (i == 0) {
- tmp = tmps[0];
- } else {
- tmp = tmps[1];
- }
- //TraceManager.addDev("Testing with: " + tmp);
+ tmp = tmps[i];
+
if (tmp.length() > 0) {
- index = tmp.indexOf('.');
- if (index != -1) {
- try {
- TraceManager.addDev("Testing with: " + _blockName + "." + _stateName);
- if (tmp.substring(0, index).compareTo(_blockName) == 0) {
- tmp = tmp.substring(index+1, tmp.length());
- index = tmp.indexOf('.');
- if (index != -1) {
- if (tmp.substring(0, index).compareTo(_stateName) == 0) {
- ret.add(new String("authenticity__" + _blockName + "__" + _stateName + "__" + tmp.substring(index+1, tmp.length()) + "__" + cpt + "(" + tmp.substring(index+1, tmp.length()) + ")"));
- TraceManager.addDev("Pragma added:" + ret.get(ret.size()-1));
- }
- }
-
- //name = attributeName;
- /*index = name.indexOf("__");
- if (index != -1) {
- name = name.substring(0, index);
- }*/
- /*if (tmp.substring(index+1, tmp.length()).compareTo(name) == 0) {
- TraceManager.addDev("Found authenticity");
- return true;
-
- }*/
+
+ int index = tmp.indexOf('.');
+ if ( index != -1
+ && tmp.substring(0, index).compareTo(_blockName) == 0) {
+
+ tmp = tmp.substring(index+1);
+ index = tmp.indexOf('.');
+ if ( index != -1
+ && tmp.substring(0, index).compareTo(_stateName) == 0)
+ ret.add ("authenticity__" + _blockName + "__" + _stateName + "__" + tmp.substring(index+1) + "__" + cpt + "(" + tmp.substring(index+1) + ")");
}
- } catch (Exception e) {
- TraceManager.addDev("Error on testing pragma");
- }
- }
}
}
- }
-
}
}
- TraceManager.addDev("Authenticity done found:" + ret.size());
-
return ret;
}
public boolean isPublicPrivateKeyPragma(String _blockName, String attributeName) {
LinkedList<String> pragmas = avspec.getPragmas();
- String tmp;
- String tmps [];
- int index;
- for(String pragma: pragmas) {
+ for(String pragma: pragmas)
if (isPrivatePublicKeyPragma(pragma)) {
- tmp = pragma.substring(18, pragma.length()).trim();
-
- //TraceManager.addDev("Testing prama: " + tmp);
+ String tmp = pragma.substring(18).trim();
- if (tmp.length() == 0) {
+ if (tmp.isEmpty ())
return false;
- }
- tmps = tmp.split(" ");
+ String[] tmps = tmp.split(" ");
for(int i=0; i<tmps.length; i++) {
tmp = tmps[i];
- //TraceManager.addDev("Testing with: " + tmp);
- if (tmp.length() > 0) {
- index = tmp.indexOf('.');
- if (index != -1) {
- try {
- if (tmp.substring(0, index).compareTo(_blockName) == 0) {
- if (tmp.substring(index+1, tmp.length()).compareTo(attributeName) == 0) {
- return true;
- }
- }
- } catch (Exception e) {
- TraceManager.addDev("Error on testing pragma");
- }
- } else {
- if (tmp.compareTo(attributeName) == 0) {
- return true;
- }
- }
- }
+ int index = tmp.indexOf('.');
+ if ( (index != -1
+ && tmp.substring(0, index).compareTo(_blockName) == 0
+ && tmp.substring(index+1).compareTo(attributeName) == 0)
+ || tmp.compareTo(attributeName) == 0)
+ return true;
}
-
}
- }
return false;
}
public boolean hasSecretPragmaWithAttribute(String _blockName, String attributeName) {
LinkedList<String> pragmas = avspec.getPragmas();
- String tmp;
- String tmps [];
- int index;
- for(String pragma: pragmas) {
+ for(String pragma: pragmas)
if (isSecretPragma(pragma)) {
- tmp = pragma.substring(7, pragma.length()).trim();
-
- //TraceManager.addDev("Testing prama: " + tmp);
+ String tmp = pragma.substring(7).trim();
- if (tmp.length() == 0) {
+ if (tmp.isEmpty ())
return false;
- }
- tmps = tmp.split(" ");
+ String[] tmps = tmp.split(" ");
for(int i=0; i<tmps.length; i++) {
tmp = tmps[i];
- //TraceManager.addDev("Testing with: " + tmp);
- if (tmp.length() > 0) {
- index = tmp.indexOf('.');
- if (index != -1) {
- try {
- if (tmp.substring(0, index).compareTo(_blockName) == 0) {
- if (tmp.substring(index+1, tmp.length()).compareTo(attributeName) == 0) {
- return true;
- }
- }
- } catch (Exception e) {
- TraceManager.addDev("Error on testing pragma");
- }
- }
- }
+ int index = tmp.indexOf('.');
+ if ( index != -1
+ && tmp.substring(0, index).compareTo(_blockName) == 0
+ && tmp.substring(index+1).compareTo(attributeName) == 0)
+ return true;
}
-
}
- }
return false;
}
public String hasConstantPragmaStartingWithAttribute(String _blockName, String attributeName) {
LinkedList<String> pragmas = avspec.getPragmas();
- String tmp;
- String tmps [];
- int index;
- for(String pragma: pragmas) {
+ for(String pragma: pragmas)
if (isConstantPragma(pragma)) {
- tmp = pragma.substring(8, pragma.length()).trim();
-
- TraceManager.addDev("Testing CONSTANT pragma: " + tmp);
+ String tmp = pragma.substring(8).trim();
- if (tmp.length() == 0) {
+ if (tmp.isEmpty ())
return null;
- }
- tmps = tmp.split(" ");
+ String[] tmps = tmp.split(" ");
tmp = tmps[0];
- index = tmp.indexOf('.');
- if (index != -1) {
- try {
- if (tmp.substring(0, index).compareTo(_blockName) == 0) {
- if (tmp.substring(index+1, tmp.length()).compareTo(attributeName) == 0) {
- return pragma;
- }
- }
- } catch (Exception e) {
- TraceManager.addDev("Error on testing pragma");
- }
- }
+ int index = tmp.indexOf('.');
+ if ( index != -1
+ && tmp.substring(0, index).compareTo(_blockName) == 0
+ && tmp.substring(index+1).compareTo(attributeName) == 0)
+ return pragma;
}
- }
-
return null;
}
public boolean hasSecretPragmaWithAttribute(String attributeName) {
LinkedList<String> pragmas = avspec.getPragmas();
- String tmp;
- String tmps [];
- int index;
- for(String pragma: pragmas) {
+ for(String pragma: pragmas)
if (isSecretPragma(pragma)) {
- tmp = pragma.substring(7, pragma.length()).trim();
-
- //TraceManager.addDev("Testing prama: " + tmp);
+ String tmp = pragma.substring(7).trim();
- if (tmp.length() == 0) {
+ if (tmp.isEmpty ())
return false;
- }
-
- tmps = tmp.split(" ");
- for(int i=0; i<tmps.length; i++) {
- tmp = tmps[i];
- //TraceManager.addDev("Testing with: " + tmp);
- if (tmp.length() > 0) {
- index = tmp.indexOf('.');
- if (index != -1) {
- try {
-
- if (tmp.substring(index+1, tmp.length()).compareTo(attributeName) == 0) {
- return true;
- }
- } catch (Exception e) {
- TraceManager.addDev("Error on testing pragma");
- }
- }
- }
+ String[] tmps = tmp.split(" ");
+ for(String attribute: tmps) {
+ int index = attribute.indexOf('.');
+ if ( index != -1
+ && attribute.substring(index+1).compareTo(attributeName) == 0)
+ return true;
}
-
}
- }
return false;
}
public boolean hasPrivatePublicKeysPragmaWithAttribute(String _blockName, String attributeName) {
LinkedList<String> pragmas = avspec.getPragmas();
- String tmp;
- String tmps [];
- int index;
- boolean foundBlock = false;
- for(String pragma: pragmas) {
+ for(String pragma: pragmas)
if (isPrivatePublicKeyPragma(pragma)) {
- tmp = pragma.substring(17, pragma.length()).trim();
+ String tmp = pragma.substring(17).trim();
- //TraceManager.addDev("Testing prama: " + tmp);
-
- if (tmp.length() == 0) {
+ if (tmp.isEmpty ())
return false;
- }
- tmps = tmp.split(" ");
- for(int i=0; i<tmps.length; i++) {
+ String[] tmps = tmp.split(" ");
+ if (tmp.compareTo(_blockName) != 0)
+ continue;
+
+ for(int i=1; i<tmps.length; i++) {
tmp = tmps[i];
- if (i == 0) {
- if (tmp.compareTo(_blockName) == 0) {
- foundBlock = true;
- }
- } else {
- if ((tmp.compareTo(attributeName) == 0) && (foundBlock)) {
- return true;
- }
- }
+ if (tmp.compareTo(attributeName) == 0)
+ return true;
}
-
}
- }
return false;
}
public boolean hasInitialSystemKnowledgePragmaWithAttribute(String _blockName, String attributeName) {
LinkedList<String> pragmas = avspec.getPragmas();
- String tmp;
- String tmps [];
- int index;
- for(String pragma: pragmas) {
+ for(String pragma: pragmas)
if (isInitialSystemKnowledgePragma(pragma)) {
- tmp = pragma.substring(23, pragma.length()).trim();
-
- //TraceManager.addDev("Testing pragma: " + tmp);
+ String tmp = pragma.substring(23, pragma.length()).trim();
- if (tmp.length() == 0) {
+ if (tmp.isEmpty ())
return false;
- }
- tmps = tmp.split(" ");
- for(int i=0; i<tmps.length; i++) {
- tmp = tmps[i];
- //TraceManager.addDev("Testing with: " + tmp);
- if (tmp.length() > 0) {
- index = tmp.indexOf('.');
- if (index != -1) {
- try {
- if (tmp.substring(0, index).compareTo(_blockName) == 0) {
- if (tmp.substring(index+1, tmp.length()).compareTo(attributeName) == 0) {
- return true;
- }
- }
- } catch (Exception e) {
- TraceManager.addDev("Error on testing pragma");
- }
- }
- }
+ String[] tmps = tmp.split(" ");
+ for(String attribute: tmps) {
+ int index = attribute.indexOf('.');
+ if ( index != -1
+ && attribute.substring(0, index).compareTo(_blockName) == 0
+ && attribute.substring(index+1).compareTo(attributeName) == 0)
+ return true;
}
-
}
- }
return false;
}
@@ -749,111 +571,86 @@ public class AVATAR2ProVerif {
public String[] getListOfBlockParams(String _pragma) {
String s = _pragma;
- if (isSecretPragma(s)) {
- s = s.substring(7, s.length()).trim();
- } else if (isInitialSystemKnowledgePragma(s)) {
- s = s.substring(23, s.length()).trim();
- } else if (isInitialSessionKnowledgePragma(s)) {
- s = s.substring(24, s.length()).trim();
- } else if (isConstantPragma(s)) {
- s = s.substring(8, s.length()).trim();
- } else if (isSecrecyAssumptionPragma(s)) {
- s = s.substring(17, s.length()).trim();
- } else {
+ if (isSecretPragma(s))
+ s = s.substring(7);
+ else if (isInitialSystemKnowledgePragma(s))
+ s = s.substring(23);
+ else if (isInitialSessionKnowledgePragma(s))
+ s = s.substring(24);
+ else if (isConstantPragma(s))
+ s = s.substring(8);
+ else if (isSecrecyAssumptionPragma(s))
+ s = s.substring(17);
+ else
return null;
- }
- return s.split(" ");
+ return s.trim ().split (" ");
}
public void makeStartingProcess() {
- String action = "";
- String tmp, tmp1, tmp2, attributeName;
- int index;
- boolean found;
+ TraceManager.addDev("\n\n=+=+=+ Making Starting Process +=+=+=");
- ProVerifProcess p = new ProVerifProcess();
- p.processName = "starting__";
+ ProVerifProcess p = new ProVerifProcess("starting__", new ProVerifVar[] {});
+ ProVerifProcInstr lastInstr = p;
LinkedList<AvatarBlock> blocks = avspec.getListOfBlocks();
- HashMap<String, String> pubs = new HashMap<String, String>();
+ HashMap<String, String> pubs = new HashMap<String, String>();
- //LinkedList<String> createdVariables = new LinkedList<String>();
String[] list;
String blockName, paramName;
- for(String pragma: avspec.getPragmas()) {
- TraceManager.addDev("Working on pragma: " + pragma);
+ TraceManager.addDev("Exploring Pragmas of all Processes");
+ for(String pragma: avspec.getPragmas())
if (isInitialSystemKnowledgePragma(pragma)) {
// Identify each blockName / paramName
list = getListOfBlockParams(pragma);
-
// Declare only the first one of the list
if (list.length > 0) {
- tmp = list[0];
- index = tmp.indexOf('.');
+ String tmp = list[0];
+ int index = tmp.indexOf('.');
if (index != -1) {
blockName = tmp.substring(0, index).trim();
- paramName = tmp.substring(index+1, tmp.length());
-
- String known = pubs.get(blockName + "__" + paramName);
- if (known != null) {
- action += makeLetActionFromBlockParam(blockName, paramName, known);
- } else {
- action += makeActionFromBlockParam(blockName, paramName);
- }
- TraceManager.addDev("Adding action=" + action);
- addDeclarationsFromList(1, list, makeAttrName(blockName, paramName));
+ paramName = tmp.substring(index+1);
+
+ // TODO: move that outside the process ?
+ String blockParamName = makeAttrName(blockName, paramName);
+ String known = pubs.get(blockParamName);
+ ProVerifProcInstr tmpInstr;
+ if (known != null)
+ tmpInstr = makeLetActionFromBlockParam(blockName, paramName, known);
+ else
+ tmpInstr = makeActionFromBlockParam(blockName, paramName);
+
+ addDeclarationsFromList(1, list, blockParamName);
+ TraceManager.addDev("| Initial knowledge pragma: " + blockParamName);
+ lastInstr = lastInstr.setNextInstr (tmpInstr);
}
}
- /*for(int i=0; i<list.length; i++) {
- tmp = list[i];
- index = tmp.indexOf('.');
- if (index != -1) {
- blockName = tmp.substring(0, index).trim();
- paramName = tmp.substring(index+1, tmp.length());
-
- // Verify whether they are secret or not
- if ((!hasSecretPragmaWithAttribute(paramName)) && (!hasPrivatePublicKeysPragmaWithAttribute(blockName, paramName))){
- found = false;
- // If not, add them if not already added
- for(String st: createdVariables) {
- if (st.compareTo(paramName) == 0) {
- found = true;
- break;
- }
- }
- if (!found) {
- action += "new " + paramName + ";\n";
- createdVariables.add(paramName);
- }
- }
- }
- }*/
} else if (isPrivatePublicKeyPragma(pragma)) {
- TraceManager.addDev("Pragma Public: " + pragma);
String privK, pubK;
- index = pragma.indexOf(" ");
+ int index = pragma.indexOf(" ");
if (index != -1) {
- tmp = pragma.substring(index+1, pragma.length()).trim();
+ String tmp = pragma.substring(index+1).trim();
index = tmp.indexOf(" ");
if (index != -1) {
blockName = tmp.substring(0, index);
- tmp2 = tmp.substring(index+1, tmp.length()).trim();
+ String tmp2 = tmp.substring(index+1).trim();
index = tmp2.indexOf(" ");
if (index != -1) {
privK = tmp2.substring(0, index).trim();
- pubK = tmp2.substring(index+1, tmp2.length()).trim();
+ pubK = tmp2.substring(index+1).trim();
+ TraceManager.addDev("| Private Public key pragma: " + privK + " / " + pubK);
- pubs.put(blockName + "__" + pubK, pubK);
+ String pubAttrName = makeAttrName(blockName, pubK);
+ pubs.put(pubAttrName, pubK);
- action += makeActionFromBlockParam(blockName, privK);
+ lastInstr = lastInstr.setNextInstr (makeActionFromBlockParam(blockName, privK));
- action += "let " + makeAttrName(blockName, pubK) + " = pk(" + makeAttrName(blockName, privK) + ") in \n";
- action += "out(ch, " + makeAttrName(blockName, pubK) + ");\n";
+ lastInstr = lastInstr.setNextInstr (new ProVerifProcLet (new ProVerifVar[] {new ProVerifVar (pubAttrName, "bitstring")}, PK_PK + "(" + makeAttrName(blockName, privK) + ")"));;
+ lastInstr = lastInstr.setNextInstr (new ProVerifProcRaw ("out (" + CH_MAINCH + ", " + pubAttrName + ");"));
//TraceManager.addDev("********************************* Putting :" + makeAttrName(blockName, pubK + " -> " + makeAttrName(blockName, pubK)));
- declarations.put(makeAttrName(blockName, pubK), makeAttrName(blockName, pubK));
+ declarations.put(pubAttrName, pubAttrName);
}
}
}
@@ -861,458 +658,455 @@ public class AVATAR2ProVerif {
// Identify each blockName / paramName
list = getListOfBlockParams(pragma);
-
+ // TODO: move that outside the process ?
// Declare only the first one of the list
if (list.length > 0) {
- tmp = list[0];
- index = tmp.indexOf('.');
+ String tmp = list[0];
+ int index = tmp.indexOf('.');
if (index != -1) {
blockName = tmp.substring(0, index).trim();
- paramName = tmp.substring(index+1, tmp.length());
+ paramName = tmp.substring(index+1);
- action += makeActionFromBlockParam(blockName, paramName);
+ TraceManager.addDev("| Secrecy assumption pragma: " + blockName + "__" + paramName);
+ lastInstr = lastInstr.setNextInstr (makeActionFromBlockParam(blockName, paramName));
}
}
}
+
+ ProVerifProcRawGlobing globing = new ProVerifProcRawGlobing ("(", ")");
+ lastInstr.setNextInstr (globing);
+ lastInstr = globing.getIntra ();
+ String action = "";
+ for(AvatarBlock block: blocks) {
+ HashMap<AvatarStateMachineElement, Integer> simplifiedElements = block.getStateMachine ().getSimplifiedElements ();
+ int index = 0;
+ for (AvatarStateMachineElement asme: simplifiedElements.keySet ()) {
+ if (index != 0)
+ action += " | ";
+ index ++;
+ action += "!" + block.getName() + "__" + simplifiedElements.get (asme);
+ }
+ action += " | ";
}
- action += "(!\n(";
+ lastInstr = lastInstr.setNextInstr (new ProVerifProcRaw (action));
+ globing = new ProVerifProcRawGlobing ("! (", ")");
+ lastInstr.setNextInstr (globing);
+ lastInstr = globing.getIntra ();
+
+ TraceManager.addDev("Finding session knowledge");
+ this.sessionKnowledge = new LinkedList<ProVerifVar> ();
// Must add Session Knowledge
- for(String pragma: avspec.getPragmas()) {
- TraceManager.addDev("Working on pragma: " + pragma);
+ for(String pragma: avspec.getPragmas())
+ //TraceManager.addDev("Working on pragma: " + pragma);
if (isInitialSessionKnowledgePragma(pragma)) {
list = getListOfBlockParams(pragma);
// Declare only the first one of the list
if (list.length > 0) {
- tmp = list[0];
- index = tmp.indexOf('.');
+ String tmp = list[0];
+ int index = tmp.indexOf('.');
if (index != -1) {
blockName = tmp.substring(0, index).trim();
- paramName = tmp.substring(index+1, tmp.length());
+ paramName = tmp.substring(index+1);
- action += makeActionFromBlockParam(blockName, paramName);
+ TraceManager.addDev("| Session knowledge pragma: " + blockName + "__" + paramName);
+ lastInstr = lastInstr.setNextInstr (makeActionFromBlockParam(blockName, paramName));
+ this.sessionKnowledge.add (new ProVerifVar (blockName + "__" + paramName, "bitstring"));
addDeclarationsFromList(1, list, makeAttrName(blockName, paramName));
}
}
}
- }
- index = 0;
- for(AvatarBlock block: blocks) {
- if (index != 0) {
- action += " | ";
- }
- index ++;
- action += "(" + block.getName() + "__0)";
- }
- action += "))";
- p.processLines.add(action);
- spec.addProcess(p);
- spec.setStartingProcess(p);
+
+ TraceManager.addDev("Finding processes");
+ ProVerifProcParallel paral = new ProVerifProcParallel ();
+ for(AvatarBlock block: blocks)
+ paral.addInstr (new ProVerifProcCall (block.getName() + "__start", this.sessionKnowledge.toArray (new ProVerifVar[this.sessionKnowledge.size ()])));
+ lastInstr = lastInstr.setNextInstr (paral);
+ spec.setMainProcess(p);
+ }
+
+ private String translateTerm (AvatarTerm term) {
+ return term.getName ();
}
+ /**
+ * Generate ProVerif code for each process for each Avatar block
+ */
public void makeBlocks() {
+ TraceManager.addDev("\n\n=+=+=+ Making Blocks +=+=+=");
+
LinkedList<AvatarBlock> blocks = avspec.getListOfBlocks();
- for(AvatarBlock block: blocks) {
+ for(AvatarBlock block: blocks)
makeBlock(block);
- }
}
- public void makeBlock(AvatarBlock ab) {
- String dec;
-
- LinkedList<ProVerifProcess> tmpprocesses = new LinkedList<ProVerifProcess>();
- LinkedList<AvatarState> states = new LinkedList<AvatarState>();
-
- // First process : variable declaration
- ProVerifProcess p = new ProVerifProcess(ab.getName() + "__0");
- spec.addProcess(p);
-
- for(AvatarAttribute aa: ab.getAttributes()) {
- //TraceManager.addDev("Testing: " + ab.getName() + "." + aa.getName());
- /*if ((!hasInitialSystemKnowledgePragmaWithAttribute(ab.getName(), aa.getName())) && (!(hasSecretPragmaWithAttribute(ab.getName(), aa.getName())))) {
- if (!isPublicPrivateKeyPragma(ab.getName(), aa.getName())) {
- TraceManager.addDev(" Adding: " + aa.getName());
- addLine(p, "new " + aa.getName());
- }
- }*/
- TraceManager.addDev("Getting:" + makeAttrName(ab.getName(), aa.getName()));
- dec = declarations.get(makeAttrName(ab.getName(), aa.getName()));
- if (dec == null) {
- addLine(p, "new " + aa.getName());
- } else {
- if (dec.compareTo(aa.getName()) != 0) {
- addLineNoEnd(p, "let " + aa.getName() + " = " + dec + " in");
- }
- }
+ /**
+ * Compute a list of ProVerifVar corresponding to the attributes of the block
+ */
+ private LinkedList<ProVerifVar> getAttributesFromBlock (AvatarBlock ab) {
+ LinkedList<ProVerifVar> result = new LinkedList<ProVerifVar> ();
+ for(AvatarAttribute aa: ab.getAttributes())
+ result.add (new ProVerifVar (aa.getName (), "bitstring"));
+ return result;
+ }
+ /**
+ * Generate ProVerif code for one Avatar block
+ */
+ public void makeBlock(AvatarBlock ab) {
+ TraceManager.addDev("\nAvatarBlock: " + ab.getName ());
+
+ // Create first ProVerif process for this block and add it to the ProVerif specification
+ ProVerifProcInstr lastInstr = new ProVerifProcess(ab.getName() + "__start", this.sessionKnowledge.toArray (new ProVerifVar[this.sessionKnowledge.size ()]));
+ spec.addDeclaration (lastInstr);
+
+ // Create a ProVerif Variable corresponding to each attribute block
+ LinkedList<ProVerifVar> attributes = this.getAttributesFromBlock (ab);
+ for(ProVerifVar aa: attributes) {
+ String dec = declarations.get(makeAttrName(ab.getName(), aa.getName()));
+ if (dec == null)
+ lastInstr = lastInstr.setNextInstr (new ProVerifProcNew (aa.getName (), "bitstring"));
+ else if (dec.compareTo(aa.getName()) != 0)
+ lastInstr = lastInstr.setNextInstr (new ProVerifProcLet (new ProVerifVar[] {new ProVerifVar (aa.getName (), "bitstring")}, dec));
+ TraceManager.addDev("| AvatarAttribute: " + aa.getName ());
}
- AvatarStateMachine asm = ab.getStateMachine();
- AvatarStartState ass = asm.getStartState();
-
+ // Call the first "real" process
+ String tmp = "out (" + CHCTRL_CH + ", " + CHCTRL_ENCRYPT + " ((call__" + ab.getName () + "__0";
+ for(ProVerifVar aa: attributes)
+ tmp += ", " + aa.getName ();
+ lastInstr = lastInstr.setNextInstr (new ProVerifProcRaw (tmp + ")))"));
macs.clear();
-
- if (ass != null) {
- makeBlockProcesses(ab, asm, ass.getNext(0), p, tmpprocesses, states, null);
- }
+
+ // Generate a new process for every simplified element of the block's state machine
+ attributes.add (0, new ProVerifVar ("call__num", "bitstring"));
+ HashMap<AvatarStateMachineElement, Integer> simplifiedElements = ab.getStateMachine ().getSimplifiedElements ();
+ for (AvatarStateMachineElement asme: simplifiedElements.keySet ())
+ if (asme != null) {
+ // Create the ProVerif process and add it to the ProVerif specification
+ ProVerifProcInstr p = new ProVerifProcess(makeAttrName(ab.getName(), simplifiedElements.get (asme).toString ()), new ProVerifVar[] {});
+ this.spec.addDeclaration (p);
+
+ // TODO: add parameters
+ // Read and decrypt control data: variables sent to the process and the call__num variable
+ p = p.setNextInstr (new ProVerifProcIn (CHCTRL_CH, new ProVerifVar[] {new ProVerifVar ("chControlData", "bitstring")}));
+ p = p.setNextInstr (new ProVerifProcLet (attributes.toArray (new ProVerifVar[attributes.size()]), CHCTRL_DECRYPT + " (chControlData)"));
+
+ // Check that call__num variable really corresponds to this process
+ p = p.setNextInstr (new ProVerifProcITE ("call__num = call__" + ab.getName () + "__" + simplifiedElements.get (asme)));
+
+ // Create an object that will serve as an argument passed to the translation functions
+ ProVerifTranslatorParameter arg = new ProVerifTranslatorParameter ();
+ arg.block = ab;
+ arg.choiceInfo = null;
+ arg.lastInstr = p;
+ arg.simplifiedElements = simplifiedElements;
+
+ // Translate this simplified element
+ asme.translate (this, arg);
+ }
}
- public void makeBlockProcesses(AvatarBlock _block, AvatarStateMachine _asm, AvatarStateMachineElement _asme, ProVerifProcess _p, LinkedList<ProVerifProcess> _processes, LinkedList<AvatarState> _states, String _choiceInfo) {
- avatartranslator.AvatarSignal as;
- AvatarActionOnSignal aaos;
- AvatarTransition at;
- ProVerifProcess p, ptmp, ptmp1, ptmp2;
- String tmp, name, value, term;
- int i, j;
- int index0, index1;
- avatartranslator.AvatarMethod am;
- boolean found;
- LinkedList<String> pos;
-
- // Null element
- if (_asme == null) {
- terminate0Process(_p);
- return;
- }
+ class ProVerifTranslatorParameter {
+ AvatarBlock block;
+ String choiceInfo;
+ ProVerifProcInstr lastInstr;
+ HashMap<AvatarStateMachineElement, Integer> simplifiedElements;
+ }
- // Stop state
- if (_asme instanceof AvatarStopState) {
- terminate0Process(_p);
- return;
+ /**
+ * Commodity method that translates the transition to the next Avatar state machine element
+ */
+ private void translateNext (AvatarStateMachineElement current, AvatarStateMachineElement next, Object _arg) {
+ ProVerifTranslatorParameter arg = (ProVerifTranslatorParameter) _arg;
+ // Check if next is not null
+ if (next != null) {
+
+ // Check if next is the root of a process
+ Integer n = arg.simplifiedElements.get (next);
+ if (n != null) {
+ // If next is the root of a process send the attributes and arguments on the control channel
+ String tmp = "out (" + CHCTRL_CH + ", " + CHCTRL_ENCRYPT + " ((call__" + arg.block.getName () + "__" + n;
+ for(ProVerifVar aa: this.getAttributesFromBlock (arg.block))
+ tmp += ", " + aa.getName ();
+
+ // Generate the arguments to send to the next process from the previous Avatar transition
+ if (current instanceof AvatarTransition) {
+ for(AvatarActionAssignment action: ((AvatarTransition) current).getAssignments ()) {
+ AvatarLeftHand leftHand = action.getLeftHand ();
+ if (leftHand instanceof AvatarTuple)
+ for (AvatarTerm term: ((AvatarTuple) leftHand).getComponents ())
+ tmp += ", " + ((AvatarLocalVar) term).getName ();
+ else
+ tmp += ", " + ((AvatarLocalVar) leftHand).getName ();
+ }
- // Action on signal
- } else if (_asme instanceof AvatarActionOnSignal){
- aaos = (AvatarActionOnSignal)_asme;
- as = aaos.getSignal();
+ for(AvatarTermFunction action: ((AvatarTransition) current).getFunctionCalls ()) {
+ String name = action.getMethod ().getName ();
- boolean isPrivate = false;
- AvatarRelation ar = avspec.getAvatarRelationWithSignal(as);
- if (ar != null) {
- isPrivate = ar.isPrivate();
- }
+ if (name.equals ("get2") || name.equals ("get3") || name.equals ("get4")) {
+ LinkedList<AvatarTerm> args = action.getArgs ();
- if (as.isOut()) {
- if (aaos.getNbOfValues() == 0) {
- addLine(_p, "new data__");
+ if (args.get(0) instanceof AvatarLocalVar)
+ tmp += ", " + ((AvatarLocalVar) args.get(0)).getName ();
+ }
+ }
}
- tmp ="out";
- } else {
- tmp = "in";
+ arg.lastInstr.setNextInstr (new ProVerifProcRaw (tmp + ")))"));
}
+ else
+ // If the next state machine element is not the root of a process, simply translate it
+ next.translate (this, arg);
+ }
+ }
- if (!isPrivate) {
- tmp+="(ch, ";
- } else {
- tmp +="(chprivate, ";
- }
+ /**
+ * Translation function handling ActionOnSignal states
+ */
+ public void translateActionOnSignal (AvatarActionOnSignal _asme, Object _arg) {
+ TraceManager.addDev("| Action on signal");
+
+ ProVerifTranslatorParameter arg = (ProVerifTranslatorParameter) _arg;
+ avatartranslator.AvatarSignal as = _asme.getSignal();
+ ProVerifProcInstr _lastInstr = arg.lastInstr;
+
+ // Check if the channel is private
+ boolean isPrivate = false;
+ AvatarRelation ar = this.avspec.getAvatarRelationWithSignal(as);
+ if (ar != null)
+ isPrivate = ar.isPrivate();
+
+ if (as.isOut()) {
+ // If this is an out operation
- if (aaos.getNbOfValues() == 0) {
+ // Use a dummy name if no value is sent
+ if (_asme.getNbOfValues() == 0)
+ _lastInstr = _lastInstr.setNextInstr (new ProVerifProcNew ("data__", "bistring"));
+
+ String tmp = "out (" + CH_MAINCH + ", ";
+ if (isPrivate)
+ tmp += CH_ENCRYPT + " (";
+
+ if (_asme.getNbOfValues() == 0)
tmp += "data__";
- } else {
- for(i=0; i<aaos.getNbOfValues(); i++) {
- if (i>0) {
+ else
+ for(int i=0; i<_asme.getNbOfValues(); i++) {
+ if (i>0)
tmp += ", ";
- }
- // Work on authenticity
- /*if (hasAuthenticityPragma(as.isOut(), _block.getName(), aaos.getValue(i))) {
- if (as.isOut()) {
- addLine(_p, "event authenticity__" + _block.getName() + "__" + aaos.getValue(i) + "__out()");
- }
- }*/
- tmp += aaos.getValue(i);
+ tmp += _asme.getValue(i);
}
- }
- tmp += ")";
- addLine(_p, tmp);
- /*for(i=0; i<aaos.getNbOfValues(); i++) {
- if (hasAuthenticityPragma(as.isOut(), _block.getName(), aaos.getValue(i))) {
- if (!as.isOut()) {
- addLine(_p, "event authenticity__" + _block.getName() + "__" + aaos.getValue(i) + "__in()");
- }
- }
- }*/
- makeBlockProcesses(_block, _asm, _asme.getNext(0), _p, _processes, _states, null);
-
-
- // State
- } else if (_asme instanceof AvatarState){
- i = _states.indexOf(_asme);
- if (i != -1) {
- // State has already been met
- // Must branch to the corresponding process
- p = _processes.get(i);
- addLineNoEnd(_p, p.processName + ".");
- return;
- } else {
- // New state
- // We create a new process for each state
- p = new ProVerifProcess(_block.getName() + "__" + (_processes.size() + 1));
- spec.addProcess(p);
- _processes.add(p);
- _states.add((AvatarState)_asme);
- addLine(p, "event enteringState__" + _block.getName() + "__" + _asme.getName() + "()");
-
- // Adding an event if authenticity is concerned with that state
- pos = getAuthenticityPragmas( _block.getName(), _asme.getName());
- for(String sp: pos) {
- addLine(p, "event " + sp);
- }
+ if (isPrivate)
+ tmp += ")";
+ tmp += ")";
+ TraceManager.addDev("| | " + tmp);
- // Calling the new process from the old one
- addLine(_p, p.processName);
- terminateProcess(_p);
+ _lastInstr = _lastInstr.setNextInstr (new ProVerifProcRaw (tmp, true));
- // Making the new process (the old one is finished);
- if (_asme.nbOfNexts() ==0) {
- terminateProcess(p);
- return;
- }
+ } else {
+ // If it's an In operation
+ LinkedList<ProVerifVar> vars = new LinkedList<ProVerifVar> ();
+ if (_asme.getNbOfValues() == 0)
+ vars.add (new ProVerifVar ("data__", "bitstring"));
+ else
+ for(int i=0; i<_asme.getNbOfValues(); i++)
+ vars.add (new ProVerifVar (_asme.getValue(i), "bitstring"));
+
+ // If the channel is private use the CH_DECRYPT function
+ if (isPrivate) {
+ TraceManager.addDev("| | in (chPriv, ...)");
+ _lastInstr = _lastInstr.setNextInstr (new ProVerifProcIn (CH_MAINCH, new ProVerifVar[] {new ProVerifVar ("privChData", "bitstring")}));
+ _lastInstr = _lastInstr.setNextInstr (new ProVerifProcLet (vars.toArray (new ProVerifVar[vars.size()]), CH_DECRYPT + " (privChData)"));
+ } else {
+ TraceManager.addDev("| | in (ch, ...)");
+ _lastInstr = _lastInstr.setNextInstr (new ProVerifProcIn (CH_MAINCH, vars.toArray (new ProVerifVar[vars.size()])));
+ }
+ }
- if (_asme.nbOfNexts() ==1) {
- makeBlockProcesses(_block, _asm, _asme.getNext(0), p, _processes, _states, null);
- return ;
- }
+ arg.lastInstr = _lastInstr;
+ this.translateNext (_asme, _asme.getNext(0), arg);
+ }
+ /**
+ * Translation function handling Avatar Transitions
+ */
+ public void translateTransition (AvatarTransition _asme, Object _arg) {
+ TraceManager.addDev("| Transition");
+ ProVerifTranslatorParameter arg = (ProVerifTranslatorParameter) _arg;
+ ProVerifProcInstr _lastInstr = arg.lastInstr;
+
+ // Check if the transition is guarded
+ if (_asme.isGuarded()) {
+ String tmp = modifyGuard(arg.block, _asme.getGuard().toString ());
+ if (tmp != null) {
+ TraceManager.addDev("| | transition is guarded by " + tmp);
+ _lastInstr = _lastInstr.setNextInstr (new ProVerifProcITE (tmp));
+ } else {
+ CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "Guard: " + _asme.getGuard() + " in block " + arg.block.getName() + " is not supported. Replacing by an empty guard");
+ ce.setAvatarBlock(arg.block);
+ ce.setTDiagramPanel(((AvatarDesignPanel)(avspec.getReferenceObject())).getAvatarSMDPanel(arg.block.getName()));
+ ce.setTGComponent((TGComponent)(_asme.getReferenceObject()));
+ warnings.add(ce);
+ _lastInstr = _lastInstr.setNextInstr (new ProVerifProcRaw ("(* Unsuported guard:" + _asme.getGuard() + " *)"));
+ }
+ }
- 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()) + ")";
+ TraceManager.addDev("| | Actions");
+ // Loop over all assigment functions
+ for(AvatarActionAssignment action: _asme.getAssignments ()) {
+ TraceManager.addDev("| | | assignment found: " + action);
+
+ // Compute left hand part of the assignment
+ AvatarLeftHand leftHand = action.getLeftHand ();
+ LinkedList<ProVerifVar> proVerifLeftHand = new LinkedList<ProVerifVar> ();
+ if (leftHand instanceof AvatarTuple)
+ for (AvatarTerm term: ((AvatarTuple) leftHand).getComponents ())
+ proVerifLeftHand.add (new ProVerifVar (((AvatarLocalVar) term).getName (), "bitstring"));
+ else if (leftHand instanceof AvatarLocalVar)
+ proVerifLeftHand.add (new ProVerifVar (((AvatarLocalVar) leftHand).getName (), "bitstring"));
+ else
+ proVerifLeftHand.add (new ProVerifVar (((AvatarAttribute) leftHand).getName (), "bitstring"));
+
+ // Compute right part of assignment
+ AvatarTerm rightHand = action.getRightHand ();
+ String proVerifRightHand = null;
+ if (rightHand instanceof AvatarTermFunction) {
+ // If it's a function call
+ String name = ((AvatarTermFunction) rightHand).getMethod ().getName ();
+ LinkedList<AvatarTerm> args = ((AvatarTermFunction) rightHand).getArgs ();
+
+ if (name.equals ("verifyMAC") && advancedTranslation) {
+ // If the function called is verifyMAC and advanced translation is enabled, perform translation
+ _lastInstr = _lastInstr.setNextInstr (new ProVerifProcLet (new ProVerifVar[] {new ProVerifVar ("MAC__tmp0__" + GENERAL_ID, "bitstring")}, "MAC(" + args.get (0).getName () + " , " + args.get (1).getName () + ")"));
+ _lastInstr = _lastInstr.setNextInstr (new ProVerifProcLet (new ProVerifVar[] {new ProVerifVar ("MAC__tmp1__" + GENERAL_ID, "bitstring")}, args.get (2).getName ()));
+ macs.remove(leftHand.getName ());
+ macs.put(leftHand.getName (), new Integer(GENERAL_ID));
+ GENERAL_ID++;
+ } else if (name.equals ("concat2") || name.equals ("concat3") || name.equals ("concat4")) {
+ // If it's a concat function, just use tuples
+ String tmp = "(";
+ boolean first = true;
+ for (AvatarTerm term: args) {
+ if (first)
+ first = false;
+ else
+ tmp += ", ";
+ tmp += term.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 {
+ _lastInstr = _lastInstr.setNextInstr (new ProVerifProcLet (new ProVerifVar[] {new ProVerifVar (leftHand.getName (), "bitstring")}, tmp));
+ } else
+ // Else use the function as is
+ proVerifRightHand = this.translateTerm (rightHand);
+ } else
+ // If it's not a function, use it as is
+ proVerifRightHand = this.translateTerm (rightHand);
+
+ if (proVerifRightHand != null)
+ _lastInstr = _lastInstr.setNextInstr (new ProVerifProcLet (proVerifLeftHand.toArray (new ProVerifVar[proVerifLeftHand.size ()]), proVerifRightHand));
+ }
- // 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() + ")");
+ // Loop over all function calls
+ for(AvatarTermFunction action: _asme.getFunctionCalls ()) {
+ String name = action.getMethod ().getName ();
+ if (name.equals ("get2") || name.equals ("get3") || name.equals ("get4")) {
+ // If the function called is get[234]
+ LinkedList<AvatarTerm> args = action.getArgs ();
+ int index = (int) name.charAt (3) - 49;
- 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);
- }
+ if (args.get(0) instanceof AvatarLocalVar)
+ // Create the corresponding assignment
+ _lastInstr = _lastInstr.setNextInstr (new ProVerifProcLet (new ProVerifVar[] {new ProVerifVar (((AvatarLocalVar) args.get(0)).getName (), "bitstring")}, this.translateTerm (args.get (index))));
}
+ }
- // Transition
- } else if (_asme instanceof AvatarTransition) {
- at = (AvatarTransition)_asme;
- // Guard
- if (at.isGuarded()) {
- tmp = modifyGuard(at.getGuard());
- if (tmp != null) {
- TraceManager.addDev(" Adding guard: " + tmp);
- addLineNoEnd(_p, "if " + tmp + " then");
- } else {
- CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "Guard: " + at.getGuard() + " in block " + _block.getName() + " is not supported. Replacing by an empty guard");
- ce.setAvatarBlock(_block);
- ce.setTDiagramPanel(((AvatarDesignPanel)(avspec.getReferenceObject())).getAvatarSMDPanel(_block.getName()));
- ce.setTGComponent((TGComponent)(at.getReferenceObject()));
- warnings.add(ce);
- addLineNoEnd(_p, "(* Unsuported guard:" + at.getGuard() + " *)");
- }
- }
+ arg.lastInstr = _lastInstr;
+ this.translateNext (_asme, _asme.getNext(0), arg);
+ }
+ public void translateState (AvatarState _asme, Object _arg) {
+ TraceManager.addDev("| State");
+ ProVerifTranslatorParameter arg = (ProVerifTranslatorParameter) _arg;
+ ProVerifProcInstr _lastInstr = arg.lastInstr;
- // Transition from a state -> this transition must be the one selected
- if (_choiceInfo != null) {
- addLine(_p, "in(chprivate, m__)");
- tmp = "if choice__" + _choiceInfo + " = m__ then";
- addLineNoEnd(_p, tmp);
- }
+ // Adding an event for reachability of the state
+ _lastInstr = _lastInstr.setNextInstr (new ProVerifProcRaw ("event enteringState__" + arg.block.getName() + "__" + _asme.getName() + "()", true));
- // 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);
- index0 = tmp.indexOf('=');
- index1 = tmp.indexOf('(');
- term = "";
- if (index0 != -1) {
- term = tmp.substring(0, index0).trim();
- }
- if ((index0 == -1) || (index1 == -1) || (index0 > index1) || (term.length() == 0)) {
- name = tmp.substring(0, index1).trim();
- index0 = tmp.indexOf(')');
-
- // get functions
- if ((name.compareTo("get2") == 0) || (name.compareTo("get3") == 0) || (name.compareTo("get4") == 0)) {
- int index2 = tmp.indexOf(',');
- if ((index2 != -1) && (index2 > index1)) {
- addLineNoEnd(p, "let (" + tmp.substring(index2+1, index0+1).trim() + " = " + tmp.substring(index1+1, index2).trim() + " in");
- } else {
- addLineNoEnd(p, "let " + tmp + " in");
- }
- } else {
- addLineNoEnd(p, "let " + tmp + " in");
- }
+ // Adding an event if authenticity is concerned with that state
+ LinkedList<String> pos = getAuthenticityPragmas (arg.block.getName(), _asme.getName());
+ for(String sp: pos) {
+ TraceManager.addDev("| | authenticity event " + sp + "added");
+ _lastInstr = _lastInstr.setNextInstr (new ProVerifProcRaw ("event " + sp, true));
+ }
- } 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;
- }
- }
- }
+ int nbOfNexts = _asme.nbOfNexts ();
+ if (nbOfNexts == 0)
+ return;
+ else if (nbOfNexts == 1) {
+ arg.lastInstr = _lastInstr;
+ this.translateNext (_asme, _asme.getNext(0), arg);
- index0 = tmp.indexOf(')');
- if ((found) && (name.compareTo("verifyMAC") == 0) && (advancedTranslation)){
- // Verify MAC!
- 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__tmp0__" + GENERAL_ID + " = MAC(" + values[0].trim() + " , " + values[1].trim() + ") in");
- addLineNoEnd(p, "let MAC__tmp1__" + GENERAL_ID + " = " + values[2].trim() + " in");
-
- macs.remove(term);
- macs.put(term, new Integer(GENERAL_ID));
- GENERAL_ID++;
- //addLine(p, "new choice__mac");
- //addLine(p, "out(chprivate, choice__mac)");
-
- // We don't need anymore the two parralel process
- /*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 if ((name.compareTo("concat2") == 0) || (name.compareTo("concat3") == 0) || (name.compareTo("concat4") == 0)){
- addLineNoEnd(p, "let " + term + " = " + tmp.substring(index1, tmp.length()) + " in");
- } else if ((name.compareTo("get2") == 0) || (name.compareTo("get3") == 0) || (name.compareTo("get4") == 0)) {
- int index2 = tmp.indexOf(',');
- if ((index2 != -1) && (index2 > index1)) {
- addLineNoEnd(p, "let (" + tmp.substring(index2+1, index0) + " = " + tmp.substring(index1, index2) + " in");
- } else {
- addLineNoEnd(p, "let " + tmp + " in");
- }
- } else {
- addLineNoEnd(p, "let " + tmp + " in");
- }
+ } else if (_asme.hasElseChoiceType1()) {
+ TraceManager.addDev("| | calling next ITE");
+ ProVerifProcITE ite = new ProVerifProcITE (this.modifyGuard (arg.block, ((AvatarTransition) _asme.getNext (0)).getGuard ().toString ()));
+ arg.lastInstr = _lastInstr.setNextInstr (ite);
+ this.translateNext (_asme.getNext (0), _asme.getNext (0).getNext (0), arg);
- }
+ arg.lastInstr = ite.getElse ();
+ this.translateNext (_asme.getNext (1), _asme.getNext (1).getNext (0), arg);
- } else if (AvatarSpecification.isABasicVariableSettingString(tmp)) {
- TraceManager.addDev("Found variable setting: " + tmp);
- addLineNoEnd(p, "let " + tmp + " in ");
- } else {
- TraceManager.addDev("Assignment expression: " + tmp);
- int index = tmp.indexOf("=");
- if (index > -1) {
- String var = tmp.substring(0, index).trim();
- if (var.length() > 0) {
- addLine(p, "new " + var);
- }
- }
-
- }
+ } else {
+ TraceManager.addDev("| | non deterministic next state");
+ for (int i=0; i<nbOfNexts-1; i++) {
+ String choice = "choice__" + _asme.getName () + "__" + i;
+ _lastInstr = _lastInstr.setNextInstr (new ProVerifProcNew (choice, "bistring"));
+ _lastInstr = _lastInstr.setNextInstr (new ProVerifProcRaw ("out (" + CH_MAINCH + ", " + choice + ");"));
}
+ _lastInstr = _lastInstr.setNextInstr (new ProVerifProcIn (CH_MAINCH, new ProVerifVar[] {new ProVerifVar ("choice__" + _asme.getName (), "bitstring")}));
+ for (int i=0; i<nbOfNexts-1; i++) {
+ String choice = "choice__" + _asme.getName () + "__" + i;
+ ProVerifProcITE ite = new ProVerifProcITE ("choice__" + _asme.getName () + " = " + choice);
- makeBlockProcesses(_block, _asm, _asme.getNext(0), p, _processes, _states, null);
+ arg.lastInstr = _lastInstr.setNextInstr (ite);
+ this.translateNext (_asme, _asme.getNext (i), arg);
- // Ignored elements
- } else {
- // Go to the next element
- makeBlockProcesses(_block, _asm, _asme.getNext(0), _p, _processes, _states, null);
+ _lastInstr = ite.getElse ();
+ }
+
+ arg.lastInstr = _lastInstr;
+ this.translateNext (_asme, _asme.getNext (nbOfNexts-1), arg);
}
}
+ public void translateRandom (AvatarRandom _asme, Object _arg) {
+ this.translateNext (_asme, _asme.getNext(0), _arg);
+ }
+
+ public void translateStartState (AvatarStartState _asme, Object _arg) {
+ this.translateNext (_asme, _asme.getNext(0), _arg);
+ }
+
+ public void translateTimerOperator (AvatarTimerOperator _asme, Object _arg) {
+ this.translateNext (_asme, _asme.getNext(0), _arg);
+ }
+
+ public void translateStopState (AvatarStopState _asme, Object _arg) {
+ }
// Supported guards: a == b, not(a == b)
// -> transformed into a = b, a <> b
// Returns nulls otherwise
- public String modifyGuard(String _guard) {
+ public String modifyGuard(AvatarBlock _block, String _guard) {
String[] ab;
- TraceManager.addDev(" -> Analyzing guard: " + _guard);
-
String s = Conversion.replaceAllString(_guard, "[", "");
s = Conversion.replaceAllString(s, "]", "").trim();
s = Conversion.replaceAllString(s, " ", "");
@@ -1323,18 +1117,18 @@ public class AVATAR2ProVerif {
// Should have a "a == b";
- ab = getEqualGuard(s);
- if (ab == null) {
+ ab = getEqualGuard(_block, s);
+ if (ab == null)
return null;
- }
+
return ab[0] + " <> " + ab[1];
}
return null;
} else {
- ab = getEqualGuard(s);
- if (ab == null) {
+ ab = getEqualGuard(_block, s);
+ if (ab == null)
return null;
- }
+
return ab[0] + " = " + ab[1];
}
}
@@ -1343,13 +1137,14 @@ public class AVATAR2ProVerif {
// With a and b ids.
// Returns a and b
// Otherwise, returns null;
- public String[] getEqualGuard(String _guard) {
+ public String[] getEqualGuard(AvatarBlock _block, String _guard) {
Integer myInt;
- TraceManager.addDev(" -> Analyzing equal guard: " + _guard);
int index = _guard.indexOf("==");
if (index == -1) {
- _guard = myTrim(_guard);
- if (AvatarAttribute.isAValidAttributeName(_guard)) {
+ _guard = myTrim(_guard);
+ AvatarTerm term = AvatarTerm.createFromString (_block, _guard);
+ if (term instanceof AvatarLocalVar || term instanceof AvatarAttribute) {
+ _guard = term.getName ();
myInt = macs.get(_guard.trim());
String[] ab = new String[2];
if (myInt != null) {
@@ -1357,21 +1152,21 @@ public class AVATAR2ProVerif {
ab[1] = "MAC__tmp1__" + myInt.intValue();
} else {
ab[0] = _guard;
- ab[1] = "true";
+ ab[1] = TRUE;
}
return ab;
- } else {
- return null;
}
+
+ return null;
}
- String a = _guard.substring(0, index).trim();
- String b = _guard.substring(index+2, _guard.length()).trim();
+ AvatarTerm a = AvatarTerm.createFromString (_block, _guard.substring(0, index).trim());
+ AvatarTerm b = AvatarTerm.createFromString (_block, _guard.substring(index+2).trim());
- if (AvatarAttribute.isAValidAttributeName(a) && AvatarAttribute.isAValidAttributeName(b)) {
+ if ((a instanceof AvatarLocalVar || a instanceof AvatarAttribute) && (b instanceof AvatarLocalVar || b instanceof AvatarAttribute)) {
String[] ab = new String[2];
- ab[0] = a;
- ab[1] = b;
+ ab[0] = a.getName ();
+ ab[1] = b.getName ();
return ab;
}
@@ -1380,54 +1175,15 @@ public class AVATAR2ProVerif {
// Remove all begining and trailing parenthesis and spaces
private String myTrim(String toBeTrimmed) {
- int length = toBeTrimmed.length();
- String tmp = toBeTrimmed.trim();
- if (tmp.startsWith("(")) {
- tmp = tmp.substring(1, tmp.length());
- }
- if (tmp.endsWith(")")) {
- tmp = tmp.substring(0, tmp.length()-1);
- }
- if (tmp.length() != length) {
- return myTrim(tmp);
- }
- return tmp;
-
- }
-
- public void terminateProcess(ProVerifProcess _p) {
- if ((_p == null) || (_p.processLines == null)) {
- return;
- }
-
- if (_p.processLines.size() == 0) {
- return;
- }
-
- String s = _p.processLines.get(_p.processLines.size() - 1);
- s = s .trim();
- s = s.substring(0, s.length()-1) + ".";
- _p.processLines.remove(_p.processLines.size() - 1);
- _p.processLines.add(s);
- }
-
- public void terminate0Process(ProVerifProcess _p) {
- if ((_p == null) || (_p.processLines == null)) {
- return;
- }
-
- _p.processLines.add("0.");
- }
+ int length = toBeTrimmed.length();
+ String tmp = toBeTrimmed.trim();
+ while (tmp.startsWith("("))
+ tmp = tmp.substring(1).trim ();
+ while (tmp.endsWith(")"))
+ tmp = tmp.substring(0, tmp.length()-1).trim ();
-
- public void addLine(ProVerifProcess _p, String _line) {
- _p.processLines.add(_line + ";\n");
- }
-
- public void addLineNoEnd(ProVerifProcess _p, String _line) {
- _p.processLines.add(_line + "\n");
+ return tmp;
}
-
}
diff --git a/src/avatartranslator/touppaal/AVATAR2UPPAAL.java b/src/avatartranslator/touppaal/AVATAR2UPPAAL.java
index d6dac199c8c57a282e08b6ab9ba94eb65f2ad8b5..5daba7a38c982d7cb9973b1fca93a77367b86390 100755
--- a/src/avatartranslator/touppaal/AVATAR2UPPAAL.java
+++ b/src/avatartranslator/touppaal/AVATAR2UPPAAL.java
@@ -685,7 +685,7 @@ public class AVATAR2UPPAAL {
//TraceManager.addDev("Transition with guard = " + at.getGuard() + " previous=" + _previousState);
if ((at.getNext(0) instanceof AvatarActionOnSignal) && !(at.hasActions()) && _previousState) {
if (at.isGuarded()) {
- makeElementBehavior(_block, _template, _elt.getNext(0), _previous, _end, at.getGuard(), false, false);
+ makeElementBehavior(_block, _template, _elt.getNext(0), _previous, _end, at.getGuard().toString (), false, false);
} else {
makeElementBehavior(_block, _template, _elt.getNext(0), _previous, _end, null, false, false);
}
@@ -762,7 +762,7 @@ public class AVATAR2UPPAAL {
//_previous.setCommitted();
loc1 = addLocation(_template);
tr = addTransition(_template, _previous, loc1);
- tmps = convertGuard(_at.getGuard());
+ tmps = convertGuard(_at.getGuard().toString ());
setGuard(tr, tmps);
TraceManager.addDev("MAKE CHOICE from guard");
setSynchronization(tr, "makeChoice!");
@@ -786,10 +786,10 @@ public class AVATAR2UPPAAL {
if (_at.hasActions()) {
for(i=0; i<_at.getNbOfAction(); i++) {
TraceManager.addDev("Adding Action :" + _at.getAction(i));
- tmps = _at.getAction(i);
+ tmps = _at.getAction(i).toString ();
// Setting a variable
- if (AvatarSpecification.isAVariableSettingString(tmps)) {
+ if (AvatarAction.createFromString (_block, tmps).isAVariableSetting ()) {
loc1 = addLocation(_template);
//loc.setCommitted();
tr = addTransition(_template, loc, loc1);
@@ -813,7 +813,7 @@ public class AVATAR2UPPAAL {
} else {
loc.setUrgent();
}
- setSynchronization(tr, AvatarSpecification.getMethodCallFromAction(tmps) + "!");
+ setSynchronization(tr, ((AvatarTermFunction) AvatarAction.createFromString (_block, tmps)).getMethod ().getName () + "!");
madeTheChoice = true;
makeMethodCall(_block, tr, tmps);
loc = loc1;
@@ -875,7 +875,7 @@ public class AVATAR2UPPAAL {
// Computing guard
if (at.isGuarded()) {
- tmps = convertGuard(at.getGuard());
+ tmps = convertGuard(at.getGuard().toString ());
} else {
tmps = "";
}
@@ -891,8 +891,8 @@ public class AVATAR2UPPAAL {
}
} else if (at.hasActions()) {
- tmps0 = at.getAction(0);
- if (AvatarSpecification.isAVariableSettingString(tmps0)) {
+ tmps0 = at.getAction(0).toString ();
+ if (AvatarAction.createFromString (_block, tmps0).isAVariableSetting ()) {
// We must introduce a fake action
tr = addTransition(_template, _loc, locend);
if (tmps != null) {
@@ -994,53 +994,57 @@ public class AVATAR2UPPAAL {
}
public void makeMethodCall(AvatarBlock _block, UPPAALTransition _tr, String _call) {
- int j;
- AvatarAttribute aa;
- String result = "";
- int nbOfInt = 0;
- int nbOfBool = 0;
- String tmps;
-
- TraceManager.addDev("Making method call:" + _call);
-
- String mc = "";
- AvatarBlock block = _block;
- String method = AvatarSpecification.getMethodCallFromAction(_call);
-
- block = _block.getBlockOfMethodWithName(method);
-
- if (block != null) {
- mc = block.getName() + "__" + method + "!";
- }
-
- TraceManager.addDev("Method name:" + mc);
-
- setSynchronization(_tr, mc);
- for(j=0; j<AvatarSpecification.getNbOfParametersInAction(_call); j++) {
- tmps = AvatarSpecification.getParameterInAction(_call, j);
- TraceManager.addDev("Attribute #j: " + tmps);
- aa = _block.getAvatarAttributeWithName(tmps);
- if (aa != null) {
- if ((nbOfInt > 0) || (nbOfBool > 0)) {
- result = result + ",\n";
- }
- if (aa.isInt()) {
- result = result + ACTION_INT + nbOfInt + " =" + aa.getName();
- nbOfInt ++;
- } else {
- result = result + ACTION_BOOL + nbOfBool + " =" + aa.getName();
- nbOfBool ++;
- }
- }
- }
-
- if (result.length() > 0) {
- setAssignment(_tr, result);
- }
-
- nbOfIntParameters = Math.max(nbOfIntParameters, nbOfInt);
- nbOfBooleanParameters = Math.max(nbOfBooleanParameters, nbOfBool);
-
+ int j;
+ AvatarAttribute aa;
+ String result = "";
+ int nbOfInt = 0;
+ int nbOfBool = 0;
+ String tmps;
+
+ TraceManager.addDev("Making method call:" + _call);
+
+ String mc = "";
+ AvatarBlock block = _block;
+ AvatarAction action = AvatarAction.createFromString (_block, _call);
+ if (!action.isAMethodCall ())
+ return;
+
+ AvatarMethod avMethod = ((AvatarTermFunction) action).getMethod ();
+ String method = avMethod.getName ();
+
+ block = _block.getBlockOfMethodWithName(method);
+
+ if (block != null) {
+ mc = block.getName() + "__" + method + "!";
+ }
+
+ TraceManager.addDev("Method name:" + mc);
+
+ setSynchronization(_tr, mc);
+ LinkedList<AvatarTerm> arguments = ((AvatarTermFunction) action).getArgs ();
+ for(AvatarTerm arg: arguments) {
+ if (!(arg instanceof AvatarAttribute))
+ continue;
+
+ aa = (AvatarAttribute) arg;
+ if ((nbOfInt > 0) || (nbOfBool > 0))
+ result = result + ",\n";
+
+ if (aa.isInt()) {
+ result = result + ACTION_INT + nbOfInt + " =" + aa.getName();
+ nbOfInt ++;
+ } else {
+ result = result + ACTION_BOOL + nbOfBool + " =" + aa.getName();
+ nbOfBool ++;
+ }
+ }
+
+ if (result.length() > 0) {
+ setAssignment(_tr, result);
+ }
+
+ nbOfIntParameters = Math.max(nbOfIntParameters, nbOfInt);
+ nbOfBooleanParameters = Math.max(nbOfBooleanParameters, nbOfBool);
}
public UPPAALLocation makeTimeInterval(UPPAALTemplate _template, UPPAALLocation _previous, String _minint, String _maxint) {
diff --git a/src/proverifspec/ProVerifComment.java b/src/proverifspec/ProVerifComment.java
new file mode 100644
index 0000000000000000000000000000000000000000..be79bc1c9c902a523e978298d997e0df5a09ef24
--- /dev/null
+++ b/src/proverifspec/ProVerifComment.java
@@ -0,0 +1,69 @@
+/**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 ProVerifComment
+ * Creation: 13/09/2015
+ * @version 1.0 13/09/2015
+ * @author Florian LUGOU
+ * @see
+ */
+
+package proverifspec;
+
+import java.util.*;
+
+public class ProVerifComment implements ProVerifDeclaration {
+ protected LinkedList<String> lines;
+
+ public ProVerifComment () {
+ this.lines = new LinkedList<String> ();
+ }
+
+ public ProVerifComment (String _line) {
+ this ();
+ this.addLine (_line);
+ }
+
+ public void addLine (String _line) {
+ this.lines.add (_line);
+ }
+
+ public void translate (ProVerifSyntaxer _syntaxer, int _alinea) {
+ _syntaxer.translateComment (this, _alinea);
+ }
+}
diff --git a/src/proverifspec/ProVerifConst.java b/src/proverifspec/ProVerifConst.java
new file mode 100644
index 0000000000000000000000000000000000000000..1c680d8db3bb02dbf3a0beac31ec105198c18ed7
--- /dev/null
+++ b/src/proverifspec/ProVerifConst.java
@@ -0,0 +1,64 @@
+/**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 ProVerifConst
+ * Creation: 13/09/2015
+ * @version 1.0 13/09/2015
+ * @author Florian LUGOU
+ * @see
+ */
+
+package proverifspec;
+
+public class ProVerifConst implements ProVerifDeclaration {
+ protected String name;
+ protected String type;
+
+ public ProVerifConst (String _name) {
+ this.name = _name;
+ }
+
+ public ProVerifConst (String _name, String _type) {
+ this (_name);
+ this.type = _type;
+ }
+
+ public void translate (ProVerifSyntaxer _syntaxer, int _alinea) {
+ _syntaxer.translateConst (this, _alinea);
+ }
+}
diff --git a/src/proverifspec/ProVerifDeclaration.java b/src/proverifspec/ProVerifDeclaration.java
new file mode 100644
index 0000000000000000000000000000000000000000..258847c5a3d8c316562c2747ef7e437b3b570aca
--- /dev/null
+++ b/src/proverifspec/ProVerifDeclaration.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 ProVerifDeclaration
+ * Creation: 13/09/2015
+ * @version 1.0 13/09/2015
+ * @author Florian LUGOU
+ * @see
+ */
+
+package proverifspec;
+
+public interface ProVerifDeclaration {
+ public void translate (ProVerifSyntaxer _syntaxer, int _alinea);
+}
diff --git a/src/proverifspec/ProVerifEvDecl.java b/src/proverifspec/ProVerifEvDecl.java
new file mode 100644
index 0000000000000000000000000000000000000000..3709b33b30af558d08d526bac24f65882bc886f6
--- /dev/null
+++ b/src/proverifspec/ProVerifEvDecl.java
@@ -0,0 +1,60 @@
+/**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 ProVerifEvDecl
+ * Creation: 13/09/2015
+ * @version 1.0 13/09/2015
+ * @author Florian LUGOU
+ * @see
+ */
+
+package proverifspec;
+
+public class ProVerifEvDecl implements ProVerifDeclaration {
+ protected String name;
+ protected String[] args;
+
+ public ProVerifEvDecl (String _name, String[] _args) {
+ this.name = _name;
+ this.args = _args;
+ }
+
+ public void translate (ProVerifSyntaxer _syntaxer, int _alinea) {
+ _syntaxer.translateEvDecl (this, _alinea);
+ }
+}
diff --git a/src/proverifspec/ProVerifFunc.java b/src/proverifspec/ProVerifFunc.java
new file mode 100644
index 0000000000000000000000000000000000000000..de75473fa46e6f68228051aa7def3bea674de703
--- /dev/null
+++ b/src/proverifspec/ProVerifFunc.java
@@ -0,0 +1,68 @@
+/**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 ProVerifFunc
+ * Creation: 13/09/2015
+ * @version 1.0 13/09/2015
+ * @author Florian LUGOU
+ * @see
+ */
+
+package proverifspec;
+
+public class ProVerifFunc implements ProVerifDeclaration {
+ protected String name;
+ protected String[] types;
+ protected String returnType;
+ protected boolean priv;
+
+ public ProVerifFunc (String _name, String[] _types, String _returnType) {
+ this.name = _name;
+ this.types = _types;
+ this.returnType = _returnType;
+ }
+
+ public ProVerifFunc (String _name, String[] _types, String _returnType, boolean _priv) {
+ this (_name, _types, _returnType);
+ this.priv = _priv;
+ }
+
+ public void translate (ProVerifSyntaxer _syntaxer, int _alinea) {
+ _syntaxer.translateFunc (this, _alinea);
+ }
+}
diff --git a/src/proverifspec/ProVerifPiSyntaxer.java b/src/proverifspec/ProVerifPiSyntaxer.java
new file mode 100644
index 0000000000000000000000000000000000000000..42096540da1544dac8a155e7ec6bfc047f098650
--- /dev/null
+++ b/src/proverifspec/ProVerifPiSyntaxer.java
@@ -0,0 +1,164 @@
+/**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 ProVerifPiSyntaxer
+ * Creation: 13/09/2015
+ * @version 1.0 13/09/2015
+ * @author Florian LUGOU
+ * @see
+ */
+
+package proverifspec;
+
+public class ProVerifPiSyntaxer extends ProVerifSyntaxer {
+
+ protected void translateConst (ProVerifConst _node, int _alinea) {
+ this.fullSpec += "\n" + this.printAlinea (_alinea);
+ this.fullSpec += "data " + _node.name + "/0.";
+ }
+
+ protected void translateFunc (ProVerifFunc _node, int _alinea) {
+ this.fullSpec += "\n" + this.printAlinea (_alinea);
+ if (_node.priv)
+ this.fullSpec += "private ";
+ this.fullSpec += "fun " + _node.name + "/" + _node.types.length + ".";
+ }
+
+ protected void translateReduc (ProVerifReduc _node, int _alinea) {
+ this.fullSpec += "\n" + this.printAlinea (_alinea);
+ if (_node.priv)
+ this.fullSpec += "private ";
+ this.fullSpec += "reduc " + _node.formula + ".";
+ }
+
+ protected void translateVar (ProVerifVar _node, int _alinea) {
+ this.fullSpec += "\n" + this.printAlinea (_alinea);
+ if (_node.priv)
+ this.fullSpec += "private ";
+ this.fullSpec += "free " + _node.name + ".";
+ }
+
+ protected void translateQueryAtt (ProVerifQueryAtt _node, int _alinea) {
+ this.fullSpec += "\n" + this.printAlinea (_alinea);
+ this.fullSpec += "query attacker:" + _node.name + ".";
+ }
+
+ protected void translateQueryEv (ProVerifQueryEv _node, int _alinea) {
+ this.fullSpec += "\n" + this.printAlinea (_alinea);
+ this.fullSpec += "query ev:" + _node.name + "().";
+ }
+
+ protected void translateQueryEvinj (ProVerifQueryEvinj _node, int _alinea) {
+ this.fullSpec += "\n" + this.printAlinea (_alinea);
+ this.fullSpec += "query evinj:" + _node.ev1 + " ==> evinj:" + _node.ev2 + ".";
+ }
+
+ protected void translateEvDecl (ProVerifEvDecl _node, int _alinea) {
+ }
+
+ protected void translateProcess (ProVerifProcess _node, int _alinea) {
+ this.fullSpec += "\n\n" + this.printAlinea (_alinea);
+ this.fullSpec += "let " + _node.name + " =";
+ if (_node.next != null)
+ this.translate (_node.next, _alinea+1);
+ else
+ this.fullSpec += "0";
+ this.fullSpec += ".";
+ }
+
+ protected void translateProcNew (ProVerifProcNew _node, int _alinea) {
+ this.fullSpec += "\n" + this.printAlinea (_alinea);
+ this.fullSpec += "new " + _node.name + ";";
+ if (_node.next == null) {
+ this.fullSpec += "\n" + this.printAlinea (_alinea);
+ this.fullSpec += "0";
+ } else
+ this.translate (_node.next, _alinea);
+ }
+
+ protected void translateProcIn (ProVerifProcIn _node, int _alinea) {
+ this.fullSpec += "\n" + this.printAlinea (_alinea);
+ this.fullSpec += "in (" + _node.channel + ", ";
+ boolean first = true;
+ for (ProVerifVar var: _node.vars) {
+ if (first)
+ first = false;
+ else
+ this.fullSpec += ", ";
+ this.fullSpec += var.name;
+ }
+ this.fullSpec += ")";
+ if (_node.next != null) {
+ this.fullSpec += ";";
+ this.translate (_node.next, _alinea);
+ }
+ }
+
+ protected void translateProcCall (ProVerifProcCall _node, int _alinea) {
+ this.fullSpec += "\n" + this.printAlinea (_alinea);
+ this.fullSpec += _node.name;
+ if (_node.next != null) {
+ this.fullSpec += ";";
+ this.translate (_node.next, _alinea);
+ }
+ }
+
+ protected void translateProcLet (ProVerifProcLet _node, int _alinea) {
+ this.fullSpec += "\n" + this.printAlinea (_alinea);
+ this.fullSpec += "let ";
+ boolean first = true;
+ if (_node.vars.length > 1)
+ this.fullSpec += "(";
+ for (ProVerifVar var: _node.vars) {
+ if (first)
+ first = false;
+ else
+ this.fullSpec += ", ";
+ this.fullSpec += var.name;
+ }
+ if (_node.vars.length > 1)
+ this.fullSpec += ")";
+ this.fullSpec += " = " + _node.value + " in";
+ if (_node.next != null)
+ this.translate (_node.next, _alinea);
+ else {
+ this.fullSpec += "\n" + this.printAlinea (_alinea);
+ this.fullSpec += "0";
+ }
+ }
+}
diff --git a/src/proverifspec/ProVerifPitypeSyntaxer.java b/src/proverifspec/ProVerifPitypeSyntaxer.java
new file mode 100644
index 0000000000000000000000000000000000000000..e645c5598813fd26f37b724f9467b75ade06a72a
--- /dev/null
+++ b/src/proverifspec/ProVerifPitypeSyntaxer.java
@@ -0,0 +1,250 @@
+/**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 ProVerifPitypeSyntaxer
+ * Creation: 13/09/2015
+ * @version 1.0 13/09/2015
+ * @author Florian LUGOU
+ * @see
+ */
+
+package proverifspec;
+
+public class ProVerifPitypeSyntaxer extends ProVerifSyntaxer {
+
+ protected void translateConst (ProVerifConst _node, int _alinea) {
+ this.fullSpec += "\n" + this.printAlinea (_alinea);
+ this.fullSpec += "const " + _node.name + ": " + _node.type + " [data].";
+ }
+
+ protected void translateFunc (ProVerifFunc _node, int _alinea) {
+ this.fullSpec += "\n" + this.printAlinea (_alinea);
+ this.fullSpec += "fun " + _node.name + " (";
+ boolean first = true;
+ for (String type: _node.types) {
+ if (first)
+ first = false;
+ else
+ this.fullSpec += ", ";
+ this.fullSpec += type;
+ }
+ this.fullSpec += "): " + _node.returnType;
+ if (_node.priv)
+ this.fullSpec += " [private]";
+ this.fullSpec += ".";
+ }
+
+ protected void translateReduc (ProVerifReduc _node, int _alinea) {
+ this.fullSpec += "\n" + this.printAlinea (_alinea);
+ this.fullSpec += "reduc ";
+ if (_node.vars.length > 0) {
+ this.fullSpec += "forall ";
+ boolean first = true;
+ for (ProVerifVar var: _node.vars) {
+ if (first)
+ first = false;
+ else
+ this.fullSpec += ", ";
+ this.fullSpec += var.name + ": " + var.type;
+ }
+ this.fullSpec += "; ";
+ }
+ this.fullSpec += _node.formula;
+ if (_node.priv)
+ this.fullSpec += " [private]";
+ this.fullSpec += ".";
+ }
+
+ protected void translateVar (ProVerifVar _node, int _alinea) {
+ this.fullSpec += "\n" + this.printAlinea (_alinea);
+ this.fullSpec += "free " + _node.name + ": " + _node.type;
+ if (_node.priv)
+ this.fullSpec += " [private]";
+ this.fullSpec += ".";
+ }
+
+ protected void translateQueryAtt (ProVerifQueryAtt _node, int _alinea) {
+ this.fullSpec += "\n" + this.printAlinea (_alinea);
+ this.fullSpec += "query attacker(" + _node.name + ").";
+ }
+
+ protected void translateQueryEv (ProVerifQueryEv _node, int _alinea) {
+ this.fullSpec += "\n" + this.printAlinea (_alinea);
+ this.fullSpec += "query ";
+ if (_node.vars.length > 0) {
+ boolean first = true;
+ for (ProVerifVar var: _node.vars) {
+ if (first)
+ first = false;
+ else
+ this.fullSpec += ", ";
+ this.fullSpec += var.name + ": " + var.type;
+ }
+ this.fullSpec += "; ";
+ }
+ this.fullSpec += "event(" + _node.name + "()).";
+ }
+
+ protected void translateQueryEvinj (ProVerifQueryEvinj _node, int _alinea) {
+ this.fullSpec += "\n" + this.printAlinea (_alinea);
+ this.fullSpec += "query ";
+ if (_node.vars.length > 0) {
+ boolean first = true;
+ for (ProVerifVar var: _node.vars) {
+ if (first)
+ first = false;
+ else
+ this.fullSpec += ", ";
+ this.fullSpec += var.name + ": " + var.type;
+ }
+ this.fullSpec += "; ";
+ }
+ this.fullSpec += "inj-event(" + _node.ev1 + ") ==> inj-event(" + _node.ev2 + ").";
+ }
+
+ protected void translateEvDecl (ProVerifEvDecl _node, int _alinea) {
+ this.fullSpec += "\n" + this.printAlinea (_alinea);
+ this.fullSpec += "event " + _node.name + "(";
+ boolean first = true;
+ for (String arg: _node.args) {
+ if (first)
+ first = false;
+ else
+ this.fullSpec += ", ";
+ this.fullSpec += arg;
+ }
+ this.fullSpec += ").";
+ }
+
+ protected void translateProcess (ProVerifProcess _node, int _alinea) {
+ this.fullSpec += "\n\n" + this.printAlinea (_alinea);
+ this.fullSpec += "let " + _node.name;
+ if (_node.args.length > 0) {
+ boolean first = true;
+ this.fullSpec += " (";
+ for (ProVerifVar var: _node.args) {
+ if (first)
+ first = false;
+ else
+ this.fullSpec += ", ";
+ this.fullSpec += var.name + ": " + var.type;
+ }
+ this.fullSpec += ")";
+ }
+ this.fullSpec += " =";
+ if (_node.next != null)
+ this.translate (_node.next, _alinea+1);
+ else
+ this.fullSpec += " 0";
+ this.fullSpec += ".";
+ }
+
+ protected void translateProcNew (ProVerifProcNew _node, int _alinea) {
+ this.fullSpec += "\n" + this.printAlinea (_alinea);
+ this.fullSpec += "new " + _node.name + ": " + _node.type + ";";
+ if (_node.next == null) {
+ this.fullSpec += "\n" + this.printAlinea (_alinea);
+ this.fullSpec += "0";
+ } else
+ this.translate (_node.next, _alinea);
+ }
+
+ protected void translateProcIn (ProVerifProcIn _node, int _alinea) {
+ this.fullSpec += "\n" + this.printAlinea (_alinea);
+ this.fullSpec += "in (" + _node.channel + ", ";
+ boolean first = true;
+ for (ProVerifVar var: _node.vars) {
+ if (first)
+ first = false;
+ else
+ this.fullSpec += ", ";
+ this.fullSpec += var.name + ": " + var.type;
+ }
+ this.fullSpec += ")";
+ if (_node.next != null) {
+ this.fullSpec += ";";
+ this.translate (_node.next, _alinea);
+ }
+ }
+
+ protected void translateProcCall (ProVerifProcCall _node, int _alinea) {
+ this.fullSpec += "\n" + this.printAlinea (_alinea);
+ this.fullSpec += _node.name;
+ if (_node.args.length > 0) {
+ boolean first = true;
+ this.fullSpec += " (";
+ for (ProVerifVar var: _node.args) {
+ if (first)
+ first = false;
+ else
+ this.fullSpec += ", ";
+ this.fullSpec += var.name;
+ }
+ this.fullSpec += ")";
+ }
+
+ if (_node.next != null) {
+ this.fullSpec += ";";
+ this.translate (_node.next, _alinea);
+ }
+ }
+
+ protected void translateProcLet (ProVerifProcLet _node, int _alinea) {
+ this.fullSpec += "\n" + this.printAlinea (_alinea);
+ this.fullSpec += "let ";
+ boolean first = true;
+ if (_node.vars.length > 1)
+ this.fullSpec += "(";
+ for (ProVerifVar var: _node.vars) {
+ if (first)
+ first = false;
+ else
+ this.fullSpec += ", ";
+ this.fullSpec += var.name + ": " + var.type;
+ }
+ if (_node.vars.length > 1)
+ this.fullSpec += ")";
+ this.fullSpec += " = " + _node.value + " in";
+ if (_node.next != null)
+ this.translate (_node.next, _alinea);
+ else {
+ this.fullSpec += "\n" + this.printAlinea (_alinea);
+ this.fullSpec += "0";
+ }
+ }
+}
diff --git a/src/proverifspec/ProVerifProcCall.java b/src/proverifspec/ProVerifProcCall.java
new file mode 100644
index 0000000000000000000000000000000000000000..e67a22295e8cae49191b0609d4520876930d0a98
--- /dev/null
+++ b/src/proverifspec/ProVerifProcCall.java
@@ -0,0 +1,61 @@
+/**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 ProVerifProcCall
+ * Creation: 13/09/2015
+ * @version 1.0 13/09/2015
+ * @author Florian LUGOU
+ * @see
+ */
+
+package proverifspec;
+
+public class ProVerifProcCall extends ProVerifProcInstr {
+
+ protected String name;
+ protected ProVerifVar[] args;
+
+ public ProVerifProcCall (String _name, ProVerifVar[] _args) {
+ this.name = _name;
+ this.args = _args;
+ }
+
+ public void translate (ProVerifSyntaxer _syntaxer, int _alinea) {
+ _syntaxer.translateProcCall (this, _alinea);
+ }
+}
diff --git a/src/proverifspec/ProVerifProcITE.java b/src/proverifspec/ProVerifProcITE.java
new file mode 100644
index 0000000000000000000000000000000000000000..92a019bcce3278349b879fad1e8fd357bab64f2a
--- /dev/null
+++ b/src/proverifspec/ProVerifProcITE.java
@@ -0,0 +1,67 @@
+/**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 ProVerifProcITE
+ * Creation: 13/09/2015
+ * @version 1.0 13/09/2015
+ * @author Florian LUGOU
+ * @see
+ */
+
+package proverifspec;
+
+public class ProVerifProcITE extends ProVerifProcInstr {
+
+ protected String cond;
+ protected ProVerifProcInstr elseInstr;
+
+ public ProVerifProcITE (String _cond) {
+ this.cond = _cond;
+ this.elseInstr = new ProVerifProcInstr () {
+ public void translate (ProVerifSyntaxer _syntaxer, int _alinea) { }
+ };
+ }
+
+ public ProVerifProcInstr getElse () {
+ return this.elseInstr;
+ }
+
+ public void translate (ProVerifSyntaxer _syntaxer, int _alinea) {
+ _syntaxer.translateProcITE (this, _alinea);
+ }
+}
diff --git a/src/proverifspec/ProVerifProcIn.java b/src/proverifspec/ProVerifProcIn.java
new file mode 100644
index 0000000000000000000000000000000000000000..e5922052257b1ff7d90a03ad0e784c9630822a7b
--- /dev/null
+++ b/src/proverifspec/ProVerifProcIn.java
@@ -0,0 +1,61 @@
+/**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 ProVerifProcIn
+ * Creation: 13/09/2015
+ * @version 1.0 13/09/2015
+ * @author Florian LUGOU
+ * @see
+ */
+
+package proverifspec;
+
+public class ProVerifProcIn extends ProVerifProcInstr {
+
+ protected String channel;
+ protected ProVerifVar[] vars;
+
+ public ProVerifProcIn (String _channel, ProVerifVar[] _vars) {
+ this.channel = _channel;
+ this.vars = _vars;
+ }
+
+ public void translate (ProVerifSyntaxer _syntaxer, int _alinea) {
+ _syntaxer.translateProcIn (this, _alinea);
+ }
+}
diff --git a/src/proverifspec/ProVerifProcInstr.java b/src/proverifspec/ProVerifProcInstr.java
new file mode 100644
index 0000000000000000000000000000000000000000..5f8904930325d47050a755fd17f9d36e18869d75
--- /dev/null
+++ b/src/proverifspec/ProVerifProcInstr.java
@@ -0,0 +1,59 @@
+/**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 ProVerifProcInstr
+ * Creation: 13/09/2015
+ * @version 1.0 13/09/2015
+ * @author Florian LUGOU
+ * @see
+ */
+
+package proverifspec;
+
+public abstract class ProVerifProcInstr implements ProVerifDeclaration {
+
+ protected ProVerifProcInstr next;
+
+ public ProVerifProcInstr setNextInstr (ProVerifProcInstr _next) {
+ if (_next == null)
+ return this;
+
+ this.next = _next;
+ return _next;
+ }
+}
diff --git a/src/proverifspec/ProVerifProcLet.java b/src/proverifspec/ProVerifProcLet.java
new file mode 100644
index 0000000000000000000000000000000000000000..a5fd6dba6808c707d176692592db4ac5e77a2e1c
--- /dev/null
+++ b/src/proverifspec/ProVerifProcLet.java
@@ -0,0 +1,61 @@
+/**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 ProVerifProcLet
+ * Creation: 13/09/2015
+ * @version 1.0 13/09/2015
+ * @author Florian LUGOU
+ * @see
+ */
+
+package proverifspec;
+
+public class ProVerifProcLet extends ProVerifProcInstr {
+
+ protected ProVerifVar[] vars;
+ protected String value;
+
+ public ProVerifProcLet (ProVerifVar[] _vars, String _value) {
+ this.vars = _vars;
+ this.value = _value;
+ }
+
+ public void translate (ProVerifSyntaxer _syntaxer, int _alinea) {
+ _syntaxer.translateProcLet (this, _alinea);
+ }
+}
diff --git a/src/proverifspec/ProVerifProcNew.java b/src/proverifspec/ProVerifProcNew.java
new file mode 100644
index 0000000000000000000000000000000000000000..61922b04e6391c4ee751b79116ea14b396f5f719
--- /dev/null
+++ b/src/proverifspec/ProVerifProcNew.java
@@ -0,0 +1,65 @@
+/**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 ProVerifProcNew
+ * Creation: 13/09/2015
+ * @version 1.0 13/09/2015
+ * @author Florian LUGOU
+ * @see
+ */
+
+package proverifspec;
+
+public class ProVerifProcNew extends ProVerifProcInstr {
+
+ protected String name;
+ protected String type;
+
+ public ProVerifProcNew (String _name) {
+ this.name = _name;
+ }
+
+ public ProVerifProcNew (String _name, String _type) {
+ this (_name);
+ this.type = _type;
+ }
+
+ public void translate (ProVerifSyntaxer _syntaxer, int _alinea) {
+ _syntaxer.translateProcNew (this, _alinea);
+ }
+}
diff --git a/src/proverifspec/ProVerifProcParallel.java b/src/proverifspec/ProVerifProcParallel.java
new file mode 100644
index 0000000000000000000000000000000000000000..7c4ced67309e0474c22f523d14c69c1d55213a70
--- /dev/null
+++ b/src/proverifspec/ProVerifProcParallel.java
@@ -0,0 +1,65 @@
+/**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 ProVerifProcParallel
+ * Creation: 13/09/2015
+ * @version 1.0 13/09/2015
+ * @author Florian LUGOU
+ * @see
+ */
+
+package proverifspec;
+
+import java.util.LinkedList;
+
+public class ProVerifProcParallel extends ProVerifProcInstr {
+
+ protected LinkedList<ProVerifProcInstr> instrs;
+
+ public ProVerifProcParallel () {
+ this.instrs = new LinkedList<ProVerifProcInstr> ();
+ }
+
+ public void addInstr (ProVerifProcInstr instr) {
+ this.instrs.add (instr);
+ }
+
+ public void translate (ProVerifSyntaxer _syntaxer, int _alinea) {
+ _syntaxer.translateProcParallel (this, _alinea);
+ }
+}
diff --git a/src/proverifspec/ProVerifProcRaw.java b/src/proverifspec/ProVerifProcRaw.java
new file mode 100644
index 0000000000000000000000000000000000000000..717efc40d7c4d854a04ebcafc650a35bba51d116
--- /dev/null
+++ b/src/proverifspec/ProVerifProcRaw.java
@@ -0,0 +1,66 @@
+/**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 ProVerifProcRaw
+ * Creation: 13/09/2015
+ * @version 1.0 13/09/2015
+ * @author Florian LUGOU
+ * @see
+ */
+
+package proverifspec;
+
+public class ProVerifProcRaw extends ProVerifProcInstr {
+
+ protected String raw;
+ protected boolean nextOptional;
+
+ public ProVerifProcRaw (String _raw) {
+ this.raw = _raw;
+ this.nextOptional = false;
+ }
+
+ public ProVerifProcRaw (String _raw, boolean _nextOptional) {
+ this.raw = _raw;
+ this.nextOptional = _nextOptional;
+ }
+
+ public void translate (ProVerifSyntaxer _syntaxer, int _alinea) {
+ _syntaxer.translateProcRaw (this, _alinea);
+ }
+}
diff --git a/src/proverifspec/ProVerifProcRawGlobing.java b/src/proverifspec/ProVerifProcRawGlobing.java
new file mode 100644
index 0000000000000000000000000000000000000000..dd605d87f44422f5b91732d29dcd8d98b0617ab9
--- /dev/null
+++ b/src/proverifspec/ProVerifProcRawGlobing.java
@@ -0,0 +1,69 @@
+/**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 ProVerifProcRawGlobing
+ * Creation: 13/09/2015
+ * @version 1.0 13/09/2015
+ * @author Florian LUGOU
+ * @see
+ */
+
+package proverifspec;
+
+public class ProVerifProcRawGlobing extends ProVerifProcInstr {
+
+ protected String before;
+ protected String after;
+ protected ProVerifProcInstr intraInstr;
+
+ public ProVerifProcRawGlobing (String _before, String _after) {
+ this.before = _before;
+ this.after = _after;
+ this.intraInstr = new ProVerifProcInstr () {
+ public void translate (ProVerifSyntaxer _syntaxer, int _alinea) { }
+ };
+ }
+
+ public ProVerifProcInstr getIntra () {
+ return this.intraInstr;
+ }
+
+ public void translate (ProVerifSyntaxer _syntaxer, int _alinea) {
+ _syntaxer.translateProcRawGlobing (this, _alinea);
+ }
+}
diff --git a/src/proverifspec/ProVerifProcess.java b/src/proverifspec/ProVerifProcess.java
index c381d3dba035f286c2a1dca537f0bf6afa739975..70e7613e68ffc578742603be3b8a1db2f2435e18 100755
--- a/src/proverifspec/ProVerifProcess.java
+++ b/src/proverifspec/ProVerifProcess.java
@@ -1,47 +1,47 @@
/**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 ProVerifProcess
-* Creation: 03/09/2010
-* @version 1.0 03/09/2010
-* @author Ludovic APVRILLE
-* @see
-*/
+ *
+ * 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 ProVerifProcess
+ * Creation: 03/09/2010
+ * @version 1.0 03/09/2010
+ * @author Ludovic APVRILLE
+ * @see
+ */
package proverifspec;
@@ -50,17 +50,29 @@ import java.util.*;
import myutil.*;
-public class ProVerifProcess {
- public String processName;
- public LinkedList<String> processLines;
+public class ProVerifProcess extends ProVerifProcInstr {
+ protected String name;
+ protected ProVerifVar[] args;
- public ProVerifProcess() {
- processLines = new LinkedList<String>();
+ public ProVerifProcess(String _name) {
+ this.name = _name;
}
-
- public ProVerifProcess(String _processName) {
- processName = _processName;
- processLines = new LinkedList<String>();
- }
-
-}
\ No newline at end of file
+
+ public ProVerifProcess(String _name, ProVerifVar[] _args) {
+ this (_name);
+ this.args = _args;
+ }
+
+ public ProVerifProcess(String _name, ProVerifVar[] _args, ProVerifProcInstr _next) {
+ this (_name, _args);
+ this.next = _next;
+ }
+
+ public String getName () {
+ return this.name;
+ }
+
+ public void translate (ProVerifSyntaxer _syntaxer, int _alinea) {
+ _syntaxer.translateProcess (this, _alinea);
+ }
+}
diff --git a/src/proverifspec/ProVerifQueryAtt.java b/src/proverifspec/ProVerifQueryAtt.java
new file mode 100644
index 0000000000000000000000000000000000000000..8d54055e307a8f856cfc73da29b07d59328e8043
--- /dev/null
+++ b/src/proverifspec/ProVerifQueryAtt.java
@@ -0,0 +1,58 @@
+/**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 ProVerifQueryAtt
+ * Creation: 13/09/2015
+ * @version 1.0 13/09/2015
+ * @author Florian LUGOU
+ * @see
+ */
+
+package proverifspec;
+
+public class ProVerifQueryAtt implements ProVerifDeclaration {
+ protected String name;
+
+ public ProVerifQueryAtt (String _name) {
+ this.name = _name;
+ }
+
+ public void translate (ProVerifSyntaxer _syntaxer, int _alinea) {
+ _syntaxer.translateQueryAtt (this, _alinea);
+ }
+}
diff --git a/src/proverifspec/ProVerifQueryEv.java b/src/proverifspec/ProVerifQueryEv.java
new file mode 100644
index 0000000000000000000000000000000000000000..92b4643582f60733407b6e286ea9d35f688cebf0
--- /dev/null
+++ b/src/proverifspec/ProVerifQueryEv.java
@@ -0,0 +1,60 @@
+/**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 ProVerifQueryEv
+ * Creation: 13/09/2015
+ * @version 1.0 13/09/2015
+ * @author Florian LUGOU
+ * @see
+ */
+
+package proverifspec;
+
+public class ProVerifQueryEv implements ProVerifDeclaration {
+ protected String name;
+ protected ProVerifVar[] vars;
+
+ public ProVerifQueryEv (ProVerifVar[] _vars, String _name) {
+ this.vars = _vars;
+ this.name = _name;
+ }
+
+ public void translate (ProVerifSyntaxer _syntaxer, int _alinea) {
+ _syntaxer.translateQueryEv (this, _alinea);
+ }
+}
diff --git a/src/proverifspec/ProVerifQueryEvinj.java b/src/proverifspec/ProVerifQueryEvinj.java
new file mode 100644
index 0000000000000000000000000000000000000000..e66c423b9a8b1513aa878a636c77cdd99c60532a
--- /dev/null
+++ b/src/proverifspec/ProVerifQueryEvinj.java
@@ -0,0 +1,61 @@
+/**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 ProVerifQueryEvinj
+ * Creation: 13/09/2015
+ * @version 1.0 13/09/2015
+ * @author Florian LUGOU
+ * @see
+ */
+
+package proverifspec;
+
+public class ProVerifQueryEvinj implements ProVerifDeclaration {
+ protected String ev1, ev2;
+ protected ProVerifVar[] vars;
+
+ public ProVerifQueryEvinj (ProVerifVar[] _vars, String _ev1, String _ev2) {
+ this.vars = _vars;
+ this.ev1 = _ev1;
+ this.ev2 = _ev2;
+ }
+
+ public void translate (ProVerifSyntaxer _syntaxer, int _alinea) {
+ _syntaxer.translateQueryEvinj (this, _alinea);
+ }
+}
diff --git a/src/proverifspec/ProVerifReduc.java b/src/proverifspec/ProVerifReduc.java
new file mode 100644
index 0000000000000000000000000000000000000000..a8753a4a7a3eb7e688efa8300c2e43988648559d
--- /dev/null
+++ b/src/proverifspec/ProVerifReduc.java
@@ -0,0 +1,66 @@
+/**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 ProVerifReduc
+ * Creation: 13/09/2015
+ * @version 1.0 13/09/2015
+ * @author Florian LUGOU
+ * @see
+ */
+
+package proverifspec;
+
+public class ProVerifReduc implements ProVerifDeclaration {
+ protected ProVerifVar[] vars;
+ protected String formula;
+ protected boolean priv;
+
+ public ProVerifReduc (ProVerifVar[] _vars, String _formula) {
+ this.vars = _vars;
+ this.formula = _formula;
+ }
+
+ public ProVerifReduc (ProVerifVar[] _vars, String _formula, boolean _priv) {
+ this (_vars, _formula);
+ this.priv = _priv;
+ }
+
+ public void translate (ProVerifSyntaxer _syntaxer, int _alinea) {
+ _syntaxer.translateReduc (this, _alinea);
+ }
+}
diff --git a/src/proverifspec/ProVerifSecrecyAssum.java b/src/proverifspec/ProVerifSecrecyAssum.java
new file mode 100644
index 0000000000000000000000000000000000000000..21a5178254223446b2e94e6ea1760da0c7d81334
--- /dev/null
+++ b/src/proverifspec/ProVerifSecrecyAssum.java
@@ -0,0 +1,58 @@
+/**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 ProVerifSecrecyAssum
+ * Creation: 13/09/2015
+ * @version 1.0 13/09/2015
+ * @author Florian LUGOU
+ * @see
+ */
+
+package proverifspec;
+
+public class ProVerifSecrecyAssum implements ProVerifDeclaration {
+ protected String name;
+
+ public ProVerifSecrecyAssum (String _name) {
+ this.name = _name;
+ }
+
+ public void translate (ProVerifSyntaxer _syntaxer, int _alinea) {
+ _syntaxer.translateSecrecyAssum (this, _alinea);
+ }
+}
diff --git a/src/proverifspec/ProVerifSpec.java b/src/proverifspec/ProVerifSpec.java
index da8ecc19e6d29a64c0ad2cd6fa2a15e18ec402e7..99011a031660d843b52ee3244c82f612e00e9b65 100755
--- a/src/proverifspec/ProVerifSpec.java
+++ b/src/proverifspec/ProVerifSpec.java
@@ -1,47 +1,47 @@
/**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 ProVerifSpec
-* Creation: 03/09/2010
-* @version 1.0 03/09/2010
-* @author Ludovic APVRILLE
-* @see
-*/
+ *
+ * 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 ProVerifSpec
+ * Creation: 13/09/2015
+ * @version 1.0 13/09/2015
+ * @author Florian LUGOU
+ * @see
+ */
package proverifspec;
@@ -50,87 +50,44 @@ import java.util.*;
import myutil.*;
-public class ProVerifSpec {
-
- private static final String DEC = "\t";
-
- private String globalDeclaration = "";
- private LinkedList<ProVerifProcess> processes;
- private LinkedList<ProVerifQuery> queries;
- private LinkedList<ProVerifFunction> functions;
-
- private ProVerifProcess startingProcess;
-
- private String fullSpec;
-
-
- public ProVerifSpec() {
- processes = new LinkedList<ProVerifProcess>();
- queries = new LinkedList<ProVerifQuery>();
- functions = new LinkedList<ProVerifFunction>();
+public class ProVerifSpec implements ProVerifDeclaration {
+
+ protected ProVerifProcess mainProcess;
+ protected LinkedList<ProVerifDeclaration> declarations;
+ protected boolean modified;
+
+ private ProVerifSyntaxer syntaxer;
+
+ public ProVerifSpec(ProVerifSyntaxer _syntaxer) {
+ this.declarations = new LinkedList<ProVerifDeclaration>();
+ this.declarations.add (new ProVerifComment ("Generated ProVerif specification"));
+ this.syntaxer = _syntaxer;
+ this.modified = true;
}
-
- public String getStringSpec() {
- return fullSpec;
- }
-
- public String makeSpec() {
- // Global code
- fullSpec = "(* Generated proverif specification *)\n\n";
- fullSpec += globalDeclaration;
-
- // Processes
- for(ProVerifProcess p: processes) {
- if (p != startingProcess) {
- fullSpec += "\n\nlet " + p.processName + " = \n";
- for(String s:p.processLines) {
- fullSpec += DEC + s;
- }
- }
- }
-
- // Starting process
- if (startingProcess != null) {
- fullSpec += "\n\nprocess\n";
- for(String s:startingProcess.processLines) {
- fullSpec += DEC + s + "\n";
- }
- }
-
-
- return fullSpec;
+
+ public String getStringSpec() {
+ if (this.syntaxer != null)
+ return this.syntaxer.getStringSpec (this);
+ // TODO: raise error
+ return "";
}
-
- public LinkedList<ProVerifProcess> getProcesses() {
- return processes;
+
+ public void setMainProcess (ProVerifProcess _mainProcess) {
+ this.mainProcess = _mainProcess;
+ this.modified = true;
}
-
- public LinkedList<ProVerifQuery> getQueries() {
- return queries;
+
+ public void addDeclaration (ProVerifDeclaration _d) {
+ this.declarations.add(_d);
+ this.modified = true;
+ }
+
+ public void setSyntaxer (ProVerifSyntaxer _syntaxer) {
+ this.syntaxer = _syntaxer;
+ this.modified = true;
}
-
- public LinkedList<ProVerifFunction> getFunctions() {
- return functions;
+
+ public void translate (ProVerifSyntaxer _syntaxer, int _alinea) {
+ _syntaxer.translateSpec (this, _alinea);
}
-
- public void addProcess(ProVerifProcess _p) {
- processes.add(_p);
- }
-
- public void addQuery(ProVerifQuery _q) {
- queries.add(_q);
- }
-
- public void addFunction(ProVerifFunction _f) {
- functions.add(_f);
- }
-
- public void setStartingProcess(ProVerifProcess _process) {
- startingProcess = _process;
- }
-
- public void addToGlobalSpecification(String _text) {
- globalDeclaration += _text;
- }
-
-}
\ No newline at end of file
+}
diff --git a/src/proverifspec/ProVerifSyntaxer.java b/src/proverifspec/ProVerifSyntaxer.java
new file mode 100644
index 0000000000000000000000000000000000000000..cc6ad316570b6e738b62bb4f82385c2549cf9614
--- /dev/null
+++ b/src/proverifspec/ProVerifSyntaxer.java
@@ -0,0 +1,206 @@
+/**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 ProVerifSyntaxer
+ * Creation: 13/09/2015
+ * @version 1.0 13/09/2015
+ * @author Florian LUGOU
+ * @see
+ */
+
+package proverifspec;
+
+import myutil.*;
+
+public abstract class ProVerifSyntaxer {
+
+ public static final String DEC = "\t";
+ public static final int DECLEN = DEC.length();
+
+ protected String fullSpec;
+
+ public ProVerifSyntaxer () {
+ this.fullSpec = "";
+ }
+
+ protected static String printAlinea (int _alinea) {
+ int i;
+ String res = "";
+
+ for (i=0; i<_alinea; i++)
+ res += ProVerifSyntaxer.DEC;
+
+ return res;
+ }
+
+ public void translate (ProVerifDeclaration _node, int _alinea) {
+ if (_node != null)
+ _node.translate (this, _alinea);
+ }
+
+ protected void translateSpec (ProVerifSpec _node, int _alinea) {
+ for (ProVerifDeclaration decl: _node.declarations)
+ this.translate (decl, _alinea);
+
+ this.fullSpec += "\n\n";
+ this.fullSpec += this.printAlinea (_alinea);
+ this.fullSpec += "process";
+ this.translate (_node.mainProcess.next, _alinea+1);
+ }
+
+ protected void translateComment (ProVerifComment _node, int _alinea) {
+ if (_node.lines.isEmpty())
+ return;
+
+ this.fullSpec += "\n\n";
+ this.fullSpec += this.printAlinea (_alinea);
+ this.fullSpec += "(* ";
+
+ boolean first = true;
+ for (String l: _node.lines) {
+ if (first)
+ first = false;
+ else {
+ this.fullSpec += "\n";
+ this.fullSpec += this.printAlinea (_alinea);
+ this.fullSpec += " * ";
+ }
+ this.fullSpec += l;
+ }
+
+ this.fullSpec += " *)";
+ }
+
+ protected void translateSecrecyAssum (ProVerifSecrecyAssum _node, int _alinea) {
+ this.fullSpec += "\n" + this.printAlinea (_alinea);
+ this.fullSpec += "not " + _node.name + ".";
+ }
+
+ protected void translateProcRaw (ProVerifProcRaw _node, int _alinea) {
+ this.fullSpec += "\n" + this.printAlinea (_alinea);
+ this.fullSpec += _node.raw;
+ if (_node.next != null) {
+ if (_node.nextOptional)
+ this.fullSpec += ";";
+ this.translate (_node.next, _alinea);
+ }
+ }
+
+ protected void translateProcITE (ProVerifProcITE _node, int _alinea) {
+ this.fullSpec += "\n" + this.printAlinea (_alinea);
+ this.fullSpec += "if " + _node.cond + " then";
+ if (_node.next != null)
+ this.translate (_node.next, _alinea+1);
+ else
+ this.fullSpec += " 0";
+ if (_node.elseInstr.next != null) {
+ this.fullSpec += "\n" + this.printAlinea (_alinea);
+ this.fullSpec += "else";
+ this.translate (_node.elseInstr.next, _alinea+1);
+ }
+ }
+
+ protected void translateProcRawGlobing (ProVerifProcRawGlobing _node, int _alinea) {
+ this.fullSpec += "\n" + this.printAlinea (_alinea);
+ this.fullSpec += _node.before;
+ if (_node.intraInstr.next != null)
+ this.translate (_node.intraInstr.next, _alinea+1);
+ else
+ this.fullSpec += " 0 ";
+ this.fullSpec += _node.after;
+
+ if (_node.next != null) {
+ this.fullSpec += ";";
+ this.translate (_node.next, _alinea+1);
+ }
+ }
+
+ protected void translateProcParallel (ProVerifProcParallel _node, int _alinea) {
+ if (_node.instrs.size () == 1)
+ this.translate (_node.instrs.get (0), _alinea);
+ else if (_node.instrs.size () > 1) {
+ this.fullSpec += "\n" + this.printAlinea (_alinea);
+ this.fullSpec += "((";
+ boolean first = true;
+ for (ProVerifProcInstr instr: _node.instrs) {
+ if (first)
+ first = false;
+ else {
+ this.fullSpec += "\n" + this.printAlinea (_alinea);
+ this.fullSpec += ") | (";
+ }
+
+ this.translate (instr, _alinea+1);
+ }
+ this.fullSpec += "\n" + this.printAlinea (_alinea);
+ this.fullSpec += "))";
+ }
+
+ if (_node.next != null) {
+ this.fullSpec += ";";
+ this.translate (_node.next, _alinea);
+ }
+ }
+
+ protected abstract void translateConst (ProVerifConst _node, int _alinea);
+ protected abstract void translateFunc (ProVerifFunc _node, int _alinea);
+ protected abstract void translateReduc (ProVerifReduc _node, int _alinea);
+ protected abstract void translateVar (ProVerifVar _node, int _alinea);
+ protected abstract void translateQueryAtt (ProVerifQueryAtt _node, int _alinea);
+ protected abstract void translateQueryEv (ProVerifQueryEv _node, int _alinea);
+ protected abstract void translateQueryEvinj (ProVerifQueryEvinj _node, int _alinea);
+ protected abstract void translateEvDecl (ProVerifEvDecl _node, int _alinea);
+ protected abstract void translateProcess (ProVerifProcess _node, int _alinea);
+ protected abstract void translateProcNew (ProVerifProcNew _node, int _alinea);
+ protected abstract void translateProcIn (ProVerifProcIn _node, int _alinea);
+ protected abstract void translateProcLet (ProVerifProcLet _node, int _alinea);
+ protected abstract void translateProcCall (ProVerifProcCall _node, int _alinea);
+
+ private void makeSpec (ProVerifSpec _spec) {
+ this.translate (_spec, 0);
+ }
+
+ public String getStringSpec (ProVerifSpec _spec) {
+ if (_spec.modified) {
+ this.makeSpec (_spec);
+ _spec.modified = false;
+ }
+
+ return this.fullSpec;
+ }
+}
diff --git a/src/proverifspec/ProVerifVar.java b/src/proverifspec/ProVerifVar.java
new file mode 100644
index 0000000000000000000000000000000000000000..7d6e424cdd7c032834bed84a1d911cb1b9d9eb71
--- /dev/null
+++ b/src/proverifspec/ProVerifVar.java
@@ -0,0 +1,70 @@
+/**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 ProVerifVar
+ * Creation: 13/09/2015
+ * @version 1.0 13/09/2015
+ * @author Florian LUGOU
+ * @see
+ */
+
+package proverifspec;
+
+public class ProVerifVar implements ProVerifDeclaration {
+ protected String name;
+ protected String type;
+ protected boolean priv;
+
+ public ProVerifVar (String _name, String _type) {
+ this.name = _name;
+ this.type = _type;
+ }
+
+ public ProVerifVar (String _name, String _type, boolean _priv) {
+ this (_name, _type);
+ this.priv = _priv;
+ }
+
+ public void translate (ProVerifSyntaxer _syntaxer, int _alinea) {
+ _syntaxer.translateVar (this, _alinea);
+ }
+
+ public String getName () {
+ return this.name;
+ }
+}
diff --git a/src/ui/AttackTreePanelTranslator.java b/src/ui/AttackTreePanelTranslator.java
index 69096826b54edbbd0e28d29122cde99b2dd7a3ea..5f7892f9fbae330ef0d0a30b4eb9c1f0638875f4 100644
--- a/src/ui/AttackTreePanelTranslator.java
+++ b/src/ui/AttackTreePanelTranslator.java
@@ -403,32 +403,32 @@ public class AttackTreePanelTranslator {
asm.addElement(getStop);
- AvatarTransition at = new AvatarTransition("at1", _ref);
+ AvatarTransition at = new AvatarTransition(_ab, "at1", _ref);
asm.addElement(at);
start.addNext(at);
at.addNext(mainState);
- at = new AvatarTransition("at2", _ref);
+ at = new AvatarTransition(_ab, "at2", _ref);
asm.addElement(at);
mainState.addNext(at);
at.addNext(getMake);
- at = new AvatarTransition("at3", _ref);
+ at = new AvatarTransition(_ab, "at3", _ref);
asm.addElement(at);
getMake.addNext(at);
at.addNext(performedState);
- at = new AvatarTransition("backToMain", _ref);
+ at = new AvatarTransition(_ab, "backToMain", _ref);
asm.addElement(at);
performedState.addNext(at);
at.addNext(mainState);
- at = new AvatarTransition("at4", _ref);
+ at = new AvatarTransition(_ab, "at4", _ref);
asm.addElement(at);
mainState.addNext(at);
at.addNext(getStop);
- at = new AvatarTransition("at5", _ref);
+ at = new AvatarTransition(_ab, "at5", _ref);
asm.addElement(at);
getStop.addNext(at);
at.addNext(mainStop);
@@ -446,17 +446,17 @@ public class AttackTreePanelTranslator {
asm.addElement(getStop);
- AvatarTransition at = new AvatarTransition("at1", _ref);
+ AvatarTransition at = new AvatarTransition(_ab, "at1", _ref);
asm.addElement(at);
start.addNext(at);
at.addNext(mainState);
- at = new AvatarTransition("at4", _ref);
+ at = new AvatarTransition(_ab, "at4", _ref);
asm.addElement(at);
mainState.addNext(at);
at.addNext(getStop);
- at = new AvatarTransition("at5", _ref);
+ at = new AvatarTransition(_ab, "at5", _ref);
asm.addElement(at);
getStop.addNext(at);
at.addNext(mainStop);
@@ -498,70 +498,70 @@ public class AttackTreePanelTranslator {
asm.addElement(getActivateAfterStop);
- AvatarTransition at = new AvatarTransition("at1", _ref);
+ AvatarTransition at = new AvatarTransition(_ab, "at1", _ref);
asm.addElement(at);
start.addNext(at);
at.addNext(activateState);
- at = new AvatarTransition("at1_act", _ref);
+ at = new AvatarTransition(_ab, "at1_act", _ref);
asm.addElement(at);
activateState.addNext(at);
at.addNext(getActivate);
- at = new AvatarTransition("at1_performed", _ref);
+ at = new AvatarTransition(_ab, "at1_performed", _ref);
asm.addElement(at);
getActivate.addNext(at);
at.addNext(activatedState);
- at = new AvatarTransition("at2_main", _ref);
+ at = new AvatarTransition(_ab, "at2_main", _ref);
asm.addElement(at);
activatedState.addNext(at);
at.addNext(mainState);
at.setHidden(true);
- at = new AvatarTransition("at2", _ref);
+ at = new AvatarTransition(_ab, "at2", _ref);
asm.addElement(at);
mainState.addNext(at);
at.addNext(getMake);
- at = new AvatarTransition("at3", _ref);
+ at = new AvatarTransition(_ab, "at3", _ref);
asm.addElement(at);
getMake.addNext(at);
at.addNext(performedState);
- at = new AvatarTransition("backToMain", _ref);
+ at = new AvatarTransition(_ab, "backToMain", _ref);
asm.addElement(at);
performedState.addNext(at);
at.addNext(mainState);
- at = new AvatarTransition("at4", _ref);
+ at = new AvatarTransition(_ab, "at4", _ref);
asm.addElement(at);
mainState.addNext(at);
at.addNext(getStop);
- at = new AvatarTransition("at5", _ref);
+ at = new AvatarTransition(_ab, "at5", _ref);
asm.addElement(at);
getStop.addNext(at);
at.addNext(mainStop);
// Stop before activate
- at = new AvatarTransition("at6", _ref);
+ at = new AvatarTransition(_ab, "at6", _ref);
asm.addElement(at);
activateState.addNext(at);
at.addNext(getStopInitial);
- at = new AvatarTransition("at7", _ref);
+ at = new AvatarTransition(_ab, "at7", _ref);
asm.addElement(at);
getStopInitial.addNext(at);
at.addNext(stopBeforeActivate);
- at = new AvatarTransition("at8", _ref);
+ at = new AvatarTransition(_ab, "at8", _ref);
asm.addElement(at);
stopBeforeActivate.addNext(at);
at.addNext(getActivateAfterStop);
- at = new AvatarTransition("at9", _ref);
+ at = new AvatarTransition(_ab, "at9", _ref);
asm.addElement(at);
getActivateAfterStop.addNext(at);
at.addNext(mainStop);
@@ -589,54 +589,54 @@ public class AttackTreePanelTranslator {
asm.addElement(getActivateAfterStop);
- AvatarTransition at = new AvatarTransition("at1", _ref);
+ AvatarTransition at = new AvatarTransition(_ab, "at1", _ref);
asm.addElement(at);
start.addNext(at);
at.addNext(activateState);
- at = new AvatarTransition("at1_act", _ref);
+ at = new AvatarTransition(_ab, "at1_act", _ref);
asm.addElement(at);
activateState.addNext(at);
at.addNext(getActivate);
- at = new AvatarTransition("at1_performed", _ref);
+ at = new AvatarTransition(_ab, "at1_performed", _ref);
asm.addElement(at);
getActivate.addNext(at);
at.addNext(activatedState);
- at = new AvatarTransition("at2_main", _ref);
+ at = new AvatarTransition(_ab, "at2_main", _ref);
asm.addElement(at);
activatedState.addNext(at);
at.addNext(mainState);
at.setHidden(true);
- at = new AvatarTransition("at4", _ref);
+ at = new AvatarTransition(_ab, "at4", _ref);
asm.addElement(at);
mainState.addNext(at);
at.addNext(getStop);
- at = new AvatarTransition("at5", _ref);
+ at = new AvatarTransition(_ab, "at5", _ref);
asm.addElement(at);
getStop.addNext(at);
at.addNext(mainStop);
// Stop before activate
- at = new AvatarTransition("at6", _ref);
+ at = new AvatarTransition(_ab, "at6", _ref);
asm.addElement(at);
activateState.addNext(at);
at.addNext(getStopInitial);
- at = new AvatarTransition("at7", _ref);
+ at = new AvatarTransition(_ab, "at7", _ref);
asm.addElement(at);
getStopInitial.addNext(at);
at.addNext(stopBeforeActivate);
- at = new AvatarTransition("at8", _ref);
+ at = new AvatarTransition(_ab, "at8", _ref);
asm.addElement(at);
stopBeforeActivate.addNext(at);
at.addNext(getActivateAfterStop);
- at = new AvatarTransition("at9", _ref);
+ at = new AvatarTransition(_ab, "at9", _ref);
asm.addElement(at);
getActivateAfterStop.addNext(at);
at.addNext(mainStop);
@@ -687,7 +687,7 @@ public class AttackTreePanelTranslator {
asm.addElement(mainState);
asm.addElement(endState);
asm.addElement(overallState);
- AvatarTransition atF = new AvatarTransition("at1", _ref);
+ AvatarTransition atF = new AvatarTransition(_ab, "at1", _ref);
asm.addElement(atF);
start.addNext(atF);
atF.addNext(mainState);
@@ -707,12 +707,12 @@ public class AttackTreePanelTranslator {
avatartranslator.AvatarSignal sigAtt = _main.getAvatarSignalWithName("accept__" + att.getName());
AvatarActionOnSignal acceptAttack = new AvatarActionOnSignal("AcceptAttack", sigAtt, _ref1);
asm.addElement(acceptAttack);
- AvatarTransition at = new AvatarTransition("at_toInputAttack", _ref);
+ AvatarTransition at = new AvatarTransition(_ab, "at_toInputAttack", _ref);
asm.addElement(at);
mainState.addNext(at);
at.addNext(acceptAttack);
- at.setGuard("["+att.getName() + "__performed == false]");
- at = new AvatarTransition("at_fromInputAttack", _ref);
+ at.setGuard(new AvatarGuard ("["+att.getName() + "__performed == false]"));
+ at = new AvatarTransition(_ab, "at_fromInputAttack", _ref);
at.addAction(att.getName() + "__performed = true");
asm.addElement(at);
acceptAttack.addNext(at);
@@ -721,7 +721,7 @@ public class AttackTreePanelTranslator {
}
// Adding resulting attack
- AvatarTransition at = new AvatarTransition("at_toEnd", _ref);
+ AvatarTransition at = new AvatarTransition(_ab, "at_toEnd", _ref);
asm.addElement(at);
mainState.addNext(at);
at.addNext(endState);
@@ -731,11 +731,11 @@ public class AttackTreePanelTranslator {
avatartranslator.AvatarSignal sigAttack = _main.getAvatarSignalWithName("nodeDone__" + resulting.getName());
AvatarActionOnSignal resultingAttack = new AvatarActionOnSignal("ResultingAttack", sigAttack, _ref1);
asm.addElement(resultingAttack);
- at = new AvatarTransition("at_toResultingAttack", _ref);
+ at = new AvatarTransition(_ab, "at_toResultingAttack", _ref);
asm.addElement(at);
endState.addNext(at);
at.addNext(resultingAttack);
- at = new AvatarTransition("at_Overall", _ref);
+ at = new AvatarTransition(_ab, "at_Overall", _ref);
asm.addElement(at);
resultingAttack.addNext(at);
at.addNext(overallState);
@@ -758,7 +758,7 @@ public class AttackTreePanelTranslator {
asm.addElement(endState);
asm.addElement(overallState);
- AvatarTransition atF = new AvatarTransition("at1", _ref);
+ AvatarTransition atF = new AvatarTransition(_ab, "at1", _ref);
asm.addElement(atF);
start.addNext(atF);
atF.addNext(mainState);
@@ -777,12 +777,12 @@ public class AttackTreePanelTranslator {
avatartranslator.AvatarSignal sigAtt = _main.getAvatarSignalWithName("accept__" + att.getName());
AvatarActionOnSignal acceptAttack = new AvatarActionOnSignal("AcceptAttack", sigAtt, _ref1);
asm.addElement(acceptAttack);
- AvatarTransition at = new AvatarTransition("at_toInputAttack", _ref);
+ AvatarTransition at = new AvatarTransition(_ab, "at_toInputAttack", _ref);
asm.addElement(at);
mainState.addNext(at);
at.addNext(acceptAttack);
at.setGuard("["+att.getName() + "__performed == false]");
- at = new AvatarTransition("at_fromInputAttack", _ref);
+ at = new AvatarTransition(_ab, "at_fromInputAttack", _ref);
at.addAction(att.getName() + "__performed = true");
asm.addElement(at);
acceptAttack.addNext(at);
@@ -791,12 +791,12 @@ public class AttackTreePanelTranslator {
// Link from End
acceptAttack = new AvatarActionOnSignal("AcceptAttack", sigAtt, _ref1);
asm.addElement(acceptAttack);
- at = new AvatarTransition("at_toInputAttack", _ref);
+ at = new AvatarTransition(_ab, "at_toInputAttack", _ref);
asm.addElement(at);
endState.addNext(at);
at.addNext(acceptAttack);
at.setGuard("["+att.getName() + "__performed == false]");
- at = new AvatarTransition("at_fromInputAttack", _ref);
+ at = new AvatarTransition(_ab, "at_fromInputAttack", _ref);
at.addAction(att.getName() + "__performed = true");
asm.addElement(at);
acceptAttack.addNext(at);
@@ -805,12 +805,12 @@ public class AttackTreePanelTranslator {
// Link from Overall
acceptAttack = new AvatarActionOnSignal("AcceptAttack", sigAtt, _ref1);
asm.addElement(acceptAttack);
- at = new AvatarTransition("at_toInputAttack", _ref);
+ at = new AvatarTransition(_ab, "at_toInputAttack", _ref);
asm.addElement(at);
overallState.addNext(at);
at.addNext(acceptAttack);
at.setGuard("["+att.getName() + "__performed == false]");
- at = new AvatarTransition("at_fromInputAttack", _ref);
+ at = new AvatarTransition(_ab, "at_fromInputAttack", _ref);
at.addAction(att.getName() + "__performed = true");
asm.addElement(at);
acceptAttack.addNext(at);
@@ -821,7 +821,7 @@ public class AttackTreePanelTranslator {
// Adding resulting attack
- AvatarTransition at = new AvatarTransition("at_toEnd", _ref);
+ AvatarTransition at = new AvatarTransition(_ab, "at_toEnd", _ref);
asm.addElement(at);
mainState.addNext(at);
at.addNext(endState);
@@ -831,11 +831,11 @@ public class AttackTreePanelTranslator {
avatartranslator.AvatarSignal sigAttack = _main.getAvatarSignalWithName("nodeDone__" + resulting.getName());
AvatarActionOnSignal resultingAttack = new AvatarActionOnSignal("ResultingAttack", sigAttack, _ref1);
asm.addElement(resultingAttack);
- at = new AvatarTransition("at_toResultingAttack", _ref);
+ at = new AvatarTransition(_ab, "at_toResultingAttack", _ref);
asm.addElement(at);
endState.addNext(at);
at.addNext(resultingAttack);
- at = new AvatarTransition("at_Overall", _ref);
+ at = new AvatarTransition(_ab, "at_Overall", _ref);
asm.addElement(at);
resultingAttack.addNext(at);
at.addNext(overallState);
@@ -862,7 +862,7 @@ public class AttackTreePanelTranslator {
asm.addElement(stoppingAll);
- AvatarTransition atF = new AvatarTransition("at1", _ref);
+ AvatarTransition atF = new AvatarTransition(_ab, "at1", _ref);
atF.setHidden(true);
asm.addElement(atF);
start.addNext(atF);
@@ -885,12 +885,12 @@ public class AttackTreePanelTranslator {
avatartranslator.AvatarSignal sigAtt = _main.getAvatarSignalWithName("accept__" + att.getName());
AvatarActionOnSignal acceptAttack = new AvatarActionOnSignal("AcceptAttack", sigAtt, _ref1);
asm.addElement(acceptAttack);
- AvatarTransition at = new AvatarTransition("at_toInputAttack", _ref);
+ AvatarTransition at = new AvatarTransition(_ab, "at_toInputAttack", _ref);
asm.addElement(at);
mainState.addNext(at);
at.addNext(acceptAttack);
at.setGuard("[("+att.getName() + "__performed == false) && (oneDone == false)]");
- at = new AvatarTransition("at_fromInputAttack", _ref);
+ at = new AvatarTransition(_ab, "at_fromInputAttack", _ref);
at.addAction(att.getName() + "__performed = true");
at.setHidden(true);
at.addAction("oneDone = true");
@@ -904,12 +904,12 @@ public class AttackTreePanelTranslator {
sigAtt = _main.getAvatarSignalWithName("acceptStop__" + att.getName());
acceptAttack = new AvatarActionOnSignal("StopAttack", sigAtt, _ref1);
asm.addElement(acceptAttack);
- at = new AvatarTransition("at_toInputAttack_leaf", _ref);
+ at = new AvatarTransition(_ab, "at_toInputAttack_leaf", _ref);
asm.addElement(at);
stoppingAll.addNext(at);
at.addNext(acceptAttack);
at.setGuard("["+att.getName() + "__performed == false]");
- at = new AvatarTransition("at_fromInputAttack", _ref);
+ at = new AvatarTransition(_ab, "at_fromInputAttack", _ref);
at.addAction(att.getName() + "__performed = true");
at.setHidden(true);
asm.addElement(at);
@@ -929,7 +929,7 @@ public class AttackTreePanelTranslator {
}
// Adding link to stopping all
- AvatarTransition at = new AvatarTransition("at_toStoppingAll", _ref);
+ AvatarTransition at = new AvatarTransition(_ab, "at_toStoppingAll", _ref);
asm.addElement(at);
mainState.addNext(at);
at.addNext(stoppingAll);
@@ -937,7 +937,7 @@ public class AttackTreePanelTranslator {
// Adding resulting attack
- at = new AvatarTransition("at_toEnd", _ref);
+ at = new AvatarTransition(_ab, "at_toEnd", _ref);
asm.addElement(at);
stoppingAll.addNext(at);
at.addNext(endState);
@@ -947,11 +947,11 @@ public class AttackTreePanelTranslator {
avatartranslator.AvatarSignal sigAttack = _main.getAvatarSignalWithName("nodeDone__" + resulting.getName());
AvatarActionOnSignal resultingAttack = new AvatarActionOnSignal("ResultingAttack", sigAttack, _ref1);
asm.addElement(resultingAttack);
- at = new AvatarTransition("at_toResultingAttack", _ref);
+ at = new AvatarTransition(_ab, "at_toResultingAttack", _ref);
asm.addElement(at);
endState.addNext(at);
at.addNext(resultingAttack);
- at = new AvatarTransition("at_Overall", _ref);
+ at = new AvatarTransition(_ab, "at_Overall", _ref);
asm.addElement(at);
resultingAttack.addNext(at);
at.addNext(overallState);
@@ -978,7 +978,7 @@ public class AttackTreePanelTranslator {
asm.addElement(overallState);
- AvatarTransition at = new AvatarTransition("at", _ref);
+ AvatarTransition at = new AvatarTransition(_ab, "at", _ref);
asm.addElement(at);
start.addNext(at);
at.addNext(mainState);
@@ -993,18 +993,18 @@ public class AttackTreePanelTranslator {
AvatarActionOnSignal acceptAttack = new AvatarActionOnSignal("AcceptAttack", sigAtt, _ref1);
asm.addElement(acceptAttack);
- at = new AvatarTransition("at", _ref);
+ at = new AvatarTransition(_ab, "at", _ref);
asm.addElement(at);
previousState.addNext(at);
at.addNext(acceptAttack);
- at = new AvatarTransition("at", _ref);
+ at = new AvatarTransition(_ab, "at", _ref);
asm.addElement(at);
acceptAttack.addNext(at);
at.addNext(state);
previousState = state;
}
- at = new AvatarTransition("at", _ref);
+ at = new AvatarTransition(_ab, "at", _ref);
asm.addElement(at);
previousState.addNext(at);
at.addNext(endState);
@@ -1015,11 +1015,11 @@ public class AttackTreePanelTranslator {
avatartranslator.AvatarSignal sigAttack = _main.getAvatarSignalWithName("nodeDone__" + resulting.getName());
AvatarActionOnSignal resultingAttack = new AvatarActionOnSignal("ResultingAttack", sigAttack, _ref1);
asm.addElement(resultingAttack);
- at = new AvatarTransition("at_toResultingAttack", _ref);
+ at = new AvatarTransition(_ab, "at_toResultingAttack", _ref);
asm.addElement(at);
endState.addNext(at);
at.addNext(resultingAttack);
- at = new AvatarTransition("at_Overall", _ref);
+ at = new AvatarTransition(_ab, "at_Overall", _ref);
asm.addElement(at);
resultingAttack.addNext(at);
at.addNext(overallState);
@@ -1043,7 +1043,7 @@ public class AttackTreePanelTranslator {
asm.addElement(overallState);
- AvatarTransition at = new AvatarTransition("at", _ref);
+ AvatarTransition at = new AvatarTransition(_ab, "at", _ref);
asm.addElement(at);
start.addNext(at);
at.addNext(mainState);
@@ -1059,14 +1059,14 @@ public class AttackTreePanelTranslator {
AvatarActionOnSignal acceptAttack = new AvatarActionOnSignal("AcceptAttack", sigAtt, _ref1);
asm.addElement(acceptAttack);
- at = new AvatarTransition("at", _ref);
+ at = new AvatarTransition(_ab, "at", _ref);
asm.addElement(at);
previousState.addNext(at);
at.addNext(acceptAttack);
if (cpt > 0) {
at.setDelays("" + _node.getTime(), "" + _node.getTime());
}
- at = new AvatarTransition("at", _ref);
+ at = new AvatarTransition(_ab, "at", _ref);
asm.addElement(at);
acceptAttack.addNext(at);
at.addNext(state);
@@ -1074,7 +1074,7 @@ public class AttackTreePanelTranslator {
cpt ++;
}
- at = new AvatarTransition("at", _ref);
+ at = new AvatarTransition(_ab, "at", _ref);
asm.addElement(at);
previousState.addNext(at);
at.addNext(endState);
@@ -1085,11 +1085,11 @@ public class AttackTreePanelTranslator {
avatartranslator.AvatarSignal sigAttack = _main.getAvatarSignalWithName("nodeDone__" + resulting.getName());
AvatarActionOnSignal resultingAttack = new AvatarActionOnSignal("ResultingAttack", sigAttack, _ref1);
asm.addElement(resultingAttack);
- at = new AvatarTransition("at_toResultingAttack", _ref);
+ at = new AvatarTransition(_ab, "at_toResultingAttack", _ref);
asm.addElement(at);
endState.addNext(at);
at.addNext(resultingAttack);
- at = new AvatarTransition("at_Overall", _ref);
+ at = new AvatarTransition(_ab, "at_Overall", _ref);
asm.addElement(at);
resultingAttack.addNext(at);
at.addNext(overallState);
@@ -1115,7 +1115,7 @@ public class AttackTreePanelTranslator {
asm.addElement(timeout);
- AvatarTransition at = new AvatarTransition("at", _ref);
+ AvatarTransition at = new AvatarTransition(_ab, "at", _ref);
asm.addElement(at);
start.addNext(at);
at.addNext(mainState);
@@ -1131,18 +1131,18 @@ public class AttackTreePanelTranslator {
AvatarActionOnSignal acceptAttack = new AvatarActionOnSignal("AcceptAttack", sigAtt, _ref1);
asm.addElement(acceptAttack);
- at = new AvatarTransition("at", _ref);
+ at = new AvatarTransition(_ab, "at", _ref);
asm.addElement(at);
previousState.addNext(at);
at.addNext(acceptAttack);
if (cpt > 0) {
- at = new AvatarTransition("at_totimeout", _ref);
+ at = new AvatarTransition(_ab, "at_totimeout", _ref);
asm.addElement(at);
previousState.addNext(at);
at.addNext(timeout);
at.setDelays("" + _node.getTime(), "" + _node.getTime());
}
- at = new AvatarTransition("at", _ref);
+ at = new AvatarTransition(_ab, "at", _ref);
asm.addElement(at);
acceptAttack.addNext(at);
at.addNext(state);
@@ -1150,7 +1150,7 @@ public class AttackTreePanelTranslator {
cpt ++;
}
- at = new AvatarTransition("at", _ref);
+ at = new AvatarTransition(_ab, "at", _ref);
asm.addElement(at);
previousState.addNext(at);
at.addNext(endState);
@@ -1161,11 +1161,11 @@ public class AttackTreePanelTranslator {
avatartranslator.AvatarSignal sigAttack = _main.getAvatarSignalWithName("nodeDone__" + resulting.getName());
AvatarActionOnSignal resultingAttack = new AvatarActionOnSignal("ResultingAttack", sigAttack, _ref1);
asm.addElement(resultingAttack);
- at = new AvatarTransition("at_toResultingAttack", _ref);
+ at = new AvatarTransition(_ab, "at_toResultingAttack", _ref);
asm.addElement(at);
endState.addNext(at);
at.addNext(resultingAttack);
- at = new AvatarTransition("at_Overall", _ref);
+ at = new AvatarTransition(_ab, "at_Overall", _ref);
asm.addElement(at);
resultingAttack.addNext(at);
at.addNext(overallState);
diff --git a/src/ui/AvatarDesignPanelTranslator.java b/src/ui/AvatarDesignPanelTranslator.java
index 42704bdabfb4209ec46b21fc044292ee7d2401a9..f6281218cb7acc8f9eac3b41e1b17c993fe214c7 100644
--- a/src/ui/AvatarDesignPanelTranslator.java
+++ b/src/ui/AvatarDesignPanelTranslator.java
@@ -1152,19 +1152,20 @@ public class AvatarDesignPanelTranslator {
element1 = (AvatarStateMachineElement)(listE.getObject(tgc1));
element2 = (AvatarStateMachineElement)(listE.getObject(tgc2));
if ((element1 != null) && (element2 != null)) {
- at = new AvatarTransition("avatar transition", tgc);
+ at = new AvatarTransition(_ab, "avatar transition", tgc);
// Guard
tmp = modifyString(asmdco.getGuard());
- if (AvatarSpecification.isElseGuard(tmp)) {
- at.setGuard(tmp);
+ AvatarGuard guard = new AvatarGuard (tmp);
+ if (guard.isElseGuard()) {
+ at.setGuard(guard);
} else {
error = AvatarSyntaxChecker.isAValidGuard(_as, _ab, tmp);
if (error < 0) {
makeError(error, tdp, _ab, tgc, "transition guard", tmp);
} else {
- at.setGuard(tmp);
+ at.setGuard(guard);
}
}
@@ -1262,7 +1263,7 @@ public class AvatarDesignPanelTranslator {
}
}
- asm.handleUnfollowedStartState();
+ asm.handleUnfollowedStartState(_ab);
// Investigate all states -> put warnings for all empty transitions from a state to the same one (infinite loop)
int nb;
diff --git a/src/ui/GTURTLEModeling.java b/src/ui/GTURTLEModeling.java
index e7c952f1639432163760a8c9f6fa3291dba1c618..de85d4ed76401978fd888700760daaf435f09963 100755
--- a/src/ui/GTURTLEModeling.java
+++ b/src/ui/GTURTLEModeling.java
@@ -624,11 +624,11 @@ public class GTURTLEModeling {
return avatarspec;
}
- public boolean generateProVerifFromAVATAR(String _path, boolean _stateReachability, boolean _advancedTranslation) {
+ public boolean generateProVerifFromAVATAR(String _path, boolean _stateReachability, boolean _advancedTranslation, boolean _typed) {
avatar2proverif = new AVATAR2ProVerif(avatarspec);
//tml2uppaal.setChoiceDeterministic(choices);
//tml2uppaal.setSizeInfiniteFIFO(_size);
- proverif = avatar2proverif.generateProVerif(true, true, _stateReachability, _advancedTranslation);
+ proverif = avatar2proverif.generateProVerif(true, true, _stateReachability, _advancedTranslation, _typed);
warnings = avatar2proverif.getWarnings();
languageID = PROVERIF;
mgui.setMode(MainGUI.EDIT_PROVERIF_OK);
diff --git a/src/ui/window/JDialogProVerifGeneration.java b/src/ui/window/JDialogProVerifGeneration.java
index 7af509132b27c12a5b98e2af64606007adffed2c..70ffff23922e4a3f04c64280038aa5f4a0c7a755 100644
--- a/src/ui/window/JDialogProVerifGeneration.java
+++ b/src/ui/window/JDialogProVerifGeneration.java
@@ -91,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 stateReachability, translationOfBooleanFunction, outputOfProVerif;
+ protected JCheckBox stateReachability, translationOfBooleanFunction, outputOfProVerif, typedLanguage;
protected JComboBox versionSimulator;
private Thread t;
@@ -180,6 +180,10 @@ public class JDialogProVerifGeneration extends javax.swing.JDialog implements Ac
translationOfBooleanFunction.setSelected(true);
jp01.add(translationOfBooleanFunction, c01);
+ typedLanguage = new JCheckBox("Generate typed Pi calculus");
+ typedLanguage.setSelected(true);
+ jp01.add(typedLanguage, c01);
+
/*optimizemode = new JCheckBox("Optimize code");
optimizemode.setSelected(optimizeModeSelected);
@@ -326,7 +330,7 @@ public class JDialogProVerifGeneration extends javax.swing.JDialog implements Ac
testGo();
- if (mgui.gtm.generateProVerifFromAVATAR(pathCode, stateReachability.isSelected(), translationOfBooleanFunction.isSelected())) {
+ if (mgui.gtm.generateProVerifFromAVATAR(pathCode, stateReachability.isSelected(), translationOfBooleanFunction.isSelected(), typedLanguage.isSelected())) {
jta.append("ProVerif code generation done\n");
} else {
jta.append("Could not generate proverif code\n");