adhoc Expression Normaliser for NuSMV Text Generation.

refs 3025

org.fortiss.af3.tools/trunk/src/org/fortiss/af3/tools/nusmv/textgen/NuSMVTextGenerator.java

@@ -482,11 +482,21 @@ public class NuSMVTextGenerator implements ITextGenerator<NuSMVFile> {
 			if(call.getArguments().size() == 1) {
 				// get(0) is safe because of the condition in the if statement
 				IExpressionTerm arg0 = (IExpressionTerm)call.getArguments().get(0);
+				if(op == EOperator.NOT && isUnaryNOT(arg0)) {
+					return convertExpressionToString((IExpressionTerm)((FunctionCall)arg0)
+							.getArguments().get(0));
+				}
 				return getNuSMVString(op) + "(" + convertExpressionToString(arg0) + ")";
 			} else if(call.getArguments().size() == 2) {
 				// get(0) is safe because of the condition in the if statement
 				IExpressionTerm lhs = (IExpressionTerm)call.getArguments().get(0);
 				IExpressionTerm rhs = (IExpressionTerm)call.getArguments().get(1);
+				if(op == EOperator.OR && isUnaryNOT(lhs)) {
+					return "(" +
+							convertExpressionToString((IExpressionTerm)((FunctionCall)lhs)
+									.getArguments().get(0)) + " -> " +
+							convertExpressionToString(rhs) + ")";
+				}
 				String lhsString = convertExpressionToString(lhs);
 				String rhsString = convertExpressionToString(rhs);
 				if(op == EOperator.INDEX) {
@@ -510,6 +520,14 @@ public class NuSMVTextGenerator implements ITextGenerator<NuSMVFile> {
 		throw new UnknownLanguageFragmentException(call.toString());
 	}
 
+	/** evaluates to true if the expression term is a negation (e.g. !(a == b)) */
+	private static boolean isUnaryNOT(IExpressionTerm exp) {
+		return exp instanceof FunctionCall &&
+				((FunctionCall)exp).getFunction() instanceof PredefinedFunction &&
+				((PredefinedFunction)((FunctionCall)exp).getFunction()).getOperator() == EOperator.NOT &&
+				((FunctionCall)exp).getArguments().size() == 1;
+	}
+
 	/** nuXmv string representation of an @{link EOperator}. */
 	private static String getNuSMVString(EOperator op) throws UnknownLanguageFragmentException {
 		switch(op) {