diff --git a/Makefile b/Makefile
index b4a8cc945674e5d8cace75d7a853a00bed7de269..e6b70a1bdd56b3428e5bbf64387550a85f73ef29 100755
--- a/Makefile
+++ b/Makefile
@@ -151,7 +151,7 @@ jar: launcher ttooljar tiftranslator tmltranslator rundse remotesimulator
ttooljar:
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/totpn/* avatartranslator/*.class avatartranslator/toturtle/*.java automata/*.class compiler/tmlparser/*.class nc/*.class tepe/*.class tmltranslator/*.class tmltranslator/tmlcp/*.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/navigation/*.gif ui/images/toolbarButtonGraphics/media/*.gif $(TTOOL_BIN)/$(LAUNCHER_BINARY) RTLLauncher.class launcher/*.class fr/inria/oasis/vercors/cttool/model/*.class remotesimulation/*.class tmltranslator/ctranslator/*.class attacktrees/*.class myutil/externalSearch/*.class ddtranslatorSoclib/*.class ddtranslatorSoclib/toSoclib/*.class ddtranslatorSoclib/toTopCell/*.class #compiler/tmlCPparser/parser/*.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/toavatar/*.class tmltranslator/tmlcp/*.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/navigation/*.gif ui/images/toolbarButtonGraphics/media/*.gif $(TTOOL_BIN)/$(LAUNCHER_BINARY) RTLLauncher.class launcher/*.class fr/inria/oasis/vercors/cttool/model/*.class remotesimulation/*.class tmltranslator/ctranslator/*.class attacktrees/*.class myutil/externalSearch/*.class ddtranslatorSoclib/*.class ddtranslatorSoclib/toSoclib/*.class ddtranslatorSoclib/toTopCell/*.class #compiler/tmlCPparser/parser/*.class
launcher:
rm -f $(TTOOL_BIN)/$(LAUNCHER_BINARY)
diff --git a/src/avatartranslator/AvatarStateMachineElement.java b/src/avatartranslator/AvatarStateMachineElement.java
index 3f5024e433c78de2eb345d3a519eccc28966eca6..001877d52bbe55bc0ec692e84f180f8d5067a007 100644
--- a/src/avatartranslator/AvatarStateMachineElement.java
+++ b/src/avatartranslator/AvatarStateMachineElement.java
@@ -96,6 +96,12 @@ public abstract class AvatarStateMachineElement extends AvatarElement {
return null;
}
+ public void removeNext(int _index){
+ if (_index < nexts.size()){
+ nexts.remove(_index);
+ }
+ }
+
public void setHidden(boolean _b) {
isHidden = _b;
}
diff --git a/src/tmltranslator/toavatar/TML2Avatar.java b/src/tmltranslator/toavatar/TML2Avatar.java
new file mode 100644
index 0000000000000000000000000000000000000000..98b20679ff9226b4c4013e1d7c1f70c282a67795
--- /dev/null
+++ b/src/tmltranslator/toavatar/TML2Avatar.java
@@ -0,0 +1,849 @@
+/**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.toavatar;
+import tmltranslator.*;
+import java.util.List;
+import java.util.LinkedList;
+import java.util.HashMap;
+import java.util.Map;
+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;
+ TMLModeling tmlmodel;
+
+ public HashMap<TMLChannel, Integer> channelMap = new HashMap<TMLChannel,Integer>();
+ public HashMap<TMLTask, AvatarBlock> taskBlockMap = new HashMap<TMLTask, AvatarBlock>();
+ HashMap<String, AvatarSignal> signalMap = new HashMap<String, AvatarSignal>();
+ List<AvatarSignal> signals = new ArrayList<AvatarSignal>();
+ private final static Integer channelPublic = 0;
+ private final static Integer channelPrivate = 1;
+ private final static Integer channelUnreachable = 2;
+
+
+ List<String> allStates;
+ public TML2Avatar(TMLMapping tmlmap) {
+ this.tmlmap = tmlmap;
+ this.tmlmodel = tmlmap.getTMLModeling();
+ allStates = new ArrayList<String>();
+ }
+
+ public void checkChannels(){
+ ArrayList<TMLChannel> channels = tmlmodel.getChannels();
+ List<TMLTask> destinations = new ArrayList<TMLTask>();
+ TMLTask a;
+ for (AvatarSignal sig:signals){
+ System.out.println("signal "+sig.getName());
+ }
+ for (TMLChannel channel: channels){
+ System.out.println(channel.getName());
+ 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) tmlmap.getHwNodeOf(a);
+ for (TMLTask t: destinations){
+ List<HwBus> buses = new ArrayList<HwBus>();
+ HwNode node2 = tmlmap.getHwNodeOf(t);
+ if (node1==node2){
+ System.out.println("Channel "+channel.getName() + " between Task "+ a.getTaskName() + " and Task " + t.getTaskName() + " is confidential");
+ channelMap.put(channel, channelPrivate);
+ }
+ if (node1!=node2){
+ //Navigate architecture for node
+ List<HwLink> links = tmlmap.getTMLArchitecture().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());
+ channelMap.put(channel, channelUnreachable);
+ }
+ else {
+ int priv=1;
+ HwBus bus;
+ //Check if all buses and bridges are private
+ for (HwNode n: path){
+ if (n instanceof HwBus){
+ bus = (HwBus) n;
+ System.out.println("BUS PRIVACY "+bus.privacy);
+ if (bus.privacy ==0){
+ priv=0;
+ break;
+ }
+ }
+ }
+ channelMap.put(channel, priv);
+ System.out.println("Channel "+channel.getName() + " between Task "+ a.getTaskName() + " and Task " + t.getTaskName() + " is " + (priv==1 ? "confidential" : "not confidential"));
+ }
+ }
+ }
+ }
+ }
+
+
+ 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);
+ List<AvatarStateMachineElement> tmp;
+ // elementList.addAll(seq);
+ //get rid of any stops in the middle of the sequence and replace with the start of the next sequence
+ for (int i=1; i< ae.getNbNext(); i++){
+ tmp = translateState(ae.getNextElement(i), block);
+ for (AvatarStateMachineElement e: seq){
+ if (e instanceof AvatarStopState){
+ //ignore
+ }
+ else if (e.getNexts().size()==0){
+ e.addNext(tmp.get(0));
+ elementList.add(e);
+ }
+ else if (e.getNext(0) instanceof AvatarStopState){
+ //Remove the transition to AvatarStopState
+ e.removeNext(0);
+ e.addNext(tmp.get(0));
+ elementList.add(e);
+ }
+ else {
+ elementList.add(e);
+ }
+ }
+ //elementList.addAll(tmp);
+ seq = tmp;
+ }
+ //Put stop states on the end of the last in sequence
+
+ for (AvatarStateMachineElement e: seq){
+ if (e.getNexts().size()==0 && !(e instanceof AvatarStopState)){
+ AvatarStopState stop = new AvatarStopState("stop", null);
+ e.addNext(stop);
+ elementList.add(stop);
+ }
+ elementList.add(e);
+ }
+ return elementList;
+
+ }
+ else if (ae instanceof TMLSendRequest){
+ TMLSendRequest sr= (TMLSendRequest) ae;
+ TMLRequest req = sr.getRequest();
+ AvatarSignal sig;
+ if (!signalMap.containsKey(block.getName()+"__"+req.getName())){
+ sig = new AvatarSignal(block.getName()+"__"+req.getName(), AvatarSignal.OUT, req.getReferenceObject());
+ signals.add(sig);
+ signalMap.put(block.getName()+"__"+req.getName(), sig);
+ block.addSignal(sig);
+ }
+ else {
+ sig=signalMap.get(block.getName()+"__"+req.getName());
+ }
+ AvatarActionOnSignal as= new AvatarActionOnSignal(ae.getName(), sig, ae.getReferenceObject());
+ for (int i=0; i<sr.getNbOfParams(); i++){
+ as.addValue(sr.getParam(i));
+ }
+ tran= new AvatarTransition(block, "__after_"+ae.getName(), null);
+ elementList.add(as);
+ as.addNext(tran);
+ elementList.add(tran);
+ }
+ 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){
+ List<AvatarStateMachineElement> set0= translateState(ae.getNextElement(0), block);
+ List<AvatarStateMachineElement> set1 = translateState(ae.getNextElement(1), block);
+// elementList.addAll(set0);
+
+ //Remove stop states of sets and route their transitions to the first element of the following sequence
+ for (AvatarStateMachineElement e: set0){
+ if (e instanceof AvatarStopState){
+ //ignore
+ }
+ else if (e.getNexts().size()==0){
+ e.addNext(set1.get(0));
+ elementList.add(e);
+ }
+ else if (e.getNext(0) instanceof AvatarStopState){
+ //Remove the transition to AvatarStopState
+ e.removeNext(0);
+ e.addNext(set1.get(0));
+ elementList.add(e);
+ }
+ else {
+ elementList.add(e);
+ }
+ }
+
+
+ //Build branch 0
+ tran = new AvatarTransition(block, "__after_"+ae.getName()+"_0", null);
+ choiceState.addNext(tran);
+ elementList.add(tran);
+ tran.addNext(set0.get(0));
+ //Put stop states at the end of set1 if they don't already exist
+ AvatarStopState stop = new AvatarStopState("stop", null);
+ for (AvatarStateMachineElement e: set1){
+ if (e.getNexts().size()==0 && (e instanceof AvatarTransition)){
+ e.addNext(stop);
+ }
+ elementList.add(e);
+ }
+ elementList.add(stop);
+
+ //Build branch 1
+ List<AvatarStateMachineElement> set0_1 = translateState(ae.getNextElement(0), block);
+ List<AvatarStateMachineElement> set1_1 = translateState(ae.getNextElement(1), block);
+ for (AvatarStateMachineElement e: set1_1){
+ if (e instanceof AvatarStopState){
+ //ignore
+ }
+ else if (e.getNexts().size()==0){
+ e.addNext(set0_1.get(0));
+ elementList.add(e);
+ }
+ else if (e.getNext(0) instanceof AvatarStopState){
+ //Remove the transition to AvatarStopState
+ e.removeNext(0);
+ e.addNext(set0_1.get(0));
+ elementList.add(e);
+ }
+ else {
+ elementList.add(e);
+ }
+ }
+ tran = new AvatarTransition(block, "__after_"+ae.getName()+"_1", null);
+ elementList.add(tran);
+ choiceState.addNext(tran);
+ tran.addNext(set1_1.get(0));
+ stop = new AvatarStopState("stop", null);
+ for (AvatarStateMachineElement e: set0_1){
+ if (e.getNexts().size()==0 && (e instanceof AvatarTransition)){
+ e.addNext(stop);
+ }
+ elementList.add(e);
+ }
+ elementList.add(stop);
+
+ }
+ else {
+ //This gets really complicated in ProVerif
+ 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;
+ if (!signalMap.containsKey(block.getName()+"__"+ch.getName())){
+ sig = new AvatarSignal(block.getName()+"__"+ch.getName(), AvatarSignal.OUT, ch.getReferenceObject());
+ signals.add(sig);
+ block.addSignal(sig);
+ signalMap.put(block.getName()+"__"+ch.getName(), sig);
+ }
+ else {
+ sig=signalMap.get(block.getName()+"__"+ch.getName());
+ }
+ 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;
+ if (!signalMap.containsKey(block.getName()+"__"+ch.getName())){
+ sig = new AvatarSignal(block.getName()+"__"+ch.getName(), AvatarSignal.IN, ch.getReferenceObject());
+ signals.add(sig);
+ block.addSignal(sig);
+ signalMap.put(block.getName()+"__"+ch.getName(), sig);
+ }
+ else {
+ sig=signalMap.get(block.getName()+"__"+ch.getName());
+ }
+ 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
+ AvatarRandom as = new AvatarRandom(ae.getName(), ae.getReferenceObject());
+ tran = new AvatarTransition(block, "__after_"+ae.getName(), null);
+ as.setVariable(aee.getVariable());
+ as.setValues("0", Integer.toString(aee.getEvents().size()));
+ 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);
+ 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){
+ if (!signalMap.containsKey(block.getName()+"__"+ch.getName())){
+ sig = new AvatarSignal(block.getName()+"__"+ch.getName(), AvatarSignal.IN, ch.getReferenceObject());
+ signals.add(sig);
+ signalMap.put(block.getName()+"__"+ch.getName(), sig);
+ block.addSignal(sig);
+ AvatarAttribute channelData= new AvatarAttribute(ch.getName()+"__chData", AvatarType.INTEGER, block, null);
+ block.addAttribute(channelData);
+ }
+ else {
+ sig=signalMap.get(block.getName()+"__"+ch.getName());
+ }
+ }
+ else {
+ if (!signalMap.containsKey(block.getName()+"__"+ch.getName())){
+ sig = new AvatarSignal(block.getName()+"__"+ch.getName(), AvatarSignal.OUT, ch.getReferenceObject());
+ signals.add(sig);
+ block.addSignal(sig);
+ signalMap.put(block.getName()+"__"+ch.getName(), sig);
+ AvatarAttribute channelData= new AvatarAttribute(ch.getName()+"__chData", AvatarType.INTEGER, block, null);
+ block.addAttribute(channelData);
+ }
+ else {
+ sig=signalMap.get(block.getName()+"__"+ch.getName());
+ }
+ }
+ AvatarActionOnSignal as = new AvatarActionOnSignal(ae.getName(), sig, ae.getReferenceObject());
+ as.addValue(ch.getName()+"__chData");
+ 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);
+ //AvatarTransition looptran = new AvatarTransition(block, "loop__"+ae.getName(), null);
+ //elementList.addAll(elements);
+ //elementList.add(looptran);
+ //replace stop states and point empty transitions to start of loop
+ for (AvatarStateMachineElement e: elements){
+ if (e instanceof AvatarStopState){
+ }
+ else if (e.getNexts().size()==0){
+ e.addNext(elements.get(0));
+ elementList.add(e);
+ }
+ else if (e.getNext(0) instanceof AvatarStopState){
+ //Remove the transition to AvatarStopState
+ e.removeNext(0);
+ e.addNext(elements.get(0));
+ elementList.add(e);
+ }
+ else {
+ elementList.add(e);
+ }
+ }
+ return elementList;
+ }
+ else {
+ //Make initializaton, then choice state with transitions
+ List<AvatarStateMachineElement> elements=translateState(ae.getNextElement(0), block);
+ List<AvatarStateMachineElement> afterloop = translateState(ae.getNextElement(1), block);
+ AvatarState initState = new AvatarState(ae.getName()+"__init", ae.getReferenceObject(), true);
+ elementList.add(initState);
+ //Build transition to choice
+ tran = new AvatarTransition(block, "loop_init__"+ae.getName(), null);
+ tran.addAction(AvatarTerm.createActionFromString(block, loop.getInit()));
+ elementList.add(tran);
+ initState.addNext(tran);
+ //Choice state
+ AvatarState as = new AvatarState(ae.getName()+"__choice", ae.getReferenceObject(), true);
+ elementList.add(as);
+ tran.addNext(as);
+ //transition to first element of loop
+ tran = new AvatarTransition(block, "loop_increment__"+ae.getName(), null);
+ tran.addGuard(loop.getCondition());
+ tran.addAction(AvatarTerm.createActionFromString(block, loop.getIncrement()));
+ tran.addNext(elements.get(0));
+ as.addNext(tran);
+ elementList.add(tran);
+ //Process elements in loop to remove stop states and empty transitions, and loop back to choice
+ for (AvatarStateMachineElement e: elements){
+ if (e instanceof AvatarStopState){
+ }
+ else if (e.getNexts().size()==0){
+ e.addNext(as);
+ elementList.add(e);
+ }
+ else if (e.getNext(0) instanceof AvatarStopState){
+ //Remove the transition to AvatarStopState
+ e.removeNext(0);
+ e.addNext(as);
+ elementList.add(e);
+ }
+ else {
+ elementList.add(e);
+ }
+ }
+
+ //Transition if exiting loop
+ tran=new AvatarTransition(block, "end_loop__"+ae.getName(), null);
+ tran.addGuard("else");
+ as.addNext(tran);
+ if (afterloop.size()==0){
+ afterloop.add(new AvatarStopState("stop", null));
+ }
+ tran.addNext(afterloop.get(0));
+ elementList.add(tran);
+ elementList.addAll(afterloop);
+ return elementList;
+ }
+ }
+ 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());
+ elementList.add(as);
+ //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.add(tran);
+ 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(){
+ //TODO: Broadcast channels
+ //TODO: Request parameters
+ //TODO:
+ 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());
+ taskBlockMap.put(task, block);
+ 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();
+
+ //what do we do about multiple requests?
+ if (tmlmodel.getRequestToMe(task)!=null){
+ TMLRequest request= tmlmodel.getRequestToMe(task);
+ //Oh this is fun...let's restructure the state machine
+ //Create own start state, and ignore the returned one
+ List<AvatarStateMachineElement> elementList= translateState(task.getActivityDiagram().get(0), block);
+ AvatarStartState ss = new AvatarStartState("start", task.getActivityDiagram().get(0).getReferenceObject());
+ asm.addElement(ss);
+ AvatarTransition at= new AvatarTransition(block, "__after_start", null);
+ ss.addNext(at);
+ asm.addElement(at);
+ AvatarSignal sig = new AvatarSignal(block.getName()+"__"+request.getName(), AvatarSignal.IN, request.getReferenceObject());
+ block.addSignal(sig);
+ signals.add(sig);
+ AvatarActionOnSignal as= new AvatarActionOnSignal("getRequest__"+request.getName(), sig, request.getReferenceObject());
+ at.addNext(as);
+ asm.addElement(as);
+ AvatarTransition tran = new AvatarTransition(block, "__after_" + request.getName(), null);
+ as.addNext(tran);
+ asm.addElement(tran);
+
+ //Find the original start state, transition, and next element
+ AvatarStateMachineElement start = elementList.get(0);
+ AvatarStateMachineElement startTran= start.getNext(0);
+ AvatarStateMachineElement newStart = startTran.getNext(0);
+ tran.addNext(newStart);
+ elementList.remove(start);
+ elementList.remove(startTran);
+ //Find every stop state, remove them, reroute transitions to them
+ for (AvatarStateMachineElement e: elementList){
+ e.setName(processName(e.getName(), e.getID()));
+ if (e instanceof AvatarStopState){
+ //ignore it
+ }
+ else {
+ for (int i=0; i< e.getNexts().size(); i++){
+ if (e.getNext(i) instanceof AvatarStopState){
+ e.removeNext(i);
+ //Route it back to the state with request
+ e.addNext(as);
+ }
+ }
+ asm.addElement(e);
+ }
+ }
+ asm.setStartState((AvatarStartState) ss);
+ }
+ else {
+ List<AvatarStateMachineElement> elementList= translateState(task.getActivityDiagram().get(0), block);
+ for (AvatarStateMachineElement e: elementList){
+ e.setName(processName(e.getName(), e.getID()));
+ asm.addElement(e);
+ }
+ asm.setStartState((AvatarStartState) elementList.get(0));
+ }
+ avspec.addBlock(block);
+ }
+ checkChannels();
+ for (TMLChannel channel:channelMap.keySet()){
+ AvatarRelation ar= new AvatarRelation(channel.getName(), taskBlockMap.get(channel.getOriginTask()), taskBlockMap.get(channel.getDestinationTask()), channel.getReferenceObject());
+ ar.setPrivate(channelMap.get(channel)==1);
+ //Find in signal
+ List<AvatarSignal> sig1 = new ArrayList<AvatarSignal>();
+ List<AvatarSignal> sig2 = new ArrayList<AvatarSignal>();
+ for (AvatarSignal sig: signals){
+ if (sig.getInOut()==AvatarSignal.IN){
+ String name = sig.getName();
+ if (name.equals(channel.getDestinationTask().getName()+"__"+channel.getName())){
+ sig1.add(sig);
+ }
+ }
+ }
+ //Find out signal
+ for (AvatarSignal sig: signals){
+ if (sig.getInOut()==AvatarSignal.OUT){
+ String name = sig.getName();
+ if (name.equals(channel.getOriginTask().getName()+"__"+channel.getName())){
+ sig2.add(sig);
+ }
+ }
+ }
+ if (sig1.size()==0){
+ sig1.add(new AvatarSignal(channel.getDestinationTask().getName()+"__"+channel.getName(), AvatarSignal.IN, null));
+ }
+ if (sig2.size()==0){
+ sig2.add(new AvatarSignal(channel.getOriginTask().getName()+"__"+channel.getName(), AvatarSignal.OUT, null));
+ }
+ if (sig1.size()==1 && sig2.size()==1){
+ ar.addSignals(sig2.get(0), sig1.get(0));
+ }
+ else {
+ //Throw error
+ }
+ avspec.addRelation(ar);
+ }
+ for (TMLRequest request: tmlmodel.getRequests()){
+ AvatarRelation ar = new AvatarRelation(request.getName(), taskBlockMap.get(request.getOriginTasks().get(0)), taskBlockMap.get(request.getDestinationTask()), request.getReferenceObject());
+ ar.setPrivate(false);
+ List<AvatarSignal> sig1 = new ArrayList<AvatarSignal>();
+ List<AvatarSignal> sig2 = new ArrayList<AvatarSignal>();
+ for (AvatarSignal sig: signals){
+ if (sig.getInOut()==AvatarSignal.IN){
+ String name = sig.getName();
+ if (name.equals(request.getDestinationTask().getName()+"__"+request.getName())){
+ sig1.add(sig);
+ }
+ }
+ }
+ //Find out signal
+ for (AvatarSignal sig: signals){
+ if (sig.getInOut()==AvatarSignal.OUT){
+ String name = sig.getName();
+ if (name.equals(request.getOriginTasks().get(0).getName()+"__"+request.getName())){
+ sig2.add(sig);
+ }
+ }
+ }
+ if (sig1.size()==0){
+ sig1.add(new AvatarSignal(request.getDestinationTask().getName()+"__"+request.getName(), AvatarSignal.IN, null));
+ }
+ if (sig2.size()==0){
+ sig2.add(new AvatarSignal(request.getOriginTasks().get(0).getName()+"__"+request.getName(), AvatarSignal.OUT, null));
+ }
+ if (sig1.size()==1 && sig2.size()==1){
+ ar.addSignals(sig2.get(0), sig1.get(0));
+ }
+ else {
+ //Throw error
+ System.out.println("Could not match for " + request.getName());
+ }
+ avspec.addRelation(ar);
+ }
+ for (TMLEvent event: tmlmodel.getEvents()){
+ AvatarRelation ar = new AvatarRelation(event.getName(), taskBlockMap.get(event.getOriginTask()), taskBlockMap.get(event.getDestinationTask()), event.getReferenceObject());
+ ar.setPrivate(false);
+ List<AvatarSignal> sig1 = new ArrayList<AvatarSignal>();
+ List<AvatarSignal> sig2 = new ArrayList<AvatarSignal>();
+ for (AvatarSignal sig: signals){
+ if (sig.getInOut()==AvatarSignal.IN){
+ String name = sig.getName();
+ if (name.equals(event.getDestinationTask().getName()+"__"+event.getName())){
+ sig1.add(sig);
+ }
+ }
+ }
+ //Find out signal
+ for (AvatarSignal sig: signals){
+ if (sig.getInOut()==AvatarSignal.OUT){
+ String name = sig.getName();
+ if (name.equals(event.getOriginTask().getName()+"__"+event.getName())){
+ sig2.add(sig);
+ }
+ }
+ }
+ if (sig1.size()==0){
+ sig1.add(new AvatarSignal(event.getDestinationTask().getName()+"__"+event.getName(), AvatarSignal.IN, null));
+ }
+ if (sig2.size()==0){
+ sig2.add(new AvatarSignal(event.getOriginTask().getName()+"__"+event.getName(), AvatarSignal.OUT, null));
+ }
+ if (sig1.size()==1 && sig2.size()==1){
+ ar.addSignals(sig2.get(0), sig1.get(0));
+ }
+ else {
+ //Throw error
+ System.out.println("Could not match for " + event.getName());
+ }
+ avspec.addRelation(ar);
+ }
+ for (AvatarSignal s: signals){
+
+ System.out.println(s.getName());
+ }
+ for (AvatarRelation ar: avspec.getRelations()){
+ System.out.println(ar.getName());
+ }
+ //Check if we matched up all signals
+ System.out.println(avspec);
+ return avspec;
+ }
+
+}
diff --git a/src/ui/GTMLModeling.java b/src/ui/GTMLModeling.java
index d3a36dccc7d941697c9fab733d8c205c91b2cbbd..2426d6c2023866d191e7a0832bee3c6adeb7e666 100755
--- a/src/ui/GTMLModeling.java
+++ b/src/ui/GTMLModeling.java
@@ -57,6 +57,7 @@ import ui.tmldd.*;
import ui.tmlcp.*;
import ui.tmlsd.*;
import tmltranslator.*;
+import tmltranslator.toavatar.*;
import tmltranslator.tmlcp.*;
import tmltranslator.toproverif.*;
import proverifspec.*;
diff --git a/src/ui/MainGUI.java b/src/ui/MainGUI.java
index 141ffc4356bb9ea5c930f35723ffe373dbaf03b7..590ad4814b29e99ea48ffd13d5500c063fc25916 100755
--- a/src/ui/MainGUI.java
+++ b/src/ui/MainGUI.java
@@ -3752,13 +3752,19 @@ public class MainGUI implements ActionListener, WindowListener, KeyListener, Pe
return;
}
- if (!(tp instanceof AvatarDesignPanel)) {
- return;
+ if (tp instanceof AvatarDesignPanel) {
+ AvatarDesignPanel adp = (AvatarDesignPanel)tp;
+ adp.modelBacktracingProVerif(pvoa);
+ getCurrentTDiagramPanel().repaint();
}
-
- AvatarDesignPanel adp = (AvatarDesignPanel)tp;
- adp.modelBacktracingProVerif(pvoa);
- getCurrentTDiagramPanel().repaint();
+ else if (tp instanceof TMLArchiPanel) {
+ }
+ else if (tp instanceof TMLDesignPanel){
+ TMLDesignPanel tap = (TMLDesignPanel) tp;
+ tap.modelBacktracingProVerif(pvoa);
+ getCurrentTDiagramPanel().repaint();
+ }
+ return;
}
public void modelBacktracingUPPAAL(HashMap<String, Integer> verifMap) {
diff --git a/src/ui/TMLArchiPanel.java b/src/ui/TMLArchiPanel.java
index e51f48d9ee7ba96490b58e65a35fe27f46059671..23a4fff09b280127ccab42a736314bc4169f0f71 100755
--- a/src/ui/TMLArchiPanel.java
+++ b/src/ui/TMLArchiPanel.java
@@ -109,10 +109,9 @@ public class TMLArchiPanel extends TURTLEPanel {
return mgui.getTitleAt(this) + " (DIPLODOCUS Mapping View)";
}
- public void renameMapping(String oldName, String newName) {
- if (tmlap != null) {
- tmlap.renameMapping(oldName, newName);
- }
+ public void renameMapping(String oldName, String newName) {
+ if (tmlap != null) {
+ tmlap.renameMapping(oldName, newName);
}
-
-}
\ No newline at end of file
+ }
+}
diff --git a/src/ui/TMLDesignPanel.java b/src/ui/TMLDesignPanel.java
index cee06f27e9bac8902c046734021ecc64b3dbb044..be277e18b3e84b813644e4e5f9976211130e7ba6 100755
--- a/src/ui/TMLDesignPanel.java
+++ b/src/ui/TMLDesignPanel.java
@@ -54,7 +54,7 @@ import java.util.*;
import ui.tmlcd.*;
import ui.tmlad.*;
import ui.tmldd.*;
-
+import proverifspec.*;
public class TMLDesignPanel extends TURTLEPanel {
public TMLTaskDiagramPanel tmltdp;
public Vector validated, ignored;
@@ -183,5 +183,103 @@ public class TMLDesignPanel extends TURTLEPanel {
}
}
}
-
+ public void modelBacktracingProVerif(ProVerifOutputAnalyzer pvoa) {
+
+ resetModelBacktracingProVerif();
+ TMLActivityDiagramPanel tmladp;
+ for(int i=1; i<panels.size(); i++) {
+ tmladp = (TMLActivityDiagramPanel)(panels.elementAt(i));
+ }
+ String block;
+ String state;
+ int index;
+ ListIterator iterator;
+ // Confidential attributes
+ // LinkedList<AvatarAttribute> secretAttributes = pvoa.getSecretTerms ();
+ // LinkedList<AvatarAttribute> nonSecretAttributes = pvoa.getNonSecretTerms ();
+ // Reachable states
+ for(String s: pvoa.getReachableEvents()) {
+ index = s.indexOf("__");
+ if (index != -1) {
+ block = s.substring(index+2, s.length());
+ index = block.indexOf("__");
+ if (index != -1) {
+ state = block.substring(index+2, block.length());
+ block = block.substring(0, index);
+
+ System.out.println("reachable event "+block+ " "+state);
+ for(int i=0; i<panels.size(); i++) {
+ tdp = (TDiagramPanel)(panels.get(i));
+ if ((tdp instanceof TMLActivityDiagramPanel) && (tdp.getName().compareTo(block) == 0)){
+ iterator = ((TDiagramPanel)(panels.get(i))).getComponentList().listIterator();
+ /* while(iterator.hasNext()) {
+ tgc = (TGComponent)(iterator.next());
+ if (tgc instanceof TMLADChoicee) {
+ ((AvatarSMDState)tgc).setSecurityInfo(AvatarSMDState.REACHABLE, state);
+ }
+ }
+ */
+ }
+ }
+ }
+ }
+ }
+/*
+ for(String s: pvoa.getNonReachableEvents()) {
+ index = s.indexOf("__");
+ if (index != -1) {
+ block = s.substring(index+2, s.length());
+ index = block.indexOf("__");
+ if (index != -1) {
+ state = block.substring(index+2, block.length());
+ block = block.substring(0, index);
+ TraceManager.addDev("Block=" + block + " state=" + state);
+ for(i=0; i<panels.size(); i++) {
+ tdp = (TDiagramPanel)(panels.get(i));
+ if ((tdp instanceof AvatarSMDPanel) && (tdp.getName().compareTo(block) == 0)){
+ iterator = ((TDiagramPanel)(panels.get(i))).getComponentList().listIterator();
+ while(iterator.hasNext()) {
+ tgc = (TGComponent)(iterator.next());
+ if (tgc instanceof AvatarSMDState) {
+ ((AvatarSMDState)tgc).setSecurityInfo(AvatarSMDState.NOT_REACHABLE, state);
+ }
+ }
+ }
+ }
+ }
+ }
+ }
+*/
+ LinkedList<String> notProved = pvoa.getNotProved ();
+ LinkedList<String> satisfied = pvoa.getSatisfiedAuthenticity ();
+ LinkedList<String> satisfiedWeak = pvoa.getSatisfiedWeakAuthenticity ();
+ LinkedList<String> nonSatisfied = pvoa.getNonSatisfiedAuthenticity ();
+ }
+
+
+ public void resetModelBacktracingProVerif() {
+ /*if (abdp == null) {
+ return;
+ }
+
+ // Reset confidential attributes
+ for(AvatarBDBlock block1: abdp.getFullBlockList()) {
+ block1.resetConfidentialityOfAttributes();
+ }
+ for (Object tgc: abdp.getComponentList()){
+ if (tgc instanceof AvatarBDPragma){
+ AvatarBDPragma pragma = (AvatarBDPragma) tgc;
+ pragma.authStrongMap.clear();
+ pragma.authWeakMap.clear();
+
+ }
+ }
+ // Reset reachable states
+ for(int i=0; i<panels.size(); i++) {
+ tdp = (TDiagramPanel)(panels.get(i));
+ if (tdp instanceof AvatarSMDPanel) {
+ ((AvatarSMDPanel)tdp).resetStateSecurityInfo();
+ }
+ }*/
+ }
}
diff --git a/src/ui/tmlad/TMLADChoice.java b/src/ui/tmlad/TMLADChoice.java
index 29d0896a569d486b54852adcbafe504b0d83d217..23a536434a6a3df9c6a06e53131997d9032e4002 100755
--- a/src/ui/tmlad/TMLADChoice.java
+++ b/src/ui/tmlad/TMLADChoice.java
@@ -59,7 +59,12 @@ public class TMLADChoice extends TGCWithInternalComponent implements EmbeddedCom
private int textX1, textY1, textX2, textY2, textX3, textY3;
protected int stateOfError = 0; // Not yet checked
-
+ public final static int NOT_VERIFIED = 0;
+ public final static int REACHABLE = 1;
+ public final static int NOT_REACHABLE = 2;
+
+ public int securityInformation;
+
public TMLADChoice(int _x, int _y, int _minX, int _maxX, int _minY, int _maxY, boolean _pos, TGComponent _father, TDiagramPanel _tdp) {
super(_x, _y, _minX, _maxX, _minY, _maxY, _pos, _father, _tdp);
@@ -164,6 +169,32 @@ public class TMLADChoice extends TGCWithInternalComponent implements EmbeddedCom
}
return "";
}
+ public void drawSecurityInformation(Graphics g) {
+ if (securityInformation > 0) {
+
+ Color c = g.getColor();
+ Color c1;
+ switch(securityInformation) {
+ case REACHABLE:
+ c1 = Color.green;
+ break;
+ case NOT_REACHABLE:
+ c1 = Color.red;
+ break;
+ default:
+ return;
+ }
+
+ GraphicLib.arrowWithLine(g, 1, 0, 10, x-30, y+4, x-15, y+4, true);
+ g.drawOval(x-11, y-3, 7, 9);
+ g.setColor(c1);
+ g.fillRect(x-12, y, 9, 7);
+ g.setColor(c);
+ g.drawRect(x-12, y, 9, 7);
+
+ }
+
+ }
public void setGuard(String guard, int i) {
if ((i>=0) && (i<nbInternalTGComponent)) {