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 avatartranslator.intboolsolver.AvatarIBSolver;
import myutil.Conversion;
import myutil.TraceManager;
import translator.CheckingError;
import ui.avatarbd.*;
import ui.avatarsmd.*;

import java.awt.*;
import java.util.*;
import java.util.List;

/**
 * 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

    private Map<String, List<TAttribute>> typeAttributesMap;
    private Map<String, String> nameTypeMap;

    public AvatarDesignPanelTranslator(AvatarDesignPanel _adp) {
        adp = _adp;
        checkingErrors = new LinkedList<CheckingError>();
        warnings = new LinkedList<CheckingError>();
        listE = new CorrespondanceTGElement();

    }

    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<AvatarBDLibraryFunction> libraryFunctions = new LinkedList<AvatarBDLibraryFunction>();
        List<AvatarBDDataType> listOfDataTypes = new LinkedList<>();

        for (AvatarBDStateMachineOwner owner : _blocks)
            if (owner instanceof AvatarBDBlock)
                blocks.add((AvatarBDBlock) owner);
            else if (owner instanceof AvatarBDLibraryFunction)
                libraryFunctions.add((AvatarBDLibraryFunction) owner);
            else {
                CheckingError ce = new CheckingError(CheckingError.STRUCTURE_ERROR, owner.getOwnerName() + " is not a supported type");
                addCheckingError(ce);
            }

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

        //TraceManager.addDev("Getting graphical data types");
        if (adp != null) {
            AvatarBDPanel abdp = adp.getAvatarBDPanel();
            if (abdp != null) {
                as.addApplicationCode(abdp.getMainCode());
                for(TGComponent tgc: abdp.getAllComponentList()) {
                    if (tgc instanceof AvatarBDDataType) {
                        listOfDataTypes.add((AvatarBDDataType)(tgc));
                    }
                }
                // Find data types

            }
        }

        TraceManager.addDev("Nb of data types: " + listOfDataTypes.size());

        typeAttributesMap = new HashMap<String, List<TAttribute>>();
        nameTypeMap = new HashMap<String, String>();
        createDataTypes(as, listOfDataTypes);
        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);
        }

        if (checkingErrors.size() == 0) {
            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());
                }
                addCheckingError(ce);
            }


            ArrayList<AvatarError> listW = AvatarSyntaxChecker.checkSyntaxWarnings(as);
            for (AvatarError ar : listW) {
                UICheckingError ce;
                if (ar.firstAvatarElement != null) {
                    if (ar.secondAvatarElement == null) {
                        ce = new UICheckingError(CheckingError.BEHAVIOR_ERROR,
                                AvatarError.errorStrings[ar.error] + ": " + ar.firstAvatarElement.getName());
                    } else {
                        ce = new UICheckingError(CheckingError.BEHAVIOR_ERROR,
                                AvatarError.errorStrings[ar.error] + ": " +
                                        ar.firstAvatarElement.getName() + " / " + ar.secondAvatarElement.getName());
                    }
                } else {
                    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);
            }
        }

        as.makeAllTags();
        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, tgsp);
                    } 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 = AvatarIBSolver.parser.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("Safety 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("Safety Pragma " + _pragma + " improperly formatted");
            return false;
        } else if (returnVal == -1) {
            return false;
        } else {
            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("Safety 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("Safety 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("Safety 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, "Safety 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, "Safety 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, "Safety 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, "Safety 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, "Safety 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, "Safety 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, "Safety 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;
        char a;
        for (int i = startChar; i < expression.length(); i++) {
            a = expression.charAt(i);
            if (a == ')') {
                if (level == 0) {
                    return i;
                } else {
                    level--;
                }
            } else if (a == '(') {
                level++;
            }
        }
        return -1;
    }

    private boolean checkSymbols(String expression) {
        if (expression.matches(".*\\b\\|\\b.*") || expression.matches(".*\\b&\\b.*") || expression.contains("\\$") ||
                expression.contains(":") || expression.contains(";")) {
            return false;
        } else {
            return true;
        }
    }

    private String replaceOperators(String expression) {
        expression = expression.replaceAll("\\|\\|", "\\|").trim();
        expression = expression.replaceAll("&&", "&").trim();
        expression = expression.replaceAll("==", "=").trim();
        expression = expression.replaceAll("!=", "\\$").trim();
        expression = expression.replaceAll(">=", ":").trim();
        expression = expression.replaceAll("<=", ";").trim();
        expression = expression.replaceAll("\\bor\\b", "\\|").trim();
        expression = expression.replaceAll("\\band\\b", "&").trim();
        return expression;
    }

    private int getOperatorIndex(String expression) {
        int index;
        // find the last executed operator
        int i, level, priority;
        boolean subVar = true; //when a subtraction is only one one variable
        char a;
        level = 0;
        priority = 0;
        for (i = 0, index = -1; i < expression.length(); i++) {
            a = expression.charAt(i);
            switch (a) {
                case '|':
                    if (level == 0) {
                        index = i;
                        priority = 5;
                    }
                    break;
                case '&':
                    if (level == 0 && priority < 5) {
                        index = i;
                        priority = 4;
                    }
                    break;
                case '=':
                    if (level == 0 && priority < 4) {
                        index = i;
                        priority = 3;
                    }
                    subVar = true;
                    break;
                case '$':
                    if (level == 0 && priority < 4) {
                        index = i;
                        priority = 3;
                    }
                    subVar = true;
                    break;
                case '<':
                    if (level == 0 && priority < 3) {
                        index = i;
                        priority = 2;
                    }
                    subVar = true;
                    break;
                case '>':
                    if (level == 0 && priority < 3) {
                        index = i;
                        priority = 2;
                    }
                    subVar = true;
                    break;
                case ':':
                    if (level == 0 && priority < 3) {
                        index = i;
                        priority = 2;
                    }
                    subVar = true;
                    break;
                case ';':
                    if (level == 0 && priority < 3) {
                        index = i;
                        priority = 2;
                    }
                    subVar = true;
                    break;
                case '-':
                    if (level == 0 && !subVar && priority < 2) {
                        index = i;
                        priority = 1;
                    }
                    break;
                case '+':
                    if (level == 0 && !subVar && priority < 2) {
                        index = i;
                        priority = 1;
                    }
                    break;
                case '/':
                    if (level == 0 && priority == 0) {
                        index = i;
                    }
                    break;
                case '*':
                    if (level == 0 && priority == 0) {
                        index = i;
                    }
                    break;
                case '(':
                    level++;
                    subVar = true;
                    break;
                case ')':
                    level--;
                    subVar = false;
                    break;
                case ' ':
                    break;
                default:
                    subVar = false;
                    break;
            }
        }
        return index;
    }

    private int getType(char operator) {
        int optype;

        switch (operator) {
            case '=':