diff --git a/Makefile b/Makefile
index cf32a59b3db19f5d663a5af98e70932d052b3a6b..e0367ff595bde24c8affe3f8dd8131273146a49a 100755
--- a/Makefile
+++ b/Makefile
@@ -14,7 +14,7 @@ GZIP = gzip -9 -f
DEBUG = -g
CLASSPATH = -classpath
CLASSPATH = -sourcepath
-PACKAGE = avatartranslator avatartranslator/toexecutable avatartranslator/directsimulation avatartranslator/tocppsim avatartranslator/touppaal avatartranslator/toturtle avatartranslator/toproverif automata compiler/tmlparser vcd nc ddtranslator launcher myutil tpndescription sddescription sdtranslator tepe translator tmltranslator tmltranslator/toautomata tmltranslator/tosystemc tmltranslator/tomappingsystemc tmltranslator/tomappingsystemc2 tmltranslator/touppaal tmltranslator/toturtle translator/tojava translator/tosimujava translator/totpn translator/touppaal ui ui/avatarbd 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
+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/toautomata tmltranslator/tosystemc tmltranslator/tomappingsystemc tmltranslator/tomappingsystemc2 tmltranslator/touppaal tmltranslator/toturtle translator/tojava translator/tosimujava translator/totpn translator/touppaal ui ui/avatarbd 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
BUILDER = builder.jar
BUILD_INFO = build.txt
BUILD_TO_MODIFY = src/ui/DefaultText.java
@@ -100,7 +100,7 @@ basic:
ttooljar_std:
rm -f $(TTOOL_BIN)/$(TTOOL_BINARY)
cp $(TTOOL_SRC)/ui/images/$(STD_LOGO) $(TTOOL_SRC)/ui/images/$(LOGO)
- cd $(TTOOL_SRC); $(JAR) cmf $(TTOOL_JAR_TXT) $(TTOOL_BIN)/$(TTOOL_BINARY) Main.class vcd/*.class avatartranslator/*.class avatartranslator/toexecutable/*.class avatartranslator/directsimulation/*.class avatartranslator/touppaal/*.class avatartranslator/toproverif/*.class avatartranslator/*.class avatartranslator/toturtle/*.java automata/*.class compiler/tmlparser/*.class nc/*.class tepe/*.class tmltranslator/*.class tmltranslator/toautomata/*.class tmatrix/*.class tmltranslator/toturtle/*.class tmltranslator/touppaal/*.class tmltranslator/tosystemc/*.class tmltranslator/tomappingsystemc/*.class tmltranslator/tomappingsystemc2/*.class tpndescription/*.class ddtranslator/*.class launcher/*.class myutil/*.class sddescription/*.class sdtranslator/*.class translator/*.class translator/tojava/*.class translator/tosimujava/*.class translator/touppaal/*.class translator/totpn/*.class req/ebrdd/*.java ui/*.class ui/*/*.class ui/*/*/*.class proverifspec/*.class uppaaldesc/*.class ui/images/*.* ui/images/toolbarButtonGraphics/general/*.gif ui/images/toolbarButtonGraphics/media/*.gif $(TTOOL_BIN)/$(LAUNCHER_BINARY) RTLLauncher.class launcher/*.class fr/inria/oasis/vercors/cttool/model/*.class remotesimulation/*.class
+ cd $(TTOOL_SRC); $(JAR) cmf $(TTOOL_JAR_TXT) $(TTOOL_BIN)/$(TTOOL_BINARY) Main.class vcd/*.class avatartranslator/*.class avatartranslator/toexecutable/*.class avatartranslator/directsimulation/*.class avatartranslator/touppaal/*.class avatartranslator/toproverif/*.class avatartranslator/totpn/* avatartranslator/*.class avatartranslator/toturtle/*.java automata/*.class compiler/tmlparser/*.class nc/*.class tepe/*.class tmltranslator/*.class tmltranslator/toautomata/*.class tmatrix/*.class tmltranslator/toturtle/*.class tmltranslator/touppaal/*.class tmltranslator/tosystemc/*.class tmltranslator/tomappingsystemc/*.class tmltranslator/tomappingsystemc2/*.class tpndescription/*.class ddtranslator/*.class launcher/*.class myutil/*.class sddescription/*.class sdtranslator/*.class translator/*.class translator/tojava/*.class translator/tosimujava/*.class translator/touppaal/*.class translator/totpn/*.class req/ebrdd/*.java ui/*.class ui/*/*.class ui/*/*/*.class proverifspec/*.class uppaaldesc/*.class ui/images/*.* ui/images/toolbarButtonGraphics/general/*.gif ui/images/toolbarButtonGraphics/media/*.gif $(TTOOL_BIN)/$(LAUNCHER_BINARY) RTLLauncher.class launcher/*.class fr/inria/oasis/vercors/cttool/model/*.class remotesimulation/*.class
launcher:
diff --git a/src/Main.java b/src/Main.java
index 1c28f79e75e714fb1cdaadc903dea1e3c5a5d274..5d8404c1be14063af49ca9f1c5fe019c4fb9edef 100755
--- a/src/Main.java
+++ b/src/Main.java
@@ -329,14 +329,27 @@ public class Main implements ActionListener {
public static void testMatrix() {
- String[] names = {"a", "b", "e", "ae4", "be"};
+
+ //int[] numbers = {42, 18, 12,-12};
+ //System.out.println("GCD=" + MyMath.gcd(numbers));
+
+
+ /*String[] names = {"a", "b", "e", "ae4"};
int [] line0 ={-1, 1, 0, 0};
int [] line1 ={0, 0,-1, 1};
int [] line2 ={-4, 4, -1, 1};
int [] line3 ={1, -1, 0, 0};
int [] line4 ={0, 0, 1, -1};
+ int [] line4_fake ={10, 10, 11, -11};
+
- Matrice myMat = new Matrice(5, 4);
+ int [] line0b ={-1, 1, 1, -1};
+ int [] line1b ={1, -1,-1, 1};
+ int [] line2b ={0, 0, 1, 0};
+ int [] line3b ={1, 0, 0, -1};
+ int [] line4b ={-1, 0, 0, 1};
+
+ IntMatrix myMat = new IntMatrix(4, 4);
myMat.setNamesOfLine(names);
@@ -344,13 +357,33 @@ public class Main implements ActionListener {
myMat.setLineValues(1, line1);
myMat.setLineValues(2, line2);
myMat.setLineValues(3, line3);
- myMat.setLineValues(4, line4);
+ System.out.println("mat=\n" + myMat.toString() + "\n\n");
+
+ myMat.addLine(line4_fake, "duplicate-be");
+ myMat.addLine(line4, "be");
System.out.println("mat=\n" + myMat.toString() + "\n\n");
- myMat.swapLines(0, 1);
+
+ myMat.removeLine(4);
+
+
+ System.out.println("mat=\n" + myMat.toString() + "\n\n");
+ myMat.Farkas();
System.out.println("mat=\n" + myMat.toString() + "\n\n");
+ myMat = new IntMatrix(5, 4);
+
+
+ myMat.setLineValues(0, line0b);
+ myMat.setLineValues(1, line1b);
+ myMat.setLineValues(2, line2b);
+ myMat.setLineValues(3, line3b);
+ myMat.setLineValues(4, line4b);
+ System.out.println("matb=\n" + myMat.toString() + "\n\n");
+ myMat.Farkas();
+ System.out.println("matb=\n" + myMat.toString() + "\n\n");*/
+
}
} // Class Main
diff --git a/src/avatartranslator/directsimulation/AvatarSpecificationSimulation.java b/src/avatartranslator/directsimulation/AvatarSpecificationSimulation.java
index f54b53932eedaec46fa566e5ecd12a62ad5abbc1..14276a3cd895618d9c14717a08523235bb8146d8 100644
--- a/src/avatartranslator/directsimulation/AvatarSpecificationSimulation.java
+++ b/src/avatartranslator/directsimulation/AvatarSpecificationSimulation.java
@@ -55,9 +55,9 @@ import myutil.*;
public class AvatarSpecificationSimulation {
- private static int MAX_TRANSACTION_IN_A_ROW = 1000;
+ public static int MAX_TRANSACTION_IN_A_ROW = 1000;
- public static int MAX_TRANSACTIONS = 100000000;
+ public static int MAX_TRANSACTIONS = 100000;
public final static int INITIALIZE = 0;
public final static int RESET = 1;
diff --git a/src/avatartranslator/toproverif/AVATAR2ProVerif.java b/src/avatartranslator/toproverif/AVATAR2ProVerif.java
index 6e220e9bb68962e169966b45287bf7e8610adc39..2d01dc289fc38d92c27fbe8660d1d3a02aeab0bf 100755
--- a/src/avatartranslator/toproverif/AVATAR2ProVerif.java
+++ b/src/avatartranslator/toproverif/AVATAR2ProVerif.java
@@ -62,7 +62,7 @@ public class AVATAR2ProVerif {
private final static String BOOLEAN_DATA_HEADER = "(* Boolean return types *)\ndata true/0.\ndata false/0.\n";
private final static String FUNC_DATA_HEADER = "(* Functions data *)\ndata " + UNKNOWN + "/0.\n";
- private final static String PK_HEADER = "(* Public key cryptography *)\nfun pk/1.\nfun aencryptPK/2.\nreduc adecryptPK(aencryptPK(x,pk(y)),y) = x.\n";
+ 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";
diff --git a/src/avatartranslator/totpn/AVATAR2TPN.java b/src/avatartranslator/totpn/AVATAR2TPN.java
new file mode 100755
index 0000000000000000000000000000000000000000..c3e33f9ae66cd8348da45ad11c448b56d01cfeea
--- /dev/null
+++ b/src/avatartranslator/totpn/AVATAR2TPN.java
@@ -0,0 +1,258 @@
+/**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 AVATAR2TPN
+* Creation: 08/02/2012
+* @version 1.1 08/02/2012
+* @author Ludovic APVRILLE
+* @see
+*/
+
+package avatartranslator.totpn;
+
+import java.awt.*;
+import java.util.*;
+
+import tpndescription.*;
+import myutil.*;
+import avatartranslator.*;
+
+public class AVATAR2TPN {
+
+ private static int GENERAL_ID = 0;
+
+
+
+ private TPN tpn;
+ private AvatarSpecification avspec;
+
+ private Hashtable<AvatarStateMachineElement, Place> entryPlaces;
+ private Hashtable<AvatarStateMachineElement, Place> exitPlaces;
+ private LinkedList<AvatarActionOnSignal> sendActions;
+ private LinkedList<AvatarActionOnSignal> receiveActions;
+
+
+ private Vector warnings;
+
+
+
+ public AVATAR2TPN(AvatarSpecification _avspec) {
+ avspec = _avspec;
+ }
+
+
+
+ public Vector getWarnings() {
+ return warnings;
+ }
+
+
+
+ public TPN generateTPN(boolean _debug, boolean _optimize) {
+ GENERAL_ID = 0;
+
+ entryPlaces = new Hashtable<AvatarStateMachineElement, Place>();
+ exitPlaces = new Hashtable<AvatarStateMachineElement, Place>();
+
+ sendActions = new LinkedList<AvatarActionOnSignal>();
+ receiveActions = new LinkedList<AvatarActionOnSignal>();
+
+ warnings = new Vector();
+ tpn = new TPN();
+
+ avspec.removeCompositeStates();
+ avspec.removeTimers();
+
+ makeBlocks();
+
+ TraceManager.addDev("-> tpn:" + tpn.toString());
+
+
+ /*if (_optimize) {
+ spec.optimize();
+ }*/
+
+
+ return tpn;
+ }
+
+ public void makeBlocks() {
+ LinkedList<AvatarBlock> blocks = avspec.getListOfBlocks();
+ for(AvatarBlock block: blocks) {
+ makeBlock(block);
+ }
+ }
+
+ public void makeBlock(AvatarBlock ab) {
+ AvatarStateMachine asm = ab.getStateMachine();
+ AvatarStartState ass = asm.getStartState();
+
+ makeBlockTPN(ab, asm, ass,null);
+
+ interconnectSynchro();
+ }
+
+ public void makeBlockTPN(AvatarBlock _block, AvatarStateMachine _asm, AvatarStateMachineElement _asme, AvatarStateMachineElement _previous) {
+
+ Place p0, p1, pentry=null, pexit=null;
+ Transition t0;
+ AvatarActionOnSignal aaos;
+
+ p0 = entryPlaces.get(_asme);
+ if (_previous== null) {
+ p1 = null;
+ } else {
+ p1 = exitPlaces.get(_previous);
+ }
+
+ boolean link=false;
+
+ // Element already taken into account?
+ if (p0 != null) {
+ // Link the exit place of the previous element to the one of the current element
+ if (p1 != null){
+ t0 = new Transition(getTPNName(_block, _previous) + " to " + getTPNName(_block, _asme));
+ t0.addDestinationPlace(p0);
+ t0.addOriginPlace(p1);
+ tpn.addTransition(t0);
+ }
+ return;
+ }
+
+ // New element!
+
+ //Start state
+ if ((_asme instanceof AvatarStartState)|| (_asme instanceof AvatarStopState) || (_asme instanceof AvatarState)) {
+ pentry = new Place(getTPNName(_block, _asme));
+ pexit = pentry;
+ entryPlaces.put(_asme, pentry);
+ exitPlaces.put(_asme, pexit);
+ TraceManager.addDev("Adding place : " + pentry);
+ tpn.addPlace(pentry);
+ link = true;
+
+ } else if ((_asme instanceof AvatarTransition) || (_asme instanceof AvatarRandom)) {
+ if (p1 != null){
+ entryPlaces.put(_asme, p1);
+ exitPlaces.put(_asme, p1);
+ } else {
+ TraceManager.addDev("Previous element without pexit!!");
+ }
+
+ } else if (_asme instanceof AvatarActionOnSignal){
+ aaos = (AvatarActionOnSignal)_asme;
+
+ if (aaos.getSignal().isOut()) {
+ sendActions.add(aaos);
+ } else {
+ receiveActions.add(aaos);
+ }
+
+ pentry = p1;
+ pexit = new Place("synchroDone__" + getTPNName(_block, _asme));
+ entryPlaces.put(_asme, pentry);
+ exitPlaces.put(_asme, pexit);
+
+ tpn.addPlace(pexit);
+ TraceManager.addDev("Adding place : " + pentry);
+
+ } else {
+ TraceManager.addDev("UNMANAGED ELEMENTS: " +_asme);
+ }
+
+
+ // Must link the new element to the previous one
+ if ((p1 != null) && (link)){
+ t0 = new Transition(getTPNName(_block, _previous) + " to " + getTPNName(_block, _asme));
+ t0.addDestinationPlace(pentry);
+ t0.addOriginPlace(p1);
+ tpn.addTransition(t0);
+ }
+
+ // Work with next elements
+ for(int i=0; i<_asme.nbOfNexts(); i++) {
+ makeBlockTPN(_block, _asm, _asme.getNext(i), _asme);
+ }
+
+
+
+ }
+
+ public void interconnectSynchro() {
+ int index;
+ AvatarSignal sig;
+ Transition t0;
+
+ TraceManager.addDev("Interconnecting synchro");
+
+ // Interconnect sender and receivers together!
+ for(AvatarActionOnSignal destination: receiveActions) {
+ // Find the related relation
+ for(AvatarRelation ar: avspec.getRelations()) {
+ if (ar.containsSignal(destination.getSignal()) && !ar.isAsynchronous()) {
+ index = ar.getIndexOfSignal(destination.getSignal());
+ sig = ar.getOutSignal(index);
+ for(AvatarActionOnSignal origin:sendActions) {
+ if (origin.getSignal() == sig) {
+ // combination found!
+ TraceManager.addDev("Combination found");
+ t0 = new Transition("Synchro from " + getShortTPNName(origin) + " to " + getShortTPNName(destination));
+ t0.addOriginPlace(entryPlaces.get(origin));
+ t0.addDestinationPlace(exitPlaces.get(origin));
+ t0.addOriginPlace(entryPlaces.get(destination));
+ t0.addDestinationPlace(exitPlaces.get(destination));
+ tpn.addTransition(t0);
+ }
+ }
+ }
+ }
+ }
+
+ }
+
+ public String getTPNName(AvatarBlock _block, AvatarStateMachineElement _asme) {
+ return _block.getName() + "__" + _asme.getName() + "__" + _asme.getID();
+ }
+
+ public String getShortTPNName(AvatarStateMachineElement _asme) {
+ return _asme.getName() + "__" + _asme.getID();
+ }
+
+
+
+}
\ No newline at end of file
diff --git a/src/myutil/IntMatrix.java b/src/myutil/IntMatrix.java
new file mode 100755
index 0000000000000000000000000000000000000000..30694700fa3f269f74a5b24ef821252609e59d60
--- /dev/null
+++ b/src/myutil/IntMatrix.java
@@ -0,0 +1,343 @@
+/**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 IntMatrix
+ * Creation: 06/02/2012
+ * Version 2.0 06/02/2012
+ * @author Ludovic APVRILLE
+ * @see
+ */
+
+package myutil;
+
+import java.util.*;
+
+public class IntMatrix {
+ public int [][] matrice;
+ public int sizeRow;
+ public int sizeColumn;
+ private String []nameOfRows;
+
+ public IntMatrix(int _sizeRow, int _sizeColumn) {
+ matrice = new int[_sizeRow][_sizeColumn];
+ sizeRow= _sizeRow;
+ sizeColumn = _sizeColumn;
+ nameOfRows = new String[sizeRow];
+ for(int i=0; i<sizeRow; i++) {
+ nameOfRows[i] = "" + i;
+ }
+ }
+
+ public void setValue(int i, int j, int value) {
+ matrice[i][j] = value;
+ }
+
+ public void setLineValues(int line, int[] values) {
+ for(int j=0; j<sizeColumn; j++) {
+ matrice[line][j] = values[j];
+ }
+ }
+
+ public int getValue(int i, int j) {
+ try {
+ return matrice[i][j];
+ } catch (Exception e) {}
+ return -1;
+ }
+
+ public void setNameOfLine(int line, String name) {
+ try {
+ nameOfRows[line] = name;
+ } catch(Exception e) {
+ }
+ }
+
+ public void setNamesOfLine(String []names) {
+ try {
+ for(int i=0; i<sizeRow; i++){
+ nameOfRows[i] = names[i];
+ }
+ } catch(Exception e) {
+ }
+ }
+
+ public String toString() {
+ StringBuffer sb = new StringBuffer("Size:" + sizeRow + "x" + sizeColumn+ ":\n");
+ for(int i=0; i<sizeRow; i++) {
+ sb.append("Row #" + i + " / " + nameOfRows[i] + ": ");
+ for(int j=0; j<sizeColumn; j++) {
+ sb.append(" " + matrice[i][j]);
+ }
+ sb.append("\n");
+ }
+ return sb.toString();
+ }
+
+ public void swapLines(int line0, int line1) {
+ int tmp;
+ for(int j=0; j<sizeColumn; j++){
+ tmp = matrice[line0][j];
+ matrice[line0][j] = matrice[line1][j];
+ matrice[line1][j] = tmp;
+ }
+
+ String tmpName = nameOfRows[line0];
+ nameOfRows[line0] = nameOfRows[line1];
+ nameOfRows[line1] = tmpName;
+ }
+
+
+ // Apply a division on all elements of a line
+ public void unitLine(int line0, int diviser) {
+ for(int j=0; j<sizeColumn; j++){
+ matrice[line0][j] = matrice[line0][j] / diviser;
+ }
+ }
+
+ // Combine line line0 minus m times line1 ; line0 gets the result
+ public void linearCombination(int line0, int line1, int m) {
+ TraceManager.addDev("combination l0 = " + line0 + " line1 = " + line1 + " multiplier m=" + m);
+ for(int j=0; j<sizeColumn; j++){
+ matrice[line0][j] = matrice[line0][j] - (m * matrice[line1][j]);
+ }
+ }
+
+ // Returns the line number at which there is the first non nul element of column col0
+ // Returns -1 in case none is found
+ public int rgpivot(int col0, int nbOfLines) {
+ int i = col0;
+ while((i<(nbOfLines)) && (matrice[i][col0] == 0)) {
+ i++;
+ }
+ if (matrice[i][col0] == 0) {
+ return 0;
+ } else {
+ return i;
+ }
+ }
+
+ public IntMatrix clone() {
+ IntMatrix im = new IntMatrix(sizeRow, sizeColumn);
+ for(int i=0; i<sizeRow; i++) {
+ for(int j=0; j<sizeColumn; j++) {
+ im.matrice[i][j] = matrice[i][j];
+ }
+ setNameOfLine(i, nameOfRows[i]);
+ }
+
+ return im;
+ }
+
+ public void concatAfter(IntMatrix im) {
+ int tmp = sizeColumn;
+ sizeColumn += im.sizeColumn;
+ int [][] newMatrice = new int[sizeRow][sizeColumn];
+ for(int i=0; i<sizeRow; i++) {
+ for(int j=0; j<sizeColumn; j++) {
+ if (j<tmp) {
+ newMatrice[i][j] = matrice[i][j];
+ } else {
+ newMatrice[i][j] = im.matrice[i][j-tmp];
+ }
+ }
+ }
+ matrice = newMatrice;
+ }
+
+ public int[] getLine(int lineIndex) {
+ int[] line =new int[sizeColumn];
+ for(int j=0; j<sizeColumn;j++){
+ line[j] = matrice[lineIndex][j];
+ }
+ return line;
+ }
+
+ public String lineToString(int []line) {
+ String s="";
+ for(int i=0; i<line.length; i++) {
+ s += line[i] + " ";
+ }
+ return s;
+ }
+
+ public String namesOfRowToString() {
+ String s="";
+ for(int i=0; i<nameOfRows.length; i++) {
+ s += nameOfRows[i] + "\n";
+ }
+ return s;
+ }
+
+
+ // Add a line at the end of the matrix
+ public void addLine(int[] newLine, String nameOfRow) {
+ sizeRow ++;
+ int [][] newMatrice = new int[sizeRow][sizeColumn];
+ for(int j=0; j<sizeColumn; j++) {
+ for(int i=0; i<sizeRow-1; i++) {
+ newMatrice[i][j] = matrice[i][j];
+ }
+ newMatrice[sizeRow-1][j] = newLine[j];
+ }
+ matrice = newMatrice;
+
+ String []newNameOfRows = new String[sizeRow];
+ for(int k=0; k<sizeRow-1; k++) {
+ newNameOfRows[k] = nameOfRows[k];
+ }
+ if(nameOfRow == null) {
+ newNameOfRows[sizeRow-1] = "" + (sizeRow-1);
+ } else {
+ newNameOfRows[sizeRow-1] = nameOfRow;
+ }
+ nameOfRows = newNameOfRows;
+ }
+
+ public void removeLine(int lineIndex) {
+ sizeRow --;
+ int [][] newMatrice = new int[sizeRow][sizeColumn];
+ for(int i=0; i<sizeRow+1; i++) {
+ for(int j=0; j<sizeColumn; j++) {
+ if (i < lineIndex) {
+ newMatrice[i][j] = matrice[i][j];
+ } else {
+ if (i>lineIndex){
+ newMatrice[i-1][j] = matrice[i][j];
+ }
+ }
+ }
+ }
+ matrice = newMatrice;
+
+ String []newNameOfRows = new String[sizeRow];
+ int dec=0;
+ for(int k=0; k<sizeRow+1; k++) {
+ if (k != lineIndex) {
+ newNameOfRows[k-dec] = nameOfRows[k];
+ } else {
+ dec ++;
+ }
+ }
+ nameOfRows = newNameOfRows;
+ }
+
+ public void makeID() {
+ for(int i=0; i<sizeRow; i++) {
+ for(int j=0; j<sizeColumn; j++) {
+ if (i==j) {
+ matrice[i][j] = 1;
+ } else {
+ matrice[i][j] = 0;
+ }
+ }
+ }
+ }
+
+
+
+ public void Farkas() {
+ int sizeColumBeforeConcat = sizeColumn;
+ IntMatrix idMat = new IntMatrix(sizeRow, sizeRow);
+ idMat.makeID();
+ concatAfter(idMat);
+ System.out.println("matconcat=\n" + toString() + "\n\n");
+ int[] lined1, lined2, lined;
+ int gcd;
+ int l, i;
+ String s0, s1;
+ String nameOfNewLine;
+
+ for(int j=0; j<sizeColumBeforeConcat; j++) {
+ // Loop on lines to add line combinations
+ for(i=0; i<sizeRow-1; i++) {
+ lined1 = getLine(i);
+ for(int k=i+1; k<sizeRow; k++) {
+ lined2 = getLine(k);
+
+ // lines d1 and 2 have opposite signs?
+ if (((lined1[j] < 0) && (lined2[j]>0)) || ((lined1[j]>0) && (lined2[j]<0))) {
+ lined = new int[lined1.length];
+ for(l=0; l<lined.length; l++) {
+ lined[l] = Math.abs(lined2[j])*lined1[l] + Math.abs(lined1[j])*lined2[l];
+ }
+ if (Math.abs(lined2[j]) == 1) {
+ s0 = nameOfRows[i] + " + ";
+ } else {
+ s0 = "" + Math.abs(lined2[j]) + "*(" + nameOfRows[i] + ") + ";
+ }
+
+ if (Math.abs(lined2[j]) == 1) {
+ s1 = nameOfRows[k];
+ } else {
+ s1 = "" + Math.abs(lined1[j]) + "*(" + nameOfRows[k] + ")";
+ }
+
+ nameOfNewLine = s0 + s1;
+ gcd = MyMath.gcd(lined);
+ //System.out.println("gcd =" + gcd + " of line =" + lineToString(lined) + " i.e.:" + nameOfNewLine);
+
+ if (gcd != 0) {
+ for(l=0; l<lined.length; l++) {
+ lined[l] = lined[l] / gcd;
+ }
+ }
+
+ addLine(lined, nameOfNewLine);
+ //System.out.println("matafterline=\n" + toString() + "\n\n");
+ }
+ }
+ }
+
+ // Remove lines whose element #j is not 0
+ for(i=0;i<sizeRow; i++) {
+ if (matrice[i][j] != 0) {
+ removeLine(i);
+ System.out.println("matafterremove " + i + "=\n" + toString() + "\n\n");
+ i--;
+ }
+ }
+
+ System.out.println("----------------\nD"+ (j+1) +"=\n" + toString() + "\n\n");
+
+ }
+
+ }
+
+
+
+}
diff --git a/src/myutil/Matrice.java b/src/myutil/Matrice.java
deleted file mode 100755
index 34bac1fae5173898e5990b09f164e1fa1fbabaec..0000000000000000000000000000000000000000
--- a/src/myutil/Matrice.java
+++ /dev/null
@@ -1,158 +0,0 @@
-/**Copyright or (C) or Copr. GET / ENST, Telecom-Paris, Ludovic Apvrille
-
-ludovic.apvrille AT enst.fr
-
-This software is a computer program whose purpose is to allow the
-edition of TURTLE analysis, design and deployment diagrams, to
-allow the generation of RT-LOTOS or Java code from this diagram,
-and at last to allow the analysis of formal validation traces
-obtained from external tools, e.g. RTL from LAAS-CNRS and CADP
-from INRIA Rhone-Alpes.
-
-This software is governed by the CeCILL license under French law and
-abiding by the rules of distribution of free software. You can use,
-modify and/ or redistribute the software under the terms of the CeCILL
-license as circulated by CEA, CNRS and INRIA at the following URL
-"http://www.cecill.info".
-
-As a counterpart to the access to the source code and rights to copy,
-modify and redistribute granted by the license, users are provided only
-with a limited warranty and the software's author, the holder of the
-economic rights, and the successive licensors have only limited
-liability.
-
-In this respect, the user's attention is drawn to the risks associated
-with loading, using, modifying and/or developing or reproducing the
-software by the user in light of its specific status of free software,
-that may mean that it is complicated to manipulate, and that also
-therefore means that it is reserved for developers and experienced
-professionals having in-depth computer knowledge. Users are therefore
-encouraged to load and test the software's suitability as regards their
-requirements in conditions enabling the security of their systems and/or
-data to be ensured and, more generally, to use and operate it in the
-same conditions as regards security.
-
-The fact that you are presently reading this means that you have had
-knowledge of the CeCILL license and that you accept its terms.
-
-/**
- * Class Matrice
- * Creation: 06/02/2012
- * Version 2.0 06/02/2012
- * @author Ludovic APVRILLE
- * @see
- */
-
-package myutil;
-
-import java.util.*;
-
-public class Matrice {
- private int [][] matrice;
- private int sizeRow;
- private int sizeColumn;
- private String []nameOfRows;
-
- public Matrice(int _sizeRow, int _sizeColumn) {
- matrice = new int[_sizeRow][_sizeColumn];
- sizeRow= _sizeRow;
- sizeColumn = _sizeColumn;
- nameOfRows = new String[sizeRow];
- for(int i=0; i<sizeRow; i++) {
- nameOfRows[i] = "" + i;
- }
- }
-
- public void setValue(int i, int j, int value) {
- matrice[i][j] = value;
- }
-
- public void setLineValues(int line, int[] values) {
- for(int j=0; j<sizeColumn; j++) {
- matrice[line][j] = values[j];
- }
- }
-
- public int getValue(int i, int j) {
- try {
- return matrice[i][j];
- } catch (Exception e) {}
- return -1;
- }
-
- public void setNameOfLine(int line, String name) {
- try {
- nameOfRows[line] = name;
- } catch(Exception e) {
- }
- }
-
- public void setNamesOfLine(String []names) {
- try {
- for(int i=0; i<sizeRow; i++){
- nameOfRows[i] = names[i];
- }
- } catch(Exception e) {
- }
- }
-
- public String toString() {
- StringBuffer sb = new StringBuffer("");
- for(int i=0; i<sizeRow; i++) {
- sb.append("Row #" + i + " / " + nameOfRows[i] + ": ");
- for(int j=0; j<sizeColumn; j++) {
- sb.append(" " + matrice[i][j]);
- }
- sb.append("\n");
- }
- return sb.toString();
- }
-
- public void swapLines(int line0, int line1) {
- int tmp;
- for(int j=0; j<sizeColumn; j++){
- tmp = matrice[line0][j];
- matrice[line0][j] = matrice[line1][j];
- matrice[line1][j] = tmp;
- }
-
- String tmpName = nameOfRows[line0];
- nameOfRows[line0] = nameOfRows[line1];
- nameOfRows[line1] = tmpName;
- }
-
-
- // Apply a division on all elements of a line
- public void unitLine(int line0, int diviser) {
- for(int j=0; j<sizeColumn; j++){
- matrice[line0][j] = matrice[line0][j] / diviser;
- }
- }
-
- // Combine line line0 minus m times line1 ; line0 gets the result
- public void linearCombination(int line0, int line1, int m) {
- for(int j=0; j<sizeColumn; j++){
- matrice[line0][j] = matrice[line0][j] - (m * matrice[line1][j]);
- }
- }
-
- // Returns the line number at which there is the first non nul element of column col0
- // Returns -1 in case none is found
- public int rgpivot(int col0, int nbOfLines) {
- int i = col0;
- while((i<(nbOfLines)) && (matrice[i][col0] == 0)) {
- i++;
- }
- if (matrice[i][col0] == 0) {
- return 0;
- } else {
- return i;
- }
- }
-
-
-
-
-
-
-}
diff --git a/src/myutil/MyMath.java b/src/myutil/MyMath.java
new file mode 100755
index 0000000000000000000000000000000000000000..17c597fea508629af32f22479f13d4dbfe50df9e
--- /dev/null
+++ b/src/myutil/MyMath.java
@@ -0,0 +1,89 @@
+/**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 MyMath
+ * Creation: 08/02/2012
+ * Version 1.0 08/02/2012
+ * @author Ludovic APVRILLE
+ * @see
+ */
+
+package myutil;
+
+import java.util.*;
+
+public class MyMath {
+
+
+ public static int gcd(int[] numbers) {
+ if ((numbers ==null) || (numbers.length == 0)){
+ return -1;
+ }
+
+ if (numbers.length ==1) {
+ return Math.abs(numbers[0]);
+ }
+
+ int egcd = egcd(Math.abs(numbers[0]), Math.abs(numbers[1]));
+ int index = 2;
+ while(index<numbers.length) {
+ egcd = egcd(egcd, Math.abs(numbers[index]));
+ index ++;
+ }
+
+ return egcd;
+
+ }
+
+ // Euclidian algorithm for GCD
+ // a and b must be positive
+ public static int egcd(int a, int b) {
+ if (a == 0)
+ return b;
+ while (b != 0) {
+ if (a > b)
+ a = a - b;
+ else
+ b = b - a;
+ }
+ return a;
+ }
+
+
+
+}
diff --git a/src/tpndescription/Place.java b/src/tpndescription/Place.java
index 95483b2b93b00b8b65e76259e574122bc930aed2..642b84be8029f7a11d282931428c17741003a0b6 100755
--- a/src/tpndescription/Place.java
+++ b/src/tpndescription/Place.java
@@ -55,6 +55,10 @@ public class Place {
name = generateName();
}
+ public Place(String _name) {
+ name = _name;
+ }
+
public String generateName() {
int index = INDEX;
INDEX ++;
diff --git a/src/tpndescription/TPN.java b/src/tpndescription/TPN.java
index 0f82a9bc00d610e3c731e834b5d0dcf5c1dc14df..3415b10c47414054c9d9158285ef6408abaa265c 100755
--- a/src/tpndescription/TPN.java
+++ b/src/tpndescription/TPN.java
@@ -47,11 +47,13 @@ package tpndescription;
import java.util.*;
+import myutil.*;
+
public class TPN {
public static int INDEX = 0;
- private LinkedList places;
- private LinkedList transitions;
+ private LinkedList<Place> places;
+ private LinkedList<Transition> transitions;
private LinkedList attributes;
public TPN() {
@@ -67,22 +69,36 @@ public class TPN {
transitions.add(tr);
}
- public String toString() {
+ public String toTINAString() {
Place p;
String tpn = "net generatedWithTTool\n\n";
ListIterator iterator = transitions.listIterator();
while(iterator.hasNext()) {
tpn += ((Transition)(iterator.next())).toTINAString() + "\n";
}
- iterator = places.listIterator();
- while(iterator.hasNext()) {
- p = (Place)(iterator.next());
+ ListIterator iterator0 = places.listIterator();
+ while(iterator0.hasNext()) {
+ p = (Place)(iterator0.next());
if (p.nbOfToken > 0)
tpn += p.toTINAString() + "\n";
}
return tpn;
}
+ public String toString() {
+ String tpn = "net generatedWithTTool\n\n";
+ ListIterator iterator = transitions.listIterator();
+ while(iterator.hasNext()) {
+ tpn += "transition " + ((Transition)(iterator.next())).toString() + "\n";
+ }
+ tpn +=" Nb of places: " + places.size() + "\n";
+ for(Place p: places) {
+
+ tpn += "place "+ p.toString() + "\n";
+ }
+ return tpn;
+ }
+
public String getCString() {
return "";
}
@@ -97,5 +113,31 @@ public class TPN {
// Rename places and transitions
}
+
+ public IntMatrix getIncidenceMatrix() {
+ IntMatrix im = new IntMatrix(places.size(), transitions.size());
+
+ int i, j;
+
+ // putting names of lines;
+ i = 0;
+ for(Place p: places){
+ im.setNameOfLine(i, p.toString());
+ i++;
+ }
+
+ j=0;
+ for(Transition tr: transitions) {
+ for(Place pl0: tr.getDestinationPlaces()) {
+ im.setValue(places.indexOf(pl0), j, 1);
+ }
+ for(Place pl1: tr.getOriginPlaces()) {
+ im.setValue(places.indexOf(pl1), j, -1);
+ }
+ j++;
+ }
+
+ return im;
+ }
}
\ No newline at end of file
diff --git a/src/tpndescription/Transition.java b/src/tpndescription/Transition.java
index a9082e5201afbb710e4487a380cf9f15f41e676f..8cc211fa04c80ffbce9eb351ab3c291600bebda2 100755
--- a/src/tpndescription/Transition.java
+++ b/src/tpndescription/Transition.java
@@ -61,8 +61,8 @@ public class Transition {
public String action; /* action on a variable for example */
public String infoSynchro; /* action coming along with synchro; for example !x?y */
- private LinkedList originPlaces;
- private LinkedList destinationPlaces;
+ private LinkedList<Place> originPlaces;
+ private LinkedList<Place> destinationPlaces;
public Transition(String _label) {
label = _label;
@@ -71,6 +71,15 @@ public class Transition {
destinationPlaces = new LinkedList();
}
+
+ public LinkedList<Place> getOriginPlaces() {
+ return originPlaces;
+ }
+
+ public LinkedList<Place> getDestinationPlaces() {
+ return destinationPlaces;
+ }
+
public void addOriginPlace(Place p) {
originPlaces.add(p);
}
@@ -93,7 +102,7 @@ public class Transition {
}
public String toString() {
- return name + " " + getStringInterval();
+ return label;
}
public String toTINAString() {
diff --git a/src/ui/AvatarDesignPanelTranslator.java b/src/ui/AvatarDesignPanelTranslator.java
index 2211b0f03a5d590d676d8e84dc93c4eb62d6885c..259abeff8b26e2cf75cfdbce0251aadd23050333 100644
--- a/src/ui/AvatarDesignPanelTranslator.java
+++ b/src/ui/AvatarDesignPanelTranslator.java
@@ -291,6 +291,7 @@ public class AvatarDesignPanelTranslator {
return null;
}
+ // Other than PrivatePublicKeys
} else {
index = tmp.indexOf(".");
if (index == -1) {
@@ -303,8 +304,9 @@ public class AvatarDesignPanelTranslator {
for(Object o: _blocks) {
block = (AvatarBDBlock)o;
if (block.getBlockName().compareTo(blockName) == 0) {
+
if (b) {
- // authenticity
+ // Authenticity
stateName = tmp.substring(index+1, tmp.length());
//TraceManager.addDev("stateName=" + stateName);
index = stateName.indexOf(".");
@@ -320,7 +322,7 @@ public class AvatarDesignPanelTranslator {
found = true;
if ((ta.getType() == TAttribute.NATURAL) || (ta.getType() == TAttribute.INTEGER) || (ta.getType() == TAttribute.BOOLEAN)) {
- ret = ret + blockName + "." + paramName + " ";
+ ret = ret + blockName + "." + stateName + "." + paramName + " ";
} else if (ta.getType() == TAttribute.OTHER) {
// Must find all subsequent types
types = adp.getAvatarBDPanel().getAttributesOfDataType(ta.getTypeOther());
@@ -341,9 +343,8 @@ public class AvatarDesignPanelTranslator {
}
} else {
-
-
// Other: confidentiality, initial system knowledge, initial session knowledge, constant
+
paramName = tmp.substring(index+1, tmp.length());
for(Object oo: block.getAttributeList()) {
ta = (TAttribute)oo;
diff --git a/src/ui/GTURTLEModeling.java b/src/ui/GTURTLEModeling.java
index 69c207c222536274ee63175d374742ca5788f030..331ce40da531531170064af7432621e97f9e5579 100755
--- a/src/ui/GTURTLEModeling.java
+++ b/src/ui/GTURTLEModeling.java
@@ -86,6 +86,9 @@ import avatartranslator.*;
import avatartranslator.toturtle.*;
import avatartranslator.touppaal.*;
import avatartranslator.toproverif.*;
+import avatartranslator.totpn.*;
+
+import tpndescription.*;
import ui.tmlad.*;
import ui.tmlcd.*;
@@ -149,6 +152,9 @@ public class GTURTLEModeling {
private ProVerifSpec proverif;
+ private AVATAR2TPN avatar2tpn;
+ private TPN tpnFromAvatar;
+
private String tpn;
private String sim;
private String dta;
@@ -473,6 +479,35 @@ public class GTURTLEModeling {
}
}
+ public TPN generateTPNFromAvatar() {
+ avatar2tpn = new AVATAR2TPN(avatarspec);
+ //tml2uppaal.setChoiceDeterministic(choices);
+ //tml2uppaal.setSizeInfiniteFIFO(_size);
+ tpnFromAvatar = avatar2tpn.generateTPN(true, true);
+ languageID = TPN;
+ return tpnFromAvatar;
+ }
+ /*IntMatrix im = tpnFromAvatar.getIncidenceMatrix();
+ TraceManager.addDev("Farkas computing on " + im.toString());
+ im.Farkas();
+ TraceManager.addDev("Farkas done:" + im.toString());
+
+
+
+ languageID = TPN;
+ mgui.setMode(MainGUI.EDIT_PROVERIF_OK);
+ //mgui.setMode(MainGUI.MODEL_PROVERIF_OK);
+ //uppaalTable = tml2uppaal.getRelationTIFUPPAAL(_debug);
+ return true;
+ /*try {
+ avatar2tpn.saveInFile(_path);
+ TraceManager.addDev("Specification generated in " + _path);
+ return true;
+ } catch (FileException fe) {
+ TraceManager.addError("Exception: " + fe.getMessage());
+ return false;
+ }*/
+
public ArrayList<String> getUPPAALQueries() {
//TraceManager.addDev("Searching for queries");
TURTLEPanel tp = mgui.getCurrentTURTLEPanel();
diff --git a/src/ui/JMenuBarTurtle.java b/src/ui/JMenuBarTurtle.java
index 241948b521f9d2f8382d6a59673fe0d3d3706f5a..f98d0525cc86805807f02423e35fd1474355fca8 100755
--- a/src/ui/JMenuBarTurtle.java
+++ b/src/ui/JMenuBarTurtle.java
@@ -472,6 +472,8 @@ public class JMenuBarTurtle extends JMenuBar {
menuItem.addMouseListener(mgui.mouseHandler);
menuItem = vAndV.add(mgui.actions[TGUIAction.ACT_AVATAR_FV_PROVERIF]);
menuItem.addMouseListener(mgui.mouseHandler);
+ menuItem = vAndV.add(mgui.actions[TGUIAction.ACT_AVATAR_FV_STATICANALYSIS]);
+ menuItem.addMouseListener(mgui.mouseHandler);
/*vAndV.addSeparator();
menuItem = vAndV.add(mgui.actions[TGUIAction.ACT_DEADLOCK_SEEKER_AUT]);
diff --git a/src/ui/JToolBarMainTurtle.java b/src/ui/JToolBarMainTurtle.java
index e08c9df1d4fd2ac4ce4f80b0da7bf46f8f5669a0..275073a4e53a08d38da1a0b922dc72a7bdda5ece 100755
--- a/src/ui/JToolBarMainTurtle.java
+++ b/src/ui/JToolBarMainTurtle.java
@@ -59,7 +59,7 @@ import myutil.*;
public class JToolBarMainTurtle extends JToolBar {
// Avatar
- JButton avatarSimu, avatarFVUPPAAL, avatarFVProVerif, avatarCodeGeneration;
+ JButton avatarSimu, avatarFVUPPAAL, avatarFVProVerif, avatarFVStaticAnalysis, avatarCodeGeneration;
// Other
JButton genrtlotos, genlotos, genuppaal, gendesign;
@@ -154,6 +154,9 @@ public class JToolBarMainTurtle extends JToolBar {
avatarFVProVerif.addMouseListener(mgui.mouseHandler);
}
+ avatarFVStaticAnalysis = add(mgui.actions[TGUIAction.ACT_AVATAR_FV_STATICANALYSIS]);
+ avatarFVStaticAnalysis.addMouseListener(mgui.mouseHandler);
+
addSeparator();
avatarCodeGeneration = add(mgui.actions[TGUIAction.ACT_AVATAR_EXECUTABLE_GENERATION]);
@@ -264,6 +267,8 @@ public class JToolBarMainTurtle extends JToolBar {
if (avatarFVProVerif != null) {
avatarFVProVerif.setVisible(b);
}
+ //avatarFVStaticAnalysis.setVisible(b);
+ avatarFVStaticAnalysis.setVisible(false);
avatarCodeGeneration.setVisible(b);
if (genrtlotos != null) {
diff --git a/src/ui/MainGUI.java b/src/ui/MainGUI.java
index ce75a69d89604805d116ba22c55fd505e5b3dbf8..0a6008eeddb951769849d879f16147164665484d 100755
--- a/src/ui/MainGUI.java
+++ b/src/ui/MainGUI.java
@@ -602,7 +602,8 @@ public class MainGUI implements ActionListener, WindowListener, KeyListener {
case AVATAR_SYNTAXCHECKING_OK:
actions[TGUIAction.ACT_AVATAR_SIM].setEnabled(true);
actions[TGUIAction.ACT_AVATAR_FV_UPPAAL].setEnabled(true);
- actions[TGUIAction.ACT_AVATAR_FV_PROVERIF].setEnabled(true);
+ actions[TGUIAction.ACT_AVATAR_FV_PROVERIF].setEnabled(true);
+ actions[TGUIAction.ACT_AVATAR_FV_STATICANALYSIS].setEnabled(true);
actions[TGUIAction.ACT_AVATAR_EXECUTABLE_GENERATION].setEnabled(true);
break;
case REQ_OK:
@@ -643,6 +644,7 @@ public class MainGUI implements ActionListener, WindowListener, KeyListener {
actions[TGUIAction.ACT_AVATAR_SIM].setEnabled(false);
actions[TGUIAction.ACT_AVATAR_FV_UPPAAL].setEnabled(false);
actions[TGUIAction.ACT_AVATAR_FV_PROVERIF].setEnabled(false);
+ actions[TGUIAction.ACT_AVATAR_FV_STATICANALYSIS].setEnabled(false);
actions[TGUIAction.ACT_AVATAR_EXECUTABLE_GENERATION].setEnabled(false);
break;
case METHO_CHANGED:
@@ -3207,6 +3209,15 @@ public class MainGUI implements ActionListener, WindowListener, KeyListener {
dtree.toBeUpdated();
}
+ public void avatarStaticAnalysis() {
+ TraceManager.addDev("Avatar static analysis invariants");
+ JDialogInvariantAnalysis jgen = new JDialogInvariantAnalysis(frame, this, "Static analysis: invariants computation");
+ jgen.setSize(500, 450);
+ GraphicLib.centerOnParent(jgen);
+ jgen.setVisible(true);
+ dtree.toBeUpdated();
+ }
+
public void avatarExecutableCodeGeneration() {
TraceManager.addDev("Avatar code generation");
JDialogAvatarExecutableCodeGeneration jgen = new JDialogAvatarExecutableCodeGeneration(frame, this, "Executable Code generation, compilation and execution", ConfigurationTTool.AVATARExecutableCodeHost, ConfigurationTTool.AVATARExecutableCodeDirectory, ConfigurationTTool.AVATARExecutableCodeCompileCommand, ConfigurationTTool.AVATARExecutableCodeExecuteCommand, ConfigurationTTool.AVATARExecutableSoclibCodeCompileCommand, ConfigurationTTool.AVATARExecutableSoclibCodeExecuteCommand, ConfigurationTTool.AVATARExecutableSoclibTraceFile);
@@ -6518,6 +6529,8 @@ public class MainGUI implements ActionListener, WindowListener, KeyListener {
avatarUPPAALVerification();
} else if (command.equals(actions[TGUIAction.ACT_AVATAR_FV_PROVERIF].getActionCommand())) {
avatarProVerifVerification();
+ } else if (command.equals(actions[TGUIAction.ACT_AVATAR_FV_STATICANALYSIS].getActionCommand())) {
+ avatarStaticAnalysis();
} else if (command.equals(actions[TGUIAction.ACT_AVATAR_EXECUTABLE_GENERATION].getActionCommand())) {
avatarExecutableCodeGeneration();
diff --git a/src/ui/TGUIAction.java b/src/ui/TGUIAction.java
index 338a0cdecf70f46f8de7a84e684324a14b8ec793..d7b62c3e6db69e3c00529ac28cdc2f94e820d898 100755
--- a/src/ui/TGUIAction.java
+++ b/src/ui/TGUIAction.java
@@ -483,13 +483,14 @@ public class TGUIAction extends AbstractAction {
public static final int ACT_AVATAR_SIM = 339;
public static final int ACT_AVATAR_FV_UPPAAL = 337;
public static final int ACT_AVATAR_FV_PROVERIF = 338;
+ public static final int ACT_AVATAR_FV_STATICANALYSIS = 365;
public static final int ACT_AVATAR_EXECUTABLE_GENERATION = 340;
//Action for the help button created by Solange
public static final int PRUEBA_1 = 205;
- public static final int NB_ACTION = 365;
+ public static final int NB_ACTION = 366;
private static final TAction [] actions = new TAction[NB_ACTION];
@@ -617,6 +618,7 @@ public class TGUIAction extends AbstractAction {
actions[ACT_AVATAR_SIM] = new TAction("avatar-simu", "Interactive simulation", IconManager.imgic18, IconManager.imgic18, "Interactive simulation", "Interactive simulation of the AVATAR design under edition", '0');
actions[ACT_AVATAR_FV_UPPAAL] = new TAction("avatar-formal-verification-uppaal", "Formal verification with UPPAAL (Safety)", IconManager.imgic86, IconManager.imgic86, "Formal verification with UPPAAL (Safety)", "Formal verification with UPPAAL (Safety) of the AVATAR design under edition", '0');
actions[ACT_AVATAR_FV_PROVERIF] = new TAction("avatar-formal-verification-proverif", "Formal verification with ProVerif (Security)", IconManager.imgic88, IconManager.imgic88, "Formal verification with ProVerif (Security)", "Formal verification with ProVerif (Security) of the AVATAR design under edition", '0');
+ actions[ACT_AVATAR_FV_STATICANALYSIS] = new TAction("avatar-formal-verification-staticanalysis", "Static analysis (invariants)", IconManager.imgic88, IconManager.imgic88, "Static analysis (Invariant)", "Static analysis (invariants) of the AVATAR design under edition", '0');
actions[ACT_AVATAR_EXECUTABLE_GENERATION] = new TAction("avatar-executable-generation", "Generation of executable code", IconManager.imgic94, IconManager.imgic94, "Generation of executable code", "Generation of executable code from AVATAR design under edition", '0');
diff --git a/src/ui/avatarinteractivesimulation/JFrameAvatarInteractiveSimulation.java b/src/ui/avatarinteractivesimulation/JFrameAvatarInteractiveSimulation.java
index 2a66d5e5b427dbd55587cd41c5e956a1eb368fb2..ec5bd0789905f1b8681dcd89df1df60057bda5ff 100755
--- a/src/ui/avatarinteractivesimulation/JFrameAvatarInteractiveSimulation.java
+++ b/src/ui/avatarinteractivesimulation/JFrameAvatarInteractiveSimulation.java
@@ -788,7 +788,7 @@ public class JFrameAvatarInteractiveSimulation extends JFrame implements AvatarS
public void runSimulation() {
previousTime = System.currentTimeMillis();
if (ass != null) {
- ass.setNbOfCommands(AvatarSpecificationSimulation.MAX_TRANSACTIONS);
+ ass.setNbOfCommands(AvatarSpecificationSimulation.MAX_TRANSACTION_IN_A_ROW);
ass.goSimulation();
}
}
diff --git a/src/ui/window/JDialogInvariantAnalysis.java b/src/ui/window/JDialogInvariantAnalysis.java
new file mode 100644
index 0000000000000000000000000000000000000000..cb4540e57ae28fe6b39f9f10434b8d7467a92d3c
--- /dev/null
+++ b/src/ui/window/JDialogInvariantAnalysis.java
@@ -0,0 +1,305 @@
+/**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 JDialogInvariantAnalysis
+ * Dialog for managing the generation of ProVerif code and execution of
+ * ProVerif
+ * Creation: 09/02/2012
+ * @version 1.0 09/01/2012
+ * @author Ludovic APVRILLE
+ * @see
+ */
+
+package ui.window;
+
+import java.awt.*;
+import java.awt.event.*;
+import javax.swing.*;
+import javax.swing.event.*;
+import java.util.*;
+
+import myutil.*;
+import avatartranslator.totpn.*;
+import avatartranslator.*;
+import tpndescription.*;
+import ui.*;
+
+import launcher.*;
+
+
+public class JDialogInvariantAnalysis extends javax.swing.JDialog implements ActionListener, Runnable {
+
+ protected MainGUI mgui;
+
+ private JTabbedPane jp1;
+
+
+ protected final static int NOT_STARTED = 1;
+ protected final static int STARTED = 2;
+ protected final static int STOPPED = 3;
+
+ int mode;
+
+ //components
+ protected JTextArea jta, jtatpn, jtamatrix, jtainvariants;
+ protected JButton start;
+ protected JButton stop;
+ protected JButton close;
+
+
+ private Thread t;
+ private boolean go = false;
+ private boolean hasError = false;
+ //protected boolean startProcess = false;
+
+ private String hostProVerif;
+
+ protected RshClient rshc;
+
+
+ /** Creates new form */
+ public JDialogInvariantAnalysis(Frame f, MainGUI _mgui, String title) {
+ super(f, title, true);
+
+ mgui = _mgui;
+
+ initComponents();
+ myInitComponents();
+ pack();
+
+ //getGlassPane().addMouseListener( new MouseAdapter() {});
+ getGlassPane().setCursor(Cursor.getPredefinedCursor(Cursor.WAIT_CURSOR));
+ }
+
+ protected void myInitComponents() {
+ mode = NOT_STARTED;
+ setButtons();
+ }
+
+ protected void initComponents() {
+ JScrollPane jsp;
+
+ Container c = getContentPane();
+ setFont(new Font("Helvetica", Font.PLAIN, 14));
+ Font f = new Font("Courrier", Font.BOLD, 12);
+ c.setLayout(new BorderLayout());
+ //setDefaultCloseOperation(JFrame.DISPOSE_ON_CLOSE);
+
+ jp1 = new JTabbedPane();
+
+
+ jta = new ScrolledJTextArea();
+ jta.setEditable(false);
+ jta.setMargin(new Insets(10, 10, 10, 10));
+ jta.setTabSize(3);
+ jta.append("Press start to compute invariants\n");
+
+ jta.setFont(f);
+ jsp = new JScrollPane(jta, JScrollPane.VERTICAL_SCROLLBAR_ALWAYS, JScrollPane.HORIZONTAL_SCROLLBAR_ALWAYS);
+ jp1.add("Compute invariants", jsp);
+
+ jtatpn = new ScrolledJTextArea();
+ jtatpn.setEditable(false);
+ jtatpn.setMargin(new Insets(10, 10, 10, 10));
+ jtatpn.setTabSize(3);
+ //jta.append("Press start to compute invariants\n");
+ jtatpn.setFont(f);
+ jsp = new JScrollPane(jtatpn, JScrollPane.VERTICAL_SCROLLBAR_ALWAYS, JScrollPane.HORIZONTAL_SCROLLBAR_ALWAYS);
+ jp1.add("Petri net", jsp);
+
+ jtamatrix = new ScrolledJTextArea();
+ jtamatrix.setEditable(false);
+ jtamatrix.setMargin(new Insets(10, 10, 10, 10));
+ jtamatrix.setTabSize(3);
+ //jtamatrix.append("Press start to compute invariants\n");
+ jtamatrix.setFont(f);
+ jsp = new JScrollPane(jtamatrix, JScrollPane.VERTICAL_SCROLLBAR_ALWAYS, JScrollPane.HORIZONTAL_SCROLLBAR_ALWAYS);
+ jp1.add("Incidence matrix", jsp);
+
+ jtainvariants = new ScrolledJTextArea();
+ jtainvariants.setEditable(false);
+ jtainvariants.setMargin(new Insets(10, 10, 10, 10));
+ jtainvariants.setTabSize(3);
+ //jtamatrix.append("Press start to compute invariants\n");
+ jtainvariants.setFont(f);
+ jsp = new JScrollPane(jtainvariants, JScrollPane.VERTICAL_SCROLLBAR_ALWAYS, JScrollPane.HORIZONTAL_SCROLLBAR_ALWAYS);
+ jp1.add("Invariants", jsp);
+
+ c.add(jp1, BorderLayout.CENTER);
+
+ start = new JButton("Start", IconManager.imgic53);
+ stop = new JButton("Stop", IconManager.imgic55);
+ close = new JButton("Close", IconManager.imgic27);
+
+ start.setPreferredSize(new Dimension(100, 30));
+ stop.setPreferredSize(new Dimension(100, 30));
+ close.setPreferredSize(new Dimension(100, 30));
+
+ start.addActionListener(this);
+ stop.addActionListener(this);
+ close.addActionListener(this);
+
+ JPanel jp2 = new JPanel();
+ jp2.add(start);
+ jp2.add(stop);
+ jp2.add(close);
+
+ c.add(jp2, BorderLayout.SOUTH);
+
+ }
+
+ public void actionPerformed(ActionEvent evt) {
+ String command = evt.getActionCommand();
+
+ if (command.equals("Start")) {
+ startProcess();
+ } else if (command.equals("Stop")) {
+ stopProcess();
+ } else if (command.equals("Close")) {
+ closeDialog();
+ }
+ }
+
+ public void closeDialog() {
+ if (mode == STARTED) {
+ stopProcess();
+ }
+ dispose();
+ }
+
+ public void stopProcess() {
+ mode = STOPPED;
+ setButtons();
+ go = false;
+ if (t != null) {
+ t.interrupt();
+ }
+ }
+
+ public void startProcess() {
+ t = new Thread(this);
+ mode = STARTED;
+ setButtons();
+ go = true;
+ t.start();
+ }
+
+ private void testGo() throws InterruptedException {
+ if (go == false) {
+ throw new InterruptedException("Stopped by user");
+ }
+ }
+
+ public void run() {
+ TPN tpn;
+ hasError = false;
+
+ TraceManager.addDev("Thread started");
+
+ try {
+ jta.append("Generating Petri Net\n");
+ tpn = mgui.gtm.generateTPNFromAvatar();
+ jtatpn.append("Petri Net:\n" + tpn.toString() + "\n\n");
+ testGo();
+
+ jta.append("Computing incidence matrix\n");
+ IntMatrix im = tpn.getIncidenceMatrix();
+ jtamatrix.append("Incidence matrix:\n" + im.toString() + "\n\n");
+ jta.append("Incidence matrix computed\n");
+ testGo();
+
+ jta.append("Computing invariants\n");
+ im.Farkas();
+ jtainvariants.append("Invariants:\n" + im.namesOfRowToString() + "\n\n");
+ jta.append("Invariants computed\n");
+ testGo();
+
+ jta.append("All done\n");
+
+
+
+ } catch (InterruptedException ie) {
+ jta.append("Interrupted\n");
+ }
+
+ jta.append("\n\nReady to process next command\n");
+
+ checkMode();
+ setButtons();
+
+ //System.out.println("Selected item=" + selectedItem);
+ }
+
+ protected void checkMode() {
+ mode = NOT_STARTED;
+ }
+
+ protected void setButtons() {
+ switch(mode) {
+ case NOT_STARTED:
+ start.setEnabled(true);
+ stop.setEnabled(false);
+ close.setEnabled(true);
+ //setCursor(Cursor.getPredefinedCursor(Cursor.DEFAULT_CURSOR));
+ getGlassPane().setVisible(false);
+ break;
+ case STARTED:
+ start.setEnabled(false);
+ stop.setEnabled(true);
+ close.setEnabled(false);
+ getGlassPane().setVisible(true);
+ //setCursor(Cursor.getPredefinedCursor(Cursor.WAIT_CURSOR));
+ break;
+ case STOPPED:
+ default:
+ start.setEnabled(false);
+ stop.setEnabled(false);
+ close.setEnabled(true);
+ getGlassPane().setVisible(false);
+ break;
+ }
+ }
+
+ public boolean hasToContinue() {
+ return (go == true);
+ }
+
+ public void setError() {
+ hasError = true;
+ }
+}