AvatarDesignPanelTranslator.java

/* Copyright or (C) or Copr. GET / ENST, Telecom-Paris, Ludovic Apvrille
 *
 * ludovic.apvrille AT enst.fr
 *
 * This software is a computer program whose purpose is to allow the
 * edition of TURTLE analysis, design and deployment diagrams, to
 * allow the generation of RT-LOTOS or Java code from this diagram,
 * and at last to allow the analysis of formal validation traces
 * obtained from external tools, e.g. RTL from LAAS-CNRS and CADP
 * from INRIA Rhone-Alpes.
 *
 * This software is governed by the CeCILL  license under French law and
 * abiding by the rules of distribution of free software.  You can  use,
 * modify and/ or redistribute the software under the terms of the CeCILL
 * license as circulated by CEA, CNRS and INRIA at the following URL
 * "http://www.cecill.info".
 *
 * As a counterpart to the access to the source code and  rights to copy,
 * modify and redistribute granted by the license, users are provided only
 * with a limited warranty  and the software's author,  the holder of the
 * economic rights,  and the successive licensors  have only  limited
 * liability.
 *
 * In this respect, the user's attention is drawn to the risks associated
 * with loading,  using,  modifying and/or developing or reproducing the
 * software by the user in light of its specific status of free software,
 * that may mean  that it is complicated to manipulate,  and  that  also
 * therefore means  that it is reserved for developers  and  experienced
 * professionals having in-depth computer knowledge. Users are therefore
 * encouraged to load and test the software's suitability as regards their
 * requirements in conditions enabling the security of their systems and/or
 * data to be ensured and,  more generally, to use and operate it in the
 * same conditions as regards security.
 *
 * The fact that you are presently reading this means that you have had
 * knowledge of the CeCILL license and that you accept its terms.
 */

package ui;

import avatartranslator.*;
import myutil.Conversion;
import myutil.TraceManager;
import translator.CheckingError;
import ui.avatarbd.*;
import ui.avatarsmd.*;

import java.util.*;

/**
 * Class AvatarDesignPanelTranslator
 * Creation: 18/05/2010
 *
 * @author Ludovic APVRILLE
 */
public class AvatarDesignPanelTranslator {

    private final AvatarDesignPanel adp;
    private final List<CheckingError> checkingErrors, warnings;
    private final CorrespondanceTGElement listE; // usual list
    //protected CorrespondanceTGElement listB; // list for particular element -> first element of group of blocks
    //protected List <TDiagramPanel> panels;
    private Map<String, List<TAttribute>> typeAttributesMap;
    private Map<String, String> nameTypeMap;

    public AvatarDesignPanelTranslator(AvatarDesignPanel _adp) {
        adp = _adp;
        //   reinit();
        // }

        //public void reinit() {
        checkingErrors = new LinkedList<CheckingError>();
        warnings = new LinkedList<CheckingError>();
        listE = new CorrespondanceTGElement();
        //panels = new LinkedList <TDiagramPanel>();
    }

    public List<CheckingError> getErrors() {
        return checkingErrors;
    }

    public List<CheckingError> getWarnings() {
        return warnings;
    }

    public CorrespondanceTGElement getCorrespondanceTGElement() {
        return listE;
    }

    public AvatarSpecification generateAvatarSpecification(List<AvatarBDStateMachineOwner> _blocks) {
        List<AvatarBDBlock> blocks = new LinkedList<AvatarBDBlock>();
        //	List<AvatarBDInterface> interfaces = new LinkedList<AvatarBDInterface>();
        List<AvatarBDLibraryFunction> libraryFunctions = new LinkedList<AvatarBDLibraryFunction>();

        for (AvatarBDStateMachineOwner owner : _blocks)
            if (owner instanceof AvatarBDBlock)
                blocks.add((AvatarBDBlock) owner);
                //  else if (owner instanceof AvatarBDInterface)
                //        interfaces.add((AvatarBDInterface) owner);
            else
                libraryFunctions.add((AvatarBDLibraryFunction) owner);

        AvatarSpecification as = new AvatarSpecification("avatarspecification", adp);

        if (adp != null) {
            AvatarBDPanel abdp = adp.getAvatarBDPanel();
            if (abdp != null) {
                as.addApplicationCode(abdp.getMainCode());
            }
        }
        typeAttributesMap = new HashMap<String, List<TAttribute>>();
        nameTypeMap = new HashMap<String, String>();
        createLibraryFunctions(as, libraryFunctions);
        createBlocks(as, blocks);
        //createInterfaces(as, interfaces);
        createRelationsBetweenBlocks(as, blocks);
        //createRelationsBetweenBlocksAndInterfaces(as, blocks, interfaces);
        makeBlockStateMachines(as);
        createPragmas(as, blocks);

        //TraceManager.addDev("Removing else guards");
        as.removeElseGuards();


        // Checking integer values
        ArrayList<AvatarElement> listOfBadInt = AvatarSyntaxChecker.useOfInvalidUPPAALNumericalValues(as, AvatarSpecification.UPPAAL_MAX_INT);
        // Adding warnings for each element
        for (AvatarElement ae : listOfBadInt) {
            UICheckingError ce = new UICheckingError(CheckingError.STRUCTURE_ERROR, "Integer expression outside UPPAAL range: " +
                    ae.toString() +
                    "-> UPPAAL verification may fail");
            ce.setTDiagramPanel(adp.getAvatarBDPanel());
            if (ae.getReferenceObject() instanceof TGComponent) {
                ce.setTGComponent((TGComponent) ae.getReferenceObject());
            }
            addWarning(ce);
        }

        //TraceManager.addDev("Removing else guards ... done");
        //System.out.println(as.toString());

        ArrayList<AvatarError> list = AvatarSyntaxChecker.checkSyntaxErrors(as);
        for (AvatarError ar : list) {
            UICheckingError ce = new UICheckingError(CheckingError.STRUCTURE_ERROR, AvatarError.errorStrings[ar.error]);
            ce.setTDiagramPanel(adp.getAvatarBDPanel());
            Object o = ar.firstAvatarElement.getReferenceObject();
            if (o instanceof TGComponent) {
                ce.setTGComponent((TGComponent) o);
                ce.setTDiagramPanel(((TGComponent) o).getTDiagramPanel());
            }
            addWarning(ce);
        }

        ArrayList<AvatarError> listW = AvatarSyntaxChecker.checkSyntaxWarnings(as);
        for (AvatarError ar : listW) {
            UICheckingError ce = new UICheckingError(CheckingError.BEHAVIOR_ERROR, AvatarError.errorStrings[ar.error]);
            ce.setTDiagramPanel(adp.getAvatarBDPanel());
            Object o = ar.firstAvatarElement.getReferenceObject();
            if (o instanceof TGComponent) {
                ce.setTGComponent((TGComponent) o);
                ce.setTDiagramPanel(((TGComponent) o).getTDiagramPanel());
            }
            addWarning(ce);
        }

        adp.abdp.repaint();
        return as;
    }

    private void createPragmas(AvatarSpecification _as, List<AvatarBDBlock> _blocks) {
        Iterator<TGComponent> iterator = adp.getAvatarBDPanel().getComponentList().listIterator();
        TGComponent tgc;
        AvatarBDPragma tgcn;
        AvatarBDSafetyPragma tgsp;
        AvatarBDPerformancePragma tgpp;
        String values[];
        String tmp;
        List<AvatarPragma> pragmaList;

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

            if (tgc instanceof AvatarBDPragma) {
                ErrorAccumulator errorAcc = new ErrorAccumulator(tgc, adp.getAvatarBDPanel());
                tgcn = (AvatarBDPragma) tgc;
                tgcn.syntaxErrors.clear();
                values = tgcn.getValues();
                for (int i = 0; i < values.length; i++) {
                    tmp = values[i].trim();
                    if ((tmp.startsWith("#") && (tmp.length() > 1))) {
                        tmp = tmp.substring(1, tmp.length()).trim();

                        //TraceManager.addDev("Reworking pragma =" + tmp);
                        pragmaList = AvatarPragma.createFromString(tmp, tgc, _as.getListOfBlocks(), typeAttributesMap, nameTypeMap, errorAcc);

                        //TraceManager.addDev("Reworked pragma =" + tmp);

                        for (AvatarPragma tmpPragma : pragmaList) {
                            if (tmpPragma instanceof AvatarPragmaConstant) {
                                AvatarPragmaConstant apg = (AvatarPragmaConstant) tmpPragma;
                                for (AvatarConstant ac : apg.getConstants()) {
                                    _as.addConstant(ac);
                                }
                            }
                            _as.addPragma(tmpPragma);
                            //TraceManager.addDev("Adding pragma:" + tmp);
                        }
                    } else {
                        tgcn.syntaxErrors.add(values[i]);
                    }
                }
            }

            if (tgc instanceof AvatarBDSafetyPragma) {
                tgsp = (AvatarBDSafetyPragma) tgc;
                values = tgsp.getValues();
                tgsp.syntaxErrors.clear();
                for (String s : values) {
                    // Remove data types from pragma
                    String prag = removeDataTypesFromPragma(s, _blocks);
                    if (checkSafetyPragma(prag, _blocks, _as, tgc)) {
                        _as.addSafetyPragma(prag, s);
                    } else {
                        tgsp.syntaxErrors.add(prag);
                    }
                }
            }

            if (tgc instanceof AvatarBDPerformancePragma) {
                tgpp = (AvatarBDPerformancePragma) tgc;
                values = tgpp.getValues();
                for (String s : values) {
                    AvatarPragmaLatency pragma = checkPerformancePragma(s, _blocks, _as, tgc);
                    if (pragma != null) {
                        _as.addLatencyPragma(pragma);
                    } else {
                        tgpp.syntaxErrors.add(s);
                    }
                }
            }
        }
    }

    public AvatarPragmaLatency checkPerformancePragma(String _pragma, List<AvatarBDBlock> _blocks, AvatarSpecification as, TGComponent tgc) {
        if (_pragma.contains("=") || (!_pragma.contains(">") && !_pragma.contains("<") && !_pragma.contains("?")) || !_pragma.contains("Latency(")) {
            UICheckingError ce = new UICheckingError(CheckingError.STRUCTURE_ERROR, "No latency expression found in pragma " + _pragma);
            ce.setTDiagramPanel(adp.getAvatarBDPanel());
            ce.setTGComponent(tgc);
            addWarning(ce);
            TraceManager.addDev("No latency expression found in pragma " + _pragma);
            return null;
        }

        String pragma = _pragma.trim();
        pragma = pragma.split("Latency\\(")[1];
        //Find first block.state


        String p1 = pragma.split(",")[0];
        //Throw error if lack of '.' in block.signal
        if (!p1.contains(".")) {
            UICheckingError ce = new UICheckingError(CheckingError.STRUCTURE_ERROR, "Invalid block.signal format in pragma " + _pragma);
            ce.setTDiagramPanel(adp.getAvatarBDPanel());
            ce.setTGComponent(tgc);
            addWarning(ce);
            TraceManager.addDev("Invalid block.signal format in pragma " + _pragma);
            return null;
        }
        String block1 = p1.split("\\.")[0];
        String state1 = p1.split("\\.", -1)[1];
        AvatarBlock bl1;
        AvatarStateMachineElement st1 = null;
        List<String> id1 = new ArrayList<String>();
        bl1 = as.getBlockWithName(block1);
        if (bl1 == null) {
            UICheckingError ce = new UICheckingError(CheckingError.STRUCTURE_ERROR, "Block " + block1 + " in pragma does not exist");
            ce.setTDiagramPanel(adp.getAvatarBDPanel());
            ce.setTGComponent(tgc);
            addWarning(ce);
            TraceManager.addDev("Block " + block1 + " in pragma does not exist");
            return null;
        }
        AvatarStateMachine asm = bl1.getStateMachine();
        for (AvatarActionOnSignal aaos : asm.getAllAOSWithName(state1)) {
            if (aaos.getCheckLatency()) {
                id1.add((aaos.getSignal().isIn() ? "Receive signal" : "Send signal") + "-" + aaos.getSignal().getName() + ":" + aaos.getID());
                st1 = aaos;
            }
        }
        AvatarState astate1 = asm.getStateWithName(state1);
        if (astate1 != null) {
            if (astate1.getCheckLatency()) {
                id1.add("State-" + state1 + ":" + astate1.getID());
                st1 = astate1;
            }
        }

        if (id1.size() == 0) {
            UICheckingError ce = new UICheckingError(CheckingError.STRUCTURE_ERROR, "Cannot find checkable state " + block1 + "." + state1 + " in pragma");
            ce.setTDiagramPanel(adp.getAvatarBDPanel());
            ce.setTGComponent(tgc);
            addWarning(ce);
            TraceManager.addDev("Cannot find checkable state " + block1 + "." + state1 + " in pragma");
            return null;
        }


        //Find second block.signal
        //Throw error if lack of '.'


        String p2 = pragma.split(",")[1].split("\\)")[0];
        if (!p2.contains(".")) {
            UICheckingError ce = new UICheckingError(CheckingError.STRUCTURE_ERROR, "Invalid block.signal format in pragma " + _pragma);
            ce.setTDiagramPanel(adp.getAvatarBDPanel());
            ce.setTGComponent(tgc);
            addWarning(ce);
            TraceManager.addDev("Invalid block.signal format");
            return null;
        }

        String block2 = p2.split("\\.")[0];
        String state2 = p2.split("\\.", -1)[1];


        AvatarBlock bl2;
        AvatarStateMachineElement st2 = null;

        bl2 = as.getBlockWithName(block2);
        if (bl2 == null) {
            UICheckingError ce = new UICheckingError(CheckingError.STRUCTURE_ERROR, "Block " + block2 + " in pragma does not exist");
            ce.setTDiagramPanel(adp.getAvatarBDPanel());
            ce.setTGComponent(tgc);
            addWarning(ce);
            TraceManager.addDev("Block " + block2 + " in pragma does not exist");
            return null;
        }
        asm = bl2.getStateMachine();

        List<String> id2 = new ArrayList<String>();
        for (AvatarActionOnSignal aaos : asm.getAllAOSWithName(state2)) {

            if (aaos.getCheckLatency()) {
                id2.add((aaos.getSignal().isIn() ? "Receive signal" : "Send signal") + "-" + aaos.getSignal().getName() + ":" + aaos.getID());
                st2 = aaos;
            }
        }

        AvatarState astate2 = asm.getStateWithName(state2);
        if (astate2 != null) {
            if (astate2.getCheckLatency()) {
                id2.add("State-" + state2 + ":" + astate2.getID());
                st2 = astate2;
            }
        }

        if (id2.size() == 0) {
            UICheckingError ce = new UICheckingError(CheckingError.STRUCTURE_ERROR, "Cannot find checkable state " + block2 + "." + state2 + " in pragma");
            ce.setTDiagramPanel(adp.getAvatarBDPanel());
            ce.setTGComponent(tgc);
            addWarning(ce);
            TraceManager.addDev("Cannot find checkable state " + block2 + "." + state2 + " in pragma");
            return null;
        }


        String equation = pragma.split("\\)")[1];
        equation = equation.replaceAll(" ", "");
        int symbolType = 0;
        int time = 0;
        if (equation.substring(0, 1).equals("<")) {
            symbolType = AvatarPragmaLatency.lessThan;
            try {
                time = Integer.valueOf(equation.split("<")[1]);
            } catch (Exception e) {
                UICheckingError ce = new UICheckingError(CheckingError.STRUCTURE_ERROR, "Invalid number format in " + _pragma);
                ce.setTDiagramPanel(adp.getAvatarBDPanel());
                ce.setTGComponent(tgc);
                addWarning(ce);
                TraceManager.addDev("Invalid number format");
                return null;
            }
        } else if (equation.substring(0, 1).equals(">")) {
            symbolType = AvatarPragmaLatency.greaterThan;
            try {
                time = Integer.valueOf(equation.split(">")[1]);
            } catch (Exception e) {
                UICheckingError ce = new UICheckingError(CheckingError.STRUCTURE_ERROR, "Invalid number format in " + _pragma);
                ce.setTDiagramPanel(adp.getAvatarBDPanel());
                ce.setTGComponent(tgc);
                addWarning(ce);
                TraceManager.addDev("Invalid number format");
                return null;
            }
        } else if (equation.substring(0, 1).equals("?")) {
            symbolType = AvatarPragmaLatency.query;
        } else {
            UICheckingError ce = new UICheckingError(CheckingError.STRUCTURE_ERROR, "no latency expression found in " + _pragma);
            ce.setTDiagramPanel(adp.getAvatarBDPanel());
            ce.setTGComponent(tgc);
            addWarning(ce);
            TraceManager.addDev("No latency expression found");
            return null;
        }
        return new AvatarPragmaLatency(_pragma, tgc, bl1, st1, bl2, st2, symbolType, time, id1, id2, _pragma);


    }

    private String removeDataTypesFromPragma(String _pragma, List<AvatarBDBlock> _blocks) {
        // For each data type, and each attribute, check if it is present. IF yes
        // replace it with its value. If no value, the default initial value

        // Make all possible String DataType.elt
        //TraceManager.addDev("removeDataTypesFromPragma in " + _pragma);
        Vector<String> dataType;

        if (_blocks.size() < 1) {
            return _pragma;
        }

        TDiagramPanel tdp = _blocks.get(0).getTDiagramPanel();
        dataType = tdp.getAllDataTypes();

        /*for(AvatarBDBlock b: _blocks) {
            for (TAttribute a : b.getAttributeList()) {
                TraceManager.addDev("Analyzing attribute  " + a.getId() + " / type" + a.getType() + " in block " + b.getBlockName());
                if (a.isAvatarDefault()) {
                    TraceManager.addDev("Adding type " + a.getType());
                    dataType.add(a.getTypeOther());
                }
            }
        }*/

        if (dataType.size() == 0) {
            //TraceManager.addDev("No Datatype");
            return _pragma;
        }

        // At least one DataType

        for (String dt : dataType) {
            List<TAttribute> attr = adp.getAvatarBDPanel().getAttributesOfDataType(dt);
            if (attr != null) {
                //TraceManager.addDev("Found " + attr.size() + " attributes in " + dt);
                for (TAttribute t : attr) {
                    _pragma = removeDataTypesAttrFromPragma(_pragma, dt, t);
                }
            }
        }

        return _pragma;
    }

    private String removeDataTypesAttrFromPragma(String _pragma, String _dataType, TAttribute _t) {
        String init = _t.getInitialValue();
        if (init == null) {
            return _pragma;
        }

        String loc = _dataType + "." + _t.getId();

        // Replace in pragmas loc by its value init
        // We must be sure to correctly identify loc
        _pragma = AvatarExpressionSolver.replaceVariable(_pragma, loc, init);

        //TraceManager.addDev("PRAGMA: new pragma=" + _pragma);

        return _pragma;
    }

    public boolean checkSafetyPragma(String _pragma, List<AvatarBDBlock> _blocks, AvatarSpecification as, TGComponent tgc) {
        //Todo: check types
        //Todo: handle complex types
        _pragma = _pragma.trim();

        if (_pragma.compareTo("") == 0) {
            // empty pragma
            return false;
        }

        //remove expected result letter from the start if present
        if (_pragma.matches("^[TtFf]\\s.*")) {
            _pragma = _pragma.substring(2).trim();
        }

        if (_pragma.contains("=") && !(_pragma.contains("==") || _pragma.contains("<=") || _pragma.contains(">=") || _pragma.contains("!="))) {
            //not a query
            UICheckingError ce = new UICheckingError(CheckingError.STRUCTURE_ERROR, "Pragma " + _pragma + " cannot be parsed");
            ce.setTDiagramPanel(adp.getAvatarBDPanel());
            ce.setTGComponent(tgc);
            addWarning(ce);
            TraceManager.addDev("Safety Pragma " + _pragma + " cannot be parsed");
            return false;
        }

        int indexOfWrongLeadsTo = _pragma.indexOf("->");
        if (indexOfWrongLeadsTo > 0) {
            if (_pragma.charAt(indexOfWrongLeadsTo - 1) != '-') {
                //not a query
                UICheckingError ce = new UICheckingError(CheckingError.STRUCTURE_ERROR, "Pragma " + _pragma + " uses an invalid operator(->). Maybe you wanted to use \"-->\" instead?");
                ce.setTDiagramPanel(adp.getAvatarBDPanel());
                ce.setTGComponent(tgc);
                addWarning(ce);
                TraceManager.addDev("Safety Pragma " + _pragma + " cannot be parsed");
                return false;
            }
        }


        String header = _pragma.split(" ")[0];
        if (_pragma.contains("-->")) {
            //will be implies
            _pragma = _pragma.replaceAll(" ", "");
            String state1 = _pragma.split("-->")[0];
            String state2 = _pragma.split("-->")[1];
            //    System.out.println("checking... " + state1 + " " + state2);
//            if (!state1.contains(".") || !state2.contains(".")) {
//                TraceManager.addDev("Safety Pragma " + _pragma + " cannot be parsed: missing '.'");
//                return false;
//            }
            if (!statementParser(state1, as, _pragma, tgc)) {
                return false;
            }
            //check the second half of implies
            if (!statementParser(state2, as, _pragma, tgc)) {
                return false;
            }
        } else if (header.equals("E[]") || header.equals("E<>") || header.equals("A[]") || header.equals("A<>")) {
            String state = _pragma.replace("E[]", "").replace("A[]", "").replace("E<>", "").replace("A<>", "").replaceAll(" ", "");
            state = state.trim();
            // if (!state.contains("||") && !state.contains("&&")){
            if (!statementParser(state, as, _pragma, tgc)) {
                return false;
            }
            //}


        } else {
            UICheckingError ce = new UICheckingError(CheckingError.STRUCTURE_ERROR, "Pragma " + _pragma + " cannot be parsed: wrong or missing CTL header");
            ce.setTDiagramPanel(adp.getAvatarBDPanel());
            ce.setTGComponent(tgc);
            addWarning(ce);
            TraceManager.addDev("Safety Pragma " + _pragma + " cannot be parsed");
            return false;
        }
        return true;
    }

    private boolean statementParser(String state, AvatarSpecification as, String _pragma, TGComponent tgc) {
        //check the syntax of a single statement

        if (!checkSymbols(state)) {
            UICheckingError ce = new UICheckingError(CheckingError.STRUCTURE_ERROR, "Safety Pragma " + _pragma + " cannot be parsed");
            ce.setTDiagramPanel(adp.getAvatarBDPanel());
            ce.setTGComponent(tgc);
            addWarning(ce);
            TraceManager.addDev("UPPAAL Pragma " + _pragma + " cannot be parsed");
            return false;
        }

        state = replaceOperators(state);
        int returnVal = statementParserRec(state, as, _pragma, tgc);
        if (returnVal == 1) {
            UICheckingError ce = new UICheckingError(CheckingError.STRUCTURE_ERROR, "Safety Pragma " + _pragma + " has invalid return type");
            ce.setTDiagramPanel(adp.getAvatarBDPanel());
            ce.setTGComponent(tgc);
            addWarning(ce);
            TraceManager.addDev("UPPAAL Pragma " + _pragma + " improperly formatted");
            return false;
        } else if (returnVal == -1) {
            return false;
        } else {
            return true;
        }

        //Divide into simple statements

//        String[] split = state.split("[|&]+");
//        //     System.out.println("split " + split[0]);
//        if (split.length > 1) {
//            boolean validity = true;
//            for (String fragment : split) {
//                if (fragment.length() > 2) {
//                    validity = validity && statementParser(fragment, as, _pragma, tgc);
//                }
//            }
//            return validity;
//        }
//        String number = "[0-9]+";
//        String bo = "(?i)true|false";
//        if (state.contains("=") || state.contains("<") || state.contains(">")) {
//            String state1 = state.split("==|>(=)?|!=|<(=)?")[0];
//            String state2 = state.split("==|>(=)?|!=|<(=)?")[1];
//            if (!state1.contains(".")) {
//                UICheckingError ce = new UICheckingError(CheckingError.STRUCTURE_ERROR, "Pragma " + _pragma + " cannot be parsed: missing '.'");
//                ce.setTDiagramPanel(adp.getAvatarBDPanel());
//                ce.setTGComponent(tgc);
//                addWarning(ce);
//
//                TraceManager.addDev("Safety Pragma " + _pragma + " cannot be parsed: missing '.'");
//                return false;
//            }
//
//            String block1 = state1.split("\\.", 2)[0];
//            String attr1 = state1.split("\\.", 2)[1];
//            if (attr1.contains(".")) {
//                UICheckingError ce = new UICheckingError(CheckingError.STRUCTURE_ERROR, "Complex UPPAAL Pragma attribute " + attr1 + " must contain __ and not .");
//                ce.setTDiagramPanel(adp.getAvatarBDPanel());
//                ce.setTGComponent(tgc);
//                addWarning(ce);
//
//                TraceManager.addDev("Complex Safety Pragma attribute " + attr1 + " must contain __ and not .");
//                return false;
//            }
//
//            attr1 = attr1.replace(".", "__");
//            AvatarType p1Type = AvatarType.UNDEFINED;
//            AvatarBlock bl1 = as.getBlockWithName(block1);
//            if (bl1 != null) {
//                //AvatarStateMachine asm = bl1.getStateMachine();
//                if (bl1.getIndexOfAvatarAttributeWithName(attr1) == -1) {
//                    UICheckingError ce = new UICheckingError(CheckingError.STRUCTURE_ERROR, "UPPAAL Pragma " + _pragma + " contains invalid attribute name " + attr1);
//                    ce.setTDiagramPanel(adp.getAvatarBDPanel());
//                    ce.setTGComponent(tgc);
//                    addWarning(ce);
//                    TraceManager.addDev("Safety Pragma " + _pragma + " contains invalid attribute name " + attr1);
//                    return false;
//                } else {
//                    int ind = bl1.getIndexOfAvatarAttributeWithName(attr1);
//                    AvatarAttribute attr = bl1.getAttribute(ind);
//                    p1Type = attr.getType();
//                }
//            } else {
//                UICheckingError ce = new UICheckingError(CheckingError.STRUCTURE_ERROR, "UPPAAL Pragma " + _pragma + " contains invalid block name " + block1);
//                ce.setTDiagramPanel(adp.getAvatarBDPanel());
//                ce.setTGComponent(tgc);
//                addWarning(ce);
//                TraceManager.addDev("Safety Pragma " + _pragma + " contains invalid block name " + block1);
//                return false;
//            }
//
//
//            if (state2.contains(".")) {
//                String block2 = state2.split("\\.", 2)[0];
//                String attr2 = state2.split("\\.", 2)[1];
//                if (attr2.contains(".")) {
//                    UICheckingError ce = new UICheckingError(CheckingError.STRUCTURE_ERROR, "Complex UPPAAL Pragma attribute " + attr2 + " must contain __ and not .");
//                    ce.setTDiagramPanel(adp.getAvatarBDPanel());
//                    ce.setTGComponent(tgc);
//                    addWarning(ce);
//                    TraceManager.addDev("Complex Safety Pragma attribute " + attr2 + " must contain __ and not .");
//                    return false;
//                }
//
//                AvatarBlock bl2 = as.getBlockWithName(block2);
//                if (bl2 != null) {
//                    if (bl2.getIndexOfAvatarAttributeWithName(attr2) == -1) {
//                        UICheckingError ce = new UICheckingError(CheckingError.STRUCTURE_ERROR, "UPPAAL Pragma " + _pragma + " contains invalid attribute name " + attr2);
//                        ce.setTDiagramPanel(adp.getAvatarBDPanel());
//                        ce.setTGComponent(tgc);
//                        addWarning(ce);
//                        TraceManager.addDev("Safety Pragma " + _pragma + " contains invalid attribute name " + attr2);
//                        return false;
//                    }
//                    int ind = bl2.getIndexOfAvatarAttributeWithName(attr2);
//                    AvatarAttribute attr = bl2.getAttribute(ind);
//                    p1Type = attr.getType();
//
//                } else {
//                    UICheckingError ce = new UICheckingError(CheckingError.STRUCTURE_ERROR, "Safety Pragma " + _pragma + " contains invalid block name " + block2);
//                    ce.setTDiagramPanel(adp.getAvatarBDPanel());
//                    ce.setTGComponent(tgc);
//                    addWarning(ce);
//                    TraceManager.addDev("Safety Pragma " + _pragma + " contains invalid block name " + block2);
//                    return false;
//                }
//            } else {
//                if (state2.matches(number)) {
//                    if (p1Type != AvatarType.INTEGER) {
//                        UICheckingError ce = new UICheckingError(CheckingError.STRUCTURE_ERROR, "UPPAAL Pragma " + _pragma + " has incompatible types");
//                        ce.setTDiagramPanel(adp.getAvatarBDPanel());
//                        ce.setTGComponent(tgc);
//                        addWarning(ce);
//                        TraceManager.addDev("Safety Pragma " + _pragma + " has incompatible types");
//                        return false;
//                    }
//                } else if (state2.matches(bo)) {
//                    if (p1Type != AvatarType.BOOLEAN) {
//                        UICheckingError ce = new UICheckingError(CheckingError.STRUCTURE_ERROR, "UPPAAL Pragma " + _pragma + " has incompatible types");
//                        ce.setTDiagramPanel(adp.getAvatarBDPanel());
//                        ce.setTGComponent(tgc);
//                        addWarning(ce);
//                        TraceManager.addDev("Safety Pragma " + _pragma + " has incompatible types");
//                        return false;
//                    }
//                } else {
//                    UICheckingError ce = new UICheckingError(CheckingError.STRUCTURE_ERROR, "UPPAAL Pragma " + _pragma + " cannot be parsed");
//                    ce.setTDiagramPanel(adp.getAvatarBDPanel());
//                    ce.setTGComponent(tgc);
//                    addWarning(ce);
//                    TraceManager.addDev("Safety Pragma " + _pragma + " cannot be parsed");
//                    return false;
//                }
//            }
//        } else {
//            if (!state.contains(".")) {
//                UICheckingError ce = new UICheckingError(CheckingError.STRUCTURE_ERROR, "Safety Pragma " + _pragma + " cannot be parsed: missing '.'");
//                ce.setTDiagramPanel(adp.getAvatarBDPanel());
//                ce.setTGComponent(tgc);
//                addWarning(ce);
//                TraceManager.addDev("UPPAAL Pragma " + _pragma + " improperly formatted");
//                return false;
//            }
//            String block1 = state.split("\\.", 2)[0];
//            String attr1 = state.split("\\.", 2)[1];
//            if (attr1.contains(".")) {
//                UICheckingError ce = new UICheckingError(CheckingError.STRUCTURE_ERROR, "Complex Safety Pragma attribute " + attr1 + " must contain __ and not .");
//                ce.setTDiagramPanel(adp.getAvatarBDPanel());
//                ce.setTGComponent(tgc);
//                addWarning(ce);
//                TraceManager.addDev("Complex Safety Pragma attribute " + attr1 + " must contain __ and not .");
//                return false;
//            }
//            AvatarBlock bl1 = as.getBlockWithName(block1);
//            if (bl1 != null) {
//                AvatarStateMachine asm = bl1.getStateMachine();
//                if (bl1.getIndexOfAvatarAttributeWithName(attr1) == -1 && asm.getStateWithName(attr1) == null) {
//                    UICheckingError ce = new UICheckingError(CheckingError.STRUCTURE_ERROR, "UPPAAL Pragma " + _pragma + " contains invalid attribute or state name " + attr1);
//                    ce.setTDiagramPanel(adp.getAvatarBDPanel());
//                    ce.setTGComponent(tgc);
//                    addWarning(ce);
//
//                    TraceManager.addDev("Safety Pragma " + _pragma + " contains invalid attribute or state name " + attr1);
//                    return false;
//                }
//
//                int ind = bl1.getIndexOfAvatarAttributeWithName(attr1);
//                if (ind != -1) {
//                    AvatarAttribute attr = bl1.getAttribute(ind);
//                    if (attr.getType() != AvatarType.BOOLEAN) {
//                        UICheckingError ce = new UICheckingError(CheckingError.STRUCTURE_ERROR, "UPPAAL Pragma " + _pragma + " performs query on non-boolean attribute");
//                        ce.setTDiagramPanel(adp.getAvatarBDPanel());
//                        ce.setTGComponent(tgc);
//                        addWarning(ce);
//                        TraceManager.addDev("Safety Pragma " + _pragma + " performs query on non-boolean attribute");
//                        return false;
//                    }
//                }
//            } else {
//                UICheckingError ce = new UICheckingError(CheckingError.STRUCTURE_ERROR, "UPPAAL Pragma " + _pragma + " contains invalid block name " + block1);
//                ce.setTDiagramPanel(adp.getAvatarBDPanel());
//                ce.setTGComponent(tgc);
//                addWarning(ce);
//                TraceManager.addDev("Safety Pragma " + _pragma + " contains invalid block name " + block1);
//                return false;
//            }
//        }
//        return true;
    }

    private int statementParserRec(String state, AvatarSpecification as, String _pragma, TGComponent tgc) {
        //returns -1 for errors, 0 for boolean result type, and 1 for int result type
        boolean isNot = false;
        boolean isNegated = false;

        state = removeExternalBrackets(state);

        if (state.startsWith("not(") || state.startsWith("!(")) {
            state = removeNot(state);
            isNot = true;
        }

        if (state.startsWith("-(")) {
            state = removeNegated(state);
            isNegated = true;
        }

        if (!state.matches("^.+[\\+\\-<>=:;\\$&\\|\\*/].*$")) {
            // attribute
            if (state.startsWith("-") && isNegated != true) {
                state = removeNegated2(state);
                isNegated = true;
            }

            if (state.equals("true") || state.equals("false")) {
                if (isNegated) {
                    UICheckingError ce = new UICheckingError(CheckingError.STRUCTURE_ERROR, "Safety Pragma " + _pragma + " negation of a boolean value");
                    ce.setTDiagramPanel(adp.getAvatarBDPanel());
                    ce.setTGComponent(tgc);
                    addWarning(ce);
                    TraceManager.addDev("UPPAAL Pragma " + _pragma + " improperly formatted");
                    return -1;
                }
                return 0;
            } else if (state.matches("-?\\d+")) {
                if (isNot) {
                    UICheckingError ce = new UICheckingError(CheckingError.STRUCTURE_ERROR, "Safety Pragma " + _pragma + " not of an integer value");
                    ce.setTDiagramPanel(adp.getAvatarBDPanel());
                    ce.setTGComponent(tgc);
                    addWarning(ce);
                    TraceManager.addDev("UPPAAL Pragma " + _pragma + " improperly formatted");
                    return -1;
                }
                return 1;
            } else {
                if (!state.contains(".")) {
                    UICheckingError ce = new UICheckingError(CheckingError.STRUCTURE_ERROR, "Safety Pragma " + _pragma + " cannot be parsed: missing '.'");
                    ce.setTDiagramPanel(adp.getAvatarBDPanel());
                    ce.setTGComponent(tgc);
                    addWarning(ce);
                    TraceManager.addDev("UPPAAL Pragma " + _pragma + " improperly formatted");
                    return -1;
                }
                String block = state.split("\\.", 2)[0];
                String attr = state.split("\\.", 2)[1];
                if (attr.contains(".")) {
                    UICheckingError ce = new UICheckingError(CheckingError.STRUCTURE_ERROR, "Complex Safety Pragma attribute " + attr + " must contain __ and not .");
                    ce.setTDiagramPanel(adp.getAvatarBDPanel());
                    ce.setTGComponent(tgc);
                    addWarning(ce);
                    TraceManager.addDev("Complex Safety Pragma attribute " + attr + " must contain __ and not .");
                    return -1;
                }
                AvatarBlock bl = as.getBlockWithName(block);
                if (bl != null) {
                    AvatarStateMachine asm = bl.getStateMachine();
                    if (bl.getIndexOfAvatarAttributeWithName(attr) == -1 && asm.getStateWithName(attr) == null) {
                        UICheckingError ce = new UICheckingError(CheckingError.STRUCTURE_ERROR, "UPPAAL Pragma " + _pragma + " contains invalid attribute or state name " + attr);
                        ce.setTDiagramPanel(adp.getAvatarBDPanel());
                        ce.setTGComponent(tgc);
                        addWarning(ce);

                        TraceManager.addDev("Safety Pragma " + _pragma + " contains invalid attribute or state name " + attr);
                        return -1;
                    }

                    int ind = bl.getIndexOfAvatarAttributeWithName(attr);
                    if (ind != -1) {
                        AvatarAttribute aa = bl.getAttribute(ind);
                        if (aa.getType() == AvatarType.BOOLEAN) {
                            return 0;
                        } else {
                            return 1;
                        }
                    } else {
                        //state as boolean condition
                        return 0;
                    }
                } else {
                    UICheckingError ce = new UICheckingError(CheckingError.STRUCTURE_ERROR, "UPPAAL Pragma " + _pragma + " contains invalid block name " + block);
                    ce.setTDiagramPanel(adp.getAvatarBDPanel());
                    ce.setTGComponent(tgc);
                    addWarning(ce);

                    TraceManager.addDev("Safety Pragma " + _pragma + " contains invalid block name " + block);
                    return -1;
                }
            }
        }

        int index = getOperatorIndex(state);

        if (index == -1) {
            UICheckingError ce = new UICheckingError(CheckingError.STRUCTURE_ERROR, "UPPAAL Pragma " + _pragma + " cannot parse " + state);
            ce.setTDiagramPanel(adp.getAvatarBDPanel());
            ce.setTGComponent(tgc);
            addWarning(ce);

            TraceManager.addDev("Safety Pragma " + _pragma + " cannot parse " + state);
            return -1;
        }

        char operator = state.charAt(index);

        //split and recur
        String leftState = state.substring(0, index).trim();
        String rightState = state.substring(index + 1, state.length()).trim();

        int optype = getType(operator);
        int optypel = statementParserRec(leftState, as, _pragma, tgc);
        int optyper = statementParserRec(rightState, as, _pragma, tgc);

        if (optypel == -1 || optyper == -1) {
            return -1;
        }

        UICheckingError ce;

        switch (optype) {
            case -1:
                ce = new UICheckingError(CheckingError.STRUCTURE_ERROR, "UPPAAL Pragma " + _pragma + " unrecognized " + operator);
                ce.setTDiagramPanel(adp.getAvatarBDPanel());
                ce.setTGComponent(tgc);
                addWarning(ce);

                TraceManager.addDev("Safety Pragma " + _pragma + " unrecognized operator " + operator);
                return -1;
            case 1:
                if (!(optypel == 1 && optyper == 1)) {
                    ce = new UICheckingError(CheckingError.STRUCTURE_ERROR, "UPPAAL Pragma " + _pragma + " expected integer attributes around " + operator);
                    ce.setTDiagramPanel(adp.getAvatarBDPanel());
                    ce.setTGComponent(tgc);
                    addWarning(ce);

                    TraceManager.addDev("Safety Pragma " + _pragma + " expected integer attributes around " + operator);
                    return -1;
                }
                break;
            case 0:
                if (!(optypel == 0 && optyper == 0)) {
                    ce = new UICheckingError(CheckingError.STRUCTURE_ERROR, "UPPAAL Pragma " + _pragma + " expected boolean attributes around " + operator);
                    ce.setTDiagramPanel(adp.getAvatarBDPanel());
                    ce.setTGComponent(tgc);
                    addWarning(ce);

                    TraceManager.addDev("Safety Pragma " + _pragma + " expected boolean attributes around " + operator);
                    return -1;
                }
                break;
            case 3:
                if (optypel != optyper) {
                    ce = new UICheckingError(CheckingError.STRUCTURE_ERROR, "UPPAAL Pragma " + _pragma + " has incompatible types around " + operator);
                    ce.setTDiagramPanel(adp.getAvatarBDPanel());
                    ce.setTGComponent(tgc);
                    addWarning(ce);

                    TraceManager.addDev("Safety Pragma " + _pragma + " has incompatible types around " + operator);
                    return -1;
                }
                break;
            default:
                break;
        }

        return getReturnType(operator);
    }

    private String removeNot(String expression) {
        if (expression.startsWith("not(")) {
            //not bracket must be closed in the last char
            int closingIndex = getClosingBracket(expression, 4);

            if (closingIndex == -1) {
                return expression;
            }
            if (closingIndex == expression.length() - 1) {
                //not(expression)
                return expression.substring(4, expression.length() - 1).trim();
            }
        } else if (expression.startsWith("!(")) {
            int closingIndex = getClosingBracket(expression, 2);

            if (closingIndex == -1) {
                return expression;
            }
            if (closingIndex == expression.length() - 1) {
                //not(expression)
                return expression.substring(2, expression.length() - 1).trim();
            }
        }
        return expression;
    }

    private String removeNegated(String expression) {
        if (expression.startsWith("-(")) {
            //not bracket must be closed in the last char
            int closingIndex = getClosingBracket(expression, 2);

            if (closingIndex == -1) {
                return expression;
            }
            if (closingIndex == expression.length() - 1) {
                //-(expression)
                return expression.substring(2, expression.length() - 1).trim();
            }
        }
        return expression;
    }

    private String removeNegated2(String expression) {
        if (expression.startsWith("-")) {
            return expression.substring(1, expression.length()).trim();
        }
        return expression;
    }

    private String removeExternalBrackets(String expression) {
        while (expression.startsWith("(") && expression.endsWith(")")) {
            if (getClosingBracket(expression, 1) == expression.length() - 1) {
                expression = expression.substring(1, expression.length() - 1).trim();
            } else {
                break;
            }
        }
        return expression;
    }

    private int getClosingBracket(String expression, int startChar) {
        int level = 0;