Skip to content
Snippets Groups Projects
GTURTLEModeling.java 389 KiB
Newer Older
/* Copyright or (C) or Copr. GET / ENST, Telecom-Paris, Ludovic Apvrille
 * ludovic.apvrille AT telecom-paristech.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;

import avatartranslator.*;
import avatartranslator.toproverif.AVATAR2ProVerif;
import avatartranslator.totpn.AVATAR2TPN;
import avatartranslator.toturtle.AVATAR2TURTLE;
import avatartranslator.touppaal.AVATAR2UPPAAL;
import common.ConfigurationTTool;
import common.SpecConfigTTool;
import ddtranslator.DDSyntaxException;
import ddtranslator.DDTranslator;
Ludovic Apvrille's avatar
Ludovic Apvrille committed
import graph.RG;
import launcher.LauncherException;
import launcher.RemoteExecutionThread;
import launcher.RshClient;
import myutil.*;
import nc.NCStructure;
import org.w3c.dom.Document;
import org.w3c.dom.Element;
import org.w3c.dom.Node;
import org.w3c.dom.NodeList;
import org.xml.sax.SAXException;
import proverifspec.ProVerifOutputAnalyzer;
import proverifspec.ProVerifSpec;
import req.ebrdd.EBRDD;
import sddescription.HMSC;
import sddescription.MSC;
import sdtranslator.SDTranslationException;
import sdtranslator.SDTranslator;
import tmatrix.RequirementModeling;
import tmltranslator.*;
import tmltranslator.modelcompiler.TMLModelCompiler;
import tmltranslator.toautomata.TML2AUT;
import tmltranslator.toautomata.TML2AUTviaLOTOS;
import tmltranslator.toavatar.FullTML2Avatar;
import tmltranslator.toavatarsec.TML2Avatar;
import tmltranslator.tosystemc.TML2SystemC;
import tmltranslator.toturtle.Mapping2TIF;
import tmltranslator.toturtle.TML2TURTLE;
import tmltranslator.touppaal.RelationTMLUPPAAL;
import tmltranslator.touppaal.TML2UPPAAL;
import tpndescription.TPN;
import translator.*;
import translator.totpn.TURTLE2TPN;
import translator.touppaal.RelationTIFUPPAAL;
import translator.touppaal.TURTLE2UPPAAL;
import ui.ad.TActivityDiagramPanel;
import ui.atd.AttackTreeDiagramPanel;
import ui.avatarad.AvatarADPanel;
import ui.avatarbd.*;
import ui.avatarcd.AvatarCDPanel;
import ui.avatardd.ADDDiagramPanel;
import ui.avatarmad.AvatarMADPanel;
import ui.avatarmethodology.AvatarMethodologyDiagramPanel;
import ui.avatarpd.AvatarPDPanel;
import ui.avatarrd.AvatarRDPanel;
import ui.avatarsmd.*;
import ui.cd.TCDTClass;
import ui.cd.TCDTObject;
import ui.cd.TClassDiagramPanel;
import ui.dd.TDDArtifact;
import ui.dd.TDDNode;
import ui.dd.TDeploymentDiagramPanel;
import ui.diplodocusmethodology.DiplodocusMethodologyDiagramPanel;
import ui.ebrdd.EBRDDPanel;
Ludovic Apvrille's avatar
Ludovic Apvrille committed
import ui.eln.ELNDiagramPanel;
apvrille's avatar
apvrille committed
import ui.ftd.FaultTreeDiagramPanel;
import ui.iod.InteractionOverviewDiagramPanel;
import ui.ncdd.NCDiagramPanel;
import ui.osad.TURTLEOSActivityDiagramPanel;
import ui.oscd.TOSClass;
import ui.oscd.TURTLEOSClassDiagramPanel;
import ui.procsd.ProCSDComponent;
import ui.procsd.ProactiveCSDPanel;
import ui.prosmd.ProactiveSMDPanel;
import ui.req.Requirement;
import ui.req.RequirementDiagramPanel;
import ui.syscams.SysCAMSComponentTaskDiagramPanel;
import ui.sysmlsecmethodology.SysmlsecMethodologyDiagramPanel;
import ui.tmlad.*;
import ui.tmlcd.TMLTaskDiagramPanel;
import ui.tmlcd.TMLTaskOperator;
import ui.tmlcompd.*;
import ui.tmlcp.TMLCPPanel;
import ui.tmldd.*;
import ui.tmlsd.TMLSDPanel;
apvrille's avatar
apvrille committed
import ui.tree.*;
import ui.ucd.UseCaseDiagramPanel;
import ui.util.DefaultText;
import ui.util.IconManager;
import ui.window.JFrameSimulationTrace;
import uppaaldesc.UPPAALSpec;

import javax.swing.*;
apvrille's avatar
apvrille committed
import javax.swing.tree.TreePath;
import javax.xml.parsers.DocumentBuilder;
import javax.xml.parsers.DocumentBuilderFactory;
import javax.xml.parsers.ParserConfigurationException;
import java.awt.*;
import java.io.*;
import java.util.*;
import java.util.List;

// AVATAR
// AVATAR

//Communication Pattern javaCC parser
//Communication Pattern javaCC parser
//import compiler.tmlCPparser.*;

 * Class GTURTLEModeling
 * Creation: 09/12/2003
 * Version: 1.1 02/06/2014
apvrille's avatar
apvrille committed
 *
Ludovic Apvrille's avatar
Ludovic Apvrille committed
    //Added by Solange
Ludovic Apvrille's avatar
Ludovic Apvrille committed
    public GProactiveDesign gpdtemp;


    //
    private Vector<TURTLEPanel> panels; /* analysis, design, deployment, tml design */
    private TURTLEModeling tm;
    private AvatarSpecification avatarspec;
    //  private AttackTree attackTree;
    private AVATAR2UPPAAL avatar2uppaal;
    private AVATAR2ProVerif avatar2proverif;
    private boolean optimizeAvatar;
    private int tmState; // 0:generated, 1: to be generated from mapping, 2: to be generated from TML modeling

    private TMLModeling<TGComponent> tmlm;
    private TMLMapping<TGComponent> artificialtmap;
    private TMLMapping<TGComponent> tmap;
    private TMLCP tmlcp;
    private TML2Avatar t2a;
    private RequirementModeling rm;
    private NCStructure ncs;
    private final MainGUI mgui;
    private CorrespondanceTGElement listE;
    private String rtlotos;

    private EBRDD ebrdd;

    private UPPAALSpec uppaal;
    private RelationTIFUPPAAL uppaalTIFTable;
    private RelationTMLUPPAAL uppaalTMLTable;

    private ProVerifSpec proverif;

    private AVATAR2TPN avatar2tpn;
    private TPN tpnFromAvatar;

    private String tpn;
    private String sim;
    private String dta;
    private String dtadot;
    private String rg;
    private String rgdot;
    private String rgaut;
    private String rgautdot;
    private String rgautproj;
    private String rgautprojdot;
    private String tlsa;
    private String tlsadot;

    private List<SimulationTrace> simulationTraces;
Ludovic Apvrille's avatar
Ludovic Apvrille committed
    private List<RG> graphs;
    private GraphTree gt;
    private SimulationTraceTree stt;
Ludovic Apvrille's avatar
Ludovic Apvrille committed

    private int nbRTLOTOS;
    private int nbSuggestedDesign;
    //  private int nbSuggestedAnalysis;
    //  private int nbTPN;

    //private ValidationDataTree vdt;
    private SearchTree st;
    private SyntaxAnalysisTree mcvdt;
    private InvariantDataTree idt;
apvrille's avatar
apvrille committed
    private HelpTree ht;
Ludovic Apvrille's avatar
Ludovic Apvrille committed

    private List<CheckingError> checkingErrors;
    private List<CheckingError> warnings;

    private List<Invariant> invariants;

    List<TGConnectorInfo> pendingConnectors;

    private Vector<String> savedOperations;
    private Vector<Point> savedPanels;
    private int nbMaxSavedOperations = 10;
    private int pointerOperation;

    private DocumentBuilderFactory dbf;
    private DocumentBuilder db;
    private Document docCopy;

    private int decX, decY, decId;

    private static int graphId = 0;

    private int languageID;
    public final static int RT_LOTOS = 0;
    public final static int LOTOS = 1;
    public final static int AUT = 2;
    public final static int TPN = 3;
    public final static int MATRIX = 4;
    public final static int UPPAAL = 5;
    public final static int PROVERIF = 6;

    private boolean undoRunning = false;


    boolean hasCrypto = false;
    //private Charset chset1, chset2;

    public GTURTLEModeling(MainGUI _mgui, Vector<TURTLEPanel> _panels) {
        mgui = _mgui;
        panels = _panels;
        try {
            dbf = DocumentBuilderFactory.newInstance();
            db = dbf.newDocumentBuilder();
        } catch (ParserConfigurationException e) {
            dbf = null;
            db = null;
        }
        savedOperations = new Vector<String>();
        savedPanels = new Vector<Point>();
        pointerOperation = -1;

        graphs = new ArrayList<RG>();
        simulationTraces = new ArrayList<SimulationTrace>();
Ludovic Apvrille's avatar
Ludovic Apvrille committed
        invariants = new LinkedList<Invariant>();

        //vdt = new ValidationDataTree(mgui);
        mcvdt = new SyntaxAnalysisTree(mgui);
        idt = new InvariantDataTree(mgui);
        st = new SearchTree(mgui);
        gt = new GraphTree(mgui);
        stt = new SimulationTraceTree(mgui);
apvrille's avatar
apvrille committed
        ht = new HelpTree(mgui);
Ludovic Apvrille's avatar
Ludovic Apvrille committed
		/*if (!Charset.isSupported("UTF-8")) {
		  ErrorGUI.exit(ErrorGUI.ERROR_CHARSET);
		  }
Ludovic Apvrille's avatar
Ludovic Apvrille committed
		  chset1 = Charset.forName("UTF-8");*/
    }

    public int getLanguageID() {
        return languageID;
    }

    public boolean isRegularTM() {
        if (tm == null) {
            return false;
        }
        return tm.isARegularTIFSpec();
    }

    public List<SimulationTrace> getSimulationTraces() {
        return simulationTraces;
    }

    public void addSimulationTrace(SimulationTrace newTrace) {
        //TraceManager.addDev("Adding new simulation trace " + newTrace);
        if (newTrace.hasFile()) {
            // We have to remove identical traces
            LinkedList<SimulationTrace> ll = new LinkedList<>();
            for (SimulationTrace trace : simulationTraces) {
                if (trace.hasFile()) {
                    if (trace.getFullPath().compareTo(newTrace.getFullPath()) == 0) {
                        ll.add(trace);
                    }
                }
            }
            for (SimulationTrace trace : ll) {
                simulationTraces.remove(trace);
            }
        }

        simulationTraces.add(newTrace);
    }

    public void removeSimulationTrace(SimulationTrace oldTrace) {
        //TraceManager.addDev("Adding new graph " + newGraph);
        simulationTraces.remove(oldTrace);
    }

Ludovic Apvrille's avatar
Ludovic Apvrille committed
    public List<RG> getRGs() {
        return graphs;
    }

    public void addRG(RG newGraph) {
        //TraceManager.addDev("Adding new graph " + newGraph);
        graphs.add(newGraph);
    }

    public void removeRG(RG oldGraph) {
        //TraceManager.addDev("Adding new graph " + newGraph);
        graphs.remove(oldGraph);
    }


    public List<Invariant> getInvariants() {
        return invariants;
    }


    public void addInvariant(Invariant _inv) {
        invariants.add(_inv);
        TraceManager.addDev("Adding invariant: " + _inv.toString());
    }

    public void clearInvariants() {
        invariants.clear();
    }


    public String saveTIF() {
        if (tm == null) {
            TraceManager.addDev("NO TIF to save");
            return null;
        }

        TIFExchange tif = new TIFExchange();
        tif.setTURTLEModeling(tm);
        String ret = tif.saveInXMLTIF();
        TraceManager.addDev("TIF=\n" + ret);
        return ret;
    }

    public boolean openTIF(String s) {
        TIFExchange tif = new TIFExchange();
        boolean ret = false;

        try {
            ret = tif.loadFromXMLTIF(s);
            if (ret) {
                tm = tif.getTURTLEModeling();
                tmState = 0;
                TraceManager.addDev("Got TIF");
                generateDesign();
            }
        } catch (Exception e) {
            TraceManager.addDev("Exception on TIF: " + e.getMessage());
        }
        return ret;
    }

    public boolean openSD(String s) {
        SDExchange sde = new SDExchange();
        boolean ret = false;

        try {
            ret = sde.loadFromXMLSD(s);
            if (ret) {
                //tm = tif.getTURTLEModeling();
                //tmState = 0;
                TraceManager.addDev("Got SD");
                generateIOD(sde.getHMSC(), sde.getMSC());
            }
        } catch (Exception e) {
            TraceManager.addDev("Exception on SD: " + e.getMessage());
        }
        return ret;
    }
Ludovic Apvrille's avatar
Ludovic Apvrille committed
	/*public void mergeChoices(boolean nonDeterministic) {
	  if (tm != null) {
	  tm.mergeChoices(nonDeterministic);
	  }
	  }*/
Ludovic Apvrille's avatar
Ludovic Apvrille committed
    public NCStructure getNCS() {
        return ncs;
    }

    public void generateRTLOTOS(File f) {
        TURTLETranslator tt = new TURTLETranslator(tm);
        rtlotos = tt.generateRTLOTOS();
        warnings = tt.getWarnings();
        nbRTLOTOS++;
        if (f != null) {
            saveInFile(f, rtlotos);
        }
        languageID = RT_LOTOS;
        mgui.setMode(MainGUI.RTLOTOS_OK);
    }

    public void generateFullLOTOS(File f) {
        reinitSIM();
        reinitDTA();
        reinitRG();
        reinitRGAUT();
        reinitRGAUTPROJDOT();
        //TraceManager.addDev("generate LOTOS");
        generateLOTOS(f);
    }

    public void generateLOTOS(File f) {
        //tm.print();
        TraceManager.addDev("Generating Lotos");
        TURTLETranslator tt = new TURTLETranslator(tm);
        rtlotos = tt.generateLOTOS(true);
        warnings = tt.getWarnings();
        TraceManager.addDev("Lotos generated");


        nbRTLOTOS++;
        if (f != null) {
            saveInFile(f, rtlotos);
        }
        TraceManager.addDev("LOTOS to file done");
        languageID = LOTOS;
        mgui.setMode(MainGUI.RTLOTOS_OK);
    }

    public void generateTPN(File f) {
        //tm.print();
        TURTLE2TPN t2tpn = new TURTLE2TPN(tm);
        tpn = t2tpn.generateTPN().toString();
        warnings = t2tpn.getWarnings();

        //  nbTPN ++;
        if (f != null) {
            TraceManager.addDev("Saving in file: " + f);
            saveInFile(f, tpn);
        }
        languageID = TPN;

        // For debug purpose
        //TraceManager.addDev(tpn);

        mgui.setMode(MainGUI.RTLOTOS_OK);
    }

    public List<String> generateAUT(String path) {
        TML2AUT tml2aut = new TML2AUT(tmlm);
        tml2aut.generateAutomatas(true);
        try {
            return tml2aut.saveInFiles(path);
        } catch (FileException fe) {
            return null;
        }
    }

    public boolean generateCCode(String directory, String compilationOptions) {

        //CheckingError ce;
        //int type;
        // TGComponent tgc;
        String applicationName;
        TMLModelCompiler CCode;

        if (tmap == null) {
            JOptionPane.showMessageDialog(mgui.frame, "C code is only generated from an architecture diagram with mapping information", "Control code generation failed", JOptionPane.INFORMATION_MESSAGE);
            return true;
        }
        // Get the file from DiplodocusPECPragma
        //List<TGComponent> components = mgui.getCurrentArchiPanel().tmlap.getComponentList();
        // Parse the PEC file and the library of code snippets for each DIPLODOCUS unit
        applicationName = tmap.getMappedTasks().get(0).getName().split("__")[0];        // Remember that it works only for one application
        CCode = new TMLModelCompiler(directory, applicationName, mgui.frame, mgui.getAllTMLCP(), tmap);

        // Issue #98: Use the passed directory
        File dir = new File(directory /*ConfigurationTTool.CCodeDirectory*/ + File.separator);

        if (!dir.exists()) {
            dir.mkdirs();
        }

        CCode.toTextFormat();

        try {
            if (directory.equals("")) {

                JOptionPane.showMessageDialog(mgui.frame,
                        "No directory for C code generation found in config.xml. The C code cannot be generated.",
                        "Control code generation failed", JOptionPane.INFORMATION_MESSAGE);
                return true;
            } else {
                SpecConfigTTool.checkAndCreateCCodeDir(directory);
                CCode.saveFile(directory + File.separator, applicationName);
            }
        } catch (Exception e) {
            JOptionPane.showMessageDialog(mgui.frame, "The application C files could not be saved: " + e.getMessage(), "Control code generation failed", JOptionPane.INFORMATION_MESSAGE);
            return true;
        }
        return false;
    }

Ludovic Apvrille's avatar
Ludovic Apvrille committed
    public boolean generateTMLTxt(String _title) {

        //This branch is activated if doing the syntax check from the architecture panel.
        //It generates the text TML for the architecture and the application + mapping information
        if (tmap != null) {
            TMLMappingTextSpecification<TGComponent> spec = new TMLMappingTextSpecification<>(_title);
            spec.toTextFormat(tmap);    //TMLMapping
Ludovic Apvrille's avatar
Ludovic Apvrille committed
            try {
                //TraceManager.addDev( "*** " + ConfigurationTTool.TMLCodeDirectory + File.separator );
                spec.saveFile(SpecConfigTTool.TMLCodeDirectory, "spec");
                FileUtils.saveFile(SpecConfigTTool.TMLCodeDirectory + "spec.xml", XMLSpec);
Ludovic Apvrille's avatar
Ludovic Apvrille committed
            } catch (Exception e) {
                TraceManager.addError("Files could not be saved: " + e.getMessage());
                return false;
            }
        }

        if (tmlcp != null) {         //Use the data structure filled by translateToTML... and pass it to the appropriate toTextFormat()
            TraceManager.addError("About to generate the TMLText for CPs");
            TMLCPTextSpecification specCP = new TMLCPTextSpecification(_title);

            //get the architecture panel and the nodes
            TMLArchiDiagramPanel tmlap = mgui.getTMLArchiDiagramPanels().get(0).tmlap;
            List<TGComponent> components = tmlap.getComponentList();
            Iterator<TGComponent> iterator = components.listIterator();
            TGComponent tgc;

            while (iterator.hasNext()) {
                tgc = iterator.next();

                if (tgc instanceof TMLArchiCPNode) {
                    TMLArchiCPNode node = (TMLArchiCPNode) tgc;
                    TraceManager.addDev("Found CP node: " + node.getName());
                    TraceManager.addDev("with mapping info: " + node.getMappedUnits());
                }
            }
Ludovic Apvrille's avatar
Ludovic Apvrille committed
            List<TMLCommunicationPatternPanel> tmlcpPanelsList = new ArrayList<TMLCommunicationPatternPanel>();
            //get the TMLCommunicationPatternPanels :)
            for (int i = 0; i < mgui.tabs.size(); i++) {
                TURTLEPanel panel = mgui.tabs.get(i);
Ludovic Apvrille's avatar
Ludovic Apvrille committed
                if (panel instanceof TMLCommunicationPatternPanel) {
                    tmlcpPanelsList.add((TMLCommunicationPatternPanel) panel);
                    TraceManager.addDev("Found TMLCommunicationPatternPanel: " + panel.toString());
                }
            }

            specCP.toTextFormat(tmlcp);          // the data structure tmlcp is filled with the info concerning the CP panel
            // from which the button is pressed. If there are multiple CP panels this operation must be repeated for each panel. It
            // should be no difficult to implement.
            try {
                specCP.saveFile(SpecConfigTTool.TMLCodeDirectory, "spec.tmlcp");
            } catch (Exception e) {
                TraceManager.addError("Writing TMLText for CPs, file could not be saved: " + e.getMessage());
                return false;
            }

        } else if (tmap == null) {
            //This branch is activated if doing the syntax check from the application panel.
            //It only generates the application TML text
            if (tmap == null) {
                TMLTextSpecification<TGComponent> spec = new TMLTextSpecification<>(_title);
                spec.toTextFormat(tmlm);        //TMLModeling
                try {
                    String XMLSpecTML = tmlm.toXML();
                    FileUtils.saveFile(SpecConfigTTool.TMLCodeDirectory + "spec.xml", XMLSpecTML);
Ludovic Apvrille's avatar
Ludovic Apvrille committed
                    spec.saveFile(SpecConfigTTool.TMLCodeDirectory, "spec.tml");
                } catch (Exception e) {
                    TraceManager.addError("File could not be saved: " + e.getMessage());
                    return false;
                }
            }


        }
        return true;    //temporary, just to check functionality
    }

    public boolean generateUPPAALFromTIF(String path, boolean debug, int nb, boolean choices, boolean variables) {
        TURTLE2UPPAAL turtle2uppaal = new TURTLE2UPPAAL(tm);
        turtle2uppaal.setChoiceDeterministic(choices);
        turtle2uppaal.setVariablesAsActions(variables);
        uppaal = turtle2uppaal.generateUPPAAL(debug, nb);
        TraceManager.addDev("Building relation table");
        uppaalTIFTable = turtle2uppaal.getRelationTIFUPPAAL();
        TraceManager.addDev("Building relation table done");
        uppaalTMLTable = null;

        languageID = UPPAAL;
        mgui.setMode(MainGUI.UPPAAL_OK);

        try {
            TraceManager.addDev("Saving specification in " + path + "\n");

            // DB: Moved from TURTLE2UPPAAL (introduced for project management)
            SpecConfigTTool.checkAndCreateUPPAALDir(path);

            turtle2uppaal.saveInFile(path);
            TraceManager.addDev("UPPAAL specification has been generated in " + path + "\n");
            return true;
        } catch (FileException fe) {
            TraceManager.addError("Exception: " + fe.getMessage());
            return false;
        }
    }

    public boolean generateUPPAALFromTML(String _path, boolean _debug, int _size, boolean choices) {
        TraceManager.addDev("Generate UPPAAL from TML");
        TML2UPPAAL tml2uppaal = new TML2UPPAAL(tmlm);
        //tml2uppaal.setChoiceDeterministic(choices);
        tml2uppaal.setSizeInfiniteFIFO(_size);
        uppaal = tml2uppaal.generateUPPAAL(_debug);
        uppaalTMLTable = tml2uppaal.getRelationTMLUPPAAL();
        uppaalTIFTable = null;
        languageID = UPPAAL;
        mgui.setMode(MainGUI.UPPAAL_OK);
        //uppaalTable = tml2uppaal.getRelationTIFUPPAAL(_debug);
        try {
            tml2uppaal.saveInFile(_path);
            return true;
        } catch (FileException fe) {
            TraceManager.addError("Exception: " + fe.getMessage());
            return false;
        }
    }

    public boolean generateUPPAALFromAVATAR(String _path) {
apvrille's avatar
apvrille committed
        long timeBeg, timeEnd;
        timeBeg = System.currentTimeMillis();
Ludovic Apvrille's avatar
Ludovic Apvrille committed
        if (avatarspec == null) {
            TraceManager.addDev("Null avatar spec");
            return false;
        }
        avatar2uppaal = new AVATAR2UPPAAL(avatarspec);
        //tml2uppaal.setChoiceDeterministic(choices);
        //tml2uppaal.setSizeInfiniteFIFO(_size);
        uppaal = avatar2uppaal.generateUPPAAL(true, optimizeAvatar);
        warnings = avatar2uppaal.getWarnings();
        uppaalTMLTable = null;
        uppaalTIFTable = null;
        languageID = UPPAAL;
        mgui.setMode(MainGUI.UPPAAL_OK);
        //uppaalTable = tml2uppaal.getRelationTIFUPPAAL(_debug);
        try {
            avatar2uppaal.saveInFile(_path);
apvrille's avatar
apvrille committed
            timeEnd = System.currentTimeMillis();
            TraceManager.addDev("Total time toUPPAAL: " + (timeEnd-timeBeg) + " ms");
Ludovic Apvrille's avatar
Ludovic Apvrille committed
            return true;
        } catch (FileException fe) {
            TraceManager.addError("Exception: " + fe.getMessage());
            return false;
        }
Ludovic Apvrille's avatar
Ludovic Apvrille committed
    }

    public AvatarSpecification getAvatarSpecification() {
        return avatarspec;
    }

    public AVATAR2UPPAAL getAvatar2Uppaal() {
        return avatar2uppaal;
    }

    public ProVerifOutputAnalyzer getProVerifOutputAnalyzer() {
        return this.avatar2proverif.getOutputAnalyzer();
    }

    public boolean generateProVerifFromAVATAR(String _path, int _stateReachability, boolean _typed, boolean allowPrivateChannelDuplication) {
        return generateProVerifFromAVATAR(_path, _stateReachability, _typed, allowPrivateChannelDuplication, "1");
    }

    public int calcSec() {
        int overhead = 0;
        //count # of insecure channels?
        return overhead;
    }

    public boolean channelAllowed(TMLMapping<TGComponent> map, TMLChannel chan) {
        TMLTask orig = chan.getOriginTask();
        TMLTask dest = chan.getDestinationTask();
        List<HwNode> path = getPath(map, orig, dest);
        for (HwNode node : path) {
            if (node instanceof HwBridge) {
                for (String rule : ((HwBridge) node).firewallRules) {
                    String t1 = rule.split("->")[0];
                    String t2 = rule.split("->")[1];
                    if (t1.equals(orig.getName().replaceAll("__", "::")) || t1.equals("*")) {
                        if (t2.equals(dest.getName().replaceAll("__", "::")) || t2.equals("*")) {
                            return false;
                        }
                    }
                }
            }
        }
        return true;
    }

    public List<HwNode> getPath(TMLMapping<TGComponent> map, TMLTask t1, TMLTask t2) {
        HwNode node1 = map.getHwNodeOf(t1);
        HwNode node2 = map.getHwNodeOf(t2);
        List<HwNode> path = new ArrayList<HwNode>();
        if (node1 == node2) {
            return path;
        }
        if (node1 != node2) {
            //Navigate architecture for node
            List<HwLink> links = map.getTMLArchitecture().getHwLinks();
            //  HwNode last = node1;
            List<HwNode> found = new ArrayList<HwNode>();
            List<HwNode> done = new ArrayList<HwNode>();
            Map<HwNode, List<HwNode>> pathMap = new HashMap<HwNode, List<HwNode>>();
            for (HwLink link : links) {
                if (link.hwnode == node1) {
                    found.add(link.bus);
                    List<HwNode> tmp = new ArrayList<HwNode>();
                    tmp.add(link.bus);
                    pathMap.put(link.bus, tmp);
                }
            }
            outerloop:
            while (found.size() > 0) {
                HwNode curr = found.remove(0);
                for (HwLink link : links) {
                    if (curr == link.bus) {
                        if (link.hwnode == node2) {
                            path = pathMap.get(curr);
                            break outerloop;
                        }
                        if (!done.contains(link.hwnode) && !found.contains(link.hwnode) && link.hwnode instanceof HwBridge) {
                            found.add(link.hwnode);
                            List<HwNode> tmp = new ArrayList<HwNode>(pathMap.get(curr));
                            tmp.add(link.hwnode);
                            pathMap.put(link.hwnode, tmp);
                        }
                    } else if (curr == link.hwnode) {
                        if (!done.contains(link.bus) && !found.contains(link.bus)) {
                            found.add(link.bus);
                            List<HwNode> tmp = new ArrayList<HwNode>(pathMap.get(curr));
                            tmp.add(link.bus);
                            pathMap.put(link.bus, tmp);
                        }
                    }
                }
                done.add(curr);
            }
        }
        return path;
    }

    public boolean commPath(TMLMapping<TGComponent> map, HwBridge firewallNode, TMLTask t1) {
        //Check if a task has any write communications that pass through firewallNode


        for (TMLChannel chan : map.getTMLModeling().getChannels(t1)) {
            if (!chan.isBasicChannel()) {
                //
            } else {
                if (t1 == chan.getOriginTask()) {
                    TMLTask originTask = chan.getOriginTask();
                    TMLTask destTask = chan.getDestinationTask();
                    if (pathExists(map, firewallNode, destTask) && pathExists(map, firewallNode, originTask) && pathIncludes(map, originTask, destTask, firewallNode)) {
                        System.out.println("found channel " + t1.getName());
                        return true;
                    } else {
                        System.out.println("NO Channel " + chan.getName());
                    }
                }
            }
        }
        return false;
    }

    public boolean pathIncludes(TMLMapping<TGComponent> map, TMLTask t1, TMLTask t2, HwBridge firewallNode) {
        //Check if a path between two tasks uses firewallnode
        boolean secure = true;
        List<HwLink> links = map.getTMLArchitecture().getHwLinks();
        HwExecutionNode node1 = map.getHwNodeOf(t1);
        HwExecutionNode node2 = map.getHwNodeOf(t2);
Ludovic Apvrille's avatar
Ludovic Apvrille committed
        List<HwNode> found = new ArrayList<HwNode>();
        List<HwNode> done = new ArrayList<HwNode>();
        List<HwNode> path = new ArrayList<HwNode>();
        Map<HwNode, List<HwNode>> pathMap = new HashMap<HwNode, List<HwNode>>();
        TraceManager.addDev("Links " + links);
        if (node1 == node2) {
            return false;
        }
        for (HwLink link : links) {
            if (link.hwnode == node1) {
                found.add(link.bus);
                List<HwNode> tmp = new ArrayList<HwNode>();
                tmp.add(link.bus);
                pathMap.put(link.bus, tmp);
            }
        }
        outerloop:
        while (found.size() > 0) {
            HwNode curr = found.remove(0);
            for (HwLink link : links) {
                if (curr == link.bus) {
                    if (link.hwnode == node2) {
                        path = pathMap.get(curr);
                        break outerloop;
                    }
                    if (!done.contains(link.hwnode) && !found.contains(link.hwnode) && link.hwnode instanceof HwBridge) {
                        found.add(link.hwnode);
                        List<HwNode> tmp = new ArrayList<HwNode>(pathMap.get(curr));
                        tmp.add(link.hwnode);
                        pathMap.put(link.hwnode, tmp);
                    }
                } else if (curr == link.hwnode) {
                    if (!done.contains(link.bus) && !found.contains(link.bus)) {
                        found.add(link.bus);
                        List<HwNode> tmp = new ArrayList<HwNode>(pathMap.get(curr));
                        tmp.add(link.bus);
                        pathMap.put(link.bus, tmp);
                    }
                }
            }
            done.add(curr);
        }
        if (path.size() == 0) {

            return true;
        } else {
            HwBus bus;
            //Check if all buses and bridges are private
            for (HwNode n : path) {
                if (n == firewallNode) {
                    return true;
                }
            }
        }
        return false;
    }


    public boolean pathExists(TMLMapping<TGComponent> map, HwBridge firewallNode, TMLTask t1) {
        //System.out.println("Checking path " + firewallNode.getName() + t1.getName());
        List<HwLink> links = map.getTMLArchitecture().getHwLinks();
        List<HwNode> found = new ArrayList<HwNode>();
        List<HwNode> done = new ArrayList<HwNode>();
        //List<HwNode> path = new ArrayList<HwNode>();

        HwExecutionNode node1 = map.getHwNodeOf(t1);
Ludovic Apvrille's avatar
Ludovic Apvrille committed

        //Map<HwNode, List<HwNode>> pathMap = new HashMap<HwNode, List<HwNode>>();
        for (HwLink link : links) {
            if (link.hwnode == node1) {
                found.add(link.bus);
            }
        }
        while (found.size() > 0) {
            HwNode curr = found.remove(0);
            for (HwLink link : links) {
                //System.out.println("LINK " + link.hwnode.getName() + " " + link.bus.getName());
                if (curr == link.bus) {

                    if (link.hwnode.getName().equals(firewallNode.getName())) {
                        return true;
                    }
                    if (!done.contains(link.hwnode) && !found.contains(link.hwnode) && link.hwnode instanceof HwBridge) {
                        found.add(link.hwnode);
                    }
                } else if (curr == link.hwnode) {
                    if (!done.contains(link.bus) && !found.contains(link.bus)) {
                        found.add(link.bus);
                    }
                }
            }
            done.add(curr);
        }

        return false;
    }

    public TMLMapping<TGComponent> drawFirewall(TMLMapping<TGComponent> map) {


        Map<String, Integer> channelIndexMap = new HashMap<String, Integer>();
        //
        //Request Index indicates channel or update rules
        //index = 0 : update rules
        //index = 1-n: channel
        int index = 1;
        TGComponent comp = map.getTMLModeling().getTGComponent();
        TMLComponentDesignPanel tmlcdp = (TMLComponentDesignPanel) comp.getTDiagramPanel().tp;
        // TMLComponentDesignPanel tmlcdp = map.getTMLCDesignPanel();
        TMLModeling<TGComponent> tmlm = map.getTMLModeling();
        TMLArchitecture archi = map.getArch();
        TURTLEPanel tmlap = map.getCorrespondanceList().getTG(archi.getFirstCPU()).getTDiagramPanel().tp;
        TMLActivityDiagramPanel firewallADP = null;
        TMLComponentDesignPanel tcp = tmlcdp;

        TMLArchiPanel newarch = null;

        TMLComponentTaskDiagramPanel tcdp = tmlcdp.tmlctdp;
        TMLComponentTaskDiagramPanel newtcdp = tcp.tmlctdp;
        if (TraceManager.devPolicy == TraceManager.TO_CONSOLE) {
            MainGUI gui = tmlcdp.getMainGUI();

            int arch = mgui.tabs.indexOf(tmlap);
            gui.cloneRenameTab(arch, "firewallArch");
            newarch = (TMLArchiPanel) gui.tabs.get(gui.tabs.size() - 1);
            int ind = gui.tabs.indexOf(tmlcdp);
            String tabName = gui.getTitleAt(tmlcdp);
            gui.cloneRenameTab(ind, "firewallDesign");
            tcp = (TMLComponentDesignPanel) gui.tabs.get(gui.tabs.size() - 1);
            newtcdp = tcp.tmlctdp;
            newarch.renameMapping(tabName, tabName + "_firewallDesign");

        } else {
            return null;
        }
        for (HwBridge firewallNode : map.getTMLArchitecture().getFirewalls()) {
            List<String> chansToRemove = new ArrayList<String>();
            TraceManager.addDev("Found firewall " + firewallNode.getName());
            TMLCPrimitiveComponent firewallComp = null;
            TMLADStartState adStart = null;
            //TMLADForEverLoop adLoop = null;
            TMLADChoice adChoice = null;
            TMLADChoice adChoice2 = null;
            TMLADChoice adChoiceMain = null;
            TMLADReadChannel adRC = null;
            TMLADReadRequestArg req = null;
            TMLADExecI exec = null;
            TMLADWriteChannel adWC = null;
            TMLADStopState adStop = null;
            TMLADStopState adStop2 = null;

            //Add a single connection to update rules
            boolean updateRulesAdded = false;


            int links = map.getArch().getLinkByHwNode(firewallNode).size();
            TraceManager.addDev("Links " + links);

            HwCPU cpu = new HwCPU(firewallNode.getName());
            map.getTMLArchitecture().replaceFirewall(firewallNode, cpu);

            //Replace Firewall on new Architecture diagram
            TGComponent firewallArchComp = null;
            for (TGComponent tg : newarch.tmlap.getComponentList()) {
                if (tg.getName().equals(firewallNode.getName())) {
                    firewallArchComp = tg;
                }
            }
            if (firewallArchComp != null) {
Ludovic Apvrille's avatar
Ludovic Apvrille committed
                String refTask = "";
                for (TGComponent tg : newarch.tmlap.getComponentList()) {
                    if (tg instanceof TMLArchiCPUNode) {
                        TMLArchiCPUNode tmpcpu = (TMLArchiCPUNode) tg;
                        if (tmpcpu.getArtifactList().size() != 0) {
                            TMLArchiArtifact art = tmpcpu.getArtifactList().get(0);
                            refTask = art.getReferenceTaskName();
                            break;
                        }