diff --git a/src/tmltranslator/TMLRequest.java b/src/tmltranslator/TMLRequest.java
index 51ac20f00247af9967d0af2e4e10b67bcc73185b..9b0cc46dc7b0c3446782954147b8de769bc14aa2 100755
--- a/src/tmltranslator/TMLRequest.java
+++ b/src/tmltranslator/TMLRequest.java
@@ -84,10 +84,10 @@ public class TMLRequest extends TMLCommunicationElement {
}
}
public String getParam(int i){
- if (i<getNbOfParams()) {
+ if (i<paramNames.size()) {
return paramNames.get(i);
} else {
- return null;
+ return "";
}
}
public void setDestinationTask(TMLTask _task) {
diff --git a/src/tmltranslator/toavatar/TML2Avatar.java b/src/tmltranslator/toavatar/TML2Avatar.java
index 44cbba389824f968a151418d97a6f4d30111a0a1..d9b968264c5531d17a14dadc52925318443597ab 100644
--- a/src/tmltranslator/toavatar/TML2Avatar.java
+++ b/src/tmltranslator/toavatar/TML2Avatar.java
@@ -51,6 +51,8 @@ import java.util.HashMap;
import java.util.Map;
import java.util.HashSet;
import java.util.Vector;
+import java.util.regex.Matcher;
+import java.util.regex.Pattern;
import java.io.*;
import javax.swing.*;
import java.util.ArrayList;
@@ -79,6 +81,7 @@ public class TML2Avatar {
private final static Integer channelPublic = 0;
private final static Integer channelPrivate = 1;
private final static Integer channelUnreachable = 2;
+ public int loopLimit = 1;
AvatarSpecification avspec;
ArrayList<String> attrsToCheck;
List<String> allStates;
@@ -690,32 +693,58 @@ public class TML2Avatar {
else if (ae instanceof TMLForLoop){
TMLForLoop loop = (TMLForLoop)ae;
if (loop.isInfinite()){
- List<AvatarStateMachineElement> elements = translateState(ae.getNextElement(0), block);
- //AvatarTransition looptran = new AvatarTransition(block, "loop__"+ae.getName(), null);
- //elementList.addAll(elements);
- //elementList.add(looptran);
- //replace stop states and point empty transitions to start of loop
+ //Make initializaton, then choice state with transitions
+ List<AvatarStateMachineElement> elements=translateState(ae.getNextElement(0), block);
+ List<AvatarStateMachineElement> afterloop = translateState(ae.getNextElement(1), block);
+ AvatarState initState = new AvatarState(ae.getName()+"__init", ae.getReferenceObject());
+ elementList.add(initState);
+ //Build transition to choice
+ tran = new AvatarTransition(block, "loop_init__"+ae.getName(), ae.getReferenceObject());
+ tran.addAction(AvatarTerm.createActionFromString(block, "loop_index=0"));
+ elementList.add(tran);
+ initState.addNext(tran);
+ //Choice state
+ AvatarState as = new AvatarState(ae.getName()+"__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){
- e.addNext(elements.get(0));
+ e.addNext(as);
elementList.add(e);
}
else if (e.getNext(0) instanceof AvatarStopState){
//Remove the transition to AvatarStopState
e.removeNext(0);
- e.addNext(elements.get(0));
+ e.addNext(as);
elementList.add(e);
}
else {
elementList.add(e);
}
}
+
+ //Transition if exiting loop
+ tran=new AvatarTransition(block, "end_loop__"+ae.getName(), ae.getReferenceObject());
+ tran.setGuard(new AvatarGuardElse());
+ as.addNext(tran);
+ AvatarStopState stop = new AvatarStopState("stop", null);
+ tran.addNext(stop);
+ elementList.add(tran);
+ elementList.add(stop);
return elementList;
}
else {
- boolean guardEx=true;
//Make initializaton, then choice state with transitions
List<AvatarStateMachineElement> elements=translateState(ae.getNextElement(0), block);
List<AvatarStateMachineElement> afterloop = translateState(ae.getNextElement(1), block);
@@ -724,6 +753,7 @@ public class TML2Avatar {
//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
@@ -732,21 +762,15 @@ public class TML2Avatar {
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));
AvatarGuard guard = AvatarGuard.createFromString (block, loop.getCondition().replaceAll("<", "!="));
- if (guard.isElseGuard()) {
- tran.setGuard(guard);
- } else {
- int error = AvatarSyntaxChecker.isAValidGuard(avspec, block, loop.getCondition().replaceAll("<","!="));
- if (error < 0 || loop.getCondition().length()>4) {
- //guardEx=false;
- AvatarGuard defaultGuard = AvatarGuard.createFromString(block, loop.getCondition().split("<")[0]+"!=5");
- tran.setGuard(defaultGuard);
- System.out.println("cannot translate guard " + loop.getCondition().replaceAll("<", "!="));
- } else {
- tran.setGuard(guard);
- }
+ int error = AvatarSyntaxChecker.isAValidGuard(avspec, block, loop.getCondition().replaceAll("<","!="));
+ if (error != 0) {
+ tran.addGuard(loop.getCondition().replaceAll("<", "!="));
}
tran.addAction(AvatarTerm.createActionFromString(block, loop.getIncrement()));
+ tran.addAction(AvatarTerm.createActionFromString(block, "loop_index = loop_index + 1"));
tran.addNext(elements.get(0));
as.addNext(tran);
elementList.add(tran);
@@ -771,9 +795,7 @@ public class TML2Avatar {
//Transition if exiting loop
tran=new AvatarTransition(block, "end_loop__"+ae.getName(), ae.getReferenceObject());
- if (guardEx){
- tran.setGuard(new AvatarGuardElse());
- }
+ tran.setGuard(new AvatarGuardElse());
as.addNext(tran);
if (afterloop.size()==0){
afterloop.add(new AvatarStopState("stop", null));
@@ -844,7 +866,7 @@ public class TML2Avatar {
}*/
- public AvatarSpecification generateAvatarSpec(){
+ public AvatarSpecification generateAvatarSpec(String _loopLimit){
//TODO: Add pragmas
//TODO: Make state names readable
//TODO: Put back numeric guards
@@ -856,7 +878,14 @@ public class TML2Avatar {
return avspec;
}
attrsToCheck.clear();
-
+
+ //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;
@@ -878,6 +907,8 @@ public class TML2Avatar {
//Add temp variable for unsendable signals
AvatarAttribute tmp = new AvatarAttribute("tmp", 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){
@@ -897,6 +928,10 @@ public class TML2Avatar {
//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
@@ -904,62 +939,97 @@ public class TML2Avatar {
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);
- AvatarSignal sig = new AvatarSignal(block.getName()+"__IN__"+request.getName(), AvatarSignal.IN, request.getReferenceObject());
- block.addSignal(sig);
- signals.add(sig);
- AvatarActionOnSignal as= new AvatarActionOnSignal("getRequest__"+request.getName(), sig, request.getReferenceObject());
- at.addNext(as);
- asm.addElement(as);
- as.addValue(request.getName()+"__reqData");
- AvatarAttribute requestData= new AvatarAttribute(request.getName()+"__reqData", AvatarType.INTEGER, block, null);
- block.addAttribute(requestData);
- for (int i=0; i< request.getNbOfParams(); i++){
- if (block.getAvatarAttributeWithName(request.getParam(i))==null){
- //Throw Error
- as.addValue("tmp");
- }
- else {
- as.addValue(request.getParam(i));
- }
- }
- AvatarTransition tran = new AvatarTransition(block, "__after_" + request.getName(), task.getActivityDiagram().get(0).getReferenceObject());
- as.addNext(tran);
- asm.addElement(tran);
+
+ AvatarState loopstart = new AvatarState("loopstart", task.getActivityDiagram().get(0).getReferenceObject());
+ at.addNext(loopstart);
+ asm.addElement(loopstart);
//Find the original start state, transition, and next element
AvatarStateMachineElement start = elementList.get(0);
AvatarStateMachineElement startTran= start.getNext(0);
AvatarStateMachineElement newStart = startTran.getNext(0);
- tran.addNext(newStart);
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()));
- asm.addElement(e);
stateObjectMap.put(task.getName()+"__"+e.getName(), e.getReferenceObject());
- }
- /* if (e instanceof AvatarStopState){
+
+ if (e instanceof AvatarStopState){
//ignore it
}
else {
for (int i=0; i< e.getNexts().size(); i++){
if (e.getNext(i) instanceof AvatarStopState){
e.removeNext(i);
- //Route it back to the state with request
- e.addNext(as);
+ //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());
+
+
+ //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 (!signalMap.containsKey(block.getName()+"__IN__"+req.getName())){
+ sig = new AvatarSignal(block.getName()+"__IN__"+req.getName(), AvatarSignal.IN, req.getReferenceObject());
+ block.addSignal(sig);
+ signals.add(sig);
+ signalMap.put(block.getName()+"__IN__"+req.getName(),sig);
+ }
+ else {
+ sig = signalMap.get(block.getName()+"__IN__"+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< request.getNbOfParams(); i++){
+ if (block.getAvatarAttributeWithName(request.getParam(i))==null){
+ //Throw Error
+ as.addValue("tmp");
+ }
+ else {
+ as.addValue(request.getParam(i));
+ }
+ }
+ AvatarTransition tran = new AvatarTransition(block, "__after_" + request.getName(), task.getActivityDiagram().get(0).getReferenceObject());
+ as.addNext(tran);
+ asm.addElement(tran);
+ tran.addNext(newStart);
+ }
+
+
+
+
+
+
+
asm.setStartState((AvatarStartState) ss);
+
}
else {
+ //Not requested
List<AvatarStateMachineElement> elementList= translateState(task.getActivityDiagram().get(0), block);
for (AvatarStateMachineElement e: elementList){
e.setName(processName(e.getName(), e.getID()));
@@ -1134,7 +1204,7 @@ public class TML2Avatar {
avspec.addRelation(ar);
}
for (AvatarSignal sig: signals){
- //$%^&*() check that all signals are put in relations
+ //check that all signals are put in relations
AvatarRelation ar = avspec.getAvatarRelationWithSignal(sig);
if (ar==null){
System.out.println("missing relation for " + sig.getName());
diff --git a/src/ui/GTURTLEModeling.java b/src/ui/GTURTLEModeling.java
index ce16d877b7e0eb702ef97c7ad037da687b571b08..e5ed370137af966ca4cf622187e5aa6f471bfa69 100755
--- a/src/ui/GTURTLEModeling.java
+++ b/src/ui/GTURTLEModeling.java
@@ -633,16 +633,18 @@ public class GTURTLEModeling {
return this.avatar2proverif.getOutputAnalyzer ();
}
- public boolean generateProVerifFromAVATAR(String _path, int _stateReachability, boolean _typed) {
- if (avatarspec==null){
- if (tmap!=null){
- t2a = new TML2Avatar(tmap);
- avatarspec = t2a.generateAvatarSpec();
- }
- else {
- return false;
- }
+ public boolean generateProVerifFromAVATAR(String _path, int _stateReachability, boolean _typed){
+ return generateProVerifFromAVATAR(_path, _stateReachability, _typed, "1");
+ }
+ public boolean generateProVerifFromAVATAR(String _path, int _stateReachability, boolean _typed, String loopLimit) {
+ if (tmap!=null){
+ t2a = new TML2Avatar(tmap);
+ avatarspec = t2a.generateAvatarSpec(loopLimit);
}
+ else {
+ return false;
+ }
+
avatar2proverif = new AVATAR2ProVerif(avatarspec);
//tml2uppaal.setChoiceDeterministic(choices);
//tml2uppaal.setSizeInfiniteFIFO(_size);
diff --git a/src/ui/window/JDialogProVerifGeneration.java b/src/ui/window/JDialogProVerifGeneration.java
index 615d627b821475b2cd3cb40dd488bb07e1520267..f55a9746d839ff840de5bf661ce2647ac9b329ca 100644
--- a/src/ui/window/JDialogProVerifGeneration.java
+++ b/src/ui/window/JDialogProVerifGeneration.java
@@ -93,7 +93,7 @@ public class JDialogProVerifGeneration extends javax.swing.JDialog implements Ac
protected JRadioButton exe, exeint;
protected ButtonGroup exegroup;
protected JLabel gen, comp;
- protected JTextField code1, code2, unitcycle, compiler1, exe1, exe2, exe3, exe2int;
+ protected JTextField code1, code2, unitcycle, compiler1, exe1, exe2, exe3, exe2int, loopLimit;
protected JTabbedPane jp1;
protected JScrollPane jsp;
protected JCheckBox outputOfProVerif, typedLanguage;
@@ -209,8 +209,10 @@ public class JDialogProVerifGeneration extends javax.swing.JDialog implements Ac
typedLanguage = new JCheckBox("Generate typed Pi calculus");
typedLanguage.setSelected(true);
jp01.add(typedLanguage, c01);
-
-
+ jp01.add(new JLabel("Limit on loop iterations"));
+ c01.gridwidth= GridBagConstraints.REMAINDER;
+ loopLimit = new JTextField("1", 3);
+ jp01.add(loopLimit,c01);
/*optimizemode = new JCheckBox("Optimize code");
optimizemode.setSelected(optimizeModeSelected);
jp01.add(optimizemode, c01);
@@ -375,8 +377,7 @@ public class JDialogProVerifGeneration extends javax.swing.JDialog implements Ac
// FIXME Raise error
System.out.println("FILE EXISTS!!!");
}
-
- if (mgui.gtm.generateProVerifFromAVATAR(pathCode, stateReachabilityAll.isSelected () ? REACHABILITY_ALL : stateReachabilitySelected.isSelected () ? REACHABILITY_SELECTED : REACHABILITY_NONE, typedLanguage.isSelected())) {
+ if (mgui.gtm.generateProVerifFromAVATAR(pathCode, stateReachabilityAll.isSelected () ? REACHABILITY_ALL : stateReachabilitySelected.isSelected () ? REACHABILITY_SELECTED : REACHABILITY_NONE, typedLanguage.isSelected(), loopLimit.getText())) {
jta.append("ProVerif code generation done\n");
} else {
setError();