From c0d84c87911ad534b3c128cb9048abda791fa489 Mon Sep 17 00:00:00 2001
From: apvrille <ludovic.apvrille@eurecom.fr>
Date: Wed, 27 Feb 2019 12:29:48 +0100
Subject: [PATCH] Adding optimization result: dialog window
---
src/main/java/ui/window/JDialogDSEZ3.java | 440 ++++++++++++++++++++++
1 file changed, 440 insertions(+)
create mode 100644 src/main/java/ui/window/JDialogDSEZ3.java
diff --git a/src/main/java/ui/window/JDialogDSEZ3.java b/src/main/java/ui/window/JDialogDSEZ3.java
new file mode 100644
index 0000000000..3d75afdaf4
--- /dev/null
+++ b/src/main/java/ui/window/JDialogDSEZ3.java
@@ -0,0 +1,440 @@
+/* Copyright or (C) or Copr. GET / ENST, Telecom-Paris, Ludovic Apvrille
+ *
+ * ludovic.apvrille AT enst.fr
+ *
+ * This software is a computer program whose purpose is to allow the
+ * edition of TURTLE analysis, design and deployment diagrams, to
+ * allow the generation of RT-LOTOS or Java code from this diagram,
+ * and at last to allow the analysis of formal validation traces
+ * obtained from external tools, e.g. RTL from LAAS-CNRS and CADP
+ * from INRIA Rhone-Alpes.
+ *
+ * This software is governed by the CeCILL license under French law and
+ * abiding by the rules of distribution of free software. You can use,
+ * modify and/ or redistribute the software under the terms of the CeCILL
+ * license as circulated by CEA, CNRS and INRIA at the following URL
+ * "http://www.cecill.info".
+ *
+ * As a counterpart to the access to the source code and rights to copy,
+ * modify and redistribute granted by the license, users are provided only
+ * with a limited warranty and the software's author, the holder of the
+ * economic rights, and the successive licensors have only limited
+ * liability.
+ *
+ * In this respect, the user's attention is drawn to the risks associated
+ * with loading, using, modifying and/or developing or reproducing the
+ * software by the user in light of its specific status of free software,
+ * that may mean that it is complicated to manipulate, and that also
+ * therefore means that it is reserved for developers and experienced
+ * professionals having in-depth computer knowledge. Users are therefore
+ * encouraged to load and test the software's suitability as regards their
+ * requirements in conditions enabling the security of their systems and/or
+ * data to be ensured and, more generally, to use and operate it in the
+ * same conditions as regards security.
+ *
+ * The fact that you are presently reading this means that you have had
+ * knowledge of the CeCILL license and that you accept its terms.
+ */
+
+
+package ui.window;
+
+import common.ConfigurationTTool;
+import common.SpecConfigTTool;
+import dseengine.DSEConfiguration;
+import launcher.LauncherException;
+import launcher.RshClient;
+import myutil.GraphicLib;
+import myutil.ScrolledJTextArea;
+import myutil.TraceManager;
+import tmltranslator.TMLMapping;
+import tmltranslator.TMLModeling;
+import tmltranslator.dsez3engine.InputInstance;
+import tmltranslator.dsez3engine.OptimizationModel;
+import tmltranslator.dsez3engine.OptimizationResult;
+import ui.util.IconManager;
+import ui.MainGUI;
+
+import javax.swing.*;
+import javax.swing.event.DocumentListener;
+import javax.swing.event.DocumentEvent;
+import javax.swing.event.ListSelectionEvent;
+import javax.swing.event.ListSelectionListener;
+import java.awt.*;
+import java.awt.event.ActionEvent;
+import java.awt.event.ActionListener;
+import java.util.*;
+
+
+import com.microsoft.z3.*;
+import tmltranslator.*;
+
+import java.util.ArrayList;
+import java.util.HashMap;
+import java.util.List;
+import myutil.TraceManager;
+
+
+/**
+ * Class JDialogDSE
+ * Dialog for managing DSE with Z3
+ * Creation: 26/02/2019
+ *
+ * @author Ludovic APVRILLE
+ * @version 1.0 26/02/2019
+ */
+public class JDialogDSEZ3 extends JDialog implements ActionListener, ListSelectionListener, Runnable {
+
+ protected MainGUI mgui;
+
+
+ protected final static int NOT_SELECTED = 0;
+ protected final static int NOT_STARTED = 1;
+ protected final static int STARTED = 2;
+ protected final static int STOPPED = 3;
+ int mode;
+
+
+
+ protected JButton start;
+ protected JButton stop;
+ protected JButton close;
+
+ protected JTextArea outputText;
+ protected String output = "";
+
+ protected String TMLDirectory;
+
+
+ private Thread t;
+ private boolean go = false;
+
+
+ protected RshClient rshc;
+
+ private TMLMapping map;
+ private InputInstance inputInstance;
+ private OptimizationModel optimizationModel;
+
+
+ /*
+ * Creates new form
+ */
+ public JDialogDSEZ3(Frame f, MainGUI _mgui, String title, TMLMapping map, String dir) {
+ super(f, title, true);
+
+ mgui = _mgui;
+ TMLDirectory = dir + "/";
+
+ this.map = map;
+
+ initComponents();
+ myInitComponents();
+
+ pack();
+
+
+ //getGlassPane().addMouseListener( new MouseAdapter() {});
+ getGlassPane().setCursor(Cursor.getPredefinedCursor(Cursor.WAIT_CURSOR));
+ }
+
+ protected void myInitComponents() {
+ mode = NOT_STARTED;
+ setButtons();
+ handleStartButton();
+ }
+
+ protected void initComponents() {
+
+ Container c = getContentPane();
+ setFont(new Font("Helvetica", Font.PLAIN, 14));
+ c.setLayout(new BorderLayout());
+
+
+
+ JPanel jp03 = new JPanel();
+ GridBagLayout gridbag03 = new GridBagLayout();
+ GridBagConstraints c03 = new GridBagConstraints();
+ jp03.setLayout(gridbag03);
+ jp03.setBorder(new javax.swing.border.TitledBorder("DSE Options"));
+ c03.weighty = 1.0;
+ c03.weightx = 1.0;
+ c03.gridwidth = GridBagConstraints.REMAINDER; //end row
+ c03.fill = GridBagConstraints.BOTH;
+ c03.gridheight = 1;
+
+
+
+
+ JPanel jp04 = new JPanel();
+
+ GridBagLayout gridbag04 = new GridBagLayout();
+ GridBagConstraints c04 = new GridBagConstraints();
+ jp04.setLayout(gridbag04);
+
+ c04.weighty = 1.0;
+ c04.weightx = 1.0;
+ c04.gridwidth = GridBagConstraints.REMAINDER; //end row
+ c04.fill = GridBagConstraints.BOTH;
+ c04.gridheight = 1;
+
+ //jp04.setBorder(new javax.swing.border.TitledBorder("DSE Output"));
+ //jp04.add(new JLabel("Design Space Exploration Output"), c04);
+
+
+ outputText = new ScrolledJTextArea();
+ outputText.setEditable(false);
+ outputText.setMargin(new Insets(10, 10, 10, 10));
+ outputText.setTabSize(3);
+ outputText.append("How to start?" +
+ "\n - Simply click on start ^^\n");
+ JScrollPane jsp = new JScrollPane(outputText, JScrollPane.VERTICAL_SCROLLBAR_ALWAYS,
+ JScrollPane.HORIZONTAL_SCROLLBAR_ALWAYS);
+ jsp.setPreferredSize(new Dimension(300, 300));
+ Font f = new Font("Courrier", Font.BOLD, 12);
+ outputText.setFont(f);
+ jp04.add(jsp, c04);
+ //jp1.add("Results", jp04);
+
+ c.add(jp03, BorderLayout.NORTH);
+ c.add(jp04, BorderLayout.CENTER);
+
+ start = new JButton("Start", IconManager.imgic53);
+ stop = new JButton("Stop", IconManager.imgic55);
+ close = new JButton("Close", IconManager.imgic27);
+
+
+ start.setPreferredSize(new Dimension(100, 30));
+ stop.setPreferredSize(new Dimension(100, 30));
+ close.setPreferredSize(new Dimension(120, 30));
+
+
+ start.addActionListener(this);
+ stop.addActionListener(this);
+ close.addActionListener(this);
+
+ JPanel jp2 = new JPanel();
+
+ jp2.add(start);
+ jp2.add(stop);
+ jp2.add(close);
+
+
+ c.add(jp2, BorderLayout.SOUTH);
+
+
+ }
+
+
+
+ private void handleStartButton() {
+ //TraceManager.addDev("Handle start button");
+
+ /*boolean b = dseButton.isSelected() || dseButtonFromFile.isSelected();
+ nbOfMappings.setEnabled(b);
+ infoNbOfMappings.setEnabled(b);
+ randomMappingBox.setEnabled(b);
+ randomMappingNb.setEnabled(b);
+ outputTML.setEnabled(b);
+ outputGUI.setEnabled(b);*/
+ //dseOptions.repaint();
+
+ if (mode != NOT_STARTED && mode != NOT_SELECTED) {
+ return;
+ }
+
+
+ setButtons();
+
+ }
+
+ public void valueChanged(ListSelectionEvent e) {
+ }
+
+
+ public void actionPerformed(ActionEvent evt) {
+
+ if (evt.getSource() == start) {
+ startProcess();
+ } else if (evt.getSource() == stop) {
+ stopProcess();
+ } else if (evt.getSource() == close) {
+ closeDialog();
+ }
+ }
+
+
+
+
+ public void closeDialog() {
+ if (mode == STARTED) {
+ stopProcess();
+ }
+ dispose();
+ }
+
+ public void stopProcess() {
+ mode = STOPPED;
+ setButtons();
+ go = false;
+
+ }
+
+
+ public void startProcess() {
+ t = new Thread(this);
+ mode = STARTED;
+ setButtons();
+ go = true;
+ t.start();
+ }
+ //
+ // private void testGo() throws InterruptedException {
+ // if (go == false) {
+ // throw new InterruptedException("Stopped by user");
+ // }
+ // }
+
+ public void run() {
+ // String cmd;
+ // String list, data;
+ // int cycle = 0;
+ output = "";
+
+ // hasError = false;
+ //try {
+
+
+ TraceManager.addDev("Thread started");
+ outputText.append("\nPreparing input model for Z3\n");
+ // File testFile;
+ TMLArchitecture tmla = map.getTMLArchitecture();
+ TMLModeling tmlm = map.getTMLModeling();
+
+ inputInstance = new InputInstance(tmla, tmlm);
+ optimizationModel = new OptimizationModel(inputInstance);
+
+
+ outputText.append("Loading Z3 libs\n");
+ String error = loadZ3Libs();
+
+ if (error != null) {
+ outputText.append(error);
+ stopProcess();
+ return;
+ }
+
+
+
+ /*try {
+ System.load("/opt/z3/bin/libz3.so");
+ System.load("/opt/z3/bin/libz3java.so");
+ } catch (UnsatisfiedLinkError e) {
+ outputText.append("Z3 lib could not be loaded\n");
+ stopProcess();
+ return;
+ }*/
+
+ outputText.append("Z3 libs loaded.\n");
+
+
+ Context ctx = null;
+ outputText.append("Looking for optimized mapping, please wait\n");
+ OptimizationResult result = null;
+ try {
+ result = optimizationModel.findOptimizedMapping();
+ } catch (Exception e) {
+ outputText.append("Exception during Z3 execution\nBadly installed?\n");
+ }
+
+ if (result == null) {
+ outputText.append("ERROR: an unknown error occured");
+ } else {
+ if (result.hasError()) {
+ outputText.append("ERROR: " + result.error);
+ } else {
+ if (result.mappingFound) {
+ outputText.append("Optimized mapping found");
+ } else {
+ outputText.append("No suitable mapping could be found");
+ }
+ }
+ }
+ stopProcess();
+
+ }
+
+ // Returns an error string in case of failure
+ private String loadZ3Libs() {
+ if ((ConfigurationTTool.Z3LIBS == null) || (ConfigurationTTool.Z3LIBS.length() == 0)) {
+ return "Z3 libraries not configured.\n Set them in configuration file (e.g. config.xml)\n" +
+ "For instance:\n<Z3LIBS data=\"/opt/z3/bin/libz3.so:/opt/z3/bin/libz3java.so\" />\n";
+ }
+
+ try {
+ String [] libs = ConfigurationTTool.Z3LIBS.split(":");
+ for (int i=0; i<libs.length; i++) {
+ String tmp = libs[i].trim();
+ if (tmp.length() > 0) {
+ TraceManager.addDev("Loading Z3 lib: " + tmp);
+ System.load(tmp);
+ }
+ }
+
+ } catch (UnsatisfiedLinkError e) {
+ return ("Z3 libs + " + ConfigurationTTool.Z3LIBS + " could not be loaded\n");
+ }
+
+ return null;
+ }
+
+
+
+ protected void checkMode() {
+ mode = NOT_SELECTED;
+ }
+
+ protected void setButtons() {
+ switch (mode) {
+ case NOT_SELECTED:
+ start.setEnabled(false);
+ stop.setEnabled(false);
+ close.setEnabled(true);
+ //setCursor(CursoretPredefinedCursor(Cursor.DEFAULT_CURSOR));
+ getGlassPane().setVisible(false);
+ break;
+ case NOT_STARTED:
+ start.setEnabled(true);
+ stop.setEnabled(false);
+ close.setEnabled(true);
+ //setCursor(Cursor.getPredefinedCursor(Cursor.DEFAULT_CURSOR));
+ getGlassPane().setVisible(false);
+ break;
+ case STARTED:
+ start.setEnabled(false);
+ stop.setEnabled(true);
+ close.setEnabled(false);
+ getGlassPane().setVisible(true);
+ //setCursor(Cursor.getPredefinedCursor(Cursor.WAIT_CURSOR));
+ break;
+ case STOPPED:
+ default:
+ start.setEnabled(false);
+ stop.setEnabled(false);
+ close.setEnabled(true);
+ getGlassPane().setVisible(false);
+ break;
+ }
+ }
+
+
+
+ public boolean hasToContinue() {
+ return (go == true);
+ }
+ //
+ // public void setError() {
+ // hasError = true;
+ // }
+ //
+}
--
GitLab