diff --git a/build.txt b/build.txt
index ff731a055aecf94a81f8d90ee5c7b5b46d9333c5..63586c4a7050bd891d1a42689ccb82d4d004f33d 100644
--- a/build.txt
+++ b/build.txt
@@ -1 +1 @@
-13465
\ No newline at end of file
+13471
\ No newline at end of file
diff --git a/doc/avatarmodelchecker/images/AUTgraphlist.png b/doc/avatarmodelchecker/images/AUTgraphlist.png
new file mode 100644
index 0000000000000000000000000000000000000000..09d10072a55164e49f7b56e4f256c027b20fdcd6
Binary files /dev/null and b/doc/avatarmodelchecker/images/AUTgraphlist.png differ
diff --git a/doc/avatarmodelchecker/images/counterexamplegraph.png b/doc/avatarmodelchecker/images/counterexamplegraph.png
new file mode 100644
index 0000000000000000000000000000000000000000..0b4deb1fedcfa349513213ad74525b333814b8cf
Binary files /dev/null and b/doc/avatarmodelchecker/images/counterexamplegraph.png differ
diff --git a/doc/avatarmodelchecker/images/modelcheckerwindow.jpg b/doc/avatarmodelchecker/images/modelcheckerwindow.jpg
index e8a83ca3facc0960f82c446f82dbffecf2a640d1..ef713229fe7dba317121ed9c5b13912011f4e76f 100644
Binary files a/doc/avatarmodelchecker/images/modelcheckerwindow.jpg and b/doc/avatarmodelchecker/images/modelcheckerwindow.jpg differ
diff --git a/doc/avatarmodelchecker/ttool_avatarmodelchecker.tex b/doc/avatarmodelchecker/ttool_avatarmodelchecker.tex
index c31f168e28d27c38942deffdce57ba8822c398fe..9ae2f8f37a6a1a77846f78307179976fc0de8a30 100644
--- a/doc/avatarmodelchecker/ttool_avatarmodelchecker.tex
+++ b/doc/avatarmodelchecker/ttool_avatarmodelchecker.tex
@@ -228,7 +228,7 @@ To start the CTL query verification, let's compile again and let's open the mode
\includegraphics[width=0.7\textwidth]{images/safety_result.png}
\caption{Safety Result}
\label{fig:sresult}
-\end{figure}
+\end{figure}\\\\
\newpage
\section{Verification Guide} \label{sec:vg}
@@ -248,7 +248,7 @@ The next section contains options for basic properties verification:
\item \textbf{Reachability}: it checks for states reachability
\item \textbf{Liveness}: it checks for states liveness
\end{itemize}
-The next section allows to execute safety and liveness pragmas written as a CTL formula. Each of them can be selected or not for the verification.
+The next section allows us to execute safety and liveness pragmas written as a CTL formula. Each of them can be selected or not for verification. Also, counterexample traces can be generated for each CTL query and deadlock check. The option \textbf{Generate counterexample traces} generates a trace in a text file for each pragma with a counterexample. The trace contains all the states and transitions that lead to a counterexample step by step. Selecting \textbf{Generate counterexample AUT graphs}, a displayable graph will appear in the reachability graphs section. A detailed example is available in section \ref{sec:tg}.
\\\\
Then, \textbf{Reachability Graph Generation} options is used to generate and save the reachability graph. Moreover, it can can be saved also in "dotty" format.
@@ -268,6 +268,35 @@ Expression \texttt{p} and \texttt{q} may be on states or variables. The format u
\item \textit{DoorAndLockButton.IN\_EMERGENCY\_CALL --> DoorAndLockButton.CLOSED\_AND\_LOCKED || DoorAndLockButton.CLOSED\_AND\_UNLOCKED}: whenever DoorAndLockButton.IN\_EMERGENCY\_CALL state is encounted, then or DoorAndLockButton.CLOSED\_AND\_LOCKED or DoorAndLockButton.CLOSED\_AND\_UNLOCKED will be encounted at some subsequent moment.
\end{itemize}
+\subsection{Traces generation} \label{sec:tg}
+For advanced verification queries and deadlock check, there is the possibility of generating counterexample traces that show the path to prove or disprove a property. In particular:
+\begin{itemize}
+\item \textbf{A[] p}: shows the path that disproves the property
+\item \textbf{A<> p}: shows the path that disproves the property
+\item \textbf{E[] p}: shows the path that proves the property
+\item \textbf{E<> p}: shows the path that proves the property
+\item \textbf{p --> q}: shows the path that disproves the property starting from a state with p valid.
+\item \textbf{No deadlocks?}: shows a path to a deadlock
+\end{itemize}
+The \textbf{Generate counterexample traces} option writes, in the file indicated in the text field on the right, all the steps to reach a counterexample. State lines show the current state in the state machine for each block in the system. Transition lines show details of the transition taken to reach the next state.
+\\\\
+The \textbf{Generate counterexample AUT graphs} option allows us to display the trace as a reachability graph, saving it in AUT format. Entry to the graph, with the name of the query, will appear in the \textit{R. Graphs} section in TTool.
+\\\\
+Let's do a guidated example to traces generation. Let's open again the "PressureController.xml" model used in the previous section. Let's execute a verification of the only query \textit{MainController.LowPressure --> AlarmManager.AlarmIsOff} activating both the options \textit{Generate counterexample traces} and \textit{Generate counterexample AUT graphs}. Let's press start to execute the verification. If now we open the file \textit{trace*.txt} in which the trace is saved, we can see the name of the trace in the first line, and then states and transitions alternating until the counterexample state that disprove the property. The first state has the state machine pointed to MainController.LowPressure (or to a direct child like MainController.WaitFirstHighPressure). The last state indicates a loop or a state for which the property is prooved to be never satisfied. The AUT graph is visible with the name of the query in the Reachability graphs section as shown in Figure \ref{fig:aut}
+\begin{figure}[h!]
+\centering
+\includegraphics[width=0.7\textwidth]{images/AUTgraphlist.png}
+\caption{Link to the AUT graph generated on query}
+\label{fig:aut}
+\end{figure}
+Doing right click on the graph and pressing show, we are able to see graphically the trace (see Figure \ref{fig:trgraph}).
+\begin{figure}[h!]
+\centering
+\includegraphics[width=0.9\textwidth]{images/counterexamplegraph.png}
+\caption{AUT graph generated on query}
+\label{fig:trgraph}
+\end{figure}
+
\subsection{Concurrency behavior} \label{sec:cb}
In section \ref{sec:vg}, we discussed about the option \textit{Ignore concurrency between internal actions} and how it could effect the model-checker behavior. In this section, we will show with a guided example the differences between having this option on or off.
\\\\
diff --git a/src/main/java/avatartranslator/AvatarActionAssignment.java b/src/main/java/avatartranslator/AvatarActionAssignment.java
index d4c9a54c53dfe9a4b99aca2028eab8e5cc3c0c3a..54b17f1291a7089b0c3b229b6fe333e5f15e53e1 100644
--- a/src/main/java/avatartranslator/AvatarActionAssignment.java
+++ b/src/main/java/avatartranslator/AvatarActionAssignment.java
@@ -100,8 +100,15 @@ public class AvatarActionAssignment implements AvatarAction {
boolean res;
actionSolver = new AvatarExpressionSolver(rightHand.getName());
res = actionSolver.buildExpression(block);
- leftAttribute = new AvatarExpressionAttribute(block, leftHand.getName());
- res &= !leftAttribute.hasError();
+ if (AvatarExpressionSolver.containsElementAttribute(leftHand)) {
+ leftAttribute = AvatarExpressionSolver.getElementAttribute(leftHand);
+ } else {
+ leftAttribute = new AvatarExpressionAttribute(block, leftHand.getName());
+ res &= !leftAttribute.hasError();
+ if (res) {
+ AvatarExpressionSolver.addElementAttribute(leftHand, leftAttribute);
+ }
+ }
return res;
}
diff --git a/src/main/java/avatartranslator/AvatarActionOnSignal.java b/src/main/java/avatartranslator/AvatarActionOnSignal.java
index 23fbf3458617c358bb4a3ca0d73a83c536c2f46c..da3fb30b03ae77b3e7f2b3bba2083b96d3e0a4c2 100644
--- a/src/main/java/avatartranslator/AvatarActionOnSignal.java
+++ b/src/main/java/avatartranslator/AvatarActionOnSignal.java
@@ -112,12 +112,22 @@ public class AvatarActionOnSignal extends AvatarStateMachineElement {
public boolean buildActionSolver(AvatarBlock block) {
AvatarExpressionAttribute aea;
+ AvatarElement attr;
boolean res = true;
+
actionAttr = new ArrayList<AvatarExpressionAttribute>();
for (String val : values) {
- aea = new AvatarExpressionAttribute(block, val);
- actionAttr.add(aea);
- res &= aea.hasError();
+ attr = AvatarExpressionAttribute.getElement(val, block);
+ if (attr != null && AvatarExpressionSolver.containsElementAttribute(attr)) {
+ actionAttr.add(AvatarExpressionSolver.getElementAttribute(attr));
+ } else {
+ aea = new AvatarExpressionAttribute(block, val);
+ res &= !aea.hasError();
+ if (res) {
+ AvatarExpressionSolver.addElementAttribute(attr, aea);
+ actionAttr.add(aea);
+ }
+ }
}
return res;
}
diff --git a/src/main/java/avatartranslator/AvatarBlock.java b/src/main/java/avatartranslator/AvatarBlock.java
index 596ac54083a08ec0e6786702d2a72d638798901b..750a768f5c6ed7ff7d333f11f5885586a53edd58 100644
--- a/src/main/java/avatartranslator/AvatarBlock.java
+++ b/src/main/java/avatartranslator/AvatarBlock.java
@@ -42,7 +42,6 @@ import java.util.ArrayList;
import java.util.LinkedList;
import java.util.List;
-
/**
* Class AvatarBlock
* Creation: 20/05/2010
@@ -61,6 +60,10 @@ public class AvatarBlock extends AvatarElement implements AvatarStateMachineOwne
private int blockIndex; //Index of block in the Avatar Specification
private String globalCode;
+
+ private int booleanOffset;
+ private int attributeOptRatio;
+ private List<AvatarAttribute> constants;
public AvatarBlock(String _name, AvatarSpecification _avspec, Object _referenceObject) {
@@ -71,6 +74,8 @@ public class AvatarBlock extends AvatarElement implements AvatarStateMachineOwne
methods = new LinkedList<AvatarMethod>();
signals = new LinkedList<AvatarSignal>();
asm = new AvatarStateMachine(this, "statemachineofblock__" + _name, _referenceObject);
+ booleanOffset = -1;
+ attributeOptRatio = 1;
}
@@ -119,6 +124,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;
}
@@ -164,11 +181,15 @@ public class AvatarBlock extends AvatarElement implements AvatarStateMachineOwne
}
}
- public void addIntAttributeIfApplicable(String _name) {
- if (getAvatarAttributeWithName(_name) == null) {
- AvatarAttribute aa = new AvatarAttribute(_name, AvatarType.INTEGER, this, null);
- attributes.add(aa);
+ public AvatarAttribute addIntAttributeIfApplicable(String _name) {
+ AvatarAttribute old = getAvatarAttributeWithName(_name);
+ if (old != null) {
+ return old;
}
+
+ AvatarAttribute aa = new AvatarAttribute(_name, AvatarType.INTEGER, this, null);
+ attributes.add(aa);
+ return aa;
}
public String toString() {
@@ -283,6 +304,28 @@ public class AvatarBlock extends AvatarElement implements AvatarStateMachineOwne
}
return -1;
}
+
+ public int getIndexOfConstantWithName(String _name) {
+ int cpt = 0;
+
+ if (constants == null) {
+ return -1;
+ }
+ for (AvatarAttribute attribute : constants) {
+ if (attribute.getName().compareTo(_name) == 0) {
+ return cpt;
+ }
+ cpt++;
+ }
+ return -1;
+ }
+
+ public AvatarAttribute getConstantWithIndex(int index) {
+ if (constants == null) {
+ return null;
+ }
+ return constants.get(index);
+ }
/**
* Look for an attribute with the provided name.
@@ -697,6 +740,96 @@ public class AvatarBlock extends AvatarElement implements AvatarStateMachineOwne
}
return outside;
}
+
+
+ //move boolean attributes to last positions in list attributes
+ public void sortAttributes() {
+ List<AvatarAttribute> newAttributes = new LinkedList<AvatarAttribute>();
+
+ for (AvatarAttribute attribute : attributes) {
+ if (attribute.getType() != AvatarType.BOOLEAN) {
+ newAttributes.add(attribute);
+ }
+ }
+
+ booleanOffset = newAttributes.size();
+
+ for (AvatarAttribute attribute : attributes) {
+ if (attribute.getType() == AvatarType.BOOLEAN) {
+ newAttributes.add(attribute);
+ }
+ }
+
+ attributes = newAttributes;
+ }
+
+ public int getBooleanOffset() {
+ return booleanOffset;
+ }
+
+
+ public int getAttributeOptRatio() {
+ return attributeOptRatio;
+ }
+
+ public void setAttributeOptRatio(int attributeOptRatio) {
+ if (attributeOptRatio == 2 || attributeOptRatio == 4) {
+ this.attributeOptRatio = attributeOptRatio;
+ } else {
+ this.attributeOptRatio = 1;
+ }
+ }
+
+
+ public void removeConstantAttributes() {
+ AvatarTransition at;
+ List<AvatarAttribute> newAttributes = new LinkedList<AvatarAttribute>();
+ constants = new LinkedList<AvatarAttribute>();
+
+ for (AvatarAttribute attr : attributes) {
+ boolean toKeep = false;
+
+ if (attr.isTimer()) {
+ toKeep = true;
+ }
+ for (AvatarStateMachineElement elt : asm.getListOfElements()) {
+ if (elt instanceof AvatarTransition) {
+ at = (AvatarTransition) elt;
+ for (AvatarAction aa : at.getActions()) {
+ if (aa instanceof AvatarActionAssignment) {
+ if (((AvatarActionAssignment) aa).leftHand.getName().compareTo(attr.name) == 0) {
+ //assigned
+ toKeep = true;
+ }
+ }
+ }
+ } else if (elt instanceof AvatarActionOnSignal) {
+ AvatarSignal sig = ((AvatarActionOnSignal) elt).getSignal();
+ if (sig != null && sig.isIn()) {
+ for (String val : ((AvatarActionOnSignal) elt).getValues()) {
+ if (val.compareTo(attr.name) == 0) {
+ //assigned
+ toKeep = true;
+ }
+ }
+ }
+ } else if (elt instanceof AvatarRandom) {
+ if (((AvatarRandom) elt).getVariable().compareTo(attr.name) == 0) {
+ toKeep = true;
+ }
+ }
+ if (toKeep) {
+ break;
+ }
+ }
+ if (!toKeep) {
+ constants.add(attr);
+ } else {
+ newAttributes.add(attr);
+ }
+ }
+ attributes = newAttributes;
+ }
@Override
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/avatartranslator/AvatarExpressionAttribute.java b/src/main/java/avatartranslator/AvatarExpressionAttribute.java
index a3e7a4696e3fe7cbea38246ad45251a3d470bb85..8521c2adac9bcaa07256aadbff7b40a20f0f8d6c 100644
--- a/src/main/java/avatartranslator/AvatarExpressionAttribute.java
+++ b/src/main/java/avatartranslator/AvatarExpressionAttribute.java
@@ -56,41 +56,45 @@ public class AvatarExpressionAttribute {
private AvatarStateMachineElement state;
private String s;
private boolean isState;
- private boolean error;
+ private int error; //0: no error; -1: building error; -2: is constant
+ private int shift;
+ private int mask;
public AvatarExpressionAttribute(AvatarSpecification spec, String s) {
this.s = s;
isState = false;
- error = !initAttributes(spec);
+ error = initAttributes(spec);
}
public AvatarExpressionAttribute(AvatarBlock block, String s) {
this.s = s;
isState = false;
- error = !initAttributes(block);
+ error = initAttributes(block);
}
public AvatarExpressionAttribute(AvatarBlock block, AvatarStateMachineElement asme) {
this.s = asme.name;
isState = true;
state = asme;
- error = false;
+ error = 0;
accessIndex = -1;
+ shift = 0;
+ mask = 0xFFFFFFFF;
block = null;
}
- private boolean initAttributes(AvatarSpecification spec) {
+ private int initAttributes(AvatarSpecification spec) {
//Extract Block and Attribute
String[] splitS;
String blockString;
String fieldString;
if (spec == null) {
- return false;
+ return -1;
}
if (s.matches(".+\\..+")) {
@@ -98,37 +102,60 @@ public class AvatarExpressionAttribute {
blockString = splitS[0];
fieldString = splitS[1];
} else {
- return false;
+ return -1;
}
block = spec.getBlockWithName(blockString);
if (block == null) {
- return false;
+ return -1;
}
blockIndex = spec.getBlockIndex(block);
int attributeIndex = block.getIndexOfAvatarAttributeWithName(fieldString);
+ shift = 0;
+ mask = 0xFFFFFFFF;
+
if (attributeIndex == -1) {
- // state?
- state = block.getStateMachine().getStateWithName(fieldString);
- if (state == null) {
- return false;
+ attributeIndex = block.getIndexOfConstantWithName(fieldString);
+ if (attributeIndex == -1) {
+ // state?
+ state = block.getStateMachine().getStateWithName(fieldString);
+ if (state == null) {
+ return -1;
+ }
+ isState = true;
+ accessIndex = block.getStateMachine().getIndexOfState((AvatarStateElement) state);
+ } else {
+ accessIndex = attributeIndex;
+ return -2; //constant
}
- isState = true;
- accessIndex = block.getStateMachine().getIndexOfState((AvatarStateElement) state);
} else {
- accessIndex = attributeIndex + SpecificationBlock.ATTR_INDEX;
+ int offset = block.getBooleanOffset();
+ int optRatio = block.getAttributeOptRatio();
+ if (offset == -1 || attributeIndex < offset) {
+ accessIndex = attributeIndex / optRatio + SpecificationBlock.ATTR_INDEX;
+ shift = (attributeIndex % optRatio) * (32 / optRatio);
+ if (optRatio == 2) {
+ mask = 0xFFFF;
+ } else if (optRatio == 4) {
+ mask = 0xFF;
+ }
+ } else {
+ accessIndex = SpecificationBlock.ATTR_INDEX + (offset + optRatio - 1) / optRatio + ((attributeIndex - offset) / 32);
+ shift = (attributeIndex - offset) % 32;
+ mask = 1;
+ }
}
- return true;
+ return 0;
}
- private boolean initAttributes(AvatarBlock block) {
+ private int initAttributes(AvatarBlock block) {
//Extract Attribute
if (block == null) {
- return false;
+ return -1;
}
this.block = block;
@@ -136,22 +163,56 @@ public class AvatarExpressionAttribute {
int attributeIndex = block.getIndexOfAvatarAttributeWithName(s);
+ shift = 0;
+ mask = 0xFFFFFFFF;
+
if (attributeIndex == -1) {
- // state?
- state = block.getStateMachine().getStateWithName(s);
- if (state == null) {
- return false;
+ attributeIndex = block.getIndexOfConstantWithName(s);
+ if (attributeIndex == -1) {
+ // state?
+ state = block.getStateMachine().getStateWithName(s);
+ if (state == null) {
+ return -1;
+ }
+ isState = true;
+ accessIndex = block.getStateMachine().getIndexOfState((AvatarStateElement) state);
+ } else {
+ accessIndex = attributeIndex;
+ return -2; //constant
}
- isState = true;
- accessIndex = block.getStateMachine().getIndexOfState((AvatarStateElement) state);
} else {
- accessIndex = attributeIndex + SpecificationBlock.ATTR_INDEX;
+ int offset = block.getBooleanOffset();
+ int optRatio = block.getAttributeOptRatio();
+ if (offset == -1 || attributeIndex < offset) {
+ accessIndex = attributeIndex / optRatio + SpecificationBlock.ATTR_INDEX;
+ shift = (attributeIndex % optRatio) * (32 / optRatio);
+ if (optRatio == 2) {
+ mask = 0xFFFF;
+ } else if (optRatio == 4) {
+ mask = 0xFF;
+ }
+ } else {
+ accessIndex = SpecificationBlock.ATTR_INDEX + (offset + optRatio - 1) / optRatio + ((attributeIndex - offset) / 32);
+ shift = (attributeIndex - offset) % 32;
+ mask = 1;
+ }
}
- return true;
+ return 0;
}
public boolean hasError() {
- return error == true;
+ return error == -1;
+ }
+
+ public boolean isConstant() {
+ return error == -2;
+ }
+
+ public AvatarAttribute getConstAttribute() {
+ if (error == -2) {
+ return block.getConstantWithIndex(accessIndex);
+ }
+ return null;
}
public int getValue(SpecificationState ss) {
@@ -168,7 +229,7 @@ public class AvatarExpressionAttribute {
}
}
- value = ss.blocks[blockIndex].values[accessIndex];
+ value = (ss.blocks[blockIndex].values[accessIndex] >> shift) & mask;
return value;
}
@@ -180,7 +241,7 @@ public class AvatarExpressionAttribute {
return (state == asme) ? 1 : 0;
}
- value = ss.blocks[blockIndex].values[accessIndex];
+ value = (ss.blocks[blockIndex].values[accessIndex] >> shift) & mask;
return value;
}
@@ -199,7 +260,7 @@ public class AvatarExpressionAttribute {
}
}
- value = sb.values[accessIndex];
+ value = (sb.values[accessIndex] >> shift) & mask;
return value;
}
@@ -208,37 +269,34 @@ public class AvatarExpressionAttribute {
int value;
if (isState) {
- return 0;
+ return 0;
}
//Cancel offset based on Specification Blocks
- value = attributesValues[accessIndex - SpecificationBlock.ATTR_INDEX];
+ value = (attributesValues[accessIndex - SpecificationBlock.ATTR_INDEX] >> shift) & mask;
return value;
}
- public void setValue(SpecificationState ss, int value) {
- int v;
-
+ public void setValue(SpecificationState ss, int value) {
if (isState) {
return;
}
- v = value;
-
- ss.blocks[blockIndex].values[accessIndex] = v;
+ ss.blocks[blockIndex].values[accessIndex] = (ss.blocks[blockIndex].values[accessIndex] & (~(mask << shift))) | ((value & mask) << shift);
}
- public void setValue(SpecificationBlock sb, int value) {
- int v;
-
+ public void setValue(SpecificationBlock sb, int value) {
if (isState) {
return;
}
-
- v = value;
-
- sb.values[accessIndex] = v;
+
+// if (shift == -1) {
+// sb.values[accessIndex] = value;
+// } else {
+// sb.values[accessIndex] ^= ((-(value & 1))^ sb.values[accessIndex]) & (1 << shift);
+// }
+ sb.values[accessIndex] = (sb.values[accessIndex] & (~(mask << shift))) | ((value & mask) << shift);
}
//Link state to access index in the state machine
@@ -256,10 +314,18 @@ public class AvatarExpressionAttribute {
public int getAttributeType() {
if (isState) {
return AvatarExpressionSolver.IMMEDIATE_BOOL;
- } else if (block.getAttribute(accessIndex - SpecificationBlock.ATTR_INDEX).getType() == AvatarType.BOOLEAN) {
- return AvatarExpressionSolver.IMMEDIATE_BOOL;
+ }
+ int offset = block.getBooleanOffset();
+ int ratio = block.getAttributeOptRatio();
+ int attributeIndex = (accessIndex - SpecificationBlock.ATTR_INDEX) * ratio + shift * ratio / 32;
+ if (offset == -1 || (attributeIndex < offset)) {
+ if (block.getAttribute((accessIndex - SpecificationBlock.ATTR_INDEX)).getType() == AvatarType.BOOLEAN) {
+ return AvatarExpressionSolver.IMMEDIATE_BOOL;
+ } else {
+ return AvatarExpressionSolver.IMMEDIATE_INT;
+ }
} else {
- return AvatarExpressionSolver.IMMEDIATE_INT;
+ return AvatarExpressionSolver.IMMEDIATE_BOOL;
}
}
@@ -272,4 +338,71 @@ public class AvatarExpressionAttribute {
return s;
}
+ public static AvatarElement getElement(String s, AvatarSpecification spec) {
+ //Extract Block and Attribute
+ String[] splitS;
+ String blockString;
+ String fieldString;
+ AvatarBlock block;
+ int blockIndex;
+
+ if (spec == null) {
+ return null;
+ }
+
+ if (s.matches(".+\\..+")) {
+ splitS = s.split("\\.");
+ blockString = splitS[0];
+ fieldString = splitS[1];
+ } else {
+ return null;
+ }
+
+ block = spec.getBlockWithName(blockString);
+
+ if (block == null) {
+ return null;
+ }
+
+ blockIndex = spec.getBlockIndex(block);
+
+ int attributeIndex = block.getIndexOfAvatarAttributeWithName(fieldString);
+
+ if (attributeIndex == -1) {
+ attributeIndex = block.getIndexOfConstantWithName(fieldString);
+ if (attributeIndex == -1) {
+ // state?
+ return block.getStateMachine().getStateWithName(fieldString);
+ } else {
+ //not created for constants
+ return null;
+ }
+ } else {
+ return block.getAvatarAttributeWithName(fieldString);
+ }
+ }
+
+ public static AvatarElement getElement(String s, AvatarBlock block) {
+ //Extract Attribute
+ if (block == null) {
+ return null;
+ }
+
+
+ int attributeIndex = block.getIndexOfAvatarAttributeWithName(s);
+
+ if (attributeIndex == -1) {
+ attributeIndex = block.getIndexOfConstantWithName(s);
+ if (attributeIndex == -1) {
+ // state?
+ return block.getStateMachine().getStateWithName(s);
+ } else {
+ //not created for constants
+ return null;
+ }
+ } else {
+ return block.getAvatarAttributeWithName(s);
+ }
+ }
+
}
diff --git a/src/main/java/avatartranslator/AvatarExpressionSolver.java b/src/main/java/avatartranslator/AvatarExpressionSolver.java
index a38cf52683824e2714ecb70f931a0c4bf784cd6a..cad5b1a88667f5013b7375330d9efef81b7f6ccd 100644
--- a/src/main/java/avatartranslator/AvatarExpressionSolver.java
+++ b/src/main/java/avatartranslator/AvatarExpressionSolver.java
@@ -38,6 +38,8 @@
package avatartranslator;
+import java.util.HashMap;
+import java.util.Map;
import avatartranslator.modelchecker.SpecificationBlock;
import avatartranslator.modelchecker.SpecificationState;
@@ -65,6 +67,8 @@ public class AvatarExpressionSolver {
private int intValue;
private AvatarExpressionAttribute leaf;
+ private static Map<AvatarElement, AvatarExpressionAttribute> attributesMap;
+
public AvatarExpressionSolver() {
left = null;
@@ -95,6 +99,9 @@ public class AvatarExpressionSolver {
public boolean buildExpression(AvatarSpecification spec) {
boolean returnVal;
+ if (attributesMap == null) {
+ attributesMap = new HashMap<AvatarElement, AvatarExpressionAttribute>();
+ }
returnVal = buildExpressionRec(spec);
if (returnVal == false) {
return false;
@@ -106,6 +113,9 @@ public class AvatarExpressionSolver {
public boolean buildExpression(AvatarBlock block) {
boolean returnVal;
+ if (attributesMap == null) {
+ attributesMap = new HashMap<AvatarElement, AvatarExpressionAttribute>();
+ }
returnVal = buildExpressionRec(block);
if (returnVal == false) {
return false;
@@ -158,8 +168,22 @@ public class AvatarExpressionSolver {
isImmediateValue = IMMEDIATE_INT;
returnVal = true;
} else {
- leaf = new AvatarExpressionAttribute(spec, expression);
- returnVal = !leaf.hasError();
+ AvatarElement ae = AvatarExpressionAttribute.getElement(expression, spec);
+ if (ae != null && attributesMap.containsKey(ae)) {
+ leaf = attributesMap.get(ae);
+ returnVal = true;
+ } else {
+ leaf = new AvatarExpressionAttribute(spec, expression);
+ returnVal = !leaf.hasError();
+ if (leaf.isConstant()) {
+ AvatarAttribute attr = leaf.getConstAttribute();
+ intValue = attr.getInitialValueInInt();
+ isImmediateValue = attr.isBool() ? IMMEDIATE_BOOL : IMMEDIATE_INT;
+ leaf = null;
+ } else if (returnVal == true) {
+ attributesMap.put(ae, leaf);
+ }
+ }
}
//System.out.println("Variable " + expression + "\n");
return returnVal;
@@ -219,8 +243,22 @@ public class AvatarExpressionSolver {
isImmediateValue = IMMEDIATE_INT;
returnVal = true;
} else {
- leaf = new AvatarExpressionAttribute(block, expression);
- returnVal = !leaf.hasError();
+ AvatarElement ae = AvatarExpressionAttribute.getElement(expression, block);
+ if (ae != null && attributesMap.containsKey(ae)) {
+ leaf = attributesMap.get(ae);
+ returnVal = true;
+ } else {
+ leaf = new AvatarExpressionAttribute(block, expression);
+ returnVal = !leaf.hasError();
+ if (leaf.isConstant()) {
+ AvatarAttribute attr = leaf.getConstAttribute();
+ intValue = attr.getInitialValueInInt();
+ isImmediateValue = attr.isBool() ? IMMEDIATE_BOOL : IMMEDIATE_INT;
+ leaf = null;
+ } else if (returnVal == true) {
+ attributesMap.put(ae, leaf);
+ }
+ }
}
//System.out.println("Variable " + expression + "\n");
return returnVal;
@@ -720,6 +758,38 @@ public class AvatarExpressionSolver {
right.linkStates();
}
}
+
+
+ public static boolean containsElementAttribute(AvatarElement ae) {
+ if (attributesMap != null) {
+ return attributesMap.containsKey(ae);
+ } else {
+ return false;
+ }
+ }
+
+
+ public static AvatarExpressionAttribute getElementAttribute(AvatarElement ae) {
+ if (attributesMap != null) {
+ return attributesMap.get(ae);
+ } else {
+ return null;
+ }
+ }
+
+
+ public static void addElementAttribute(AvatarElement ae, AvatarExpressionAttribute aexa) {
+ if (attributesMap == null) {
+ attributesMap = new HashMap<AvatarElement, AvatarExpressionAttribute>();
+ }
+ attributesMap.put(ae, aexa);
+ }
+
+
+ public static void emptyAttributesMap() {
+ attributesMap = new HashMap<AvatarElement, AvatarExpressionAttribute>();
+ }
+
private boolean checkIntegrity() {
int optype, optypel, optyper;
diff --git a/src/main/java/avatartranslator/AvatarSpecification.java b/src/main/java/avatartranslator/AvatarSpecification.java
index f5de87261bfdc81597dfa3bab9d16f1ef34ca1bf..44b5770b6cce5659b93ede234bed61997af1e2d1 100644
--- a/src/main/java/avatartranslator/AvatarSpecification.java
+++ b/src/main/java/avatartranslator/AvatarSpecification.java
@@ -355,6 +355,8 @@ public class AvatarSpecification extends AvatarElement {
AvatarTransition at;
boolean returnVal;
+ AvatarExpressionSolver.emptyAttributesMap();
+
for (AvatarBlock block : getListOfBlocks()) {
AvatarStateMachine asm = block.getStateMachine();
@@ -367,6 +369,12 @@ public class AvatarSpecification extends AvatarElement {
errors.add(at);
}
}
+ if (at.hasDelay()) {
+ returnVal = at.buildDelaySolver();
+ if (returnVal == false) {
+ errors.add(at);
+ }
+ }
for (AvatarAction aa : at.getActions()) {
if (aa instanceof AvatarActionAssignment) {
returnVal = ((AvatarActionAssignment) aa).buildActionSolver(block);
@@ -426,6 +434,24 @@ public class AvatarSpecification extends AvatarElement {
addBlock(addedBlocks.get(i));
}
}
+
+ public void removeConstants() {
+ for(AvatarBlock block : blocks) {
+ block.removeConstantAttributes();
+ }
+ }
+
+ public void sortAttributes() {
+ for(AvatarBlock block: blocks) {
+ block.sortAttributes();
+ }
+ }
+
+ public void setAttributeOptRatio(int attributeOptRatio) {
+ for(AvatarBlock block: blocks) {
+ block.setAttributeOptRatio(attributeOptRatio);
+ }
+ }
//
// private void renameTimers() {
// // Check whether timers have the same name in different blocks
diff --git a/src/main/java/avatartranslator/AvatarTransition.java b/src/main/java/avatartranslator/AvatarTransition.java
index 18fc1432d4e874f956e46269592d144983d5ea33..935731cda87359024f60feb2942c12a9811a78df 100644
--- a/src/main/java/avatartranslator/AvatarTransition.java
+++ b/src/main/java/avatartranslator/AvatarTransition.java
@@ -93,10 +93,9 @@ public class AvatarTransition extends AvatarStateMachineElement {
private String minCompute = "", maxCompute = "";
private AvatarStateMachineOwner block;
-
-
-
private AvatarExpressionSolver guardSolver;
+ private AvatarExpressionSolver minDelaySolver;
+ private AvatarExpressionSolver maxDelaySolver;
private List<AvatarAction> actions; // actions on variable, or method call
@@ -106,6 +105,8 @@ public class AvatarTransition extends AvatarStateMachineElement {
this.guard = new AvatarGuardEmpty();
this.block = _block;
guardSolver = null;
+ minDelaySolver = null;
+ maxDelaySolver = null;
}
public AvatarGuard getGuard() {
@@ -113,15 +114,42 @@ public class AvatarTransition extends AvatarStateMachineElement {
}
public boolean buildGuardSolver() {
- String expr = guard.toString().replaceAll("\\[", "").trim();
- expr = expr.replaceAll("\\]", "");
- guardSolver = new AvatarExpressionSolver(expr);
- return guardSolver.buildExpression((AvatarBlock) block);
+ if (isGuarded()) {
+ String expr = guard.toString().replaceAll("\\[", "").trim();
+ expr = expr.replaceAll("\\]", "");
+ guardSolver = new AvatarExpressionSolver(expr);
+ return guardSolver.buildExpression((AvatarBlock) block);
+ }
+ return true;
+ }
+
+ public boolean buildDelaySolver() {
+ boolean result;
+ if (hasDelay()) {
+ minDelaySolver = new AvatarExpressionSolver(minDelay);
+ result = minDelaySolver.buildExpression((AvatarBlock) block);
+ if (maxDelay.trim().length() != 0) {
+ maxDelaySolver = new AvatarExpressionSolver(maxDelay);
+ result &= maxDelaySolver.buildExpression((AvatarBlock) block);
+ } else {
+ maxDelaySolver = minDelaySolver;
+ }
+ return result;
+ }
+ return true;
}
public AvatarExpressionSolver getGuardSolver() {
return guardSolver;
}
+
+ public AvatarExpressionSolver getMinDelaySolver() {
+ return minDelaySolver;
+ }
+
+ public AvatarExpressionSolver getMaxDelaySolver() {
+ return maxDelaySolver;
+ }
public void setGuard(AvatarGuard _guard) {
this.guard = _guard;
diff --git a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
index 1110313997794262fb42b2721234f131b824cac9..abf79a425ace87130d49c79c0646028ee9a050ae 100644
--- a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
+++ b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
@@ -84,6 +84,8 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
private boolean ignoreEmptyTransitions;
private boolean ignoreConcurrenceBetweenInternalActions;
private boolean ignoreInternalStates;
+ private boolean verboseInfo;
+ private int compressionFactor;
// RG
private boolean computeRG;
@@ -134,6 +136,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
initialSpec.removeCompositeStates();
//TraceManager.addDev("Before clone:\n" + initialSpec);
spec = initialSpec.advancedClone();
+ spec.removeConstants();
//TraceManager.addDev("After clone:\n" + spec);
}
ignoreEmptyTransitions = true;
@@ -150,6 +153,8 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
timeLimit = 500;
counterexample = false;
freeIntermediateStateCoding = true;
+ verboseInfo = true;
+ compressionFactor = 1;
}
public AvatarSpecification getInitialSpec() {
@@ -211,6 +216,16 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
ignoreInternalStates = _b;
}
+ public void setCompressionFactor(int compressionFactor) {
+ if (compressionFactor == 2 || compressionFactor == 4) {
+ this.compressionFactor = compressionFactor;
+ spec.sortAttributes();
+ spec.setAttributeOptRatio(compressionFactor);
+ } else {
+ compressionFactor = 1;
+ }
+ }
+
public void setCheckNoDeadlocks(boolean _checkNoDeadlocks) {
checkNoDeadlocks = _checkNoDeadlocks;
deadlockStop = false;
@@ -362,7 +377,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
return counterTraceReport.toString();
}
- public List<String> getAUTTraces() {
+ public List<CounterexampleQueryReport> getAUTTraces() {
if (counterTrace == null) {
return null;
}
@@ -420,6 +435,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
studyRI = studyReinit;
genRG = computeRG;
genTrace = counterexample;
+ verboseInfo = false;
//then compute livenesses
computeRG = false;
@@ -522,6 +538,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
if (studyR || genRG) {
if (genRG) {
deadlocks = 0;
+ verboseInfo = true;
}
studyReachability = studyR;
computeRG = genRG;
@@ -730,7 +747,9 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
//TraceManager.addDev("Preparing Avatar specification :" + spec.toString());
prepareStates();
-
+
+ spec.sortAttributes();
+ spec.setAttributeOptRatio(compressionFactor);
initExpressionSolvers();
prepareTransitions();
@@ -933,13 +952,14 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
if (counterexample) {
counterTrace.reset();
traceStates = Collections.synchronizedMap(new HashMap<Integer, CounterexampleTraceState>());
+ verboseInfo = true;
}
}
private void generateCounterexample() {
if (counterexample && counterTrace.hasCounterexample()) {
- counterTrace.buildTrace();
+ counterTrace.buildTrace(states, traceStates);
if (studySafety) {
counterTraceReport.append("Trace for " + safety.getRawProperty() + "\n");
counterTraceReport.append(counterTrace.generateSimpleTrace(states) + "\n\n");
@@ -951,17 +971,18 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
if (studySafety) {
counterTrace.generateTraceAUT(safety.getRawProperty(), states);
} else if (deadlockStop) {
- counterTrace.generateTraceAUT("No Deadlocks", states);
+ counterTrace.generateTraceAUT("No Deadlocks?", states);
}
}
}
+ verboseInfo = false;
}
- private void prepareTransitionsOfState(SpecificationState _ss) {
+ private ArrayList<SpecificationTransition> prepareTransitionsOfState(SpecificationState _ss) {
int cpt;
- _ss.transitions = new ArrayList<SpecificationTransition>();
+ ArrayList<SpecificationTransition> transitions = new ArrayList<SpecificationTransition>();
//TraceManager.addDev("Preparing transitions of state " + _ss);
@@ -976,12 +997,14 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
for (AvatarStateMachineElement elt : ase.getNexts()) {
if (elt instanceof AvatarTransition) {
- handleAvatarTransition((AvatarTransition) elt, block, sb, cpt, _ss.transitions, ase.getNexts().size() > 1);
+ handleAvatarTransition((AvatarTransition) elt, block, sb, cpt, transitions, ase.getNexts().size() > 1);
}
}
cpt++;
}
+
+ return transitions;
}
@@ -993,10 +1016,10 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
return;
}
- prepareTransitionsOfState(_ss);
+ ArrayList<SpecificationTransition> transitions = prepareTransitionsOfState(_ss);
- if (_ss.transitions == null) {
+ if (transitions == null) {
TraceManager.addDev("null transitions");
nbOfDeadlocks++;
checkPropertyOnDeadlock(_ss);
@@ -1005,7 +1028,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
}
//TraceManager.addDev("Possible transitions 1:" + transitions.size());
- ArrayList<SpecificationTransition> transitions = computeValidTransitions(_ss.transitions);
+ transitions = computeValidTransitions(transitions);
//TraceManager.addDev("Possible transitions 3:" + transitions.size());
@@ -1095,8 +1118,10 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
// Compute the hash of the new state, and create the link to the right next state
SpecificationLink link = new SpecificationLink();
link.originState = _ss;
- action += " [" + tr.clockMin + "..." + tr.clockMax + "]";
- link.action = action;
+ if (verboseInfo) {
+ action += " [" + tr.clockMin + "..." + tr.clockMax + "]";
+ link.action = action;
+ }
newState.computeHash(blockValues);
//SpecificationState similar = states.get(newState.getHash(blockValues));
@@ -1166,8 +1191,6 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
if (freeIntermediateStateCoding) {
_ss.freeUselessAllocations();
- } else {
- _ss.finished();
}
mustStop();
@@ -1199,8 +1222,10 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
if (similar != null) {
SpecificationLink link = new SpecificationLink();
link.originState = _ss;
- action += " [" + st.clockMin + "..." + st.clockMax + "]";
- link.action = action;
+ if (verboseInfo) {
+ action += " [" + st.clockMin + "..." + st.clockMax + "]";
+ link.action = action;
+ }
link.destinationState = similar;
nbOfLinks++;
_ss.addNext(link);
@@ -1210,8 +1235,10 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
//already elaborated, add that state
SpecificationLink link = new SpecificationLink();
link.originState = _ss;
- action += " [" + "0...0" + "]";
- link.action = action;
+ if (verboseInfo) {
+ action += " [" + "0...0" + "]";
+ link.action = action;
+ }
link.destinationState = newState;
synchronized (this) {
similar = states.get(newState.getHash(blockValues));
@@ -1250,8 +1277,10 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
similar = findSimilarState(newState);
SpecificationLink link = new SpecificationLink();
link.originState = _ss;
- action += " [" + st.clockMin + "..." + st.clockMax + "]";
- link.action = action;
+ if (verboseInfo) {
+ action += " [" + st.clockMin + "..." + st.clockMax + "]";
+ link.action = action;
+ }
if (similar != null) {
link.destinationState = similar;
} else {
@@ -1268,9 +1297,9 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
// Compute next transition
//prepareTransitionsOfState(previousState);
- prepareTransitionsOfState(newState);
+ ArrayList<SpecificationTransition> transitions = prepareTransitionsOfState(newState);
- if (newState.transitions == null) {
+ if (transitions == null) {
TraceManager.addDev("null transitions");
nbOfDeadlocks++;
checkPropertyOnDeadlock(_ss);
@@ -1278,7 +1307,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
return;
}
- ArrayList<SpecificationTransition> transitions = computeValidTransitions(newState.transitions);
+ transitions = computeValidTransitions(transitions);
st = null;
if (ignoreConcurrenceBetweenInternalActions) {
@@ -1300,8 +1329,10 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
//Creating new link
SpecificationLink link = new SpecificationLink();
link.originState = _ss;
- action += " [" + "0...0" + "]";
- link.action = action;
+ if (verboseInfo) {
+ action += " [" + "0...0" + "]";
+ link.action = action;
+ }
synchronized (this) {
similar = states.get(newState.getHash(blockValues));
if (similar == null) {
@@ -1347,8 +1378,6 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
if (freeIntermediateStateCoding) {
_ss.freeUselessAllocations();
- } else {
- _ss.finished();
}
mustStop();
@@ -1364,13 +1393,13 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
ArrayList<Integer> stackStates = new ArrayList<>(); //keeps track of the block hashes
do {
- prepareTransitionsOfState(prevState);
+ ArrayList<SpecificationTransition> transitions = prepareTransitionsOfState(prevState);
- if (prevState.transitions == null) {
+ if (transitions == null) {
return prevState;
}
- ArrayList<SpecificationTransition> transitions = computeValidTransitions(prevState.transitions);
+ transitions = computeValidTransitions(transitions);
stackStates.add(prevState.hashValue);
found = false;
@@ -1476,13 +1505,13 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
if ((minDelay == null) || (minDelay.length() == 0)) {
st.clockMin = 0 - _sb.values[SpecificationBlock.CLOCKMAX_INDEX];
} else {
- st.clockMin = evaluateIntExpression(_at.getMinDelay(), _block, _sb) - _sb.values[SpecificationBlock.CLOCKMAX_INDEX];
+ st.clockMin = _at.getMinDelaySolver().getResult(_sb) - _sb.values[SpecificationBlock.CLOCKMAX_INDEX];
}
String maxDelay = _at.getMaxDelay().trim();
if ((maxDelay == null) || (maxDelay.length() == 0)) {
st.clockMax = 0 - _sb.values[SpecificationBlock.CLOCKMIN_INDEX];
} else {
- int resMax = evaluateIntExpression(_at.getMaxDelay(), _block, _sb);
+ int resMax = _at.getMaxDelaySolver().getResult(_sb);
_sb.maxClock = Math.max(_sb.maxClock, resMax);
st.clockMax = resMax - _sb.values[SpecificationBlock.CLOCKMIN_INDEX];
}
diff --git a/src/main/java/avatartranslator/modelchecker/CounterexampleQueryReport.java b/src/main/java/avatartranslator/modelchecker/CounterexampleQueryReport.java
new file mode 100644
index 0000000000000000000000000000000000000000..260d42048594ff00b842f897c63aeb2562726aa5
--- /dev/null
+++ b/src/main/java/avatartranslator/modelchecker/CounterexampleQueryReport.java
@@ -0,0 +1,39 @@
+package avatartranslator.modelchecker;
+
+public class CounterexampleQueryReport {
+ private String name;
+ private String query;
+ private String report;
+
+ public CounterexampleQueryReport(String name) {
+ this.name = name;
+ }
+
+ public CounterexampleQueryReport(String name, String query) {
+ this.name = name;
+ this.query = query;
+ }
+
+ public CounterexampleQueryReport(String name, String query, String report) {
+ this.name = name;
+ this.query = query;
+ this.report = report;
+ }
+
+ public String getName() {
+ return this.name;
+ }
+
+ public String getQuery() {
+ return this.query;
+ }
+
+ public String getReport() {
+ return this.report;
+ }
+
+ public void setReport(String report) {
+ this.report = report;
+ }
+
+}
diff --git a/src/main/java/avatartranslator/modelchecker/CounterexampleTrace.java b/src/main/java/avatartranslator/modelchecker/CounterexampleTrace.java
index 028eeab1292e1525c2e9ea1452d8101d1327fd8f..ab127305cd0ca0122dfee1d5448a17748e3d2e99 100644
--- a/src/main/java/avatartranslator/modelchecker/CounterexampleTrace.java
+++ b/src/main/java/avatartranslator/modelchecker/CounterexampleTrace.java
@@ -2,19 +2,20 @@ package avatartranslator.modelchecker;
import java.util.ArrayList;
import java.util.HashMap;
+import java.util.HashSet;
import java.util.LinkedList;
import java.util.List;
import java.util.Map;
-
+import java.util.Set;
import avatartranslator.AvatarBlock;
import avatartranslator.AvatarSpecification;
-import avatartranslator.AvatarStateMachine;
+
public class CounterexampleTrace {
private LinkedList<CounterexampleTraceState> trace;
private CounterexampleTraceState counterexampleState;
private AvatarSpecification spec;
- private List<String> autTraces;
+ private List<CounterexampleQueryReport> autTraces;
public CounterexampleTrace(AvatarSpecification spec) {
@@ -41,7 +42,7 @@ public class CounterexampleTrace {
}
- public List<String> getAUTTrace() {
+ public List<CounterexampleQueryReport> getAUTTrace() {
return autTraces;
}
@@ -78,6 +79,70 @@ public class CounterexampleTrace {
}
+ public boolean buildTrace(Map<Integer, SpecificationState> states, Map<Integer, CounterexampleTraceState> counterstates) {
+ if (counterexampleState == null) {
+ return false;
+ }
+
+ trace = new LinkedList<CounterexampleTraceState>();
+
+ CounterexampleTraceState cs = counterexampleState;
+ CounterexampleTraceState loopPoint = counterstates.get(counterexampleState.hash);
+
+ if (loopPoint != null) {
+ //search for a loop
+ boolean loop = false;
+ while (cs.father != null) {
+ cs = cs.father;
+ if (cs == loopPoint) {
+ loop = true;
+ }
+ }
+ if (loop == true) {
+ //registered path contains a loop
+ cs = counterexampleState;
+ trace.add(cs);
+ while (cs.father != null) {
+ cs = cs.father;
+ trace.add(0, cs);
+ }
+ } else {
+ //registered path does not contain a loop
+ cs = loopPoint;
+ trace.add(cs);
+ while (cs.father != null) {
+ cs = cs.father;
+ trace.add(0, cs);
+ }
+ List<SpecificationState> loopTrace = findLoopTrace(states.get(loopPoint.hash));
+ if (loopTrace != null) {
+ //integrate
+ for (SpecificationState ss : loopTrace) {
+ trace.add(counterstates.get(ss.hashValue));
+ }
+ } else {
+ //continue normally
+ int pos = trace.size();
+ cs = counterexampleState;
+ while (cs.father != loopPoint) {
+ cs = cs.father;
+ trace.add(pos, cs);
+ }
+ }
+ }
+ } else {
+ //normal trace
+ trace.add(cs);
+ while (cs.father != null) {
+ cs = cs.father;
+ trace.add(0, cs);
+ }
+ }
+
+ return true;
+ }
+
+
public String toString() {
if (trace == null) {
return "";
@@ -138,7 +203,7 @@ public class CounterexampleTrace {
int id = 0;
SpecificationState state = null;
for (CounterexampleTraceState cs : trace) {
- if (state != null) {
+ if (state != null && state.nexts != null) {
for (SpecificationLink sl : state.nexts) {
if (sl.destinationState.hashValue == cs.hash) {
s.append("Transition " + sl.action + "\n");
@@ -158,13 +223,13 @@ public class CounterexampleTrace {
return s.toString();
}
- public void generateTraceAUT(String name, Map<Integer, SpecificationState> states) {
+ public void generateTraceAUT(String query, Map<Integer, SpecificationState> states) {
if (trace == null) {
return;
}
if (autTraces == null) {
- autTraces = new ArrayList<String>();
+ autTraces = new ArrayList<CounterexampleQueryReport>();
}
List<AvatarBlock> blocks = spec.getListOfBlocks();
@@ -200,8 +265,42 @@ public class CounterexampleTrace {
s.insert(0 ,"des(0," + (trace.size() - 1) + "," + statesID.size() + ")\n");
+ CounterexampleQueryReport cr = new CounterexampleQueryReport(null, query, s.toString());
+ autTraces.add(cr);
+ }
+
+ private List<SpecificationState> findLoopTrace(SpecificationState start) {
+ Set<Long> visited= new HashSet<Long>();
+ List<SpecificationState> loopTrace = new ArrayList<>();
+
+ if (!(start.getNextsSize() == 0 || visited.contains(start.id))) {
+ for (SpecificationLink i : start.nexts) {
+ if(findLoopTraceRec(i.destinationState, start, visited, loopTrace, 0)) {
+ return loopTrace;
+ }
+ }
+ }
+
+ return null;
+ }
+
+ private boolean findLoopTraceRec(SpecificationState start, SpecificationState arrival, Set<Long> visited, List<SpecificationState> loopTrace, int depth) {
+ loopTrace.add(depth, start);
+
+ if (start == arrival) {
+ return true;
+ } else if (start.getNextsSize() == 0 || visited.contains(start.id)) {
+ return false;
+ }
- autTraces.add(s.toString());
+ visited.add(start.id);
+ for (SpecificationLink i : start.nexts) {
+ if (findLoopTraceRec(i.destinationState, arrival, visited, loopTrace, depth + 1)) {
+ return true;
+ }
+ }
+ loopTrace.remove(depth);
+ return false;
}
}
diff --git a/src/main/java/avatartranslator/modelchecker/SpecificationBlock.java b/src/main/java/avatartranslator/modelchecker/SpecificationBlock.java
index e632831482d6ae0c184f2c506da4497c00c09a2e..24fae0af3bb32e456a66b624b376977416231043 100644
--- a/src/main/java/avatartranslator/modelchecker/SpecificationBlock.java
+++ b/src/main/java/avatartranslator/modelchecker/SpecificationBlock.java
@@ -62,10 +62,7 @@ public class SpecificationBlock {
public static final int ATTR_INDEX = 3;
public int [] values; // state in block, clockmin, clockmax, variables
- public int maxClock;
-
- public AvatarBlock block;
-
+ public int maxClock;
public SpecificationBlock() {
}
@@ -84,11 +81,21 @@ public class SpecificationBlock {
return Arrays.hashCode(values);
}
- public void init(AvatarBlock _block, boolean _ignoreEmptyTransitions) {
+ public void init(AvatarBlock _block, boolean _ignoreEmptyTransitions, boolean compress) {
List<AvatarAttribute> attrs = _block.getAttributes();
//TraceManager.addDev("Nb of attributes:" + attrs.size());
//TraceManager.addDev("in block=" + _block.toString());
- values = new int[HEADER_VALUES+attrs.size()];
+ int booleanIndex = _block.getBooleanOffset();
+ int optRatio = _block.getAttributeOptRatio();
+ if (!compress || booleanIndex == -1) {
+ values = new int[HEADER_VALUES+attrs.size()];
+ } else {
+ if (optRatio > 1) {
+ values = new int[HEADER_VALUES+(booleanIndex+optRatio-1)/optRatio+((attrs.size()-booleanIndex+31)/32)];
+ } else {
+ values = new int[HEADER_VALUES+booleanIndex+((attrs.size()-booleanIndex+31)/32)];
+ }
+ }
// Initial state
if (_ignoreEmptyTransitions) {
@@ -104,9 +111,33 @@ public class SpecificationBlock {
// Attributes
int cpt = HEADER_VALUES;
//String initial;
- for(AvatarAttribute attr: attrs) {
- values[cpt++] = attr.getInitialValueInInt();
- }
+ if (!compress) {
+ for(AvatarAttribute attr: attrs) {
+ values[cpt++] = attr.getInitialValueInInt();
+ }
+ } else {
+ int i = 0;
+ for(AvatarAttribute attr: attrs) {
+ if (i < booleanIndex) {
+ if (i % optRatio == 0) {
+ values[cpt] = attr.getInitialValueInInt();
+ } else {
+ values[cpt] |= attr.getInitialValueInInt() << ((i % optRatio) * (32 / optRatio));
+ }
+ if (i % optRatio + 1 == optRatio || i + 1 == booleanIndex) {
+ cpt++;
+ }
+ } else if (((i - booleanIndex) % 32) == 0) {
+ values[cpt] = attr.getInitialValueInInt();
+ } else {
+ values[cpt] |= attr.getInitialValueInInt() << ((i - booleanIndex) % 32);
+ if (((i - booleanIndex) % 32) == 31) {
+ cpt++;
+ }
+ }
+ i++;
+ }
+ }
}
@Override
diff --git a/src/main/java/avatartranslator/modelchecker/SpecificationState.java b/src/main/java/avatartranslator/modelchecker/SpecificationState.java
index 6e72e75e54e5a9323cf7a32eccc59e80ed5e3f4b..2d4533bad7ee002d79bd774dce3ac545a067cc16 100644
--- a/src/main/java/avatartranslator/modelchecker/SpecificationState.java
+++ b/src/main/java/avatartranslator/modelchecker/SpecificationState.java
@@ -65,9 +65,8 @@ public class SpecificationState implements Comparable<SpecificationState> {
public LinkedList<SpecificationLink> nexts; // The RG is there
public boolean property; //trace the property check at this state
public boolean elaborated; //true only if the elaboration has been completed
- public ArrayList<SpecificationTransition> transitions;
-// public long distance; //max #steps to be reached from S0
+
public SpecificationState() {
hashComputed = false;
property = false;
@@ -105,7 +104,7 @@ public class SpecificationState implements Comparable<SpecificationState> {
for(AvatarBlock block: _spec.getListOfBlocks()) {
blocks[cpt] = new SpecificationBlock();
- blocks[cpt].init(block, _ignoreEmptyTransitions);
+ blocks[cpt].init(block, _ignoreEmptyTransitions, true);
cpt ++;
}
@@ -141,8 +140,8 @@ public class SpecificationState implements Comparable<SpecificationState> {
if (!(_st.hasBlockIndex(i))) {
sb.values[SpecificationBlock.CLOCKMIN_INDEX] += _st.clockMin;
sb.values[SpecificationBlock.CLOCKMAX_INDEX] += _st.clockMax;
- sb.values[SpecificationBlock.CLOCKMIN_INDEX] = Math.min(sb.values[SpecificationBlock.CLOCKMIN_INDEX], sb.maxClock);
- sb.values[SpecificationBlock.CLOCKMAX_INDEX] = Math.min(sb.values[SpecificationBlock.CLOCKMAX_INDEX], sb.maxClock);
+ sb.values[SpecificationBlock.CLOCKMIN_INDEX] = Math.min(sb.values[SpecificationBlock.CLOCKMIN_INDEX], sb.maxClock);
+ sb.values[SpecificationBlock.CLOCKMAX_INDEX] = Math.min(sb.values[SpecificationBlock.CLOCKMAX_INDEX], sb.maxClock);
} else {
sb.values[SpecificationBlock.CLOCKMIN_INDEX] = 0;
sb.values[SpecificationBlock.CLOCKMAX_INDEX] = 0;
@@ -193,14 +192,8 @@ public class SpecificationState implements Comparable<SpecificationState> {
return 0;
}
- public void finished() {
- //blocks = null;
- transitions = null;
- }
-
public void freeUselessAllocations() {
blocks = null;
- transitions = null;
}
public int compareTo( SpecificationState _s ) {
diff --git a/src/main/java/cli/Action.java b/src/main/java/cli/Action.java
index 9517a5e392ecb278aee3ac92909a47444e9cf6d1..ebee80e5eb78938988912ac20196673678d07dea 100644
--- a/src/main/java/cli/Action.java
+++ b/src/main/java/cli/Action.java
@@ -41,6 +41,7 @@ package cli;
import avatartranslator.AvatarSpecification;
import avatartranslator.modelchecker.AvatarModelChecker;
+import avatartranslator.modelchecker.CounterexampleQueryReport;
import avatartranslator.modelcheckervalidator.ModelCheckerValidator;
import common.ConfigurationTTool;
import common.SpecConfigTTool;
@@ -854,7 +855,8 @@ public class Action extends Command {
+ "-n NUM\tmaximum states created (Only for a non verification study)\n"
+ "-t NUM\tmaximum time (ms) (Only for a non verification study)\n"
+ "-c\tconsider full concurrency between actions\n"
- + "-v FILE\tsave counterexample traces for pragmas in FILE";
+ + "-v FILE\tsave counterexample traces for pragmas in FILE"
+ + "-va FILE\tsave counterexample traces and AUT graph for pragmas in FILE";
}
public String getExample() {
@@ -889,6 +891,7 @@ public class Action extends Command {
amc.setComputeRG(false);
boolean rgGraph = false;
boolean counterTraces = false;
+ boolean counterTracesAUT = false;
boolean reachabilityAnalysis = false;
boolean livenessAnalysis = false;
boolean safetyAnalysis = false;
@@ -997,6 +1000,16 @@ public class Action extends Command {
return Interpreter.BAD;
}
break;
+ case "-va":
+ if (i != commands.length - 1) {
+ counterPath = commands[++i];
+ amc.setCounterExampleTrace(true, true);
+ counterTraces = true;
+ counterTracesAUT = true;
+ } else {
+ return Interpreter.BAD;
+ }
+ break;
default:
return Interpreter.BAD;
}
@@ -1031,17 +1044,40 @@ public class Action extends Command {
if (counterTraces) {
String trace = amc.getCounterTrace();
- String autfile;
+ String file;
if (counterPath.indexOf("$") != -1) {
- autfile = Conversion.replaceAllChar(counterPath, '$', dateAndTime);
+ file = Conversion.replaceAllChar(counterPath, '$', dateAndTime);
} else {
- autfile = counterPath;
+ file = counterPath;
}
try {
- FileUtils.saveFile(autfile, trace);
- System.out.println("\nCounterexample trace saved in " + autfile + "\n");
+ File f = new File(file);
+ FileUtils.saveFile(file, trace);
+ System.out.println("\nCounterexample trace saved in " + file + "\n");
} catch (Exception e) {
- System.out.println("\nCounterexample trace could not be saved in " + autfile + "\n");
+ System.out.println("\nCounterexample trace could not be saved in " + file + "\n");
+ }
+
+ List<CounterexampleQueryReport> autTraces = amc.getAUTTraces();
+ if (autTraces != null) {
+ int i = 0;
+ String autfile = FileUtils.removeFileExtension(file);
+ for (CounterexampleQueryReport tr : autTraces) {
+ String filename = autfile + "_" + i + ".aut";
+ try {
+ RG rg = new RG(file);
+ rg.data = tr.getReport();
+ rg.fileName = filename;
+ rg.name = tr.getQuery();
+ interpreter.mgui.addRG(rg);
+ File f = new File(filename);
+ FileUtils.saveFile(filename, tr.getReport());
+ System.out.println("Counterexample graph trace " + tr.getQuery() + " saved in " + filename + "\n");
+ } catch (Exception e) {
+ System.out.println("Counterexample graph trace "+ tr.getQuery() + " could not be saved in " + filename + "\n");
+ }
+ i++;
+ }
}
}
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 b87cbad030eb80013763c2e4131096f96d756c4e..a6ed7ed783a67869815f1b4c75a85adc5a65f290 100644
--- a/src/main/java/tmltranslator/toavatar/FullTML2Avatar.java
+++ b/src/main/java/tmltranslator/toavatar/FullTML2Avatar.java
@@ -1,51 +1,52 @@
/* ludovic.apvrille AT enst.fr
-*
-* This software is a computer program whose purpose is to allow the
-* edition of TURTLE analysis, design and deployment diagrams, to
-* allow the generation of RT-LOTOS or Java code from this diagram,
-* and at last to allow the analysis of formal validation traces
-* obtained from external tools, e.g. RTL from LAAS-CNRS and CADP
-* from INRIA Rhone-Alpes.
-*
-* This software is governed by the CeCILL license under French law and
-* abiding by the rules of distribution of free software. You can use,
-* modify and/ or redistribute the software under the terms of the CeCILL
-* license as circulated by CEA, CNRS and INRIA at the following URL
-* "http://www.cecill.info".
-*
-* As a counterpart to the access to the source code and rights to copy,
-* modify and redistribute granted by the license, users are provided only
-* with a limited warranty and the software's author, the holder of the
-* economic rights, and the successive licensors have only limited
-* liability.
-*
-* In this respect, the user's attention is drawn to the risks associated
-* with loading, using, modifying and/or developing or reproducing the
-* software by the user in light of its specific status of free software,
-* that may mean that it is complicated to manipulate, and that also
-* therefore means that it is reserved for developers and experienced
-* professionals having in-depth computer knowledge. Users are therefore
-* encouraged to load and test the software's suitability as regards their
-* requirements in conditions enabling the security of their systems and/or
-* data to be ensured and, more generally, to use and operate it in the
-* same conditions as regards security.
-*
-* The fact that you are presently reading this means that you have had
-* knowledge of the CeCILL license and that you accept its terms.
-*/
+ *
+ * This software is a computer program whose purpose is to allow the
+ * edition of TURTLE analysis, design and deployment diagrams, to
+ * allow the generation of RT-LOTOS or Java code from this diagram,
+ * and at last to allow the analysis of formal validation traces
+ * obtained from external tools, e.g. RTL from LAAS-CNRS and CADP
+ * from INRIA Rhone-Alpes.
+ *
+ * This software is governed by the CeCILL license under French law and
+ * abiding by the rules of distribution of free software. You can use,
+ * modify and/ or redistribute the software under the terms of the CeCILL
+ * license as circulated by CEA, CNRS and INRIA at the following URL
+ * "http://www.cecill.info".
+ *
+ * As a counterpart to the access to the source code and rights to copy,
+ * modify and redistribute granted by the license, users are provided only
+ * with a limited warranty and the software's author, the holder of the
+ * economic rights, and the successive licensors have only limited
+ * liability.
+ *
+ * In this respect, the user's attention is drawn to the risks associated
+ * with loading, using, modifying and/or developing or reproducing the
+ * software by the user in light of its specific status of free software,
+ * that may mean that it is complicated to manipulate, and that also
+ * therefore means that it is reserved for developers and experienced
+ * professionals having in-depth computer knowledge. Users are therefore
+ * encouraged to load and test the software's suitability as regards their
+ * requirements in conditions enabling the security of their systems and/or
+ * data to be ensured and, more generally, to use and operate it in the
+ * same conditions as regards security.
+ *
+ * The fact that you are presently reading this means that you have had
+ * knowledge of the CeCILL license and that you accept its terms.
+ */
package tmltranslator.toavatar;
import avatartranslator.*;
import myutil.TraceManager;
-import proverifspec.ProVerifQueryResult;
import tmltranslator.*;
import ui.TGComponent;
-import ui.tmlad.*;
import ui.tmlcompd.TMLCPrimitivePort;
-import java.util.*;
+import java.util.ArrayList;
+import java.util.HashMap;
+import java.util.List;
+import java.util.Map;
import java.util.regex.Matcher;
import java.util.regex.Pattern;
@@ -57,7 +58,11 @@ import java.util.regex.Pattern;
* @version 2.0 19/06/2020
*/
public class FullTML2Avatar {
- private TMLMapping<?> tmlmap;
+ private final static String NOTIFIED = "_NOTIFIED";
+
+
+
+ //private TMLMapping<?> tmlmap;
private TMLModeling<?> tmlmodel;
private Map<SecurityPattern, List<AvatarAttribute>> symKeys = new HashMap<SecurityPattern, List<AvatarAttribute>>();
@@ -90,1017 +95,721 @@ public class FullTML2Avatar {
boolean mc = true;
boolean security = false;
- public FullTML2Avatar(TMLMapping<?> tmlmap) {
- this.tmlmap = tmlmap;
-
- this.tmlmodel = tmlmap.getTMLModeling();
+ public FullTML2Avatar(TMLModeling<?> tmlmodel) {
+ this.tmlmodel = tmlmodel;
-
allStates = new ArrayList<String>();
attrsToCheck = new ArrayList<String>();
}
- public void checkConnections() {
- List<HwLink> links = tmlmap.getTMLArchitecture().getHwLinks();
- for (TMLTask t1 : tmlmodel.getTasks()) {
- List<SecurityPattern> keys = new ArrayList<SecurityPattern>();
- accessKeys.put(t1, keys);
-
- HwExecutionNode node1 = tmlmap.getHwNodeOf(t1);
- //Try to find memory using only private buses from origin
- List<HwNode> toVisit = new ArrayList<HwNode>();
- //List<HwNode> toMemory = new ArrayList<HwNode>();
- List<HwNode> complete = new ArrayList<HwNode>();
- for (HwLink link : links) {
- if (link.hwnode == node1) {
- if (link.bus.privacy == 1) {
- toVisit.add(link.bus);
- }
- }
- }
- boolean memory = false;
- //memloop:
- while (toVisit.size() > 0) {
- HwNode curr = toVisit.remove(0);
- for (HwLink link : links) {
- if (curr == link.bus) {
- if (link.hwnode instanceof HwMemory) {
- memory = true;
- List<SecurityPattern> patterns = tmlmap.getMappedPatterns((HwMemory) link.hwnode);
- accessKeys.get(t1).addAll(patterns);
- // break memloop;
- }
- if (!complete.contains(link.hwnode) && !toVisit.contains(link.hwnode) && link.hwnode instanceof HwBridge) {
- toVisit.add(link.hwnode);
- }
- } else if (curr == link.hwnode) {
- if (!complete.contains(link.bus) && !toVisit.contains(link.bus) && link.bus.privacy == 1) {
- toVisit.add(link.bus);
- }
- }
- }
- complete.add(curr);
+
+ public AvatarSpecification generateAvatarSpec(String _loopLimit) {
+
+ //TraceManager.addDev("security patterns " + tmlmodel.secPatterns);
+ //TraceManager.addDev("keys " + tmlmap.mappedSecurity);
+
+
+ //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();
+
+// System.out.println("MODIFIED model " + tmlmodel);
+
+ for (TMLChannel chan : tmlmodel.getChannels()) {
+ //System.out.println("chan " + chan);
+ TMLTask task = chan.getOriginTask();
+ TMLTask task2 = chan.getDestinationTask();
+
+ if (chan.getName().contains("fork__") || chan.getName().contains("FORKCHANNEL")) {
+ chan.setName(chan.getName().replaceAll("__", ""));
}
+ }
- //Find path to secure memory from destination node
+ //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;
+ }
+ }
- for (TMLTask t2 : tmlmodel.getTasks()) {
- HwExecutionNode node2 = tmlmap.getHwNodeOf(t2);
- if (!memory) {
- //There is no path to a private memory
- originDestMap.put(t1.getName() + "__" + t2.getName(), channelPublic);
- } else if (node1 == node2) {
+ 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);
+ }
- originDestMap.put(t1.getName() + "__" + t2.getName(), channelPrivate);
- } else {
- //Navigate architecture for node
-
- //HwNode last = node1;
- List<HwNode> found = new ArrayList<HwNode>();
- List<HwNode> done = new ArrayList<HwNode>();
- List<HwNode> path = new ArrayList<HwNode>();
- Map<HwNode, List<HwNode>> pathMap = new HashMap<HwNode, List<HwNode>>();
- for (HwLink link : links) {
- if (link.hwnode == node1) {
- found.add(link.bus);
- List<HwNode> tmp = new ArrayList<HwNode>();
- tmp.add(link.bus);
- pathMap.put(link.bus, tmp);
- }
- }
- outerloop:
- while (found.size() > 0) {
- HwNode curr = found.remove(0);
- for (HwLink link : links) {
- if (curr == link.bus) {
- if (link.hwnode == node2) {
- path = pathMap.get(curr);
- break outerloop;
- }
- if (!done.contains(link.hwnode) && !found.contains(link.hwnode) && link.hwnode instanceof HwBridge) {
- found.add(link.hwnode);
- List<HwNode> tmp = new ArrayList<HwNode>(pathMap.get(curr));
- tmp.add(link.hwnode);
- pathMap.put(link.hwnode, tmp);
- }
- } else if (curr == link.hwnode) {
- if (!done.contains(link.bus) && !found.contains(link.bus)) {
- found.add(link.bus);
- List<HwNode> tmp = new ArrayList<HwNode>(pathMap.get(curr));
- tmp.add(link.bus);
- pathMap.put(link.bus, tmp);
- }
- }
- }
- done.add(curr);
- }
- if (path.size() == 0) {
- originDestMap.put(t1.getName() + "__" + t2.getName(), channelUnreachable);
- } else {
- int priv = 1;
- HwBus bus;
- //Check if all buses and bridges are private
- for (HwNode n : path) {
- if (n instanceof HwBus) {
- bus = (HwBus) n;
- if (bus.privacy == 0) {
- priv = 0;
- break;
- }
- }
- }
- originDestMap.put(t1.getName() + "__" + t2.getName(), priv);
- }
- }
+ 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();
- /* public void checkChannels(){
- List<TMLChannel> channels = tmlmodel.getChannels();
- List<TMLTask> destinations = new ArrayList<TMLTask>();
- TMLTask a;
- for (TMLChannel channel: channels){
- destinations.clear();
- if (channel.isBasicChannel()){
- a = channel.getOriginTask();
- destinations.add(channel.getDestinationTask());
+ //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);
}
- else {
- a=channel.getOriginTasks().get(0);
- destinations.addAll(channel.getDestinationTasks());
- }
- HwExecutionNode node1 = tmlmap.getHwNodeOf(a);
- for (TMLTask t: destinations){
- //List<HwBus> buses = new ArrayList<HwBus>();
- HwNode node2 = tmlmap.getHwNodeOf(t);
-
- //Check if each node has a secure path to memory
-
-
-
-
- if (node1==node2){
- channelMap.put(channel, channelPrivate);
- }
+ }*/
- if (node1!=node2){
- //Navigate architecture for node
- List<HwLink> links = tmlmap.getTMLArchitecture().getHwLinks();
- //HwNode last = node1;
- List<HwNode> found = new ArrayList<HwNode>();
- List<HwNode> done = new ArrayList<HwNode>();
- List<HwNode> path = new ArrayList<HwNode>();
- Map<HwNode, List<HwNode>> pathMap = new HashMap<HwNode, List<HwNode>>();
-
- for (HwLink link: links){
- if (link.hwnode == node1){
- found.add(link.bus);
- List<HwNode> tmp = new ArrayList<HwNode>();
- tmp.add(link.bus);
- pathMap.put(link.bus, tmp);
- }
- }
- outerloop:
- while (found.size()>0){
- HwNode curr = found.remove(0);
- for (HwLink link: links){
- if (curr == link.bus){
- if (link.hwnode == node2){
- path = pathMap.get(curr);
- break outerloop;
- }
- if (!done.contains(link.hwnode) && !found.contains(link.hwnode) && link.hwnode instanceof HwBridge){
- found.add(link.hwnode);
- List<HwNode> tmp = new ArrayList<HwNode>(pathMap.get(curr));
- tmp.add(link.hwnode);
- pathMap.put(link.hwnode, tmp);
- }
- }
- else if (curr == link.hwnode){
- if (!done.contains(link.bus) && !found.contains(link.bus)){
- found.add(link.bus);
- List<HwNode> tmp = new ArrayList<HwNode>(pathMap.get(curr));
- tmp.add(link.bus);
- pathMap.put(link.bus, tmp);
- }
- }
- }
- done.add(curr);
- }
+ for (TMLTask task : tasks) {
- if (path.size() ==0){
-
- channelMap.put(channel, channelUnreachable);
- }
- else {
- int priv=1;
- HwBus bus;
- //Check if all buses and bridges are private
- for (HwNode n: path){
- if (n instanceof HwBus){
- bus = (HwBus) n;
- if (bus.privacy ==0){
- priv=0;
- break;
- }
- }
- }
-
- channelMap.put(channel, priv);
- //TraceManager.addDev("Channel "+channel.getName() + " between Task "+ a.getTaskName() + " and Task " + t.getTaskName() + " is " + (priv==1 ? "confidential" : "not confidential"));
- }
- }
- }
- }
- TraceManager.addDev(channelMap);
- }*/
+ AvatarBlock block = taskBlockMap.get(task);
+ //Add temp variable for unsendable signals
- public List<AvatarStateMachineElement> translateState(TMLActivityElement ae, AvatarBlock block) {
+ //Add all signals
+ for (TMLChannel chan : tmlmodel.getChannels(task)) {
+ if (chan.hasOriginTask(task)) {
+ AvatarSignal sig = new AvatarSignal(chan.getOriginPort().getName(), AvatarSignal.OUT, chan.getReferenceObject());
- // 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;
+ 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);
- AvatarTransition tran = new AvatarTransition(block, "", null);
- List<AvatarStateMachineElement> elementList = new ArrayList<AvatarStateMachineElement>();
+ }
- if (ae == null) {
- return elementList;
- }
+ if (chan.hasDestinationTask(task)) {
- 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);
+ 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);
}
- //elementList.addAll(tmp);
- seq = tmp;
}
- //Put stop states on the end of the last in sequence
- for (AvatarStateMachineElement e : seq) {
- if (e.getNexts().size() == 0 && !(e instanceof AvatarStopState)) {
- AvatarStopState stop = new AvatarStopState("stop", null);
- e.addNext(stop);
- elementList.add(stop);
- }
- elementList.add(e);
- }
- return elementList;
+ // 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);
- } 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();
- }
- boolean checked = false;
- if (ae.getReferenceObject() != null) {
- checked = ((TGComponent) ae.getReferenceObject()).hasCheckedAccessibility();
- }
- 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());
- }
+ //Adding parameter
+ int cpt = 0;
+ for(TMLType tmlt: evt.getParams()) {
+ AvatarAttribute aa = new AvatarAttribute("p" + cpt, getAvatarType(tmlt), null, null);
+ sig.addParameter(aa);
+ cpt ++;
+ }
- 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 (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);
- //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);
+ //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);
+
}
+ }
- //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);
- }
- elementList.add(e);
- }
- elementList.add(stop);
- //Build branch 1
- List<AvatarStateMachineElement> set0_1 = translateState(ae.getNextElement(0), block);
- List<AvatarStateMachineElement> set1_1 = translateState(ae.getNextElement(1), block);
- for (AvatarStateMachineElement e : set1_1) {
- if (e instanceof AvatarStopState) {
- //ignore
- } else if (e.getNexts().size() == 0) {
- e.addNext(set0_1.get(0));
- elementList.add(e);
- } else if (e.getNext(0) instanceof AvatarStopState) {
- //Remove the transition to AvatarStopState
- e.removeNext(0);
- e.addNext(set0_1.get(0));
- elementList.add(e);
- } else {
- elementList.add(e);
- }
- }
- tran = new AvatarTransition(block, "__after_" + ae.getName() + "_1", 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);
+
+
+ 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);*/
+
+ AvatarAttribute loop_index = new AvatarAttribute("loop_index", AvatarType.INTEGER, block, null);
+ block.addAttribute(loop_index);
+
+ 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;
}
- elementList.add(stop);
+ AvatarAttribute avattr = new AvatarAttribute(attr.getName(), type, block, null);
+ avattr.setInitialValue(attr.getInitialValue());
+ block.addAttribute(avattr);
+ }
+ //AvatarTransition last;
+ AvatarStateMachine asm = block.getStateMachine();
- } 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);
+ //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);
+
+ //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);
+ AvatarState loopstart = new AvatarState("loopstart", task.getActivityDiagram().get(0).getReferenceObject());
+ at.addNext(loopstart);
+ asm.addElement(loopstart);
- AvatarState choiceStateEnd = new AvatarState("seqchoiceend__" + i + "_" + ae.getName().replaceAll(" ", ""), ae.getReferenceObject());
- elementList.add(choiceStateEnd);
+ //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
+ for (AvatarStateMachineElement e : elementList) {
+ e.setName(processName(e.getName(), e.getID()));
+ stateObjectMap.put(task.getName().split("__")[1] + "__" + e.getName(), e.getReferenceObject());
- //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);
+ 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);
+ }
}
+ 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());
- 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));
+ //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);
+ }*/
+ }
- 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));
+ 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));
}
- return elementList;
-
- } 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();
+ 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));
+ }
}
- boolean checked = false;
- if (ae.getReferenceObject() != null) {
- checked = ((TGComponent) ae.getReferenceObject()).hasCheckedAccessibility();
+
+ }
+
+
+ //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);
+ }
}
- 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);
+ }
+
+ //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 (channel.isBasicChannel()) {
+ TraceManager.addDev("checking channel " + channel.getName());
+ AvatarRelation ar = new AvatarRelation(channel.getName(), taskBlockMap.get(channel.getOriginTask()), taskBlockMap.get(channel.getDestinationTask()), channel.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 {
- sig = signalOutMap.get(evt.getName());
+ //Create new block, hope for best
+ if (mc) {
+ fifo = createFifo(channel.getName());
+ ar.setAsynchronous(false);
+ }
}
- 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
- sig.addParameter(block.getAvatarAttributeWithName(aee.getParam(i)));
- as.addValue(aee.getParam(i));
+ //Find in signal
+
+ 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());
- 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);
+ 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));
+ }
- } else if (ae instanceof TMLWaitEvent) {
- AvatarSignal sig;
- if (!signalInMap.containsKey(evt.getName())) {
- sig = new AvatarSignal(getName(evt.getName()), AvatarSignal.IN, evt.getReferenceObject());
- signals.add(sig);
- block.addSignal(sig);
- signalInMap.put(evt.getName(), sig);
+ 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 {
- sig = signalInMap.get(evt.getName());
+ //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());
+ }
}
- AvatarActionOnSignal as = new AvatarActionOnSignal(ae.getName(), sig, ae.getReferenceObject());
- for (int i = 0; i < aee.getNbOfParams(); i++) {
+ 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());
+ }
+ avspec.addRelation(ar);
+ }
+ }
+ }
+ }
- 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
- sig.addParameter(block.getAvatarAttributeWithName(aee.getParam(i)));
- as.addValue(aee.getParam(i));
+ 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);
+ }
}
}
+ //Find out signal
+ for (AvatarSignal sig : signals) {
+ if (sig.getInOut() == AvatarSignal.OUT) {
+ String name = sig.getName();
- 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);
+ 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());
+ }
+
+ ar.setAsynchronous(false);
+ avspec.addRelation(ar);
}
+ }
- } 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);
+ for (TMLEvent event : tmlmodel.getEvents()) {
- 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
+ TraceManager.addDev("Handling Event:" + event.getName() + " 1:" + taskBlockMap.get(event.getOriginTask()) + " 2:" + taskBlockMap.get
+ (event.getDestinationTask()));
- //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));
+ // For each event, we create a FIFO, and so a double relation
- 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 (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
- //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));
+ 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);
- 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));
+ 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));
- 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 (event.isBlocking()) {
+ ar.setAsynchronous(true);
+ ar.setBlocking(true);
+ ar.setSizeOfFIFO(event.getMaxSize());
+ } else {
+ ar.setAsynchronous(true);
+ ar.setBlocking(false);
+ ar.setSizeOfFIFO(event.getMaxSize());
- //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));
+ }
+ //avspec.addRelation(ar);
- 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"));
+ AvatarBlock FifoEvt = AvatarBlockTemplate.getFifoBlockWithNotified("Block" + event.getName(),
+ avspec, ar, event.getReferenceObject(), sigOut, sigIn, sigNotified, event.getMaxSize(), event.getID());
+ avspec.addBlock(FifoEvt);
- 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
+ ar = new AvatarRelation(event.getName()+"_FIFOIN", taskBlockMap.get(event.getOriginTask()), FifoEvt,
+ event.getReferenceObject());
+ ar.addSignals(sigOut, FifoEvt.getAvatarSignalWithName("write"));
+ avspec.addRelation(ar);
- //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
+ 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);
- //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
+ }
- //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 + ")");
- }
- }
+ // System.out.println("Avatar relations " + avspec.getRelations());
- //Create MAC method
- AvatarMethod mac = new AvatarMethod("MAC", ae);
- AvatarAttribute macattr = new AvatarAttribute(ae.securityPattern.name + "_mac", AvatarType.INTEGER, block, null);
- block.addAttribute(macattr);
+ 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);
+ }
+ }
+ tmlmodel.secChannelMap = secChannelMap;
- mac.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
- mac.addParameter(block.getAvatarAttributeWithName("key_" + ae.securityPattern.name));
- mac.addReturnParameter(macattr);
+// System.out.println("avatar spec\n" +avspec);
+ return avspec;
+ }
- 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);
-
- if (!ae.securityPattern.key.isEmpty()) {
- //Decrypting key
-
-
- //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
-
- //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));
-
- 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);
- }
-
- 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
-
- //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);
+ public List<AvatarStateMachineElement> translateState(TMLActivityElement ae, AvatarBlock block) {
- 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);
+ AvatarTransition tran = new AvatarTransition(block, "", null);
+ List<AvatarStateMachineElement> elementList = new ArrayList<AvatarStateMachineElement>();
- 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 (ae == null) {
+ return elementList;
+ }
- 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);
- }
+ 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);
}
-
-
- //Can't decrypt hash or nonce
- }
- } else {
- // See if action.
- if (ae instanceof TMLActionState) {
- String val = ((TMLActionState)ae).getAction();
- tran.addAction(val);
}
+ //elementList.addAll(tmp);
+ seq = tmp;
+ }
+ //Put stop states on the end of the last in sequence
+ for (AvatarStateMachineElement e : seq) {
+ if (e.getNexts().size() == 0 && !(e instanceof AvatarStopState)) {
+ AvatarStopState stop = new AvatarStopState("stop", null);
+ e.addNext(stop);
+ elementList.add(stop);
+ }
+ elementList.add(e);
}
- } 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);
+ return elementList;
- } else if (ae instanceof TMLActivityElementChannel) {
- TMLActivityElementChannel aec = (TMLActivityElementChannel) ae;
- TMLChannel ch = aec.getChannel(0);
+ } else if (ae instanceof TMLSendRequest) {
+ TMLSendRequest sr = (TMLSendRequest) ae;
+ TMLRequest req = sr.getRequest();
AvatarSignal sig;
boolean checkAcc = false;
if (ae.getReferenceObject() != null) {
@@ -1110,60 +819,195 @@ 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());
- if (ae instanceof TMLReadChannel) {
- //Create signal if it does not already exist
- if (!signalInMap.containsKey(ch.getName())) {
- sig = new AvatarSignal(getName(ch.getName()), AvatarSignal.IN, ch.getReferenceObject());
- signals.add(sig);
- signalInMap.put(ch.getName(), sig);
- block.addSignal(sig);
- AvatarAttribute channelData = new AvatarAttribute(getName(ch.getName()) + "_chData", AvatarType.INTEGER, block, null);
- if (block.getAvatarAttributeWithName(getName(ch.getName()) + "_chData") == null) {
- block.addAttribute(channelData);
- }
- sig.addParameter(channelData);
+ 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());
+ }
+
+ 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 {
- sig = signalInMap.get(ch.getName());
+ // Add parameter to signal and actiononsignal
+ sig.addParameter(block.getAvatarAttributeWithName(sr.getParam(i)));
+ as.addValue(sr.getParam(i));
}
- AvatarActionOnSignal as = new AvatarActionOnSignal(ae.getName(), sig, ae.getReferenceObject());
+ }
+ /*
+ 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);
- if (ae.securityPattern != null) {
- //If nonce
- if (ae.securityPattern.type.equals("Nonce")) {
- block.addAttribute(new AvatarAttribute(ae.securityPattern.name, AvatarType.INTEGER, block, null));
- as.addValue(ae.securityPattern.name);
+ } 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);
+
+ //Remove stop states of sets and route their transitions to the first element of the following sequence
+ for (AvatarStateMachineElement e : set0) {
+ if (e instanceof AvatarStopState) {
+ //ignore
+ } else if (e.getNexts().size() == 0) {
+ e.addNext(set1.get(0));
+ elementList.add(e);
+ } else if (e.getNext(0) instanceof AvatarStopState) {
+ //Remove the transition to AvatarStopState
+ e.removeNext(0);
+ e.addNext(set1.get(0));
+ elementList.add(e);
+ } else {
+ elementList.add(e);
+ }
+ }
+
+
+ //Build branch 0
+ tran = new AvatarTransition(block, "__after_" + ae.getName() + "_0", 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);
}
- //Send the encrypted key
- else if (!ae.securityPattern.key.isEmpty()) {
- as.addValue("encryptedKey_" + ae.securityPattern.key);
- AvatarAttribute data = new AvatarAttribute("encryptedKey_" + ae.securityPattern.key, AvatarType.INTEGER, block, null);
- block.addAttribute(data);
+ 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 {
- //Send the encrypted data
- if (!secChannelMap.containsKey(ae.securityPattern.name)) {
- List<String> tmp = new ArrayList<String>();
- secChannelMap.put(ae.securityPattern.name, tmp);
- }
-
- secChannelMap.get(ae.securityPattern.name).add(ch.getName());
- if (aec.getEncForm()){
- as.addValue(ae.securityPattern.name + "_encrypted");
- AvatarAttribute data = new AvatarAttribute(ae.securityPattern.name + "_encrypted", AvatarType.INTEGER, block, null);
- block.addAttribute(data);
+ elementList.add(e);
+ }
+ }
+ 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);
}
- else {
- if (block.getAvatarAttributeWithName(ae.securityPattern.name) == null){
- AvatarAttribute data = new AvatarAttribute(ae.securityPattern.name, AvatarType.INTEGER, block, null);
- block.addAttribute(data);
- }
- as.addValue(ae.securityPattern.name);
-
+ }
+
+
+ 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));
}
}
- } else {
- as.addValue(getName(ch.getName()) + "_chData");
+
+
+ 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 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());
@@ -1171,118 +1015,39 @@ public class FullTML2Avatar {
signalState.addNext(signalTran);
elementList.add(signalTran);
signalTran.addNext(as);
- as.addNext(tran);
elementList.add(as);
+ as.addNext(tran);
elementList.add(tran);
- if (ch.checkAuth) {
- //Add aftersignal state
- AvatarState afterSignalState = new AvatarState("aftersignalstate_" + ae.getName().replaceAll(" ", "") + "_" + ch.getName(), ae.getReferenceObject());
- tran.addNext(afterSignalState);
- tran = new AvatarTransition(block, "__aftersignalstate_" + ae.getName(), ae.getReferenceObject());
- afterSignalState.addNext(tran);
- elementList.add(afterSignalState);
- elementList.add(tran);
- if (block.getAvatarAttributeWithName(getName(ch.getName()) + "_chData") == null) {
- AvatarAttribute channelData = new AvatarAttribute(getName(ch.getName()) + "_chData", AvatarType.INTEGER, block, null);
- block.addAttribute(channelData);
- }
- AvatarAttributeState authDest = new AvatarAttributeState(block.getName() + "." + afterSignalState.getName() + "." + getName(ch.getName()) + "_chData", ae.getReferenceObject(), block.getAvatarAttributeWithName(getName(ch.getName()) + "_chData"), afterSignalState);
- signalAuthDestMap.put(ch.getName(), authDest);
- }
- } else {
- //WriteChannel
- if (!signalOutMap.containsKey(ch.getName())) {
- //Add signal if it does not exist
- sig = new AvatarSignal(getName(ch.getName()), AvatarSignal.OUT, ch.getReferenceObject());
- signals.add(sig);
- block.addSignal(sig);
- signalOutMap.put(ch.getName(), sig);
- AvatarAttribute channelData = new AvatarAttribute(getName(ch.getName()) + "_chData", AvatarType.INTEGER, block, null);
- if (block.getAvatarAttributeWithName(getName(ch.getName()) + "_chData") == null) {
- block.addAttribute(channelData);
- }
- sig.addParameter(channelData);
- } else {
- sig = signalOutMap.get(ch.getName());
- }
- //Add the confidentiality pragma for this channel data
- if (ch.checkConf) {
- if (ch.originalOriginTasks.size()!=0 && ch.getOriginPort().getName().contains("PORTORIGIN")){
- // System.out.println("Channel " + ch.getOriginPort().getName() + " block " + block.getName());
- if (!attrsToCheck.contains(ch.getOriginPort().getName() + "_chData") ) {
- for (TMLTask origTask: ch.originalOriginTasks){
- AvatarBlock bl = avspec.getBlockWithName(origTask.getName().split("__")[origTask.getName().split("__").length - 1]);
- if (bl!=null){
- AvatarAttribute attr = bl.getAvatarAttributeWithName(block.getName() + "_chData");
- if (attr != null) {
- attrsToCheck.add(ch.getOriginPort().getName() + "_chData");
- avspec.addPragma(new AvatarPragmaSecret("#Confidentiality " + bl.getName() + "." + block.getName() + "_chData", ch.getReferenceObject(), attr));
- }
- }
- }
- }
- }
- else {
- if (!attrsToCheck.contains(ch.getOriginPort().getName() + "_chData") ) {
- AvatarAttribute attr = block.getAvatarAttributeWithName(ch.getOriginPort().getName() + "_chData");
- if (attr != null) {
- attrsToCheck.add(ch.getOriginPort().getName() + "_chData");
- avspec.addPragma(new AvatarPragmaSecret("#Confidentiality " + block.getName() + "." + ch.getName() + "_chData", ch.getReferenceObject(), attr));
- }
- }
- }
- }
- //Add the authenticity pragma for this channel data
- if (ch.checkAuth) {
- if (block.getAvatarAttributeWithName(getName(ch.getName()) + "_chData") == null) {
- AvatarAttribute channelData = new AvatarAttribute(getName(ch.getName()) + "_chData", AvatarType.INTEGER, block, null);
- block.addAttribute(channelData);
- }
- AvatarAttributeState authOrigin = new AvatarAttributeState(block.getName() + "." + signalState.getName() + "." + getName(ch.getName()) + "_chData", ae.getReferenceObject(), block.getAvatarAttributeWithName(getName(ch.getName()) + "_chData"), signalState);
- signalAuthOriginMap.put(ch.getName(), authOrigin);
- }
+ } 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));
- if (ae.securityPattern != null) {
- //send nonce
- if (ae.securityPattern.type.equals("Nonce")) {
- block.addAttribute(new AvatarAttribute(ae.securityPattern.name, AvatarType.INTEGER, block, null));
- as.addValue(ae.securityPattern.name);
- }
- //send encrypted key
- else if (!ae.securityPattern.key.isEmpty()) {
- as.addValue("encryptedKey_" + ae.securityPattern.key);
- AvatarAttribute data = new AvatarAttribute("encryptedKey_" + ae.securityPattern.key, AvatarType.INTEGER, block, null);
- block.addAttribute(data);
+ /*if (block.getAvatarAttributeWithName(aee.getParam(i)) == null) {
+ //Throw Error
+ as.addValue("tmp");
+ TraceManager.addDev("Missing Attribute " + aee.getParam(i));
} else {
- //send encrypted data
- //
- if (aec.getEncForm()){
- as.addValue(ae.securityPattern.name + "_encrypted");
- AvatarAttribute data = new AvatarAttribute(ae.securityPattern.name + "_encrypted", AvatarType.INTEGER, block, null);
- block.addAttribute(data);
- }
- else {
- //Send unecrypted form
- if (block.getAvatarAttributeWithName(ae.securityPattern.name) == null){
- AvatarAttribute data = new AvatarAttribute(ae.securityPattern.name, AvatarType.INTEGER, block, null);
- block.addAttribute(data);
- }
- as.addValue(ae.securityPattern.name);
- }
-
- if (!secChannelMap.containsKey(ae.securityPattern.name)) {
- List<String> tmp = new ArrayList<String>();
- secChannelMap.put(ae.securityPattern.name, tmp);
+ // 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:");
}
- secChannelMap.get(ae.securityPattern.name).add(ch.getName());
- }
- } else {
- //No security pattern
- // TraceManager.addDev("no security pattern for " + ch.getName());
- as.addValue(ch.getOriginPort().getName()+ "_chData");
+ sig.addParameter(block.getAvatarAttributeWithName(aee.getParam(i)));
+
+
+
+ TraceManager.addDev("Param #" + i + " (1)");
+ as.addValue(aee.getParam(i));
+ TraceManager.addDev("Param #" + i + " (2)");
+ }*/
}
tran = new AvatarTransition(block, "__after_" + ae.getName(), ae.getReferenceObject());
@@ -1290,827 +1055,707 @@ public class FullTML2Avatar {
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);
}
- } 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);
+ } 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);
+
+ 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));
+
+ 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 (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
+
+ //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));
+
+ 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
+
+ //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));
+
+ 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 (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
+
+ //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
+
+
+ //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
+
+ //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 (e.getNext(0) instanceof AvatarStopState) {
- //Remove the transition to AvatarStopState
- e.removeNext(0);
- e.addNext(as);
- elementList.add(e);
- } else {
- elementList.add(e);
- }
- }
+ } else if (ae.securityPattern.type.equals("Asymmetric Encryption")) {
+ AvatarMethod adecrypt = new AvatarMethod("adecrypt", ae);
- //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);
- }
- //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 (!ae.securityPattern.key.isEmpty()) {
+ //Decrypting key
- //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));
- elementList.add(tran);
- elementList.addAll(nexts);
- }
- }
- return elementList;
+ //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));
- } 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);
- }
- 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;
- }
+ adecrypt.addParameter(block.getAvatarAttributeWithName("encryptedKey_" + ae.securityPattern.key));
+ adecrypt.addParameter(block.getAvatarAttributeWithName("privKey_" + ae.securityPattern.name));
+ adecrypt.addReturnParameter(block.getAvatarAttributeWithName("key_" + ae.securityPattern.key));
- public String processName(String name, int id) {
- name = name.replaceAll("-", "_").replaceAll(" ", "");
- if (allStates.contains(name)) {
- return name + id;
+ 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
- } else {
- allStates.add(name);
- return name;
- }
- }
- /* public AvatarPragma generatePragma(String[] s){
+ //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));
- }*/
+ 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);
+ }
- 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];
- }
- 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];
- }
- }
- }
+ 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
- public AvatarSpecification generateAvatarSpec(String _loopLimit) {
+ //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));
- TraceManager.addDev("security patterns " + tmlmodel.secPatterns);
- TraceManager.addDev("keys " + tmlmap.mappedSecurity);
+ 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));
- //TODO: Make state names readable
- //TODO: Put back numeric guards
- //TODO: Calcuate for temp variable
- if (tmlmap.getTMLModeling().getTGComponent() != null) {
- this.avspec = new AvatarSpecification("spec", tmlmap.getTMLModeling().getTGComponent().getTDiagramPanel().tp);
- } else {
- this.avspec = new AvatarSpecification("spec", null);
- }
- attrsToCheck.clear();
- tmlmodel.removeForksAndJoins();
-
-// System.out.println("MODIFIED model " + tmlmodel);
-
- for (TMLChannel chan: tmlmodel.getChannels()){
- //System.out.println("chan " + chan);
- TMLTask task = chan.getOriginTask();
-
- TMLTask task2 = chan.getDestinationTask();
- HwExecutionNode node = tmlmap.getHwNodeOf(task);
- HwExecutionNode node2 = tmlmap.getHwNodeOf(task2);
- if (node==null){
- tmlmap.addTaskToHwExecutionNode(task, node2);
- }
-
- if (node2==null){
- tmlmap.addTaskToHwExecutionNode(task2, node);
- }
-
- if (chan.getName().contains("fork__") || chan.getName().contains("FORKCHANNEL")){
- chan.setName(chan.getName().replaceAll("__",""));
- }
-
- }
-
- //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;
- }
- }
+ 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));
- 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);
- }
+ 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)");
- List<TMLTask> tasks = tmlmap.getTMLModeling().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();
+ 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 + ")");
+ }
- distributeKeys();
+ 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);
- 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);
- }
- }*/
+ if (!ae.securityPattern.nonce.isEmpty()) {
- for (TMLTask task : tasks) {
+ //Add extra state and transition
- AvatarBlock block = taskBlockMap.get(task);
- //Add temp variable for unsendable signals
+ 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);
- //Add all signals
- for (TMLChannel chan : tmlmodel.getChannels(task)) {
- if (chan.hasOriginTask(task)) {
- AvatarSignal sig = new AvatarSignal(chan.getOriginPort().getName(), AvatarSignal.OUT, chan.getReferenceObject());
+ 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);
- 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);
- } else if (chan.hasDestinationTask(task)) {
- AvatarSignal sig = new AvatarSignal(getName(chan.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);
+ 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);
+ }
}
- sig.addParameter(channelData);
+
+
+ //Can't decrypt hash or nonce
+ }
+ } else {
+ // See if action.
+ if (ae instanceof TMLActionState) {
+ String val = ((TMLActionState) ae).getAction();
+ tran.addAction(val);
}
+
}
- AvatarAttribute tmp = new AvatarAttribute("tmp", AvatarType.INTEGER, block, null);
- block.addAttribute(tmp);
+ } 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);
- /* tmp = new AvatarAttribute("aliceandbob", AvatarType.INTEGER, block, null);
- block.addAttribute(tmp);
- tmp = new AvatarAttribute("aliceandbob_encrypted", AvatarType.INTEGER, block, null);
- block.addAttribute(tmp);*/
+ } else if (ae instanceof TMLActivityElementChannel) {
+ TMLActivityElementChannel aec = (TMLActivityElementChannel) ae;
+ TMLChannel ch = aec.getChannel(0);
+ AvatarSignal sig;
- AvatarAttribute loop_index = new AvatarAttribute("loop_index", AvatarType.INTEGER, block, null);
- block.addAttribute(loop_index);
+ String nv = getName(ch.getName()) + "_chData";
+ block.addIntAttributeIfApplicable(nv);
- 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);
+ boolean checkAcc = false;
+ if (ae.getReferenceObject() != null) {
+ checkAcc = ((TGComponent) ae.getReferenceObject()).getCheckableAccessibility();
}
- //AvatarTransition last;
- AvatarStateMachine asm = block.getStateMachine();
+ 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());
- //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);
+ if (ae instanceof TMLReadChannel) {
+ //Create signal if it does not already exist
+ sig = signalInMap.get(ch.getName());
+ } else {
+ sig = signalOutMap.get(ch.getName());
+ }
- //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);
+ AvatarActionOnSignal as = new AvatarActionOnSignal(ae.getName(), sig, ae.getReferenceObject());
+ tran = new AvatarTransition(block, "__after_" + ae.getName(), ae.getReferenceObject());
- AvatarState loopstart = new AvatarState("loopstart", task.getActivityDiagram().get(0).getReferenceObject());
- at.addNext(loopstart);
- asm.addElement(loopstart);
+ elementList.add(signalState);
+ elementList.add(signalStateIntermediate);
+ elementList.add(as);
+ elementList.add(tran);
+ elementList.add(signalTranInit);
+ elementList.add(signalTranBefore);
+ elementList.add(signalTran);
- //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
+ 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);
+
+ signalStateIntermediate.addNext(tran);
+ tran.setGuard("else");
- 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 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) {
- //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);
- }
+ } else if (e.getNexts().size() == 0) {
+ if (e instanceof AvatarTransition) {
+ e.addNext(as);
+ elementList.add(e);
}
- asm.addElement(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);
}
}
-
- //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());
-
-
- //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);
+
+ //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);
+ }
+ //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 {
- 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));
- }
+ elementList.add(e);
}
- 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);
- }*/
-
- }
+ }
+ //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;
+ }
- asm.setStartState(ss);
+ } 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);
+ }
+ }
+ return elementList;
- }
- 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));
- }
- }
+ } 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);
+ }
+ 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){
- //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);
- }
- }
- }
+ }*/
- //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
-
- if (channel.isBasicChannel()){
- //System.out.println("checking channel " + channel.getName());
- AvatarRelation ar= new AvatarRelation(channel.getName(), taskBlockMap.get(channel.getOriginTask()), taskBlockMap.get(channel.getDestinationTask()), channel.getReferenceObject());
- LinkedList<HwCommunicationNode> path = tmlmap.findNodesForElement(channel);
- if (path.size()!=0){
- ar.setPrivate(true);
- for (HwCommunicationNode node:path){
- if (node instanceof HwBus){
- if (((HwBus) node).privacy ==0){
- ar.setPrivate(false);
- }
- }
- }
- }
- else {
- if (channel.originalOriginTasks.size()==0){
- ar.setPrivate(originDestMap.get(channel.getOriginTask().getName()+"__"+channel.getDestinationTask().getName())==1);
- }
- else {
- //System.out.println("complex channel " + channel.getName());
- //Find privacy of original tasks
- boolean priv = true;
- for (TMLTask task1: channel.originalOriginTasks){
- for (TMLTask task2: channel.originalDestinationTasks){
- if (originDestMap.get(task1.getName()+"__"+task2.getName())!=1){
- priv=false;
- break;
- }
-
- }
-
- }
- ar.setPrivate(priv);
- }
- }
- 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
-
- 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);
- }
- }
- }
- //System.out.println("size " + sig1.size() + " " + sig2.size());
- 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){
- 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());
- }
- 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();
-
- if (name.equals(getName(request.getName()))){
- sig1.add(sig);
- }
- }
- }
- //Find out signal
- for (AvatarSignal sig: signals){
- if (sig.getInOut()==AvatarSignal.OUT){
- String name = sig.getName();
-
- if (name.equals(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
- System.out.println("Could not match for " + request.getName());
- }
+ 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];
+ }
+ 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];
+ }
+ }
+ }
- ar.setAsynchronous(false);
- avspec.addRelation(ar);
- }
- }
- for (TMLEvent event: tmlmodel.getEvents()){
-
- AvatarRelation ar = new AvatarRelation(event.getName(), taskBlockMap.get(event.getOriginTask()), taskBlockMap.get(event.getDestinationTask()), event.getReferenceObject());
- ar.setPrivate(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);
- }
- }
- }
- //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);
- }
- }
- }
- 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());
- }
- avspec.addRelation(ar);
- }
-
- // System.out.println("Avatar relations " + avspec.getRelations());
-
- 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));
- }
- }
- 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);
- }
- }
-
- tmlmap.getTMLModeling().secChannelMap = secChannelMap;
-
-// System.out.println("avatar spec\n" +avspec);
- return avspec;
- }
- public void backtraceReachability( Map<AvatarPragmaReachability, ProVerifQueryResult> reachabilityResults) {
+ /*public void backtraceReachability( Map<AvatarPragmaReachability, ProVerifQueryResult> reachabilityResults) {
for (AvatarPragmaReachability pragma: reachabilityResults.keySet())
{
ProVerifQueryResult result = reachabilityResults.get(pragma);
@@ -2147,106 +1792,76 @@ public class FullTML2Avatar {
}
}
}
- }
+ }*/
- public void distributeKeys(){
- List<TMLTask> tasks = tmlmap.getTMLModeling().getTasks();
- for (TMLTask t:accessKeys.keySet()){
- AvatarBlock b = taskBlockMap.get(t);
- for (SecurityPattern sp: accessKeys.get(t)){
- if (sp.type.equals("Symmetric Encryption") || sp.type.equals("MAC")){
- AvatarAttribute key = new AvatarAttribute("key_"+sp.name, AvatarType.INTEGER, b, null);
- if (symKeys.containsKey(sp)){
- symKeys.get(sp).add(key);
- }
- else {
- LinkedList<AvatarAttribute> tmp = new LinkedList<AvatarAttribute>();
- tmp.add(key);
- symKeys.put(sp, tmp);
- }
- b.addAttribute(key);
- }
- else if (sp.type.equals("Asymmetric Encryption")){
- AvatarAttribute pubkey = new AvatarAttribute("pubKey_"+sp.name, AvatarType.INTEGER, b, null);
- b.addAttribute(pubkey);
-
- AvatarAttribute privkey = new AvatarAttribute("privKey_"+sp.name, AvatarType.INTEGER, b, null);
- b.addAttribute(privkey);
- avspec.addPragma(new AvatarPragmaPrivatePublicKey("#PrivatePublicKeys " + b.getName() + " " + privkey.getName() + " " + pubkey.getName(), null, privkey, pubkey));
- if (pubKeys.containsKey(sp)){
- pubKeys.get(sp).add(pubkey);
- }
- else {
- LinkedList<AvatarAttribute> tmp = new LinkedList<AvatarAttribute>();
- tmp.add(pubkey);
- pubKeys.put(sp, tmp);
- }
- //Distribute public key everywhere
- for (TMLTask task2 : tasks){
- AvatarBlock b2 = taskBlockMap.get(task2);
- pubkey = new AvatarAttribute("pubKey_"+sp.name, AvatarType.INTEGER, b2, null);
- b2.addAttribute(pubkey);
- if (pubKeys.containsKey(sp)){
- pubKeys.get(sp).add(pubkey);
- }
- }
- }
- }
- }
-
- }
- public AvatarBlock createFifo(String name){
- AvatarBlock fifo = new AvatarBlock("FIFO__FIFO"+name, avspec, null);
- AvatarState root = new AvatarState("root",null, false, false);
- AvatarSignal read = new AvatarSignal("readSignal", AvatarSignal.IN, null);
- AvatarAttribute data = new AvatarAttribute("data", AvatarType.INTEGER, fifo, null);
- fifo.addAttribute(data);
- read.addParameter(data);
- AvatarSignal write = new AvatarSignal("writeSignal", AvatarSignal.OUT, null);
- write.addParameter(data);
- AvatarStartState start = new AvatarStartState("start", null);
- AvatarTransition afterStart = new AvatarTransition(fifo, "afterStart", null);
- fifo.addSignal(read);
- fifo.addSignal(write);
- AvatarTransition toRead = new AvatarTransition(fifo, "toReadSignal", null);
- AvatarTransition toWrite = new AvatarTransition(fifo, "toWriteSignal", null);
- AvatarTransition afterRead = new AvatarTransition(fifo, "afterReadSignal", null);
- AvatarTransition afterWrite = new AvatarTransition(fifo, "afterWriteSignal", null);
- AvatarActionOnSignal readAction= new AvatarActionOnSignal("read", read, null);
- AvatarActionOnSignal writeAction= new AvatarActionOnSignal("write", write, null);
-
- AvatarStateMachine asm = fifo.getStateMachine();
- asm.addElement(start);
- asm.setStartState(start);
- asm.addElement(afterStart);
- asm.addElement(root);
- asm.addElement(toRead);
- asm.addElement(toWrite);
- asm.addElement(afterRead);
- asm.addElement(afterWrite);
- asm.addElement(readAction);
- asm.addElement(writeAction);
-
- start.addNext(afterStart);
- afterStart.addNext(root);
- root.addNext(toRead);
- root.addNext(toWrite);
- toRead.addNext(readAction);
- toWrite.addNext(writeAction);
- readAction.addNext(afterRead);
- writeAction.addNext(afterWrite);
- afterRead.addNext(root);
- afterWrite.addNext(root);
-
- avspec.addBlock(fifo);
- return fifo;
- }
-
-
- public AvatarSpecification convertToSecurityType(AvatarSpecification spec) {
- return spec;
+
+ public AvatarBlock createFifo(String name) {
+ AvatarBlock fifo = new AvatarBlock("FIFO__FIFO" + name, avspec, null);
+ AvatarState root = new AvatarState("root", null, false, false);
+ AvatarSignal read = new AvatarSignal("readSignal", AvatarSignal.IN, null);
+ AvatarAttribute data = new AvatarAttribute("data", AvatarType.INTEGER, fifo, null);
+ fifo.addAttribute(data);
+ read.addParameter(data);
+ AvatarSignal write = new AvatarSignal("writeSignal", AvatarSignal.OUT, null);
+ write.addParameter(data);
+ AvatarStartState start = new AvatarStartState("start", null);
+ AvatarTransition afterStart = new AvatarTransition(fifo, "afterStart", null);
+ fifo.addSignal(read);
+ fifo.addSignal(write);
+ AvatarTransition toRead = new AvatarTransition(fifo, "toReadSignal", null);
+ AvatarTransition toWrite = new AvatarTransition(fifo, "toWriteSignal", null);
+ AvatarTransition afterRead = new AvatarTransition(fifo, "afterReadSignal", null);
+ AvatarTransition afterWrite = new AvatarTransition(fifo, "afterWriteSignal", null);
+ AvatarActionOnSignal readAction = new AvatarActionOnSignal("read", read, null);
+ AvatarActionOnSignal writeAction = new AvatarActionOnSignal("write", write, null);
+
+ AvatarStateMachine asm = fifo.getStateMachine();
+ asm.addElement(start);
+ asm.setStartState(start);
+ asm.addElement(afterStart);
+ asm.addElement(root);
+ asm.addElement(toRead);
+ asm.addElement(toWrite);
+ asm.addElement(afterRead);
+ asm.addElement(afterWrite);
+ asm.addElement(readAction);
+ asm.addElement(writeAction);
+
+ start.addNext(afterStart);
+ afterStart.addNext(root);
+ root.addNext(toRead);
+ root.addNext(toWrite);
+ toRead.addNext(readAction);
+ toWrite.addNext(writeAction);
+ readAction.addNext(afterRead);
+ writeAction.addNext(afterWrite);
+ afterRead.addNext(root);
+ afterWrite.addNext(root);
+
+ avspec.addBlock(fifo);
+ return fifo;
}
+ public String getNameReworked(String name, int index) {
+ String[] split = name.split("__");
+ if (split.length > index) {
+ return split[index];
+ }
+ return name;
+ }
+
+ 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/tmltranslator/toavatar/FullTML2AvatarDP.java b/src/main/java/tmltranslator/toavatar/FullTML2AvatarDP.java
deleted file mode 100644
index 24ad29f4f940c8f712db983e4627c963d851ee24..0000000000000000000000000000000000000000
--- a/src/main/java/tmltranslator/toavatar/FullTML2AvatarDP.java
+++ /dev/null
@@ -1,383 +0,0 @@
-/* Copyright or (C) or Copr. GET / ENST, Telecom-Paris, Ludovic Apvrille
- *
- * ludovic.apvrille AT enst.fr
- *
- * This software is a computer program whose purpose is to allow the
- * edition of TURTLE analysis, design and deployment diagrams, to
- * allow the generation of RT-LOTOS or Java code from this diagram,
- * and at last to allow the analysis of formal validation traces
- * obtained from external tools, e.g. RTL from LAAS-CNRS and CADP
- * from INRIA Rhone-Alpes.
- *
- * This software is governed by the CeCILL license under French law and
- * abiding by the rules of distribution of free software. You can use,
- * modify and/ or redistribute the software under the terms of the CeCILL
- * license as circulated by CEA, CNRS and INRIA at the following URL
- * "http://www.cecill.info".
- *
- * As a counterpart to the access to the source code and rights to copy,
- * modify and redistribute granted by the license, users are provided only
- * with a limited warranty and the software's author, the holder of the
- * economic rights, and the successive licensors have only limited
- * liability.
- *
- * In this respect, the user's attention is drawn to the risks associated
- * with loading, using, modifying and/or developing or reproducing the
- * software by the user in light of its specific status of free software,
- * that may mean that it is complicated to manipulate, and that also
- * therefore means that it is reserved for developers and experienced
- * professionals having in-depth computer knowledge. Users are therefore
- * encouraged to load and test the software's suitability as regards their
- * requirements in conditions enabling the security of their systems and/or
- * data to be ensured and, more generally, to use and operate it in the
- * same conditions as regards security.
- *
- * The fact that you are presently reading this means that you have had
- * knowledge of the CeCILL license and that you accept its terms.
- */
-
-
-package tmltranslator.toavatar;
-
-import avatartranslator.*;
-import myutil.TraceManager;
-import tmltranslator.TMLMapping;
-import ui.AvatarDesignPanel;
-import ui.TAttribute;
-import ui.TGComponent;
-import ui.TGConnectingPoint;
-import ui.avatarbd.AvatarBDBlock;
-import ui.avatarbd.AvatarBDPanel;
-import ui.avatarbd.AvatarBDPortConnector;
-import ui.avatarbd.AvatarBDPragma;
-import ui.avatarsmd.*;
-
-import java.awt.*;
-import java.util.*;
-
-//import translator.*;
-
-
-/**
- * Class TML2AvatarDP
- * Creation: 05/10/2016
- *
- * @author Letitia LI, Ludovic APVRILLE
- */
-public class FullTML2AvatarDP {
-
- //protected CorrespondanceTGElement listB; // list for particular element -> first element of group of blocks
- protected TMLMapping tmlmap;
- public AvatarDesignPanel adp;
-
- private Map<AvatarTransition, TGConnectingPoint> tranSourceMap = new HashMap<AvatarTransition, TGConnectingPoint>();
- private Map<AvatarTransition, AvatarStateMachineElement> tranDestMap = new HashMap<AvatarTransition, AvatarStateMachineElement>();
- private Map<AvatarStateMachineElement, TGConnectingPoint> locMap = new HashMap<AvatarStateMachineElement, TGConnectingPoint>();
- private Map<AvatarStateMachineElement, TGComponent> SMDMap = new HashMap<AvatarStateMachineElement, TGComponent>();
- public Map<String, Set<String>> originDestMap = new HashMap<String, Set<String>>();
- public Map<String, AvatarBDBlock> blockMap = new HashMap<String, AvatarBDBlock>();
- boolean mc;
- boolean security;
- AvatarSpecification avspec;
-
- public FullTML2AvatarDP(TMLMapping tmlmapping, boolean modelcheck, boolean sec) {
- tmlmap = tmlmapping;
- mc = modelcheck;
- security = sec;
- }
-
- public FullTML2AvatarDP(AvatarSpecification av) {
- avspec = av;
- }
-
- public void commMap(AvatarSpecification avspec) {
- //Create a map of all connections
- /*TMLModeling tmlmodel=tmlmap.getTMLModeling();
- for (TMLTask t: tmlmodel.getTasks()){
- Set<String> hs = new HashSet<String>();
- //Iterate through channels
- LinkedList ll= tmlmodel.getChannelsToMe(t);
- ListIterator iterator = ll.listIterator();
- TMLChannel chanl;
- String name="";
- while(iterator.hasNext()) {
- chanl = (TMLChannel)(iterator.next());
- for (TMLTask dt: chanl.getOriginTasks()){
- name= dt.getName();
- hs.add(name.split("__")[name.split("__").length-1]);
- }
- name= chanl.getOriginTask().getName();
- hs.add(name.split("__")[name.split("__").length-1]);
- }
- name=t.getName();
- originDestMap.put(name.split("__")[name.split("__").length-1], hs);
- */
- for (AvatarRelation ar : avspec.getRelations()) {
-
- String bl1 = ar.block1.getName();
- String bl2 = ar.block2.getName();
- if (originDestMap.containsKey(bl1.split("__")[bl1.split("__").length - 1])) {
- originDestMap.get(bl1.split("__")[bl1.split("__").length - 1]).add(bl2.split("__")[bl2.split("__").length - 1]);
- } else {
- Set<String> hs = new HashSet<String>();
- hs.add(bl2.split("__")[bl2.split("__").length - 1]);
- originDestMap.put(bl1.split("__")[bl1.split("__").length - 1], hs);
- }
- }
-
- }
-
- public void addStates(AvatarStateMachineElement asme, int x, int y, AvatarSMDPanel smp, AvatarBDBlock bl) {
- TGConnectingPoint tp = new TGConnectingPoint(null, x, y, false, false);
- if (asme instanceof AvatarStartState) {
- AvatarSMDStartState smdss = new AvatarSMDStartState(x, y, x, x * 2, y, y * 2, false, null, smp);
- smp.addComponent(smdss, x, y, false, true);
- SMDMap.put(asme, smdss);
- tp = smdss.tgconnectingPointAtIndex(0);
- locMap.put(asme, tp);
- }
- if (asme instanceof AvatarTransition) {
- //
- }
- if (asme instanceof AvatarActionOnSignal) {
- avatartranslator.AvatarSignal sig = ((AvatarActionOnSignal) asme).getSignal();
- if (sig.isIn()) {
- AvatarSMDReceiveSignal smdrs = new AvatarSMDReceiveSignal(x, y, x, x * 2, y, y * 2, false, null, smp);
- smp.addComponent(smdrs, x, y, false, true);
- String name = sig.getName().split("__")[sig.getName().split("__").length - 1];
- smdrs.setValue(name + "()");
- sig.setName(name);
- smdrs.recalculateSize();
- SMDMap.put(asme, smdrs);
- tp = smdrs.getFreeTGConnectingPoint(x + smdrs.getWidth() / 2, y + smdrs.getHeight());
- TGConnectingPoint tp2 = smdrs.getFreeTGConnectingPoint(x + smdrs.getWidth() / 2, y);
- locMap.put(asme, tp2);
- if (bl.getAvatarSignalFromName(name) == null) {
- bl.addSignal(new ui.AvatarSignal(0, name, new String[0], new String[0]));
- }
-
- } else {
- AvatarSMDSendSignal smdss = new AvatarSMDSendSignal(x, y, x, x * 2, y, y * 2, false, null, smp);
- smp.addComponent(smdss, x, y, false, true);
- String name = sig.getName().split("__")[sig.getName().split("__").length - 1];
- smdss.setValue(name + "()");
- sig.setName(name);
- smdss.recalculateSize();
- SMDMap.put(asme, smdss);
- tp = smdss.getFreeTGConnectingPoint(x + smdss.getWidth() / 2, y + smdss.getHeight());
- TGConnectingPoint tp2 = smdss.getFreeTGConnectingPoint(x + smdss.getWidth() / 2, y);
- locMap.put(asme, tp2);
- if (bl.getAvatarSignalFromName(name) == null) {
- bl.addSignal(new ui.AvatarSignal(1, name, new String[0], new String[0]));
- }
- }
-
- }
- if (asme instanceof AvatarStopState) {
- AvatarSMDStopState smdstop = new AvatarSMDStopState(x, y, x, x * 2, y, y * 2, false, null, smp);
- SMDMap.put(asme, smdstop);
- smp.addComponent(smdstop, x, y, false, true);
- tp = smdstop.tgconnectingPointAtIndex(0);
- locMap.put(asme, tp);
- }
- if (asme instanceof AvatarState) {
- //check if empty checker state
- if (asme.getName().contains("signalstate_")) {
- //don't add the state, ignore next transition,
- if (asme.getNexts().size() == 1) {
- AvatarStateMachineElement next = asme.getNext(0).getNext(0);
- //Reroute transition
- for (AvatarTransition at : tranDestMap.keySet()) {
- if (tranDestMap.get(at) == asme) {
- tranDestMap.put(at, next);
- }
- }
- addStates(next, x, y, smp, bl);
- return;
- }
- }
- AvatarSMDState smdstate = new AvatarSMDState(x, y, x, x * 2, y, y * 2, false, null, smp);
- smp.addComponent(smdstate, x, y, false, true);
- smdstate.setValue(asme.getName());
- smdstate.recalculateSize();
- SMDMap.put(asme, smdstate);
- tp = smdstate.getFreeTGConnectingPoint(x + smdstate.getWidth() / 2, y + smdstate.getHeight());
- TGConnectingPoint tp2 = smdstate.getFreeTGConnectingPoint(x + smdstate.getWidth() / 2, y);
- locMap.put(asme, tp2);
- }
- int i = 1;
- int diff = 400;
- int ydiff = 50;
- for (AvatarStateMachineElement el : asme.getNexts()) {
- if (el instanceof AvatarTransition) {
- tranSourceMap.put((AvatarTransition) el, tp);
- } else {
- AvatarTransition t = (AvatarTransition) asme;
- tranDestMap.put(t, el);
- }
- if (!SMDMap.containsKey(el)) {
- addStates(el, diff * i, y + ydiff, smp, bl);
- i++;
- }
- }
- return;
- }
-
- public void translate() {
- FullTML2Avatar tml2av = new FullTML2Avatar(tmlmap);
- avspec = tml2av.generateAvatarSpec("1");
- drawPanel();
- //Create AvatarDesignDiagram
- }
-
- public void drawPanel() {
- if (adp == null) {
- return;
- }
- if (avspec == null) {
- return;
- }
- AvatarBDPanel abd = adp.abdp;
-
- //Find all blocks, create blocks from left
- int xpos = 10;
- int ypos = 10;
- for (AvatarBlock ab : avspec.getListOfBlocks()) {
- //Crypto blocks?
- AvatarBDBlock father = null;
- if (ab.getFather() != null) {
- father = blockMap.get(ab.getFather().getName().split("__")[1]);
-
- }
- AvatarBDBlock bl = new AvatarBDBlock(xpos, ypos, xpos, xpos * 2, ypos, ypos * 2, false, father, abd);
- tranSourceMap.clear();
- bl.setValue(ab.getName().split("__")[1]);
- abd.changeStateMachineTabName("Block0", bl.getValue());
- blockMap.put(bl.getValue(), bl);
- abd.addComponent(bl, xpos, ypos, false, true);
- for (AvatarAttribute attr : ab.getAttributes()) {
- int type = 5;
- if (attr.getType() == AvatarType.BOOLEAN) {
- type = 4;
- }
- if (attr.getType() == AvatarType.INTEGER) {
- type = 0;
- }
- bl.addAttribute(new TAttribute(0, attr.getName(), attr.getType().getDefaultInitialValue(), type));
- if (attr.getName().equals("key")) {
- bl.addCryptoElements();
- }
- }
- // xpos+=300;
- //Build the state machine
- int smx = 400;
- int smy = 40;
- AvatarSMDPanel smp = adp.getAvatarSMDPanel(bl.getValue());
- if (smp == null) {
- TraceManager.addDev("can't find SMP");
- return;
- }
- smp.removeAll();
- AvatarStateMachine asm = ab.getStateMachine();
- //Remove the empty check states
-
- AvatarStartState start = asm.getStartState();
- addStates(start, smx, smy, smp, bl);
- //Add transitions
- for (AvatarTransition t : tranSourceMap.keySet()) {
- TGConnectingPoint p1 = tranSourceMap.get(t);
- TGConnectingPoint p2 = locMap.get(tranDestMap.get(t));
- Vector<Point> points = new Vector<>();
- if (p1 == null || p2 == null) {
- TraceManager.addDev("Missing point");
- return;
- }
- AvatarSMDConnector SMDcon = new AvatarSMDConnector(p1.getX(), p1.getY(), p1.getX(), p1.getY(), p1.getX(), p1.getY(), true, null, smp, p1, p2, points);
- String action = "";
- if (t.getActions().size() == 0) {
- action = "";
- } else {
- action = t.getActions().get(0).toString();
- }
- SMDcon.setTransitionInfo(t.getGuard().toString(), action);
- smp.addComponent(SMDcon, p1.getX(), p1.getY(), false, true);
- }
- }
-
-
- commMap(avspec);
- //Add Relations
-
- for (String bl1 : originDestMap.keySet()) {
- for (String bl2 : originDestMap.get(bl1)) {
- Vector<Point> points = new Vector<>();
-
- //Add Relations to connector
- for (AvatarRelation ar : avspec.getRelations()) {
- if (ar.block1.getName().contains(bl1) && ar.block2.getName().contains(bl2) || ar.block1.getName().contains(bl2) && ar.block2.getName().contains(bl1)) {
- //TGConnectingPoint p1= blockMap.get(bl1).getFreeTGConnectingPoint(blockMap.get(bl1).getX(), blockMap.get(bl1).getY());
- TGConnectingPoint p1 = blockMap.get(bl1).findFirstFreeTGConnectingPoint(true, true);
- TGConnectingPoint p2 = blockMap.get(bl2).findFirstFreeTGConnectingPoint(true, true);
- // TGConnectingPoint p2=blockMap.get(bl2).getFreeTGConnectingPoint(blockMap.get(bl2).getX(),blockMap.get(bl2).getY());
- AvatarBDPortConnector conn = new AvatarBDPortConnector(0, 0, 0, 0, 0, 0, true, null, abd, p1, p2, points);
- conn.setAsynchronous(ar.isAsynchronous());
- conn.setBlocking(ar.isBlocking());
- conn.setPrivate(ar.isPrivate());
- conn.setSizeOfFIFO(ar.getSizeOfFIFO());
- TraceManager.addDev(bl1 + " " + ar.block1.getName() + " " + ar.block2.getName());
- conn.addSignal("in " + ar.getSignal1(0).getName(), true, true);
- conn.addSignal("out " + ar.getSignal2(0).getName(), false, false);
- TraceManager.addDev("Added Signals");
- conn.updateAllSignals();
- p1.setFree(false);
- p2.setFree(false);
- abd.addComponent(conn, 0, 0, false, true);
- }
- }
- /*for (ui.AvatarSignal sig:blockMap.get(bl1).getSignalList()){
- for (ui.AvatarSignal sig2: blockMap.get(bl2).getSignalList()){
- if (sig.getId().equals(sig2.getId())){
- conn.addSignal("in "+sig.getId(), true, true);
- conn.addSignal("out "+sig.getId(), false, false);
- }
- }
- }*/
- }
- }
- ypos += 100;
- //Add Pragmas
- AvatarBDPragma pragma = new AvatarBDPragma(xpos, ypos, xpos, xpos * 2, ypos, ypos * 2, false, null, abd);
- String[] arr = new String[avspec.getPragmas().size()];
- String s = "";
- int i = 0;
- for (AvatarPragma p : avspec.getPragmas()) {
-
-// arr[i] = p.getName();
- String t = "";
- String[] split = p.getName().split(" ");
- if (p.getName().contains("#Confidentiality")) {
- for (String str : split) {
- if (str.contains(".")) {
- String tmp = str.split("\\.")[0];
- String tmp2 = str.split("\\.")[1];
- TraceManager.addDev("TMP " + tmp + " " + tmp2);
- t = t.concat(tmp.split("__")[tmp.split("__").length - 1] + "." + tmp2.split("__")[Math.max(tmp2.split("__").length - 2, 0)] + " ");
- } else {
- t = t.concat(str + " ");
- }
- }
- } else if (p.getName().contains("Authenticity")) {
- }
- s = s.concat(t + "\n");
- i++;
- }
- pragma.setValue(s);
- pragma.makeValue();
- abd.addComponent(pragma, xpos, ypos, false, true);
-
- TraceManager.addDev("val " + pragma.getValues().length);
-
- }
-
-
-}
diff --git a/src/main/java/ui/GTURTLEModeling.java b/src/main/java/ui/GTURTLEModeling.java
index fed79b1ebf88716518d800c32e0202818d8b6b8f..82f441c09dd3e211f2db8ef33af8edd1200041a5 100644
--- a/src/main/java/ui/GTURTLEModeling.java
+++ b/src/main/java/ui/GTURTLEModeling.java
@@ -1894,19 +1894,22 @@ public class GTURTLEModeling {
}
public void generateFullAvatarFromTML() {
- if (tmlm != null && tmap == null) {
+ /*if (tmlm != null && tmap == null) {
tmap = tmlm.getDefaultMapping();
- }
+ }*/
- FullTML2Avatar t2a = new FullTML2Avatar(tmap);
+ FullTML2Avatar t2a = new FullTML2Avatar(tmlm);
TraceManager.addDev("Avatar spec generation");
avatarspec = t2a.generateAvatarSpec("1");
if (mgui.isExperimentalOn()) {
- mgui.drawAvatarSpecification(avatarspec);
- AvatarSpecification av2 = avatarspec.advancedClone();
- mgui.drawAvatarSpecification(av2);
+
+ TraceManager.addDev("Avatar spec:" + avatarspec.toString());
+ //mgui.drawAvatarSpecification(avatarspec);
+ //TraceManager.addDev("Avatar spec:" + avatarspec.toString());
+ //AvatarSpecification av2 = avatarspec.advancedClone();
+ //mgui.drawAvatarSpecification(av2);
}
}
@@ -9041,6 +9044,7 @@ public class GTURTLEModeling {
public void drawBlockProperties(AvatarBlock ab, AvatarBDBlock bl) {
for (avatartranslator.AvatarSignal sig : ab.getSignals()) {
String name = sig.getName().split("__")[sig.getName().split("__").length - 1];
+
// sig.setName(name);
String[] types = new String[sig.getListOfAttributes().size()];
String[] typeIds = new String[sig.getListOfAttributes().size()];
@@ -9050,7 +9054,7 @@ public class GTURTLEModeling {
typeIds[i] = attr.getName();
i++;
}
- TraceManager.addDev("Adding signal " + sig);
+ //TraceManager.addDev("Adding signal " + sig + " with name=" + name);
bl.addSignal(new ui.AvatarSignal(sig.getInOut(), name, types, typeIds));
}
@@ -9207,7 +9211,7 @@ public class GTURTLEModeling {
//Add Relations to connector
for (AvatarRelation ar : avspec.getRelations()) {
if (ar.block1.getName().contains(bl1) && ar.block2.getName().contains(bl2) || ar.block1.getName().contains(bl2) && ar.block2.getName().contains(bl1)) {
-
+ //TraceManager.addDev("Trying adding signal relations to connector");
//TGConnectingPoint p1= blockMap.get(bl1).getFreeTGConnectingPoint(blockMap.get(bl1).getX(), blockMap.get(bl1).getY());
conn.setAsynchronous(ar.isAsynchronous());
@@ -9218,8 +9222,10 @@ 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());
conn.addSignal(ar.getSignal1(i).toString(), ar.getSignal1(i).getInOut() == 0, ar.block1.getName().contains(bl1));
- conn.addSignal(ar.getSignal2(i).toString(), ar.getSignal2(i).getInOut() == 0, !ar.block1.getName().contains(bl1));
+ 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));
//
}
//
diff --git a/src/main/java/ui/avatarbd/AvatarBDBlock.java b/src/main/java/ui/avatarbd/AvatarBDBlock.java
index aa784a0c273bbede5ebac563d35ecbd629cb7148..39881d5d2ea0bdd37361cd9981d9271fabed6bc7 100644
--- a/src/main/java/ui/avatarbd/AvatarBDBlock.java
+++ b/src/main/java/ui/avatarbd/AvatarBDBlock.java
@@ -1603,20 +1603,22 @@ public class AvatarBDBlock extends TGCScalableWithInternalComponent implements S
_id = _id.trim();
//TraceManager.addDev("Searching for signal with id=" + _id);
for (AvatarSignal as : this.mySignals) {
- //
+ //TraceManager.addDev("signal? " + as.getId());
if (as.getId().compareTo(_id) == 0)
return as;
}
- //TraceManager.addDev("Not found");
+ TraceManager.addDev("Not found");
return null;
}
public AvatarSignal getAvatarSignalFromFullName(String _id) {
if (_id.startsWith("in ")) {
+ //TraceManager.addDev("in signal");
return getSignalNameBySignalDef(_id.substring(3, _id.length()).trim());
}
if (_id.startsWith("out ")) {
+ //TraceManager.addDev("out signal");
return getSignalNameBySignalDef(_id.substring(4, _id.length()).trim());
}
return null;
diff --git a/src/main/java/ui/avatarbd/AvatarBDPortConnector.java b/src/main/java/ui/avatarbd/AvatarBDPortConnector.java
index 1d05088800697c203d9aa4ab87315a28fa17dfc8..be4e463338b4d182ff2aad5f4d864ae150786c14 100644
--- a/src/main/java/ui/avatarbd/AvatarBDPortConnector.java
+++ b/src/main/java/ui/avatarbd/AvatarBDPortConnector.java
@@ -602,19 +602,30 @@ public class AvatarBDPortConnector extends TGConnectorWithCommentConnectionPoint
String s;
for (i = 0; i < outSignalsAtOrigin.size(); i++) {
+ //TraceManager.addDev("out sig origin");
try {
+ //TraceManager.addDev("sig block1: " + block1.getAvatarSignalFromFullName(outSignalsAtOrigin.get(i)).toString());
+ //TraceManager.addDev("Found");
+ //TraceManager.addDev("Size of in at dest:" + inSignalsAtDestination.size() + " signal name:" + inSignalsAtDestination.get(i)
+ //.toString());
+ //TraceManager.addDev("Sig block2: " + block2.getAvatarSignalFromFullName(inSignalsAtDestination.get(i)).toString());
+
+ //TraceManager.addDev("Found");
s = makeSignalAssociation(block1, block1.getAvatarSignalFromFullName(outSignalsAtOrigin.get(i)), block2, block2.getAvatarSignalFromFullName(inSignalsAtDestination.get(i)));
v.add(s);
} catch (Exception e) {
+ TraceManager.addDev("Exception: signal removed? out origin");
// Probably a signal has been removed
}
}
for (i = 0; i < inSignalsAtOrigin.size(); i++) {
+ //TraceManager.addDev("in sig origin");
try {
s = makeSignalAssociation(block1, block1.getAvatarSignalFromFullName(inSignalsAtOrigin.get(i)), block2, block2.getAvatarSignalFromFullName(outSignalsAtDestination.get(i)));
v.add(s);
} catch (Exception e) {
+ TraceManager.addDev("Exception: signal removed? in origin");
// Probably a signal has been removed
}
}
@@ -691,8 +702,15 @@ public class AvatarBDPortConnector extends TGConnectorWithCommentConnectionPoint
}
public void updateAllSignals() {
+ TraceManager.addDev("Updating signals");
try {
Vector<String> v = getAssociationSignals();
+
+
+ for (String s: v) {
+ TraceManager.addDev("Assoc: " + s);
+ }
+
//
inSignalsAtOrigin.clear();
inSignalsAtDestination.clear();
@@ -711,7 +729,7 @@ public class AvatarBDPortConnector extends TGConnectorWithCommentConnectionPoint
for (int i = 0; i < v.size(); i++) {
assoc = v.get(i);
- //TraceManager.addDev("assoc=" + assoc);
+ TraceManager.addDev("assoc=" + assoc);
as1 = block1.getSignalNameBySignalDef(getFirstSignalOfSignalAssociation(assoc));
as2 = block2.getSignalNameBySignalDef(getSecondSignalOfSignalAssociation(assoc));
if ((as1 != null) && (as2 != null)) {
diff --git a/src/main/java/ui/tmlad/TMLActivityDiagramToolBar.java b/src/main/java/ui/tmlad/TMLActivityDiagramToolBar.java
index f3cb3c410213708c0aaa6e7677325fed733f3686..8c29b428146cd1142038cd6e1dc0a761b4a2c9e8 100755
--- a/src/main/java/ui/tmlad/TMLActivityDiagramToolBar.java
+++ b/src/main/java/ui/tmlad/TMLActivityDiagramToolBar.java
@@ -83,7 +83,7 @@ public class TMLActivityDiagramToolBar extends TToolBar {
mgui.actions[TGUIAction.TMLAD_SEND_REQUEST].setEnabled(b);
mgui.actions[TGUIAction.TMLAD_SEND_EVENT].setEnabled(b);
mgui.actions[TGUIAction.TMLAD_WAIT_EVENT].setEnabled(b);
- mgui.actions[TGUIAction.TMLAD_WRITE_CAMS].setEnabled(b);
+ mgui.actions[TGUIAction.TMLAD_WRITE_CAMS].setEnabled(b);
mgui.actions[TGUIAction.TMLAD_READ_CAMS].setEnabled(b);
mgui.actions[TGUIAction.TMLAD_NOTIFIED_EVENT].setEnabled(b);
mgui.actions[TGUIAction.TMLAD_READ_REQUEST_ARG].setEnabled(b);
@@ -140,8 +140,6 @@ public class TMLActivityDiagramToolBar extends TToolBar {
button = this.add(mgui.actions[TGUIAction.TMLAD_WRITE_CHANNEL]);
button.addMouseListener(mgui.mouseHandler);
- button = this.add(mgui.actions[TGUIAction.TMLAD_WRITE_CAMS]);
- button.addMouseListener(mgui.mouseHandler);
button = this.add(mgui.actions[TGUIAction.TMLAD_SEND_EVENT]);
button.addMouseListener(mgui.mouseHandler);
@@ -155,8 +153,7 @@ public class TMLActivityDiagramToolBar extends TToolBar {
button.addMouseListener(mgui.mouseHandler);
- button = this.add(mgui.actions[TGUIAction.TMLAD_READ_CAMS]);
- button.addMouseListener(mgui.mouseHandler);
+
button = this.add(mgui.actions[TGUIAction.TMLAD_WAIT_EVENT]);
@@ -168,6 +165,14 @@ public class TMLActivityDiagramToolBar extends TToolBar {
button = this.add(mgui.actions[TGUIAction.TMLAD_READ_REQUEST_ARG]);
button.addMouseListener(mgui.mouseHandler);
+ this.addSeparator();
+
+ button = this.add(mgui.actions[TGUIAction.TMLAD_WRITE_CAMS]);
+ button.addMouseListener(mgui.mouseHandler);
+
+ button = this.add(mgui.actions[TGUIAction.TMLAD_READ_CAMS]);
+ button.addMouseListener(mgui.mouseHandler);
+
this.addSeparator();
button = this.add(mgui.actions[TGUIAction.TMLAD_ACTION_STATE]);
diff --git a/src/main/java/ui/util/DefaultText.java b/src/main/java/ui/util/DefaultText.java
index a4e2d1c863a24a9c8cf59481eb44995fe85050fb..e3a611265e40cae88ba13ad2f6074ca95b45e09a 100755
--- a/src/main/java/ui/util/DefaultText.java
+++ b/src/main/java/ui/util/DefaultText.java
@@ -50,8 +50,8 @@ package ui.util;
*/
public class DefaultText {
- public static String BUILD = "13464";
- public static String DATE = "2020/06/25 03:02:23 CET";
+ public static String BUILD = "13470";
+ public static String DATE = "2020/07/01 03:02:21 CET";
public static StringBuffer sbAbout = makeAbout();
diff --git a/src/main/java/ui/window/JDialogAvatarModelChecker.java b/src/main/java/ui/window/JDialogAvatarModelChecker.java
index 9a97fb1ce519444f3bf2154afb7f1068f991e855..609b25baf477a3457301ac043eb814fcee326dd9 100644
--- a/src/main/java/ui/window/JDialogAvatarModelChecker.java
+++ b/src/main/java/ui/window/JDialogAvatarModelChecker.java
@@ -42,6 +42,7 @@ package ui.window;
import avatartranslator.AvatarSpecification;
import avatartranslator.AvatarStateMachineElement;
import avatartranslator.modelchecker.AvatarModelChecker;
+import avatartranslator.modelchecker.CounterexampleQueryReport;
import avatartranslator.modelchecker.SafetyProperty;
import avatartranslator.modelchecker.SpecificationReachability;
import avatartranslator.modelchecker.SpecificationPropertyPhase;
@@ -106,6 +107,7 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
protected static boolean checkReinitSelected = false;
protected static boolean limitStatesSelected = false;
protected static boolean generateCountertraceSelected = false;
+ protected static boolean generateCountertraceAUTSelected = false;
protected static String countertracePath;
protected static String stateLimitValue;
protected static boolean limitTimeSelected = false;
@@ -159,6 +161,7 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
protected JCheckBox reinit;
protected JCheckBox safety;
protected JCheckBox countertrace;
+ protected JCheckBox countertraceAUT;
protected JTextField countertraceField;
protected JButton checkUncheckAllPragmas;
protected java.util.List<JCheckBox> customChecks;
@@ -456,6 +459,9 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
countertrace = new JCheckBox("Generate counterexample traces", generateCountertraceSelected);
countertrace.addActionListener(this);
jpadvanced.add(countertrace, cadvanced);
+ countertraceAUT = new JCheckBox("Generate counterexample AUT graphs", generateCountertraceAUTSelected);
+ countertraceAUT.addActionListener(this);
+ jpadvanced.add(countertraceAUT, cadvanced);
cadvanced.gridwidth = GridBagConstraints.REMAINDER;
countertraceField = new JTextField(countertracePath);
jpadvanced.add(countertraceField, cadvanced);
@@ -723,12 +729,13 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
timer.scheduleAtFixedRate(mcm, 0, 500);
// Setting options
+ amc.setCompressionFactor(2);
amc.setIgnoreEmptyTransitions(ignoreEmptyTransitionsSelected);
amc.setIgnoreConcurrenceBetweenInternalActions(ignoreConcurrenceBetweenInternalActionsSelected);
amc.setIgnoreInternalStates(ignoreInternalStatesSelected);
amc.setCheckNoDeadlocks(checkNoDeadSelected);
amc.setReinitAnalysis(checkReinitSelected);
- amc.setCounterExampleTrace(generateCountertraceSelected, false);
+ amc.setCounterExampleTrace(generateCountertraceSelected, generateCountertraceAUTSelected);
// Reachability
int res;
@@ -901,24 +908,39 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
if (generateCountertraceSelected) {
String trace = amc.getCounterTrace();
- String autfile;
+ String file;
if (countertraceField.getText().indexOf("$") != -1) {
- autfile = Conversion.replaceAllChar(countertraceField.getText(), '$', dateAndTime);
+ file = Conversion.replaceAllChar(countertraceField.getText(), '$', dateAndTime);
} else {
- autfile = countertraceField.getText();
+ file = countertraceField.getText();
}
try {
- FileUtils.saveFile(autfile, trace);
- jta.append("\nCounterexample trace saved in " + autfile + "\n");
+ File f = new File(file);
+ FileUtils.saveFile(file, trace);
+ jta.append("\nCounterexample trace saved in " + file + "\n");
} catch (Exception e) {
- jta.append("\nCounterexample trace could not be saved in " + autfile + "\n");
+ jta.append("\nCounterexample trace could not be saved in " + file + "\n");
}
- List<String> autTraces = amc.getAUTTraces();
+ List<CounterexampleQueryReport> autTraces = amc.getAUTTraces();
if (autTraces != null) {
- for (String tr : autTraces) {
- System.out.println(tr + "\n");
- mgui.showAUTFromString("Last RG", tr);
+ int i = 0;
+ String autfile = FileUtils.removeFileExtension(file);
+ for (CounterexampleQueryReport tr : autTraces) {
+ String filename = autfile + "_" + i + ".aut";
+ try {
+ RG rg = new RG(file);
+ rg.data = tr.getReport();
+ rg.fileName = filename;
+ rg.name = tr.getQuery();
+ mgui.addRG(rg);
+ File f = new File(filename);
+ FileUtils.saveFile(filename, tr.getReport());
+ jta.append("Counterexample graph trace " + tr.getQuery() + " saved in " + filename + "\n");
+ } catch (Exception e) {
+ jta.append("Counterexample graph trace "+ tr.getQuery() + " could not be saved in " + filename + "\n");
+ }
+ i++;
}
}
}
@@ -1091,8 +1113,11 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
}
countertrace.setEnabled(safety.isSelected() || noDeadlocks.isSelected());
+ countertraceAUT.setEnabled(countertrace.isSelected());
countertraceField.setEnabled(countertrace.isSelected());
generateCountertraceSelected = countertrace.isSelected();
+ generateCountertraceAUTSelected = countertraceAUT.isSelected();
+
stateLimitField.setEnabled(stateLimit.isSelected());
limitStatesSelected = stateLimit.isSelected();
diff --git a/ttool/src/test/java/avatartranslator/AvatarExpressionTest.java b/ttool/src/test/java/avatartranslator/AvatarExpressionTest.java
index a76a076d8afabc8af08b6e490bee157baad5a5a6..34c35bdd04568fba88f11a9137c2b73cb11b4604 100644
--- a/ttool/src/test/java/avatartranslator/AvatarExpressionTest.java
+++ b/ttool/src/test/java/avatartranslator/AvatarExpressionTest.java
@@ -134,12 +134,17 @@ public class AvatarExpressionTest {
@Test
public void testBlock() {
SpecificationBlock specBlock = new SpecificationBlock();
- specBlock.init(block1, false);
+ specBlock.init(block1, false, false);
int[] attributes = {2, 3, 7, 0, 1};
+ AvatarExpressionSolver.emptyAttributesMap();
+
AvatarExpressionSolver e1 = new AvatarExpressionSolver("x + y");
assertTrue(e1.buildExpression(block1));
AvatarExpressionSolver e2 = new AvatarExpressionSolver("-x / y - 15 * z + 1 == -31");
+ assertTrue(AvatarExpressionSolver.containsElementAttribute(block1.getAttribute(0)));
+ assertTrue(AvatarExpressionSolver.containsElementAttribute(block1.getAttribute(1)));
+ assertFalse(AvatarExpressionSolver.containsElementAttribute(block1.getAttribute(2)));
assertTrue(e2.buildExpression(block1));
AvatarExpressionSolver e3 = new AvatarExpressionSolver("not(-x / z - (x + y) * 2 + 1 >= -(60 - 26))");
assertTrue(e3.buildExpression(block1));
@@ -180,18 +185,42 @@ public class AvatarExpressionTest {
@Test
public void testSpec() {
+ as.sortAttributes();
+ as.setAttributeOptRatio(2);
SpecificationState ss = new SpecificationState();
ss.setInit(as, false);
+ AvatarExpressionSolver.emptyAttributesMap();
AvatarExpressionSolver e1 = new AvatarExpressionSolver("block1.x + block2.y");
assertTrue(e1.buildExpression(as));
AvatarExpressionSolver e2 = new AvatarExpressionSolver("-block1.x / block1.y - 15 * block2.z + 1 == -46");
+ assertTrue(AvatarExpressionSolver.containsElementAttribute(block1.getAttribute(0)));
+ assertTrue(AvatarExpressionSolver.containsElementAttribute(block2.getAttribute(1)));
+ assertFalse(AvatarExpressionSolver.containsElementAttribute(block1.getAttribute(1)));
+ assertFalse(AvatarExpressionSolver.containsElementAttribute(block2.getAttribute(0)));
assertTrue(e2.buildExpression(as));
+ assertTrue(AvatarExpressionSolver.containsElementAttribute(block2.getAttribute(2)));
AvatarExpressionSolver e3 = new AvatarExpressionSolver("not(-block2.x / block2.z - not(block1.x + block2.y) * -2 + -(1) <= -(-4 + 7))");
assertFalse(e3.buildExpression(as));
assertTrue(e1.getResult(ss) == 17);
assertTrue(e2.getResult(ss) == 1);
assertTrue(e3.getResult(ss) == 0);
+
+ as.removeConstants();
+ as.sortAttributes();
+ as.setAttributeOptRatio(4);
+ ss = new SpecificationState();
+ ss.setInit(as, false);
+
+ e1 = new AvatarExpressionSolver("block1.x + block2.y");
+ assertTrue(e1.buildExpression(as));
+ e2 = new AvatarExpressionSolver("-block1.x / block1.y - 15 * block2.z + 1 == -46");
+ assertTrue(e2.buildExpression(as));
+ e3 = new AvatarExpressionSolver("not(-block2.x / block2.z - not(block1.x + block2.y) * -2 + -(1) <= -(-4 + 7))");
+ assertFalse(e3.buildExpression(as));
+ assertTrue(e1.getResult(ss) == 17);
+ assertTrue(e2.getResult(ss) == 1);
+ assertTrue(e3.getResult(ss) == 0);
}
}