diff --git a/src/avatartranslator/AvatarAttribute.java b/src/avatartranslator/AvatarAttribute.java index 7700a33a2258a31de110971569bb720456cb685d..65b46523c206d95ff85c83512de56c17e3c654e7 100644 --- a/src/avatartranslator/AvatarAttribute.java +++ b/src/avatartranslator/AvatarAttribute.java @@ -92,10 +92,6 @@ public class AvatarAttribute extends AvatarElement{ return (type == AvatarType.INTEGER); } - public boolean isNat() { - return (type == AvatarType.NATURAL); - } - public boolean isBool() { return (type == AvatarType.BOOLEAN); } diff --git a/src/avatartranslator/AvatarSyntaxChecker.java b/src/avatartranslator/AvatarSyntaxChecker.java index 3235a7facaecb75cde3f27b726af80e9e6f648f2..785be91ce500195e1fe1391da54d66c75f4791ad 100644 --- a/src/avatartranslator/AvatarSyntaxChecker.java +++ b/src/avatartranslator/AvatarSyntaxChecker.java @@ -87,7 +87,7 @@ public class AvatarSyntaxChecker { String action = _expr.substring(index0 + 1, _expr.length()).trim(); - if (aa.isInt() || aa.isNat()) { + if (aa.isInt()) { return parse(_as, _ab, "actionnat", action); } else if (aa.isBool()) { return parse(_as, _ab, "actionbool", action); diff --git a/src/avatartranslator/AvatarType.java b/src/avatartranslator/AvatarType.java index a0a489ea9a52deaf9b3da4133962d3737e3f883c..ad34ef363ee89190a9dda5b2c7262226d2b41ab6 100644 --- a/src/avatartranslator/AvatarType.java +++ b/src/avatartranslator/AvatarType.java @@ -54,42 +54,43 @@ import myutil.*; public class AvatarType { // Types of parameters - public final static int NATURAL = 0; + //public final static int NATURAL = 0; public final static int BOOLEAN = 1; public final static int INTEGER = 2; + public final static int TIMER = 3; public static int getType(String s) { - if (s.equals("nat")) { - return NATURAL; - } else if (s.equals("bool")) { + if (s.equals("bool")) { return BOOLEAN; } else if (s.equals("int")) { return INTEGER; + } else if (s.equals("Timer")) { + return TIMER; } return -1; } public static String getStringType(int _type) { switch(_type) { - case NATURAL: - return "nat"; case BOOLEAN: return "bool"; case INTEGER: return "int"; + case TIMER: + return "timer"; } return ""; } public static String getDefaultInitialValue(int _type) { switch(_type) { - case NATURAL: - return "0"; case BOOLEAN: return "false"; case INTEGER: return "0"; + case TIMER: + return "0"; } return ""; } diff --git a/src/avatartranslator/touppaal/AVATAR2UPPAAL.java b/src/avatartranslator/touppaal/AVATAR2UPPAAL.java index 3e730c37aad5857d1bf56d48a3dd207f794d90c9..d315fd24bf656237972d46f765a813b324ff1346 100755 --- a/src/avatartranslator/touppaal/AVATAR2UPPAAL.java +++ b/src/avatartranslator/touppaal/AVATAR2UPPAAL.java @@ -318,7 +318,7 @@ public class AVATAR2UPPAAL { for(i=0; i<_block.attributeNb(); i++) { aa = _block.getAttribute(i); - if (aa.isInt() || aa.isNat()) { + if (aa.isInt()) { _template.addDeclaration("int "); } else { _template.addDeclaration("bool "); @@ -418,7 +418,7 @@ public class AVATAR2UPPAAL { for(AvatarAttribute aa: sig1.getListOfAttributes()) { listName = "list__" + name0 + "_" + cpt; - if (aa.isInt() || aa.isNat()) { + if (aa.isInt()) { templateAsynchronous.addDeclaration("int " + listName + "[" + ar.getSizeOfFIFO() + "];\n"); enqueue += " " + listName + "[tail__" + name0 + "] = " + ACTION_INT + cpt + ";\n"; dequeue += " " + ACTION_INT + cpt + " = " + listName + "[tail__" + name0 + "] " + ";\n"; @@ -843,7 +843,7 @@ public class AVATAR2UPPAAL { if ((nbOfInt > 0) || (nbOfBool > 0)) { result = result + ",\n"; } - if (aa.isInt() || aa.isNat()) { + if (aa.isInt()) { result = result + ACTION_INT + nbOfInt + " =" + aa.getName(); nbOfInt ++; } else { @@ -930,7 +930,7 @@ public class AVATAR2UPPAAL { val = _aaos.getValue(i); aa = _block.getAvatarAttributeWithName(val); if (aa != null) { - if (aa.isInt() || aa.isNat()) { + if (aa.isInt()) { if (_aaos.isSending()) { result[1] = result[1] + ACTION_INT + nbOfInt + " = " + aa.getName(); } else { @@ -989,7 +989,7 @@ public class AVATAR2UPPAAL { val = _aaos.getValue(i); aa = _block.getAvatarAttributeWithName(val); if (aa != null) { - if (aa.isInt() || aa.isNat()) { + if (aa.isInt()) { if (_aaos.isSending()) { result[1] = result[1] + ACTION_INT + nbOfInt + " = " + aa.getName(); } else { diff --git a/src/translator/touppaal/TURTLE2UPPAAL.java b/src/translator/touppaal/TURTLE2UPPAAL.java index b8a75a17736ea859578382d96d0847be36f350dd..d0aa8b93ad7b3005c18c21db242e9a1a61a13304 100755 --- a/src/translator/touppaal/TURTLE2UPPAAL.java +++ b/src/translator/touppaal/TURTLE2UPPAAL.java @@ -1098,7 +1098,8 @@ public class TURTLE2UPPAAL { guadelay = "(" + gua + ") && (" + guadelay + ")"; } - tmp = "((choice__" + i + " >0) && ( h__<= choice__" + i + ")) || (choice__" + i + "==0)"; + //tmp = "((choice__" + i + " >0) && ( h__<= choice__" + i + ")) || (choice__" + i + "==0)"; + tmp = "((choice__" + i + " >0) && ( h__<= choice__" + i + "))"; if (inv.length() ==0) { inv = tmp; } else { diff --git a/src/ui/AvatarDesignPanelTranslator.java b/src/ui/AvatarDesignPanelTranslator.java index fafcc7f0281cb32471bf8c08b06209937832a0d4..990575267f118d2a1d3a80c67b671f819919cbc8 100644 --- a/src/ui/AvatarDesignPanelTranslator.java +++ b/src/ui/AvatarDesignPanelTranslator.java @@ -102,9 +102,11 @@ public class AvatarDesignPanelTranslator { if (_a.getType() == TAttribute.INTEGER){ type = AvatarType.INTEGER; } else if (_a.getType() == TAttribute.NATURAL){ - type = AvatarType.NATURAL; + type = AvatarType.INTEGER; } else if (_a.getType() == TAttribute.BOOLEAN) { type = AvatarType.BOOLEAN; + } else if (_a.getType() == TAttribute.TIMER) { + type = AvatarType.TIMER; } AvatarAttribute aa = new AvatarAttribute(_preName + _a.getId(), type, _a); aa.setInitialValue(_a.getInitialValue()); @@ -139,6 +141,8 @@ public class AvatarDesignPanelTranslator { addRegularAttribute(ab, a, ""); } else if (a.getType() == TAttribute.BOOLEAN) { addRegularAttribute(ab, a, ""); + } else if (a.getType() == TAttribute.TIMER) { + addRegularAttribute(ab, a, ""); } else { // other //TraceManager.addDev(" -> Other type found: " + a.getTypeOther()); @@ -220,9 +224,11 @@ public class AvatarDesignPanelTranslator { if (ta.getType() == TAttribute.INTEGER){ type = AvatarType.INTEGER; } else if (ta.getType() == TAttribute.NATURAL){ - type = AvatarType.NATURAL; + type = AvatarType.INTEGER; } else if (ta.getType() == TAttribute.BOOLEAN) { type = AvatarType.BOOLEAN; + } else if (ta.getType() == TAttribute.TIMER) { + type = AvatarType.TIMER; } aa = new AvatarAttribute(typeIds[i] + "__" + ta.getId(), type, _uiam); _atam.addParameter(aa); @@ -726,32 +732,39 @@ public class AvatarDesignPanelTranslator { block1 = port.getAvatarBDBlock1(); block2 = port.getAvatarBDBlock2(); + TraceManager.addDev("Searching block with name " + block1.getBlockName()); b1 = _as.getBlockWithName(block1.getBlockName()); b2 = _as.getBlockWithName(block2.getBlockName()); - r = new AvatarRelation("relation", b1, b2, tgc); - // Signals of l1 - l1 = port.getListOfSignalsOrigin(); - l2 = port.getListOfSignalsDestination(); + if ((b1 != null) && (b2 != null)) { - for(i=0; i<l1.size(); i++) { - name1 = AvatarSignal.getSignalNameFromFullSignalString(l1.get(i)); - name2 = AvatarSignal.getSignalNameFromFullSignalString(l2.get(i)); - atas1 = b1.getAvatarSignalWithName(name1); - atas2 = b2.getAvatarSignalWithName(name2); - if ((atas1 != null) && (atas2 != null)) { - r.addSignals(atas1, atas2); - } else { - TraceManager.addDev("null gates in AVATAR relation: " + name1 + " " + name2); + r = new AvatarRelation("relation", b1, b2, tgc); + // Signals of l1 + l1 = port.getListOfSignalsOrigin(); + l2 = port.getListOfSignalsDestination(); + + for(i=0; i<l1.size(); i++) { + name1 = AvatarSignal.getSignalNameFromFullSignalString(l1.get(i)); + name2 = AvatarSignal.getSignalNameFromFullSignalString(l2.get(i)); + TraceManager.addDev("Searching signal with name " + name1 + " in block " + b1.getName()); + atas1 = b1.getAvatarSignalWithName(name1); + atas2 = b2.getAvatarSignalWithName(name2); + if ((atas1 != null) && (atas2 != null)) { + r.addSignals(atas1, atas2); + } else { + TraceManager.addDev("null gates in AVATAR relation: " + name1 + " " + name2); + } } + + // Attribute of the relation + r.setBlocking(port.isBlocking()); + r.setAsynchronous(port.isAsynchronous()); + r.setSizeOfFIFO(port.getSizeOfFIFO()); + + _as.addRelation(r); + } else { + TraceManager.addDev("Null block b1=" + b1 + " b2=" + b2); } - - // Attribute of the relation - r.setBlocking(port.isBlocking()); - r.setAsynchronous(port.isAsynchronous()); - r.setSizeOfFIFO(port.getSizeOfFIFO()); - - _as.addRelation(r); } } } diff --git a/src/ui/TAttribute.java b/src/ui/TAttribute.java index e13eadc3bdbe4e4740391b3cbd3323e3729624cf..88487fb134147c281af9d73e67623205ffa19098 100755 --- a/src/ui/TAttribute.java +++ b/src/ui/TAttribute.java @@ -69,6 +69,7 @@ public class TAttribute { public final static int QUEUE_NAT = 6; public final static int ARRAY_NAT = 7; public final static int INTEGER = 8; + public final static int TIMER = 9; private int access; @@ -200,6 +201,10 @@ public class TAttribute { return true; } return false; + case INTEGER: + return value.matches("\\d*"); + case TIMER: + return ((value == null) ||(value.equals(""))); default: return false; } @@ -248,8 +253,10 @@ public class TAttribute { return QUEUE_NAT; } else if (s.equals("Array_nat")) { return ARRAY_NAT; - } else if (s.equals("int")) { - return ARRAY_NAT; + } else if (s.equals("Integer")) { + return INTEGER; + } else if (s.equals("Timer")) { + return TIMER; } else if (!s.equals("")) { return OTHER; } @@ -291,7 +298,9 @@ public class TAttribute { case ARRAY_NAT: return "Array_nat"; case INTEGER: - return "int"; + return "Integer"; + case TIMER: + return "Timer"; default: return ""; } diff --git a/src/ui/avatarbd/AvatarBDBlock.java b/src/ui/avatarbd/AvatarBDBlock.java index d983d2ab99daec4e046ac1203ed25b653fff10c1..01e210149584b2072335066a0d062ef49c69342a 100644 --- a/src/ui/avatarbd/AvatarBDBlock.java +++ b/src/ui/avatarbd/AvatarBDBlock.java @@ -498,9 +498,10 @@ public class AvatarBDBlock extends TGCScalableWithInternalComponent implements S protected void setJDialogOptions(JDialogAvatarBlock _jdab) { //jda.addAccess(TAttribute.getStringAccess(TAttribute.PUBLIC)); _jdab.addAccess(TAttribute.getStringAccess(TAttribute.PRIVATE)); - _jdab.addType(TAttribute.getStringType(TAttribute.NATURAL), true); + //_jdab.addType(TAttribute.getStringType(TAttribute.NATURAL), true); _jdab.addType(TAttribute.getStringType(TAttribute.BOOLEAN), true); _jdab.addType(TAttribute.getStringType(TAttribute.INTEGER), true); + _jdab.addType(TAttribute.getStringType(TAttribute.TIMER), false); for(String s: tdp.getAllDataTypes()) { _jdab.addType(s, false); @@ -683,7 +684,7 @@ public class AvatarBDBlock extends TGCScalableWithInternalComponent implements S valueAtt = ""; } if ((TAttribute.isAValidId(id, false, false)) && (TAttribute.isAValidInitialValue(type, valueAtt))) { - //System.out.println("Adding attribute " + id + " typeOther=" + typeOther); + System.out.println("Adding attribute " + id + " typeOther=" + typeOther); TAttribute ta = new TAttribute(access, id, valueAtt, type, typeOther); myAttributes.addElement(ta); }