diff --git a/build.txt b/build.txt
index 4860db97cf1aef7979d88eb319db17334e72e626..ba09e3960b9a4c98b981e3748e5e1b6a8041a6cb 100644
--- a/build.txt
+++ b/build.txt
@@ -1 +1 @@
-12959
\ No newline at end of file
+12962
\ No newline at end of file
diff --git a/libs/com.microsoft.z3.jar b/libs/com.microsoft.z3.jar
new file mode 100644
index 0000000000000000000000000000000000000000..0ee9d9054f7d2a6310bb2fafc87a24ff0442463e
Binary files /dev/null and b/libs/com.microsoft.z3.jar differ
diff --git a/rundse/build.gradle b/rundse/build.gradle
index 49bc159bc6d02c39b3556520f355c6edbd989e84..ed941fa63fb3b40cd263453fbfa77c617034ecf1 100644
--- a/rundse/build.gradle
+++ b/rundse/build.gradle
@@ -24,6 +24,7 @@ dependencies {
compileOnly name:'batik-dom'
compileOnly name:'batik-util'
compile name:'jautomata-core'
+ compile name:'com.microsoft.z3'
}
jar {
diff --git a/rundse/manifest.txt b/rundse/manifest.txt
index 18e66503cd6d4de0cbbbfb608a66e099d2efef45..7ae7016992ad1704b32de0b058f74780cc53c74a 100755
--- a/rundse/manifest.txt
+++ b/rundse/manifest.txt
@@ -1 +1,2 @@
Main-Class: RunDSE
+Class-Path: com.microsoft.z3.jar
diff --git a/src/main/java/tmltranslator/dsez3engine/InputInstance.java b/src/main/java/tmltranslator/dsez3engine/InputInstance.java
new file mode 100644
index 0000000000000000000000000000000000000000..d9e5183d5b9217ecda60d9c5a592c3a909aab9f8
--- /dev/null
+++ b/src/main/java/tmltranslator/dsez3engine/InputInstance.java
@@ -0,0 +1,123 @@
+package tmltranslator.dsez3engine;
+
+import tmltranslator.*;
+
+import java.util.ArrayList;
+import java.util.List;
+
+
+public class InputInstance {
+
+ private TMLArchitecture architecture;
+ private TMLModeling modeling;
+
+ public InputInstance(TMLArchitecture architecture, TMLModeling modeling) {
+ this.architecture = architecture;
+ this.modeling = modeling;
+ }
+
+ //get the list of eligible CPUs for a given task
+ public List<HwExecutionNode> getFeasibleCPUs(TMLTask tmlTask) {
+
+ List<HwExecutionNode> feasibleCPUs = new ArrayList<>();
+
+ for (HwNode hwNode : architecture.getHwNodes()) {
+ if (hwNode instanceof HwExecutionNode) {
+
+ for (String operationType : ((HwExecutionNode) hwNode).getOperationTypes()) {
+ if (operationType.equals(tmlTask.getOperation())) {
+ feasibleCPUs.add((HwExecutionNode) hwNode);
+ break;
+ }
+ }
+ }
+
+ }
+ return feasibleCPUs;
+ }
+
+ // TODO the location of the implemented methods (better in TMLTask).
+ public int getBufferIn(TMLTask tmlTask) {
+
+ int bin = 0;
+ for (TMLChannel tmlReadChannel : tmlTask.getReadTMLChannels()) { // TODO replace with getReadChannels() once finished integration
+ bin = bin + tmlReadChannel.getNumberOfSamples();
+ }
+
+ return bin;
+ }
+
+ public int getBufferOut(TMLTask tmlTask) {
+ int bout = 0;
+ for (TMLChannel tmlWriteChannel : tmlTask.getWriteTMLChannels()) {
+ bout = bout + tmlWriteChannel.getNumberOfSamples();
+ }
+ return bout;
+ }
+
+ public int getWCET(TMLTask tmlTask, HwExecutionNode hwExecutionNode) {
+ return (tmlTask.getWorstCaseIComplexity() * hwExecutionNode.getExeciTime());
+ }
+
+ //should work for cases where each processing unit is equipped with a unique local memory connected directly through a bus
+ public HwMemory getLocalMemoryOfHwExecutionNode(HwNode hwNode) {
+
+ List<HwLink> firstLinks = new ArrayList<>();
+
+ for (int i = 0; i < architecture.getLinkByHwNode(hwNode).size(); i++) {
+ firstLinks.add(architecture.getLinkByHwNode(hwNode).get(i));
+ }
+
+
+ HwMemory tempMem = new HwMemory("");
+
+ if ((!firstLinks.isEmpty())) {
+ List<HwLink> secondLinks = new ArrayList<>();
+
+ for (int i = 0; i < architecture.getLinkByBus(firstLinks.get(0).bus).size(); i++) {
+ secondLinks.add(architecture.getLinkByBus(firstLinks.get(0).bus).get(i)); // link 1 and 1 cpu side
+ }
+
+
+ for (HwLink secondlink : secondLinks) {
+ if (secondlink.hwnode instanceof HwMemory) {
+ tempMem = (HwMemory) secondlink.hwnode;
+
+ }
+ }
+ }
+
+
+//TODO
+ /* if(firstLinks.size() >= 1){
+ for(HwLink recursiveHwLink : firstLinks){
+
+ }
+
+ }*/
+
+ return tempMem;
+ }
+
+ //TODO this supposes that we have one single final task
+
+ public TMLTask getFinalTask(TMLModeling tmlm){
+ TMLTask finalTask = null;
+ for (Object tmlTask : tmlm.getTasks()){
+ TMLTask taskCast = (TMLTask)tmlTask;
+ if (taskCast.getWriteTMLChannels().isEmpty())
+ finalTask = taskCast;
+ }
+
+ return finalTask;
+ }
+
+
+ public TMLArchitecture getArchitecture() {
+ return architecture;
+ }
+
+ public TMLModeling getModeling() {
+ return modeling;
+ }
+}
diff --git a/src/main/java/tmltranslator/dsez3engine/OptimizationModel.java b/src/main/java/tmltranslator/dsez3engine/OptimizationModel.java
new file mode 100644
index 0000000000000000000000000000000000000000..cb99bb9666c1da906f520f12ca465ca3890a7fac
--- /dev/null
+++ b/src/main/java/tmltranslator/dsez3engine/OptimizationModel.java
@@ -0,0 +1,752 @@
+package tmltranslator.dsez3engine;
+
+import com.microsoft.z3.*;
+import myutil.TraceManager;
+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;
+
+
+public class OptimizationModel {
+
+ private Map<String, Integer> optimizedSolutionX = new HashMap<String, Integer>();
+ private Map<String, Integer> optimizedSolutionStart = new HashMap<String, Integer>();
+ private InputInstance inputInstance;
+
+ public OptimizationModel(InputInstance inputInstance) {
+
+ this.inputInstance = inputInstance;
+ }
+
+ public Map<String, Integer> getOptimizedSolutionX() {
+ return optimizedSolutionX;
+ }
+
+ public void setOptimizedSolutionX(Map<String, Integer> optimizedSolutionX) {
+ this.optimizedSolutionX = optimizedSolutionX;
+ }
+
+ public Map<String, Integer> getOptimizedSolutionStart() {
+ return optimizedSolutionStart;
+ }
+
+ public void setOptimizedSolutionStart(Map<String, Integer> optimizedSolutionStart) {
+ this.optimizedSolutionStart = optimizedSolutionStart;
+ }
+
+
+ public void findFeasibleMapping(Context ctx) throws TestFailedException {
+
+ TraceManager.addDev("\nFind feasible Mapping");
+
+ //Decision variables
+
+ //Definition of Xtp as a matrix. Each cell corresponds to a combination of a task and a processor.
+ IntExpr[][] X = new IntExpr[inputInstance.getModeling().getTasks().size()][inputInstance.getArchitecture().getCPUs().size()]; //getCPUs returns only HwCPU elements
+
+ //TODO paths
+
+ //Definition of Ycw as a matrix. Each cell corresponds to a combination of a channel and a path.
+ // IntExpr[][] Y = new IntExpr[inputInstance.getModeling().getChannels().size()][tmlcpSequenceDiagrams.size()];
+
+ //Definition of start time variable for each task
+ IntExpr[] start = new IntExpr[inputInstance.getModeling().getTasks().size()];
+
+
+ //Mapping Constraints :
+ BoolExpr mapping_constraints = ctx.mkTrue();
+
+ //Matrix of constraints to define the interval of Xtp : 0 <= Xtp <= 1
+ BoolExpr[][] c_bound_x = new BoolExpr[inputInstance.getModeling().getTasks().size()][inputInstance.getArchitecture().getCPUs().size()];
+
+ //TraceManager.addDev("\nDefining the bounds of Xtp (1)");
+
+ 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_" + taskCast.getID() + "_" + hwNode.getID());
+
+ // Constraints: 0 <= Xtp <= 1
+ c_bound_x[t][p] = ctx.mkAnd(ctx.mkLe(ctx.mkInt(0), X[t][p]),
+ ctx.mkLe(X[t][p], ctx.mkInt(1)));
+
+ // TraceManager.addDev(c_bound_x[t][p]);
+ }
+ }
+
+ //Constraint on start >=0
+ BoolExpr[] c_bound_start = new BoolExpr[inputInstance.getModeling().getTasks().size()];
+
+ for (Object tmlTask : inputInstance.getModeling().getTasks()) {
+ int t = inputInstance.getModeling().getTasks().indexOf(tmlTask);
+ 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]);
+ }
+
+ // TODO add the definition interval for Ycw
+
+ //CONSTRAINTS//
+ //Each task must be mapped to exactly 1 processing unit in its eligibility set:
+
+ // ∀t, SUM p (X tp) ≤ 1
+
+ //TraceManager.addDev("\nUnique task-CPU mapping constraints (3)");
+ BoolExpr[] c_unique_x = new BoolExpr[inputInstance.getModeling().getTasks().size()];
+ 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));
+ // TraceManager.addDev(c_unique_x[t]);
+
+ }
+
+
+ //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 (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(taskCast)) {
+
+ int p = inputInstance.getArchitecture().getCPUs().indexOf(hwNode);
+
+ sum_X = ctx.mkAdd(sum_X, X[t][p]);
+ }
+ c_feasibleMapX[t] = ctx.mkEq(sum_X, ctx.mkInt(1));
+
+ //TraceManager.addDev(c_feasibleMapX[t]);
+
+ }
+
+ //Memory size constraint: ∀p, ∀t, X tp × (bin + bout ) ≤ mem
+
+ //TraceManager.addDev("\nMemory size constraints (5)");
+ BoolExpr[][] c_mem = new BoolExpr[inputInstance.getArchitecture().getNbOfCPU()][inputInstance.getModeling().getTasks().size()];
+
+ for (HwNode hwNode : inputInstance.getArchitecture().getCPUs()) {
+ int p = inputInstance.getArchitecture().getCPUs().indexOf(hwNode);
+
+ IntExpr mem = ctx.mkInt(inputInstance.getLocalMemoryOfHwExecutionNode(hwNode).memorySize);
+
+
+ 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(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);
+
+ // TraceManager.addDev(c_mem[p][t]);
+
+ }
+ }
+
+/*
+ //At least one route Constraint: ∀c, (t1,t2) in c; X t1p1 + X t2p2 − r p1p2 ≤ 1
+ TraceManager.addDev("\nAt least one route constraints (6)");
+ BoolExpr[] c_route = new BoolExpr[inputInstance.getModeling().getChannels().size()];
+
+ IntExpr[][] r = new IntExpr[inputInstance.getArchitecture().getCPUs().size()][inputInstance.getArchitecture().getCPUs().size()];
+
+ for (TMLChannel channel : (List<TMLChannel>) inputInstance.getModeling().getChannels()) {
+
+ int c = inputInstance.getModeling().getChannels().indexOf(channel);
+ //for each channel get producer and consumer
+ TMLTask producer = channel.getOriginTask();
+ int prodIndex = inputInstance.getModeling().getTasks().indexOf(producer);
+
+ TMLTask consumer = channel.getDestinationTask();
+ int consIndex = inputInstance.getModeling().getTasks().indexOf(consumer);
+
+ for (HwNode source : inputInstance.getArchitecture().getCPUs()) {
+ int src = inputInstance.getArchitecture().getCPUs().indexOf(source);
+
+ for (HwNode destination : inputInstance.getArchitecture().getCPUs()) {
+ int dst = inputInstance.getArchitecture().getCPUs().indexOf(destination);
+ //for each couple of processors TODO calculate rp1p2
+ r[src][dst] = ctx.mkInt(1);
+ ArithExpr Xp_plus_Xc = ctx.mkAdd(X[prodIndex][src], X[consIndex][dst]);
+ ArithExpr Xp_plus_Xc_minus_r = ctx.mkSub(Xp_plus_Xc, r[src][dst]);
+
+ c_route[c] = ctx.mkLe(Xp_plus_Xc_minus_r, ctx.mkInt(1));
+
+ TraceManager.addDev("Channel(" + channel.toString() + ") " + c_route[c]);
+
+
+ // mapping_constraints = ctx.mkAnd(c_route[c], mapping_constraints);
+ }
+ }
+ }
+*/
+ //Scheduling: Precedence constraints: ∀c, τs (t cons ) ≥ τe (t prod )
+ // TraceManager.addDev("\nPrecedence constraints (11)");
+ BoolExpr[] c_precedence = new BoolExpr[inputInstance.getModeling().getChannels().size()];
+
+ 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 = channelCast.getOriginTask();
+ int prodIndex = inputInstance.getModeling().getTasks().indexOf(producer);
+
+ TMLTask consumer = channelCast.getDestinationTask();
+ int consIndex = inputInstance.getModeling().getTasks().indexOf(consumer);
+
+ ArithExpr wcetProducer = ctx.mkInt(0);
+
+ for (HwExecutionNode hwNode : inputInstance.getFeasibleCPUs(producer)) {
+ int p = inputInstance.getArchitecture().getCPUs().indexOf(hwNode);
+
+ wcetProducer = ctx.mkAdd(wcetProducer, ctx.mkMul(X[prodIndex][p], ctx.mkInt(inputInstance.getWCET(producer, hwNode))));
+
+ }
+
+ ArithExpr endProducer = ctx.mkAdd(start[prodIndex], wcetProducer);
+ ArithExpr startC_minus_endP = ctx.mkSub(start[consIndex], endProducer);
+
+ c_precedence[c] = ctx.mkGe(startC_minus_endP, ctx.mkInt(0));
+
+ // TraceManager.addDev(c_precedence[c]);
+
+ mapping_constraints = ctx.mkAnd(mapping_constraints, c_precedence[c]);
+
+ }
+
+
+ //∀p∀t i ∀t j 6 = t i , ¬((X t i p = 1) ∧ (X t j p = 1)) ∨ ((τ s (t j ) ≥ τ e (t i )) ∨ (τ s (t i ) ≥ τ e (t j )))
+ //Scheduling: One single task running on CPU ∀t
+ //TraceManager.addDev("\n Same resource/no time overlap Constraints (12)");
+ BoolExpr c_monoTask[][][] = new BoolExpr[inputInstance.getArchitecture().getCPUs().size()][inputInstance.getModeling().getTasks().size()][inputInstance.getModeling().getTasks().size()];
+
+ for (HwNode hwNode : inputInstance.getArchitecture().getCPUs()) {
+ int p = inputInstance.getArchitecture().getCPUs().indexOf(hwNode);
+
+ 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(taskiCast)) {
+ int ip = inputInstance.getArchitecture().getCPUs().indexOf(ihwNode);
+
+ wceti = ctx.mkAdd(wceti, ctx.mkMul(X[ti][ip], ctx.mkInt(inputInstance.getWCET(taskiCast, ihwNode))));
+
+ }
+
+ ArithExpr endti = ctx.mkAdd(start[ti], wceti);
+
+ for (Object taskj : inputInstance.getModeling().getTasks()) {
+
+ int tj = inputInstance.getModeling().getTasks().indexOf(taskj);
+ TMLTask taskjCast = (TMLTask)taskj;
+
+
+ if (tj != ti) {
+ //Calculate End times of tj
+
+ ArithExpr wcetj = ctx.mkInt(0);
+
+ 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(taskjCast, jhwNode))));
+
+
+ }
+
+ ArithExpr endtj = ctx.mkAdd(start[tj], wcetj);
+
+ BoolExpr alpha = ctx.mkAnd(ctx.mkEq(X[ti][p], ctx.mkInt(1)), ctx.mkEq(X[tj][p], ctx.mkInt(1)));
+
+ BoolExpr not_alpha = ctx.mkNot(alpha);
+
+ BoolExpr beta = ctx.mkOr(ctx.mkGe(start[ti], endtj), ctx.mkGe(start[tj], endti));
+
+ //
+ c_monoTask[p][ti][tj] = ctx.mkOr(not_alpha, beta);
+ // TraceManager.addDev("\n" + c_monoTask[p][ti][tj]);
+
+ mapping_constraints = ctx.mkAnd(mapping_constraints, c_monoTask[p][ti][tj]);
+ }
+ }
+
+ }
+
+ }
+
+
+ //Grouping remaining constraints of the model
+
+ // TraceManager.addDev("\nAll mapping constraints");
+ 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);
+
+ mapping_constraints = ctx.mkAnd(c_bound_x[t][p], mapping_constraints);
+ mapping_constraints = ctx.mkAnd(c_mem[p][t], mapping_constraints);
+
+ }
+
+ // Constraint: feasible unique mapping of tasks
+ mapping_constraints = ctx.mkAnd(c_unique_x[t], mapping_constraints);
+ mapping_constraints = ctx.mkAnd(c_feasibleMapX[t], mapping_constraints);
+
+ }
+
+ //Creating a solver instance
+ Solver s = ctx.mkSolver();
+ s.add(mapping_constraints);
+
+
+ if (s.check() == Status.SATISFIABLE) {
+ Model m = s.getModel();
+ Expr[][] optimized_result_X = new Expr[inputInstance.getModeling().getTasks().size()][inputInstance.getArchitecture().getCPUs().size()];
+ Expr[] optimized_result_start = new Expr[inputInstance.getModeling().getTasks().size()];
+
+ TraceManager.addDev("Proposed feasible Mapping solution:");
+
+
+ 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[" + taskCast.getName() + "][" + hwNode.getName() + "] = " + optimized_result_X[t][p]);
+
+ }
+
+ TraceManager.addDev("\n");
+ }
+
+ 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[" + taskCast.getName() + "] = " + optimized_result_start[t]);
+
+ }
+
+
+ } else {
+ TraceManager.addDev("Failed to solve mapping problem");
+ throw new TestFailedException();
+ }
+
+
+ }//findFeasibleMapping()
+
+
+ public void findOptimizedMapping(Context ctx) throws TestFailedException {
+
+ TraceManager.addDev("\nFind an optimized Mapping");
+
+ //Decision variables
+
+ //Definition of Xtp as a matrix. Each cell corresponds to a combination of a task and a processor.
+ IntExpr[][] X = new IntExpr[inputInstance.getModeling().getTasks().size()][inputInstance.getArchitecture().getCPUs().size()]; //getCPUs returns only HwCPU elements
+
+
+ //Definition of start time variable for each task
+ IntExpr[] start = new IntExpr[inputInstance.getModeling().getTasks().size()];
+
+
+ //Mapping Constraints :
+ BoolExpr mapping_constraints = ctx.mkTrue();
+
+ //Matrix of constraints to define the interval of Xtp : 0 <= Xtp <= 1
+ BoolExpr[][] c_bound_x = new BoolExpr[inputInstance.getModeling().getTasks().size()][inputInstance.getArchitecture().getCPUs().size()];
+
+ //TraceManager.addDev("\nDefining the bounds of Xtp (1)");
+
+ 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_" + taskCast.getID() + "_" + hwNode.getID());
+
+ // Constraints: 0 <= Xtp <= 1
+ c_bound_x[t][p] = ctx.mkAnd(ctx.mkLe(ctx.mkInt(0), X[t][p]),
+ ctx.mkLe(X[t][p], ctx.mkInt(1)));
+
+ // TraceManager.addDev(c_bound_x[t][p]);
+ }
+ }
+
+ //Constraint on start >=0
+ BoolExpr[] c_bound_start = new BoolExpr[inputInstance.getModeling().getTasks().size()];
+
+ for (Object tmlTask : inputInstance.getModeling().getTasks()) {
+ int t = inputInstance.getModeling().getTasks().indexOf(tmlTask);
+
+ 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]);
+ }
+
+
+ //CONSTRAINTS//
+ //Each task must be mapped to exactly 1 processing unit in its eligibility set:
+
+ // ∀t, SUM p (X tp) ≤ 1
+
+ //TraceManager.addDev("\nUnique task-CPU mapping constraints (3)");
+ BoolExpr[] c_unique_x = new BoolExpr[inputInstance.getModeling().getTasks().size()];
+ 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]);
+ c_unique_x[t] = ctx.mkLe(sum_X, ctx.mkInt(1));
+ // TraceManager.addDev(c_unique_x[t]);
+
+ }
+
+
+ //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 (Object tmlTask : inputInstance.getModeling().getTasks()) {
+ int t = inputInstance.getModeling().getTasks().indexOf(tmlTask);
+ ArithExpr sum_X = ctx.mkInt(0);
+
+ TMLTask taskCast = (TMLTask)tmlTask;
+
+ for (HwNode hwNode : inputInstance.getFeasibleCPUs(taskCast)) {
+
+ int p = inputInstance.getArchitecture().getCPUs().indexOf(hwNode);
+
+ sum_X = ctx.mkAdd(sum_X, X[t][p]);
+ }
+ c_feasibleMapX[t] = ctx.mkEq(sum_X, ctx.mkInt(1));
+
+ //TraceManager.addDev(c_feasibleMapX[t]);
+
+ }
+
+ //Memory size constraint: ∀p, ∀t, X tp × (bin + bout ) ≤ mem
+
+ //TraceManager.addDev("\nMemory size constraints (5)");
+ BoolExpr[][] c_mem = new BoolExpr[inputInstance.getArchitecture().getNbOfCPU()][inputInstance.getModeling().getTasks().size()];
+
+ for (HwNode hwNode : inputInstance.getArchitecture().getCPUs()) {
+ int p = inputInstance.getArchitecture().getCPUs().indexOf(hwNode);
+
+ IntExpr mem = ctx.mkInt(inputInstance.getLocalMemoryOfHwExecutionNode(hwNode).memorySize);
+
+
+ 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(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);
+
+ // TraceManager.addDev(c_mem[p][t]);
+
+ }
+ }
+
+/*
+ //At least one route Constraint: ∀c, (t1,t2) in c; X t1p1 + X t2p2 − r p1p2 ≤ 1
+ TraceManager.addDev("\nAt least one route constraints (6)");
+ BoolExpr[] c_route = new BoolExpr[inputInstance.getModeling().getChannels().size()];
+
+ IntExpr[][] r = new IntExpr[inputInstance.getArchitecture().getCPUs().size()][inputInstance.getArchitecture().getCPUs().size()];
+
+ for (TMLChannel channel : (List<TMLChannel>) inputInstance.getModeling().getChannels()) {
+
+ int c = inputInstance.getModeling().getChannels().indexOf(channel);
+ //for each channel get producer and consumer
+ TMLTask producer = channel.getOriginTask();
+ int prodIndex = inputInstance.getModeling().getTasks().indexOf(producer);
+
+ TMLTask consumer = channel.getDestinationTask();
+ int consIndex = inputInstance.getModeling().getTasks().indexOf(consumer);
+
+ for (HwNode source : inputInstance.getArchitecture().getCPUs()) {
+ int src = inputInstance.getArchitecture().getCPUs().indexOf(source);
+
+ for (HwNode destination : inputInstance.getArchitecture().getCPUs()) {
+ int dst = inputInstance.getArchitecture().getCPUs().indexOf(destination);
+ //for each couple of processors TODO calculate rp1p2
+ r[src][dst] = ctx.mkInt(1);
+ ArithExpr Xp_plus_Xc = ctx.mkAdd(X[prodIndex][src], X[consIndex][dst]);
+ ArithExpr Xp_plus_Xc_minus_r = ctx.mkSub(Xp_plus_Xc, r[src][dst]);
+
+ c_route[c] = ctx.mkLe(Xp_plus_Xc_minus_r, ctx.mkInt(1));
+
+ TraceManager.addDev("Channel(" + channel.toString() + ") " + c_route[c]);
+
+
+ // mapping_constraints = ctx.mkAnd(c_route[c], mapping_constraints);
+ }
+ }
+ }
+*/
+ //Scheduling: Precedence constraints: ∀c, τs (t cons ) ≥ τe (t prod )
+ // TraceManager.addDev("\nPrecedence constraints (11)");
+ BoolExpr[] c_precedence = new BoolExpr[inputInstance.getModeling().getChannels().size()];
+
+ for (Object channel : inputInstance.getModeling().getChannels()) {
+
+ int c = inputInstance.getModeling().getChannels().indexOf(channel);
+ //for each channel get producer and consumer
+ TMLChannel channelCast = (TMLChannel)channel;
+ TMLTask producer = channelCast.getOriginTask();
+ int prodIndex = inputInstance.getModeling().getTasks().indexOf(producer);
+
+ TMLTask consumer = channelCast.getDestinationTask();
+ int consIndex = inputInstance.getModeling().getTasks().indexOf(consumer);
+
+ //TraceManager.addDev("\nChannel(" + producer.getId() + "," + consumer.getId() + ")");
+
+ ArithExpr wcetProducer = ctx.mkInt(0);
+
+ for (HwExecutionNode hwNode : inputInstance.getFeasibleCPUs(producer)) {
+ int p = inputInstance.getArchitecture().getCPUs().indexOf(hwNode);
+
+ wcetProducer = ctx.mkAdd(wcetProducer, ctx.mkMul(X[prodIndex][p], ctx.mkInt(inputInstance.getWCET(producer, hwNode))));
+
+ }
+
+ ArithExpr endProducer = ctx.mkAdd(start[prodIndex], wcetProducer);
+ ArithExpr startC_minus_endP = ctx.mkSub(start[consIndex], endProducer);
+
+ c_precedence[c] = ctx.mkGe(startC_minus_endP, ctx.mkInt(0));
+
+ // TraceManager.addDev(c_precedence[c]);
+
+ mapping_constraints = ctx.mkAnd(mapping_constraints, c_precedence[c]);
+
+ }
+
+
+ //∀p∀t i ∀t j 6 = t i , ¬((X t i p = 1) ∧ (X t j p = 1)) ∨ ((τ s (t j ) ≥ τ e (t i )) ∨ (τ s (t i ) ≥ τ e (t j )))
+ //Scheduling: One single task running on CPU ∀t
+ //TraceManager.addDev("\n Same resource/no time overlap Constraints (12)");
+ BoolExpr c_monoTask[][][] = new BoolExpr[inputInstance.getArchitecture().getCPUs().size()][inputInstance.getModeling().getTasks().size()][inputInstance.getModeling().getTasks().size()];
+
+ for (HwNode hwNode : inputInstance.getArchitecture().getCPUs()) {
+ int p = inputInstance.getArchitecture().getCPUs().indexOf(hwNode);
+
+ for (Object taski : inputInstance.getModeling().getTasks()) {
+
+ int ti = inputInstance.getModeling().getTasks().indexOf(taski);
+ //Calculate End times of ti
+ ArithExpr wceti = ctx.mkInt(0);
+
+ 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(taskiCast, ihwNode))));
+
+ }
+
+ ArithExpr endti = ctx.mkAdd(start[ti], wceti);
+
+ for (Object taskj : inputInstance.getModeling().getTasks()) {
+
+ int tj = inputInstance.getModeling().getTasks().indexOf(taskj);
+
+
+ if (tj != ti) {
+ //Calculate End times of tj
+
+ ArithExpr wcetj = ctx.mkInt(0);
+
+ 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(taskjCast, jhwNode))));
+
+
+ }
+
+ ArithExpr endtj = ctx.mkAdd(start[tj], wcetj);
+
+ BoolExpr alpha = ctx.mkAnd(ctx.mkEq(X[ti][p], ctx.mkInt(1)), ctx.mkEq(X[tj][p], ctx.mkInt(1)));
+
+ BoolExpr not_alpha = ctx.mkNot(alpha);
+
+ BoolExpr beta = ctx.mkOr(ctx.mkGe(start[ti], endtj), ctx.mkGe(start[tj], endti));
+
+ //
+ c_monoTask[p][ti][tj] = ctx.mkOr(not_alpha, beta);
+ // TraceManager.addDev("\n" + c_monoTask[p][ti][tj]);
+
+ mapping_constraints = ctx.mkAnd(mapping_constraints, c_monoTask[p][ti][tj]);
+ }
+ }
+
+ }
+
+ }
+
+
+ //Grouping remaining constraints of the model
+
+ // TraceManager.addDev("\nAll mapping constraints");
+ 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);
+
+ mapping_constraints = ctx.mkAnd(c_bound_x[t][p], mapping_constraints);
+ mapping_constraints = ctx.mkAnd(c_mem[p][t], mapping_constraints);
+
+ }
+
+ // Constraint: feasible unique mapping of tasks
+ mapping_constraints = ctx.mkAnd(c_unique_x[t], mapping_constraints);
+ mapping_constraints = ctx.mkAnd(c_feasibleMapX[t], mapping_constraints);
+
+ }
+
+ //OPTIMIZE CONTEXT
+
+ //Create an Optimize context
+ Optimize opt = ctx.mkOptimize();
+
+ //Assert a constraints into the optimize solver
+ opt.Add(mapping_constraints);
+
+
+ // Objective: minimize latency
+
+ //Creating an expression for latency
+
+ //Calculating end time of last task
+ TMLTask finalTask = inputInstance.getFinalTask(inputInstance.getModeling());
+ int finalTaskIndex = inputInstance.getModeling().getTasks().indexOf(inputInstance.getFinalTask(inputInstance.getModeling()));
+ ArithExpr wcet_last = ctx.mkInt(0);
+ int l = 0;
+ for (HwExecutionNode hwNode : inputInstance.getFeasibleCPUs(inputInstance.getFinalTask(inputInstance.getModeling()))) {
+ int p = inputInstance.getArchitecture().getCPUs().indexOf(hwNode);
+ wcet_last = ctx.mkAdd(wcet_last, ctx.mkMul(X[finalTaskIndex][p], ctx.mkInt(inputInstance.getWCET(finalTask, hwNode))));
+ l += 1;
+
+ }
+
+ ArithExpr end_last = ctx.mkAdd(start[finalTaskIndex], wcet_last);
+
+ ArithExpr latency = ctx.mkSub(end_last, ctx.mkInt(0));
+
+
+ // Add minimization objective.
+ Optimize.Handle objective_latency = opt.MkMinimize(latency);
+
+ String outputToDisplay;
+
+ if (opt.Check() == Status.SATISFIABLE) {
+ Model m = opt.getModel();
+ Expr[][] optimized_result_X = new Expr[inputInstance.getModeling().getTasks().size()][inputInstance.getArchitecture().getCPUs().size()];
+ Expr[] optimized_result_start = new Expr[inputInstance.getModeling().getTasks().size()];
+
+ outputToDisplay ="The optimal mapping solution is:\n\n";
+
+ 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);
+ 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]);
+ }
+
+ TraceManager.addDev("\n");
+ }
+
+ 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[" + taskCast.getName() + "] = ", Integer.parseInt(optimized_result_start[t].toString()));
+
+ // TraceManager.addDev("start[" + task.getName() + "] = " + optimized_result_start[t]);
+
+ }
+
+ for(Map.Entry<String, Integer> entry : optimizedSolutionX.entrySet()) {
+ outputToDisplay = outputToDisplay + entry.getKey() + " = " + entry.getValue() + "\n";
+ }
+
+ outputToDisplay += "\n\n";
+
+ for(Map.Entry<String, Integer> entry : optimizedSolutionStart.entrySet()) {
+ outputToDisplay = outputToDisplay + entry.getKey() + " = " + entry.getValue() + "\n";
+ }
+
+ TraceManager.addDev(outputToDisplay);
+
+ } else {
+ outputToDisplay ="Failed to solve mapping problem";
+ TraceManager.addDev(outputToDisplay);
+ throw new TestFailedException();
+ }
+
+ }
+
+
+ class TestFailedException extends Exception {
+ public TestFailedException() {
+ super("Check FAILED");
+ }
+ }
+
+
+}
diff --git a/src/main/java/ui/ActionPerformer.java b/src/main/java/ui/ActionPerformer.java
index 18d5b9846f93578b73756508ff36bfa24be0aa96..28bb9705c00b458e1cc11704bc19044df6d05901 100644
--- a/src/main/java/ui/ActionPerformer.java
+++ b/src/main/java/ui/ActionPerformer.java
@@ -173,6 +173,10 @@ public class ActionPerformer {
mgui.generateUPPAAL();
} else if (command.equals(mgui.actions[TGUIAction.ACT_DSE].getActionCommand())) {
mgui.dse();
+ } else if (command.equals(mgui.actions[TGUIAction.ACT_DSE_Z3].getActionCommand())) {
+ mgui.dseZ3();
+ } else if (command.equals(mgui.actions[TGUIAction.ACT_DSE].getActionCommand())) {
+ mgui.dse();
} else if (command.equals(mgui.actions[TGUIAction.ACT_AVATAR_MODEL_CHECKER].getActionCommand())) {
mgui.avatarModelChecker();
} else if (command.equals(mgui.actions[TGUIAction.ACT_GEN_JAVA].getActionCommand())) {
diff --git a/src/main/java/ui/JToolBarMainTurtle.java b/src/main/java/ui/JToolBarMainTurtle.java
index c926eb9a104cebe3d3c88729ee8dae247eeed35a..69dc3d24ac599c7896ed37580b1ed5e2fe3076c3 100644
--- a/src/main/java/ui/JToolBarMainTurtle.java
+++ b/src/main/java/ui/JToolBarMainTurtle.java
@@ -64,7 +64,7 @@ public class JToolBarMainTurtle extends JToolBar implements ActionListener
JButton avatarSimu, avatarFVUPPAAL, avatarFVProVerif, avatarFVStaticAnalysis, avatarCodeGeneration, avatarMC;
// Other
- JButton genrtlotos, genlotos, genuppaal, gendesign, dse;
+ JButton genrtlotos, genlotos, genuppaal, gendesign, dse, dseZ3;
JButton checkcode, simulation, validation;
JButton oneClickrtlotos, onclicklotos, gensystemc, simusystemc, gentml, genC, genjava, nc,externalSearch, internalSearch;
@@ -166,6 +166,11 @@ public class JToolBarMainTurtle extends JToolBar implements ActionListener
dse = add(mgui.actions[TGUIAction.ACT_DSE]);
dse.addMouseListener(mgui.mouseHandler);
+ if (MainGUI.experimentalOn) {
+ dseZ3 = add(mgui.actions[TGUIAction.ACT_DSE_Z3]);
+ dseZ3.addMouseListener(mgui.mouseHandler);
+ }
+
addSeparator();
//if (MainGUI.experimentalOn) {
@@ -318,6 +323,7 @@ public class JToolBarMainTurtle extends JToolBar implements ActionListener
//TraceManager.addDev("Show avatar options with b = " + b);
dse.setVisible(!b);
+ dseZ3.setVisible(!b);
avatarSimu.setVisible(b);
avatarFVUPPAAL.setVisible(b);
@@ -395,6 +401,7 @@ public class JToolBarMainTurtle extends JToolBar implements ActionListener
//TraceManager.addDev("Show diplodocus options with b = " + b);
dse.setVisible(b);
+ dseZ3.setVisible(b);
avatarSimu.setVisible(!b);
avatarFVUPPAAL.setVisible(!b);
avatarFVStaticAnalysis.setVisible(!b);
diff --git a/src/main/java/ui/MainGUI.java b/src/main/java/ui/MainGUI.java
index 3f9ff6ba8112d005283a48bfd7955fde4885a315..498d6b496192a7939a5422c30c1bbfd0320b3085 100644
--- a/src/main/java/ui/MainGUI.java
+++ b/src/main/java/ui/MainGUI.java
@@ -4793,6 +4793,15 @@ public class MainGUI implements ActionListener, WindowListener, KeyListener, Per
dtree.toBeUpdated();
}
+ public void dseZ3() {
+ TraceManager.addDev("Design space exploration with Z3");
+ /*JDialogDSE jdse = new JDialogDSE(frame, this, "Design Space Exploration", SpecConfigTTool.SystemCCodeDirectory, SpecConfigTTool.TMLCodeDirectory);
+ // jdse.setSize(600,800);
+ GraphicLib.centerOnParent(jdse, 700, 800);
+ jdse.setVisible(true);
+ dtree.toBeUpdated();*/
+ }
+
public void avatarStaticAnalysis() {
TraceManager.addDev("Avatar static analysis invariants");
JDialogInvariantAnalysis jgen = new JDialogInvariantAnalysis(frame, this, "Static analysis: invariants computation");
diff --git a/src/main/java/ui/ModeManager.java b/src/main/java/ui/ModeManager.java
index d771aec8268fe34be460b41fd63a79520aadd676..37712ad69d103a0ecdd2a500864568d96d4df278 100644
--- a/src/main/java/ui/ModeManager.java
+++ b/src/main/java/ui/ModeManager.java
@@ -144,6 +144,7 @@ public class ModeManager {
actions[TGUIAction.ACT_GEN_RTLOTOS].setEnabled(true);
actions[TGUIAction.ACT_GEN_LOTOS].setEnabled(true);
actions[TGUIAction.ACT_DSE].setEnabled(true);
+ actions[TGUIAction.ACT_DSE_Z3].setEnabled(true);
if (mgui.getCurrentTURTLEPanel() instanceof TMLComponentDesignPanel) {
actions[TGUIAction.ACT_GEN_UPPAAL].setEnabled(true);
} else {
@@ -228,6 +229,7 @@ public class ModeManager {
actions[TGUIAction.ACT_GEN_RTLOTOS].setEnabled(false);
actions[TGUIAction.ACT_GEN_LOTOS].setEnabled(false);
actions[TGUIAction.ACT_DSE].setEnabled(false);
+ actions[TGUIAction.ACT_DSE_Z3].setEnabled(false);
actions[TGUIAction.ACT_GEN_JAVA].setEnabled(false);
actions[TGUIAction.ACT_SIMU_JAVA].setEnabled(false);
actions[TGUIAction.ACT_GEN_DESIGN].setEnabled(false);
@@ -252,6 +254,7 @@ public class ModeManager {
actions[TGUIAction.ACT_GEN_RTLOTOS].setEnabled(false);
actions[TGUIAction.ACT_GEN_LOTOS].setEnabled(false);
actions[TGUIAction.ACT_DSE].setEnabled(false);
+ actions[TGUIAction.ACT_DSE_Z3].setEnabled(false);
actions[TGUIAction.ACT_CHECKCODE].setEnabled(false);
actions[TGUIAction.ACT_SIMULATION].setEnabled(false);
actions[TGUIAction.ACT_VALIDATION].setEnabled(false);
@@ -272,6 +275,7 @@ public class ModeManager {
actions[TGUIAction.ACT_GEN_RTLOTOS].setEnabled(false);
actions[TGUIAction.ACT_GEN_LOTOS].setEnabled(false);
actions[TGUIAction.ACT_DSE].setEnabled(false);
+ actions[TGUIAction.ACT_DSE_Z3].setEnabled(false);
actions[TGUIAction.ACT_GEN_JAVA].setEnabled(false);
actions[TGUIAction.ACT_SIMU_JAVA].setEnabled(false);
actions[TGUIAction.ACT_GEN_DESIGN].setEnabled(false);
diff --git a/src/main/java/ui/TGUIAction.java b/src/main/java/ui/TGUIAction.java
index 2b4bfd066bbf84e9c886fbb8562a7ecd1e3249a7..6defdce51bbd17189e592a6bfd472366d62dbde9 100644
--- a/src/main/java/ui/TGUIAction.java
+++ b/src/main/java/ui/TGUIAction.java
@@ -649,6 +649,7 @@ public class TGUIAction extends AbstractAction {
public static final int ACT_AVATAR_EXECUTABLE_GENERATION = 340;
public static final int ACT_DSE = 434;
+ public static final int ACT_DSE_Z3 = 516;
// Ontologies
public static final int ACT_GENERATE_ONTOLOGIES_CURRENT_DIAGRAM = 367;
@@ -667,7 +668,7 @@ public class TGUIAction extends AbstractAction {
public static final int MOVE_ENABLED = 463;
public static final int FIRST_DIAGRAM = 464;
- public static final int NB_ACTION = 516;
+ public static final int NB_ACTION = 517;
private static final TAction [] actions = new TAction[NB_ACTION];
@@ -866,7 +867,9 @@ public class TGUIAction extends AbstractAction {
actions[ACT_VIEW_PM_AUT] = new TAction("viewpmaut-command", "Power Management Analysis (last AUT graph)", IconManager.imgic28, IconManager.imgic29, "Power Management Analysis (last AUT graph)", "Power Management Analysis on the last generated reachability graph generated in AUT (Aldebaran) format", 0);
actions[ACT_VIEW_PM_AUTPROJ] = new TAction("viewpmautproj-command", "Power Management Analysis (last minimized AUT graph)", IconManager.imgic28, IconManager.imgic29, "Power Management Analysis (last minimized AUT graph)", "Power Management Analysis on the last minimized reachability graph in AUT (Aldebaran) format", 0);
actions[ACT_VIEW_PM_SAVED_AUT] = new TAction("viewpmsavedautproj-command", "Power Management Analysis (saved AUT graph)", IconManager.imgic28, IconManager.imgic29, "Power Management Analysis (saved AUT graph)", "Power Management Analysis on a graph saved in AUT (Aldebaran) format", 0);
- actions[ACT_DSE] = new TAction("auto-dse", "Automated Design Space Exploration", IconManager.imgic89, IconManager.imgic89, "Automated Design Space Exploration", "Find the optimal mapping and security additions automatically",0);
+ actions[ACT_DSE] = new TAction("auto-dse", "Automated Design Space Exploration", IconManager.imgic89, IconManager.imgic89, "Automated Design Space Exploration", "Find the optimal mapping with brute-force simulations",0);
+ actions[ACT_DSE_Z3] = new TAction("auto-dse-z3", "Automated Design Space Exploration with Z3", IconManager.imgic89_z3, IconManager.imgic89_z3, "Automated Design Space Exploration with Z3", "Find the optimal mapping with Z3",0);
+
// AVATAR
actions[ACT_AVATAR_SIM] = new TAction("avatar-simu", "Interactive simulation", IconManager.imgic18, IconManager.imgic18, "Interactive simulation", "Interactive simulation of the AVATAR design under edition", '2');
actions[ACT_AVATAR_FV_UPPAAL] = new TAction("avatar-formal-verification-uppaal", "Safety formal verification with UPPAAL (Safety)", IconManager.imgic86, IconManager.imgic86, "Formal verification with UPPAAL (Safety)", "Formal verification with UPPAAL (Safety) of the AVATAR design under edition", '3');
diff --git a/src/main/java/ui/util/DefaultText.java b/src/main/java/ui/util/DefaultText.java
index ee0e4edb277de676582a85e5735491f3f244fa54..76862b2fd2cd74d4383e0ed308b66b6a36897168 100755
--- a/src/main/java/ui/util/DefaultText.java
+++ b/src/main/java/ui/util/DefaultText.java
@@ -50,8 +50,8 @@ package ui.util;
*/
public class DefaultText {
- public static String BUILD = "12958";
- public static String DATE = "2019/02/23 03:02:12 CET";
+ public static String BUILD = "12961";
+ public static String DATE = "2019/02/26 03:02:13 CET";
public static StringBuffer sbAbout = makeAbout();
diff --git a/src/main/java/ui/util/IconManager.java b/src/main/java/ui/util/IconManager.java
index d85639588433221e0c71ba60057ee2823edfe669..0a0a2f1a821671528a0f08908514f33f61c9e7bb 100755
--- a/src/main/java/ui/util/IconManager.java
+++ b/src/main/java/ui/util/IconManager.java
@@ -71,7 +71,7 @@ public class IconManager {
public static ImageIcon imgic50, imgic51, imgic52, imgic53, imgic54, imgic55, imgic56, imgic57, imgic58, imgic59;
public static ImageIcon imgic60, imgic61, imgic62, imgic63, imgic64, imgic65, imgic66, imgic68;
public static ImageIcon imgic70, imgic71, imgic72, imgic73, imgic75, imgic76, imgic77, imgic78, imgic79, imgic780;
- public static ImageIcon imgic80, imgic82, imgic84, imgic86, imgic88, imgic89;
+ public static ImageIcon imgic80, imgic82, imgic84, imgic86, imgic88, imgic89, imgic89_z3;
public static ImageIcon imgic90, imgic92, imgic94, imgic96, imgic98, imgic99;
public static ImageIcon imgic142;
@@ -295,6 +295,7 @@ public class IconManager {
private static String icon86 = "avatarfvuppaal.png";
private static String icon88 = "avatarfvproverif.png";
private static String icon89 = "dse.png";
+ private static String icon89_z3 = "dse_z3.png";
private static String icon90 = "genlotos.gif";
private static String icon92 = "genuppaal.gif";
private static String icon94 = "avatarcodegeneration.gif";
@@ -837,6 +838,7 @@ public class IconManager {
imgic86 = getIcon(icon86);
imgic88 = getIcon(icon88);
imgic89 = getIcon(icon89);
+ imgic89_z3 = getIcon(icon89_z3);
imgic90 = getIcon(icon90);
imgic92 = getIcon(icon92);
imgic94 = getIcon(icon94);
diff --git a/src/main/resources/ui/util/dse_z3.png b/src/main/resources/ui/util/dse_z3.png
new file mode 100644
index 0000000000000000000000000000000000000000..9a6a70af8532cb69785839876f2f5e114a1e6ea1
Binary files /dev/null and b/src/main/resources/ui/util/dse_z3.png differ
diff --git a/tmltranslator/build.gradle b/tmltranslator/build.gradle
index 4346731a9719460a767df3c62d32662784a8e812..e03e31b7e47fe6f4b00ca9c441ea77a20a66d77a 100644
--- a/tmltranslator/build.gradle
+++ b/tmltranslator/build.gradle
@@ -25,6 +25,7 @@ dependencies {
compileOnly name:'batik-util'
compile name: 'commons-math3-3.6.1'
compile name: 'jautomata-core'
+ compile name: 'com.microsoft.z3'
}
jar {
diff --git a/tmltranslator/manifest.txt b/tmltranslator/manifest.txt
index 9c6dd6c3cc95d482fbb78a50590ce6ffd97da599..d0d5ac1d610e1fe17c8652d6d91e40dd1043071d 100755
--- a/tmltranslator/manifest.txt
+++ b/tmltranslator/manifest.txt
@@ -1 +1,2 @@
Main-Class: TMLTranslator
+Class-Path: com.microsoft.z3.jar
diff --git a/ttool-cli/build.gradle b/ttool-cli/build.gradle
index 61e6870757c78d21c9a29378dfcaf30ec37f7806..74cce3de0d81798f340a9ac6c2a9f70b1d5c975f 100644
--- a/ttool-cli/build.gradle
+++ b/ttool-cli/build.gradle
@@ -33,6 +33,7 @@ dependencies {
compile name: 'batik-dom'
compile name: 'batik-awt-util'
compile name: 'jautomata-core'
+ compile name: 'com.microsoft.z3'
// Use JUnit test framework
testCompile 'junit:junit:4.12'
diff --git a/ttool-cli/manifest.txt b/ttool-cli/manifest.txt
index cac8cac5cbd65fa321d0c6dc2a41fa415bb94f59..f71b884ab16c9a2e4c5597b71b45ab6d115fadd7 100755
--- a/ttool-cli/manifest.txt
+++ b/ttool-cli/manifest.txt
@@ -1,2 +1,2 @@
Main-Class: TToolCLI
-Class-Path:
+Class-Path: jsoup-1.8.1.jar commons-codec-1.10.jar gs-core-1.3.jar gs-ui-1.3.jar commons-io-2.5.jar commons-math3-3.6.1.jar batik-awt-util.jar batik-dom.jar batik-svggen.jar batik-util.jar batik-xml.jar jautomata-core.jar com.microsoft.z3.jar
diff --git a/ttool/META-INF/MANIFEST.MF b/ttool/META-INF/MANIFEST.MF
index 69ee18c82fcb07e48b000dd3570b52c519db03ad..c8d960fb4fde248bf284c6f813720ac087406387 100644
--- a/ttool/META-INF/MANIFEST.MF
+++ b/ttool/META-INF/MANIFEST.MF
@@ -1,4 +1,4 @@
Manifest-Version: 1.0
-Class-Path: jsoup-1.8.1.jar commons-codec-1.10.jar gs-core-1.3.jar gs-ui-1.3.jar commons-io-2.5.jar commons-math3-3.6.1.jar batik-awt-util.jar batik-dom.jar batik-svggen.jar batik-util.jar batik-xml.jar jautomata-core.jar
+Class-Path: jsoup-1.8.1.jar commons-codec-1.10.jar gs-core-1.3.jar gs-ui-1.3.jar commons-io-2.5.jar commons-math3-3.6.1.jar batik-awt-util.jar batik-dom.jar batik-svggen.jar batik-util.jar batik-xml.jar jautomata-core.jar com.microsoft.z3.jar
Main-Class: Main
diff --git a/ttool/build.gradle b/ttool/build.gradle
index da6aff06ccadf740793159657b6ef83a85f219df..a1346c22c42c058ae1695b081416d3febd83370d 100644
--- a/ttool/build.gradle
+++ b/ttool/build.gradle
@@ -33,6 +33,7 @@ dependencies {
compile name: 'batik-dom'
compile name: 'batik-awt-util'
compile name: 'jautomata-core'
+ compile name: 'com.microsoft.z3'
compile name: 'assertj/assertj-swing/3.8.0/assertj-swing-3.8.0'
compile name: 'assertj/assertj-swing/3.8.0/assertj-swing-3.8.0-sources'
compile name: 'assertj/assertj-swing-junit/3.8.0/assertj-swing-junit-3.8.0'
diff --git a/ttool/src/test/java/tmltranslator/dsez3engine/InputInstanceTest.java b/ttool/src/test/java/tmltranslator/dsez3engine/InputInstanceTest.java
new file mode 100644
index 0000000000000000000000000000000000000000..0dc2ccf6a8f6f58487fae6eaea92b02e0bc47b1f
--- /dev/null
+++ b/ttool/src/test/java/tmltranslator/dsez3engine/InputInstanceTest.java
@@ -0,0 +1,380 @@
+package tmltranslator.dsez3engine;
+
+import com.microsoft.z3.*;
+import org.junit.Assert;
+import org.junit.Before;
+import org.junit.Test;
+import tmltranslator.*;
+
+import java.util.ArrayList;
+import java.util.HashMap;
+import java.util.List;
+import myutil.TraceManager;
+
+import static org.junit.Assert.*;
+
+public class InputInstanceTest {
+
+ public TMLArchitecture tmla;
+ public TMLModeling tmlm;
+
+ public InputInstance inputInstance;
+
+ public OptimizationModel optimizationModel;
+
+ @Before
+ public void setUpTest() {
+
+ tmla = setUpTMLArchitecture();
+ tmlm = setUpTMLModeling();
+
+ inputInstance = new InputInstance(tmla, tmlm);
+
+ optimizationModel = new OptimizationModel(inputInstance);
+ }
+
+ private TMLModeling setUpTMLModeling() {
+
+ tmlm = new TMLModeling();
+
+
+ TMLTask taskA = new TMLTask("task__A", null, null);
+ TMLTask taskB = new TMLTask("task__B", null, null);
+ TMLTask taskD = new TMLTask("task__D", null, null);
+ TMLTask taskE = new TMLTask("task__E", null, null);
+
+ //filling activity diagrams of tasks
+
+ //taskA
+ TMLActivityElementWithAction firstA = new TMLExecI("execiA", null);
+ firstA.setAction("150");
+ taskA.getActivityDiagram().setFirst(firstA);
+
+ TMLActivityElement AwB = new TMLWriteChannel("AwB", null);
+ taskA.getActivityDiagram().addLinkElement(firstA, AwB);
+ taskA.getActivityDiagram().addElement(AwB);
+
+ TMLActivityElement AwD = new TMLWriteChannel("AwD", null);
+ taskA.getActivityDiagram().addLinkElement(AwB, AwD);
+ taskA.getActivityDiagram().addElement(AwD);
+
+ //taskB
+ TMLActivityElement firstB = new TMLReadChannel("BrA", null);
+ taskB.getActivityDiagram().setFirst(firstB);
+
+ TMLActivityElementWithAction execiB = new TMLExecI("execiB", null);
+ execiB.setAction("100");
+ taskB.getActivityDiagram().addLinkElement(firstB, execiB);
+ taskB.getActivityDiagram().addElement(execiB);
+
+ TMLActivityElement BwE = new TMLWriteChannel("BwE", null);
+ taskB.getActivityDiagram().addLinkElement(execiB, BwE);
+ taskB.getActivityDiagram().addElement(BwE);
+
+ //taskD
+ TMLActivityElement firstD = new TMLReadChannel("DrA", null);
+ taskD.getActivityDiagram().setFirst(firstD);
+
+ TMLActivityElementWithAction execiD = new TMLExecI("execiD", null);
+ execiD.setAction("100");
+ taskD.getActivityDiagram().addLinkElement(firstD, execiD);
+ taskD.getActivityDiagram().addElement(execiD);
+
+ TMLActivityElement DwE = new TMLWriteChannel("DwE", null);
+ taskD.getActivityDiagram().addLinkElement(execiD, DwE);
+ taskD.getActivityDiagram().addElement(DwE);
+
+ //taskE
+ TMLActivityElement firstE = new TMLReadChannel("ErB", null);
+ taskE.getActivityDiagram().setFirst(firstE);
+
+ TMLActivityElement ErD = new TMLReadChannel("ErD", null);
+ taskE.getActivityDiagram().addLinkElement(firstE, ErD);
+ taskE.getActivityDiagram().addElement(ErD);
+
+ TMLActivityElementWithAction execiE = new TMLExecI("execiE", null);
+ execiE.setAction("50");
+ taskE.getActivityDiagram().addLinkElement(ErD, execiE);
+ taskE.getActivityDiagram().addElement(execiE);
+
+
+ taskA.addOperation("generic");
+ taskB.addOperation("fft");
+ taskD.addOperation("fft");
+ taskE.addOperation("generic");
+
+ //creating channels
+ TMLChannel ab = new TMLChannel("ab", null);
+ TMLChannel ad = new TMLChannel("ad", null);
+ TMLChannel be = new TMLChannel("be", null);
+ TMLChannel de = new TMLChannel("de", null);
+
+ taskA.addWriteTMLChannel(ab);
+ taskA.addWriteTMLChannel(ad);
+
+ taskB.addReadTMLChannel(ab);
+ taskB.addWriteTMLChannel(be);
+
+ taskD.addReadTMLChannel(ad);
+ taskD.addWriteTMLChannel(de);
+
+ taskE.addReadTMLChannel(be);
+ taskE.addReadTMLChannel(de);
+
+ ab.setTasks(taskA, taskB);
+ ad.setTasks(taskA, taskD);
+ be.setTasks(taskB, taskE);
+ de.setTasks(taskD, taskE);
+
+ ab.setNumberOfSamples(2);
+ ad.setNumberOfSamples(2);
+ be.setNumberOfSamples(5);
+ de.setNumberOfSamples(5);
+
+ tmlm.addTask(taskA);
+ tmlm.addTask(taskB);
+ tmlm.addTask(taskD);
+ tmlm.addTask(taskE);
+
+ tmlm.addChannel(ab);
+ tmlm.addChannel(ad);
+ tmlm.addChannel(be);
+ tmlm.addChannel(de);
+
+
+ return tmlm;
+ }
+
+
+ private TMLArchitecture setUpTMLArchitecture() {
+
+ HwExecutionNode mainCPU = new HwCPU("MainCPU");
+ HwMemory mainMem = new HwMemory("mainMem");
+
+ HwExecutionNode dsp = new HwCPU("dsp");
+ HwMemory dspMem = new HwMemory("dspMem");
+
+ HwBus bus0 = new HwBus("bus0");
+ HwBus bus1 = new HwBus("bus1");
+
+
+ HwLink maincpu_bus0 = new HwLink("maincpu_bus0");
+ HwLink bus0_cpumem = new HwLink("bus0_cpumem");
+
+ HwLink dsp_bus1 = new HwLink("dsp_bus1");
+ HwLink bus1_dspmem = new HwLink("bus1_dspmem");
+
+ mainCPU.execiTime = 2;
+ dsp.execiTime = 1;
+
+
+ mainCPU.addOperationType("generic");
+ mainCPU.addOperationType("fft");
+
+ mainMem.memorySize = 200;
+
+ dsp.addOperationType("fft");
+ dspMem.memorySize = 100;
+
+ maincpu_bus0.hwnode = mainCPU;
+ maincpu_bus0.bus = bus0;
+
+ bus0_cpumem.bus = bus0;
+ bus0_cpumem.hwnode = mainMem;
+
+ dsp_bus1.hwnode = dsp;
+ dsp_bus1.bus = bus1;
+
+ bus1_dspmem.bus = bus1;
+ bus1_dspmem.hwnode = dspMem;
+
+
+ tmla = new TMLArchitecture();
+
+ tmla.addHwNode(mainCPU);
+ tmla.addHwNode(dsp);
+ tmla.addHwNode(mainMem);
+ tmla.addHwNode(dspMem);
+ tmla.addHwNode(bus0);
+ tmla.addHwNode(bus1);
+ tmla.addHwLink(maincpu_bus0);
+ tmla.addHwLink(bus0_cpumem);
+ tmla.addHwLink(dsp_bus1);
+ tmla.addHwLink(bus1_dspmem);
+
+ return tmla;
+ }
+
+ @Test
+ public void findOptimizedMapping() {
+
+ try {
+
+ // These examples need model generation turned on.
+ HashMap<String, String> cfg = new HashMap<String, String>();
+ cfg.put("model", "true");
+ Context ctx = new Context(cfg);
+
+
+ optimizationModel.findOptimizedMapping(ctx);
+
+ Log.close();
+ if (Log.isOpen())
+ TraceManager.addDev("Log is still open!");
+ } catch (Z3Exception ex) {
+ TraceManager.addDev("Z3 Managed Exception: " + ex.getMessage());
+ TraceManager.addDev("Stack trace: ");
+ ex.printStackTrace(
+ System.out);
+ } catch (OptimizationModel.TestFailedException ex) {
+ TraceManager.addDev("TEST CASE FAILED: " + ex.getMessage());
+ TraceManager.addDev("Stack trace: ");
+ ex.printStackTrace(System.out);
+ } catch (Exception ex) {
+ TraceManager.addDev("Unknown Exception: " + ex.getMessage());
+ TraceManager.addDev("Stack trace: ");
+ ex.printStackTrace(System.out);
+ }
+
+ assertEquals(1, optimizationModel.getOptimizedSolutionX().get("X[task__A][MainCPU] = ").intValue());
+ assertEquals(0, optimizationModel.getOptimizedSolutionX().get("X[task__A][dsp] = ").intValue());
+ assertEquals(0, optimizationModel.getOptimizedSolutionX().get("X[task__B][MainCPU] = ").intValue());
+ assertEquals(1, optimizationModel.getOptimizedSolutionX().get("X[task__B][dsp] = ").intValue());
+ assertEquals(0, optimizationModel.getOptimizedSolutionX().get("X[task__D][MainCPU] = ").intValue());
+ assertEquals(1, optimizationModel.getOptimizedSolutionX().get("X[task__D][dsp] = ").intValue());
+ assertEquals(1, optimizationModel.getOptimizedSolutionX().get("X[task__E][MainCPU] = ").intValue());
+ assertEquals(0, optimizationModel.getOptimizedSolutionX().get("X[task__E][dsp] = ").intValue());
+
+ assertEquals(0, optimizationModel.getOptimizedSolutionStart().get("start[task__A] = ").intValue());
+ assertEquals(300, optimizationModel.getOptimizedSolutionStart().get("start[task__B] = ").intValue());
+ assertEquals(400, optimizationModel.getOptimizedSolutionStart().get("start[task__D] = ").intValue());
+ assertEquals(500, optimizationModel.getOptimizedSolutionStart().get("start[task__E] = ").intValue());
+
+ }
+
+
+ @Test
+ public void findFeasibleMapping() {
+
+ try {
+
+ // These examples need model generation turned on.
+ HashMap<String, String> cfg = new HashMap<String, String>();
+ cfg.put("model", "true");
+ Context ctx = new Context(cfg);
+
+
+ optimizationModel.findFeasibleMapping(ctx);
+
+ Log.close();
+ if (Log.isOpen())
+ TraceManager.addDev("Log is still open!");
+ } catch (Z3Exception ex) {
+ TraceManager.addDev("Z3 Managed Exception: " + ex.getMessage());
+ TraceManager.addDev("Stack trace: ");
+ ex.printStackTrace(
+ System.out);
+ } catch (OptimizationModel.TestFailedException ex) {
+ TraceManager.addDev("TEST CASE FAILED: " + ex.getMessage());
+ TraceManager.addDev("Stack trace: ");
+ ex.printStackTrace(System.out);
+ } catch (Exception ex) {
+ TraceManager.addDev("Unknown Exception: " + ex.getMessage());
+ TraceManager.addDev("Stack trace: ");
+ ex.printStackTrace(System.out);
+ }
+
+
+ }
+
+
+ @Test
+ public void getFeasibleCPUs() {
+
+ Boolean test = false;
+ List <HwExecutionNode> expectedList = new ArrayList<>();
+ expectedList.add(inputInstance.getArchitecture().getHwCPUByName("MainCPU"));
+ expectedList.add(inputInstance.getArchitecture().getHwCPUByName("dsp"));
+
+ TMLTask tempTask = (TMLTask) inputInstance.getModeling().getTasks().get(2);
+
+
+ List<HwExecutionNode> actualList = new ArrayList<>();
+
+ for (int i = 0; i < inputInstance.getFeasibleCPUs(tempTask).size(); i++) {
+ actualList.add(inputInstance.getFeasibleCPUs(tempTask).get(i));
+ }
+
+ assertEquals(actualList.size(), expectedList.size());
+
+ for (HwExecutionNode hwExecutionNode : actualList){
+ assertTrue(expectedList.contains(hwExecutionNode));
+ }
+
+ }
+
+ @Test
+ public void getBufferIn() {
+
+ List<TMLTask> tempTasks = new ArrayList<>();
+ for (int i = 0; i < inputInstance.getModeling().getTasks().size(); i++) {
+ tempTasks.add((TMLTask) inputInstance.getModeling().getTasks().get(i));
+ }
+
+ assertEquals(inputInstance.getBufferIn((TMLTask) tempTasks.get(0)), 0);
+ assertEquals(inputInstance.getBufferIn((TMLTask) tempTasks.get(1)), 2);
+ assertEquals(inputInstance.getBufferIn((TMLTask) tempTasks.get(2)), 2);
+ assertEquals(inputInstance.getBufferIn((TMLTask) tempTasks.get(3)), 10);
+
+
+ }
+
+ @Test
+ public void getBufferOut() {
+ List<TMLTask> tempTasks = new ArrayList<>();
+ for (int i = 0; i < inputInstance.getModeling().getTasks().size(); i++) {
+ tempTasks.add((TMLTask) inputInstance.getModeling().getTasks().get(i));
+ }
+
+ assertEquals(inputInstance.getBufferOut((TMLTask) tempTasks.get(0)), 4);
+ assertEquals(inputInstance.getBufferOut((TMLTask) tempTasks.get(1)), 5);
+ assertEquals(inputInstance.getBufferOut((TMLTask) tempTasks.get(2)), 5);
+ assertEquals(inputInstance.getBufferOut((TMLTask) tempTasks.get(3)), 0);
+
+ }
+
+
+ @Test
+ public void getLocalMemoryOfHwExecutionNode() {
+
+ HwNode output1 = inputInstance.getArchitecture().getHwMemoryByName("mainMem");
+ HwNode output2 = inputInstance.getArchitecture().getHwMemoryByName("dspMem");
+
+ assertTrue("comparing between the expected local memory for main_CPU and the memory found", inputInstance.getLocalMemoryOfHwExecutionNode(inputInstance.getArchitecture().getHwNodeByName("MainCPU")) == output1);
+ assertTrue("comparing between the expected local memory for DSP and the memory found", inputInstance.getLocalMemoryOfHwExecutionNode(inputInstance.getArchitecture().getHwNodeByName("dsp")) == output2);
+
+ }
+
+
+ @Test
+ public void getWCET() {
+ //a temporary list of the tasks
+ List<TMLTask> tempTasks = new ArrayList<>();
+ for (int i = 0; i < inputInstance.getModeling().getTasks().size(); i++) {
+ tempTasks.add((TMLTask) inputInstance.getModeling().getTasks().get(i));
+ }
+ int expectedWcetA_CPU = 300;
+ int expectedWcetA_dsp = 150;
+
+ assertEquals("comparing between the expected WCET of task A on main_CPU and the computed value", expectedWcetA_CPU, inputInstance.getWCET(tempTasks.get(0), (HwExecutionNode) inputInstance.getArchitecture().getHwNodeByName("MainCPU")));
+ assertEquals("comparing between the expected WCET of task A on DSP and the computed value", expectedWcetA_dsp, inputInstance.getWCET(tempTasks.get(0), (HwExecutionNode) inputInstance.getArchitecture().getHwNodeByName("dsp")));
+
+ }
+
+
+ @Test
+ public void getFinalTask() {
+ assertEquals("checking the last task", inputInstance.getModeling().getTMLTaskByName("task__E"), inputInstance.getFinalTask(inputInstance.getModeling()));
+
+ }
+}
\ No newline at end of file
diff --git a/ttool/ttool.txt b/ttool/ttool.txt
index 10097015927284921e727b51a256033bd3248606..6def7b20843c61978d1caedc95357eebb43d3759 100755
--- a/ttool/ttool.txt
+++ b/ttool/ttool.txt
@@ -1,2 +1,2 @@
Main-Class: Main
-Class-Path: ./opencloud.jar ./JavaPlot.jar ./derbynet.jar ./commons-math3-3.6.1.jar ./jsoup-1.8.1.jar ./commons-codec-1.10.jar ./gs-core-1.3.jar ./gs-ui-1.3.jar ./commons-io-2.5.jar ./batik-awt-util.jar ./batik-dom.jar ./batik-svggen.jar ./batik-util.jar ./batik-xml.jar ./jautomata-core.jar
+Class-Path: ./opencloud.jar ./JavaPlot.jar ./derbynet.jar ./commons-math3-3.6.1.jar ./jsoup-1.8.1.jar ./commons-codec-1.10.jar ./gs-core-1.3.jar ./gs-ui-1.3.jar ./commons-io-2.5.jar ./batik-awt-util.jar ./batik-dom.jar ./batik-svggen.jar ./batik-util.jar ./batik-xml.jar ./jautomata-core.jar ./com.microsoft.z3.jar