diff --git a/src/tmltranslator/tomappingsystemc2/TML2MappingSystemC.java b/src/tmltranslator/tomappingsystemc2/TML2MappingSystemC.java
index 21b53f0148dc2b12efc5b804166d4b42838da86d..b9906ae41b56675e9e26b232d84326d833c17d17 100755
--- a/src/tmltranslator/tomappingsystemc2/TML2MappingSystemC.java
+++ b/src/tmltranslator/tomappingsystemc2/TML2MappingSystemC.java
@@ -189,8 +189,9 @@ public class TML2MappingSystemC {
//tmlmapping.getTMLArchitecture().getMasterClockFrequency() * exNode.sliceTime
//declaration += "RRScheduler* " + exNode.getName() + "_scheduler = new RRScheduler(\"" + exNode.getName() + "_RRSched\", 0, 5, " + (int) Math.ceil(((float)exNode.execiTime)*(1+((float)exNode.branchingPredictionPenalty)/100)) + " ) " + SCCR;
declaration += "RRScheduler* " + exNode.getName() + "_scheduler = new RRScheduler(\"" + exNode.getName() + "_RRSched\", 0, " + (tmlmapping.getTMLArchitecture().getMasterClockFrequency() * exNode.sliceTime) + ", " + (int) Math.ceil((float)(exNode.clockRatio * Math.max(exNode.execiTime,exNode.execcTime) * (exNode.branchingPredictionPenalty * exNode.pipelineSize +100 - exNode.branchingPredictionPenalty))/100) + " ) " + SCCR;
- //for(int cores=0; cores<exNode.nbOfCores; cores++){
- for(int cores=0; cores<1; cores++){
+ System.out.println("cores " + exNode.nbOfCores);
+ for(int cores=0; cores<exNode.nbOfCores; cores++){
+ //for(int cores=0; cores<1; cores++){
//if (tmlmapping.isAUsedHwNode(node)) {
declaration += "CPU* " + exNode.getName() + cores + " = new SingleCoreCPU(" + exNode.getID() + ", \"" + exNode.getName() + "_" + cores + "\", " + exNode.getName() + "_scheduler" + ", ";
@@ -266,8 +267,8 @@ public class TML2MappingSystemC {
for(HwLink link: nodeLinks){
//declaration+= "BusMaster* " + node.getName() + "_" + link.bus.getName() + "_Master = new BusMaster(\"" + node.getName() + "_" + link.bus.getName() + "_Master\", " + link.getPriority() + ", 1, array(1, (SchedulableCommDevice*)" + link.bus.getName() + "))" + SCCR;
int noOfCores;
- //if (node instanceof HwCPU) noOfCores= ((HwCPU)node).nbOfCores; else noOfCores=1;
- noOfCores=1;
+ if (node instanceof HwCPU) noOfCores= ((HwCPU)node).nbOfCores; else noOfCores=1;
+ //noOfCores=2;
for (int cores=0; cores<noOfCores; cores++){
String nodeName=node.getName();
if ((node instanceof HwCPU) || (node instanceof HwA) )
@@ -380,8 +381,8 @@ public class TML2MappingSystemC {
for(HwLink link: busLinks){
if (link.hwnode instanceof HwExecutionNode || link.hwnode instanceof HwBridge){
if ((link.hwnode instanceof HwCPU) || (link.hwnode instanceof HwA)){
- //for (int cores=0; cores< ((HwCPU)link.hwnode).nbOfCores; cores++){
- for (int cores=0; cores< 1; cores++){
+ for (int cores=0; cores< ((HwCPU)link.hwnode).nbOfCores; cores++){
+ //for (int cores=0; cores< 1; cores++){
devices += ", (WorkloadSource*)" + link.hwnode.getName()+ cores + "_" + node.getName() + "_Master";
numDevices++;
}
@@ -422,23 +423,23 @@ public class TML2MappingSystemC {
declaration += task.getName() + "* task__" + task.getName() + " = new " + task.getName() + "("+ task.getID() +","+ task.getPriority() + ",\"" + task.getName() + "\", array(";
if (node instanceof HwCPU){
- //declaration+= ((HwCPU)node).nbOfCores;
- declaration+= 1;
- //for (int cores=0; cores< ((HwCPU)node).nbOfCores; cores++){
- for (int cores=0; cores< 1; cores++){
+ declaration+= ((HwCPU)node).nbOfCores;
+ //declaration+= 1;
+ for (int cores=0; cores< ((HwCPU)node).nbOfCores; cores++){
+ //for (int cores=0; cores< 1; cores++){
declaration+= "," + node.getName()+cores;
}
//declaration+= ")," + ((HwCPU)node).nbOfCores + CR;
declaration+= "),1" + CR;
}else if (node instanceof HwA){
- //declaration+= ((HwCPU)node).nbOfCores;
- declaration+= 1;
- //for (int cores=0; cores< ((HwCPU)node).nbOfCores; cores++){
- for (int cores=0; cores< 1; cores++){
+ declaration+= ((HwCPU)node).nbOfCores;
+ //declaration+= 1;
+ for (int cores=0; cores< ((HwCPU)node).nbOfCores; cores++){
+ //for (int cores=0; cores< 1; cores++){
declaration+= "," + node.getName()+cores;
}
- //declaration+= ")," + ((HwCPU)node).nbOfCores + CR;
- declaration+= "),1" + CR;
+ declaration+= ")," + ((HwCPU)node).nbOfCores + CR;
+ //declaration+= "),1" + CR;
} else {
declaration += "1," + node.getName() + "),1" + CR;
}
diff --git a/src/ui/AvatarDesignPanel.java b/src/ui/AvatarDesignPanel.java
index b81d17a04a48ea93d8414112f58c0b13e183379a..19517985967f3a7743e34cec596aab544ec2ed63 100644
--- a/src/ui/AvatarDesignPanel.java
+++ b/src/ui/AvatarDesignPanel.java
@@ -331,6 +331,17 @@ public class AvatarDesignPanel extends TURTLEPanel {
}
}
}
+
+
+ public void modelBacktracingUppaal(HashMap verifMap){
+ for (Object ob: abdp.getComponentList()) {
+ if (ob instanceof AvatarBDSafetyPragma) {
+ AvatarBDSafetyPragma pragma = (AvatarBDSafetyPragma) ob;
+ pragma.verifMap = verifMap;
+ }
+ }
+ }
+
public void modelBacktracingProVerif(ProVerifOutputAnalyzer pvoa) {
diff --git a/src/ui/MainGUI.java b/src/ui/MainGUI.java
index 700f7395d537878fcfe94642161c95cff99f833d..335290fa97110d827511d76296f9e7ea0c2837e2 100755
--- a/src/ui/MainGUI.java
+++ b/src/ui/MainGUI.java
@@ -3715,6 +3715,21 @@ public class MainGUI implements ActionListener, WindowListener, KeyListener, Pe
getCurrentTDiagramPanel().repaint();
}
+ public void modelBacktracingUPPAAL(HashMap<String, Integer> verifMap) {
+ TURTLEPanel tp = getCurrentTURTLEPanel();
+ if (tp == null) {
+ return;
+ }
+
+ if (!(tp instanceof AvatarDesignPanel)) {
+ return;
+ }
+
+ AvatarDesignPanel adp = (AvatarDesignPanel)tp;
+ adp.modelBacktracingUppaal(verifMap);
+ getCurrentTDiagramPanel().repaint();
+ }
+
public void generateRTLOTOS() {
generateRTLOTOS(false);
}
diff --git a/src/ui/avatarbd/AvatarBDSafetyPragma.java b/src/ui/avatarbd/AvatarBDSafetyPragma.java
index b7417ed62e6e566a65988cfa246389c56838b98c..8d6099f078cfcfa7df0b26ade91cd8078ced3be2 100644
--- a/src/ui/avatarbd/AvatarBDSafetyPragma.java
+++ b/src/ui/avatarbd/AvatarBDSafetyPragma.java
@@ -76,8 +76,12 @@ public class AvatarBDSafetyPragma extends TGCScalableWithoutInternalComponent {
private Font myFont, myFontB;
private int maxFontSize = 30;
private int minFontSize = 4;
+ public final static int PROVED_TRUE = 1;
+ public final static int PROVED_FALSE = 0;
private int currentFontSize = -1;
private final String[] pPragma = {"A[]", "A<>", "E[]", "E<>"};
+ public HashMap<String, Integer> verifMap = new HashMap<String, Integer>();
+
protected Graphics graphics;
public AvatarBDSafetyPragma(int _x, int _y, int _minX, int _maxX, int _minY, int _maxY, boolean _pos, TGComponent _father, TDiagramPanel _tdp) {
super(_x, _y, _minX, _maxX, _minY, _maxY, _pos, _father, _tdp);
@@ -192,6 +196,7 @@ public class AvatarBDSafetyPragma extends TGCScalableWithoutInternalComponent {
g.setFont(fold);
for (String s: properties){
g.drawString(s, x + textX, y + textY + (i+1)* currentFontSize);
+ drawVerification(s, g, x+textX, y+textY + (i+1)* currentFontSize);
i++;
}
@@ -296,7 +301,33 @@ public class AvatarBDSafetyPragma extends TGCScalableWithoutInternalComponent {
sb.append("</extraparam>\n");
return new String(sb);
}
-
+ private void drawVerification(String s, Graphics g, int _x, int _y){
+ Color c = g.getColor();
+ Color c1;
+ int status;
+ if (verifMap.containsKey(s)){
+ status = verifMap.get(s);
+ if (status== PROVED_TRUE){
+ g.setColor(Color.green);
+ int[] xp1 = new int[]{_x-20, _x-18, _x-12, _x-14};
+ int[] yp1 = new int[]{_y-3, _y-5, _y-1, _y+1};
+ int[] xp2 = new int[]{_x-14, _x-12, _x-3, _x-5};
+ int[] yp2 = new int[]{_y-1, _y+1, _y-8, _y-10};
+ g.fillPolygon(xp1, yp1, 4);
+ g.fillPolygon(xp2, yp2, 4);
+ }
+ else {
+ g.setColor(Color.red);
+ int[] xp1 = new int[]{_x-17, _x-15, _x-6, _x-8};
+ int[] yp1 = new int[]{_y-8, _y-6, _y+2, _y+4};
+ int[] xp2 = new int[]{_x-15, _x-17, _x-8, _x-6};
+ int[] yp2 = new int[]{_y+4, _y+2, _y-8, _y-6};
+ g.fillPolygon(xp1, yp1, 4);
+ g.fillPolygon(xp2, yp2, 4);
+ }
+ }
+ g.setColor(c);
+ }
public void loadExtraParam(NodeList nl, int decX, int decY, int decId) throws MalformedModelingException{
value = "";
values = null;
diff --git a/src/ui/window/JDialogUPPAALValidation.java b/src/ui/window/JDialogUPPAALValidation.java
index f60509f35a77607911d99dcd784543985fa084f7..c942a4f3397954bdb53f0bc2d952788e89039754 100755
--- a/src/ui/window/JDialogUPPAALValidation.java
+++ b/src/ui/window/JDialogUPPAALValidation.java
@@ -92,8 +92,8 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti
protected LinkedList<JCheckBox> customChecks;
protected LinkedList<String> customQueries;
-
-
+ public HashMap<String, Integer> verifMap;
+ protected int status = -1;
/** Creates new form */
public JDialogUPPAALValidation(Frame f, MainGUI _mgui, String title, String _cmdVerifyta, String _pathTrace, String _fileName, String _spec, String _host, TURTLEPanel _tp) {
super(f, title, true);
@@ -115,6 +115,7 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti
customChecks = new LinkedList<JCheckBox>();
initComponents();
myInitComponents();
+ verifMap = new HashMap<String, Integer>();
pack();
//getGlassPane().addMouseListener( new MouseAdapter() {});
@@ -449,10 +450,13 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti
if (j.isSelected()){
jta.append(j.getText()+"\n");
String translation = translateCustomQuery(j.getText());
+ status = -1;
workQuery(translation, fn, trace_id, rshc);
+ verifMap.put(j.getText(), status);
trace_id++;
}
}
+ mgui.modelBacktracingUPPAAL(verifMap);
}
//Removing files
@@ -485,7 +489,7 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti
} catch (LauncherException le1) {}
return;
}
-
+
mode = NOT_STARTED;
setButtons();
}
@@ -562,9 +566,11 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti
}
else if (data.indexOf("Property is satisfied") >-1){
jta.append("-> property is satisfied\n");
+ status=1;
}
else if (data.indexOf("Property is NOT satisfied") > -1) {
jta.append("-> property is NOT satisfied\n");
+ status = 0;
}
else {
jta.append("ERROR -> property could not be studied\n");
@@ -578,6 +584,7 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti
if (generateTrace.isSelected()) {
generateTraceFile(fn, trace_id, rshc);
}
+
}
private void generateTraceFile(String fn, int trace_id, RshClient rshc) throws LauncherException{