/* 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 avatartranslator;
import avatartranslator.intboolsolver.AvatarIBSExpressions;
import avatartranslator.intboolsolver.AvatarIBSolver;
import compiler.tmlparser.ParseException;
import compiler.tmlparser.SimpleNode;
import compiler.tmlparser.TMLExprParser;
import compiler.tmlparser.TokenMgrError;
import myutil.Conversion;
import myutil.IntExpressionEvaluator;
import myutil.NameChecker;
import myutil.TraceManager;
import myutil.intboolsolver.IBSExpressions;
import java.io.StringReader;
import java.util.ArrayList;
import java.util.List;
/**
* Class AvatarSyntaxChecker
* Creation: 21/05/2010
*
* @author Ludovic APVRILLE
* @version 1.0 21/05/2010
*/
public class AvatarSyntaxChecker {
// Errors are defined in AvatarError
private final static int UNUSED_ELEMENT = 10;
private final static int FIRST_UPPER_CASE = 11;
private final static int FIRST_LOWER_CASE = 12;
private final static int ERROR_IN_ELSE_GUARD = 13;
public AvatarSyntaxChecker() {
}
public static ArrayList<AvatarError> checkSyntaxErrors(AvatarSpecification avspec) {
ArrayList<AvatarError> errors = new ArrayList<>();
errors.addAll(checkNextASMSpec(avspec));
errors.addAll(checkMethodTypes(avspec));
errors.addAll(checkSignalTypes(avspec));
errors.addAll(checkSignalRelations(avspec));
errors.addAll(checkActionOnSignals(avspec));
errors.addAll(checkActions(avspec));
errors.addAll(checkASMLibraryFunctions(avspec));
errors.addAll(checkElseInGuards(avspec));
return errors;
}
public static ArrayList<AvatarError> checkSyntaxWarnings(AvatarSpecification avspec) {
ArrayList<AvatarError> warnings = new ArrayList<>();
//warnings.addAll(checkIsolatedElements(avspec));
warnings.addAll(checkNames(avspec));
return warnings;
}
public static ArrayList<AvatarError> checkIsolatedElements(AvatarSpecification avspec) {
ArrayList<AvatarError> warnings = new ArrayList<>();
for (AvatarBlock ab : avspec.getListOfBlocks()) {
warnings.addAll(checkIsolatedElements(avspec, ab));
}
return warnings;
}
public static ArrayList<AvatarError> checkIsolatedElements(AvatarSpecification avspec, AvatarBlock ab) {
ArrayList<AvatarError> warnings = new ArrayList<>();
AvatarStateMachine asm = ab.getStateMachine();
if (asm == null) {
return warnings;
}
List<AvatarStateMachineElement> unused = asm.getUnusedElements();
if (unused != null) {
for (AvatarStateMachineElement asme : unused) {
AvatarError warning = new AvatarError(avspec);
warning.firstAvatarElement = asme;
warning.secondAvatarElement = ab;
warning.error = UNUSED_ELEMENT;
warnings.add(warning);
}
}
return warnings;
}
public static ArrayList<AvatarError> checkNames(AvatarSpecification avspec) {
ArrayList<AvatarError> warnings = new ArrayList<>();
for(NameChecker.NamedElement ne: avspec.getSubNamedElements()) {
warnings.addAll(checkNames(avspec, ne));
}
return warnings;
}
public static ArrayList<AvatarError> checkNames(AvatarSpecification _avspec, NameChecker.NamedElement _ne) {
ArrayList<AvatarError> warnings = new ArrayList<>();
// Checking block name
//TraceManager.addDev("Checking name: " + _ne.getName());
if (_ne instanceof NameChecker.NameStartWithUpperCase) {
if (!NameChecker.checkName(_ne)) {
newError(_avspec, warnings, (AvatarElement) _ne, null, FIRST_UPPER_CASE);
}
} else if (_ne instanceof NameChecker.NameStartWithLowerCase) {
if (!NameChecker.checkName(_ne)) {
newError(_avspec, warnings, (AvatarElement) _ne, null, FIRST_LOWER_CASE);
}
}
for(NameChecker.NamedElement sub: _ne.getSubNamedElements()) {
//TraceManager.addDev("Checking sub name: " + sub.getName());
if (sub instanceof NameChecker.NameStartWithUpperCase) {
if (!NameChecker.checkName(sub)) {
newError(_avspec, warnings, (AvatarElement) _ne, (AvatarElement)sub, FIRST_UPPER_CASE);
}
} else if (sub instanceof NameChecker.NameStartWithLowerCase) {
if (!NameChecker.checkName(sub)) {
newError(_avspec, warnings, (AvatarElement) _ne, (AvatarElement)sub, FIRST_LOWER_CASE);
}
}
}
// Checking attribute, methods and signal names
/*for (AvatarAttribute aa: ab.getAttributes()) {
if (!Conversion.startsWithLowerCase(aa.getName())) {
newError(avspec, warnings, ab, aa, FIRST_LOWER_CASE);
}
}
for (AvatarMethod am: ab.getMethods()) {
if (!Conversion.startsWithLowerCase(am.getName())) {
newError(avspec, warnings, ab, am, FIRST_LOWER_CASE);
}
}
for (AvatarSignal as: ab.getSignals()) {
if (!Conversion.startsWithLowerCase(as.getName())) {
newError(avspec, warnings, ab, as, FIRST_LOWER_CASE);
}
}*/
return warnings;
}
public static ArrayList<AvatarError> checkNextASMSpec(AvatarSpecification avspec) {
ArrayList<AvatarError> errors = new ArrayList<>();
for (AvatarBlock ab : avspec.getListOfBlocks()) {
errors.addAll(checkNextASMBlock(avspec, ab));
}
return errors;
}
public static ArrayList<AvatarError> checkNextASMBlock(AvatarSpecification avspec, AvatarBlock ab) {
ArrayList<AvatarError> errors = new ArrayList<>();
AvatarStateMachine asm = ab.getStateMachine();
if (asm == null) {
AvatarError error = new AvatarError(avspec);
error.firstAvatarElement = ab;
error.secondAvatarElement = null;
error.error = 9;
errors.add(error);
} else {
for (AvatarStateMachineElement asme : asm.getListOfElements()) {
if (!((asme instanceof AvatarState) || (asme instanceof AvatarStopState) || (asme instanceof AvatarStartState))) {
if (asme.nexts.isEmpty()) {
AvatarError error = new AvatarError(avspec);
error.firstAvatarElement = asme;
error.secondAvatarElement = ab;
error.error = 8;
errors.add(error);
}
}
}
}
return errors;
}
public static ArrayList<AvatarError> checkASMLibraryFunctions(AvatarSpecification avspec) {
ArrayList<AvatarError> errors = new ArrayList<>();
for (AvatarLibraryFunction alf : avspec.getListOfLibraryFunctions()) {
errors.addAll(checkASMLibraryFunction(avspec, alf));
}
return errors;
}
public static ArrayList<AvatarError> checkASMLibraryFunction(AvatarSpecification avspec, AvatarLibraryFunction alf) {
ArrayList<AvatarError> errors = new ArrayList<>();
AvatarStateMachine asm = alf.getStateMachine();
for (AvatarStateMachineElement elt : asm.getListOfElements()) {
if (!(elt instanceof AvatarStopState)) {
if (elt.getNexts().size() == 0) {
AvatarError error = new AvatarError(avspec);
error.firstAvatarElement = alf;
error.secondAvatarElement = elt;
error.error = 7;
errors.add(error);
}
}
}
return errors;
}
public static ArrayList<AvatarError> checkMethodTypes(AvatarSpecification avspec) {
ArrayList<AvatarError> errors = new ArrayList<>();
for (AvatarBlock block : avspec.getListOfBlocks()) {
for(AvatarMethod am: block.getMethods()) {
AvatarError err = checkMethodTypes(avspec, block, am);
if (err != null) {
errors.add(err);
}
}
}
return errors;
}
public static AvatarError checkMethodTypes(AvatarSpecification avspec, AvatarBlock ab, AvatarMethod am) {
for(AvatarAttribute aa: am.getListOfAttributes()) {
if (aa.getType() == AvatarType.TIMER) {
AvatarError err = new AvatarError(avspec);
err.error = 15;
err.block = ab;
err.firstAvatarElement = am;
return err;
}
}
return null;
}
public static ArrayList<AvatarError> checkSignalTypes(AvatarSpecification avspec) {
ArrayList<AvatarError> errors = new ArrayList<>();
List<AvatarSignal> signals1, signals2;
for (AvatarRelation relation : avspec.getRelations()) {
signals1 = relation.getSignals1();
signals2 = relation.getSignals2();
List<AvatarSignal> list = new ArrayList<>();
list.addAll(signals1);
list.addAll(signals2);
for(AvatarSignal sig: list) {
AvatarError err = checkSignalTypes(avspec, sig);
if (err != null) {
errors.add(err);
}
}
}
return errors;
}
public static AvatarError checkSignalTypes(AvatarSpecification avspec, AvatarSignal sig) {
for(AvatarAttribute aa: sig.getListOfAttributes()) {
if (aa.getType() == AvatarType.TIMER) {
AvatarError err = new AvatarError(avspec);
err.error = 14;
err.firstAvatarElement = sig;
return err;
}
}
return null;
}
public static ArrayList<AvatarError> checkSignalRelations(AvatarSpecification avspec) {
ArrayList<AvatarError> errors = new ArrayList<>();
List<AvatarSignal> signals1, signals2;
// Check relations are corrects
for (AvatarRelation relation : avspec.getRelations()) {
signals1 = relation.getSignals1();
signals2 = relation.getSignals2();
AvatarBlock block1, block2;
block1 = relation.block1;
block2 = relation.block2;
if (block1 == null) {
AvatarError error = new AvatarError(avspec);
error.relation = relation;
error.error = 4;
errors.add(error);
}
if (block2 == null) {
AvatarError error = new AvatarError(avspec);
error.relation = relation;
error.error = 5;
errors.add(error);
}
if (signals1.size() != signals2.size()) {
AvatarError error = new AvatarError(avspec);
error.relation = relation;
error.error = 0;
errors.add(error);
} else {
// Compare signals characteristics
AvatarSignal sig1, sig2;
for (int i = 0; i < signals1.size(); i++) {
sig1 = signals1.get(i);
sig2 = signals2.get(i);
// In vs out
if (sig1.isIn() && sig2.isIn()) {
AvatarError error = new AvatarError(avspec);
error.relation = relation;
error.firstAvatarElement = sig1;
error.secondAvatarElement = sig2;
error.error = 1;
errors.add(error);
} else if (sig1.isOut() && sig2.isOut()) {
AvatarError error = new AvatarError(avspec);
error.relation = relation;
error.firstAvatarElement = sig1;
error.secondAvatarElement = sig2;
error.error = 2;
errors.add(error);
}
// Attributes
//TraceManager.addDev("Checking attributes compatibility");
if (!(sig1.isCompatibleWith(sig2))) {
AvatarError error = new AvatarError(avspec);
error.relation = relation;
error.firstAvatarElement = sig1;
error.secondAvatarElement = sig2;
error.error = 3;
errors.add(error);
}
// Both signals exist in their respective block
if (block1 != null) {
AvatarSignal as = block1.getSignalByName(sig1.getSignalName());
if (as == null) {
AvatarError error = new AvatarError(avspec);
error.relation = relation;
error.block = block1;
error.firstAvatarElement = sig1;
error.error = 6;
errors.add(error);
}
}
if (block2 != null) {
AvatarSignal as = block2.getSignalByName(sig2.getSignalName());
if (as == null) {
AvatarError error = new AvatarError(avspec);
error.relation = relation;
error.block = block2;
error.firstAvatarElement = sig2;
error.error = 6;
errors.add(error);
}
}
}
}
}
return errors;
}
public static ArrayList<AvatarError> checkActionOnSignals(AvatarSpecification avspec) {
ArrayList<AvatarError> errors = new ArrayList<>();
for (AvatarBlock block : avspec.getListOfBlocks()) {
AvatarStateMachine asm = block.getStateMachine();
if (asm != null) {
for(AvatarStateMachineElement asme: asm.getListOfElements()) {
if (asme instanceof AvatarActionOnSignal) {
AvatarActionOnSignal aaos = (AvatarActionOnSignal)asme;
AvatarSignal sig = aaos.getSignal();
if (aaos.getValues().size() != sig.getListOfAttributes().size()) {
AvatarError error = new AvatarError(avspec);
error.block = block;
error.firstAvatarElement = aaos;
error.error = 16;
errors.add(error);
} else {
for(int i=0; i<sig.getListOfAttributes().size(); i++) {
// Check that value correspond to the expected type
// If sig is in then only variables are expected
String value = aaos.getValues().get(i);
AvatarAttribute param = sig.getListOfAttributes().get(i);
// We expect a variable only
if (param.getType() == AvatarType.TIMER) {
AvatarError error = new AvatarError(avspec);
error.block = block;
error.firstAvatarElement = aaos;
error.error = 14;
errors.add(error);
} else if (sig.isIn() || param.getType() == AvatarType.UNDEFINED) {
AvatarAttribute aa = block.getAvatarAttributeWithName(value);
if (aa == null) {
AvatarError error = new AvatarError(avspec);
error.block = block;
error.firstAvatarElement = aaos;
error.error = 17;
errors.add(error);
} else {
// We check the type of the two is equivalent
if (aa.getType() != param.getType()) {
AvatarError error = new AvatarError(avspec);
error.block = block;
error.firstAvatarElement = aaos;
error.error = 17;
errors.add(error);
}
}
} else {
// int or boot expr
if (param.getType() == AvatarType.INTEGER) {
AvatarIBSExpressions.IExpr e1 = AvatarIBSolver.parseInt(block,value);
if (e1 == null) {
AvatarError error = new AvatarError(avspec);
error.block = block;
error.firstAvatarElement = aaos;
error.error = 19;
errors.add(error);
}
} else if (param.getType() == AvatarType.BOOLEAN) {
IBSExpressions.BExpr e1 = AvatarIBSolver.parseBool(block,value);
if (e1 == null) {
AvatarError error = new AvatarError(avspec);
error.block = block;
error.firstAvatarElement = aaos;
error.error = 20;
errors.add(error);
}
} else {
AvatarError error = new AvatarError(avspec);
error.block = block;
error.firstAvatarElement = aaos;
error.error = 18;
errors.add(error);
}
}
}
}
}
}
}
}
return errors;
}
public static AvatarError checkAvatarTermFunction(AvatarSpecification avspec, AvatarBlock block,
AvatarTransition asme, AvatarTermFunction atf) {
int size = atf.getMethod().getListOfAttributes().size();
if (size != atf.getArgs().components.size()) {
AvatarError error = new AvatarError(avspec);
error.block = block;
error.firstAvatarElement = atf;
error.error = 21;
return error;
}
for(int i=0; i<size; i++) {
// Check that each value correspond to the expected type
AvatarAttribute param = atf.getMethod().getListOfAttributes().get(i);
AvatarTerm term = atf.getArgs().components.get(i);
if (term instanceof AvatarAttribute) {
if ( ((AvatarAttribute)term).getType() != param.getType()) {
AvatarError error = new AvatarError(avspec);
error.block = block;
error.firstAvatarElement = asme;
error.error = 25;
return error;
}
} else {
String value = term.toString();
TraceManager.addDev("Value:>" + value + "< of class>" + term.getClass().toString() + "<");
if (param.getType() == AvatarType.INTEGER) {
TraceManager.addDev("Trying to parse int expr: " + value);
AvatarIBSExpressions.IExpr e1 = AvatarIBSolver.parseInt(block, value);
if (e1 == null) {
TraceManager.addDev("Parse error in int expr: " + value);
AvatarError error = new AvatarError(avspec);
error.block = block;
error.firstAvatarElement = asme;
error.error = 22;
return error;
}
TraceManager.addDev("Parse ok in int expr: " + value);
} else if (param.getType() == AvatarType.BOOLEAN) {
IBSExpressions.BExpr e1 = AvatarIBSolver.parseBool(block, value);
if (e1 == null) {
AvatarError error = new AvatarError(avspec);
error.block = block;
error.firstAvatarElement = asme;
error.error = 23;
return error;
}
} else {
AvatarError error = new AvatarError(avspec);
error.block = block;
error.firstAvatarElement = asme;
error.error = 18;
return error;
}
}
}
return null;
}
public static ArrayList<AvatarError> checkActions(AvatarSpecification avspec) {
ArrayList<AvatarError> errors = new ArrayList<>();
for (AvatarBlock block : avspec.getListOfBlocks()) {
AvatarStateMachine asm = block.getStateMachine();
if (asm != null) {
for (AvatarStateMachineElement asme : asm.getListOfElements()) {
if (asme instanceof AvatarTransition) {
for(AvatarAction aa: ((AvatarTransition)(asme)).getActions()) {
AvatarError ae = checkAction(avspec, block, ((AvatarTransition)(asme)), aa);
if (ae != null)
errors.add( ae );
}
}
}
}
}
return errors;
}
public static AvatarError checkAction(AvatarSpecification avspec, AvatarBlock block, AvatarTransition asme, AvatarAction aa) {
if (aa instanceof AvatarTermFunction) {
AvatarTermFunction atf = (AvatarTermFunction) aa;
AvatarError err = checkAvatarTermFunction(avspec, block, asme, atf);
if (err != null) {
return err;
}
}
// We assume that this is a variable setting, possibly with a method call
// v = method()
// v = expr
// v = w
TraceManager.addDev("Class>" + aa.getClass().toString() + "<");
if (aa instanceof avatartranslator.AvatarActionAssignment) {
AvatarActionAssignment aaa = (AvatarActionAssignment)aa;
AvatarLeftHand alh = aaa.leftHand;
// Left hand must be an attribute or a tuple with attributes
if (!(alh instanceof AvatarAttribute) && (!(alh instanceof AvatarTuple))) {
AvatarError error = new AvatarError(avspec);
error.block = block;
error.firstAvatarElement = asme;
error.error = 26;
return error;
}
ArrayList<AvatarType> listOfTypes = new ArrayList<>();
if (alh instanceof AvatarAttribute) {
AvatarAttribute avat = (AvatarAttribute) alh;
if (block.getAvatarAttributeWithName(avat.getName()) == null) {
AvatarError error = new AvatarError(avspec);
error.block = block;
error.firstAvatarElement = asme;
error.error = 26;
return error;
}
// Type of attribute must be int or boolean
if ((avat.getType() != AvatarType.INTEGER) && (avat.getType() != AvatarType.BOOLEAN)) {
AvatarError error = new AvatarError(avspec);
error.block = block;
error.firstAvatarElement = asme;
error.error = 27;
return error;
}
listOfTypes.add(avat.getType());
}
if (alh instanceof AvatarTuple) {
AvatarTuple at = (AvatarTuple) alh;
if (! ((AvatarTuple) alh).areComponentsAvatarAttributes()) {
AvatarError error = new AvatarError(avspec);
error.block = block;
error.firstAvatarElement = asme;
error.error = 26;
return error;
}
for(AvatarTerm avatTerm: at.getComponents()) {
AvatarAttribute avatAttri = (AvatarAttribute) avatTerm;
if ((avatAttri.getType() != AvatarType.INTEGER) && (avatAttri.getType() != AvatarType.BOOLEAN)) {
AvatarError error = new AvatarError(avspec);
error.block = block;
error.firstAvatarElement = asme;
error.error = 27;
return error;
}
listOfTypes.add(avatAttri.getType());
}
}
// Now that the left hand is correct, we must ensure that the right hand is correct
// and corresponds to what is expected in the left hand
if( listOfTypes.size() < 1) {
AvatarError error = new AvatarError(avspec);
error.block = block;
error.firstAvatarElement = asme;
error.error = 28;
return error;
}
AvatarTerm right = aaa.rightHand;
TraceManager.addDev("Class of right expr:>" + right.getClass().toString() + "<");
if (right instanceof AvatarTermFunction) {
AvatarTermFunction atf = (AvatarTermFunction) right;
AvatarError err = checkAvatarTermFunction(avspec, block, asme, atf);
if (err != null) {
return err;
}
// Must also check return types
if (listOfTypes.size() != atf.method.returnParameters.size()) {
AvatarError error = new AvatarError(avspec);
error.block = block;
error.firstAvatarElement = asme;
error.error = 28;
return error;
}
for(int i=0; i<listOfTypes.size(); i++) {
if (listOfTypes.get(i) != atf.method.returnParameters.get(i).getType()) {
AvatarError error = new AvatarError(avspec);
error.block = block;
error.firstAvatarElement = asme;
error.error = 28;
return error;
}
}
}
if (right instanceof AvatarAttribute) {
// Check the compatible type and the existence of the attribute
if ( ((AvatarAttribute)right).getType() != listOfTypes.get(0)) {
AvatarError error = new AvatarError(avspec);
error.block = block;
error.firstAvatarElement = asme;
error.error = 28;
return error;
}
}
if (right instanceof AvatarArithmeticOp) {
// Check that only one return type and that the two have the same type
if (listOfTypes.size() != 1) {
AvatarError error = new AvatarError(avspec);
error.block = block;
error.firstAvatarElement = asme;
error.error = 28;
return error;
}
if (listOfTypes.get(0) == AvatarType.INTEGER) {
String value = right.toString();
TraceManager.addDev("Trying to parse int expr: " + value);
AvatarIBSExpressions.IExpr e1 = AvatarIBSolver.parseInt(block, value);
if (e1 == null) {
TraceManager.addDev("Parse error in int expr: " + value);
AvatarError error = new AvatarError(avspec);
error.block = block;
error.firstAvatarElement = asme;
error.error = 29;
return error;
}
TraceManager.addDev("Parse ok in int expr: " + value);
} else if (listOfTypes.get(0) == AvatarType.BOOLEAN) {
String value = right.toString();
TraceManager.addDev("Trying to parse int expr: " + value);
IBSExpressions.BExpr e1 = AvatarIBSolver.parseBool(block, value);
if (e1 == null) {
TraceManager.addDev("Parse error in int expr: " + value);
AvatarError error = new AvatarError(avspec);
error.block = block;
error.firstAvatarElement = asme;
error.error = 30;
return error;
}
TraceManager.addDev("Parse ok in int expr: " + value);
} else {
AvatarError error = new AvatarError(avspec);
error.block = block;
error.firstAvatarElement = asme;
error.error = 28;
return error;
}
// We now evaluate the expression
}
// All done :-)
}
return null;
}
public static int isAValidGuard(AvatarSpecification _as, AvatarStateMachineOwner _ab, String _guard) {
//TraceManager.addDev("Evaluating (non modified) guard:" + _guard);
String tmp = _guard.replaceAll(" ", "");
if (tmp.compareTo("[]") == 0) {
return 0;
}
// NEW
tmp = Conversion.replaceAllChar(tmp, '[', "").trim();
tmp = Conversion.replaceAllChar(tmp, ']', "").trim();
String act = tmp;
for (AvatarAttribute aa : _ab.getAttributes()) {
if (aa.getType() != AvatarType.TIMER) {
act = Conversion.putVariableValueInString(AvatarSpecification.ops, act, aa.getName(), aa.getDefaultInitialValue());
}
}
//TraceManager.addDev("Testing guard expr=" + act);
AvatarIBSExpressions.BExpr e1 = AvatarIBSolver.parseBool(act);
return (e1 != null ? 0 : -1);
/*BoolExpressionEvaluator bee = new BoolExpressionEvaluator();
//TraceManager.addDev("Evaluating (modified) guard:" + act);
boolean result = bee.getResultOfWithIntExpr(act);
if (bee.getError() != null) {
TraceManager.addDev("Error: " + bee.getError() + " result=" + result);
return -1;
}
return 0;*/
// END of NEW
//return parse(_as, _ab, "guard", act);
}
/*
* @return 0 if ok, -1 if failure
*/
public static int isAValidIntExprReplaceVariables(AvatarSpecification _as, AvatarStateMachineOwner _ab, String _expr) {
/*AvatarExpressionSolver e1 = new AvatarExpressionSolver("x + y");
e1.buildExpression(_ab);*/
if (_expr.trim().length() == 0) {
return 0;
}
String tmp = _expr.replaceAll(" ", "").trim();
String act = tmp;
for (AvatarAttribute aa : _ab.getAttributes()) {
act = Conversion.putVariableValueInString(AvatarSpecification.ops, act, aa.getName(), aa.getDefaultInitialValue());
}
//TraceManager.addDev("Checking if expr " + _expr + " is valid");
AvatarIBSExpressions.IExpr e1 = AvatarIBSolver.parseInt(act);
//TraceManager.addDev("Checking if expr " + _expr + " is valid: " + (e1 != null));
/*IntExpressionEvaluator iee = new IntExpressionEvaluator();
//TraceManager.addDev("Evaluating int:" + act);
double result = iee.getResultOf(act);
if (iee.getError() != null) {
TraceManager.addDev("My parsing Error: " + iee.getError());
} else {
TraceManager.addDev("My parsing ok");
}*/
//TraceManager.addDev("my parsing:" + parse(_as, _ab, "actionnat", _expr));
return (e1 != null ? 0 : -1);
}
public static int isAValidIntExpr(AvatarSpecification _as, AvatarStateMachineOwner _ab, String _expr) {
/*AvatarExpressionSolver e1 = new AvatarExpressionSolver("x + y");
e1.buildExpression(_ab);*/
if (_expr.trim().length() == 0) {
return 0;
}
String tmp = _expr.replaceAll(" ", "").trim();
String act = tmp;
/*for (AvatarAttribute aa : _ab.getAttributes()) {
act = Conversion.putVariableValueInString(AvatarSpecification.ops, act, aa.getName(), aa.getDefaultInitialValue());
}*/
//TraceManager.addDev("Checking if expr " + _expr + " is valid");
if (_ab instanceof AvatarBlock) {
AvatarIBSExpressions.IExpr e1 = AvatarIBSolver.parseInt((AvatarBlock)_ab, act);
return (e1 != null ? 0 : -1);
}
return isAValidIntExprReplaceVariables(_as, _ab, _expr);
//TraceManager.addDev("Checking if expr " + _expr + " is valid: " + (e1 != null));
/*IntExpressionEvaluator iee = new IntExpressionEvaluator();
//TraceManager.addDev("Evaluating int:" + act);
double result = iee.getResultOf(act);
if (iee.getError() != null) {
TraceManager.addDev("My parsing Error: " + iee.getError());
} else {
TraceManager.addDev("My parsing ok");
}*/
//TraceManager.addDev("my parsing:" + parse(_as, _ab, "actionnat", _expr));
}
public static int isAValidProbabilityExpr(AvatarSpecification _as, AvatarStateMachineOwner _ab, String _expr) {
if (_expr.trim().length() == 0) {
return 0;
}
String tmp = _expr.replaceAll(" ", "").trim();
double prob = 0.5;
try {
prob = Double.parseDouble(tmp);
} catch (Exception e) {
return -1;
}
if ((prob < 0) || (prob > 1000)) {
return -1;
}
return 0;
}
public static int newIsAValidBoolExpr(AvatarSpecification _as, AvatarStateMachineOwner _ab, String _expr) {
if (_expr.trim().length() == 0) {
return 0;
}
String tmp = _expr.replaceAll(" ", "").trim();
String act = tmp;
for (AvatarAttribute aa : _ab.getAttributes()) {
act = Conversion.putVariableValueInString(AvatarSpecification.ops, act, aa.getName(), aa.getDefaultInitialValueTF());
}
AvatarIBSExpressions.BExpr e1 = AvatarIBSolver.parseBool(act);
return (e1 == null ? 0 : 1);
}
public static int isAValidBoolExpr(AvatarSpecification _as, AvatarStateMachineOwner _ab, String _expr) {
if (_expr.trim().length() == 0) {
return 0;
}
String tmp = _expr.replaceAll(" ", "").trim();
String act = tmp;
//TraceManager.addDev("1. IsValidBoolExpr Evaluating bool:" + act);
for (AvatarAttribute aa : _ab.getAttributes()) {
act = Conversion.putVariableValueInString(AvatarSpecification.ops, act, aa.getName(), aa.getDefaultInitialValue());
}
//TraceManager.addDev("2. IsValidBoolExpr Evaluating bool:" + act);
/*BoolExpressionEvaluator bee = new BoolExpressionEvaluator();
boolean result = bee.getResultOfWithIntExpr(act);
if (bee.getError() != null) {
TraceManager.addDev("Error in bool expr: " + bee.getError());
return -1;
} else {
//TraceManager.addDev("IsValidBoolExpr: YES (" + act + ")");
}*/
// Testing with parsing AvatarExpressionSolver
//TraceManager.addDev("3. Now with avatar expression solver:" + _expr);
AvatarIBSExpressions.BExpr aee = AvatarIBSolver.parseBool(act);
if (aee == null) {
TraceManager.addDev("4. Error with avatar expression solver:" + act);
return -1;
}
//TraceManager.addDev("4. Ok with avatar expression solver:" + act);
return 0;
// OLD return parse(_as, _ab, "actionbool", _expr);
}
public static int isAValidVariableExpr(AvatarSpecification _as, AvatarStateMachineOwner _ab, String _expr) {
int index0 = _expr.indexOf("=");
if (index0 == -1) {
return -1;
}
String attributeName = _expr.substring(0, index0).trim();
AvatarAttribute aa = _ab.getAvatarAttributeWithName(attributeName);
if (aa == null) {
return -1;
}
if (aa.isConstant()) { return -2;}
String action = _expr.substring(index0 + 1, _expr.length()).trim();
if (aa.isInt()) {
//TraceManager.addDev("Testing action+" + action);
return isAValidIntExpr(_as, _ab, action);
//return parse(_as, _ab, "actionnat", action);
} else if (aa.isBool()) {
return isAValidBoolExpr(_as, _ab, action);
//return parse(_as, _ab, "actionbool", action);
}
return -1;
}
/**
* Parsing in two steps:
* 1. Parsing the expression with no variable checking
* 2. Parsing the expression with variables values to see whether variables are well-placed or not
* The second parsing is performed iff the first one succeeds
*
* @param _as : Unused
* @param _ab : Avatar block
* @param _parseCmd : Parse Command
* @param _action : Action
* @return : return -1 in case of error in first pass
* return -2 in case of error in second pass
* return -3 in case a variable has not been declared
*/
public static int parse(AvatarSpecification _as, AvatarStateMachineOwner _ab, String _parseCmd, String _action) {
TMLExprParser parser;
SimpleNode root;
int i;
// First parsing
parser = new TMLExprParser(new StringReader(_parseCmd + " " + _action));
try {
//
root = parser.CompilationUnit();
//root.dump("pref=");
//
} catch (ParseException e) {
TraceManager.addDev("\nAvatar Parsing :" + _parseCmd + " " + _action);
TraceManager.addDev("ParseException --------> Parse error in :" + _parseCmd + " " + _action);
return -1;
} catch (TokenMgrError tke) {
TraceManager.addDev("Avatar TokenMgrError --------> Parse error in :" + _parseCmd + " " + _action);
return -1;
}
// Second parsing
// We only replace variables values after the "=" sign
int index = _action.indexOf('=');
String modif = _action;
if (_parseCmd.startsWith("ass")) {
if (index != -1) {
modif = _action.substring(index + 1, _action.length());
}
_parseCmd = "action" + _parseCmd.substring(3, _parseCmd.length());
}
/*for(i=0; i<_ab.attributeNb(); i++) {
modif = AvatarSpecification.putAttributeValueInString(modif, _ab.getAttribute(i));
}*/
parser = new TMLExprParser(new StringReader(_parseCmd + " " + modif));
try {
//
root = parser.CompilationUnit();
//root.dump("pref=");
//
} catch (ParseException e) {
TraceManager.addDev("\nAvatar Parsing :" + _parseCmd + " " + modif);
TraceManager.addDev("\n(Original parsing :" + _parseCmd + " " + _action + ")");
TraceManager.addDev("ParseException --------> Parse error in :" + _parseCmd + " " + _action);
return -2;
} catch (TokenMgrError tke) {
TraceManager.addDev("\nnAvatar Parsing :" + _parseCmd + " " + modif);
TraceManager.addDev("TokenMgrError --------> Parse error in :" + _parseCmd + " " + _action);
return -2;
}
// Tree analysis: if the tree contains a variable, then, this variable has not been declared
List<String> vars = root.getVariables();
for (String s : vars) {
// is that string a variable?
if ((s.compareTo("true") != 0) && (s.compareTo("false") != 0) && (s.compareTo("nil") != 0)) {
TraceManager.addDev("Variable not declared: " + s);
return -3;
}
}
return 0;
}
// Searches for numerical values over max
// @return list of AvatarElement not respecting this interval
public static ArrayList<AvatarElement> useOfInvalidUPPAALNumericalValues(AvatarSpecification _as, int maxV) {
ArrayList<AvatarElement> invalids = new ArrayList<AvatarElement>();
for (AvatarBlock ab : _as.getListOfBlocks()) {
// Check for attribute initial value
invalids.addAll(ab.getAttributesOverMax(maxV));
// Check operators of State machine
invalids.addAll(ab.getStateMachine().elementsWithNumericalValueOver(maxV));
}
return invalids;
}
private static void newError(AvatarSpecification _spec, ArrayList<AvatarError> _errors,
AvatarElement _first, AvatarElement _second, int _errorIndex) {
AvatarError error = new AvatarError(_spec);
error.firstAvatarElement = _first;
error.secondAvatarElement = _second;
error.error = _errorIndex;
_errors.add(error);
}
public static ArrayList<AvatarError> checkElseInGuards(AvatarSpecification avspec) {
ArrayList<AvatarError> errors = new ArrayList<>();
for (AvatarBlock block : avspec.getListOfBlocks()) {
for (AvatarStateMachineElement asme : block.getStateMachine().getListOfElements()) {
if (asme instanceof AvatarTransition) {
AvatarTransition at = (AvatarTransition) asme;
if (at.getGuard() == null) {
AvatarError error = new AvatarError(avspec);
error.firstAvatarElement = at;
error.error = ERROR_IN_ELSE_GUARD;
errors.add(error);
}
}
}
}
return errors;
}
}