From d68a3752185b4ef3a23b772b4eb2661d9f41fd8f Mon Sep 17 00:00:00 2001
From: apvrille <ludovic.apvrille@eurecom.fr>
Date: Tue, 26 Feb 2019 16:28:49 +0100
Subject: [PATCH] Adding DSE Z3 icon and button. Can be used only with
experimental option on
---
rundse/build.gradle | 1 +
rundse/manifest.txt | 1 +
src/main/java/ui/ActionPerformer.java | 4 ++++
src/main/java/ui/JToolBarMainTurtle.java | 9 ++++++++-
src/main/java/ui/MainGUI.java | 9 +++++++++
src/main/java/ui/ModeManager.java | 4 ++++
src/main/java/ui/TGUIAction.java | 7 +++++--
src/main/java/ui/util/IconManager.java | 4 +++-
src/main/resources/ui/util/dse_z3.png | Bin 0 -> 702 bytes
tmltranslator/build.gradle | 1 +
tmltranslator/manifest.txt | 1 +
11 files changed, 37 insertions(+), 4 deletions(-)
create mode 100644 src/main/resources/ui/util/dse_z3.png
diff --git a/rundse/build.gradle b/rundse/build.gradle
index 49bc159bc6..ed941fa63f 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 18e66503cd..7ae7016992 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/ui/ActionPerformer.java b/src/main/java/ui/ActionPerformer.java
index 18d5b9846f..28bb9705c0 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 c926eb9a10..69dc3d24ac 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 277aad5242..95e6711332 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 d771aec826..37712ad69d 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 2b4bfd066b..6defdce51b 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/IconManager.java b/src/main/java/ui/util/IconManager.java
index d856395884..0a0a2f1a82 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
GIT binary patch
literal 702
zcmeAS@N?(olHy`uVBq!ia0y~yU=RRd4mJh`2Kmqb6B!s7*pj^6T^Rm@;DWu&Co?cG
za29w(7Bet#3xhBt!>l<H3=9nHC7!;n?2nnG_&H2_!t@v!7?`|0T^vI!PPYcdX9OjR
z{I7gpHht#Q?8S<$)tgiJ_ikC!zDU8OYQlmmw(L9GpLt(6JTHr-IwR)P(X;GR9e)-m
zuI7!Z=4feaZK`~^>Pr&Oe;#3{FR3vG{`%j!?@r;X`A~T7eR<vf&$a9f0{zD;|EO=e
zxn^zH>b-tTgFG3SP8V;|i9VB7tT_F2thC#`J9lhyHb(5rnDvam{jmO}mtP__M({8(
zJpcT2*4wh`qgh+`3A=uLvw&^ZvYV`q8<<|OFfrcC+rIx{<v+z@Cx(v4JJc9HRoHB{
z>SuVfscL78TG@L`8)l{ho?#JjadylLSRWkv^=p@J=+(JCYR(KAGkvxtZM+da{d6g-
zt(T6U1W#L-joklz@xFmm^cWsh-eXJHQhsC~8$(_7-neuXA<Y)2g{$trS7#96U<qUI
zxo|yUlIWs~FQzQgSlZjm>$Ruq+=1lZM}El&G{iHUcw2TpL~AP3Y5zX?MMta8P5PAb
z<b(nHe<zWnonA{9mF<o__55@Fv%LE?-yRx%-?w|SL)61}{qrXo6gP<Qu(3u?d%kV^
zc3Wl<w{Oqw^k(^eH@$J|R@JQxlc29vbFJq3MTLeI?Y`@6_0Xb$^S<iAs0ls13|p4}
zSoy82inF2d?T_s)N*7g>f<mV<+_`u%*sA00UQUL<(s|!R?4LgU%+0{yIZ3GJPLA1S
ztDB4s%mpF`Hr^BDnly2Rm48%i=<h8?rIHLiyFP8<n{{<<|BF+Lf1Q$IywDuI?DbO9
z<lax=FN-s3dTm=75A-VDFHtDJm}vL))4rDzFDF`k7jIM2>Uo@aJf4Apfx*+&&t;uc
GLK6TVEIG{p
literal 0
HcmV?d00001
diff --git a/tmltranslator/build.gradle b/tmltranslator/build.gradle
index 4346731a97..e03e31b7e4 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 9c6dd6c3cc..d0d5ac1d61 100755
--- a/tmltranslator/manifest.txt
+++ b/tmltranslator/manifest.txt
@@ -1 +1,2 @@
Main-Class: TMLTranslator
+Class-Path: com.microsoft.z3.jar
--
GitLab