diff --git a/src/main/java/avatartranslator/AvatarGuard.java b/src/main/java/avatartranslator/AvatarGuard.java index f75aedd22226c555cab87f00a05344c0774b9424..3138c0758e5c7eeedbb71b3c4a0ee2e1c8766943 100644 --- a/src/main/java/avatartranslator/AvatarGuard.java +++ b/src/main/java/avatartranslator/AvatarGuard.java @@ -177,7 +177,7 @@ public abstract class AvatarGuard { } } - for (String delim: new String[] {"==", "!="}) { + for (String delim: new String[] {"==", "!=", "<", ">"}) { int indexBinaryOp = sane.indexOf (delim); if (indexBinaryOp != -1) { AvatarTerm firstTerm = AvatarTerm.createFromString (block, sane.substring (0, indexBinaryOp)); diff --git a/src/main/java/avatartranslator/AvatarSimpleGuardMono.java b/src/main/java/avatartranslator/AvatarSimpleGuardMono.java index 58aeefdd90e87cf1c8dfa12158c546ffab28903d..15c9ce5dea11c35d23f73eeec3a44af7170f0a6e 100644 --- a/src/main/java/avatartranslator/AvatarSimpleGuardMono.java +++ b/src/main/java/avatartranslator/AvatarSimpleGuardMono.java @@ -79,12 +79,9 @@ public class AvatarSimpleGuardMono extends AvatarSimpleGuard { // { // } - if (this.term instanceof AvatarAttribute) - { + if (this.term instanceof AvatarAttribute) { this.term = attributesMapping.get(this.term); - } - else - { + } else { this.term.replaceAttributes (attributesMapping); } } diff --git a/src/main/java/avatartranslator/toproverif/AVATAR2ProVerif.java b/src/main/java/avatartranslator/toproverif/AVATAR2ProVerif.java index a6ed8efef41aff5e2e2638e5ab9220838874dfcb..22ac59e016755c9edddc1463c09f828171407ac4 100755 --- a/src/main/java/avatartranslator/toproverif/AVATAR2ProVerif.java +++ b/src/main/java/avatartranslator/toproverif/AVATAR2ProVerif.java @@ -349,7 +349,9 @@ public class AVATAR2ProVerif implements AvatarTranslator { return null; if (_guard instanceof AvatarSimpleGuardMono) { + //TraceManager.addDev("SimpleGuardMono:" + _guard); String term = AVATAR2ProVerif.translateTerm (((AvatarSimpleGuardMono) _guard).getTerm (), attributeCmp); + //TraceManager.addDev("guard/ term=" + term); if (term != null) return term + " = " + TRUE; @@ -357,13 +359,19 @@ public class AVATAR2ProVerif implements AvatarTranslator { } if (_guard instanceof AvatarSimpleGuardDuo) { + //TraceManager.addDev("SimpleGuardDuo"); String delim = null; String termA = AVATAR2ProVerif.translateTerm (((AvatarSimpleGuardDuo) _guard).getTermA (), attributeCmp); String termB = AVATAR2ProVerif.translateTerm (((AvatarSimpleGuardDuo) _guard).getTermB (), attributeCmp); + if (((AvatarSimpleGuardDuo) _guard).getBinaryOp ().equals ("==")) delim = "="; + /*else if (((AvatarSimpleGuardDuo) _guard).getBinaryOp ().equals ("<")) + delim = "<";*/ else if (((AvatarSimpleGuardDuo) _guard).getBinaryOp ().equals ("!=")) delim = "<>"; + /*else if (((AvatarSimpleGuardDuo) _guard).getBinaryOp ().equals (">")) + delim = ">";*/ if (termA != null && termB != null && delim != null) return termA + " " + delim + " " + termB; @@ -372,6 +380,7 @@ public class AVATAR2ProVerif implements AvatarTranslator { } if (_guard instanceof AvatarUnaryGuard) { + //TraceManager.addDev("UnaryGuard"); String unary = ((AvatarUnaryGuard) _guard).getUnaryOp (); AvatarGuard guard = ((AvatarUnaryGuard) _guard).getGuard (); @@ -392,6 +401,7 @@ public class AVATAR2ProVerif implements AvatarTranslator { } if (_guard instanceof AvatarBinaryGuard) { + //TraceManager.addDev("BinaryGuard"); String delim = ((AvatarBinaryGuard) _guard).getBinaryOp (); AvatarGuard guardA = ((AvatarBinaryGuard) _guard).getGuardA (); AvatarGuard guardB = ((AvatarBinaryGuard) _guard).getGuardB (); @@ -411,6 +421,7 @@ public class AVATAR2ProVerif implements AvatarTranslator { } if (_guard instanceof AvatarConstantGuard) { + //TraceManager.addDev("ConstantGuard"); AvatarConstantGuard constant = (AvatarConstantGuard) _guard; if (constant.getConstant () == AvatarConstant.TRUE) return "true"; @@ -1169,6 +1180,7 @@ public class AVATAR2ProVerif implements AvatarTranslator { // Check if the transition is guarded if (_asme.isGuarded() && !arg.lastASME.hasElseChoiceType1 ()) { + TraceManager.addDev("Analyzing GUARD: " + _asme.getGuard() + " real guard=" + _asme.getGuard().getRealGuard (arg.lastASME)); String tmp = AVATAR2ProVerif.translateGuard(_asme.getGuard().getRealGuard (arg.lastASME), arg.attributeCmp); if (tmp != null) { TraceManager.addDev("| | transition is guarded by " + tmp);