Skip to content
Snippets Groups Projects
JDialogUPPAALValidation.java 27.13 KiB
/**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.
 *
 * /**
 * Class JDialogUPPAALValidation
 * Dialog for managing the syntax analysis of LOTOS specifications
 * Creation: 16/05/2007
 * @version 1.0 16/05/2007
 * @author Ludovic APVRILLE
 * @see
 */

package ui.window;

import java.awt.*;
import java.awt.event.*;
import javax.swing.*;
import java.io.*;
import java.util.*;
import java.util.regex.*;

import avatartranslator.*;
import avatartranslator.touppaal.*;
import uppaaldesc.*;
import launcher.*;
import myutil.*;
import ui.*;

public class JDialogUPPAALValidation extends javax.swing.JDialog implements ActionListener, Runnable  {
    private static boolean deadlockAChecked, deadlockEChecked, generateTraceChecked, customChecked, stateAChecked, stateEChecked, stateLChecked, showDetailsChecked, translateChecked;

    protected MainGUI mgui;

    protected String cmdVerifyta;
    protected String fileName;
    protected String pathTrace;
    protected String spec;
    protected String host;
    protected int mode;
    protected RshClient rshc;
    protected Thread t;

    protected final static int NOT_STARTED = 1;
    protected final static int STARTED = 2;
    protected final static int STOPPED = 3;

    //components
    protected JTextArea jta;
    protected JButton start;
    protected JButton stop;
    protected JButton close;
    protected JButton eraseAll;

    protected JCheckBox deadlockE, deadlockA, generateTrace, custom, stateE, stateA, stateL, showDetails;
    protected JTextField customText;
    protected JTextField translatedText;
    protected TURTLEPanel tp;
    protected LinkedList<JCheckBox> customChecks;

    protected LinkedList<String> customQueries;
    public HashMap<String, Integer> verifMap;
    protected int status = -1;
    /** Creates new form  */
    public JDialogUPPAALValidation(Frame f, MainGUI _mgui, String title, String _cmdVerifyta, String _pathTrace, String _fileName, String _spec, String _host, TURTLEPanel _tp) {
        super(f, title, true);

        mgui = _mgui;

        cmdVerifyta = _cmdVerifyta;
        fileName = _fileName;
        pathTrace = _pathTrace;
        spec = _spec;
        host = _host;
        tp = _tp;
        AvatarSpecification aspec = mgui.gtm.getAvatarSpecification();
        if (aspec != null) {
            customQueries = aspec.getSafetyPragmas();
        }

        //TraceManager.addDev("Panel in UPPAAL Validation: " + mgui.getTabName(tp));
        customChecks = new LinkedList<JCheckBox>();
        initComponents();
        myInitComponents();
	verifMap = new HashMap<String, Integer>();
        pack();

        //getGlassPane().addMouseListener( new MouseAdapter() {});
        getGlassPane().setCursor(Cursor.getPredefinedCursor(Cursor.WAIT_CURSOR));
    }


    protected void myInitComponents() {
        mode = NOT_STARTED;
        setButtons();
    }

    protected void initComponents() {

        Container c = getContentPane();
        setFont(new Font("Helvetica", Font.PLAIN, 14));
        c.setLayout(new BorderLayout());
        //setDefaultCloseOperation(JFrame.DISPOSE_ON_CLOSE);

        JPanel jp1 = new JPanel();
        GridBagLayout gridbag1 = new GridBagLayout();
        GridBagConstraints c1 = new GridBagConstraints();
        jp1.setLayout(gridbag1);
        jp1.setBorder(new javax.swing.border.TitledBorder("Verify with UPPAAL: options"));
        //jp1.setPreferredSize(new Dimension(300, 150));

        // first line panel1
        //c1.gridwidth = 3;
        c1.gridheight = 1;
        c1.weighty = 1.0;
        c1.weightx = 1.0;
        c1.gridwidth = GridBagConstraints.REMAINDER; //end row
        c1.fill = GridBagConstraints.BOTH;
        c1.gridheight = 1;

        /*deadlockE = new JCheckBox("Search for absence of deadock situations");
          deadlockE.addActionListener(this);
          jp1.add(deadlockE, c1);
          deadlockE.setSelected(deadlockEChecked);*/

        deadlockA = new JCheckBox("Search for absence of deadock situations");
        deadlockA.addActionListener(this);
        jp1.add(deadlockA, c1);
        deadlockA.setSelected(deadlockAChecked);

        stateE = new JCheckBox("Reachability of selected states");
        stateE.addActionListener(this);
        stateE.setToolTipText("Study the fact that a given state may be reachable i.e. in at least one path");
        jp1.add(stateE, c1);
        stateE.setSelected(stateEChecked);

        stateA = new JCheckBox("Liveness of selected states");
        stateA.addActionListener(this);
        stateA.setToolTipText("Study the fact that a given state is always reachable i.e. in all paths");
        jp1.add(stateA, c1);
        stateA.setSelected(stateAChecked);

        stateL = new JCheckBox("Leads to");
        stateL.addActionListener(this);
        stateL.setToolTipText("Study the fact that, if accessed,  a given state is eventually followed by another one");
        jp1.add(stateL, c1);
        stateL.setSelected(stateLChecked);
        c1.gridwidth = GridBagConstraints.REMAINDER;
        custom = new JCheckBox("Custom verification");
        custom.addActionListener(this);
        jp1.add(custom, c1);
        custom.setSelected(customChecked);
        if (customQueries != null) {
            for (String s: customQueries){
                c1.gridwidth = GridBagConstraints.RELATIVE;
                JLabel space = new JLabel("   ");
                c1.weightx=0.0;
                jp1.add(space, c1);
                c1.gridwidth = GridBagConstraints.REMAINDER; //end row
                JCheckBox cqb = new JCheckBox(s);
                cqb.addActionListener(this);
                c1.weightx=1.0;
                jp1.add(cqb, c1);
                customChecks.add(cqb);

            }
        }
        /*  jp1.add(new JLabel("Custom formula to translate = "), c1);
            c1.gridwidth = GridBagConstraints.REMAINDER; //end row
            customText = new JTextField("Type your CTL formulae here!", 80);
            customText.addActionListener(this);
            jp1.add(customText, c1);

            c1.gridwidth = 1;
            translateCustom = new JCheckBox("Use translated custom verification");
            translateCustom.addActionListener(this);
            jp1.add(translateCustom, c1);
            custom.setSelected(translateChecked);
            c1.gridwidth = GridBagConstraints.REMAINDER; //end row
            translatedText = new JTextField("Translated CTL formula here", 80);
            customText.addActionListener(this);
            jp1.add(translatedText,c1);
        */
        generateTrace = new JCheckBox("Generate simulation trace");
        generateTrace.addActionListener(this);
        jp1.add(generateTrace, c1);
        generateTrace.setSelected(generateTraceChecked);

        showDetails = new JCheckBox("Show verification details");
        showDetails.addActionListener(this);
        jp1.add(showDetails, c1);
        showDetails.setSelected(showDetailsChecked);

        jp1.setMinimumSize(jp1.getPreferredSize());
        c.add(jp1, BorderLayout.NORTH);

        jta = new ScrolledJTextArea();
        jta.setEditable(false);
        jta.setMargin(new Insets(10, 10, 10, 10));
        jta.setTabSize(3);
        jta.append("Select options and then, click on 'start' to start generation of RG\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);

        start = new JButton("Start", IconManager.imgic53);
        stop = new JButton("Stop", IconManager.imgic55);
        close = new JButton("Close", IconManager.imgic27);
        eraseAll = new JButton("Del", IconManager.imgic337);

        start.setPreferredSize(new Dimension(100, 30));
        stop.setPreferredSize(new Dimension(100, 30));
        close.setPreferredSize(new Dimension(110, 30));
        eraseAll.setPreferredSize(new Dimension(100, 30));

        start.addActionListener(this);
        stop.addActionListener(this);
        close.addActionListener(this);
        eraseAll.addActionListener(this);

        JPanel jp2 = new JPanel();
        jp2.add(start);
        jp2.add(stop);
        jp2.add(close);
        jp2.add(eraseAll);
        c.add(jp2, BorderLayout.SOUTH);
    }

    public void actionPerformed(ActionEvent evt)  {
        String command = evt.getActionCommand();

        // Compare the action command to the known actions.
        if (evt.getSource() == eraseAll) {
            eraseTextArea();
        } else if (command.equals("Start"))  {
            startProcess();
        } else if (command.equals("Stop")) {
            stopProcess();
        } else if (command.equals("Close")) {
            closeDialog();
        } else {
            setButtons();
        }

    }

    public void eraseTextArea() {
        jta.setText("");
    }

    public void closeDialog() {
        if (mode == STARTED) {
            stopProcess();
        }
        //deadlockEChecked = deadlockE.isSelected();
        deadlockAChecked = deadlockA.isSelected();
        stateEChecked = stateE.isSelected();
        stateAChecked = stateA.isSelected();
        stateLChecked = stateL.isSelected();
        customChecked = custom.isSelected();
        generateTraceChecked = generateTrace.isSelected();
        showDetailsChecked = showDetails.isSelected();
        dispose();
    }

    public void stopProcess() {
        try {
            rshc.stopFillJTA();
        } catch (LauncherException le) {
        }
        rshc = null;
        mode =  NOT_STARTED;
        setButtons();
    }

    public void startProcess() {
        t = new Thread(this);
        mode = STARTED;
        setButtons();
        t.start();
    }


    public void run() {

        String cmd1 = "";
        String data1;
        int id = 0;
        String query;
        String name;
        int trace_id = 0;
        int index;
        String fn;

        rshc = new RshClient(host);
        RshClient rshctmp = rshc;

        try {
            id = rshc.getId();
            jta.append("Session id on launcher="+id + "\n");

            fn = fileName.substring(0, fileName.length()-4) + "_" + id;

            jta.append("Sending UPPAAL specification data\n");
            rshc.sendFileData(fn+".xml", spec);

            /*if (deadlockE.isSelected()) {
              jta.append("Searching for absence of deadlock situations\n");
              workQuery("A[] not deadlock", fileName, trace_id, rshc);
              trace_id++;
              }*/

            if (deadlockA.isSelected() && (mode != NOT_STARTED)) {
                jta.append("\n\n--------------------------------------------\n");
                jta.append("Searching for absence of deadlock situations\n");
                workQuery("A[] not deadlock", fn, trace_id, rshc);
                trace_id++;
            }

            if (stateE.isSelected()&& (mode != NOT_STARTED)) {
                ArrayList<String> list = mgui.gtm.getUPPAALQueries(tp);
                if ((list != null) && (list.size() > 0)){
                    for(String s: list) {
                        index = s.indexOf('$');
                        if ((index != -1) && (mode != NOT_STARTED)) {
                            name = s.substring(index+1, s.length());
                            TraceManager.addDev("****\n name=" + name + " list=" + list + "\n****\n");
                            query = s.substring(0, index);
                            //jta.append("\n\n--------------------------------------------\n");
                            jta.append("\nReachability of: " + name + "\n");
                            workQuery("E<> " + query, fn, trace_id, rshc);
                            trace_id++;
                        } else {
                            jta.append("A component could not be studied (internal error)\n");
                        }
                    }
                } else {
                    jta.append("Accessibility: No selected component found on diagrams\n");
                }
            }

            if (stateA.isSelected() && (mode != NOT_STARTED)) {
                ArrayList<String> list = mgui.gtm.getUPPAALQueries(tp);
                if ((list != null) && (list.size() > 0)){
                    for(String s: list) {
                        index = s.indexOf('$');
                        if ((index != -1) && (mode != NOT_STARTED)) {
                            name = s.substring(index+1, s.length());
                            query = s.substring(0, index);
                            //jta.append("\n--------------------------------------------\n");
                            jta.append("\nLiveness of: " + name + "\n");
                            workQuery("A<> " + query, fn, trace_id, rshc);
                            trace_id++;
                        } else {
                            jta.append("A component could not be studied (internal error)\n");
                        }
                    }
                } else {
                    jta.append("Liveness: No selected component found on diagrams\n\n");
                }
            }
            if (stateL.isSelected() && (mode != NOT_STARTED)) {
                ArrayList<String> list = mgui.gtm.getUPPAALQueries(tp);
                String s1, s2, name1, name2, query1, query2;
                int index1, index2;
                if ((list != null) && (list.size() > 0)){
                    for(int i=0; i<list.size()-1; i++) {
                        for(int j=i+1; j<list.size(); j++) {
                            s1 = list.get(i);
                            s2 = list.get(j);
                            index1 = s1.indexOf('$');
                            index2 = s2.indexOf('$');
                            //TraceManager.addDev("\n******\n\n\n");
                            //TraceManager.addDev("s1=" + s1 + "\ns2=" + s2);
                            if ((index1 != -1) && (index2 != -1) && (mode != NOT_STARTED)) {
                                name1 = s1.substring(index1+1, s1.length());
                                query1 = s1.substring(0, index1);
                                name2 = s2.substring(index2+1, s2.length());
                                query2 = s2.substring(0, index2);
                                //TraceManager.addDev("name1=" + name1 + "\nname2=" + name2);
                                //TraceManager.addDev("query1=" + s1 + "\nquery2=" + s2);
                                if ((name1.compareTo(name2) != 0) && (name1.length() > 0) && (name2.length() > 0)) {
                                    if (!(showDetails.isSelected())) {
                                        int indexName = name1.indexOf(":");
                                        if (indexName != -1) {
                                            name1 = name1.substring(indexName+1, name1.length()).trim();
                                        }
                                        indexName = name2.indexOf(":");
                                        if (indexName != -1) {
                                            name2 = name2.substring(indexName+1, name2.length()).trim();
                                        }
                                    }
                                    jta.append("\nLeads to: " + name1 + "--> " + name2 + "\n");
                                    workQuery(query1 + " --> " + query2, fn, trace_id, rshc);
                                    trace_id++;
                                    jta.append("\nLeads to: " + name2 + "--> " + name1 + "\n");
                                    workQuery(query2 + " --> " + query1, fn, trace_id, rshc);
                                    trace_id++;
                                }
                            }else {
                                jta.append("A component could not be studied (internal error)\n");
                            }
                        }
                    }
                } else {
                    jta.append("Liveness: No selected component found on diagrams\n\n");
                }
            }

            if(custom.isSelected() && (mode != NOT_STARTED)) {
                jta.append("\n\n--------------------------------------------\n");

                jta.append("Studying custom CTL formulae\n");
                for (JCheckBox j: customChecks){
                    if (j.isSelected()){
                        jta.append(j.getText()+"\n");
                        String translation = translateCustomQuery(j.getText());
			status = -1;
                        workQuery(translation, fn, trace_id, rshc);
			verifMap.put(j.getText(), status);
                        trace_id++;
                    }
                }
		mgui.modelBacktracingUPPAAL(verifMap);
            }

            //Removing files
            rshc.deleteFile(fn+".xml");
            rshc.deleteFile(fn + ".q");
            rshc.deleteFile(fn + ".res");
            rshc.deleteFile(fn + ".xtr");

            rshc.freeId(id);
            jta.append("\nAll Done\n");

        } catch (LauncherException le) {
            jta.append(le.getMessage() + "\n");
            mode =      NOT_STARTED;
            setButtons();
            try{
                if (rshctmp != null) {
                    rshctmp.freeId(id);
                }
            } catch (LauncherException le1) {}
            return;
        } catch (Exception e) {
            TraceManager.addError("Exception: " + e.getMessage());
            mode =      NOT_STARTED;
            setButtons();
            try{
                if (rshctmp != null) {
                    rshctmp.freeId(id);
                }
            } catch (LauncherException le1) {}
            return;
        }
   	
        mode = NOT_STARTED;
        setButtons();
    }
    private String translateCustomQuery(String query){
        UPPAALSpec spec = mgui.gtm.getLastUPPAALSpecification();
        AVATAR2UPPAAL avatar2uppaal = mgui.gtm.getAvatar2Uppaal();
        AvatarSpecification avspec = mgui.gtm.getAvatarSpecification();
        Hashtable <String, String> hash = avatar2uppaal.getHash();
        String finQuery=query+" ";
        /*      String[] split = query.split("[\\s-()=]+");
                for (String s: split){
                System.out.println(s);
                } */
        /*      Pattern p = Pattern.compile("[\\s-()=]+");
                Matcher m = p.matcher(query);
                int index1=0;
                int index2=m.start();
                while (m.find()){
                System.out.println("Finding ...");
                index2=m.start();
                String rep = hash.get(finQuery.substring(index1, index2));
                if (rep !=null){
                System.out.println(finQuery.substring(index1, index2) + "--" + rep);
                finQuery = finQuery.substring(0,index1) + rep + finQuery.substring(index2, finQuery.length());
                }
                index1=index2;
                }*/
        for (String str: hash.keySet()){
            finQuery = finQuery.replaceAll(str+"\\s", hash.get(str));
            finQuery = finQuery.replaceAll(str+"\\)", hash.get(str)+"\\)");
            finQuery = finQuery.replaceAll(str+"\\-", hash.get(str)+"\\-");
        }
        if (avspec==null){
            return "";
        }

        LinkedList<AvatarBlock> blocks = avspec.getListOfBlocks();
        for (AvatarBlock block:blocks){
            UPPAALTemplate temp = spec.getTemplateByName(block.getName());
            if (temp !=null){
                int index = avatar2uppaal.getIndexOfTranslatedTemplate(temp);
                finQuery = finQuery.replaceAll(block.getName(), block.getName()+"__"+index);
            }
        }
        //translatedText.setText(finQuery);
        return finQuery;
    }
    private void workQuery(String query, String fn, int trace_id, RshClient rshc) throws LauncherException {

        TraceManager.addDev("Working on query: " + query);

        String cmd1, data;
        if(showDetails.isSelected()) {
            jta.append("-> " + query + "\n");
        }
        rshc.sendFileData(fn+".q", query);

        cmd1 = cmdVerifyta + " -u ";
        if (generateTrace.isSelected()) {
            cmd1 += "-t1 -f " + fn +  " ";
        }
        cmd1 += fn + ".xml " + fn + ".q";
        //jta.append("--------------------------------------------\n");
	//TraceManager.addDev("Query:>" + cmd1 + "<");
        data = processCmd(cmd1);
        //TraceManager.addDev("Results:>" + data + "<");
        if(showDetails.isSelected()) {
            jta.append(data);
        }
        //NOTE: [error] is only visible if Error Stream is parsed
        if (mode != NOT_STARTED) {
            if (data.trim().length() == 0) {
                //jta.append("The verifier of UPPAAL could not be started: error\n");
                throw new LauncherException("The verifier of UPPAAL could not be started.\nProbably, UPPAAL is badly installed, or TTool is badly configured:\nCheck for UPPAALVerifierPath and UPPAALVerifierHost configurations.");
            }
            else if (data.indexOf("Property is satisfied") >-1){
                jta.append("-> property is satisfied\n");
		status=1;
            }
            else if (data.indexOf("Property is NOT satisfied") > -1) {
                jta.append("-> property is NOT satisfied\n");
		status = 0;
            }
            else {
                jta.append("ERROR -> property could not be studied\n");
            }
        } else {
            jta.append("** verification stopped **\n");
        }



        if (generateTrace.isSelected()) {
            generateTraceFile(fn, trace_id, rshc);
        }
	
    }

    private void generateTraceFile(String fn, int trace_id, RshClient rshc) throws LauncherException{
        //jta.append("Going to generate trace file\n");
        String data, name;
        try {
            data = rshc.getFileData(fn + "-1.xtr");
            rshc.deleteFile(fn + "-1.xtr");
        } catch (Exception e) {
            jta.append("(no simulation trace was generated)\n");
            return;
        }
        name = pathTrace + fn + "_" + trace_id + ".xtr";
        //jta.append("Trying to generate trace file in" + name + "\n");
        try {
            FileUtils.saveFile(name, data);
            jta.append("Trace has been generated in " + name + "\n");
        } catch (FileException fe) {
            jta.append("Trace could not be generated in " + name + "\n");
            jta.append("Exception: " + fe.getMessage() + "\n");
        }
    }

    protected String processCmd(String cmd) throws LauncherException {
        rshc.setCmd(cmd);
        String s = null;
        rshc.sendProcessRequest();
        s = rshc.getDataFromProcess();
        return s;
    }

    protected void setButtons() {
        switch(mode) {
        case NOT_STARTED:
            custom.setEnabled(true);
            //deadlockE.setEnabled(true);
            deadlockA.setEnabled(true);
            stateE.setEnabled(true);
            stateA.setEnabled(true);
            stateL.setEnabled(true);
            generateTrace.setEnabled(true);
            showDetails.setEnabled(true);
            for (JCheckBox cb: customChecks){
                cb.setEnabled(custom.isSelected());
            }
            if (custom.isSelected() || /*deadlockE.isSelected() ||*/deadlockA.isSelected() || stateE.isSelected() || stateA.isSelected() || stateL.isSelected()) {
                start.setEnabled(true);
            } else {
                start.setEnabled(false);
            }

            stop.setEnabled(false);
            close.setEnabled(true);
            eraseAll.setEnabled(true);
            getGlassPane().setVisible(false);


            break;
        case STARTED:
            custom.setEnabled(false);
            //deadlockE.setEnabled(false);
            deadlockA.setEnabled(false);
            stateE.setEnabled(false);
            stateA.setEnabled(false);
            stateL.setEnabled(false);
            generateTrace.setEnabled(false);
            showDetails.setEnabled(false);
            start.setEnabled(false);
            stop.setEnabled(true);
            close.setEnabled(false);
            eraseAll.setEnabled(false);
            for (JCheckBox cb: customChecks){
                cb.setEnabled(false);
            }
            getGlassPane().setVisible(true);
            break;
        case STOPPED:
        default:
            custom.setEnabled(false);
            //deadlockE.setEnabled(false);
            deadlockA.setEnabled(false);
            stateE.setEnabled(false);
            stateA.setEnabled(false);
            stateL.setEnabled(false);
            generateTrace.setEnabled(false);
            showDetails.setEnabled(false);
            start.setEnabled(false);
            stop.setEnabled(false);
            close.setEnabled(true);
            eraseAll.setEnabled(true);
            getGlassPane().setVisible(false);
            for (JCheckBox cb: customChecks){
                cb.setEnabled(false);
            }
            break;
        }
    }
}