From c2ff5542ca8b3e86cd0f9b3aaa5b2a8ea25e366c Mon Sep 17 00:00:00 2001
From: apvrille <ludovic.apvrille@eurecom.fr>
Date: Wed, 27 Feb 2019 12:28:19 +0100
Subject: [PATCH] Adding optimization result
---
src/main/java/common/ConfigurationTTool.java | 19 +++++
.../dsez3engine/OptimizationResult.java | 73 +++++++++++++++++++
2 files changed, 92 insertions(+)
create mode 100644 src/main/java/tmltranslator/dsez3engine/OptimizationResult.java
diff --git a/src/main/java/common/ConfigurationTTool.java b/src/main/java/common/ConfigurationTTool.java
index 5838c938ae..89ee128948 100755
--- a/src/main/java/common/ConfigurationTTool.java
+++ b/src/main/java/common/ConfigurationTTool.java
@@ -141,6 +141,9 @@ public class ConfigurationTTool {
public static String AVATARExecutableSoclibCodeTraceCommand = "";
public static String AVATARExecutableSoclibTraceFile = "";
+ // Z3
+ public static String Z3LIBS = "";
+
// Ontology
//public static String RequirementOntologyWebsite = "";
@@ -432,6 +435,9 @@ public class ConfigurationTTool {
sb.append("AVATARExecutableSocLibCodeTraceCommand: " + AVATARExecutableSoclibCodeTraceCommand + "\n");
sb.append("AVATARExecutableSocLibCodeTraceFile: " + AVATARExecutableSoclibTraceFile + "\n");
+ sb.append("\nZ3 Libs:\n");
+ sb.append("Z3LIBS: " + Z3LIBS + "\n");
+
sb.append("\nProVerif:\n");
sb.append("ProVerifCodeDirectory: " + ProVerifCodeDirectory + "\n");
sb.append("ProVerifVerifierPATH: " + ProVerifVerifierPath + "\n");
@@ -707,6 +713,10 @@ public class ConfigurationTTool {
if (nl.getLength() > 0)
AVATARExecutableSoclibTraceFile(nl);
+ nl = doc.getElementsByTagName("Z3LIBS");
+ if (nl.getLength() > 0)
+ Z3LIBS(nl);
+
if (systemcOn) {
nl = doc.getElementsByTagName("SystemCHost");
if (nl.getLength() > 0)
@@ -1441,6 +1451,15 @@ public class ConfigurationTTool {
}
}
+ private static void Z3LIBS(NodeList nl) throws MalformedConfigurationException {
+ try {
+ Element elt = (Element) (nl.item(0));
+ Z3LIBS = elt.getAttribute("data");
+ } catch (Exception e) {
+ throw new MalformedConfigurationException(e.getMessage());
+ }
+ }
+
private static void ProVerifCodeDirectory(NodeList nl) throws MalformedConfigurationException {
try {
Element elt = (Element) (nl.item(0));
diff --git a/src/main/java/tmltranslator/dsez3engine/OptimizationResult.java b/src/main/java/tmltranslator/dsez3engine/OptimizationResult.java
new file mode 100644
index 0000000000..559411200e
--- /dev/null
+++ b/src/main/java/tmltranslator/dsez3engine/OptimizationResult.java
@@ -0,0 +1,73 @@
+/* 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 tmltranslator.dsez3engine;
+
+import tmltranslator.*;
+
+import java.util.ArrayList;
+import java.util.List;
+
+/**
+ * Class OptimizationResult
+ * Object for manipulating results generated by Z3
+ * Creation: 26/02/2019
+ *
+ * @author Ludovic APVRILLE
+ * @version 1.0 27/02/2019
+ */
+
+public class OptimizationResult {
+
+ public String result = "";
+ public boolean mappingFound = false;
+ public String error = null;
+
+ public OptimizationResult() {
+ }
+
+ public boolean hasError() {
+ return error != null;
+ }
+
+ public boolean mappingfound() {
+ return mappingFound;
+ }
+
+
+}
--
GitLab