diff --git a/src/main/java/help/HelpEntry.java b/src/main/java/help/HelpEntry.java
index efdd84c0a32f84e0531245bd66114bb769dfd042..975397df937f837f4b2cb654dd50dfd7ebc6a7d2 100644
--- a/src/main/java/help/HelpEntry.java
+++ b/src/main/java/help/HelpEntry.java
@@ -60,14 +60,14 @@ import java.util.stream.Collectors;
*/
public class HelpEntry implements GenericTree {
- public HelpEntry linkToParent;
- Vector<HelpEntry> entries;
+ protected HelpEntry linkToParent;
+ protected Vector<HelpEntry> entries;
- public String masterKeyword;
- public String[] keywords;
+ protected String masterKeyword;
+ protected String[] keywords;
- public String pathToHTMLFile;
- public String htmlContent;
+ protected String pathToHTMLFile;
+ protected String htmlContent;
public HelpEntry() {
@@ -103,6 +103,9 @@ public class HelpEntry implements GenericTree {
return true;
}
+
+
+
public String getToolTip() {
if (keywords == null) {
return "";
@@ -295,8 +298,43 @@ public class HelpEntry implements GenericTree {
return false;
}
+ public String getKeywords() {
+ String ret = "";
+ if (keywords != null) {
+ for (int i = 0; i < keywords.length; i++) {
+ ret += keywords[i] + " ";
+ }
+ }
+ return ret;
+ }
+
+
+ public String getKidsInHTML() {
+ String s = "";
+
+ if (entries != null) {
+ for (HelpEntry he : entries) {
+ s += "<li> ";
+ s += "<a href=\"file://" + he.getMasterKeyword() + ".html\"/>" + he.getMasterKeyword() + "</a> " +
+ he.getKeywords();
+ s += " </li>\n<br>\n";
+ }
+ }
+ return s;
+ }
+ public void search(String [] words, HelpEntry father) {
+ if (hasSimilarWords(words) > 0) {
+ father.addKid(this);
+ }
+
+ if (entries != null) {
+ for (HelpEntry he: entries) {
+ he.search(words, father);
+ }
+ }
+ }
diff --git a/src/main/java/help/SearchResultHelpEntry.java b/src/main/java/help/SearchResultHelpEntry.java
new file mode 100644
index 0000000000000000000000000000000000000000..8ffc26aba03a8a232a0ae0d000b3cb14934cf8c6
--- /dev/null
+++ b/src/main/java/help/SearchResultHelpEntry.java
@@ -0,0 +1,83 @@
+/* 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 help;
+
+import myutil.GenericTree;
+import myutil.TraceManager;
+
+import java.io.BufferedReader;
+import java.io.InputStreamReader;
+import java.net.URL;
+import java.net.URLConnection;
+import java.nio.charset.StandardCharsets;
+import java.util.Vector;
+import java.util.stream.Collectors;
+
+
+/**
+ * Class SearchResultHelpEntry
+ * Creation: 07/03/2019
+ * Version 1.0 07/03/2019
+ *
+ * @author Ludovic APVRILLE
+ */
+public class SearchResultHelpEntry extends HelpEntry {
+ public static String SEARCH_HEADER = "<h1>Search result</h1>\n<br>\n";
+
+ public SearchResultHelpEntry() {
+
+ }
+
+ @Override
+ public String getHTMLContent() {
+ String ret = super.getHTMLContent();
+ String kids = getKidsInHTML();
+ int index1 = ret.indexOf("<body>");
+ if (index1 > -1) {
+ index1 += 6;
+ ret = ret.substring(0, index1) + "\n" + SEARCH_HEADER + getNbOfKids() + " result(s) found:<br>\n" +
+ kids + ret.substring(index1+1, ret.length());
+ }
+
+ TraceManager.addDev("Resulting HTML of search:" + ret);
+
+ return ret;
+ }
+}
diff --git a/src/main/java/tmltranslator/TMLMapping.java b/src/main/java/tmltranslator/TMLMapping.java
index 6de053f010d854c4b7b2ed27cd793a07e4d0d799..9df568cb56594594c4c3f191219f2ae6632300df 100755
--- a/src/main/java/tmltranslator/TMLMapping.java
+++ b/src/main/java/tmltranslator/TMLMapping.java
@@ -792,9 +792,6 @@ public class TMLMapping<E> {
return list;
}
- public TMLMapping cloneMappingArchitecture() {
- return null;
- }
public int getArchitectureComplexity() {
if (tmla == null) {
diff --git a/src/main/java/tmltranslator/dsez3engine/OptimizationModel.java b/src/main/java/tmltranslator/dsez3engine/OptimizationModel.java
index 45641eafa1a12c18dee224c929047e1dd8e3e655..26e3b03bd5ccf2bc5744bc91c09288af45fddafe 100644
--- a/src/main/java/tmltranslator/dsez3engine/OptimizationModel.java
+++ b/src/main/java/tmltranslator/dsez3engine/OptimizationModel.java
@@ -847,6 +847,7 @@ public class OptimizationModel {
TraceManager.addDev(outputToDisplay);
result.mappingFound = true;
+ result.resultingMapping = tmlMapping;
} else {
outputToDisplay ="No suitable mapping could be found";
diff --git a/src/main/java/tmltranslator/dsez3engine/OptimizationResult.java b/src/main/java/tmltranslator/dsez3engine/OptimizationResult.java
index 559411200ef71733164251a01af2b3d5dffbe204..fa3e402a95fea87df852a22b24dee67e2deeaf87 100644
--- a/src/main/java/tmltranslator/dsez3engine/OptimizationResult.java
+++ b/src/main/java/tmltranslator/dsez3engine/OptimizationResult.java
@@ -57,6 +57,7 @@ public class OptimizationResult {
public String result = "";
public boolean mappingFound = false;
public String error = null;
+ public TMLMapping resultingMapping;
public OptimizationResult() {
}
diff --git a/src/main/java/ui/window/JDialogProverifVerification.java b/src/main/java/ui/window/JDialogProverifVerification.java
index e0c179ae2584961d96e07cd8c05395bcfa30ae64..f59300d9d2ed67a1e0075e89327b8ed7fe101d89 100644
--- a/src/main/java/ui/window/JDialogProverifVerification.java
+++ b/src/main/java/ui/window/JDialogProverifVerification.java
@@ -148,7 +148,6 @@ public class JDialogProverifVerification extends JDialog implements ActionListen
TURTLEPanel currPanel;
-
int mode;
@@ -175,7 +174,7 @@ public class JDialogProverifVerification extends JDialog implements ActionListen
JPanel listPanel;
- //security generation buttons
+ // Security generation buttons
ButtonGroup secGroup;
protected JCheckBox autoConf, autoWeakAuth, autoStrongAuth, custom, addHSM;
diff --git a/src/main/java/ui/window/JFrameHelp.java b/src/main/java/ui/window/JFrameHelp.java
index 5038f2dc5bae7bebfb5e963eaf489bd51c14dcd1..8baaf33f7916c0d419c8c38d1f2bcaa5c77e6a55 100644
--- a/src/main/java/ui/window/JFrameHelp.java
+++ b/src/main/java/ui/window/JFrameHelp.java
@@ -44,6 +44,7 @@ package ui.window;
import help.HelpEntry;
import help.HelpManager;
+import help.SearchResultHelpEntry;
import myutil.TraceManager;
import ui.MainGUI;
import ui.util.IconManager;
@@ -70,12 +71,14 @@ public class JFrameHelp extends JFrame implements ActionListener {
private HelpManager hm;
private JPanel jp01;
private JButton back, forward, up, search;
+ private JTextField searchT;
private Vector<HelpEntry> visitedEntries;
private int currentHEPointer;
public JFrameHelp(String title, HelpManager hm, HelpEntry he) {
super(title);
this.he = he;
+ this.hm = hm;
visitedEntries = new Vector<>();
setDefaultCloseOperation(JFrame.DISPOSE_ON_CLOSE);
@@ -93,9 +96,22 @@ public class JFrameHelp extends JFrame implements ActionListener {
up = new JButton("Up", IconManager.imgic78Big);
up.addActionListener(this);
topButtons.add(up);
- framePanel.add(topButtons, BorderLayout.NORTH);
+ // search
+ searchT = new JTextField("", 20);
+ searchT.setEnabled(true);
+ searchT.setEditable(true);
+ searchT.addActionListener(this);
+ topButtons.add(searchT);
+
+ search = new JButton("Search", IconManager.imgic5200);
+ search.addActionListener(this);
+ topButtons.add(search);
+
+ framePanel.add(topButtons, BorderLayout.NORTH);
+ // End of top panel
+
jp01 = new JPanel();
jp01.setLayout(new BorderLayout());
@@ -184,6 +200,8 @@ public class JFrameHelp extends JFrame implements ActionListener {
forward();
} else if (evt.getSource() == up) {
up();
+ } else if ((evt.getSource() == search) || (evt.getSource() == searchT)) {
+ search();
}
}
@@ -218,6 +236,31 @@ public class JFrameHelp extends JFrame implements ActionListener {
setHelpEntry(he.getFather());
}
+ public void search() {
+ TraceManager.addDev("Search");
+
+ if (hm == null) {
+ TraceManager.addDev("Null HM");
+ return;
+ }
+
+
+ String test = searchT.getText().trim();
+ if (test.length() == 0) {
+ TraceManager.addDev("Empty search");
+ return;
+ }
+
+ SearchResultHelpEntry srhe = new SearchResultHelpEntry();
+ srhe.fillInfos("searchresult search help list index");
+
+ hm.search(test.split(" "), srhe);
+
+
+ TraceManager.addDev("Setting new help entrywith search results ");
+ setHelpEntry(srhe);
+ }
+
} // Class
diff --git a/src/main/resources/help/clockdivider.html b/src/main/resources/help/clockdivider.html
index f22aab0ad0c0381b0fe98fee695c2bfbd3d3c07b..9968d7cd7ea66feab9dcedafde7bc8528ed5e8d2 100644
--- a/src/main/resources/help/clockdivider.html
+++ b/src/main/resources/help/clockdivider.html
@@ -16,7 +16,8 @@
<![endif]-->
</head>
<body>
-<p>The clock divider parameter specifies the relation between the main hardware clock (which is assumed to be unique) and the clock of the corresponding hardware node.</p>
-<p>Said differently, a clock divider of “x†means that the clock of this nodes runs at mainclock/x MHz.</p>
+<h2 id="clock-divider">Clock divider</h2>
+<p>The clock divider specifies the operating clock frequency of the corresponding hardware node.</p>
+<p>It is expressed via a number that is used to divide the global design frequency, whose default value is 200 MHz. Thus a clock divider equal to 4 means that the CPU operates at 200/4 = 50 MHz</p>
</body>
</html>
diff --git a/src/main/resources/help/clockdivider.md b/src/main/resources/help/clockdivider.md
index d8e26e105cc5fe1605e0381e274472d2ae7b3c28..1f20e75ef3127aba5e78f9923887eb39fe18cd7f 100644
--- a/src/main/resources/help/clockdivider.md
+++ b/src/main/resources/help/clockdivider.md
@@ -1,3 +1,9 @@
-The clock divider parameter specifies the relation between the main hardware clock (which is assumed to be unique) and the clock of the corresponding hardware node.
+## Clock divider
+
+The clock divider specifies the operating clock frequency of the corresponding hardware node.
+
+It is expressed via a number that is used to divide the global design
+frequency, whose default value is 200 MHz. Thus a clock divider equal to 4 means that the CPU operates at 200/4 = 50 MHz
+
+
-Said differently, a clock divider of "x" means that the clock of this nodes runs at mainclock/x MHz.
\ No newline at end of file
diff --git a/src/main/resources/help/searchresult.html b/src/main/resources/help/searchresult.html
new file mode 100644
index 0000000000000000000000000000000000000000..471bee0b285916a97a3057215c901cdb8a89d426
--- /dev/null
+++ b/src/main/resources/help/searchresult.html
@@ -0,0 +1,21 @@
+<!DOCTYPE html>
+<html xmlns="http://www.w3.org/1999/xhtml" lang="" xml:lang="">
+<head>
+ <meta charset="utf-8" />
+ <meta name="generator" content="pandoc" />
+ <meta name="viewport" content="width=device-width, initial-scale=1.0, user-scalable=yes" />
+ <title>searchresult</title>
+ <style>
+ code{white-space: pre-wrap;}
+ span.smallcaps{font-variant: small-caps;}
+ span.underline{text-decoration: underline;}
+ div.column{display: inline-block; vertical-align: top; width: 50%;}
+ </style>
+ <!--[if lt IE 9]>
+ <script src="//cdnjs.cloudflare.com/ajax/libs/html5shiv/3.7.3/html5shiv-printshiv.min.js"></script>
+ <![endif]-->
+</head>
+<body>
+
+</body>
+</html>
diff --git a/src/main/resources/help/searchresult.md b/src/main/resources/help/searchresult.md
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391