diff --git a/src/main/java/avatartranslator/AvatarBlock.java b/src/main/java/avatartranslator/AvatarBlock.java
index 2f226d8aaefd9765c47332b9bc496c3be8d7ac75..61d46aefc37d8606a6cdecb6da66deaca8b788a8 100644
--- a/src/main/java/avatartranslator/AvatarBlock.java
+++ b/src/main/java/avatartranslator/AvatarBlock.java
@@ -119,6 +119,18 @@ public class AvatarBlock extends AvatarElement implements AvatarStateMachineOwne
signals.add(_signal);
}
+ public AvatarSignal addSignalIfApplicable(String name, int type, Object refObject) {
+ AvatarSignal sig = getSignalByName(name);
+ if (sig != null) {
+ return sig;
+ }
+ sig = new AvatarSignal(name, type, refObject);
+ addSignal(sig);
+ return sig;
+
+ }
+
+
public List<AvatarAttribute> getAttributes() {
return attributes;
}
diff --git a/src/main/java/avatartranslator/AvatarBlockTemplate.java b/src/main/java/avatartranslator/AvatarBlockTemplate.java
index efc00cf934dec8ed842f8179fe96804b968d59f8..8941b57adcdfc04a293074d05f00cc6f04473d90 100644
--- a/src/main/java/avatartranslator/AvatarBlockTemplate.java
+++ b/src/main/java/avatartranslator/AvatarBlockTemplate.java
@@ -146,8 +146,8 @@ public class AvatarBlockTemplate {
}
- // WARNING: Does not handle the non blocking case
- public static AvatarBlock getFifoBlock(String _name, AvatarSpecification _avspec, AvatarRelation _ar, Object _referenceRelation, AvatarSignal _sig1, AvatarSignal _sig2, int _sizeOfFifo, int FIFO_ID) {
+ public static AvatarBlock getFifoBlock(String _name, AvatarSpecification _avspec, AvatarRelation _ar, Object _referenceRelation,
+ AvatarSignal _sig1, AvatarSignal _sig2, int _sizeOfFifo, int FIFO_ID) {
AvatarBlock ab = new AvatarBlock(_name, _avspec, _referenceRelation);
// Create the read and write signals
@@ -308,6 +308,180 @@ public class AvatarBlockTemplate {
return ab;
}
+ // Creates a FIFO with notified
+ public static AvatarBlock getFifoBlockWithNotified(String _name, AvatarSpecification _avspec,
+ AvatarRelation _ar, Object _referenceRelation,
+ AvatarSignal _sig1, AvatarSignal _sig2, AvatarSignal _sig3,
+ int _sizeOfFifo, int FIFO_ID) {
+ AvatarBlock ab = new AvatarBlock(_name, _avspec, _referenceRelation);
+
+ // Create the read and write signals
+ AvatarSignal write = new AvatarSignal("write", AvatarSignal.IN, _referenceRelation);
+ AvatarSignal read = new AvatarSignal("read", AvatarSignal.OUT, _referenceRelation);
+ AvatarSignal notified = new AvatarSignal("notified", AvatarSignal.OUT, _referenceRelation);
+ AvatarAttribute aNotified = new AvatarAttribute("sizeN", AvatarType.INTEGER, null, null);
+ notified.addParameter(aNotified);
+
+ ab.addSignal(write); // corresponds to sig1
+ ab.addSignal(read); // corresponds to sig2
+ ab.addSignal(notified); // corresponds to sig3
+
+ // Creating the attributes of the signals
+ // Same attributes for all signals
+ for (AvatarAttribute aa : _sig1.getListOfAttributes()) {
+ write.addParameter(aa.advancedClone(null));
+ }
+ for (AvatarAttribute aa : _sig2.getListOfAttributes()) {
+ read.addParameter(aa.advancedClone(null));
+ }
+
+
+ // Creating the attributes to support the FIFO
+ // For each parameter, we create an attribute that is similar to the one of e.g. sig1
+ // We duplicate this for the size of the fifo
+ for (AvatarAttribute aa : _sig1.getListOfAttributes()) {
+ for (int i = 0; i < _sizeOfFifo; i++) {
+ AvatarAttribute newA = aa.advancedClone(null);
+ newA.setName("arg__" + aa.getName() + "__" + i);
+ ab.addAttribute(newA);
+ }
+ }
+
+ // If lossy, add corresponding lossy attributes
+ if (_ar.isLossy()) {
+ for (AvatarAttribute aa : _sig1.getListOfAttributes()) {
+ AvatarAttribute newL = aa.advancedClone(null);
+ newL.setName("loss__" + aa.getName());
+ ab.addAttribute(newL);
+ }
+ }
+
+ // If non blocking, then, we need extra attributes
+ if (!(_ar.isBlocking())) {
+ for (AvatarAttribute aa : _sig1.getListOfAttributes()) {
+ AvatarAttribute newL = aa.advancedClone(null);
+ newL.setName("bucket__" + aa.getName());
+ ab.addAttribute(newL);
+ }
+ }
+
+ // We create the attribute to manage the FIFO
+ AvatarAttribute size = new AvatarAttribute("size", AvatarType.INTEGER, ab, _referenceRelation);
+ size.setInitialValue("0");
+ ab.addAttribute(size);
+
+ AvatarAttribute maxSize = new AvatarAttribute("maxSize", AvatarType.INTEGER, ab, _referenceRelation);
+ TraceManager.addDev("*********************************** Size of FIFO=" + _sizeOfFifo);
+ maxSize.setInitialValue("" + _sizeOfFifo);
+ ab.addAttribute(maxSize);
+
+ // Where we write: the head
+ AvatarAttribute head = new AvatarAttribute("head", AvatarType.INTEGER, ab, _referenceRelation);
+ head.setInitialValue("0");
+ ab.addAttribute(head);
+
+ // Where we read: the tail
+ AvatarAttribute tail = new AvatarAttribute("tail", AvatarType.INTEGER, ab, _referenceRelation);
+ tail.setInitialValue("0");
+ ab.addAttribute(tail);
+
+
+ // Creating the state machine
+ // Don't forget the isLossy
+
+ AvatarTransition at;
+ AvatarStateMachine asm = ab.getStateMachine();
+
+ // Start state
+ AvatarStartState ass = new AvatarStartState("start", _referenceRelation);
+ asm.setStartState(ass);
+ asm.addElement(ass);
+
+ // Main state: Wait4Request
+ AvatarState main = new AvatarState("Wait4Request", _referenceRelation);
+ asm.addElement(main);
+ at = makeAvatarEmptyTransitionBetween(ab, asm, ass, main, _referenceRelation);
+
+
+ // Can write only if fifo is not full only if transition
+ AvatarState testHead = new AvatarState("testHead", _referenceRelation);
+ asm.addElement(testHead);
+ at = makeAvatarEmptyTransitionBetween(ab, asm, testHead, main, _referenceRelation);
+ at.setGuard("[head<maxSize]");
+ at = makeAvatarEmptyTransitionBetween(ab, asm, testHead, main, _referenceRelation);
+ at.setGuard("[head==maxSize]");
+ at.addAction("head=0");
+
+ for (int i = 0; i < _sizeOfFifo; i++) {
+ AvatarActionOnSignal aaos_write = new AvatarActionOnSignal("write__" + i, write, _referenceRelation);
+ for (AvatarAttribute aa : _sig1.getListOfAttributes()) {
+ aaos_write.addValue("arg__" + aa.getName() + "__" + i);
+ }
+ asm.addElement(aaos_write);
+ at = makeAvatarEmptyTransitionBetween(ab, asm, main, aaos_write, _referenceRelation);
+ at.setGuard("[(size < maxSize) && (head==" + i + ")]");
+ at = makeAvatarEmptyTransitionBetween(ab, asm, aaos_write, testHead, _referenceRelation);
+ at.addAction("head = head + 1");
+ at.addAction("size = size + 1");
+
+ }
+ // if is lossy, can write, and does not store this nor increase the fifo size
+ if (_ar.isLossy()) {
+ AvatarActionOnSignal aaos_write_loss = new AvatarActionOnSignal("writeloss__", write, _referenceRelation);
+ for (AvatarAttribute aa : _sig1.getListOfAttributes()) {
+ aaos_write_loss.addValue("loss__" + aa.getName());
+ }
+ asm.addElement(aaos_write_loss);
+ at = makeAvatarEmptyTransitionBetween(ab, asm, main, aaos_write_loss, _referenceRelation);
+ at.setGuard("[(size < maxSize)]");
+ at = makeAvatarEmptyTransitionBetween(ab, asm, aaos_write_loss, main, _referenceRelation);
+ }
+
+ // If it is non blocking, then, the new message is written but not added
+ if (!(_ar.isBlocking())) {
+ AvatarActionOnSignal aaos_write_bucket = new AvatarActionOnSignal("writebucket__", write, _referenceRelation);
+ for (AvatarAttribute aa : _sig1.getListOfAttributes()) {
+ aaos_write_bucket.addValue("bucket__" + aa.getName());
+ }
+ asm.addElement(aaos_write_bucket);
+ at = makeAvatarEmptyTransitionBetween(ab, asm, main, aaos_write_bucket, _referenceRelation);
+ at.setGuard("[(size == maxSize)]");
+ at = makeAvatarEmptyTransitionBetween(ab, asm, aaos_write_bucket, main, _referenceRelation);
+ }
+
+ // Read
+ AvatarState testTail = new AvatarState("testTail", _referenceRelation);
+ asm.addElement(testTail);
+ at = makeAvatarEmptyTransitionBetween(ab, asm, testTail, main, _referenceRelation);
+ at.setGuard("[tail<maxSize]");
+ at = makeAvatarEmptyTransitionBetween(ab, asm, testTail, main, _referenceRelation);
+ at.setGuard("[tail==maxSize]");
+ at.addAction("tail=0");
+ for (int i = 0; i < _sizeOfFifo; i++) {
+ AvatarActionOnSignal aaos_read = new AvatarActionOnSignal("read__" + i, read, _referenceRelation);
+ for (AvatarAttribute aa : _sig1.getListOfAttributes()) {
+ aaos_read.addValue("arg__" + aa.getName() + "__" + i);
+ }
+ asm.addElement(aaos_read);
+ at = makeAvatarEmptyTransitionBetween(ab, asm, main, aaos_read, _referenceRelation);
+ at.setGuard("[(size > 0) && (tail==" + i + ")]");
+ at = makeAvatarEmptyTransitionBetween(ab, asm, aaos_read, testTail, _referenceRelation);
+ at.addAction("tail = tail + 1");
+ at.addAction("size = size - 1");
+ }
+
+ // Notified
+ AvatarActionOnSignal aaosNotified = new AvatarActionOnSignal("notified", notified, _referenceRelation);
+ aaosNotified.addValue("size");
+ asm.addElement(aaosNotified);
+ at = makeAvatarEmptyTransitionBetween(ab, asm, main, aaosNotified, _referenceRelation);
+ at = makeAvatarEmptyTransitionBetween(ab, asm, aaosNotified, main, _referenceRelation);
+
+ // Block is finished!
+
+ return ab;
+ }
+
public static AvatarBlock getSWGraphBlock(String _name, AvatarSpecification _avspec, Object _refB,
int duration, Vector<String> unblockedBy, Vector<String> unblockNext) {
diff --git a/src/main/java/tmltranslator/TMLEvent.java b/src/main/java/tmltranslator/TMLEvent.java
index 49ff30cb65abbc605e508c103511b87a816ea5b4..c8535c6cf79994ff7fd26d7d899bca091b017ac7 100755
--- a/src/main/java/tmltranslator/TMLEvent.java
+++ b/src/main/java/tmltranslator/TMLEvent.java
@@ -37,21 +37,21 @@
*/
-
-
package tmltranslator;
import ui.tmlcompd.TMLCPrimitivePort;
-import java.util.*;
-
-import myutil.*;
+import java.util.ArrayList;
+import java.util.HashSet;
+import java.util.List;
+import java.util.Vector;
/**
* Class TMLEvent
* Creation: 22/11/2005
- * @version 1.0 22/11/2005
+ *
* @author Ludovic APVRILLE
+ * @version 1.0 22/11/2005
*/
public class TMLEvent extends TMLCommunicationElement {
// Options
@@ -77,7 +77,6 @@ public class TMLEvent extends TMLCommunicationElement {
public boolean checkConf;
-
public TMLEvent(String name, Object reference, int _maxEvt, boolean _isBlocking) {
super(name, reference);
params = new Vector<TMLType>();
@@ -89,7 +88,7 @@ public class TMLEvent extends TMLCommunicationElement {
originPorts = new ArrayList<TMLPort>();
destinationPorts = new ArrayList<TMLPort>();
ports = new ArrayList<TMLCPrimitivePort>();
- checkConf=false;
+ checkConf = false;
//TraceManager.addDev("New event: " + name + " max=" + _maxEvt + " blocking=" + isBlocking);
}
@@ -97,6 +96,10 @@ public class TMLEvent extends TMLCommunicationElement {
return params.size();
}
+ public Vector <TMLType> getParams() {
+ return params;
+ }
+
public void setSizeFIFO(int _max) {
maxEvt = _max;
checkMaxEvt();
@@ -115,7 +118,6 @@ public class TMLEvent extends TMLCommunicationElement {
}
-
public void setTasks(TMLTask _origin, TMLTask _destination) {
origin = _origin;
destination = _destination;
@@ -132,11 +134,26 @@ public class TMLEvent extends TMLCommunicationElement {
return origin;
}
+
+ public boolean hasOriginTask(TMLTask t) {
+ if (origin == t) {
+ return true;
+ }
+ for (TMLTask task : originTasks) {
+ //TraceManager.addDev("Comparing " + t.getTaskName() + " with " + task.getTaskName());
+ if (task == t) {
+ return true;
+ }
+ }
+
+ return false;
+ }
+
public boolean hasDestinationTask(TMLTask t) {
if (destination == t) {
return true;
}
- for (TMLTask task: destinationTasks) {
+ for (TMLTask task : destinationTasks) {
//TraceManager.addDev("Comparing " + t.getTaskName() + " with " + task.getTaskName());
if (task == t) {
return true;
@@ -206,7 +223,7 @@ public class TMLEvent extends TMLCommunicationElement {
}
public TMLType getType(int i) {
- if (i<getNbOfParams()) {
+ if (i < getNbOfParams()) {
return params.elementAt(i);
} else {
return null;
@@ -233,8 +250,8 @@ public class TMLEvent extends TMLCommunicationElement {
if (_list.length() == 0) {
return true;
}
- String []split = _list.split(",");
- for(int i=0; i<split.length; i++) {
+ String[] split = _list.split(",");
+ for (int i = 0; i < split.length; i++) {
if (!TMLType.isAValidType(split[i])) {
return false;
}
@@ -244,9 +261,9 @@ public class TMLEvent extends TMLCommunicationElement {
public void addParam(String _list) {
- String []split = _list.split(",");
+ String[] split = _list.split(",");
TMLType type;
- for(int i=0; i<split.length; i++) {
+ for (int i = 0; i < split.length; i++) {
if (TMLType.isAValidType(split[i])) {
type = new TMLType(TMLType.getType(split[i]));
addParam(type);
@@ -316,26 +333,26 @@ public class TMLEvent extends TMLCommunicationElement {
public String toXML() {
String s = "<TMLEVENT ";
s += "name=\"" + name + "\" ";
- s += "origintask=\"" + origin.getName() + "\" ";
- if (originPort != null) {
- s += "originport=\"" + originPort.getName() + "\" ";
- }
+ s += "origintask=\"" + origin.getName() + "\" ";
+ if (originPort != null) {
+ s += "originport=\"" + originPort.getName() + "\" ";
+ }
s += "destinationtask=\"" + destination.getName() + "\" ";
- if (destinationPort != null) {
- s += "destinationport=\"" + destinationPort.getName() + "\" ";
- }
- s += "maxEvt=\"" + maxEvt + "\" ";
+ if (destinationPort != null) {
+ s += "destinationport=\"" + destinationPort.getName() + "\" ";
+ }
+ s += "maxEvt=\"" + maxEvt + "\" ";
s += "isBlocking=\"" + isBlocking + "\" ";
- s += "canBeNotified=\"" + canBeNotified + "\" ";
- s += "isLossy=\"" + isLossy + "\" ";
+ s += "canBeNotified=\"" + canBeNotified + "\" ";
+ s += "isLossy=\"" + isLossy + "\" ";
s += "lossPercentage=\"" + lossPercentage + "\" ";
- s += "maxNbOfLoss=\"" + maxNbOfLoss + "\" ";
- s += ">\n";
- for (TMLType t: params) {
- s += "<PARAM type=\"" + t.toString() + "\" />";
- }
+ s += "maxNbOfLoss=\"" + maxNbOfLoss + "\" ";
+ s += ">\n";
+ for (TMLType t : params) {
+ s += "<PARAM type=\"" + t.toString() + "\" />";
+ }
s += "</TMLEVENT>\n";
- return s;
+ return s;
}
public boolean equalSpec(Object o) {
@@ -362,7 +379,7 @@ public class TMLEvent extends TMLCommunicationElement {
if (destination != null) {
if (!destination.equalSpec(event.getDestinationTask())) return false;
}
- if(!(new HashSet<>(params).equals(new HashSet<>(event.params))))
+ if (!(new HashSet<>(params).equals(new HashSet<>(event.params))))
return false;
return maxEvt == event.maxEvt &&
isBlocking == event.isBlocking &&
diff --git a/src/main/java/tmltranslator/TMLType.java b/src/main/java/tmltranslator/TMLType.java
index 4374b0639ee5f65b2cc54855208378d3486a9db8..4aa47a269289291af6fb663f39e4f76b4ff600db 100755
--- a/src/main/java/tmltranslator/TMLType.java
+++ b/src/main/java/tmltranslator/TMLType.java
@@ -142,6 +142,7 @@ public class TMLType {
}
+
public static String getStringType(int type) {
switch(type) {
case NATURAL:
diff --git a/src/main/java/tmltranslator/toavatar/FullTML2Avatar.java b/src/main/java/tmltranslator/toavatar/FullTML2Avatar.java
index 8917beb4fdebbd5d5c7df40c0a0517364bef4cae..a6ed7ed783a67869815f1b4c75a85adc5a65f290 100644
--- a/src/main/java/tmltranslator/toavatar/FullTML2Avatar.java
+++ b/src/main/java/tmltranslator/toavatar/FullTML2Avatar.java
@@ -58,6 +58,10 @@ import java.util.regex.Pattern;
* @version 2.0 19/06/2020
*/
public class FullTML2Avatar {
+ private final static String NOTIFIED = "_NOTIFIED";
+
+
+
//private TMLMapping<?> tmlmap;
private TMLModeling<?> tmlmodel;
@@ -100,808 +104,713 @@ public class FullTML2Avatar {
}
- public List<AvatarStateMachineElement> translateState(TMLActivityElement ae, AvatarBlock block) {
+ public AvatarSpecification generateAvatarSpec(String _loopLimit) {
- // 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;
+ //TraceManager.addDev("security patterns " + tmlmodel.secPatterns);
+ //TraceManager.addDev("keys " + tmlmap.mappedSecurity);
- AvatarTransition tran = new AvatarTransition(block, "", null);
- List<AvatarStateMachineElement> elementList = new ArrayList<AvatarStateMachineElement>();
- if (ae == null) {
- return elementList;
+ //TODO: Make state names readable
+ //TODO: Put back numeric guards
+ //TODO: Calculate for temp variable
+ if (tmlmodel.getTGComponent() != null) {
+ this.avspec = new AvatarSpecification("spec", tmlmodel.getTGComponent().getTDiagramPanel().tp);
+ } else {
+ this.avspec = new AvatarSpecification("spec", null);
}
+ attrsToCheck.clear();
+ tmlmodel.removeForksAndJoins();
- 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(), ss.getReferenceObject());
- 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(), ae.getReferenceObject());
- 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
+// System.out.println("MODIFIED model " + tmlmodel);
- 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;
+ for (TMLChannel chan : tmlmodel.getChannels()) {
+ //System.out.println("chan " + chan);
+ TMLTask task = chan.getOriginTask();
+ TMLTask task2 = chan.getDestinationTask();
- } else if (ae instanceof TMLSendRequest) {
- TMLSendRequest sr = (TMLSendRequest) ae;
- TMLRequest req = sr.getRequest();
- AvatarSignal sig;
- boolean checkAcc = false;
- if (ae.getReferenceObject() != null) {
- checkAcc = ((TGComponent) ae.getReferenceObject()).getCheckableAccessibility();
+ if (chan.getName().contains("fork__") || chan.getName().contains("FORKCHANNEL")) {
+ chan.setName(chan.getName().replaceAll("__", ""));
}
- boolean checked = false;
- if (ae.getReferenceObject() != null) {
- checked = ((TGComponent) ae.getReferenceObject()).hasCheckedAccessibility();
+ }
+
+ //Only set the loop limit if it's a number
+ String pattern = "^[0-9]{1,2}$";
+ Pattern r = Pattern.compile(pattern);
+ Matcher m = r.matcher(_loopLimit);
+ if (m.find()) {
+ loopLimit = Integer.valueOf(_loopLimit);
+ }
+
+ for (TMLChannel channel : tmlmodel.getChannels()) {
+ for (TMLCPrimitivePort p : channel.ports) {
+ channel.checkConf = channel.checkConf || p.checkConf;
+ channel.checkAuth = channel.checkAuth || p.checkAuth;
}
- AvatarState signalState = new AvatarState("signalstate_" + ae.getName().replaceAll(" ", "") + "_" + req.getName().replaceAll(" ", ""), ae.getReferenceObject(), checkAcc, checked);
- AvatarTransition signalTran = new AvatarTransition(block, "__after_signalstate_" + ae.getName() + "_" + req.getName(), ae.getReferenceObject());
- if (!signalOutMap.containsKey(req.getName())) {
- sig = new AvatarSignal(getName(req.getName()), AvatarSignal.OUT, req.getReferenceObject());
- signals.add(sig);
- signalOutMap.put(req.getName(), sig);
- block.addSignal(sig);
- } else {
- sig = signalOutMap.get(req.getName());
+ }
+
+ AvatarBlock top = new AvatarBlock("TOP__TOP", avspec, null);
+ if (mc) {
+ avspec.addBlock(top);
+ AvatarStateMachine topasm = top.getStateMachine();
+ AvatarStartState topss = new AvatarStartState("start", null);
+ topasm.setStartState(topss);
+ topasm.addElement(topss);
+ }
+
+ List<TMLTask> tasks = tmlmodel.getTasks();
+
+ for (TMLTask task : tasks) {
+ AvatarBlock block = new AvatarBlock(task.getName().split("__")[task.getName().split("__").length - 1], avspec, task.getReferenceObject());
+ if (mc) {
+ block.setFather(top);
}
+ taskBlockMap.put(task, block);
+ avspec.addBlock(block);
+ }
+
+ // checkConnections();
+ // checkChannels();
+
+ //distributeKeys();
+
+ //TraceManager.addDev("ALL KEYS " + accessKeys);
+ /*for (TMLTask t: accessKeys.keySet()){
+ TraceManager.addDev("TASK " +t.getName());
+ for (SecurityPattern sp: accessKeys.get(t)){
+ TraceManager.addDev(sp.name);
+ }
+ }*/
+
+ for (TMLTask task : tasks) {
+
+ AvatarBlock block = taskBlockMap.get(task);
+ //Add temp variable for unsendable signals
+
+ //Add all signals
+ for (TMLChannel chan : tmlmodel.getChannels(task)) {
+ if (chan.hasOriginTask(task)) {
+ AvatarSignal sig = new AvatarSignal(chan.getOriginPort().getName(), AvatarSignal.OUT, chan.getReferenceObject());
+
+ block.addSignal(sig);
+ signals.add(sig);
+ AvatarAttribute channelData = new AvatarAttribute(chan.getOriginPort().getName() + "_chData", AvatarType.INTEGER, block, null);
+ if (block.getAvatarAttributeWithName(chan.getOriginPort().getName() + "_chData") == null) {
+ block.addAttribute(channelData);
+ }
+ //sig.addParameter(channelData);
+ signalOutMap.put(chan.getName(), sig);
- AvatarActionOnSignal as = new AvatarActionOnSignal(ae.getName(), sig, ae.getReferenceObject());
- for (int i = 0; i < sr.getNbOfParams(); i++) {
- if (block.getAvatarAttributeWithName(sr.getParam(i)) == null) {
- //Throw Error
- TraceManager.addDev("Missing Attribute " + sr.getParam(i));
- as.addValue("tmp");
- } else {
- // Add parameter to signal and actiononsignal
- sig.addParameter(block.getAvatarAttributeWithName(sr.getParam(i)));
- as.addValue(sr.getParam(i));
}
- }
- /*
- if (req.checkAuth){
- AvatarAttributeState authOrig = new AvatarAttributeState(block.getName()+"."+signalState.getName()+"."+requestData.getName(),ae.getReferenceObject(),requestData, signalState);
- signalAuthOriginMap.put(req.getName(), authOrig);
- }*/
- tran = new AvatarTransition(block, "__after_" + ae.getName(), ae.getReferenceObject());
- elementList.add(signalState);
- signalState.addNext(signalTran);
- elementList.add(signalTran);
- signalTran.addNext(as);
- 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().replaceAll(" ", ""), 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);
+ if (chan.hasDestinationTask(task)) {
- //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);
+ AvatarSignal sig = new AvatarSignal(chan.getDestinationPort().getName(), AvatarSignal.IN, chan.getReferenceObject());
+ block.addSignal(sig);
+ signals.add(sig);
+ signalInMap.put(chan.getName(), sig);
+ AvatarAttribute channelData = new AvatarAttribute(getName(chan.getName()) + "_chData", AvatarType.INTEGER, block, null);
+ if (block.getAvatarAttributeWithName(getName(chan.getName()) + "_chData") == null) {
+ block.addAttribute(channelData);
}
+ //sig.addParameter(channelData);
}
+ }
+ // Add all events
+ for(TMLEvent evt: tmlmodel.getEvents(task)) {
+ TraceManager.addDev("Handling evt: " + evt.getName() + " in task " + task.getName());
+ if (evt.hasOriginTask(task)) {
+ String name = getNameReworked(evt.getName(), 1);
+ TraceManager.addDev("Adding OUT evt:" + name);
+ AvatarSignal sig = block.addSignalIfApplicable(name, AvatarSignal.OUT, evt.getReferenceObject());
+ signalOutMap.put(evt.getName(), sig);
- //Build branch 0
- tran = new AvatarTransition(block, "__after_" + ae.getName() + "_0", ae.getReferenceObject());
- 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);
+ //Adding parameter
+ int cpt = 0;
+ for(TMLType tmlt: evt.getParams()) {
+ AvatarAttribute aa = new AvatarAttribute("p" + cpt, getAvatarType(tmlt), null, null);
+ sig.addParameter(aa);
+ cpt ++;
}
- 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);
+ if (evt.hasDestinationTask(task)) {
+ String name = getNameReworked(evt.getName(), 3);
+ TraceManager.addDev("Adding IN evt:" + name);
+ AvatarSignal sig = block.addSignalIfApplicable(name, AvatarSignal.IN, evt.getReferenceObject());
+ signalInMap.put(evt.getName(), sig);
+
+ //Adding parameter
+ int cpt = 0;
+ for(TMLType tmlt: evt.getParams()) {
+ AvatarAttribute aa = new AvatarAttribute("p" + cpt, getAvatarType(tmlt), null, null);
+ sig.addParameter(aa);
+ cpt ++;
}
+
+ name = getNameReworked(evt.getName(), 3) + NOTIFIED;
+ sig = block.addSignalIfApplicable(name, AvatarSignal.IN, evt.getReferenceObject());
+ signalInMap.put(evt.getName() + NOTIFIED, sig);
+
+ //Adding parameter
+ AvatarAttribute aa = new AvatarAttribute("p" + cpt, AvatarType.INTEGER, null, null);
+ sig.addParameter(aa);
+
}
- tran = new AvatarTransition(block, "__after_" + ae.getName() + "_1", ae.getReferenceObject());
- 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 Avatar...
- 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, ae.getReferenceObject());
- choiceState.addNext(tran);
- elementList.add(tran);
- List<AvatarStateMachineElement> tmp = translateState(ae.getNextElement(i), block);
- AvatarState choiceStateEnd = new AvatarState("seqchoiceend__" + i + "_" + ae.getName().replaceAll(" ", ""), ae.getReferenceObject());
- elementList.add(choiceStateEnd);
- //Remove stop states from the first generated set
- for (AvatarStateMachineElement e : tmp) {
- if (e instanceof AvatarStopState) {
- //ignore
- } else if (e.getNexts().size() == 0) {
- //e.addNext(set1.get(0));
- e.addNext(choiceStateEnd);
- elementList.add(e);
- } else if (e.getNext(0) instanceof AvatarStopState) {
- //Remove the transition to AvatarStopState
- e.removeNext(0);
- e.addNext(choiceStateEnd);
- //e.addNext(set1.get(0));
- elementList.add(e);
- } else {
- elementList.add(e);
- }
- }
+ AvatarAttribute tmp = new AvatarAttribute("tmp", AvatarType.INTEGER, block, null);
+ block.addAttribute(tmp);
+ /* tmp = new AvatarAttribute("aliceandbob", AvatarType.INTEGER, block, null);
+ block.addAttribute(tmp);
+ tmp = new AvatarAttribute("aliceandbob_encrypted", AvatarType.INTEGER, block, null);
+ block.addAttribute(tmp);*/
- tran.addNext(tmp.get(0));
+ AvatarAttribute loop_index = new AvatarAttribute("loop_index", AvatarType.INTEGER, block, null);
+ block.addAttribute(loop_index);
- 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));
- }
- }
+ 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);
+ avattr.setInitialValue(attr.getInitialValue());
+ block.addAttribute(avattr);
+ }
+ //AvatarTransition last;
+ AvatarStateMachine asm = block.getStateMachine();
+ //TODO: Create a fork with many requests. This looks terrible
+ if (tmlmodel.getRequestToMe(task) != null) {
+ //Create iteration attribute
+ AvatarAttribute req_loop_index = new AvatarAttribute("req_loop_index", AvatarType.INTEGER, block, null);
+ block.addAttribute(req_loop_index);
- tran = new AvatarTransition(block, "__after_" + ae.getNextElement(i).getName(), ae.getReferenceObject());
- choiceStateEnd.addNext(tran);
- elementList.add(tran);
+ //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", task.getActivityDiagram().get(0).getReferenceObject());
+ at.addAction(AvatarTerm.createActionFromString(block, "req_loop_index = 0"));
+ ss.addNext(at);
+ asm.addElement(at);
- List<AvatarStateMachineElement> nexts = translateState(newSeq, block);
- elementList.addAll(nexts);
- tran.addNext(nexts.get(0));
+ AvatarState loopstart = new AvatarState("loopstart", task.getActivityDiagram().get(0).getReferenceObject());
+ at.addNext(loopstart);
+ asm.addElement(loopstart);
- }
+ //Find the original start state, transition, and next element
+ AvatarStateMachineElement start = elementList.get(0);
+ AvatarStateMachineElement startTran = start.getNext(0);
+ AvatarStateMachineElement newStart = startTran.getNext(0);
+ elementList.remove(start);
+ elementList.remove(startTran);
+ //Find every stop state, remove them, reroute transitions to them
+ //For now, route every transition to stop state to remove the loop on requests
- }
- return elementList;
+ for (AvatarStateMachineElement e : elementList) {
+ e.setName(processName(e.getName(), e.getID()));
+ stateObjectMap.put(task.getName().split("__")[1] + "__" + e.getName(), e.getReferenceObject());
- } else if (ae instanceof TMLActivityElementEvent) {
- TMLActivityElementEvent aee = (TMLActivityElementEvent) ae;
- TMLEvent evt = aee.getEvent();
- boolean checkAcc = false;
- if (ae.getReferenceObject() != null) {
- checkAcc = ((TGComponent) ae.getReferenceObject()).getCheckableAccessibility();
- }
- boolean checked = false;
- if (ae.getReferenceObject() != null) {
- checked = ((TGComponent) ae.getReferenceObject()).hasCheckedAccessibility();
- }
- AvatarState signalState = new AvatarState("signalstate_" + ae.getName().replaceAll(" ", "") + "_" + evt.getName(), ae.getReferenceObject(), checkAcc, checked);
- AvatarTransition signalTran = new AvatarTransition(block, "__after_signalstate_" + ae.getName() + "_" + evt.getName(), ae.getReferenceObject());
- if (ae instanceof TMLSendEvent) {
- AvatarSignal sig;
- if (!signalOutMap.containsKey(evt.getName())) {
- sig = new AvatarSignal(getName(evt.getName()), AvatarSignal.OUT, evt.getReferenceObject());
- signals.add(sig);
- block.addSignal(sig);
- signalOutMap.put(evt.getName(), sig);
- } else {
- sig = signalOutMap.get(evt.getName());
- }
- AvatarActionOnSignal as = new AvatarActionOnSignal(ae.getName(), sig, ae.getReferenceObject());
- for (int i = 0; i < aee.getNbOfParams(); i++) {
- if (block.getAvatarAttributeWithName(aee.getParam(i)) == null) {
- //Throw Error
- as.addValue("tmp");
- TraceManager.addDev("Missing Attribute " + aee.getParam(i));
+ if (e instanceof AvatarStopState) {
+ //ignore it
} else {
- // Add parameter to signal and actiononsignal
- sig.addParameter(block.getAvatarAttributeWithName(aee.getParam(i)));
- as.addValue(aee.getParam(i));
+ for (int i = 0; i < e.getNexts().size(); i++) {
+ if (e.getNext(i) instanceof AvatarStopState) {
+ e.removeNext(i);
+ //Route it back to the loop start
+ e.addNext(loopstart);
+ }
+ }
+ asm.addElement(e);
}
}
- tran = new AvatarTransition(block, "__after_" + ae.getName(), ae.getReferenceObject());
- elementList.add(signalState);
- signalState.addNext(signalTran);
- elementList.add(signalTran);
- signalTran.addNext(as);
- elementList.add(as);
- as.addNext(tran);
- elementList.add(tran);
+ //Create exit after # of loop iterations is maxed out
+ /*AvatarStopState stop =*/
+ new AvatarStopState("stop", task.getActivityDiagram().get(0).getReferenceObject());
+ /*AvatarTransition exitTran = */
+ new AvatarTransition(block, "to_stop", task.getActivityDiagram().get(0).getReferenceObject());
- } else if (ae instanceof TMLWaitEvent) {
- AvatarSignal sig;
+ //Add Requests, direct transition to start of state machine
+ for (Object obj : tmlmodel.getRequestsToMe(task)) {
+ TMLRequest req = (TMLRequest) obj;
+ AvatarTransition incrTran = new AvatarTransition(block, "__after_loopstart__" + req.getName(), task.getActivityDiagram().get(0).getReferenceObject());
+ incrTran.addAction(AvatarTerm.createActionFromString(block, "req_loop_index = req_loop_index + 1"));
+ incrTran.setGuard(AvatarGuard.createFromString(block, "req_loop_index != " + loopLimit));
+ asm.addElement(incrTran);
+ loopstart.addNext(incrTran);
+ AvatarSignal sig;
+ if (!signalInMap.containsKey(req.getName())) {
+ sig = new AvatarSignal(getName(req.getName()), AvatarSignal.IN, req.getReferenceObject());
+ block.addSignal(sig);
+ signals.add(sig);
+ signalInMap.put(req.getName(), sig);
+ } else {
+ sig = signalInMap.get(req.getName());
+ }
+ AvatarActionOnSignal as = new AvatarActionOnSignal("getRequest__" + req.getName(), sig, req.getReferenceObject());
+ incrTran.addNext(as);
+ asm.addElement(as);
+ /*as.addValue(req.getName()+"__reqData");
+ AvatarAttribute requestData= new AvatarAttribute(req.getName()+"__reqData", AvatarType.INTEGER, block, null);
+ block.addAttribute(requestData);*/
+ for (int i = 0; i < req.getNbOfParams(); i++) {
+ if (block.getAvatarAttributeWithName(req.getParam(i)) == null) {
+ //Throw Error
+ as.addValue("tmp");
+ } else {
+ sig.addParameter(block.getAvatarAttributeWithName(req.getParam(i)));
+ as.addValue(req.getParam(i));
+ }
+ }
+ AvatarTransition tran = new AvatarTransition(block, "__after_" + req.getName(), task.getActivityDiagram().get(0).getReferenceObject());
+ as.addNext(tran);
+ asm.addElement(tran);
+ tran.addNext(newStart);
+ /*if (req.checkAuth){
+ AvatarState afterSignalState = new AvatarState("aftersignalstate_"+req.getName().replaceAll(" ","")+"_"+req.getName().replaceAll(" ",""),req.getReferenceObject());
+ AvatarTransition afterSignalTran = new AvatarTransition(block, "__aftersignalstate_"+req.getName(), req.getReferenceObject());
+ tran.addNext(afterSignalState);
+ afterSignalState.addNext(afterSignalTran);
+ asm.addElement(afterSignalState);
+ asm.addElement(afterSignalTran);
+ afterSignalTran.addNext(newStart);
+ AvatarAttributeState authDest = new AvatarAttributeState(block.getName()+"."+afterSignalState.getName()+"."+requestData.getName(),obj,requestData, afterSignalState);
+ signalAuthDestMap.put(req.getName(), authDest);
+ }
+ else {
+ tran.addNext(newStart);
+ }*/
- if (!signalInMap.containsKey(evt.getName())) {
- sig = new AvatarSignal(getName(evt.getName()), AvatarSignal.IN, evt.getReferenceObject());
- signals.add(sig);
- signalOutMap.put(evt.getName(), sig);
- block.addSignal(sig);
- } else {
- sig = signalInMap.get(evt.getName());
}
- if (sig == null) {
- TraceManager.addDev("NULL evt:" + evt.getName())
-; }
- AvatarActionOnSignal as = new AvatarActionOnSignal(ae.getName(), sig, ae.getReferenceObject());
- for (int i = 0; i < aee.getNbOfParams(); i++) {
-
- if (block.getAvatarAttributeWithName(aee.getParam(i)) == null) {
- //Throw Error
- as.addValue("tmp");
- TraceManager.addDev("Missing Attribute " + aee.getParam(i));
- } else {
- // Add parameter to signal and actiononsignal
- TraceManager.addDev("Param #" + i + ":" + aee.getParam(i));
- AvatarAttribute aa = block.getAvatarAttributeWithName(aee.getParam(i));
- if (aa == null) {
- TraceManager.addDev("NULL Att:");
- }
- sig.addParameter(block.getAvatarAttributeWithName(aee.getParam(i)));
+ asm.setStartState(ss);
+ } else {
+ //Not requested
+ List<AvatarStateMachineElement> elementList = translateState(task.getActivityDiagram().get(0), block);
+ for (AvatarStateMachineElement e : elementList) {
+ e.setName(processName(e.getName(), e.getID()));
+ asm.addElement(e);
+ stateObjectMap.put(task.getName().split("__")[1] + "__" + e.getName(), e.getReferenceObject());
+ }
+ asm.setStartState((AvatarStartState) elementList.get(0));
+ }
+ for (SecurityPattern secPattern : secPatterns) {
+ AvatarAttribute sec = block.getAvatarAttributeWithName(secPattern.name);
+ if (sec != null) {
+ //sec = new AvatarAttribute(secPattern.name, AvatarType.INTEGER, block, null);
+ //AvatarAttribute enc = new AvatarAttribute(secPattern.name+"_encrypted", AvatarType.INTEGER, block, null);
+ // block.addAttribute(sec);
+ // block.addAttribute(enc);
+ //}
+ avspec.addPragma(new AvatarPragmaSecret("#Confidentiality " + block.getName() + "." + secPattern.name, null, sec));
+ }
+ }
+ }
- TraceManager.addDev("Param #" + i + " (1)");
- as.addValue(aee.getParam(i));
- TraceManager.addDev("Param #" + i + " (2)");
- }
- }
- tran = new AvatarTransition(block, "__after_" + ae.getName(), ae.getReferenceObject());
- elementList.add(signalState);
- signalState.addNext(signalTran);
- elementList.add(signalTran);
- signalTran.addNext(as);
- 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(), ae.getReferenceObject());
- as.setVariable(aee.getVariable());
- as.setValues("0", "1");
- as.addNext(tran);
- elementList.add(as);
- elementList.add(tran);
+ //Add authenticity pragmas
+ for (String s : signalAuthOriginMap.keySet()) {
+ if (signalAuthDestMap.containsKey(s)) {
+ AvatarPragmaAuthenticity pragma = new AvatarPragmaAuthenticity("#Authenticity " + signalAuthOriginMap.get(s).getName() + " " + signalAuthDestMap.get(s).getName(), signalAuthOriginMap.get(s).getReferenceObject(), signalAuthOriginMap.get(s), signalAuthDestMap.get(s));
+ if (secChannelMap.containsKey(s)) {
+ for (String channel : secChannelMap.get(s)) {
+ TMLChannel ch = tmlmodel.getChannelByShortName(channel);
+ if (ch != null) {
+ if (ch.checkAuth) {
+ avspec.addPragma(pragma);
+ break;
+ }
+ }
+ }
+
+ } else {
+ avspec.addPragma(pragma);
+ }
}
+ }
- } else if (ae instanceof TMLActivityElementWithAction) {
- //Might be encrypt or decrypt
- AvatarState as = new AvatarState(ae.getValue().replaceAll(" ", "").replaceAll("\\*", "").replaceAll("\\+", "").replaceAll("\\-", "") + "_" + ae.getName().replaceAll(" ", "").replaceAll("\\*", "").replaceAll("\\+", "").replaceAll("\\-", ""), ae.getReferenceObject());
- tran = new AvatarTransition(block, "__after_" + ae.getName(), ae.getReferenceObject());
- as.addNext(tran);
- elementList.add(as);
- elementList.add(tran);
+ //Create relations
+ //Channels are ?? to ??
+ //Requests are n to 1
+ //Events are ?? to ??
+ AvatarBlock fifo = new AvatarBlock("FIFO", avspec, null);
- if (security && ae.securityPattern != null) {
- //If encryption
- if (ae.securityPattern != null && ae.getName().contains("encrypt")) {
- secPatterns.add(ae.securityPattern);
- if (ae.securityPattern.type.equals("Advanced")) {
- //Type Advanced
- tran.addAction(ae.securityPattern.formula);
- } else if (ae.securityPattern.type.equals("Symmetric Encryption")) {
- //Type Symmetric Encryption
- if (!ae.securityPattern.nonce.isEmpty()) {
- //Concatenate nonce to data
+ for (TMLChannel channel : tmlmodel.getChannels()) {
+ // We assume one to one because fork and join have been removed
- //Create concat2 method
- block.addAttribute(new AvatarAttribute(ae.securityPattern.nonce, AvatarType.INTEGER, block, null));
- block.addAttribute(new AvatarAttribute(ae.securityPattern.name, AvatarType.INTEGER, block, null));
+ if (channel.isBasicChannel()) {
+ TraceManager.addDev("checking channel " + channel.getName());
+ AvatarRelation ar = new AvatarRelation(channel.getName(), taskBlockMap.get(channel.getOriginTask()), taskBlockMap.get(channel.getDestinationTask()), channel.getReferenceObject());
- AvatarMethod concat2 = new AvatarMethod("concat2", ae);
- concat2.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
- concat2.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.nonce));
- concat2.addReturnParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
+ if (channel.getType() == TMLChannel.BRBW) {
+ ar.setAsynchronous(true);
+ ar.setSizeOfFIFO(channel.getSize());
+ ar.setBlocking(true);
+ } else if (channel.getType() == TMLChannel.BRNBW) {
+ ar.setAsynchronous(true);
+ ar.setSizeOfFIFO(channel.getSize());
+ ar.setBlocking(false);
+ } else {
+ //Create new block, hope for best
+ if (mc) {
+ fifo = createFifo(channel.getName());
+ ar.setAsynchronous(false);
+ }
+ }
+ //Find in signal
- if (block.getAvatarAttributeWithName(ae.securityPattern.name) != null && block.getAvatarAttributeWithName(ae.securityPattern.nonce) != null) {
- block.addMethod(concat2);
- tran.addAction(ae.securityPattern.name + "=concat2(" + ae.securityPattern.name + "," + ae.securityPattern.nonce + ")");
- }
+ List<AvatarSignal> sig1 = new ArrayList<AvatarSignal>();
+ //Sig1 contains IN Signals, Sig2 contains OUT signals
+ sig1.add(signalInMap.get(channel.getName()));
+ List<AvatarSignal> sig2 = new ArrayList<AvatarSignal>();
+ sig2.add(signalOutMap.get(channel.getName()));
+ for (AvatarSignal sig : signals) {
+ if (sig.getInOut() == AvatarSignal.IN) {
+ String name = sig.getName();
+ if (name.equals(getName(channel.getName()))) {
+ // sig1.add(sig);
}
- if (!ae.securityPattern.key.isEmpty()) {
- //Securing a key
-
- //Create sencrypt method for key
- block.addAttribute(new AvatarAttribute(ae.securityPattern.key, AvatarType.INTEGER, block, null));
- block.addAttribute(new AvatarAttribute("encryptedKey_" + ae.securityPattern.key, AvatarType.INTEGER, block, null));
- block.addAttribute(new AvatarAttribute("key_" + ae.securityPattern.name, AvatarType.INTEGER, block, null));
-
- AvatarMethod sencrypt = new AvatarMethod("sencrypt", ae);
- sencrypt.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.key));
- sencrypt.addParameter(block.getAvatarAttributeWithName("key_" + ae.securityPattern.name));
- sencrypt.addReturnParameter(block.getAvatarAttributeWithName("encryptedKey_" + ae.securityPattern.key));
+ }
+ }
+ //Find out signal
+ for (AvatarSignal sig : signals) {
+ if (sig.getInOut() == AvatarSignal.OUT) {
+ String name = sig.getName();
+ if (name.equals(channel.getOriginPort().getName())) {
+ // sig2.add(sig);
+ }
+ }
+ }
+ TraceManager.addDev("size " + sig1.size() + " " + sig2.size());
- if (block.getAvatarAttributeWithName(ae.securityPattern.key) != null && block.getAvatarAttributeWithName("encryptedKey_" + ae.securityPattern.key) != null && block.getAvatarAttributeWithName("key_" + ae.securityPattern.name) != null) {
- block.addMethod(sencrypt);
- tran.addAction("encryptedKey_" + ae.securityPattern.key + " = sencrypt(key_" + ae.securityPattern.key + ", key_" + ae.securityPattern.name + ")");
- }
- } else {
- //Securing data
+ if (sig1.size() == 0) {
+ sig1.add(new AvatarSignal(getName(channel.getName()), AvatarSignal.IN, null));
+ }
- //Create sencrypt method for data
- block.addAttribute(new AvatarAttribute(ae.securityPattern.name, AvatarType.INTEGER, block, null));
- block.addAttribute(new AvatarAttribute(ae.securityPattern.name + "_encrypted", AvatarType.INTEGER, block, null));
- block.addAttribute(new AvatarAttribute("key_" + ae.securityPattern.name, AvatarType.INTEGER, block, null));
+ if (sig2.size() == 0) {
+ sig2.add(new AvatarSignal(getName(channel.getName()), AvatarSignal.OUT, null));
+ }
- AvatarMethod sencrypt = new AvatarMethod("sencrypt", ae);
- sencrypt.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
- sencrypt.addParameter(block.getAvatarAttributeWithName("key_" + ae.securityPattern.name));
- sencrypt.addReturnParameter(block.getAvatarAttributeWithName(ae.securityPattern.name + "_encrypted"));
+ if (sig1.size() == 1 && sig2.size() == 1) {
+ if (channel.getType() == TMLChannel.NBRNBW && mc) {
+ AvatarSignal read = fifo.getSignalByName("readSignal");
- if (block.getAvatarAttributeWithName(ae.securityPattern.name) != null && block.getAvatarAttributeWithName("key_" + ae.securityPattern.name) != null && block.getAvatarAttributeWithName(ae.securityPattern.name + "_encrypted") != null) {
- block.addMethod(sencrypt);
+ ar.block2 = fifo;
+ //Set IN signal with read
+ ar.addSignals(sig1.get(0), read);
+ AvatarRelation ar2 = new AvatarRelation(channel.getName() + "2", fifo, taskBlockMap.get(channel.getDestinationTask()), channel.getReferenceObject());
+ AvatarSignal write = fifo.getSignalByName("writeSignal");
+ //set OUT signal with write
+ ar2.addSignals(write, sig2.get(0));
+ // System.out.println("Set " + sig2.get(0) + " and write");
+ ar2.setAsynchronous(false);
+ avspec.addRelation(ar2);
+ } else {
+ ar.addSignals(sig2.get(0), sig1.get(0));
+ }
+ } else {
+ //Create relation if it does not exist
+ if (top.getSignalByName(getName(channel.getName()) + "in") == null) {
+ AvatarRelation relation = new AvatarRelation(channel.getName(), top, top, channel.getReferenceObject());
+ AvatarSignal s1 = new AvatarSignal(getName(channel.getName()) + "in", AvatarSignal.IN, null);
+ AvatarSignal s2 = new AvatarSignal(getName(channel.getName()) + "out", AvatarSignal.OUT, null);
+ top.addSignal(s1);
+ top.addSignal(s2);
+ relation.addSignals(s2, s1);
+ avspec.addRelation(relation);
+ // System.out.println("Failure to match signals for TMLChannel "+ channel.getName());
+ }
+ }
+ avspec.addRelation(ar);
+ } else {
+ //System.out.println("WTF Found non-basic channel");
+ //If not a basic channel, create a relation between TOP block and itself
+ AvatarRelation relation = new AvatarRelation(channel.getName(), top, top, channel.getReferenceObject());
+ AvatarSignal s1 = new AvatarSignal(getName(channel.getName()) + "in", AvatarSignal.IN, null);
+ AvatarSignal s2 = new AvatarSignal(getName(channel.getName()) + "out", AvatarSignal.OUT, null);
+ top.addSignal(s1);
+ top.addSignal(s2);
+ relation.addSignals(s2, s1);
+ avspec.addRelation(relation);
+ for (TMLTask t1 : channel.getOriginTasks()) {
+ for (TMLTask t2 : channel.getDestinationTasks()) {
+ AvatarRelation ar = new AvatarRelation(channel.getName(), taskBlockMap.get(t1), taskBlockMap.get(t2), channel.getReferenceObject());
+ ar.setPrivate(originDestMap.get(t1.getName() + "__" + t2.getName()) == 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(getName(channel.getName()))) {
+ sig1.add(sig);
+ }
}
- tran.addAction(ae.securityPattern.name + "_encrypted = sencrypt(" + ae.securityPattern.name + ", key_" + ae.securityPattern.name + ")");
}
- //Set as origin for authenticity
- ae.securityPattern.originTask = block.getName();
- ae.securityPattern.state1 = as;
- } else if (ae.securityPattern.type.equals("Asymmetric Encryption")) {
- if (!ae.securityPattern.nonce.isEmpty()) {
- //Concatenating a nonce
- //Add concat2 method
- block.addAttribute(new AvatarAttribute(ae.securityPattern.nonce, AvatarType.INTEGER, block, null));
- block.addAttribute(new AvatarAttribute(ae.securityPattern.name, AvatarType.INTEGER, block, null));
- AvatarMethod concat2 = new AvatarMethod("concat2", ae);
- concat2.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
- concat2.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.nonce));
- if (block.getAvatarAttributeWithName(ae.securityPattern.name) != null && block.getAvatarAttributeWithName(ae.securityPattern.nonce) != null) {
- block.addMethod(concat2);
- tran.addAction(ae.securityPattern.name + "=concat2(" + ae.securityPattern.name + "," + ae.securityPattern.nonce + ")");
+ //Find out signal
+ for (AvatarSignal sig : signals) {
+ if (sig.getInOut() == AvatarSignal.OUT) {
+ String name = sig.getName();
+ if (name.equals(getName(channel.getName()))) {
+ sig2.add(sig);
+ }
}
}
- //Securing a key instead of data
- if (!ae.securityPattern.key.isEmpty()) {
- //Add aencrypt method
- AvatarMethod aencrypt = new AvatarMethod("aencrypt", ae);
- block.addAttribute(new AvatarAttribute("encryptedKey_" + ae.securityPattern.key, AvatarType.INTEGER, block, null));
- block.addAttribute(new AvatarAttribute("key_" + ae.securityPattern.key, AvatarType.INTEGER, block, null));
- block.addAttribute(new AvatarAttribute("pubKey_" + ae.securityPattern.name, AvatarType.INTEGER, block, null));
- aencrypt.addParameter(block.getAvatarAttributeWithName("key_" + ae.securityPattern.key));
- aencrypt.addParameter(block.getAvatarAttributeWithName("pubKey_" + ae.securityPattern.name));
- aencrypt.addReturnParameter(block.getAvatarAttributeWithName("encryptedKey_" + ae.securityPattern.key));
- if (block.getAvatarAttributeWithName("key_" + ae.securityPattern.key) != null && block.getAvatarAttributeWithName("pubKey_" + ae.securityPattern.name) != null && block.getAvatarAttributeWithName("encryptedKey_" + ae.securityPattern.key) != null) {
- block.addMethod(aencrypt);
- tran.addAction("encryptedKey_" + ae.securityPattern.key + " = aencrypt(key_" + ae.securityPattern.key + ", pubKey_" + ae.securityPattern.name + ")");
- }
+ if (sig1.size() == 0) {
+ sig1.add(new AvatarSignal(getName(channel.getName()), AvatarSignal.IN, null));
+ }
+ if (sig2.size() == 0) {
+ sig2.add(new AvatarSignal(getName(channel.getName()), AvatarSignal.OUT, null));
+ }
+ if (sig1.size() == 1 && sig2.size() == 1) {
+ ar.addSignals(sig2.get(0), sig1.get(0));
} else {
- //Securing data
-
- //Add aencrypt method
- AvatarMethod aencrypt = new AvatarMethod("aencrypt", ae);
- block.addAttribute(new AvatarAttribute(ae.securityPattern.name, AvatarType.INTEGER, block, null));
- block.addAttribute(new AvatarAttribute("pubKey_" + ae.securityPattern.name, AvatarType.INTEGER, block, null));
- block.addAttribute(new AvatarAttribute(ae.securityPattern.name + "_encrypted", AvatarType.INTEGER, block, null));
- aencrypt.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
- aencrypt.addParameter(block.getAvatarAttributeWithName("pubKey_" + ae.securityPattern.name));
- aencrypt.addReturnParameter(block.getAvatarAttributeWithName(ae.securityPattern.name + "_encrypted"));
- if (block.getAvatarAttributeWithName("pubKey_" + ae.securityPattern.name) != null && block.getAvatarAttributeWithName(ae.securityPattern.name) != null && block.getAvatarAttributeWithName(ae.securityPattern.name + "_encrypted") != null) {
- block.addMethod(aencrypt);
- tran.addAction(ae.securityPattern.name + "_encrypted = aencrypt(" + ae.securityPattern.name + ", pubKey_" + ae.securityPattern.name + ")");
- }
- }
- //Set as origin state for authenticity
- ae.securityPattern.originTask = block.getName();
- ae.securityPattern.state1 = as;
- } else if (ae.securityPattern.type.equals("Nonce")) {
- //Do nothing except occupy time to forge nonce
+ System.out.println("Failure to match signals for TMLChannel " + channel.getName() + " between " + t1.getName() + " and " + t2.getName());
+ }
+ avspec.addRelation(ar);
+ }
+ }
+ }
+ }
+ for (TMLRequest request : tmlmodel.getRequests()) {
+ for (TMLTask t1 : request.getOriginTasks()) {
+ AvatarRelation ar = new AvatarRelation(request.getName(), taskBlockMap.get(t1), taskBlockMap.get(request.getDestinationTask()), request.getReferenceObject());
+ ar.setPrivate(originDestMap.get(t1.getName() + "__" + request.getDestinationTask().getName()) == 1);
+ 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();
- //Create a nonce by a random function
- /*AvatarRandom arandom = new AvatarRandom("randomnonce",ae.getReferenceObject());
- arandom.setVariable(ae.securityPattern.name);
- arandom.setValues("0","10");
- elementList.add(arandom);
- tran.addNext(arandom);
- tran = new AvatarTransition(block, "__afterrandom_"+ae.getName(), ae.getReferenceObject());
- arandom.addNext(tran);
- elementList.add(tran);
- block.addAttribute(new AvatarAttribute(ae.securityPattern.name, AvatarType.INTEGER, block, null));*/
- } else if (ae.securityPattern.type.equals("Hash")) {
- AvatarMethod hash = new AvatarMethod("hash", ae);
- hash.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
- if (block.getAvatarAttributeWithName(ae.securityPattern.name) != null) {
- block.addMethod(hash);
+ if (name.equals(getName(request.getName()))) {
+ sig1.add(sig);
}
- tran.addAction(ae.securityPattern.name + "_encrypted = hash(" + ae.securityPattern.name + ")");
- } else if (ae.securityPattern.type.equals("MAC")) {
- block.addAttribute(new AvatarAttribute(ae.securityPattern.name, AvatarType.INTEGER, block, null));
- block.addAttribute(new AvatarAttribute("key_" + ae.securityPattern.name, AvatarType.INTEGER, block, null));
- block.addAttribute(new AvatarAttribute(ae.securityPattern.name + "_encrypted", AvatarType.INTEGER, block, null)); //msg + mac(msg)
- if (!ae.securityPattern.nonce.isEmpty()) {
- //Add nonce
+ }
+ }
+ //Find out signal
+ for (AvatarSignal sig : signals) {
+ if (sig.getInOut() == AvatarSignal.OUT) {
+ String name = sig.getName();
- //Add concat2 method
- AvatarMethod concat = new AvatarMethod("concat2", ae);
- concat.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
- concat.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.nonce));
- concat.addReturnParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
- if (block.getAvatarAttributeWithName(ae.securityPattern.name) != null && block.getAvatarAttributeWithName(ae.securityPattern.nonce) != null) {
- block.addMethod(concat);
- tran.addAction(ae.securityPattern.name + "=concat2(" + ae.securityPattern.name + "," + ae.securityPattern.nonce + ")");
- }
+ if (name.equals(getName(request.getName()))) {
+ sig2.add(sig);
}
+ }
+ }
+ if (sig1.size() == 0) {
+ sig1.add(new AvatarSignal(getName(request.getName()), AvatarSignal.IN, null));
+ }
+ if (sig2.size() == 0) {
+ sig2.add(new AvatarSignal(getName(request.getName()), AvatarSignal.OUT, null));
+ }
+ if (sig1.size() == 1 && sig2.size() == 1) {
+ ar.addSignals(sig2.get(0), sig1.get(0));
+ } else {
+ //Throw error
+ TraceManager.addDev("Could not match for " + request.getName());
+ }
- //Create MAC method
- AvatarMethod mac = new AvatarMethod("MAC", ae);
- AvatarAttribute macattr = new AvatarAttribute(ae.securityPattern.name + "_mac", AvatarType.INTEGER, block, null);
- block.addAttribute(macattr);
+ ar.setAsynchronous(false);
+ avspec.addRelation(ar);
+ }
+ }
+ for (TMLEvent event : tmlmodel.getEvents()) {
- mac.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
- mac.addParameter(block.getAvatarAttributeWithName("key_" + ae.securityPattern.name));
- mac.addReturnParameter(macattr);
+ TraceManager.addDev("Handling Event:" + event.getName() + " 1:" + taskBlockMap.get(event.getOriginTask()) + " 2:" + taskBlockMap.get
+ (event.getDestinationTask()));
- if (block.getAvatarAttributeWithName(ae.securityPattern.name) != null && block.getAvatarAttributeWithName("key_" + ae.securityPattern.name) != null) {
- block.addMethod(mac);
- tran.addAction(ae.securityPattern.name + "_mac = MAC(" + ae.securityPattern.name + ",key_" + ae.securityPattern.name + ")");
- }
+ // For each event, we create a FIFO, and so a double relation
- //Concatenate msg and mac(msg)
- //Create concat2 method
- AvatarMethod concat = new AvatarMethod("concat2", ae);
- concat.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
- concat.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name + "_mac"));
- concat.addReturnParameter(block.getAvatarAttributeWithName(ae.securityPattern.name + "_encrypted"));
- //concat.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.));
- if (block.getAvatarAttributeWithName(ae.securityPattern.name) != null && block.getAvatarAttributeWithName(ae.securityPattern.name + "_encrypted") != null) {
- block.addMethod(concat);
- tran.addAction(ae.securityPattern.name + "_encrypted = concat2(" + ae.securityPattern.name + "," + ae.securityPattern.name + "_mac)");
- }
- ae.securityPattern.originTask = block.getName();
- ae.securityPattern.state1 = as;
- }
- //Set attributestate for authenticity
- if (block.getAvatarAttributeWithName(ae.securityPattern.name) != null) {
- AvatarAttributeState authOrigin = new AvatarAttributeState(block.getName() + "." + as.getName() + "." + ae.securityPattern.name, ae.getReferenceObject(), block.getAvatarAttributeWithName(ae.securityPattern.name), as);
- signalAuthOriginMap.put(ae.securityPattern.name, authOrigin);
- }
- } else if (ae.securityPattern != null && ae.getName().contains("decrypt")) {
- //Decryption action
- //block.addAttribute(new AvatarAttribute(ae.securityPattern.name, AvatarType.INTEGER, block, null));
- //block.addAttribute(new AvatarAttribute(ae.securityPattern.name+"_encrypted", AvatarType.INTEGER, block, null));
- if (ae.securityPattern.type.equals("Symmetric Encryption")) {
- if (!ae.securityPattern.key.isEmpty()) {
- //Decrypting a key
- //Add sdecrypt method
- AvatarMethod sdecrypt = new AvatarMethod("sdecrypt", ae);
- block.addAttribute(new AvatarAttribute("key_" + ae.securityPattern.key, AvatarType.INTEGER, block, null));
- block.addAttribute(new AvatarAttribute("key_" + ae.securityPattern.name, AvatarType.INTEGER, block, null));
- block.addAttribute(new AvatarAttribute("encryptedKey_" + ae.securityPattern.key, AvatarType.INTEGER, block, null));
+ AvatarRelation ar = new AvatarRelation(event.getName(), taskBlockMap.get(event.getOriginTask()), taskBlockMap.get(event.getDestinationTask()),
+ event.getReferenceObject());
+ AvatarSignal sigOut = signalOutMap.get(event.getName());
+ AvatarSignal sigIn = signalInMap.get(event.getName());
+ AvatarSignal sigNotified = signalInMap.get(event.getName() + NOTIFIED);
+ ar.addSignals(sigOut, sigIn);
- sdecrypt.addParameter(block.getAvatarAttributeWithName("encryptedKey_" + ae.securityPattern.key));
- sdecrypt.addParameter(block.getAvatarAttributeWithName("key_" + ae.securityPattern.name));
- sdecrypt.addReturnParameter(block.getAvatarAttributeWithName("key_" + ae.securityPattern.key));
- if (block.getAvatarAttributeWithName("key_" + ae.securityPattern.key) != null && block.getAvatarAttributeWithName("key_" + ae.securityPattern.name) != null && block.getAvatarAttributeWithName("encryptedKey_" + ae.securityPattern.key) != null) {
- block.addMethod(sdecrypt);
- tran.addAction("key_" + ae.securityPattern.key + " = sdecrypt(encryptedKey_" + ae.securityPattern.key + ", key_" + ae.securityPattern.name + ")");
- }
- } else {
- //Decrypting data
- AvatarMethod sdecrypt = new AvatarMethod("sdecrypt", ae);
- block.addAttribute(new AvatarAttribute(ae.securityPattern.name, AvatarType.INTEGER, block, null));
- block.addAttribute(new AvatarAttribute("key_" + ae.securityPattern.name, AvatarType.INTEGER, block, null));
- block.addAttribute(new AvatarAttribute(ae.securityPattern.name + "_encrypted", AvatarType.INTEGER, block, null));
+ AvatarBlock ab0 = taskBlockMap.get(event.getOriginTask());
+ AvatarBlock ab1 = taskBlockMap.get(event.getDestinationTask());
+ //ab0.addSignal(new AvatarSignal(event.getName(), AvatarSignal.OUT, null));
+ //ab1.addSignal(new AvatarSignal(event.getName(), AvatarSignal.IN, null));
- sdecrypt.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name + "_encrypted"));
- sdecrypt.addParameter(block.getAvatarAttributeWithName("key_" + ae.securityPattern.name));
- sdecrypt.addReturnParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
- if (block.getAvatarAttributeWithName(ae.securityPattern.name + "_encrypted") != null && block.getAvatarAttributeWithName("key_" + ae.securityPattern.name) != null && block.getAvatarAttributeWithName(ae.securityPattern.name) != null) {
- block.addMethod(sdecrypt);
- tran.addAction(ae.securityPattern.name + " = sdecrypt(" + ae.securityPattern.name + "_encrypted, key_" + ae.securityPattern.name + ")");
- }
- }
- if (!ae.securityPattern.nonce.isEmpty()) {
- //Separate out the nonce
- block.addAttribute(new AvatarAttribute("testnonce_" + ae.securityPattern.nonce, AvatarType.INTEGER, block, null));
- //Add get2 method
- AvatarMethod get2 = new AvatarMethod("get2", ae);
- get2.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
- get2.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
- get2.addParameter(block.getAvatarAttributeWithName("testnonce_" + ae.securityPattern.nonce));
- if (block.getAvatarAttributeWithName(ae.securityPattern.name) != null && block.getAvatarAttributeWithName("testnonce_" + ae.securityPattern.nonce) != null) {
- block.addMethod(get2);
- tran.addAction("get2(" + ae.securityPattern.name + "," + ae.securityPattern.name + ",testnonce_" + ae.securityPattern.nonce + ")");
- }
+ if (event.isBlocking()) {
+ ar.setAsynchronous(true);
+ ar.setBlocking(true);
+ ar.setSizeOfFIFO(event.getMaxSize());
+ } else {
+ ar.setAsynchronous(true);
+ ar.setBlocking(false);
+ ar.setSizeOfFIFO(event.getMaxSize());
- //Add state after get2 statement
- AvatarState guardState = new AvatarState(ae.getName().replaceAll(" ", "") + "_guarded", ae.getReferenceObject());
- tran.addNext(guardState);
- tran = new AvatarTransition(block, "__guard_" + ae.getName(), ae.getReferenceObject());
- guardState.addNext(tran);
- elementList.add(guardState);
- elementList.add(tran);
+ }
+ //avspec.addRelation(ar);
- //Guard transition to determine if nonce matches
- tran.setGuard("testnonce_" + ae.securityPattern.nonce + "==" + ae.securityPattern.nonce);
- }
- //Add a dummy state afterwards for authenticity after decrypting the data
- AvatarState dummy = new AvatarState(ae.getName().replaceAll(" ", "") + "_dummy", ae.getReferenceObject());
- ae.securityPattern.state2 = dummy;
- tran.addNext(dummy);
- tran = new AvatarTransition(block, "__after_" + ae.getName(), ae.getReferenceObject());
- dummy.addNext(tran);
- elementList.add(dummy);
- elementList.add(tran);
- if (block.getAvatarAttributeWithName(ae.securityPattern.name) != null) {
- AvatarAttributeState authDest = new AvatarAttributeState(block.getName() + "." + dummy.getName() + "." + ae.securityPattern.name, ae.getReferenceObject(), block.getAvatarAttributeWithName(ae.securityPattern.name), dummy);
- signalAuthDestMap.put(ae.securityPattern.name, authDest);
- }
- } else if (ae.securityPattern.type.equals("Asymmetric Encryption")) {
- AvatarMethod adecrypt = new AvatarMethod("adecrypt", ae);
+ AvatarBlock FifoEvt = AvatarBlockTemplate.getFifoBlockWithNotified("Block" + event.getName(),
+ avspec, ar, event.getReferenceObject(), sigOut, sigIn, sigNotified, event.getMaxSize(), event.getID());
+ avspec.addBlock(FifoEvt);
- if (!ae.securityPattern.key.isEmpty()) {
- //Decrypting key
+ ar = new AvatarRelation(event.getName()+"_FIFOIN", taskBlockMap.get(event.getOriginTask()), FifoEvt,
+ event.getReferenceObject());
+ ar.addSignals(sigOut, FifoEvt.getAvatarSignalWithName("write"));
+ avspec.addRelation(ar);
+ ar = new AvatarRelation(event.getName()+"_FIFOIN", FifoEvt, taskBlockMap.get(event.getDestinationTask()),
+ event.getReferenceObject());
+ ar.addSignals(FifoEvt.getAvatarSignalWithName("read"), sigIn);
+ ar.addSignals(FifoEvt.getAvatarSignalWithName("notified"), sigNotified);
+ avspec.addRelation(ar);
- //Add adecrypt method
- block.addAttribute(new AvatarAttribute("encryptedKey_" + ae.securityPattern.key, AvatarType.INTEGER, block, null));
- block.addAttribute(new AvatarAttribute("privKey_" + ae.securityPattern.name, AvatarType.INTEGER, block, null));
- block.addAttribute(new AvatarAttribute("key_" + ae.securityPattern.key, AvatarType.INTEGER, block, null));
- adecrypt.addParameter(block.getAvatarAttributeWithName("encryptedKey_" + ae.securityPattern.key));
- adecrypt.addParameter(block.getAvatarAttributeWithName("privKey_" + ae.securityPattern.name));
- adecrypt.addReturnParameter(block.getAvatarAttributeWithName("key_" + ae.securityPattern.key));
+ }
- if (block.getAvatarAttributeWithName("encryptedKey_" + ae.securityPattern.key) != null && block.getAvatarAttributeWithName("privKey_" + ae.securityPattern.name) != null && block.getAvatarAttributeWithName("key_" + ae.securityPattern.key) != null) {
- block.addMethod(adecrypt);
- tran.addAction("key_" + ae.securityPattern.key + " = adecrypt(encryptedKey_" + ae.securityPattern.key + ", privKey_" + ae.securityPattern.name + ")");
- }
- } else {
- //Decrypting data
+ // System.out.println("Avatar relations " + avspec.getRelations());
- //Add adecrypt method
- block.addAttribute(new AvatarAttribute(ae.securityPattern.name + "_encrypted", AvatarType.INTEGER, block, null));
- block.addAttribute(new AvatarAttribute(ae.securityPattern.name, AvatarType.INTEGER, block, null));
- block.addAttribute(new AvatarAttribute("privKey_" + ae.securityPattern.name, AvatarType.INTEGER, block, null));
+ for (AvatarSignal sig : signals) {
+ // System.out.println("signal " + sig.getName());
+ //check that all signals are put in relations
+ AvatarRelation ar = avspec.getAvatarRelationWithSignal(sig);
+ if (ar == null) {
+ TraceManager.addDev("missing relation for " + sig.getName());
+ }
+ }
+ //Check if we matched up all signals
+ for (SecurityPattern sp : symKeys.keySet()) {
+ if (symKeys.get(sp).size() > 1) {
+ String keys = "";
+ for (AvatarAttribute key : symKeys.get(sp)) {
+ keys = keys + " " + key.getBlock().getName() + "." + key.getName();
+ }
+ avspec.addPragma(new AvatarPragmaInitialKnowledge("#InitialSessionKnowledge " + keys, null, symKeys.get(sp), true));
+ }
+ }
+ for (SecurityPattern sp : pubKeys.keySet()) {
+ if (pubKeys.get(sp).size() != 0) {
+ String keys = "";
+ List<String> pubKeyNames = new ArrayList<String>();
+ for (AvatarAttribute key : pubKeys.get(sp)) {
+ if (!pubKeyNames.contains(key.getBlock().getName() + "." + key.getName())) {
+ keys = keys + " " + key.getBlock().getName() + "." + key.getName();
+ pubKeyNames.add(key.getBlock().getName() + "." + key.getName());
+ }
+ }
+ // avspec.addPragma(new AvatarPragmaInitialKnowledge("#InitialSessionKnowledge "+keys, null, pubKeys.get(sp),true));
+ //System.out.println("pragma " + keys);
+ }
+ }
- adecrypt.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name + "_encrypted"));
- adecrypt.addParameter(block.getAvatarAttributeWithName("privKey_" + ae.securityPattern.name));
- adecrypt.addReturnParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
- if (block.getAvatarAttributeWithName(ae.securityPattern.name + "_encrypted") != null && block.getAvatarAttributeWithName("privKey_" + ae.securityPattern.name) != null && block.getAvatarAttributeWithName(ae.securityPattern.name) != null) {
- block.addMethod(adecrypt);
- tran.addAction(ae.securityPattern.name + " = adecrypt(" + ae.securityPattern.name + "_encrypted, privKey_" + ae.securityPattern.name + ")");
- }
- }
- if (!ae.securityPattern.nonce.isEmpty()) {
- block.addAttribute(new AvatarAttribute("testnonce_" + ae.securityPattern.nonce, AvatarType.INTEGER, block, null));
- AvatarMethod get2 = new AvatarMethod("get2", ae);
- get2.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
- get2.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
- get2.addParameter(block.getAvatarAttributeWithName("testnonce_" + ae.securityPattern.nonce));
- if (block.getAvatarAttributeWithName(ae.securityPattern.name) != null && block.getAvatarAttributeWithName(ae.securityPattern.name) != null) {
- block.addMethod(get2);
- }
+ tmlmodel.secChannelMap = secChannelMap;
- tran.addAction("get2(" + ae.securityPattern.name + "," + ae.securityPattern.name + ",testnonce_" + ae.securityPattern.nonce + ")");
- AvatarState guardState = new AvatarState(ae.getName().replaceAll(" ", "") + "_guarded", ae.getReferenceObject());
- tran.addNext(guardState);
- tran = new AvatarTransition(block, "__guard_" + ae.getName(), ae.getReferenceObject());
- elementList.add(guardState);
- elementList.add(tran);
- guardState.addNext(tran);
- tran.setGuard("testnonce_" + ae.securityPattern.nonce + "==" + ae.securityPattern.nonce);
- }
- AvatarState dummy = new AvatarState(ae.getName().replaceAll(" ", "") + "_dummy", ae.getReferenceObject());
- tran.addNext(dummy);
- tran = new AvatarTransition(block, "__after_" + ae.getName(), ae.getReferenceObject());
- dummy.addNext(tran);
- elementList.add(dummy);
- elementList.add(tran);
- ae.securityPattern.state2 = dummy;
- if (block.getAvatarAttributeWithName(ae.securityPattern.name) != null) {
- AvatarAttributeState authDest = new AvatarAttributeState(block.getName() + "." + dummy.getName() + "." + ae.securityPattern.name, ae.getReferenceObject(), block.getAvatarAttributeWithName(ae.securityPattern.name), dummy);
- signalAuthDestMap.put(ae.securityPattern.name, authDest);
- }
- } else if (ae.securityPattern.type.equals("MAC")) {
- //Separate MAC from MSG
+// System.out.println("avatar spec\n" +avspec);
+ return avspec;
+ }
- //Add get2 method
- AvatarMethod get2 = new AvatarMethod("get2", ae);
- AvatarAttribute mac = new AvatarAttribute(ae.securityPattern.name + "_mac", AvatarType.INTEGER, block, null);
- block.addAttribute(mac);
- block.addAttribute(new AvatarAttribute(ae.securityPattern.name + "_encrypted", AvatarType.INTEGER, block, null));
- block.addAttribute(new AvatarAttribute(ae.securityPattern.name, AvatarType.INTEGER, block, null));
- get2.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name + "_encrypted"));
- get2.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
- get2.addParameter(mac);
- if (block.getAvatarAttributeWithName(ae.securityPattern.name) != null && block.getAvatarAttributeWithName(ae.securityPattern.name + "_encrypted") != null) {
- block.addMethod(get2);
- tran.addAction("get2(" + ae.securityPattern.name + "_encrypted," + ae.securityPattern.name + "," + ae.securityPattern.name + "_mac)");
- }
- //Add verifymac method
- AvatarMethod verifymac = new AvatarMethod("verifyMAC", ae);
- block.addAttribute(new AvatarAttribute("testnonce_" + ae.securityPattern.name, AvatarType.BOOLEAN, block, null));
- verifymac.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
- verifymac.addParameter(block.getAvatarAttributeWithName("key_" + ae.securityPattern.name));
- verifymac.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name + "_mac"));
- verifymac.addReturnParameter(block.getAvatarAttributeWithName("testnonce_" + ae.securityPattern.name));
- if (block.getAvatarAttributeWithName(ae.securityPattern.name) != null && block.getAvatarAttributeWithName("key_" + ae.securityPattern.name) != null) {
- block.addMethod(verifymac);
- tran.addAction("testnonce_" + ae.securityPattern.name + "=verifyMAC(" + ae.securityPattern.name + ", key_" + ae.securityPattern.name + "," + ae.securityPattern.name + "_mac)");
- }
- if (!ae.securityPattern.nonce.isEmpty()) {
- block.addAttribute(new AvatarAttribute("testnonce_" + ae.securityPattern.nonce, AvatarType.INTEGER, block, null));
- tran.addAction("get2(" + ae.securityPattern.name + "," + ae.securityPattern.name + ",testnonce_" + ae.securityPattern.nonce + ")");
- }
- AvatarState guardState = new AvatarState(ae.getName().replaceAll(" ", "") + "_guarded", ae.getReferenceObject());
- tran.addNext(guardState);
- tran = new AvatarTransition(block, "__guard_" + ae.getName(), ae.getReferenceObject());
- elementList.add(guardState);
- elementList.add(tran);
- guardState.addNext(tran);
- tran.setGuard("testnonce_" + ae.securityPattern.name);
- if (!ae.securityPattern.nonce.isEmpty()) {
- //Add extra state and transition
- AvatarState guardState2 = new AvatarState(ae.getName().replaceAll(" ", "") + "_guarded2", ae.getReferenceObject());
- tran.addNext(guardState2);
- tran = new AvatarTransition(block, "__guard_" + ae.getName(), ae.getReferenceObject());
- tran.setGuard("testnonce_" + ae.securityPattern.nonce + "==" + ae.securityPattern.nonce);
- elementList.add(guardState2);
- elementList.add(tran);
+ public List<AvatarStateMachineElement> translateState(TMLActivityElement ae, AvatarBlock block) {
- guardState2.addNext(tran);
- }
- AvatarState dummy = new AvatarState(ae.getName().replaceAll(" ", "") + "_dummy", ae.getReferenceObject());
- ae.securityPattern.state2 = dummy;
- tran.addNext(dummy);
- elementList.add(tran);
- tran = new AvatarTransition(block, "__after_" + ae.getName(), ae.getReferenceObject());
- dummy.addNext(tran);
- elementList.add(dummy);
- elementList.add(tran);
- if (block.getAvatarAttributeWithName(ae.securityPattern.name) != null) {
- AvatarAttributeState authDest = new AvatarAttributeState(block.getName() + "." + dummy.getName() + "." + ae.securityPattern.name, ae.getReferenceObject(), block.getAvatarAttributeWithName(ae.securityPattern.name), dummy);
- signalAuthDestMap.put(ae.securityPattern.name, authDest);
- }
- }
+ AvatarTransition tran = new AvatarTransition(block, "", null);
+ List<AvatarStateMachineElement> elementList = new ArrayList<AvatarStateMachineElement>();
- //Can't decrypt hash or nonce
- }
- } else {
- // See if action.
- if (ae instanceof TMLActionState) {
- String val = ((TMLActionState) ae).getAction();
- tran.addAction(val);
- }
+ if (ae == null) {
+ return elementList;
+ }
- }
- } else if (ae instanceof TMLActivityElementWithIntervalAction) {
- AvatarState as = new AvatarState(ae.getName().replaceAll(" ", ""), ae.getReferenceObject());
+ 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(), ss.getReferenceObject());
+ 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(), ae.getReferenceObject());
- as.addNext(tran);
- elementList.add(as);
+ 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
- } else if (ae instanceof TMLActivityElementChannel) {
- TMLActivityElementChannel aec = (TMLActivityElementChannel) ae;
- TMLChannel ch = aec.getChannel(0);
- AvatarSignal sig;
-
- String nv = getName(ch.getName()) + "_chData";
- block.addIntAttributeIfApplicable(nv);
+ 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;
boolean checkAcc = false;
if (ae.getReferenceObject() != null) {
checkAcc = ((TGComponent) ae.getReferenceObject()).getCheckableAccessibility();
@@ -910,819 +819,941 @@ public class FullTML2Avatar {
if (ae.getReferenceObject() != null) {
checked = ((TGComponent) ae.getReferenceObject()).hasCheckedAccessibility();
}
- AvatarState signalState = new AvatarState("signalstate_" + ae.getName().replaceAll(" ", "") + "_" + ch.getName(), ae.getReferenceObject(), checkAcc, checked);
- AvatarTransition signalTran = new AvatarTransition(block, "__after_signalstate_" + ae.getName() + "_" + ch.getName(), ae.getReferenceObject());
- AvatarTransition signalTranBefore = new AvatarTransition(block, "__before_signalstateint_" + ae.getName() + "_" + ch.getName(), ae
- .getReferenceObject());
- AvatarState signalStateIntermediate = new AvatarState("signalstateinter_" + ae.getName().replaceAll(" ", "") + "_" + ch.getName(), ae
- .getReferenceObject(), checkAcc, checked);
- AvatarTransition signalTranInit = new AvatarTransition(block, "_init_signalstate_" + ae.getName() + "_" + ch.getName(), ae
- .getReferenceObject());
-
- if (ae instanceof TMLReadChannel) {
- //Create signal if it does not already exist
- sig = signalInMap.get(ch.getName());
+ AvatarState signalState = new AvatarState("signalstate_" + ae.getName().replaceAll(" ", "") + "_" + req.getName().replaceAll(" ", ""), ae.getReferenceObject(), checkAcc, checked);
+ AvatarTransition signalTran = new AvatarTransition(block, "__after_signalstate_" + ae.getName() + "_" + req.getName(), ae.getReferenceObject());
+ if (!signalOutMap.containsKey(req.getName())) {
+ sig = new AvatarSignal(getName(req.getName()), AvatarSignal.OUT, req.getReferenceObject());
+ signals.add(sig);
+ signalOutMap.put(req.getName(), sig);
+ block.addSignal(sig);
} else {
- sig = signalOutMap.get(ch.getName());
+ sig = signalOutMap.get(req.getName());
}
AvatarActionOnSignal as = new AvatarActionOnSignal(ae.getName(), sig, ae.getReferenceObject());
+ for (int i = 0; i < sr.getNbOfParams(); i++) {
+ if (block.getAvatarAttributeWithName(sr.getParam(i)) == null) {
+ //Throw Error
+ TraceManager.addDev("Missing Attribute " + sr.getParam(i));
+ as.addValue("tmp");
+ } else {
+ // Add parameter to signal and actiononsignal
+ sig.addParameter(block.getAvatarAttributeWithName(sr.getParam(i)));
+ as.addValue(sr.getParam(i));
+ }
+ }
+ /*
+ if (req.checkAuth){
+ AvatarAttributeState authOrig = new AvatarAttributeState(block.getName()+"."+signalState.getName()+"."+requestData.getName(),ae.getReferenceObject(),requestData, signalState);
+ signalAuthOriginMap.put(req.getName(), authOrig);
+ }*/
tran = new AvatarTransition(block, "__after_" + ae.getName(), ae.getReferenceObject());
-
elementList.add(signalState);
- elementList.add(signalStateIntermediate);
+ signalState.addNext(signalTran);
+ elementList.add(signalTran);
+ signalTran.addNext(as);
elementList.add(as);
+ as.addNext(tran);
elementList.add(tran);
- elementList.add(signalTranInit);
- elementList.add(signalTranBefore);
- elementList.add(signalTran);
- signalState.addNext(signalTranInit);
- signalTranInit.addAction(ch.getName() + "_chData = 0");
- signalTranInit.addNext(signalStateIntermediate);
- signalStateIntermediate.addNext(signalTran);
- signalTran.setGuard(ch.getName() + "_chData < (" + aec.getNbOfSamples() + ")");
- signalTran.addNext(as);
- as.addNext(signalTranBefore);
- signalTranBefore.addAction(ch.getName() + "_chData = " + ch.getName() + "_chData + 1 ");
- signalTranBefore.addNext(signalStateIntermediate);
+ } else if (ae instanceof TMLRandomSequence) {
+ //HashMap<Integer, List<AvatarStateMachineElement>> seqs = new HashMap<Integer, List<AvatarStateMachineElement>>();
+ AvatarState choiceState = new AvatarState("seqchoice__" + ae.getName().replaceAll(" ", ""), 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);
- signalStateIntermediate.addNext(tran);
- tran.setGuard("else");
+ //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);
+ }
+ }
-
- } else if (ae instanceof TMLForLoop) {
- TMLForLoop loop = (TMLForLoop) ae;
- if (loop.isInfinite()) {
- //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().replaceAll(" ", "") + "__init", ae.getReferenceObject());
- elementList.add(initState);
- //Build transition to choice
- tran = new AvatarTransition(block, "loop_init__" + ae.getName(), ae.getReferenceObject());
- tran.addAction("loop_index=0");
- elementList.add(tran);
- initState.addNext(tran);
- //Choice state
- AvatarState as = new AvatarState(ae.getName().replaceAll(" ", "") + "__choice", ae.getReferenceObject());
- elementList.add(as);
- tran.addNext(as);
- //transition to first element of loop
- tran = new AvatarTransition(block, "loop_increment__" + ae.getName(), ae.getReferenceObject());
- //Set default loop limit guard
- tran.setGuard(AvatarGuard.createFromString(block, "loop_index != " + loopLimit));
- //tran.addAction(AvatarTerm.createActionFromString(block, "loop_index = loop_index + 1"));
- tran.addNext(elements.get(0));
- as.addNext(tran);
+ //Build branch 0
+ tran = new AvatarTransition(block, "__after_" + ae.getName() + "_0", ae.getReferenceObject());
+ choiceState.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) {
+ 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) {
- if (e instanceof AvatarTransition) {
- e.addNext(as);
- elementList.add(e);
- }
+ 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(as);
+ e.addNext(set0_1.get(0));
elementList.add(e);
} else {
elementList.add(e);
}
}
-
- //Transition if exiting loop
- tran = new AvatarTransition(block, "end_loop__" + ae.getName(), ae.getReferenceObject());
- tran.setGuard(new AvatarGuardElse());
- as.addNext(tran);
- AvatarStopState stop = new AvatarStopState("stop", null);
- tran.addNext(stop);
+ tran = new AvatarTransition(block, "__after_" + ae.getName() + "_1", ae.getReferenceObject());
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);
- 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().replaceAll(" ", "") + "__init", ae.getReferenceObject());
- elementList.add(initState);
- //Build transition to choice
- tran = new AvatarTransition(block, "loop_init__" + ae.getName(), ae.getReferenceObject());
- tran.addAction(AvatarTerm.createActionFromString(block, loop.getInit()));
- //tran.addAction(AvatarTerm.createActionFromString(block, "loop_index=0"));
- elementList.add(tran);
- initState.addNext(tran);
- //Choice state
- AvatarState as = new AvatarState(ae.getName().replaceAll(" ", "") + "__choice", ae.getReferenceObject());
- elementList.add(as);
- tran.addNext(as);
- //transition to first element of loop
- tran = new AvatarTransition(block, "loop_increment__" + ae.getName(), ae.getReferenceObject());
- //Set default loop limit guard
- tran.setGuard(AvatarGuard.createFromString(block, loop.getCondition()));
- /*AvatarGuard guard = */
- //AvatarGuard.createFromString(block, loop.getCondition());
- tran.addAction(AvatarTerm.createActionFromString(block, loop.getIncrement()));
- //tran.addAction(AvatarTerm.createActionFromString(block, "loop_index = loop_index + 1"));
- if (elements.size() > 0) {
- tran.addNext(elements.get(0));
- as.addNext(tran);
+ //This gets really complicated in Avatar...
+ 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, ae.getReferenceObject());
+ choiceState.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);
+ List<AvatarStateMachineElement> tmp = translateState(ae.getNextElement(i), block);
+
+
+ AvatarState choiceStateEnd = new AvatarState("seqchoiceend__" + i + "_" + ae.getName().replaceAll(" ", ""), ae.getReferenceObject());
+ elementList.add(choiceStateEnd);
+
+
+ //Remove stop states from the first generated set
+ for (AvatarStateMachineElement e : tmp) {
+ if (e instanceof AvatarStopState) {
+ //ignore
+ } else if (e.getNexts().size() == 0) {
+ //e.addNext(set1.get(0));
+ e.addNext(choiceStateEnd);
+ elementList.add(e);
+ } else if (e.getNext(0) instanceof AvatarStopState) {
+ //Remove the transition to AvatarStopState
+ e.removeNext(0);
+ e.addNext(choiceStateEnd);
+ //e.addNext(set1.get(0));
+ elementList.add(e);
+ } else {
+ elementList.add(e);
+ }
}
- }
- //Transition if exiting loop
- tran = new AvatarTransition(block, "end_loop__" + ae.getName(), ae.getReferenceObject());
- tran.setGuard(new AvatarGuardElse());
- 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().replaceAll(" ", ""), ae.getReferenceObject());
- //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, ae.getReferenceObject());
- //tran.setGuard(c.getGuard(i));
- as.addNext(tran);
- List<AvatarStateMachineElement> nexts = translateState(ae.getNextElement(i), block);
- if (nexts.size() > 0) {
- tran.addNext(nexts.get(0));
+ 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(), ae.getReferenceObject());
+ choiceStateEnd.addNext(tran);
elementList.add(tran);
+
+ List<AvatarStateMachineElement> nexts = translateState(newSeq, block);
elementList.addAll(nexts);
+ tran.addNext(nexts.get(0));
+
}
+
}
return elementList;
- } else if (ae instanceof TMLSelectEvt) {
- AvatarState as = new AvatarState(ae.getName().replaceAll(" ", ""), 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, ae.getReferenceObject());
+ } else if (ae instanceof TMLActivityElementEvent) {
+ TMLActivityElementEvent aee = (TMLActivityElementEvent) ae;
+ TMLEvent evt = aee.getEvent();
+ boolean checkAcc = false;
+ if (ae.getReferenceObject() != null) {
+ checkAcc = ((TGComponent) ae.getReferenceObject()).getCheckableAccessibility();
+ }
+ boolean checked = false;
+ if (ae.getReferenceObject() != null) {
+ checked = ((TGComponent) ae.getReferenceObject()).hasCheckedAccessibility();
+ }
+ AvatarState signalState = new AvatarState("signalstate_" + ae.getName().replaceAll(" ", "") + "_" + evt.getName(), ae.getReferenceObject(), checkAcc, checked);
+ AvatarTransition signalTran = new AvatarTransition(block, "__after_signalstate_" + ae.getName() + "_" + evt.getName(), ae.getReferenceObject());
+
+ if (ae instanceof TMLSendEvent) {
+
+ AvatarSignal sig = signalOutMap.get(evt.getName());
+ TraceManager.addDev("sig=" + sig);
+
+ AvatarActionOnSignal as = new AvatarActionOnSignal(ae.getName(), sig, ae.getReferenceObject());
+ for (int i = 0; i < aee.getNbOfParams(); i++) {
+ as.addValue(aee.getParam(i));
+ }
+
+ tran = new AvatarTransition(block, "__after_" + ae.getName(), ae.getReferenceObject());
+ elementList.add(signalState);
+ signalState.addNext(signalTran);
+ elementList.add(signalTran);
+ signalTran.addNext(as);
+ elementList.add(as);
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 {
- TraceManager.addDev("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 AvatarPragma generatePragma(String[] s){
+ } else if (ae instanceof TMLWaitEvent) {
+ TraceManager.addDev("Looking for IN evt: " + evt.getName());
+ AvatarSignal sig = signalInMap.get(evt.getName());
+ TraceManager.addDev("sig=" + sig);
- }*/
+ AvatarActionOnSignal as = new AvatarActionOnSignal(ae.getName(), sig, ae.getReferenceObject());
+ for (int i = 0; i < aee.getNbOfParams(); i++) {
+ as.addValue(aee.getParam(i));
- public String getName(String s) {
- // System.out.println("String " + s);
- if (nameMap.containsKey(s)) {
- return nameMap.get(s);
- } else {
- if (!s.contains("__")) {
- nameMap.put(s, s);
- return s;
- } else if (s.split("__").length == 1) {
- nameMap.put(s, s.split("__")[s.split("__").length - 1]);
- return s.split("__")[s.split("__").length - 1];
- } else if (s.contains("JOIN") || s.contains("FORK")) {
- String t = "";
- t += s.split("__")[0];
- for (int i = 2; i < s.split("__").length; i++) {
- t += "JOIN" + s.split("__")[i];
+ /*if (block.getAvatarAttributeWithName(aee.getParam(i)) == null) {
+ //Throw Error
+ as.addValue("tmp");
+ TraceManager.addDev("Missing Attribute " + aee.getParam(i));
+ } else {
+ // Add parameter to signal and actiononsignal
+ TraceManager.addDev("Param #" + i + ":" + aee.getParam(i));
+ AvatarAttribute aa = block.getAvatarAttributeWithName(aee.getParam(i));
+ if (aa == null) {
+ TraceManager.addDev("NULL Att:");
+ }
+ sig.addParameter(block.getAvatarAttributeWithName(aee.getParam(i)));
+
+
+
+ TraceManager.addDev("Param #" + i + " (1)");
+ as.addValue(aee.getParam(i));
+ TraceManager.addDev("Param #" + i + " (2)");
+ }*/
}
- nameMap.put(s, t);
- return t;
+
+ tran = new AvatarTransition(block, "__after_" + ae.getName(), ae.getReferenceObject());
+ elementList.add(signalState);
+ signalState.addNext(signalTran);
+ elementList.add(signalTran);
+ signalTran.addNext(as);
+ elementList.add(as);
+ as.addNext(tran);
+ elementList.add(tran);
} else {
- /* String t = "";
- for (int i = 0; i < s.split("__").length; i++) {
- t += s.split("__")[i];
- }*/
- nameMap.put(s, s);
- return s;
- // nameMap.put(s, s.split("__")[s.split("__").length - 1]);
- // return s.split("__")[s.split("__").length - 1];
+ //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(), ae.getReferenceObject());
+ as.setVariable(aee.getVariable());
+ as.setValues("0", "1");
+ as.addNext(tran);
+ elementList.add(as);
+ elementList.add(tran);
}
- }
- }
- public AvatarSpecification generateAvatarSpec(String _loopLimit) {
+ } else if (ae instanceof TMLActivityElementWithAction) {
+ //Might be encrypt or decrypt
+ AvatarState as = new AvatarState(ae.getValue().replaceAll(" ", "").replaceAll("\\*", "").replaceAll("\\+", "").replaceAll("\\-", "") + "_" + ae.getName().replaceAll(" ", "").replaceAll("\\*", "").replaceAll("\\+", "").replaceAll("\\-", ""), ae.getReferenceObject());
+ tran = new AvatarTransition(block, "__after_" + ae.getName(), ae.getReferenceObject());
+ as.addNext(tran);
+ elementList.add(as);
+ elementList.add(tran);
- //TraceManager.addDev("security patterns " + tmlmodel.secPatterns);
- //TraceManager.addDev("keys " + tmlmap.mappedSecurity);
+ if (security && ae.securityPattern != null) {
+ //If encryption
+ if (ae.securityPattern != null && ae.getName().contains("encrypt")) {
+ secPatterns.add(ae.securityPattern);
+ if (ae.securityPattern.type.equals("Advanced")) {
+ //Type Advanced
+ tran.addAction(ae.securityPattern.formula);
+ } else if (ae.securityPattern.type.equals("Symmetric Encryption")) {
+ //Type Symmetric Encryption
+ if (!ae.securityPattern.nonce.isEmpty()) {
+ //Concatenate nonce to data
+ //Create concat2 method
+ block.addAttribute(new AvatarAttribute(ae.securityPattern.nonce, AvatarType.INTEGER, block, null));
+ block.addAttribute(new AvatarAttribute(ae.securityPattern.name, AvatarType.INTEGER, block, null));
- //TODO: Make state names readable
- //TODO: Put back numeric guards
- //TODO: Calculate for temp variable
- if (tmlmodel.getTGComponent() != null) {
- this.avspec = new AvatarSpecification("spec", tmlmodel.getTGComponent().getTDiagramPanel().tp);
- } else {
- this.avspec = new AvatarSpecification("spec", null);
- }
- attrsToCheck.clear();
- tmlmodel.removeForksAndJoins();
+ AvatarMethod concat2 = new AvatarMethod("concat2", ae);
+ concat2.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
+ concat2.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.nonce));
+ concat2.addReturnParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
-// System.out.println("MODIFIED model " + tmlmodel);
+ if (block.getAvatarAttributeWithName(ae.securityPattern.name) != null && block.getAvatarAttributeWithName(ae.securityPattern.nonce) != null) {
+ block.addMethod(concat2);
+ tran.addAction(ae.securityPattern.name + "=concat2(" + ae.securityPattern.name + "," + ae.securityPattern.nonce + ")");
+ }
+ }
+ if (!ae.securityPattern.key.isEmpty()) {
+ //Securing a key
- for (TMLChannel chan : tmlmodel.getChannels()) {
- //System.out.println("chan " + chan);
- TMLTask task = chan.getOriginTask();
- TMLTask task2 = chan.getDestinationTask();
+ //Create sencrypt method for key
+ block.addAttribute(new AvatarAttribute(ae.securityPattern.key, AvatarType.INTEGER, block, null));
+ block.addAttribute(new AvatarAttribute("encryptedKey_" + ae.securityPattern.key, AvatarType.INTEGER, block, null));
+ block.addAttribute(new AvatarAttribute("key_" + ae.securityPattern.name, AvatarType.INTEGER, block, null));
- if (chan.getName().contains("fork__") || chan.getName().contains("FORKCHANNEL")) {
- chan.setName(chan.getName().replaceAll("__", ""));
- }
- }
+ AvatarMethod sencrypt = new AvatarMethod("sencrypt", ae);
+ sencrypt.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.key));
+ sencrypt.addParameter(block.getAvatarAttributeWithName("key_" + ae.securityPattern.name));
+ sencrypt.addReturnParameter(block.getAvatarAttributeWithName("encryptedKey_" + ae.securityPattern.key));
- //Only set the loop limit if it's a number
- String pattern = "^[0-9]{1,2}$";
- Pattern r = Pattern.compile(pattern);
- Matcher m = r.matcher(_loopLimit);
- if (m.find()) {
- loopLimit = Integer.valueOf(_loopLimit);
- }
+ if (block.getAvatarAttributeWithName(ae.securityPattern.key) != null && block.getAvatarAttributeWithName("encryptedKey_" + ae.securityPattern.key) != null && block.getAvatarAttributeWithName("key_" + ae.securityPattern.name) != null) {
+ block.addMethod(sencrypt);
+ tran.addAction("encryptedKey_" + ae.securityPattern.key + " = sencrypt(key_" + ae.securityPattern.key + ", key_" + ae.securityPattern.name + ")");
+ }
+ } else {
+ //Securing data
- for (TMLChannel channel : tmlmodel.getChannels()) {
- for (TMLCPrimitivePort p : channel.ports) {
- channel.checkConf = channel.checkConf || p.checkConf;
- channel.checkAuth = channel.checkAuth || p.checkAuth;
- }
- }
+ //Create sencrypt method for data
+ block.addAttribute(new AvatarAttribute(ae.securityPattern.name, AvatarType.INTEGER, block, null));
+ block.addAttribute(new AvatarAttribute(ae.securityPattern.name + "_encrypted", AvatarType.INTEGER, block, null));
+ block.addAttribute(new AvatarAttribute("key_" + ae.securityPattern.name, AvatarType.INTEGER, block, null));
- AvatarBlock top = new AvatarBlock("TOP__TOP", avspec, null);
- if (mc) {
- avspec.addBlock(top);
- AvatarStateMachine topasm = top.getStateMachine();
- AvatarStartState topss = new AvatarStartState("start", null);
- topasm.setStartState(topss);
- topasm.addElement(topss);
- }
+ AvatarMethod sencrypt = new AvatarMethod("sencrypt", ae);
+ sencrypt.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
+ sencrypt.addParameter(block.getAvatarAttributeWithName("key_" + ae.securityPattern.name));
+ sencrypt.addReturnParameter(block.getAvatarAttributeWithName(ae.securityPattern.name + "_encrypted"));
- List<TMLTask> tasks = tmlmodel.getTasks();
+ if (block.getAvatarAttributeWithName(ae.securityPattern.name) != null && block.getAvatarAttributeWithName("key_" + ae.securityPattern.name) != null && block.getAvatarAttributeWithName(ae.securityPattern.name + "_encrypted") != null) {
+ block.addMethod(sencrypt);
+ }
+ tran.addAction(ae.securityPattern.name + "_encrypted = sencrypt(" + ae.securityPattern.name + ", key_" + ae.securityPattern.name + ")");
+ }
+ //Set as origin for authenticity
+ ae.securityPattern.originTask = block.getName();
+ ae.securityPattern.state1 = as;
+ } else if (ae.securityPattern.type.equals("Asymmetric Encryption")) {
+ if (!ae.securityPattern.nonce.isEmpty()) {
+ //Concatenating a nonce
+ //Add concat2 method
+ block.addAttribute(new AvatarAttribute(ae.securityPattern.nonce, AvatarType.INTEGER, block, null));
+ block.addAttribute(new AvatarAttribute(ae.securityPattern.name, AvatarType.INTEGER, block, null));
+ AvatarMethod concat2 = new AvatarMethod("concat2", ae);
+ concat2.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
+ concat2.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.nonce));
+ if (block.getAvatarAttributeWithName(ae.securityPattern.name) != null && block.getAvatarAttributeWithName(ae.securityPattern.nonce) != null) {
+ block.addMethod(concat2);
+ tran.addAction(ae.securityPattern.name + "=concat2(" + ae.securityPattern.name + "," + ae.securityPattern.nonce + ")");
+ }
+ }
+ //Securing a key instead of data
+ if (!ae.securityPattern.key.isEmpty()) {
+ //Add aencrypt method
+ AvatarMethod aencrypt = new AvatarMethod("aencrypt", ae);
+ block.addAttribute(new AvatarAttribute("encryptedKey_" + ae.securityPattern.key, AvatarType.INTEGER, block, null));
+ block.addAttribute(new AvatarAttribute("key_" + ae.securityPattern.key, AvatarType.INTEGER, block, null));
+ block.addAttribute(new AvatarAttribute("pubKey_" + ae.securityPattern.name, AvatarType.INTEGER, block, null));
+ aencrypt.addParameter(block.getAvatarAttributeWithName("key_" + ae.securityPattern.key));
+ aencrypt.addParameter(block.getAvatarAttributeWithName("pubKey_" + ae.securityPattern.name));
+ aencrypt.addReturnParameter(block.getAvatarAttributeWithName("encryptedKey_" + ae.securityPattern.key));
+ if (block.getAvatarAttributeWithName("key_" + ae.securityPattern.key) != null && block.getAvatarAttributeWithName("pubKey_" + ae.securityPattern.name) != null && block.getAvatarAttributeWithName("encryptedKey_" + ae.securityPattern.key) != null) {
+ block.addMethod(aencrypt);
+ tran.addAction("encryptedKey_" + ae.securityPattern.key + " = aencrypt(key_" + ae.securityPattern.key + ", pubKey_" + ae.securityPattern.name + ")");
+ }
+ } else {
+ //Securing data
- for (TMLTask task : tasks) {
- AvatarBlock block = new AvatarBlock(task.getName().split("__")[task.getName().split("__").length - 1], avspec, task.getReferenceObject());
- if (mc) {
- block.setFather(top);
- }
- taskBlockMap.put(task, block);
- avspec.addBlock(block);
- }
+ //Add aencrypt method
+ AvatarMethod aencrypt = new AvatarMethod("aencrypt", ae);
+ block.addAttribute(new AvatarAttribute(ae.securityPattern.name, AvatarType.INTEGER, block, null));
+ block.addAttribute(new AvatarAttribute("pubKey_" + ae.securityPattern.name, AvatarType.INTEGER, block, null));
+ block.addAttribute(new AvatarAttribute(ae.securityPattern.name + "_encrypted", AvatarType.INTEGER, block, null));
+ aencrypt.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
+ aencrypt.addParameter(block.getAvatarAttributeWithName("pubKey_" + ae.securityPattern.name));
+ aencrypt.addReturnParameter(block.getAvatarAttributeWithName(ae.securityPattern.name + "_encrypted"));
+ if (block.getAvatarAttributeWithName("pubKey_" + ae.securityPattern.name) != null && block.getAvatarAttributeWithName(ae.securityPattern.name) != null && block.getAvatarAttributeWithName(ae.securityPattern.name + "_encrypted") != null) {
+ block.addMethod(aencrypt);
+ tran.addAction(ae.securityPattern.name + "_encrypted = aencrypt(" + ae.securityPattern.name + ", pubKey_" + ae.securityPattern.name + ")");
+ }
+ }
+ //Set as origin state for authenticity
+ ae.securityPattern.originTask = block.getName();
+ ae.securityPattern.state1 = as;
+ } else if (ae.securityPattern.type.equals("Nonce")) {
+ //Do nothing except occupy time to forge nonce
- // checkConnections();
- // checkChannels();
- //distributeKeys();
+ //Create a nonce by a random function
+ /*AvatarRandom arandom = new AvatarRandom("randomnonce",ae.getReferenceObject());
+ arandom.setVariable(ae.securityPattern.name);
+ arandom.setValues("0","10");
+ elementList.add(arandom);
+ tran.addNext(arandom);
+ tran = new AvatarTransition(block, "__afterrandom_"+ae.getName(), ae.getReferenceObject());
+ arandom.addNext(tran);
+ elementList.add(tran);
+ block.addAttribute(new AvatarAttribute(ae.securityPattern.name, AvatarType.INTEGER, block, null));*/
+ } else if (ae.securityPattern.type.equals("Hash")) {
+ AvatarMethod hash = new AvatarMethod("hash", ae);
+ hash.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
+ if (block.getAvatarAttributeWithName(ae.securityPattern.name) != null) {
+ block.addMethod(hash);
+ }
+ tran.addAction(ae.securityPattern.name + "_encrypted = hash(" + ae.securityPattern.name + ")");
+ } else if (ae.securityPattern.type.equals("MAC")) {
+ block.addAttribute(new AvatarAttribute(ae.securityPattern.name, AvatarType.INTEGER, block, null));
+ block.addAttribute(new AvatarAttribute("key_" + ae.securityPattern.name, AvatarType.INTEGER, block, null));
+ block.addAttribute(new AvatarAttribute(ae.securityPattern.name + "_encrypted", AvatarType.INTEGER, block, null)); //msg + mac(msg)
+ if (!ae.securityPattern.nonce.isEmpty()) {
+ //Add nonce
- //TraceManager.addDev("ALL KEYS " + accessKeys);
- /*for (TMLTask t: accessKeys.keySet()){
- TraceManager.addDev("TASK " +t.getName());
- for (SecurityPattern sp: accessKeys.get(t)){
- TraceManager.addDev(sp.name);
- }
- }*/
+ //Add concat2 method
+ AvatarMethod concat = new AvatarMethod("concat2", ae);
+ concat.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
+ concat.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.nonce));
+ concat.addReturnParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
+ if (block.getAvatarAttributeWithName(ae.securityPattern.name) != null && block.getAvatarAttributeWithName(ae.securityPattern.nonce) != null) {
+ block.addMethod(concat);
+ tran.addAction(ae.securityPattern.name + "=concat2(" + ae.securityPattern.name + "," + ae.securityPattern.nonce + ")");
+ }
+ }
+
+ //Create MAC method
+ AvatarMethod mac = new AvatarMethod("MAC", ae);
+ AvatarAttribute macattr = new AvatarAttribute(ae.securityPattern.name + "_mac", AvatarType.INTEGER, block, null);
+ block.addAttribute(macattr);
+
+
+ mac.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
+ mac.addParameter(block.getAvatarAttributeWithName("key_" + ae.securityPattern.name));
+ mac.addReturnParameter(macattr);
+
+ if (block.getAvatarAttributeWithName(ae.securityPattern.name) != null && block.getAvatarAttributeWithName("key_" + ae.securityPattern.name) != null) {
+ block.addMethod(mac);
+ tran.addAction(ae.securityPattern.name + "_mac = MAC(" + ae.securityPattern.name + ",key_" + ae.securityPattern.name + ")");
+ }
+
+ //Concatenate msg and mac(msg)
+
+ //Create concat2 method
+ AvatarMethod concat = new AvatarMethod("concat2", ae);
+ concat.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
+ concat.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name + "_mac"));
+ concat.addReturnParameter(block.getAvatarAttributeWithName(ae.securityPattern.name + "_encrypted"));
+ //concat.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.));
+ if (block.getAvatarAttributeWithName(ae.securityPattern.name) != null && block.getAvatarAttributeWithName(ae.securityPattern.name + "_encrypted") != null) {
+ block.addMethod(concat);
+ tran.addAction(ae.securityPattern.name + "_encrypted = concat2(" + ae.securityPattern.name + "," + ae.securityPattern.name + "_mac)");
+ }
+ ae.securityPattern.originTask = block.getName();
+ ae.securityPattern.state1 = as;
+ }
+ //Set attributestate for authenticity
+ if (block.getAvatarAttributeWithName(ae.securityPattern.name) != null) {
+ AvatarAttributeState authOrigin = new AvatarAttributeState(block.getName() + "." + as.getName() + "." + ae.securityPattern.name, ae.getReferenceObject(), block.getAvatarAttributeWithName(ae.securityPattern.name), as);
+ signalAuthOriginMap.put(ae.securityPattern.name, authOrigin);
+ }
+
+ } else if (ae.securityPattern != null && ae.getName().contains("decrypt")) {
+ //Decryption action
+ //block.addAttribute(new AvatarAttribute(ae.securityPattern.name, AvatarType.INTEGER, block, null));
+ //block.addAttribute(new AvatarAttribute(ae.securityPattern.name+"_encrypted", AvatarType.INTEGER, block, null));
+ if (ae.securityPattern.type.equals("Symmetric Encryption")) {
+ if (!ae.securityPattern.key.isEmpty()) {
+ //Decrypting a key
+ //Add sdecrypt method
+ AvatarMethod sdecrypt = new AvatarMethod("sdecrypt", ae);
+ block.addAttribute(new AvatarAttribute("key_" + ae.securityPattern.key, AvatarType.INTEGER, block, null));
+ block.addAttribute(new AvatarAttribute("key_" + ae.securityPattern.name, AvatarType.INTEGER, block, null));
+ block.addAttribute(new AvatarAttribute("encryptedKey_" + ae.securityPattern.key, AvatarType.INTEGER, block, null));
+
+ sdecrypt.addParameter(block.getAvatarAttributeWithName("encryptedKey_" + ae.securityPattern.key));
+ sdecrypt.addParameter(block.getAvatarAttributeWithName("key_" + ae.securityPattern.name));
+ sdecrypt.addReturnParameter(block.getAvatarAttributeWithName("key_" + ae.securityPattern.key));
+ if (block.getAvatarAttributeWithName("key_" + ae.securityPattern.key) != null && block.getAvatarAttributeWithName("key_" + ae.securityPattern.name) != null && block.getAvatarAttributeWithName("encryptedKey_" + ae.securityPattern.key) != null) {
+ block.addMethod(sdecrypt);
+ tran.addAction("key_" + ae.securityPattern.key + " = sdecrypt(encryptedKey_" + ae.securityPattern.key + ", key_" + ae.securityPattern.name + ")");
+ }
+ } else {
+ //Decrypting data
+ AvatarMethod sdecrypt = new AvatarMethod("sdecrypt", ae);
+ block.addAttribute(new AvatarAttribute(ae.securityPattern.name, AvatarType.INTEGER, block, null));
+ block.addAttribute(new AvatarAttribute("key_" + ae.securityPattern.name, AvatarType.INTEGER, block, null));
+ block.addAttribute(new AvatarAttribute(ae.securityPattern.name + "_encrypted", AvatarType.INTEGER, block, null));
+
+ sdecrypt.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name + "_encrypted"));
+ sdecrypt.addParameter(block.getAvatarAttributeWithName("key_" + ae.securityPattern.name));
+ sdecrypt.addReturnParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
+ if (block.getAvatarAttributeWithName(ae.securityPattern.name + "_encrypted") != null && block.getAvatarAttributeWithName("key_" + ae.securityPattern.name) != null && block.getAvatarAttributeWithName(ae.securityPattern.name) != null) {
+ block.addMethod(sdecrypt);
+ tran.addAction(ae.securityPattern.name + " = sdecrypt(" + ae.securityPattern.name + "_encrypted, key_" + ae.securityPattern.name + ")");
+ }
+ }
+ if (!ae.securityPattern.nonce.isEmpty()) {
+ //Separate out the nonce
+ block.addAttribute(new AvatarAttribute("testnonce_" + ae.securityPattern.nonce, AvatarType.INTEGER, block, null));
+ //Add get2 method
+ AvatarMethod get2 = new AvatarMethod("get2", ae);
+ get2.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
+ get2.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
+ get2.addParameter(block.getAvatarAttributeWithName("testnonce_" + ae.securityPattern.nonce));
+ if (block.getAvatarAttributeWithName(ae.securityPattern.name) != null && block.getAvatarAttributeWithName("testnonce_" + ae.securityPattern.nonce) != null) {
+ block.addMethod(get2);
+ tran.addAction("get2(" + ae.securityPattern.name + "," + ae.securityPattern.name + ",testnonce_" + ae.securityPattern.nonce + ")");
+ }
+
+ //Add state after get2 statement
+ AvatarState guardState = new AvatarState(ae.getName().replaceAll(" ", "") + "_guarded", ae.getReferenceObject());
+ tran.addNext(guardState);
+ tran = new AvatarTransition(block, "__guard_" + ae.getName(), ae.getReferenceObject());
+ guardState.addNext(tran);
+ elementList.add(guardState);
+ elementList.add(tran);
+
+ //Guard transition to determine if nonce matches
+ tran.setGuard("testnonce_" + ae.securityPattern.nonce + "==" + ae.securityPattern.nonce);
+ }
+ //Add a dummy state afterwards for authenticity after decrypting the data
+ AvatarState dummy = new AvatarState(ae.getName().replaceAll(" ", "") + "_dummy", ae.getReferenceObject());
+ ae.securityPattern.state2 = dummy;
+ tran.addNext(dummy);
+ tran = new AvatarTransition(block, "__after_" + ae.getName(), ae.getReferenceObject());
+ dummy.addNext(tran);
+ elementList.add(dummy);
+ elementList.add(tran);
+ if (block.getAvatarAttributeWithName(ae.securityPattern.name) != null) {
+ AvatarAttributeState authDest = new AvatarAttributeState(block.getName() + "." + dummy.getName() + "." + ae.securityPattern.name, ae.getReferenceObject(), block.getAvatarAttributeWithName(ae.securityPattern.name), dummy);
+ signalAuthDestMap.put(ae.securityPattern.name, authDest);
+ }
+ } else if (ae.securityPattern.type.equals("Asymmetric Encryption")) {
+ AvatarMethod adecrypt = new AvatarMethod("adecrypt", ae);
- for (TMLTask task : tasks) {
+ if (!ae.securityPattern.key.isEmpty()) {
+ //Decrypting key
- AvatarBlock block = taskBlockMap.get(task);
- //Add temp variable for unsendable signals
- //Add all signals
- for (TMLChannel chan : tmlmodel.getChannels(task)) {
- if (chan.hasOriginTask(task)) {
- AvatarSignal sig = new AvatarSignal(chan.getOriginPort().getName(), AvatarSignal.OUT, chan.getReferenceObject());
+ //Add adecrypt method
+ block.addAttribute(new AvatarAttribute("encryptedKey_" + ae.securityPattern.key, AvatarType.INTEGER, block, null));
+ block.addAttribute(new AvatarAttribute("privKey_" + ae.securityPattern.name, AvatarType.INTEGER, block, null));
+ block.addAttribute(new AvatarAttribute("key_" + ae.securityPattern.key, AvatarType.INTEGER, block, null));
- block.addSignal(sig);
- signals.add(sig);
- AvatarAttribute channelData = new AvatarAttribute(chan.getOriginPort().getName() + "_chData", AvatarType.INTEGER, block, null);
- if (block.getAvatarAttributeWithName(chan.getOriginPort().getName() + "_chData") == null) {
- block.addAttribute(channelData);
- }
- //sig.addParameter(channelData);
- signalOutMap.put(chan.getName(), sig);
+ adecrypt.addParameter(block.getAvatarAttributeWithName("encryptedKey_" + ae.securityPattern.key));
+ adecrypt.addParameter(block.getAvatarAttributeWithName("privKey_" + ae.securityPattern.name));
+ adecrypt.addReturnParameter(block.getAvatarAttributeWithName("key_" + ae.securityPattern.key));
- } else if (chan.hasDestinationTask(task)) {
+ if (block.getAvatarAttributeWithName("encryptedKey_" + ae.securityPattern.key) != null && block.getAvatarAttributeWithName("privKey_" + ae.securityPattern.name) != null && block.getAvatarAttributeWithName("key_" + ae.securityPattern.key) != null) {
+ block.addMethod(adecrypt);
+ tran.addAction("key_" + ae.securityPattern.key + " = adecrypt(encryptedKey_" + ae.securityPattern.key + ", privKey_" + ae.securityPattern.name + ")");
+ }
+ } else {
+ //Decrypting data
- AvatarSignal sig = new AvatarSignal(chan.getDestinationPort().getName(), AvatarSignal.IN, chan.getReferenceObject());
- block.addSignal(sig);
- signals.add(sig);
- signalInMap.put(chan.getName(), sig);
- AvatarAttribute channelData = new AvatarAttribute(getName(chan.getName()) + "_chData", AvatarType.INTEGER, block, null);
- if (block.getAvatarAttributeWithName(getName(chan.getName()) + "_chData") == null) {
- block.addAttribute(channelData);
- }
- //sig.addParameter(channelData);
- }
- }
- AvatarAttribute tmp = new AvatarAttribute("tmp", AvatarType.INTEGER, block, null);
- block.addAttribute(tmp);
+ //Add adecrypt method
+ block.addAttribute(new AvatarAttribute(ae.securityPattern.name + "_encrypted", AvatarType.INTEGER, block, null));
+ block.addAttribute(new AvatarAttribute(ae.securityPattern.name, AvatarType.INTEGER, block, null));
+ block.addAttribute(new AvatarAttribute("privKey_" + ae.securityPattern.name, AvatarType.INTEGER, block, null));
- /* tmp = new AvatarAttribute("aliceandbob", AvatarType.INTEGER, block, null);
- block.addAttribute(tmp);
- tmp = new AvatarAttribute("aliceandbob_encrypted", AvatarType.INTEGER, block, null);
- block.addAttribute(tmp);*/
+ adecrypt.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name + "_encrypted"));
+ adecrypt.addParameter(block.getAvatarAttributeWithName("privKey_" + ae.securityPattern.name));
+ adecrypt.addReturnParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
+ if (block.getAvatarAttributeWithName(ae.securityPattern.name + "_encrypted") != null && block.getAvatarAttributeWithName("privKey_" + ae.securityPattern.name) != null && block.getAvatarAttributeWithName(ae.securityPattern.name) != null) {
+ block.addMethod(adecrypt);
+ tran.addAction(ae.securityPattern.name + " = adecrypt(" + ae.securityPattern.name + "_encrypted, privKey_" + ae.securityPattern.name + ")");
+ }
+ }
+ if (!ae.securityPattern.nonce.isEmpty()) {
+ block.addAttribute(new AvatarAttribute("testnonce_" + ae.securityPattern.nonce, AvatarType.INTEGER, block, null));
+ AvatarMethod get2 = new AvatarMethod("get2", ae);
+ get2.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
+ get2.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
+ get2.addParameter(block.getAvatarAttributeWithName("testnonce_" + ae.securityPattern.nonce));
+ if (block.getAvatarAttributeWithName(ae.securityPattern.name) != null && block.getAvatarAttributeWithName(ae.securityPattern.name) != null) {
+ block.addMethod(get2);
+ }
- AvatarAttribute loop_index = new AvatarAttribute("loop_index", AvatarType.INTEGER, block, null);
- block.addAttribute(loop_index);
+ tran.addAction("get2(" + ae.securityPattern.name + "," + ae.securityPattern.name + ",testnonce_" + ae.securityPattern.nonce + ")");
+ AvatarState guardState = new AvatarState(ae.getName().replaceAll(" ", "") + "_guarded", ae.getReferenceObject());
+ tran.addNext(guardState);
+ tran = new AvatarTransition(block, "__guard_" + ae.getName(), ae.getReferenceObject());
+ elementList.add(guardState);
+ elementList.add(tran);
+ guardState.addNext(tran);
+ tran.setGuard("testnonce_" + ae.securityPattern.nonce + "==" + ae.securityPattern.nonce);
+ }
+ AvatarState dummy = new AvatarState(ae.getName().replaceAll(" ", "") + "_dummy", ae.getReferenceObject());
+ tran.addNext(dummy);
+ tran = new AvatarTransition(block, "__after_" + ae.getName(), ae.getReferenceObject());
+ dummy.addNext(tran);
+ elementList.add(dummy);
+ elementList.add(tran);
+ ae.securityPattern.state2 = dummy;
+ if (block.getAvatarAttributeWithName(ae.securityPattern.name) != null) {
+ AvatarAttributeState authDest = new AvatarAttributeState(block.getName() + "." + dummy.getName() + "." + ae.securityPattern.name, ae.getReferenceObject(), block.getAvatarAttributeWithName(ae.securityPattern.name), dummy);
+ signalAuthDestMap.put(ae.securityPattern.name, authDest);
+ }
+ } else if (ae.securityPattern.type.equals("MAC")) {
+ //Separate MAC from MSG
- 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);
- avattr.setInitialValue(attr.getInitialValue());
- block.addAttribute(avattr);
- }
- //AvatarTransition last;
- AvatarStateMachine asm = block.getStateMachine();
+ //Add get2 method
+ AvatarMethod get2 = new AvatarMethod("get2", ae);
+ AvatarAttribute mac = new AvatarAttribute(ae.securityPattern.name + "_mac", AvatarType.INTEGER, block, null);
+ block.addAttribute(mac);
+ block.addAttribute(new AvatarAttribute(ae.securityPattern.name + "_encrypted", AvatarType.INTEGER, block, null));
+ block.addAttribute(new AvatarAttribute(ae.securityPattern.name, AvatarType.INTEGER, block, null));
- //TODO: Create a fork with many requests. This looks terrible
- if (tmlmodel.getRequestToMe(task) != null) {
- //Create iteration attribute
- AvatarAttribute req_loop_index = new AvatarAttribute("req_loop_index", AvatarType.INTEGER, block, null);
- block.addAttribute(req_loop_index);
+ get2.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name + "_encrypted"));
+ get2.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
+ get2.addParameter(mac);
+ if (block.getAvatarAttributeWithName(ae.securityPattern.name) != null && block.getAvatarAttributeWithName(ae.securityPattern.name + "_encrypted") != null) {
+ block.addMethod(get2);
+ tran.addAction("get2(" + ae.securityPattern.name + "_encrypted," + ae.securityPattern.name + "," + ae.securityPattern.name + "_mac)");
+ }
- //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", task.getActivityDiagram().get(0).getReferenceObject());
- at.addAction(AvatarTerm.createActionFromString(block, "req_loop_index = 0"));
- ss.addNext(at);
- asm.addElement(at);
+ //Add verifymac method
+ AvatarMethod verifymac = new AvatarMethod("verifyMAC", ae);
+ block.addAttribute(new AvatarAttribute("testnonce_" + ae.securityPattern.name, AvatarType.BOOLEAN, block, null));
- AvatarState loopstart = new AvatarState("loopstart", task.getActivityDiagram().get(0).getReferenceObject());
- at.addNext(loopstart);
- asm.addElement(loopstart);
+ verifymac.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
+ verifymac.addParameter(block.getAvatarAttributeWithName("key_" + ae.securityPattern.name));
+ verifymac.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name + "_mac"));
+ verifymac.addReturnParameter(block.getAvatarAttributeWithName("testnonce_" + ae.securityPattern.name));
- //Find the original start state, transition, and next element
- AvatarStateMachineElement start = elementList.get(0);
- AvatarStateMachineElement startTran = start.getNext(0);
- AvatarStateMachineElement newStart = startTran.getNext(0);
- elementList.remove(start);
- elementList.remove(startTran);
- //Find every stop state, remove them, reroute transitions to them
- //For now, route every transition to stop state to remove the loop on requests
+ if (block.getAvatarAttributeWithName(ae.securityPattern.name) != null && block.getAvatarAttributeWithName("key_" + ae.securityPattern.name) != null) {
+ block.addMethod(verifymac);
+ tran.addAction("testnonce_" + ae.securityPattern.name + "=verifyMAC(" + ae.securityPattern.name + ", key_" + ae.securityPattern.name + "," + ae.securityPattern.name + "_mac)");
- for (AvatarStateMachineElement e : elementList) {
- e.setName(processName(e.getName(), e.getID()));
- stateObjectMap.put(task.getName().split("__")[1] + "__" + e.getName(), e.getReferenceObject());
+ }
- 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 loop start
- e.addNext(loopstart);
- }
+
+ if (!ae.securityPattern.nonce.isEmpty()) {
+ block.addAttribute(new AvatarAttribute("testnonce_" + ae.securityPattern.nonce, AvatarType.INTEGER, block, null));
+ tran.addAction("get2(" + ae.securityPattern.name + "," + ae.securityPattern.name + ",testnonce_" + ae.securityPattern.nonce + ")");
}
- asm.addElement(e);
- }
- }
- //Create exit after # of loop iterations is maxed out
- /*AvatarStopState stop =*/
- new AvatarStopState("stop", task.getActivityDiagram().get(0).getReferenceObject());
- /*AvatarTransition exitTran = */
- new AvatarTransition(block, "to_stop", task.getActivityDiagram().get(0).getReferenceObject());
+ AvatarState guardState = new AvatarState(ae.getName().replaceAll(" ", "") + "_guarded", ae.getReferenceObject());
+ tran.addNext(guardState);
+ tran = new AvatarTransition(block, "__guard_" + ae.getName(), ae.getReferenceObject());
+ elementList.add(guardState);
+ elementList.add(tran);
+ guardState.addNext(tran);
+ tran.setGuard("testnonce_" + ae.securityPattern.name);
+ if (!ae.securityPattern.nonce.isEmpty()) {
- //Add Requests, direct transition to start of state machine
- for (Object obj : tmlmodel.getRequestsToMe(task)) {
- TMLRequest req = (TMLRequest) obj;
- AvatarTransition incrTran = new AvatarTransition(block, "__after_loopstart__" + req.getName(), task.getActivityDiagram().get(0).getReferenceObject());
- incrTran.addAction(AvatarTerm.createActionFromString(block, "req_loop_index = req_loop_index + 1"));
- incrTran.setGuard(AvatarGuard.createFromString(block, "req_loop_index != " + loopLimit));
- asm.addElement(incrTran);
- loopstart.addNext(incrTran);
- AvatarSignal sig;
- if (!signalInMap.containsKey(req.getName())) {
- sig = new AvatarSignal(getName(req.getName()), AvatarSignal.IN, req.getReferenceObject());
- block.addSignal(sig);
- signals.add(sig);
- signalInMap.put(req.getName(), sig);
- } else {
- sig = signalInMap.get(req.getName());
- }
- AvatarActionOnSignal as = new AvatarActionOnSignal("getRequest__" + req.getName(), sig, req.getReferenceObject());
- incrTran.addNext(as);
- asm.addElement(as);
- /*as.addValue(req.getName()+"__reqData");
- AvatarAttribute requestData= new AvatarAttribute(req.getName()+"__reqData", AvatarType.INTEGER, block, null);
- block.addAttribute(requestData);*/
- for (int i = 0; i < req.getNbOfParams(); i++) {
- if (block.getAvatarAttributeWithName(req.getParam(i)) == null) {
- //Throw Error
- as.addValue("tmp");
- } else {
- sig.addParameter(block.getAvatarAttributeWithName(req.getParam(i)));
- as.addValue(req.getParam(i));
- }
- }
- AvatarTransition tran = new AvatarTransition(block, "__after_" + req.getName(), task.getActivityDiagram().get(0).getReferenceObject());
- as.addNext(tran);
- asm.addElement(tran);
- tran.addNext(newStart);
- /*if (req.checkAuth){
- AvatarState afterSignalState = new AvatarState("aftersignalstate_"+req.getName().replaceAll(" ","")+"_"+req.getName().replaceAll(" ",""),req.getReferenceObject());
- AvatarTransition afterSignalTran = new AvatarTransition(block, "__aftersignalstate_"+req.getName(), req.getReferenceObject());
- tran.addNext(afterSignalState);
- afterSignalState.addNext(afterSignalTran);
- asm.addElement(afterSignalState);
- asm.addElement(afterSignalTran);
- afterSignalTran.addNext(newStart);
- AvatarAttributeState authDest = new AvatarAttributeState(block.getName()+"."+afterSignalState.getName()+"."+requestData.getName(),obj,requestData, afterSignalState);
- signalAuthDestMap.put(req.getName(), authDest);
- }
- else {
- tran.addNext(newStart);
- }*/
+ //Add extra state and transition
- }
+ AvatarState guardState2 = new AvatarState(ae.getName().replaceAll(" ", "") + "_guarded2", ae.getReferenceObject());
+ tran.addNext(guardState2);
+ tran = new AvatarTransition(block, "__guard_" + ae.getName(), ae.getReferenceObject());
+ tran.setGuard("testnonce_" + ae.securityPattern.nonce + "==" + ae.securityPattern.nonce);
+ elementList.add(guardState2);
+ elementList.add(tran);
+
+ guardState2.addNext(tran);
+ }
+ AvatarState dummy = new AvatarState(ae.getName().replaceAll(" ", "") + "_dummy", ae.getReferenceObject());
+ ae.securityPattern.state2 = dummy;
+ tran.addNext(dummy);
+ elementList.add(tran);
+ tran = new AvatarTransition(block, "__after_" + ae.getName(), ae.getReferenceObject());
+ dummy.addNext(tran);
+ elementList.add(dummy);
+ elementList.add(tran);
+ if (block.getAvatarAttributeWithName(ae.securityPattern.name) != null) {
+ AvatarAttributeState authDest = new AvatarAttributeState(block.getName() + "." + dummy.getName() + "." + ae.securityPattern.name, ae.getReferenceObject(), block.getAvatarAttributeWithName(ae.securityPattern.name), dummy);
+ signalAuthDestMap.put(ae.securityPattern.name, authDest);
+ }
+ }
- asm.setStartState(ss);
- } else {
- //Not requested
- List<AvatarStateMachineElement> elementList = translateState(task.getActivityDiagram().get(0), block);
- for (AvatarStateMachineElement e : elementList) {
- e.setName(processName(e.getName(), e.getID()));
- asm.addElement(e);
- stateObjectMap.put(task.getName().split("__")[1] + "__" + e.getName(), e.getReferenceObject());
+ //Can't decrypt hash or nonce
}
- asm.setStartState((AvatarStartState) elementList.get(0));
- }
- for (SecurityPattern secPattern : secPatterns) {
- AvatarAttribute sec = block.getAvatarAttributeWithName(secPattern.name);
- if (sec != null) {
- //sec = new AvatarAttribute(secPattern.name, AvatarType.INTEGER, block, null);
- //AvatarAttribute enc = new AvatarAttribute(secPattern.name+"_encrypted", AvatarType.INTEGER, block, null);
- // block.addAttribute(sec);
- // block.addAttribute(enc);
- //}
- avspec.addPragma(new AvatarPragmaSecret("#Confidentiality " + block.getName() + "." + secPattern.name, null, sec));
+ } else {
+ // See if action.
+ if (ae instanceof TMLActionState) {
+ String val = ((TMLActionState) ae).getAction();
+ tran.addAction(val);
}
- }
- }
+ }
+ } else if (ae instanceof TMLActivityElementWithIntervalAction) {
+ AvatarState as = new AvatarState(ae.getName().replaceAll(" ", ""), ae.getReferenceObject());
+ tran = new AvatarTransition(block, "__after_" + ae.getName(), ae.getReferenceObject());
+ 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;
- //Add authenticity pragmas
- for (String s : signalAuthOriginMap.keySet()) {
- if (signalAuthDestMap.containsKey(s)) {
- AvatarPragmaAuthenticity pragma = new AvatarPragmaAuthenticity("#Authenticity " + signalAuthOriginMap.get(s).getName() + " " + signalAuthDestMap.get(s).getName(), signalAuthOriginMap.get(s).getReferenceObject(), signalAuthOriginMap.get(s), signalAuthDestMap.get(s));
- if (secChannelMap.containsKey(s)) {
- for (String channel : secChannelMap.get(s)) {
- TMLChannel ch = tmlmodel.getChannelByShortName(channel);
- if (ch != null) {
- if (ch.checkAuth) {
- avspec.addPragma(pragma);
- break;
- }
- }
- }
+ String nv = getName(ch.getName()) + "_chData";
+ block.addIntAttributeIfApplicable(nv);
- } else {
- avspec.addPragma(pragma);
- }
+ boolean checkAcc = false;
+ if (ae.getReferenceObject() != null) {
+ checkAcc = ((TGComponent) ae.getReferenceObject()).getCheckableAccessibility();
}
- }
+ boolean checked = false;
+ if (ae.getReferenceObject() != null) {
+ checked = ((TGComponent) ae.getReferenceObject()).hasCheckedAccessibility();
+ }
+ AvatarState signalState = new AvatarState("signalstate_" + ae.getName().replaceAll(" ", "") + "_" + ch.getName(), ae.getReferenceObject(), checkAcc, checked);
+ AvatarTransition signalTran = new AvatarTransition(block, "__after_signalstate_" + ae.getName() + "_" + ch.getName(), ae.getReferenceObject());
+ AvatarTransition signalTranBefore = new AvatarTransition(block, "__before_signalstateint_" + ae.getName() + "_" + ch.getName(), ae
+ .getReferenceObject());
+ AvatarState signalStateIntermediate = new AvatarState("signalstateinter_" + ae.getName().replaceAll(" ", "") + "_" + ch.getName(), ae
+ .getReferenceObject(), checkAcc, checked);
+ AvatarTransition signalTranInit = new AvatarTransition(block, "_init_signalstate_" + ae.getName() + "_" + ch.getName(), ae
+ .getReferenceObject());
- //Create relations
- //Channels are ?? to ??
- //Requests are n to 1
- //Events are ?? to ??
- AvatarBlock fifo = new AvatarBlock("FIFO", avspec, null);
- for (TMLChannel channel : tmlmodel.getChannels()) {
- // We assume one to one because fork and join have been removed
+ if (ae instanceof TMLReadChannel) {
+ //Create signal if it does not already exist
+ sig = signalInMap.get(ch.getName());
+ } else {
+ sig = signalOutMap.get(ch.getName());
+ }
- if (channel.isBasicChannel()) {
- TraceManager.addDev("checking channel " + channel.getName());
- AvatarRelation ar = new AvatarRelation(channel.getName(), taskBlockMap.get(channel.getOriginTask()), taskBlockMap.get(channel.getDestinationTask()), channel.getReferenceObject());
+ AvatarActionOnSignal as = new AvatarActionOnSignal(ae.getName(), sig, ae.getReferenceObject());
+ tran = new AvatarTransition(block, "__after_" + ae.getName(), ae.getReferenceObject());
- if (channel.getType() == TMLChannel.BRBW) {
- ar.setAsynchronous(true);
- ar.setSizeOfFIFO(channel.getSize());
- ar.setBlocking(true);
- } else if (channel.getType() == TMLChannel.BRNBW) {
- ar.setAsynchronous(true);
- ar.setSizeOfFIFO(channel.getSize());
- ar.setBlocking(false);
- } else {
- //Create new block, hope for best
- if (mc) {
- fifo = createFifo(channel.getName());
- ar.setAsynchronous(false);
- }
- }
- //Find in signal
+ elementList.add(signalState);
+ elementList.add(signalStateIntermediate);
+ elementList.add(as);
+ elementList.add(tran);
+ elementList.add(signalTranInit);
+ elementList.add(signalTranBefore);
+ elementList.add(signalTran);
- List<AvatarSignal> sig1 = new ArrayList<AvatarSignal>();
- //Sig1 contains IN Signals, Sig2 contains OUT signals
- sig1.add(signalInMap.get(channel.getName()));
- List<AvatarSignal> sig2 = new ArrayList<AvatarSignal>();
- sig2.add(signalOutMap.get(channel.getName()));
- for (AvatarSignal sig : signals) {
- if (sig.getInOut() == AvatarSignal.IN) {
- String name = sig.getName();
- if (name.equals(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.getOriginPort().getName())) {
- // sig2.add(sig);
- }
- }
- }
- TraceManager.addDev("size " + sig1.size() + " " + sig2.size());
+ signalState.addNext(signalTranInit);
+ signalTranInit.addAction(ch.getName() + "_chData = 0");
+ signalTranInit.addNext(signalStateIntermediate);
+ signalStateIntermediate.addNext(signalTran);
+ signalTran.setGuard(ch.getName() + "_chData < (" + aec.getNbOfSamples() + ")");
+ signalTran.addNext(as);
+ as.addNext(signalTranBefore);
+ signalTranBefore.addAction(ch.getName() + "_chData = " + ch.getName() + "_chData + 1 ");
+ signalTranBefore.addNext(signalStateIntermediate);
- if (sig1.size() == 0) {
- sig1.add(new AvatarSignal(getName(channel.getName()), AvatarSignal.IN, null));
- }
+ signalStateIntermediate.addNext(tran);
+ tran.setGuard("else");
- if (sig2.size() == 0) {
- sig2.add(new AvatarSignal(getName(channel.getName()), AvatarSignal.OUT, null));
- }
- if (sig1.size() == 1 && sig2.size() == 1) {
- if (channel.getType() == TMLChannel.NBRNBW && mc) {
- AvatarSignal read = fifo.getSignalByName("readSignal");
- ar.block2 = fifo;
- //Set IN signal with read
- ar.addSignals(sig1.get(0), read);
- AvatarRelation ar2 = new AvatarRelation(channel.getName() + "2", fifo, taskBlockMap.get(channel.getDestinationTask()), channel.getReferenceObject());
- AvatarSignal write = fifo.getSignalByName("writeSignal");
- //set OUT signal with write
- ar2.addSignals(write, sig2.get(0));
- // System.out.println("Set " + sig2.get(0) + " and write");
- ar2.setAsynchronous(false);
- avspec.addRelation(ar2);
- } else {
- ar.addSignals(sig2.get(0), sig1.get(0));
- }
- } else {
- //Create relation if it does not exist
- if (top.getSignalByName(getName(channel.getName()) + "in") == null) {
- AvatarRelation relation = new AvatarRelation(channel.getName(), top, top, channel.getReferenceObject());
- AvatarSignal s1 = new AvatarSignal(getName(channel.getName()) + "in", AvatarSignal.IN, null);
- AvatarSignal s2 = new AvatarSignal(getName(channel.getName()) + "out", AvatarSignal.OUT, null);
- top.addSignal(s1);
- top.addSignal(s2);
- relation.addSignals(s2, s1);
- avspec.addRelation(relation);
- // System.out.println("Failure to match signals for TMLChannel "+ channel.getName());
- }
- }
- avspec.addRelation(ar);
- } else {
- //System.out.println("WTF Found non-basic channel");
- //If not a basic channel, create a relation between TOP block and itself
- AvatarRelation relation = new AvatarRelation(channel.getName(), top, top, channel.getReferenceObject());
- AvatarSignal s1 = new AvatarSignal(getName(channel.getName()) + "in", AvatarSignal.IN, null);
- AvatarSignal s2 = new AvatarSignal(getName(channel.getName()) + "out", AvatarSignal.OUT, null);
- top.addSignal(s1);
- top.addSignal(s2);
- relation.addSignals(s2, s1);
- avspec.addRelation(relation);
- for (TMLTask t1 : channel.getOriginTasks()) {
- for (TMLTask t2 : channel.getDestinationTasks()) {
- AvatarRelation ar = new AvatarRelation(channel.getName(), taskBlockMap.get(t1), taskBlockMap.get(t2), channel.getReferenceObject());
- ar.setPrivate(originDestMap.get(t1.getName() + "__" + t2.getName()) == 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(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(getName(channel.getName()))) {
- sig2.add(sig);
- }
- }
- }
- if (sig1.size() == 0) {
- sig1.add(new AvatarSignal(getName(channel.getName()), AvatarSignal.IN, null));
- }
- if (sig2.size() == 0) {
- sig2.add(new AvatarSignal(getName(channel.getName()), AvatarSignal.OUT, null));
- }
- if (sig1.size() == 1 && sig2.size() == 1) {
- ar.addSignals(sig2.get(0), sig1.get(0));
- } else {
- System.out.println("Failure to match signals for TMLChannel " + channel.getName() + " between " + t1.getName() + " and " + t2.getName());
+ } else if (ae instanceof TMLForLoop) {
+ TMLForLoop loop = (TMLForLoop) ae;
+ if (loop.isInfinite()) {
+ //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().replaceAll(" ", "") + "__init", ae.getReferenceObject());
+ elementList.add(initState);
+ //Build transition to choice
+ tran = new AvatarTransition(block, "loop_init__" + ae.getName(), ae.getReferenceObject());
+ tran.addAction("loop_index=0");
+ elementList.add(tran);
+ initState.addNext(tran);
+ //Choice state
+ AvatarState as = new AvatarState(ae.getName().replaceAll(" ", "") + "__choice", ae.getReferenceObject());
+ elementList.add(as);
+ tran.addNext(as);
+ //transition to first element of loop
+ tran = new AvatarTransition(block, "loop_increment__" + ae.getName(), ae.getReferenceObject());
+ //Set default loop limit guard
+ tran.setGuard(AvatarGuard.createFromString(block, "loop_index != " + loopLimit));
+ //tran.addAction(AvatarTerm.createActionFromString(block, "loop_index = loop_index + 1"));
+ 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) {
+ if (e instanceof AvatarTransition) {
+ e.addNext(as);
+ elementList.add(e);
}
- avspec.addRelation(ar);
+ } 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);
}
}
- }
- }
- for (TMLRequest request : tmlmodel.getRequests()) {
- for (TMLTask t1 : request.getOriginTasks()) {
- AvatarRelation ar = new AvatarRelation(request.getName(), taskBlockMap.get(t1), taskBlockMap.get(request.getDestinationTask()), request.getReferenceObject());
- ar.setPrivate(originDestMap.get(t1.getName() + "__" + request.getDestinationTask().getName()) == 1);
- 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(getName(request.getName()))) {
- sig1.add(sig);
- }
- }
+ //Transition if exiting loop
+ tran = new AvatarTransition(block, "end_loop__" + ae.getName(), ae.getReferenceObject());
+ tran.setGuard(new AvatarGuardElse());
+ as.addNext(tran);
+ AvatarStopState stop = new AvatarStopState("stop", null);
+ tran.addNext(stop);
+ elementList.add(tran);
+ elementList.add(stop);
+ 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().replaceAll(" ", "") + "__init", ae.getReferenceObject());
+ elementList.add(initState);
+ //Build transition to choice
+ tran = new AvatarTransition(block, "loop_init__" + ae.getName(), ae.getReferenceObject());
+ tran.addAction(AvatarTerm.createActionFromString(block, loop.getInit()));
+ //tran.addAction(AvatarTerm.createActionFromString(block, "loop_index=0"));
+ elementList.add(tran);
+ initState.addNext(tran);
+ //Choice state
+ AvatarState as = new AvatarState(ae.getName().replaceAll(" ", "") + "__choice", ae.getReferenceObject());
+ elementList.add(as);
+ tran.addNext(as);
+ //transition to first element of loop
+ tran = new AvatarTransition(block, "loop_increment__" + ae.getName(), ae.getReferenceObject());
+ //Set default loop limit guard
+ tran.setGuard(AvatarGuard.createFromString(block, loop.getCondition()));
+ /*AvatarGuard guard = */
+ //AvatarGuard.createFromString(block, loop.getCondition());
+ tran.addAction(AvatarTerm.createActionFromString(block, loop.getIncrement()));
+ //tran.addAction(AvatarTerm.createActionFromString(block, "loop_index = loop_index + 1"));
+ if (elements.size() > 0) {
+ tran.addNext(elements.get(0));
+ as.addNext(tran);
+ elementList.add(tran);
}
- //Find out signal
- for (AvatarSignal sig : signals) {
- if (sig.getInOut() == AvatarSignal.OUT) {
- String name = sig.getName();
-
- if (name.equals(getName(request.getName()))) {
- sig2.add(sig);
- }
+ //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);
}
}
- if (sig1.size() == 0) {
- sig1.add(new AvatarSignal(getName(request.getName()), AvatarSignal.IN, null));
- }
- if (sig2.size() == 0) {
- sig2.add(new AvatarSignal(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());
- }
-
- ar.setAsynchronous(false);
- avspec.addRelation(ar);
- }
- }
-
- for (TMLEvent event : tmlmodel.getEvents()) {
-
- TraceManager.addDev("Handling Event:" + event.getName() + " 1:" + taskBlockMap.get(event.getOriginTask()) + " 2:" + taskBlockMap.get
- (event.getDestinationTask()));
- AvatarRelation ar = new AvatarRelation(event.getName(), taskBlockMap.get(event.getOriginTask()), taskBlockMap.get(event.getDestinationTask()), event.getReferenceObject());
- //ar.setPrivate(originDestMap.get(event.getOriginTask().getName() + "__" + event.getDestinationTask().getName()) == 1);
- 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(getName(event.getName()))) {
- sig1.add(sig);
- }
+ //Transition if exiting loop
+ tran = new AvatarTransition(block, "end_loop__" + ae.getName(), ae.getReferenceObject());
+ tran.setGuard(new AvatarGuardElse());
+ 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;
}
- //Find out signal
- for (AvatarSignal sig : signals) {
- if (sig.getInOut() == AvatarSignal.OUT) {
- String name = sig.getName();
- if (name.equals(getName(event.getName()))) {
- sig2.add(sig);
- }
+
+ } else if (ae instanceof TMLChoice) {
+ AvatarState as = new AvatarState(ae.getName().replaceAll(" ", ""), ae.getReferenceObject());
+ //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, ae.getReferenceObject());
+ //tran.setGuard(c.getGuard(i));
+ as.addNext(tran);
+ List<AvatarStateMachineElement> nexts = translateState(ae.getNextElement(i), block);
+ if (nexts.size() > 0) {
+ tran.addNext(nexts.get(0));
+ elementList.add(tran);
+ elementList.addAll(nexts);
}
}
- if (sig1.size() == 0) {
- sig1.add(new AvatarSignal(getName(event.getName()), AvatarSignal.IN, null));
- }
- if (sig2.size() == 0) {
- sig2.add(new AvatarSignal(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());
- }
- if (event.isBlocking()) {
- ar.setAsynchronous(true);
- ar.setBlocking(true);
- ar.setSizeOfFIFO(event.getMaxSize());
- } else {
- ar.setAsynchronous(true);
- ar.setBlocking(false);
- ar.setSizeOfFIFO(event.getMaxSize());
+ return elementList;
+ } else if (ae instanceof TMLSelectEvt) {
+ AvatarState as = new AvatarState(ae.getName().replaceAll(" ", ""), 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, ae.getReferenceObject());
+ as.addNext(tran);
+ List<AvatarStateMachineElement> nexts = translateState(ae.getNextElement(i), block);
+ tran.addNext(nexts.get(0));
+ elementList.add(tran);
+ elementList.addAll(nexts);
}
- avspec.addRelation(ar);
+ return elementList;
+ } else {
+ TraceManager.addDev("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;
+ }
- // System.out.println("Avatar relations " + avspec.getRelations());
+ public String processName(String name, int id) {
+ name = name.replaceAll("-", "_").replaceAll(" ", "");
+ if (allStates.contains(name)) {
+ return name + id;
- for (AvatarSignal sig : signals) {
- // System.out.println("signal " + sig.getName());
- //check that all signals are put in relations
- AvatarRelation ar = avspec.getAvatarRelationWithSignal(sig);
- if (ar == null) {
- System.out.println("missing relation for " + sig.getName());
- }
- }
- //Check if we matched up all signals
- for (SecurityPattern sp : symKeys.keySet()) {
- if (symKeys.get(sp).size() > 1) {
- String keys = "";
- for (AvatarAttribute key : symKeys.get(sp)) {
- keys = keys + " " + key.getBlock().getName() + "." + key.getName();
- }
- avspec.addPragma(new AvatarPragmaInitialKnowledge("#InitialSessionKnowledge " + keys, null, symKeys.get(sp), true));
- }
+ } else {
+ allStates.add(name);
+ return name;
}
- for (SecurityPattern sp : pubKeys.keySet()) {
- if (pubKeys.get(sp).size() != 0) {
- String keys = "";
- List<String> pubKeyNames = new ArrayList<String>();
- for (AvatarAttribute key : pubKeys.get(sp)) {
- if (!pubKeyNames.contains(key.getBlock().getName() + "." + key.getName())) {
- keys = keys + " " + key.getBlock().getName() + "." + key.getName();
- pubKeyNames.add(key.getBlock().getName() + "." + key.getName());
- }
+ }
+ /* public AvatarPragma generatePragma(String[] s){
+
+ }*/
+
+ public String getName(String s) {
+ // System.out.println("String " + s);
+ if (nameMap.containsKey(s)) {
+ return nameMap.get(s);
+ } else {
+ if (!s.contains("__")) {
+ nameMap.put(s, s);
+ return s;
+ } else if (s.split("__").length == 1) {
+ nameMap.put(s, s.split("__")[s.split("__").length - 1]);
+ return s.split("__")[s.split("__").length - 1];
+ } else if (s.contains("JOIN") || s.contains("FORK")) {
+ String t = "";
+ t += s.split("__")[0];
+ for (int i = 2; i < s.split("__").length; i++) {
+ t += "JOIN" + s.split("__")[i];
}
- // avspec.addPragma(new AvatarPragmaInitialKnowledge("#InitialSessionKnowledge "+keys, null, pubKeys.get(sp),true));
- //System.out.println("pragma " + keys);
+ nameMap.put(s, t);
+ return t;
+ } else {
+ /* String t = "";
+ for (int i = 0; i < s.split("__").length; i++) {
+ t += s.split("__")[i];
+ }*/
+ nameMap.put(s, s);
+ return s;
+ // nameMap.put(s, s.split("__")[s.split("__").length - 1]);
+ // return s.split("__")[s.split("__").length - 1];
}
}
+ }
- tmlmodel.secChannelMap = secChannelMap;
-// System.out.println("avatar spec\n" +avspec);
- return avspec;
- }
/*public void backtraceReachability( Map<AvatarPragmaReachability, ProVerifQueryResult> reachabilityResults) {
for (AvatarPragmaReachability pragma: reachabilityResults.keySet())
@@ -1811,11 +1842,26 @@ public class FullTML2Avatar {
return fifo;
}
+ public String getNameReworked(String name, int index) {
+ String[] split = name.split("__");
+ if (split.length > index) {
+ return split[index];
+ }
+ return name;
+ }
- public AvatarSpecification convertToSecurityType(AvatarSpecification spec) {
- return spec;
+ public AvatarType getAvatarType(TMLType p) {
+ switch(p.getType()){
+ case TMLType.NATURAL:
+ return AvatarType.INTEGER;
+ case TMLType.BOOLEAN:
+ return AvatarType.BOOLEAN;
+ }
+ return AvatarType.UNDEFINED;
}
+
+
}
diff --git a/src/main/java/ui/GTURTLEModeling.java b/src/main/java/ui/GTURTLEModeling.java
index 32813f34dace90f1b005a9bbf63f36dc40a6eb04..82f441c09dd3e211f2db8ef33af8edd1200041a5 100644
--- a/src/main/java/ui/GTURTLEModeling.java
+++ b/src/main/java/ui/GTURTLEModeling.java
@@ -1906,7 +1906,7 @@ public class GTURTLEModeling {
if (mgui.isExperimentalOn()) {
TraceManager.addDev("Avatar spec:" + avatarspec.toString());
- mgui.drawAvatarSpecification(avatarspec);
+ //mgui.drawAvatarSpecification(avatarspec);
//TraceManager.addDev("Avatar spec:" + avatarspec.toString());
//AvatarSpecification av2 = avatarspec.advancedClone();
//mgui.drawAvatarSpecification(av2);
@@ -9222,9 +9222,9 @@ public class GTURTLEModeling {
for (int i = 0; i < ar.nbOfSignals(); i++) {
//TraceManager.addDev("Adding signal relations to connector");
//
- //TraceManager.addDev("Adding signal 1: " + ar.getSignal1(i).toString() + " of block " + ar.block1.getName());
+ TraceManager.addDev("Adding signal 1: " + ar.getSignal1(i).toString() + " of block " + ar.block1.getName());
conn.addSignal(ar.getSignal1(i).toString(), ar.getSignal1(i).getInOut() == 0, ar.block1.getName().contains(bl1));
- //TraceManager.addDev("Adding signal 2:" + ar.getSignal2(i).toString() + " of block " + ar.block2.getName());
+ TraceManager.addDev("Adding signal 2:" + ar.getSignal2(i).toString() + " of block " + ar.block2.getName());
conn.addSignal(ar.getSignal2(i).toString(), ar.getSignal2(i).getInOut() == 0, !ar.block2.getName().contains(bl2));
//
}