diff --git a/src/main/java/myutil/BoolExpressionEvaluator.java b/src/main/java/myutil/BoolExpressionEvaluator.java
index e9f8714ded40eb4f313993a8c2314ce38988d769..c74f9ef612967110cf37766bb04ec0c71f027562 100755
--- a/src/main/java/myutil/BoolExpressionEvaluator.java
+++ b/src/main/java/myutil/BoolExpressionEvaluator.java
@@ -713,8 +713,8 @@ public class BoolExpressionEvaluator {
_expr = Conversion.replaceAllString(_expr, "and", "&").trim();
_expr = Conversion.replaceAllString(_expr, "==", "=").trim();
_expr = Conversion.replaceAllString(_expr, "!=", "$").trim();
- //_expr = Conversion.replaceAllString(_expr, ">=", ":").trim();
- //_expr = Conversion.replaceAllString(_expr, "<=", ";").trim();
+ _expr = Conversion.replaceAllString(_expr, ">=", ":").trim();
+ _expr = Conversion.replaceAllString(_expr, "<=", ";").trim();
// For not() -> must find the closing bracket
diff --git a/src/main/java/ui/MainGUI.java b/src/main/java/ui/MainGUI.java
index d237a2ed2e5ddfa79fdc78f205fa4851e2caf463..2e4d2f814fc7ae7eb3d626ec61a18ba8837fdd4d 100644
--- a/src/main/java/ui/MainGUI.java
+++ b/src/main/java/ui/MainGUI.java
@@ -686,6 +686,13 @@ public class MainGUI implements ActionListener, WindowListener, KeyListener, Pe
jfm.setVisible(true);
}
+ public void makeRefusalGraph(RG inputGraph) {
+ JFrameRefusalGraph jfm = new JFrameRefusalGraph(frame, this, "Refusal Graph Construction", inputGraph);
+ //jfm.setSize(900, 700);
+ GraphicLib.centerOnParent(jfm, 900, 700);
+ jfm.setVisible(true);
+ }
+
public void setCurrentInvariant(Invariant inv) {
currentInvariant = inv;
diff --git a/src/main/java/ui/graph/AUTGraph.java b/src/main/java/ui/graph/AUTGraph.java
index 22f8b887479af0f4a767b5363edcbc118bdc7a83..d6ea09efecffa2a3ed62a416aa292aef1c5128dc 100755
--- a/src/main/java/ui/graph/AUTGraph.java
+++ b/src/main/java/ui/graph/AUTGraph.java
@@ -268,6 +268,10 @@ public class AUTGraph implements myutil.Graph {
statesComputed = false;
}
+ public void addState(AUTState _st) {
+ states.add(_st);
+ }
+
public int getNbPotentialDeadlocks(){
@@ -1316,6 +1320,57 @@ public class AUTGraph implements myutil.Graph {
}
+ public AUTGraph generateRefusalGraph() {
+ computeStates();
+
+ AUTState currentState = new AUTState(0);
+ ArrayList<AUTState> newStates = new ArrayList<AUTState>();
+ ArrayList<AUTTransition> newTransitions = new ArrayList<AUTTransition>();
+ newStates.add(currentState);
+
+ // We go thru the graph, starting at state1. Each time we meet an already handled state, we stop.
+ HashSet<AUTState> metStates = new HashSet<AUTState>(); // in origin Graph
+ HashMap<AUTState, AUTState> toRefusalState = new HashMap<AUTState, AUTState>();
+ LinkedList<AUTState> toHandle = new LinkedList<AUTState>();
+ toHandle.add(states.get(0));
+ toRefusalState.put(states.get(0), currentState);
+
+ while(toHandle.size() > 0) {
+ AUTState current = toHandle.get(0);
+ toHandle.remove(0);
+ metStates.add(current);
+ AUTState currentRefusal = toRefusalState.get(current);
+ if (currentRefusal == null) {
+ TraceManager.addDev("NULL current Refusal");
+ } else {
+ // For each possible transition, we create a new transition to a new destination state
+ for(AUTTransition tr: current.outTransitions) {
+ // Create new transition. Is a new staqte necessary?
+ AUTState destState = states.get(tr.destination);
+ AUTState stRefusal;
+ stRefusal = new AUTState(newStates.size());
+ newStates.add(stRefusal);
+ toRefusalState.put(destState, stRefusal);
+ AUTTransition trRefusal = new AUTTransition(current.id, tr.transition, stRefusal.id);
+ newTransitions.add(trRefusal);
+ stRefusal.addInTransition(trRefusal);
+ currentRefusal.addOutTransition(trRefusal);
+
+ if (!metStates.contains(destState)) {
+ if (!(toHandle.contains(destState))) {
+ toHandle.add(destState);
+ }
+ }
+
+ }
+ }
+ }
+ AUTGraph refusalGraph = new AUTGraph(newStates, newTransitions);
+
+ return refusalGraph;
+ }
+
+
private void printConfiguration(AUTPartition _part, AUTSplitter _w) {
TraceManager.addDev("P={" + _part.toString() + "}");
TraceManager.addDev("W={" + _w.toString() + "}");
diff --git a/src/main/java/ui/graph/RG.java b/src/main/java/ui/graph/RG.java
index 0fbd85f3eb9defec47b0542539c01cafecd9c893..2bcc48231765cd342e40241b7c7a12ebeb23e1fc 100755
--- a/src/main/java/ui/graph/RG.java
+++ b/src/main/java/ui/graph/RG.java
@@ -41,6 +41,8 @@
package ui.graph;
+import myutil.*;
+
/**
* Class RG
* Creation : 07/12/2016
@@ -71,4 +73,26 @@ public class RG {
return name + " " + nbOfStates + " states, " + nbOfTransitions + " transitions";
}
+ public RG generateRefusalGraph() {
+ if (graph == null) {
+ if (data == null){
+ return null;
+ }
+ graph = new AUTGraph();
+ graph.buildGraph(data);
+ }
+
+ TraceManager.addDev("Making Ref. G");
+ AUTGraph refusalGraph = graph.generateRefusalGraph();
+ //TraceManager.addDev("Null graph?");
+ if (refusalGraph == null) {
+ TraceManager.addDev("Null graph...");
+ return null;
+ }
+
+ RG ret = new RG(name+"_RF");
+ ret.graph = refusalGraph;
+ return ret;
+ }
+
}
diff --git a/src/main/java/ui/tree/JDiagramTree.java b/src/main/java/ui/tree/JDiagramTree.java
index a28235bc137348b4bba4ec918e1c0dec53a943da..fb8d9a5fac597137fb9678fff137d9d2e9d4c10a 100755
--- a/src/main/java/ui/tree/JDiagramTree.java
+++ b/src/main/java/ui/tree/JDiagramTree.java
@@ -86,6 +86,7 @@ public class JDiagramTree extends javax.swing.JTree implements ActionListener, M
protected JMenuItem jmiAnalyze;
protected JMenuItem jmiShow;
protected JMenuItem jmiMinimize;
+ protected JMenuItem jmiRefusalGraph;
protected JMenuItem jmiRemove;
protected JPopupMenu popupTree;
protected RG selectedRG;
@@ -192,11 +193,14 @@ public class JDiagramTree extends javax.swing.JTree implements ActionListener, M
jmiShow.addActionListener(this);
jmiMinimize = new JMenuItem("Minimize");
jmiMinimize.addActionListener(this);
+ jmiRefusalGraph = new JMenuItem("Make Refusal Graph");
+ jmiRefusalGraph.addActionListener(this);
jmiRemove = new JMenuItem("Remove from tree");
jmiRemove.addActionListener(this);
popupTree.add(jmiAnalyze);
popupTree.add(jmiShow);
popupTree.add(jmiMinimize);
+ popupTree.add(jmiRefusalGraph);
popupTree.addSeparator();
popupTree.add(jmiRemove);
}
@@ -392,7 +396,11 @@ public class JDiagramTree extends javax.swing.JTree implements ActionListener, M
if (selectedRG != null) {
mgui.minimizeRG(selectedRG);
}
- }
+ } else if (ae.getSource() == jmiRefusalGraph) {
+ if (selectedRG != null) {
+ mgui.makeRefusalGraph(selectedRG);
+ }
+ }
}
diff --git a/src/main/java/ui/window/JFrameRefusalGraph.java b/src/main/java/ui/window/JFrameRefusalGraph.java
new file mode 100755
index 0000000000000000000000000000000000000000..aebb1f30290d23b87c42f1e5aec8ccd42f584023
--- /dev/null
+++ b/src/main/java/ui/window/JFrameRefusalGraph.java
@@ -0,0 +1,238 @@
+/* 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 myutil.ScrolledJTextArea;
+import ui.util.IconManager;
+import ui.MainGUI;
+import ui.graph.AUTGraph;
+import ui.graph.RG;
+
+import javax.swing.*;
+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.ArrayList;
+import java.util.Collections;
+import java.util.HashSet;
+
+
+/**
+ * Class JFrameRefusalGraph
+ * Frame for handling the construction of the refusal graph
+ * Creation: 18/08/2017
+ * @version 1.0 18/08/2017
+ * @author Ludovic APVRILLE
+ */
+public class JFrameRefusalGraph extends javax.swing.JFrame implements ActionListener, Runnable {
+ /*private static boolean isAldebaranSelected = false;
+ private static boolean isOminSelected = false;
+ private static boolean isStrongSelected = true;*/
+
+
+ private MainGUI mgui;
+ private RG rg;
+ private RG newRG;
+
+ protected Thread t;
+
+ private int mode;
+
+ protected final static int NOT_STARTED = 1;
+ protected final static int STARTED = 2;
+ protected final static int STOPPED = 3;
+
+ //subpanels
+ private JPanel panel2;
+
+ // Main Panel
+ private ScrolledJTextArea jta;
+ private JButton start, stop, close;
+
+ /** Creates new form */
+ public JFrameRefusalGraph(Frame _f, MainGUI _mgui, String _title, RG _rg) {
+ super(_title);
+
+ mgui = _mgui;
+ rg = _rg;
+
+ initComponents();
+ myInitComponents();
+ pack();
+
+ //getGlassPane().addMouseListener( new MouseAdapter() {});
+ getGlassPane().setCursor(Cursor.getPredefinedCursor(Cursor.WAIT_CURSOR));
+ }
+
+
+ private void myInitComponents() {
+ mode = NOT_STARTED;
+ }
+
+ private void initComponents() {
+ Container c = getContentPane();
+ setFont(new Font("Helvetica", Font.PLAIN, 14));
+ c.setLayout(new BorderLayout());
+ setDefaultCloseOperation(JFrame.DISPOSE_ON_CLOSE);
+
+
+
+ // textarea panel
+ jta = new ScrolledJTextArea();
+ jta.setEditable(false);
+ jta.setMargin(new Insets(10, 10, 10, 10));
+ jta.setTabSize(3);
+ jta.append("Select actions and then, click on 'start' to start minimization\n");
+ Font f = new Font("Courrier", Font.BOLD, 12);
+ jta.setFont(f);
+ JScrollPane jsp = new JScrollPane(jta, JScrollPane.VERTICAL_SCROLLBAR_ALWAYS, JScrollPane.HORIZONTAL_SCROLLBAR_ALWAYS);
+
+ c.add(jsp, BorderLayout.CENTER);
+
+
+ // Button panel;
+ start = new JButton("Start", IconManager.imgic53);
+ stop = new JButton("Stop", IconManager.imgic55);
+ close = new JButton("Close", IconManager.imgic27);
+
+ start.setPreferredSize(new Dimension(150, 30));
+ stop.setPreferredSize(new Dimension(150, 30));
+ close.setPreferredSize(new Dimension(150, 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);
+ }
+
+ public void actionPerformed(ActionEvent evt) {
+ String command = evt.getActionCommand();
+
+ // Compare the action command to the known actions.
+ if (command.equals("Start")) {
+ startProcess();
+ } else if (command.equals("Stop")) {
+ stopProcess();
+ } else if (command.equals("Close")) {
+ closeDialog();
+ }
+ }
+
+
+
+
+ private void setButtons() {
+ switch(mode) {
+ case NOT_STARTED:
+ start.setEnabled(true);
+ stop.setEnabled(false);
+ close.setEnabled(true);
+ getGlassPane().setVisible(false);
+ break;
+ case STARTED:
+ start.setEnabled(false);
+ stop.setEnabled(true);
+ close.setEnabled(false);
+ getGlassPane().setVisible(false);
+ break;
+ case STOPPED:
+ default:
+ start.setEnabled(false);
+ stop.setEnabled(false);
+ close.setEnabled(true);
+ getGlassPane().setVisible(false);
+ break;
+ }
+ }
+
+
+ public void closeDialog() {
+ if (mode == STARTED) {
+ stopProcess();
+ }
+ dispose();
+ }
+
+ public void stopProcess() {
+
+ mode = STOPPED;
+ setButtons();
+ }
+
+ public void startProcess() {
+ t = new Thread(this);
+ mode = STARTED;
+ setButtons();
+ t.start();
+ }
+
+
+
+ public void run() {
+
+ jta.append("\nBuilding refusal graph...\n");
+
+ newRG = rg.generateRefusalGraph();
+
+ if (newRG != null) {
+ newRG.nbOfStates = newRG.graph.getNbOfStates();
+ newRG.nbOfTransitions = newRG.graph.getTransitions().size();
+ mgui.addRG(newRG);
+ jta.append("\nRefusal Graph: " + newRG.nbOfStates + " states, " + newRG.nbOfTransitions + " transitions\n");
+ } else {
+ jta.append("\nCould not build Refusal Graph\n");
+ }
+
+ mode = STOPPED;
+ setButtons();
+ }
+
+
+}