diff --git a/src/tmltranslator/touppaal/TML2UPPAAL.java b/src/tmltranslator/touppaal/TML2UPPAAL.java index 9cabe9b50c2e66bb9587286485191d237b2d3778..bf6289ea8d0737c5c3768dbf4641bde2efac007b 100755 --- a/src/tmltranslator/touppaal/TML2UPPAAL.java +++ b/src/tmltranslator/touppaal/TML2UPPAAL.java @@ -169,6 +169,7 @@ public class TML2UPPAAL { spec.addTemplate(new UPPAALFiniteFIFOTemplateLoss("channel__" + ch.getName(), ch.getName(), ch.getMax(), ch.getMaxNbOfLoss())); } else { spec.addTemplate(new UPPAALFiniteFIFOTemplate("channel__" + ch.getName(), ch.getName(), ch.getMax())); + makeLoss("ch__" + ch.getName()); } } else if (ch.getType() == TMLChannel.BRNBW) { spec.addGlobalDeclaration("urgent chan rd__" + ch.getName() + ", wr__" + ch.getName() + ";\n"); diff --git a/src/uppaaldesc/UPPAALFiniteFIFOTemplateLoss.java b/src/uppaaldesc/UPPAALFiniteFIFOTemplateLoss.java index 054087d791454b9c3d45ca7e8a710b739e45a8f5..876c5c370216b7614c4aacd7093a70dd2f304a5e 100755 --- a/src/uppaaldesc/UPPAALFiniteFIFOTemplateLoss.java +++ b/src/uppaaldesc/UPPAALFiniteFIFOTemplateLoss.java @@ -117,10 +117,11 @@ public class UPPAALFiniteFIFOTemplateLoss extends UPPAALTemplate { tr = new UPPAALTransition(); tr.sourceLoc = lossLocation; tr.destinationLoc = lossOccuredLocation; - //tr.synchronization = "evt__" + event.getName() + "__loss!"; + tr.synchronization = "ch__" + chname + "__loss!"; if (maxNbOfLoss > -1) { tr.guard = " nbOfLoss__ < " + maxNbOfLoss; } + tr.assignment = "nbOfLoss__ = nbOfLoss__ + 1"; tr.points.add(new Point(-56, -176)); transitions.add(tr); @@ -136,6 +137,7 @@ public class UPPAALFiniteFIFOTemplateLoss extends UPPAALTemplate { tr.sourceLoc = lossLocation; tr.destinationLoc = initLocation; tr.assignment = "buffer = buffer + 1"; + tr.synchronization = "ch__" + chname + "__noloss!"; tr.assignmentPoint = new Point(-304, -64); tr.points.add(new Point(-16, -200)); transitions.add(tr);