Skip to content
Snippets Groups Projects
GTURTLEModeling.java 373 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.
 */

Ludovic Apvrille's avatar
Ludovic Apvrille committed
import avatartranslator.AvatarSpecification;
import avatartranslator.toproverif.AVATAR2ProVerif;
import avatartranslator.totpn.AVATAR2TPN;
import avatartranslator.toturtle.AVATAR2TURTLE;
import avatartranslator.touppaal.AVATAR2UPPAAL;
import common.ConfigurationTTool;
import common.SpecConfigTTool;
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.SDExchange;
import tmatrix.RequirementModeling;
import tmltranslator.*;
import tmltranslator.modelcompiler.TMLModelCompiler;
import tmltranslator.toautomata.TML2AUT;
import tmltranslator.toautomata.TML2AUTviaLOTOS;
import tmltranslator.toavatar.TML2Avatar;
import tmltranslator.tosystemc.TML2SystemC;
import tmltranslator.touppaal.RelationTMLUPPAAL;
import tmltranslator.touppaal.TML2UPPAAL;
Ludovic Apvrille's avatar
Ludovic Apvrille committed
import tmltranslator.toturtle.*;
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.*;
Ludovic Apvrille's avatar
Ludovic Apvrille committed
import ui.avatarbd.AvatarBDLibraryFunction;
import ui.avatarbd.AvatarBDPanel;
import ui.avatarbd.AvatarBDStateMachineOwner;
import ui.avatarcd.AvatarCDPanel;
import ui.avatardd.ADDDiagramPanel;
import ui.avatarmad.AvatarMADPanel;
import ui.avatarmethodology.AvatarMethodologyDiagramPanel;
import ui.avatarpd.AvatarPDPanel;
import ui.avatarrd.AvatarRDPanel;
Ludovic Apvrille's avatar
Ludovic Apvrille committed
import ui.avatarsmd.AvatarSMDPanel;
import ui.avatarsmd.AvatarSMDState;
import ui.cd.*;
import ui.dd.*;
import ui.avatarsmd.*;
import ui.diplodocusmethodology.DiplodocusMethodologyDiagramPanel;
import ui.ebrdd.EBRDDPanel;
Ludovic Apvrille's avatar
Ludovic Apvrille committed
import ui.eln.ELNDiagramPanel;
import ui.syscams.SysCAMSComponentTaskDiagramPanel;
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.RequirementDiagramPanel;
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;
Ludovic Apvrille's avatar
Ludovic Apvrille committed
import ui.req.*;
Ludovic Apvrille's avatar
Ludovic Apvrille committed
import sddescription.*;
import sdtranslator.*;
import ddtranslator.*;
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;
    }

    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
577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822 823 824 825 826 827 828 829 830 831 832 833 834 835 836 837 838 839 840 841 842 843 844 845 846 847 848 849 850 851 852 853 854 855 856 857 858 859 860 861 862 863 864 865 866 867 868 869 870 871 872 873 874 875 876 877 878 879 880 881 882 883 884 885 886 887 888 889 890 891 892 893 894 895 896 897 898 899 900 901 902 903 904 905 906 907 908 909 910 911 912 913 914 915 916 917 918 919 920 921 922 923 924 925 926 927 928 929 930 931 932 933 934 935 936 937 938 939 940 941 942 943 944 945 946 947 948 949 950 951 952 953 954 955 956 957 958 959 960 961 962 963 964 965 966 967 968 969 970 971 972 973 974 975
                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 {
                    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) {
        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);
            return true;
        } catch (FileException fe) {
            TraceManager.addError("Exception: " + fe.getMessage());
            return false;
        }
    }

    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 = (HwExecutionNode) map.getHwNodeOf(t1);
        HwExecutionNode node2 = (HwExecutionNode) map.getHwNodeOf(t2);
        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 = (HwExecutionNode) map.getHwNodeOf(t1);

        //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;
                        }
Ludovic Apvrille's avatar
Ludovic Apvrille committed
                TMLArchiCPUNode newcpu = new TMLArchiCPUNode(firewallArchComp.getX() + 100, firewallArchComp.getY() + 100, newarch.tmlap.getMinX(), newarch.tmlap.getMaxX(), newarch.tmlap.getMinY(), newarch.tmlap.getMaxY(), true, null, newarch.tmlap);
                newcpu.setName("CPU" + firewallNode.getName());
                newarch.tmlap.replaceArchComponent(firewallArchComp, newcpu);
Ludovic Apvrille's avatar
Ludovic Apvrille committed
                //Add artifact
                TMLArchiArtifact hsmArt = new TMLArchiArtifact(newcpu.getX(), newcpu.getY(), newarch.tmlap.getMinX(), newarch.tmlap.getMaxX(), newarch.tmlap.getMinY(), newarch.tmlap.getMaxY(), true, newcpu, newarch.tmlap);
                newarch.tmlap.addComponent(hsmArt, newcpu.getX(), newcpu.getY(), true, true);
                hsmArt.setFullName(firewallNode.getName(), refTask);
            }