diff --git a/src/avatartranslator/toproverif/AVATAR2ProVerif.java b/src/avatartranslator/toproverif/AVATAR2ProVerif.java
index 540c3b8de1fb89d5e98372f057a98167fc62cb43..eecc8f33e170c6817da17c73e7043327396319da 100755
--- a/src/avatartranslator/toproverif/AVATAR2ProVerif.java
+++ b/src/avatartranslator/toproverif/AVATAR2ProVerif.java
@@ -787,7 +787,7 @@ public class AVATAR2ProVerif implements AvatarTranslator {
// Use a dummy name if no value is sent
if (_asme.getNbOfValues() == 0)
- _lastInstr = _lastInstr.setNextInstr (new ProVerifProcNew ("data__", "bistring"));
+ _lastInstr = _lastInstr.setNextInstr (new ProVerifProcNew ("data__", "bitstring"));
String tmp = "out (" + CH_MAINCH + ", ";
if (isPrivate)
diff --git a/src/tmltranslator/TML2Avatar.java b/src/tmltranslator/TML2Avatar.java
new file mode 100644
index 0000000000000000000000000000000000000000..29574d99239bf1631d3d251f8e6f9128bcc94d46
--- /dev/null
+++ b/src/tmltranslator/TML2Avatar.java
@@ -0,0 +1,386 @@
+/**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 AVATAR2ProVerif
+ * Creation: 29/02/2016
+ * @version 1.1 29/02/2016
+ * @author Ludovic APVRILLE, Letitia LI
+ * @see
+ */
+
+package tmltranslator;
+import tmltranslator.*;
+import java.util.List;
+import java.util.LinkedList;
+import java.util.HashMap;
+import java.util.HashSet;
+import java.util.Vector;
+import java.io.*;
+import javax.swing.*;
+import java.util.ArrayList;
+
+import javax.xml.parsers.*;
+import ui.ConfigurationTTool;
+import ui.CheckingError;
+import ui.AvatarDesignPanel;
+import ui.TGComponent;
+import proverifspec.*;
+import myutil.*;
+import avatartranslator.*;
+
+public class TML2Avatar {
+ TMLMapping tmlmap;
+ List<String> allStates;
+ public TML2Avatar(TMLMapping tmlmap) {
+ this.tmlmap = tmlmap;
+ allStates = new ArrayList<String>();
+ }
+
+ public List<AvatarStateMachineElement> translateState(TMLActivityElement ae, AvatarBlock block){
+
+ TMLActionState tmlaction;
+ TMLChoice tmlchoice;
+ TMLExecI tmlexeci;
+ TMLExecIInterval tmlexecii;
+ TMLExecC tmlexecc;
+ TMLExecCInterval tmlexecci;
+ TMLForLoop tmlforloop;
+ TMLReadChannel tmlreadchannel;
+ TMLSendEvent tmlsendevent;
+ TMLSendRequest tmlsendrequest;
+ TMLStopState tmlstopstate;
+ TMLWaitEvent tmlwaitevent;
+ TMLNotifiedEvent tmlnotifiedevent;
+ TMLWriteChannel tmlwritechannel;
+ TMLSequence tmlsequence;
+ TMLRandomSequence tmlrsequence;
+ TMLSelectEvt tmlselectevt;
+ TMLDelay tmldelay;
+
+ AvatarTransition tran= new AvatarTransition(block, "", null);
+ List<AvatarStateMachineElement> elementList = new ArrayList<AvatarStateMachineElement>();
+
+ if (ae==null){
+ return elementList;
+ }
+
+ if (ae instanceof TMLStopState){
+ AvatarStopState stops= new AvatarStopState(ae.getName(), ae.getReferenceObject());
+ elementList.add(stops);
+ return elementList;
+ }
+ else if (ae instanceof TMLStartState){
+ AvatarStartState ss= new AvatarStartState(ae.getName(), ae.getReferenceObject());
+ tran = new AvatarTransition(block, "__after_" + ae.getName(), null);
+ ss.addNext(tran);
+ elementList.add(ss);
+ elementList.add(tran);
+ }
+ else if (ae instanceof TMLRandom){
+ AvatarRandom ar = new AvatarRandom(ae.getName(), ae.getReferenceObject());
+ TMLRandom tmlr = (TMLRandom) ae;
+ ar.setVariable(tmlr.getVariable());
+ ar.setValues(tmlr.getMinValue(), tmlr.getMaxValue());
+ tran = new AvatarTransition(block, "__after_"+ae.getName(), null);
+ ar.addNext(tran);
+ //Add to list
+ elementList.add(ar);
+ elementList.add(tran);
+ }
+ else if (ae instanceof TMLSequence){
+ //Get all list of sequences and paste together
+ List<AvatarStateMachineElement> seq = translateState(ae.getNextElement(0), block);
+ elementList.addAll(seq);
+ for (int i=1; i< ae.getNbNext(); i++){
+ List<AvatarStateMachineElement> tmp = translateState(ae.getNextElement(i), block);
+ seq.get(seq.size()-1).addNext(tmp.get(0));
+ elementList.addAll(tmp);
+ seq = tmp;
+ }
+ if (!(elementList.get(elementList.size()-1) instanceof AvatarStopState)){
+ tran = new AvatarTransition(block, "end_seq", null);
+ AvatarStopState ss = new AvatarStopState("stop", null);
+ elementList.get(elementList.size()-1).addNext(tran);
+ tran.addNext(ss);
+ elementList.add(tran);
+ elementList.add(ss);
+ }
+ return elementList;
+
+ }
+ else if (ae instanceof TMLRandomSequence){
+ HashMap<Integer, List<AvatarStateMachineElement>> seqs = new HashMap<Integer, List<AvatarStateMachineElement>>();
+ AvatarState choiceState = new AvatarState("seqchoice__"+ae.getName(), ae.getReferenceObject());
+ elementList.add(choiceState);
+ if (ae.getNbNext()==2){
+ //Create 2 choices, set0 -> set1 and set1 -> set0
+ /* for (int i=0; i< ae.getNbNext(); i++){
+ List<AvatarStateMachineElement> tmp = translateState(ae.getNextElement(i), block);
+ seqs.put(i, tmp);
+ }*/
+
+ List<AvatarStateMachineElement> set0= translateState(ae.getNextElement(0), block);
+ List<AvatarStateMachineElement> set1 = translateState(ae.getNextElement(1), block);
+ elementList.addAll(set0);
+ elementList.addAll(set1);
+
+ //Build branch 0
+ tran = new AvatarTransition(block, "__after_"+ae.getName()+"_0", null);
+ choiceState.addNext(tran);
+ elementList.add(tran);
+ tran.addNext(set0.get(0));
+ set0.get(set0.size()-1).addNext(set1.get(0));
+
+
+ //Build branch 1
+ List<AvatarStateMachineElement> set0_1= translateState(ae.getNextElement(0), block);
+ List<AvatarStateMachineElement> set1_1 =translateState(ae.getNextElement(1), block);
+ elementList.addAll(set0_1);
+ elementList.addAll(set1_1);
+ tran = new AvatarTransition(block, "__after_"+ae.getName()+"_1", null);
+ elementList.add(tran);
+ choiceState.addNext(tran);
+ tran.addNext(set1_1.get(0));
+ set1_1.get(set1_1.size()-1).addNext(set0_1.get(0));
+ }
+ else {
+ for (int i=0; i< ae.getNbNext(); i++){
+ //For each of the possible state blocks, translate 1 and recurse on the remaining random sequence
+ tran = new AvatarTransition(block, "__after_"+ae.getName()+"_"+i, null);
+ choiceState.addNext(tran);
+ List<AvatarStateMachineElement> tmp = translateState(ae.getNextElement(i), block);
+ tran.addNext(tmp.get(0));
+ TMLRandomSequence newSeq = new TMLRandomSequence("seqchoice__"+i+"_"+ae.getNbNext()+"_"+ae.getName(), ae.getReferenceObject());
+ for (int j=0; j< ae.getNbNext(); j++){
+ if (j!=i){
+ newSeq.addNext(ae.getNextElement(j));
+ }
+ }
+ tran = new AvatarTransition(block, "__after_"+ae.getNextElement(i).getName(), null);
+ tmp.get(tmp.size()-1).addNext(tran);
+ elementList.addAll(tmp);
+ elementList.add(tran);
+ List<AvatarStateMachineElement> nexts = translateState(newSeq, block);
+ elementList.addAll(nexts);
+ tran.addNext(nexts.get(0));
+ }
+ }
+ return elementList;
+ }
+ else if (ae instanceof TMLActivityElementEvent){
+ TMLActivityElementEvent aee = (TMLActivityElementEvent) ae;
+ TMLEvent ch = aee.getEvent();
+ if (ae instanceof TMLSendEvent){
+ AvatarSignal sig = new AvatarSignal(ch.getName(), AvatarSignal.OUT, ch.getReferenceObject());
+ AvatarActionOnSignal as= new AvatarActionOnSignal(ae.getName(), sig, ae.getReferenceObject());
+ tran= new AvatarTransition(block, "__after_"+ae.getName(), null);
+ elementList.add(as);
+ as.addNext(tran);
+ elementList.add(tran);
+ }
+ else if (ae instanceof TMLWaitEvent){
+ AvatarSignal sig = new AvatarSignal(ch.getName(), AvatarSignal.IN, ch.getReferenceObject());
+ AvatarActionOnSignal as= new AvatarActionOnSignal(ae.getName(), sig, ae.getReferenceObject());
+ tran= new AvatarTransition(block, "__after_"+ae.getName(), null);
+ elementList.add(as);
+ as.addNext(tran);
+ elementList.add(tran);
+ }
+ else {
+ //Notify Event, I don't know how to translate this
+ AvatarState as = new AvatarState(ae.getName(), ae.getReferenceObject());
+ tran = new AvatarTransition(block, "__after_"+ae.getName(), null);
+ as.addNext(tran);
+ elementList.add(as);
+ elementList.add(tran);
+ }
+
+ }
+ else if (ae instanceof TMLActivityElementWithAction){
+ AvatarState as = new AvatarState(ae.getName(), ae.getReferenceObject());
+ tran = new AvatarTransition(block, "__after_"+ae.getName(), null);
+ tran.addAction(((TMLActivityElementWithAction) ae).getAction());
+ as.addNext(tran);
+// AvatarActionAssignment aaa= new AvatarActionAssignment(
+ elementList.add(as);
+ elementList.add(tran);
+ }
+ else if (ae instanceof TMLActivityElementWithIntervalAction){
+ AvatarState as = new AvatarState(ae.getName(), ae.getReferenceObject());
+ tran = new AvatarTransition(block, "__after_"+ae.getName(), null);
+ as.addNext(tran);
+ elementList.add(as);
+ elementList.add(tran);
+ }
+ else if (ae instanceof TMLActivityElementChannel){
+ TMLActivityElementChannel aec = (TMLActivityElementChannel) ae;
+ TMLChannel ch = aec.getChannel(0);
+ AvatarSignal sig;
+ if (ae instanceof TMLReadChannel){
+ sig = new AvatarSignal(ch.getName(), AvatarSignal.IN, ch.getReferenceObject());
+ }
+ else {
+ sig = new AvatarSignal(ch.getName(), AvatarSignal.OUT, ch.getReferenceObject());
+ }
+ AvatarActionOnSignal as = new AvatarActionOnSignal(ae.getName(), sig, ae.getReferenceObject());
+ tran= new AvatarTransition(block, "__after_"+ae.getName(), null);
+ as.addNext(tran);
+ elementList.add(as);
+ elementList.add(tran);
+ }
+ else if (ae instanceof TMLForLoop){
+ TMLForLoop loop = (TMLForLoop)ae;
+ if (loop.isInfinite()){
+ List<AvatarStateMachineElement> elements = translateState(ae.getNextElement(0), block);
+ System.out.println("looping... " + ae.getNextElement(0));
+ AvatarTransition looptran = new AvatarTransition(block, "loop__"+ae.getName(), null);
+ elementList.addAll(elements);
+ elementList.add(looptran);
+ elements.get(elements.size()-1).addNext(looptran);
+ looptran.addNext(elements.get(0));
+ return elementList;
+ }
+ else {
+ System.out.println("why isn't my loop infinite ?");
+ }
+ }
+ else if (ae instanceof TMLChoice){
+ AvatarState as = new AvatarState(ae.getName(), ae.getReferenceObject(), true);
+ //Make many choices
+ elementList.add(as);
+ TMLChoice c = (TMLChoice) ae;
+ for (int i=0; i<c.getNbGuard(); i++){
+ tran = new AvatarTransition(block, "__after_"+ae.getName()+"_"+i, null);
+ tran.addGuard(c.getGuard(i));
+ as.addNext(tran);
+ List<AvatarStateMachineElement> nexts = translateState(ae.getNextElement(i), block);
+ tran.addNext(nexts.get(0));
+ elementList.add(tran);
+ elementList.addAll(nexts);
+ }
+ return elementList;
+
+ }
+ else if (ae instanceof TMLSelectEvt){
+ AvatarState as = new AvatarState(ae.getName(), ae.getReferenceObject());
+ //Make many choices
+ TMLSelectEvt c = (TMLSelectEvt) ae;
+ for (int i=0; i < ae.getNbNext(); i++){
+ tran = new AvatarTransition(block, "__after_"+ae.getName()+"_"+i, null);
+ as.addNext(tran);
+ List<AvatarStateMachineElement> nexts = translateState(ae.getNextElement(i), block);
+ tran.addNext(nexts.get(0));
+ elementList.addAll(nexts);
+ }
+ return elementList;
+ }
+ else {
+ System.out.println("undefined tml element " + ae);
+ }
+ List<AvatarStateMachineElement> nexts = translateState(ae.getNextElement(0), block);
+ if (nexts.size()==0){
+ //in an infinite loop i hope
+ return elementList;
+ }
+ tran.addNext(nexts.get(0));
+ elementList.addAll(nexts);
+ return elementList;
+ }
+
+ public String processName(String name, int id){
+ name = name.replaceAll("-","_").replaceAll(" ","");
+ if (allStates.contains(name)){
+ return name+id;
+
+ }
+ else {
+ allStates.add(name);
+ return name;
+ }
+ }
+
+ public AvatarSpecification generateAvatarSpec(){
+ AvatarSpecification avspec = new AvatarSpecification("spec", null);
+ ArrayList<TMLTask> tasks = tmlmap.getTMLModeling().getTasks();
+ for (TMLTask task:tasks){
+ AvatarBlock block = new AvatarBlock(task.getName(), avspec, task.getReferenceObject());
+ for (TMLAttribute attr: task.getAttributes()){
+ AvatarType type;
+ if (attr.getType().getType()==TMLType.NATURAL){
+ type = AvatarType.INTEGER;
+ }
+ else if (attr.getType().getType()==TMLType.BOOLEAN) {
+ type = AvatarType.BOOLEAN;
+ }
+ else {
+ type = AvatarType.UNDEFINED;
+ }
+ AvatarAttribute avattr = new AvatarAttribute(attr.getName(), type, block, null);
+ block.addAttribute(avattr);
+ }
+ AvatarTransition last;
+ AvatarStateMachine asm = block.getStateMachine();
+ List<AvatarStateMachineElement> elementList= translateState(task.getActivityDiagram().get(0), block);
+ int i=0;
+ for (AvatarStateMachineElement e: elementList){
+ e.setName(processName(e.getName(), e.getID()));
+ i++;
+ asm.addElement(e);
+ }
+ asm.setStartState((AvatarStartState) elementList.get(0));
+ /* for (int i=1; i<task.getActivityDiagram().nElements(); i++){
+ TMLActivityElement ae= task.getActivityDiagram().get(i);
+ List<AvatarStateMachineElement> elementList= translateState(ae);
+ last.addNext(elementList.get(0));
+ for (AvatarStateMachineElement el: elementList){
+ asm.addElement(el);
+ }
+ if (elementList.get(elementList.size()-1) instanceof AvatarTransition){
+ last = elementList.get(elementList.size()-1);
+ }
+ }*/
+
+
+ avspec.addBlock(block);
+
+ }
+ System.out.println(avspec);
+ return avspec;
+ }
+
+}
diff --git a/src/tmltranslator/TMLMapping.java b/src/tmltranslator/TMLMapping.java
index 3037df545acd456414bd51a7bf0b7f1c5e5c9de3..16d0f93376ad384a257e10e1026baaa6ea375a22 100755
--- a/src/tmltranslator/TMLMapping.java
+++ b/src/tmltranslator/TMLMapping.java
@@ -67,7 +67,7 @@ public class TMLMapping {
private ArrayList<TMLCPLib> mappedCPLibs;
-
+ private ArrayList<String[]> pragmas= new ArrayList<String[]>();
private boolean optimized = false;
private int hashCode;
@@ -288,6 +288,14 @@ public class TMLMapping {
return tmla.getCPUIDs();
}
+ public void addPragma(String[] s){
+ pragmas.add(s);
+ }
+
+ public ArrayList<String[]> getPragmas(){
+ return pragmas;
+ }
+
public String[] getCPUandHwAIDs() {
if (tmla == null) {
return null;
diff --git a/src/tmltranslator/toproverif/TML2ProVerif.class b/src/tmltranslator/toproverif/TML2ProVerif.class
new file mode 100644
index 0000000000000000000000000000000000000000..f4e43056eeeadb11c71233977d3aa11303a44aec
Binary files /dev/null and b/src/tmltranslator/toproverif/TML2ProVerif.class differ
diff --git a/src/tmltranslator/toproverif/TML2ProVerif.java b/src/tmltranslator/toproverif/TML2ProVerif.java
index 9c971e82889e6dd50d714ff89a556e1b6d1ffd6e..6baa71032b40926c0be5256249295af8ed33db74 100644
--- a/src/tmltranslator/toproverif/TML2ProVerif.java
+++ b/src/tmltranslator/toproverif/TML2ProVerif.java
@@ -336,7 +336,7 @@ public class TML2ProVerif {
/* Queries */
this.spec.addDeclaration (new ProVerifComment ("Queries Secret"));
TraceManager.addDev("Queries Secret");
- for (String[] pragma: tmlmodel.getPragmas ()){
+ for (String[] pragma: tmlmap.getPragmas ()){
if (pragma[0].equals("#Confidentiality")){
this.spec.addDeclaration (new ProVerifQueryAtt (pragma[1].replaceAll("\\.", "__"), true));
TraceManager.addDev("| attacker (" + pragma[1].replaceAll("\\.", "__") + ")");
@@ -521,37 +521,45 @@ TMLActivity act= task.getActivityDiagram();
//declare entering
p = p.setNextInstr (new ProVerifProcRaw ("event enteringState__" + task.getName() + "__" + stateNum + "()", true));
stateNum++;
- if (ae instanceof TMLActivityElementChannel){
- TMLActivityElementChannel aec = (TMLActivityElementChannel) ae;
- int channelStatus = channelMap.get(aec.getChannel(0).getName());
- if (aec instanceof TMLWriteChannel){
- tmp = "out (" + CH_MAINCH + ", ";
- //Look up privacy
- if (channelStatus!=channelUnreachable){
- if (channelStatus==channelPrivate)
- tmp += CH_ENCRYPT + " (";
- tmp += "data__"+aec.getChannel(0).getName()+")";
- if (channelStatus==channelPrivate)
- tmp += ")";
- p = p.setNextInstr(new ProVerifProcRaw (tmp, true));
- }
- }
- else {
- if (channelStatus==channelPrivate) {
- LinkedList<ProVerifVar> vars = new LinkedList<ProVerifVar> ();
- TraceManager.addDev("| | in (chPriv, ...)");
- vars.add (new ProVerifVar ("data__"+ aec.getChannel(0).getName(), "bitstring"));
- p = p.setNextInstr (new ProVerifProcIn (CH_MAINCH, new ProVerifVar[] {new ProVerifVar ("privChData", "bitstring")}));
- p = p.setNextInstr (new ProVerifProcLet (vars.toArray (new ProVerifVar[vars.size()]), CH_DECRYPT + " (privChData)"));
- }
- else {
- LinkedList<ProVerifVar> vars = new LinkedList<ProVerifVar> ();
- vars.add (new ProVerifVar ("data__"+ aec.getChannel(0).getName(), "bitstring"));
- p=p.setNextInstr(new ProVerifProcIn (CH_MAINCH, vars.toArray (new ProVerifVar[vars.size()])));
- }
+ if (ae instanceof TMLChoice){
+ TMLChoice aechoice = (TMLChoice) ae;
+ for (int i=0; i< ae.getNbNext(); i++){
+
+ }
+ }
+ else {
+ if (ae instanceof TMLActivityElementChannel){
+ TMLActivityElementChannel aec = (TMLActivityElementChannel) ae;
+ int channelStatus = channelMap.get(aec.getChannel(0).getName());
+ if (aec instanceof TMLWriteChannel){
+ tmp = "out (" + CH_MAINCH + ", ";
+ //Look up privacy
+ if (channelStatus!=channelUnreachable){
+ if (channelStatus==channelPrivate)
+ tmp += CH_ENCRYPT + " (";
+ tmp += "data__"+aec.getChannel(0).getName()+")";
+ if (channelStatus==channelPrivate)
+ tmp += ")";
+ p = p.setNextInstr(new ProVerifProcRaw (tmp, true));
+ }
+ }
+ else {
+ if (channelStatus==channelPrivate) {
+ LinkedList<ProVerifVar> vars = new LinkedList<ProVerifVar> ();
+ TraceManager.addDev("| | in (chPriv, ...)");
+ vars.add (new ProVerifVar ("data__"+ aec.getChannel(0).getName(), "bitstring"));
+ p = p.setNextInstr (new ProVerifProcIn (CH_MAINCH, new ProVerifVar[] {new ProVerifVar ("privChData", "bitstring")}));
+ p = p.setNextInstr (new ProVerifProcLet (vars.toArray (new ProVerifVar[vars.size()]), CH_DECRYPT + " (privChData)"));
+ }
+ else {
+ LinkedList<ProVerifVar> vars = new LinkedList<ProVerifVar> ();
+ vars.add (new ProVerifVar ("data__"+ aec.getChannel(0).getName(), "bitstring"));
+ p=p.setNextInstr(new ProVerifProcIn (CH_MAINCH, vars.toArray (new ProVerifVar[vars.size()])));
+ }
+ }
}
+ ae = ae.getNextElement(0);
}
- ae = ae.getNextElement(0);
}
diff --git a/src/ui/GTMLModeling.java b/src/ui/GTMLModeling.java
index 2c3a200322fb116dc1cece7e33b7497f0629c512..d3a36dccc7d941697c9fab733d8c205c91b2cbbd 100755
--- a/src/ui/GTMLModeling.java
+++ b/src/ui/GTMLModeling.java
@@ -62,6 +62,8 @@ import tmltranslator.toproverif.*;
import proverifspec.*;
import myutil.*;
import tmltranslator.ctranslator.*;
+import avatartranslator.*;
+
public class GTMLModeling {
private TMLDesignPanel tmldp;
@@ -75,8 +77,7 @@ public class GTMLModeling {
private LinkedList removedChannels, removedRequests, removedEvents;
private static CorrespondanceTGElement listE;
private Hashtable<String, String> table;
- public Map<String, Boolean> channelConfMap = new HashMap<String, Boolean>();
-
+ public AvatarSpecification avspec;
//private ArrayList<HwNode> nodesToTakeIntoAccount;
private LinkedList nodesToTakeIntoAccount;
@@ -287,21 +288,21 @@ public class GTMLModeling {
}
private void addTMLPragmas(){
TGComponent tgc;
- System.out.println(tmlap);
components = tmlap.tmlap.getComponentList();
ListIterator iterator = components.listIterator();
while(iterator.hasNext()) {
- tgc = (TGComponent)(iterator.next());
- if (tgc instanceof TGCNote){
- TGCNote note = (TGCNote) tgc;
- String[] vals = note.getValues();
- for (String s: vals){
- if (s.contains(" ") && s.contains(".")){
- tmlm.addPragma(s.split(" "));
- }
+ tgc = (TGComponent)(iterator.next());
+ if (tgc instanceof TGCNote){
+ TGCNote note = (TGCNote) tgc;
+ String[] vals = note.getValues();
+ for (String s: vals){
+ System.out.println("Val " + s);
+ if (s.contains("#") && s.contains(" ")){
+ map.addPragma(s.split(" "));
+ }
+ }
}
- }
- }
+ }
}
private void addTMLTasks() throws MalformedTMLDesignException {
TGComponent tgc;
@@ -1530,6 +1531,7 @@ public class GTMLModeling {
tmlforloop.setInit("");
tmlforloop.setCondition("");
tmlforloop.setIncrement("");
+ tmlforloop.setInfinite(true);
activity.addElement(tmlforloop);
((BasicErrorHighlight)tgc).setStateAction(ErrorHighlight.OK);
listE.addCor(tmlforloop, tgc);
@@ -2242,6 +2244,7 @@ public class GTMLModeling {
bus.arbitration = busnode.getArbitrationPolicy();
bus.clockRatio = busnode.getClockRatio();
bus.sliceTime = busnode.getSliceTime();
+ bus.privacy = busnode.getPrivacy();
listE.addCor(bus, busnode);
archi.addHwNode(bus);
TraceManager.addDev("BUS node added:" + bus.getName());
@@ -3085,92 +3088,8 @@ public class GTMLModeling {
}
addTMLPragmas();
- ArrayList<TMLChannel> channels = tmlm.getChannels();
- List<TMLTask> destinations = new ArrayList<TMLTask>();
- TMLTask a;
- for (TMLChannel channel: channels){
- destinations.clear();
- if (channel.isBasicChannel()){
- a = channel.getOriginTask();
- destinations.add(channel.getDestinationTask());
- }
- else {
- a=channel.getOriginTasks().get(0);
- destinations.addAll(channel.getDestinationTasks());
- }
- HwCPU node1 = (HwCPU) map.getHwNodeOf(a);
- for (TMLTask t: destinations){
- List<HwBus> buses = new ArrayList<HwBus>();
- HwNode node2 = map.getHwNodeOf(t);
- if (node1==node2){
- System.out.println("Channel "+channel.getName() + " between Task "+ a.getTaskName() + " and Task " + t.getTaskName() + " is confidential");
- channelConfMap.put(channel.getName(), true);
- }
- if (node1!=node2){
- //Navigate architecture for node
- List<HwLink> links = archi.getHwLinks();
- HwNode last = node1;
- List<HwNode> found = new ArrayList<HwNode>();
- List<HwNode> done = new ArrayList<HwNode>();
- List<HwNode> path = new ArrayList<HwNode>();
- Map<HwNode, List<HwNode>> pathMap = new HashMap<HwNode, List<HwNode>>();
- for (HwLink link: links){
- if (link.hwnode == node1){
- found.add(link.bus);
- List<HwNode> tmp = new ArrayList<HwNode>();
- tmp.add(link.bus);
- pathMap.put(link.bus, tmp);
- }
- }
- outerloop:
- while (found.size()>0){
- HwNode curr = found.remove(0);
- for (HwLink link: links){
- if (curr == link.bus){
- if (link.hwnode == node2){
- path = pathMap.get(curr);
- break outerloop;
- }
- if (!done.contains(link.hwnode) && !found.contains(link.hwnode) && link.hwnode instanceof HwBridge){
- found.add(link.hwnode);
- List<HwNode> tmp = new ArrayList<HwNode>(pathMap.get(curr));
- tmp.add(link.hwnode);
- pathMap.put(link.hwnode, tmp);
- }
- }
- else if (curr == link.hwnode){
- if (!done.contains(link.bus) && !found.contains(link.bus)){
- found.add(link.bus);
- List<HwNode> tmp = new ArrayList<HwNode>(pathMap.get(curr));
- tmp.add(link.bus);
- pathMap.put(link.bus, tmp);
- }
- }
- }
- done.add(curr);
- }
- if (path.size() ==0){
- System.out.println("Path does not exist for channel " + channel.getName() + " between Task " + a.getTaskName() + " and Task " + t.getTaskName());
- }
- else {
- boolean priv=true;
- HwBus bus;
- //Check if all buses and bridges are private
- for (HwNode n: path){
- if (n instanceof HwBus){
- bus = (HwBus) n;
- if (bus.privacy ==0){
- priv=false;
- break;
- }
- }
- }
- channelConfMap.put(channel.getName(), priv);
- System.out.println("Channel "+channel.getName() + " between Task "+ a.getTaskName() + " and Task " + t.getTaskName() + " is " + (priv ? "confidential" : "not confidential"));
- }
- }
- }
- }
+ TML2Avatar t2a = new TML2Avatar(map);
+ avspec = t2a.generateAvatarSpec();
}
public void addToTable(String s1, String s2) {
diff --git a/src/ui/GTURTLEModeling.java b/src/ui/GTURTLEModeling.java
index 61b98f38f7c8d3999608ee4078661a3f01174ec9..b411b428bbd4818c7c33a837d59a3f6a585ad444 100755
--- a/src/ui/GTURTLEModeling.java
+++ b/src/ui/GTURTLEModeling.java
@@ -6548,13 +6548,12 @@ public class GTURTLEModeling {
artificialtmap = tmlm.getDefaultMapping();
tmap = null;
listE = gtmlm.getCorrespondanceTable();
-
//TraceManager.addDev("TML Modeling translated");
//TraceManager.addDev("----- TML Modeling -----");
//TraceManager.addDev(tmlm.toString());
//TraceManager.addDev("------------------------");
checkingErrors = gtmlm.getCheckingErrors();
-
+
if ((checkingErrors != null) && (checkingErrors.size() > 0)){
analyzeErrors();
return false;
@@ -6665,7 +6664,7 @@ public class GTURTLEModeling {
listE = gtmlm.getCorrespondanceTable();
checkingErrors = gtmlm.getCheckingErrors();
-
+ avatarspec = gtmlm.avspec;
if ((checkingErrors != null) && (checkingErrors.size() > 0)){
analyzeErrors();
warnings = gtmlm.getCheckingWarnings();
diff --git a/src/ui/JToolBarMainTurtle.java b/src/ui/JToolBarMainTurtle.java
index 80cf598954f9ed426f162c59180dafe15168caeb..4f770d38bc9a1ca626de603585ff35a056e3a52b 100755
--- a/src/ui/JToolBarMainTurtle.java
+++ b/src/ui/JToolBarMainTurtle.java
@@ -387,7 +387,7 @@ public class JToolBarMainTurtle extends JToolBar implements ActionListener
avatarSimu.setVisible(!b);
avatarFVUPPAAL.setVisible(!b);
if (avatarFVProVerif != null) {
- avatarFVProVerif.setVisible(!b);
+ avatarFVProVerif.setVisible(b);
}
avatarCodeGeneration.setVisible(!b);
diff --git a/src/ui/tmldd/TMLArchiBUSNode.java b/src/ui/tmldd/TMLArchiBUSNode.java
index c146a6eb9737f8c6400b9f6674f6084ae97a5133..8bec85d671fe3e2deabd5ea53fdd9e4bb9e2b688 100755
--- a/src/ui/tmldd/TMLArchiBUSNode.java
+++ b/src/ui/tmldd/TMLArchiBUSNode.java
@@ -303,6 +303,7 @@ public class TMLArchiBUSNode extends TMLArchiCommunicationNode implements Swallo
sb.append(" sliceTime=\"" + sliceTime + "\" ");
sb.append(" pipelineSize=\"" + pipelineSize + "\" ");
sb.append(" clockRatio=\"" + clockRatio + "\" ");
+ sb.append(" privacy=\"" + privacy + "\" ");
sb.append("/>\n");
sb.append("</extraparam>\n");
return new String(sb);
@@ -310,54 +311,53 @@ public class TMLArchiBUSNode extends TMLArchiCommunicationNode implements Swallo
public void loadExtraParam(NodeList nl, int decX, int decY, int decId) throws MalformedModelingException{
//System.out.println("*** load extra synchro ***");
- try {
-
- NodeList nli;
- Node n1, n2;
- Element elt;
- int t1id;
- String sstereotype = null, snodeName = null;
-
- for(int i=0; i<nl.getLength(); i++) {
- n1 = nl.item(i);
- //System.out.println(n1);
- if (n1.getNodeType() == Node.ELEMENT_NODE) {
- nli = n1.getChildNodes();
- for(int j=0; i<nli.getLength(); i++) {
- n2 = nli.item(i);
- //System.out.println(n2);
- if (n2.getNodeType() == Node.ELEMENT_NODE) {
- elt = (Element) n2;
- if (elt.getTagName().equals("info")) {
- sstereotype = elt.getAttribute("stereotype");
- snodeName = elt.getAttribute("nodeName");
- }
- if (sstereotype != null) {
- stereotype = sstereotype;
- }
- if (snodeName != null){
- name = snodeName;
- }
-
- if (elt.getTagName().equals("attributes")) {
- byteDataSize = Integer.decode(elt.getAttribute("byteDataSize")).intValue();
- arbitrationPolicy =Integer.decode(elt.getAttribute("arbitrationPolicy")).intValue();
- pipelineSize = Integer.decode(elt.getAttribute("pipelineSize")).intValue();
- if ((elt.getAttribute("clockRatio") != null) && (elt.getAttribute("clockRatio").length() > 0)){
- clockRatio = Integer.decode(elt.getAttribute("clockRatio")).intValue();
- }
- if ((elt.getAttribute("sliceTime") != null) && (elt.getAttribute("sliceTime").length() > 0)){
- sliceTime = Integer.decode(elt.getAttribute("sliceTime")).intValue();
- }
- }
- }
- }
+ try {
+ NodeList nli;
+ Node n1, n2;
+ Element elt;
+ int t1id;
+ String sstereotype = null, snodeName = null;
+ for(int i=0; i<nl.getLength(); i++) {
+ n1 = nl.item(i);
+ //System.out.println(n1);
+ if (n1.getNodeType() == Node.ELEMENT_NODE) {
+ nli = n1.getChildNodes();
+ for(int j=0; i<nli.getLength(); i++) {
+ n2 = nli.item(i);
+ //System.out.println(n2);
+ if (n2.getNodeType() == Node.ELEMENT_NODE) {
+ elt = (Element) n2;
+ if (elt.getTagName().equals("info")) {
+ sstereotype = elt.getAttribute("stereotype");
+ snodeName = elt.getAttribute("nodeName");
+ }
+ if (sstereotype != null) {
+ stereotype = sstereotype;
+ }
+ if (snodeName != null){
+ name = snodeName;
}
+ if (elt.getTagName().equals("attributes")) {
+ byteDataSize = Integer.decode(elt.getAttribute("byteDataSize")).intValue();
+ arbitrationPolicy =Integer.decode(elt.getAttribute("arbitrationPolicy")).intValue(); pipelineSize = Integer.decode(elt.getAttribute("pipelineSize")).intValue();
+ if ((elt.getAttribute("clockRatio") != null) && (elt.getAttribute("clockRatio").length() > 0)){
+ clockRatio = Integer.decode(elt.getAttribute("clockRatio")).intValue();
+ }
+ if ((elt.getAttribute("sliceTime") != null) && (elt.getAttribute("sliceTime").length() > 0)){
+ sliceTime = Integer.decode(elt.getAttribute("sliceTime")).intValue();
+ }
+ if ((elt.getAttribute("privacy") != null) && (elt.getAttribute("privacy").length() > 0)){
+ privacy = Integer.decode(elt.getAttribute("privacy")).intValue();
+ }
+ }
+ }
}
-
- } catch (Exception e) {
- throw new MalformedModelingException();
+ }
}
+
+ } catch (Exception e) {
+ throw new MalformedModelingException();
+ }
}
diff --git a/tests/Avatar/AvatarGuardTests.java b/tests/Avatar/AvatarGuardTests.java
index 7e0d60ec5f828d0a1064cbcd48f3a24c1a1231f9..c5fec63c84949ef75a4db77b29c1067daff31a02 100644
--- a/tests/Avatar/AvatarGuardTests.java
+++ b/tests/Avatar/AvatarGuardTests.java
@@ -36,10 +36,10 @@
* knowledge of the CeCILL license and that you accept its terms.
*
* /**
- * Class AvatarPragma
- * Creation: 20/05/2010
- * @version 1.1 01/07/2014
- * @author Ludovic APVRILLE, Raja GATGOUT
+ * Class AvatarGuardTests
+ * Creation: 20/05/2015
+ * @version 1.1 01/07/2015
+ * @author Ludovic APVRILLE, Letitia LI
* @see
*/