update on refusal graphs

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
 

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;

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() + "}");

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;
+    }
+
 }

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);
+                }
+	    }
 
         }
 

src/main/java/ui/window/JFrameRefusalGraph.java

+/* 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();
+    }
+    
+
+}