diff --git a/src/avatartranslator/toproverif/AVATAR2ProVerif.java b/src/avatartranslator/toproverif/AVATAR2ProVerif.java
index 6d31a4a0d5c2ace01abd07b40d3d98bafbb7dc74..ed2bc3d312b45220a632bda316b32687db8dee7b 100755
--- a/src/avatartranslator/toproverif/AVATAR2ProVerif.java
+++ b/src/avatartranslator/toproverif/AVATAR2ProVerif.java
@@ -51,6 +51,7 @@ import java.util.*;
 import proverifspec.*;
 import myutil.*;
 import avatartranslator.*;
+import ui.*;
 
 public class AVATAR2ProVerif {
 
@@ -961,14 +962,14 @@ public class AVATAR2ProVerif {
     }
 
     public void makeBlockProcesses(AvatarBlock _block, AvatarStateMachine _asm, AvatarStateMachineElement _asme, ProVerifProcess _p, LinkedList<ProVerifProcess> _processes, LinkedList<AvatarState> _states, String _choiceInfo) {
-        AvatarSignal as;
+        avatartranslator.AvatarSignal as;
         AvatarActionOnSignal aaos;
         AvatarTransition at;
         ProVerifProcess p, ptmp, ptmp1, ptmp2;
         String tmp, name, value, term;
         int i, j;
         int index0, index1;
-        AvatarMethod am;
+        avatartranslator.AvatarMethod am;
         boolean found;
         LinkedList<String> pos;
 
@@ -1143,6 +1144,11 @@ public class AVATAR2ProVerif {
                     TraceManager.addDev("   Adding guard: " + tmp);
                     addLineNoEnd(_p, "if " + tmp + " then");
                 } else {
+		    CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "Guard: " + at.getGuard() + " in block " + _block.getName() + " is not supported. Replacing by an empty guard");
+                    ce.setAvatarBlock(_block);
+                    ce.setTDiagramPanel(((AvatarDesignPanel)(avspec.getReferenceObject())).getAvatarSMDPanel(_block.getName()));
+                    ce.setTGComponent((TGComponent)(at.getReferenceObject()));
+                    warnings.add(ce);
 		    addLineNoEnd(_p, "(*  Unsuported guard:" + at.getGuard() + " *)");
 		}
             }
diff --git a/src/ui/AvatarDesignPanel.java b/src/ui/AvatarDesignPanel.java
index 20630c76fa40af23c7cf3086605740f2135e0dd2..f4c39f7c3258b3e115a5d6fd000fee486617c18a 100644
--- a/src/ui/AvatarDesignPanel.java
+++ b/src/ui/AvatarDesignPanel.java
@@ -324,12 +324,12 @@ public class AvatarDesignPanel extends TURTLEPanel {
     }
 
     public void modelBacktracingProVerif(ProVerifOutputAnalyzer pvoa) {
-	
+
         if (abdp == null) {
             return;
         }
 
-	resetModelBacktracingProVerif();
+        resetModelBacktracingProVerif();
 
         String block, attr, state;
         int index;
@@ -339,7 +339,7 @@ public class AvatarDesignPanel extends TURTLEPanel {
         TGComponent tgc;
 
         // Confidential attributes
-         for(String s: pvoa.getSecretTerms()) {
+        for(String s: pvoa.getSecretTerms()) {
             index = s.indexOf("__");
             if (index != -1) {
                 block = s.substring(0, index);
diff --git a/src/ui/CheckingError.java b/src/ui/CheckingError.java
index 937a5c51324efb91b471d50a1dac3d2837d0a468..cb00ca9b926b84066155b3a140dc3caf4aa147c5 100755
--- a/src/ui/CheckingError.java
+++ b/src/ui/CheckingError.java
@@ -65,7 +65,7 @@ public class CheckingError {
     private TMLTask tmlt;
     private TDiagramPanel tdp; 
     private TGComponent tgc;
-	private AvatarBlock ab;
+    private AvatarBlock ab;
     
     public CheckingError(int _type, String _message) {
         type = _type;
@@ -84,7 +84,7 @@ public class CheckingError {
         t = _t;
     }
 	
-	public void setAvatarBlock(AvatarBlock _ab) {
+    public void setAvatarBlock(AvatarBlock _ab) {
         ab = _ab;
     }
     
diff --git a/src/ui/GTURTLEModeling.java b/src/ui/GTURTLEModeling.java
index c54eff9384b86c661a6eb8a420d1d6b9b5ba0eab..e7c952f1639432163760a8c9f6fa3291dba1c618 100755
--- a/src/ui/GTURTLEModeling.java
+++ b/src/ui/GTURTLEModeling.java
@@ -629,6 +629,7 @@ public class GTURTLEModeling {
         //tml2uppaal.setChoiceDeterministic(choices);
         //tml2uppaal.setSizeInfiniteFIFO(_size);
         proverif = avatar2proverif.generateProVerif(true, true, _stateReachability, _advancedTranslation);
+	warnings = avatar2proverif.getWarnings();
         languageID = PROVERIF;
         mgui.setMode(MainGUI.EDIT_PROVERIF_OK);
         //mgui.setMode(MainGUI.MODEL_PROVERIF_OK);
diff --git a/src/ui/window/JDialogProVerifGeneration.java b/src/ui/window/JDialogProVerifGeneration.java
index acc74dcc611be8947632edd228f9d3ebea54c61d..7af509132b27c12a5b98e2af64606007adffed2c 100644
--- a/src/ui/window/JDialogProVerifGeneration.java
+++ b/src/ui/window/JDialogProVerifGeneration.java
@@ -331,6 +331,10 @@ public class JDialogProVerifGeneration extends javax.swing.JDialog implements Ac
                 } else {
                     jta.append("Could not generate proverif code\n");
                 }
+
+		//if (mgui.gtm.getCheckingWarnings().size() > 0) {
+		    jta.append("" +  mgui.gtm.getCheckingWarnings().size() + " warning(s)\n");
+		    //}
             }