From 7f58c0f7159dcce75d7bba8c60b72ac4e5148ddf Mon Sep 17 00:00:00 2001
From: Emna Gharbi <amna.gharbi@telecom-paristech.fr>
Date: Tue, 26 Feb 2019 15:59:51 +0100
Subject: [PATCH] fixing warnings

---
 .../dsez3engine/InputInstance.java            |   7 +-
 .../dsez3engine/OptimizationModel.java        | 127 +++++++++++-------
 2 files changed, 80 insertions(+), 54 deletions(-)

diff --git a/src/main/java/tmltranslator/dsez3engine/InputInstance.java b/src/main/java/tmltranslator/dsez3engine/InputInstance.java
index 20c3fe12a1..d9e5183d5b 100644
--- a/src/main/java/tmltranslator/dsez3engine/InputInstance.java
+++ b/src/main/java/tmltranslator/dsez3engine/InputInstance.java
@@ -103,9 +103,10 @@ public class InputInstance {
 
     public TMLTask getFinalTask(TMLModeling tmlm){
         TMLTask finalTask = null;
-        for (TMLTask tmlTask : (List<TMLTask>) tmlm.getTasks()){
-            if (tmlTask.getWriteTMLChannels().isEmpty())
-                finalTask = tmlTask;
+        for (Object tmlTask :  tmlm.getTasks()){
+            TMLTask taskCast = (TMLTask)tmlTask;
+            if (taskCast.getWriteTMLChannels().isEmpty())
+                finalTask = taskCast;
         }
 
         return finalTask;
diff --git a/src/main/java/tmltranslator/dsez3engine/OptimizationModel.java b/src/main/java/tmltranslator/dsez3engine/OptimizationModel.java
index d76b88c7b9..cb99bb9666 100644
--- a/src/main/java/tmltranslator/dsez3engine/OptimizationModel.java
+++ b/src/main/java/tmltranslator/dsez3engine/OptimizationModel.java
@@ -2,10 +2,11 @@ package tmltranslator.dsez3engine;
 
 import com.microsoft.z3.*;
 import myutil.TraceManager;
-import sun.util.PreHashedMap;
 import tmltranslator.*;
 
 import javax.swing.*;
+import java.lang.reflect.Array;
+import java.util.ArrayList;
 import java.util.List;
 import java.util.Map;
 import java.util.HashMap;
@@ -65,15 +66,16 @@ public class OptimizationModel {
 
         //TraceManager.addDev("\nDefining the bounds of Xtp (1)");
 
-        for (TMLTask tmlTask : (List<TMLTask>) inputInstance.getModeling().getTasks()) {
+        for (Object tmlTask : inputInstance.getModeling().getTasks()) {
 
             int t = inputInstance.getModeling().getTasks().indexOf(tmlTask);
+            TMLTask taskCast = (TMLTask)tmlTask;
 
             for (HwNode hwNode : inputInstance.getArchitecture().getCPUs()) {
 
                 int p = inputInstance.getArchitecture().getCPUs().indexOf(hwNode);
 
-                X[t][p] = ctx.mkIntConst("X_" + tmlTask.getID() + "_" + hwNode.getID());
+                X[t][p] = ctx.mkIntConst("X_" + taskCast.getID() + "_" + hwNode.getID());
 
                 // Constraints: 0 <= Xtp <= 1
                 c_bound_x[t][p] = ctx.mkAnd(ctx.mkLe(ctx.mkInt(0), X[t][p]),
@@ -86,10 +88,11 @@ public class OptimizationModel {
         //Constraint on start >=0
         BoolExpr[] c_bound_start = new BoolExpr[inputInstance.getModeling().getTasks().size()];
 
-        for (TMLTask tmlTask : (List<TMLTask>) inputInstance.getModeling().getTasks()) {
+        for (Object tmlTask :  inputInstance.getModeling().getTasks()) {
             int t = inputInstance.getModeling().getTasks().indexOf(tmlTask);
+            TMLTask taskCast = (TMLTask)tmlTask;
 
-            start[t] = ctx.mkIntConst("start_" + tmlTask.getID());
+            start[t] = ctx.mkIntConst("start_" + taskCast.getID());
             c_bound_start[t] = ctx.mkGe(start[t], ctx.mkInt(0));
             mapping_constraints = ctx.mkAnd(mapping_constraints, c_bound_start[t]);
         }
@@ -103,8 +106,8 @@ public class OptimizationModel {
 
         //TraceManager.addDev("\nUnique task-CPU mapping constraints (3)");
         BoolExpr[] c_unique_x = new BoolExpr[inputInstance.getModeling().getTasks().size()];
-        for (TMLTask tmlTask : (List<TMLTask>) inputInstance.getModeling().getTasks()) {
-            int t = inputInstance.getModeling().getTasks().indexOf(tmlTask); // TODO or use the local instance modeling
+        for (Object tmlTask :  inputInstance.getModeling().getTasks()) {
+            int t = inputInstance.getModeling().getTasks().indexOf(tmlTask);
 
             ArithExpr sum_X = ctx.mkAdd(X[t]);
             c_unique_x[t] = ctx.mkLe(sum_X, ctx.mkInt(1));
@@ -116,11 +119,12 @@ public class OptimizationModel {
         //Feasible Task map: ∀t, SUM p in F(t) (X tp) = 1
         //TraceManager.addDev("\nFeasible task-CPU mapping constraints (4)");
         BoolExpr[] c_feasibleMapX = new BoolExpr[inputInstance.getModeling().getTasks().size()];
-        for (TMLTask tmlTask : (List<TMLTask>) inputInstance.getModeling().getTasks()) {
+        for (Object tmlTask :  inputInstance.getModeling().getTasks()) {
             int t = inputInstance.getModeling().getTasks().indexOf(tmlTask);
+            TMLTask taskCast = (TMLTask)tmlTask;
             ArithExpr sum_X = ctx.mkInt(0);
 
-            for (HwNode hwNode : inputInstance.getFeasibleCPUs(tmlTask)) {
+            for (HwNode hwNode : inputInstance.getFeasibleCPUs(taskCast)) {
 
                 int p = inputInstance.getArchitecture().getCPUs().indexOf(hwNode);
 
@@ -143,10 +147,11 @@ public class OptimizationModel {
             IntExpr mem = ctx.mkInt(inputInstance.getLocalMemoryOfHwExecutionNode(hwNode).memorySize);
 
 
-            for (TMLTask tmlTask : (List<TMLTask>) inputInstance.getModeling().getTasks()) {
+            for (Object tmlTask :  inputInstance.getModeling().getTasks()) {
                 int t = inputInstance.getModeling().getTasks().indexOf(tmlTask);
+                TMLTask taskCast = (TMLTask)tmlTask;
 
-                IntExpr bin_plus_bout = ctx.mkInt(inputInstance.getBufferIn(tmlTask) + inputInstance.getBufferOut(tmlTask));
+                IntExpr bin_plus_bout = ctx.mkInt(inputInstance.getBufferIn(taskCast) + inputInstance.getBufferOut(taskCast));
                 ArithExpr bin_plus_bout_times_X = ctx.mkMul(bin_plus_bout, X[t][p]);
 
                 c_mem[p][t] = ctx.mkLe(bin_plus_bout_times_X, mem);
@@ -197,14 +202,16 @@ public class OptimizationModel {
         // TraceManager.addDev("\nPrecedence constraints (11)");
         BoolExpr[] c_precedence = new BoolExpr[inputInstance.getModeling().getChannels().size()];
 
-        for (TMLChannel channel : (List<TMLChannel>) inputInstance.getModeling().getChannels()) {
+        for (Object channel : inputInstance.getModeling().getChannels()) {
 
             int c = inputInstance.getModeling().getChannels().indexOf(channel);
+            TMLChannel channelCast = (TMLChannel) channel;
+
             //for each channel get producer and consumer
-            TMLTask producer = channel.getOriginTask();
+            TMLTask producer = channelCast.getOriginTask();
             int prodIndex = inputInstance.getModeling().getTasks().indexOf(producer);
 
-            TMLTask consumer = channel.getDestinationTask();
+            TMLTask consumer = channelCast.getDestinationTask();
             int consIndex = inputInstance.getModeling().getTasks().indexOf(consumer);
 
             ArithExpr wcetProducer = ctx.mkInt(0);
@@ -236,24 +243,26 @@ public class OptimizationModel {
         for (HwNode hwNode : inputInstance.getArchitecture().getCPUs()) {
             int p = inputInstance.getArchitecture().getCPUs().indexOf(hwNode);
 
-            for (TMLTask taski : (List<TMLTask>) inputInstance.getModeling().getTasks()) {
+            for (Object taski :  inputInstance.getModeling().getTasks()) {
 
                 int ti = inputInstance.getModeling().getTasks().indexOf(taski);
+                TMLTask taskiCast = (TMLTask)taski;
                 //Calculate End times of ti
                 ArithExpr wceti = ctx.mkInt(0);
 
-                for (HwExecutionNode ihwNode : inputInstance.getFeasibleCPUs(taski)) {
+                for (HwExecutionNode ihwNode : inputInstance.getFeasibleCPUs(taskiCast)) {
                     int ip = inputInstance.getArchitecture().getCPUs().indexOf(ihwNode);
 
-                    wceti = ctx.mkAdd(wceti, ctx.mkMul(X[ti][ip], ctx.mkInt(inputInstance.getWCET(taski, ihwNode))));
+                    wceti = ctx.mkAdd(wceti, ctx.mkMul(X[ti][ip], ctx.mkInt(inputInstance.getWCET(taskiCast, ihwNode))));
 
                 }
 
                 ArithExpr endti = ctx.mkAdd(start[ti], wceti);
 
-                for (TMLTask taskj : (List<TMLTask>) inputInstance.getModeling().getTasks()) {
+                for (Object taskj : inputInstance.getModeling().getTasks()) {
 
                     int tj = inputInstance.getModeling().getTasks().indexOf(taskj);
+                    TMLTask taskjCast = (TMLTask)taskj;
 
 
                     if (tj != ti) {
@@ -261,10 +270,10 @@ public class OptimizationModel {
 
                         ArithExpr wcetj = ctx.mkInt(0);
 
-                        for (HwExecutionNode jhwNode : inputInstance.getFeasibleCPUs(taskj)) {
+                        for (HwExecutionNode jhwNode : inputInstance.getFeasibleCPUs(taskjCast)) {
                             int jp = inputInstance.getArchitecture().getCPUs().indexOf(jhwNode);
 
-                            wcetj = ctx.mkAdd(wcetj, ctx.mkMul(X[tj][jp], ctx.mkInt(inputInstance.getWCET(taskj, jhwNode))));
+                            wcetj = ctx.mkAdd(wcetj, ctx.mkMul(X[tj][jp], ctx.mkInt(inputInstance.getWCET(taskjCast, jhwNode))));
 
 
                         }
@@ -293,9 +302,10 @@ public class OptimizationModel {
         //Grouping remaining constraints of the model
 
         // TraceManager.addDev("\nAll mapping constraints");
-        for (TMLTask task : (List<TMLTask>) inputInstance.getModeling().getTasks()) {
+        for (Object task :  inputInstance.getModeling().getTasks()) {
 
             int t = inputInstance.getModeling().getTasks().indexOf(task);
+            TMLTask taskCast = (TMLTask)task;
 
             for (HwNode hwNode : inputInstance.getArchitecture().getCPUs()) {
                 int p = inputInstance.getArchitecture().getCPUs().indexOf(hwNode);
@@ -324,26 +334,27 @@ public class OptimizationModel {
             TraceManager.addDev("Proposed feasible Mapping solution:");
 
 
-            for (TMLTask task : (List<TMLTask>) inputInstance.getModeling().getTasks()) {
+            for (Object task : inputInstance.getModeling().getTasks()) {
                 int t = inputInstance.getModeling().getTasks().indexOf(task);
+                TMLTask taskCast = (TMLTask)task;
 
                 for (HwNode hwNode : inputInstance.getArchitecture().getCPUs()) {
                     int p = inputInstance.getArchitecture().getCPUs().indexOf(hwNode);
 
 
                     optimized_result_X[t][p] = m.evaluate(X[t][p], false);
-                    TraceManager.addDev("X[" + task.getName() + "][" + hwNode.getName() + "] = " + optimized_result_X[t][p]);
+                    TraceManager.addDev("X[" + taskCast.getName() + "][" + hwNode.getName() + "] = " + optimized_result_X[t][p]);
 
                 }
 
                 TraceManager.addDev("\n");
             }
 
-            for (TMLTask task : (List<TMLTask>) inputInstance.getModeling().getTasks()) {
+            for (Object task : inputInstance.getModeling().getTasks()) {
                 int t = inputInstance.getModeling().getTasks().indexOf(task);
-
+                TMLTask taskCast = (TMLTask)task;
                 optimized_result_start[t] = m.evaluate(start[t], false);
-                TraceManager.addDev("start[" + task.getName() + "] = " + optimized_result_start[t]);
+                TraceManager.addDev("start[" + taskCast.getName() + "] = " + optimized_result_start[t]);
 
             }
 
@@ -379,15 +390,16 @@ public class OptimizationModel {
 
         //TraceManager.addDev("\nDefining the bounds of Xtp (1)");
 
-        for (TMLTask tmlTask : (List<TMLTask>) inputInstance.getModeling().getTasks()) {
+        for (Object tmlTask :  inputInstance.getModeling().getTasks()) {
 
             int t = inputInstance.getModeling().getTasks().indexOf(tmlTask);
+            TMLTask taskCast = (TMLTask)tmlTask;
 
             for (HwNode hwNode : inputInstance.getArchitecture().getCPUs()) {
 
                 int p = inputInstance.getArchitecture().getCPUs().indexOf(hwNode);
 
-                X[t][p] = ctx.mkIntConst("X_" + tmlTask.getID() + "_" + hwNode.getID());
+                X[t][p] = ctx.mkIntConst("X_" + taskCast.getID() + "_" + hwNode.getID());
 
                 // Constraints: 0 <= Xtp <= 1
                 c_bound_x[t][p] = ctx.mkAnd(ctx.mkLe(ctx.mkInt(0), X[t][p]),
@@ -400,10 +412,11 @@ public class OptimizationModel {
         //Constraint on start >=0
         BoolExpr[] c_bound_start = new BoolExpr[inputInstance.getModeling().getTasks().size()];
 
-        for (TMLTask tmlTask : (List<TMLTask>) inputInstance.getModeling().getTasks()) {
+        for (Object tmlTask :  inputInstance.getModeling().getTasks()) {
             int t = inputInstance.getModeling().getTasks().indexOf(tmlTask);
 
-            start[t] = ctx.mkIntConst("start_" + tmlTask.getID());
+            TMLTask taskCast = (TMLTask)tmlTask;
+            start[t] = ctx.mkIntConst("start_" + taskCast.getID());
             c_bound_start[t] = ctx.mkGe(start[t], ctx.mkInt(0));
             mapping_constraints = ctx.mkAnd(mapping_constraints, c_bound_start[t]);
         }
@@ -416,7 +429,7 @@ public class OptimizationModel {
 
         //TraceManager.addDev("\nUnique task-CPU mapping constraints (3)");
         BoolExpr[] c_unique_x = new BoolExpr[inputInstance.getModeling().getTasks().size()];
-        for (TMLTask tmlTask : (List<TMLTask>) inputInstance.getModeling().getTasks()) {
+        for (Object tmlTask :  inputInstance.getModeling().getTasks()) {
             int t = inputInstance.getModeling().getTasks().indexOf(tmlTask); // TODO or use the local instance modeling
 
             ArithExpr sum_X = ctx.mkAdd(X[t]);
@@ -429,11 +442,13 @@ public class OptimizationModel {
         //Feasible Task map: ∀t, SUM p in F(t) (X tp) = 1
         //TraceManager.addDev("\nFeasible task-CPU mapping constraints (4)");
         BoolExpr[] c_feasibleMapX = new BoolExpr[inputInstance.getModeling().getTasks().size()];
-        for (TMLTask tmlTask : (List<TMLTask>) inputInstance.getModeling().getTasks()) {
+        for (Object tmlTask :  inputInstance.getModeling().getTasks()) {
             int t = inputInstance.getModeling().getTasks().indexOf(tmlTask);
             ArithExpr sum_X = ctx.mkInt(0);
 
-            for (HwNode hwNode : inputInstance.getFeasibleCPUs(tmlTask)) {
+            TMLTask taskCast = (TMLTask)tmlTask;
+
+            for (HwNode hwNode : inputInstance.getFeasibleCPUs(taskCast)) {
 
                 int p = inputInstance.getArchitecture().getCPUs().indexOf(hwNode);
 
@@ -456,10 +471,12 @@ public class OptimizationModel {
             IntExpr mem = ctx.mkInt(inputInstance.getLocalMemoryOfHwExecutionNode(hwNode).memorySize);
 
 
-            for (TMLTask tmlTask : (List<TMLTask>) inputInstance.getModeling().getTasks()) {
+            for (Object tmlTask : inputInstance.getModeling().getTasks()) {
                 int t = inputInstance.getModeling().getTasks().indexOf(tmlTask);
 
-                IntExpr bin_plus_bout = ctx.mkInt(inputInstance.getBufferIn(tmlTask) + inputInstance.getBufferOut(tmlTask));
+                TMLTask taskCast = (TMLTask)tmlTask;
+
+                IntExpr bin_plus_bout = ctx.mkInt(inputInstance.getBufferIn(taskCast) + inputInstance.getBufferOut(taskCast));
                 ArithExpr bin_plus_bout_times_X = ctx.mkMul(bin_plus_bout, X[t][p]);
 
                 c_mem[p][t] = ctx.mkLe(bin_plus_bout_times_X, mem);
@@ -510,14 +527,15 @@ public class OptimizationModel {
         // TraceManager.addDev("\nPrecedence constraints (11)");
         BoolExpr[] c_precedence = new BoolExpr[inputInstance.getModeling().getChannels().size()];
 
-        for (TMLChannel channel : (List<TMLChannel>) inputInstance.getModeling().getChannels()) {
+        for (Object channel :  inputInstance.getModeling().getChannels()) {
 
             int c = inputInstance.getModeling().getChannels().indexOf(channel);
             //for each channel get producer and consumer
-            TMLTask producer = channel.getOriginTask();
+            TMLChannel channelCast = (TMLChannel)channel;
+            TMLTask producer = channelCast.getOriginTask();
             int prodIndex = inputInstance.getModeling().getTasks().indexOf(producer);
 
-            TMLTask consumer = channel.getDestinationTask();
+            TMLTask consumer = channelCast.getDestinationTask();
             int consIndex = inputInstance.getModeling().getTasks().indexOf(consumer);
 
             //TraceManager.addDev("\nChannel(" + producer.getId() + "," + consumer.getId() + ")");
@@ -551,22 +569,24 @@ public class OptimizationModel {
         for (HwNode hwNode : inputInstance.getArchitecture().getCPUs()) {
             int p = inputInstance.getArchitecture().getCPUs().indexOf(hwNode);
 
-            for (TMLTask taski : (List<TMLTask>) inputInstance.getModeling().getTasks()) {
+            for (Object taski :  inputInstance.getModeling().getTasks()) {
 
                 int ti = inputInstance.getModeling().getTasks().indexOf(taski);
                 //Calculate End times of ti
                 ArithExpr wceti = ctx.mkInt(0);
 
-                for (HwExecutionNode ihwNode : inputInstance.getFeasibleCPUs(taski)) {
+                TMLTask taskiCast = (TMLTask)taski;
+
+                for (HwExecutionNode ihwNode : inputInstance.getFeasibleCPUs(taskiCast)) {
                     int ip = inputInstance.getArchitecture().getCPUs().indexOf(ihwNode);
 
-                    wceti = ctx.mkAdd(wceti, ctx.mkMul(X[ti][ip], ctx.mkInt(inputInstance.getWCET(taski, ihwNode))));
+                    wceti = ctx.mkAdd(wceti, ctx.mkMul(X[ti][ip], ctx.mkInt(inputInstance.getWCET(taskiCast, ihwNode))));
 
                 }
 
                 ArithExpr endti = ctx.mkAdd(start[ti], wceti);
 
-                for (TMLTask taskj : (List<TMLTask>) inputInstance.getModeling().getTasks()) {
+                for (Object taskj :  inputInstance.getModeling().getTasks()) {
 
                     int tj = inputInstance.getModeling().getTasks().indexOf(taskj);
 
@@ -576,10 +596,13 @@ public class OptimizationModel {
 
                         ArithExpr wcetj = ctx.mkInt(0);
 
-                        for (HwExecutionNode jhwNode : inputInstance.getFeasibleCPUs(taskj)) {
+                        TMLTask taskjCast = (TMLTask)taskj;
+
+
+                        for (HwExecutionNode jhwNode : inputInstance.getFeasibleCPUs(taskjCast)) {
                             int jp = inputInstance.getArchitecture().getCPUs().indexOf(jhwNode);
 
-                            wcetj = ctx.mkAdd(wcetj, ctx.mkMul(X[tj][jp], ctx.mkInt(inputInstance.getWCET(taskj, jhwNode))));
+                            wcetj = ctx.mkAdd(wcetj, ctx.mkMul(X[tj][jp], ctx.mkInt(inputInstance.getWCET(taskjCast, jhwNode))));
 
 
                         }
@@ -608,7 +631,7 @@ public class OptimizationModel {
         //Grouping remaining constraints of the model
 
         // TraceManager.addDev("\nAll mapping constraints");
-        for (TMLTask task : (List<TMLTask>) inputInstance.getModeling().getTasks()) {
+        for (Object task : inputInstance.getModeling().getTasks()) {
 
             int t = inputInstance.getModeling().getTasks().indexOf(task);
 
@@ -659,7 +682,7 @@ public class OptimizationModel {
         // Add minimization objective.
         Optimize.Handle objective_latency = opt.MkMinimize(latency);
 
-        String outputToDisplay = "";
+        String outputToDisplay;
 
         if (opt.Check() == Status.SATISFIABLE) {
             Model m = opt.getModel();
@@ -668,15 +691,16 @@ public class OptimizationModel {
 
             outputToDisplay ="The optimal mapping solution is:\n\n";
 
-            for (TMLTask task : (List<TMLTask>) inputInstance.getModeling().getTasks()) {
+            for ( Object task : inputInstance.getModeling().getTasks()) {
                 int t = inputInstance.getModeling().getTasks().indexOf(task);
 
                 for (HwNode hwNode : inputInstance.getArchitecture().getCPUs()) {
                     int p = inputInstance.getArchitecture().getCPUs().indexOf(hwNode);
                     //evaluate optimal solution
                     optimized_result_X[t][p] = m.evaluate(X[t][p], true);
-
-                    optimizedSolutionX.put("X[" + task.getName() + "][" + hwNode.getName() + "] = ", Integer.parseInt(optimized_result_X[t][p]
+                    TMLTask taskCast = (TMLTask)task;
+                    optimizedSolutionX.put("X[" + taskCast.getName() + "][" + hwNode.getName() + "] = ", Integer.parseInt
+                            (optimized_result_X[t][p]
                             .toString()));
 
                    // TraceManager.addDev("X[" + task.getName() + "][" + hwNode.getName() + "] = " + optimized_result_X[t][p]);
@@ -685,12 +709,13 @@ public class OptimizationModel {
                 TraceManager.addDev("\n");
             }
 
-            for (TMLTask task : (List<TMLTask>) inputInstance.getModeling().getTasks()) {
+            for (Object task :  inputInstance.getModeling().getTasks()) {
                 int t = inputInstance.getModeling().getTasks().indexOf(task);
 
                 optimized_result_start[t] = m.evaluate(start[t], false);
+                TMLTask taskCast = (TMLTask)task;
 
-                optimizedSolutionStart.put("start[" + task.getName() + "] = ", Integer.parseInt(optimized_result_start[t].toString()));
+                optimizedSolutionStart.put("start[" + taskCast.getName() + "] = ", Integer.parseInt(optimized_result_start[t].toString()));
 
                // TraceManager.addDev("start[" + task.getName() + "] = " + optimized_result_start[t]);
 
-- 
GitLab