diff --git a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
index 737e3488a66521fac22d18d4c8d806bbe64e2145..edb394361bae356576d8fea01b80a4a72175e57d 100644
--- a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
+++ b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
@@ -385,7 +385,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
       }*/
 
     public boolean startModelCheckingProperties() {
-        boolean studyS, studyL, studyR, studyRI, genRG;
+        boolean studyS, studyL, studyR, studyRI, genRG, genTrace;
         boolean emptyTr, ignoreConcurrence;
         long deadlocks = 0;
         
@@ -408,6 +408,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
         studyS = studySafety;
         studyRI = studyReinit;
         genRG = computeRG;
+        genTrace = counterexample;
         
         //then compute livenesses
         computeRG = false;
@@ -416,6 +417,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
         studyLiveness = false;
         studyReachability = false;
         studyReinit = false;
+        counterexample = false;
                 
 
         if (studyL) {
@@ -438,6 +440,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
         
         if (studyS) {
             studySafety = true;
+            counterexample = genTrace;
             for (SafetyProperty sp : safeties) {
                 safety = sp;
                 ignoreConcurrenceBetweenInternalActions = true;
@@ -476,6 +479,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
                 resetModelChecking();
             }
             studySafety = false;
+            counterexample = false;
         }
         
         if (studyRI) {
@@ -486,6 +490,24 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
             studyReinit = false;
         }
         
+        if (checkNoDeadlocks) {
+            //If a complete study with reachability graph generation has been executed,
+            //there is no need to study deadlocks again
+            if (deadlocks == 0 || genTrace) {
+                deadlockStop = true;
+                counterexample = genTrace;
+                ignoreConcurrenceBetweenInternalActions = true;
+                initCounterexample();
+                startModelChecking(nbOfThreads);
+                generateCounterexample();
+                deadlocks = nbOfDeadlocks;
+                resetModelChecking();
+                ignoreConcurrenceBetweenInternalActions = ignoreConcurrence;
+                counterexample = false;
+                deadlockStop = false;
+            }
+        }
+        
         if (studyR || genRG) {
             if (genRG) {
                 deadlocks = 0;
@@ -501,17 +523,8 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
         
         if (genRG) {
             nbOfDeadlocks = (int) deadlocks;
-        } else if (checkNoDeadlocks) {
-            //If a complete study with reachability graph generation has been executed,
-            //there is no need to study deadlocks again
-            if (deadlocks == 0) {
-                deadlockStop = true;
-                ignoreConcurrenceBetweenInternalActions = true;
-                startModelChecking(nbOfThreads);
-                ignoreConcurrenceBetweenInternalActions = ignoreConcurrence;
-            } else {
-                nbOfDeadlocks = 1;
-            }
+        } else if (checkNoDeadlocks && deadlocks > 0) {
+            nbOfDeadlocks = 1;
         }
         
         computeRG = genRG;
@@ -594,6 +607,10 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
             actionOnProperty(initialState, 0, null, null);
         } else {
             pendingStates.add(initialState);
+            if (counterexample && deadlockStop) {
+                //Register counterexample trace
+                actionOnProperty(initialState, 0, null, null);
+            }
         }
         
         if (studyReinit) {
@@ -657,6 +674,10 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
             actionOnProperty(initialState, 0, null, null);
         } else {
             pendingStates.add(initialState);
+            if (counterexample && deadlockStop) {
+                //Register counterexample trace
+                actionOnProperty(initialState, 0, null, null);
+            }
         }
         //pendingStates.add(initialState);
            
@@ -903,7 +924,10 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
             counterTrace.buildTrace();
             if (studySafety) {
                 counterTraceReport.append("Trace for " + safety.getRawProperty() + "\n");
-                counterTraceReport.append(counterTrace.generateSimpleTrace(states) + "\n");
+                counterTraceReport.append(counterTrace.generateSimpleTrace(states) + "\n\n");
+            } else if (deadlockStop) {
+                counterTraceReport.append("Trace for NO Deadlocks\n");
+                counterTraceReport.append(counterTrace.generateSimpleTrace(states) + "\n\n");
             }
         }
     }
@@ -1077,10 +1101,14 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
                 link.destinationState = newState;
 //                newState.distance = _ss.distance + 1;
                 
-                if (!studySafety) {
-                    pendingStates.add(newState);
-                } else {
+                if (studySafety) {
                     actionOnProperty(newState, i, similar, _ss);
+                } else {
+                    pendingStates.add(newState);
+                    if (counterexample && deadlockStop) {
+                        //Register counterexample trace
+                        actionOnProperty(newState, i, similar, _ss);
+                    }
                 }
                 i++;
                 //newState.id = getStateID();
@@ -1178,10 +1206,14 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
                 } else {
                     link.destinationState = newState;
 //                    newState.distance = _ss.distance + 1;
-                    if (!studySafety) {
-                        pendingStates.add(newState);
-                    } else {
+                    if (studySafety) {
                         actionOnProperty(newState, 0, similar, _ss);
+                    } else {
+                        pendingStates.add(newState);
+                        if (counterexample && deadlockStop) {
+                            //Register counterexample trace
+                            actionOnProperty(newState, 0, similar, _ss);
+                        }
                     }
                 }
                 nbOfLinks++;
@@ -1263,10 +1295,14 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
                 } else {
                     link.destinationState = newState;
 //                    newState.distance = _ss.distance + 1;
-                    if (!studySafety) {
-                        pendingStates.add(newState);
-                    } else {
+                    if (studySafety) {
                         actionOnProperty(newState, 0, similar, _ss);
+                    } else {
+                        pendingStates.add(newState);
+                        if (counterexample && deadlockStop) {
+                            //Register counterexample trace
+                            actionOnProperty(newState, 0, similar, _ss);
+                        }
                     }
                 }
                 nbOfLinks++;
diff --git a/src/main/java/ui/window/JDialogAvatarModelChecker.java b/src/main/java/ui/window/JDialogAvatarModelChecker.java
index b3ccbac29ac0767789a92bb8ee4b8f6790432e52..9ae4db144fd30abd98395cd75732fa1b68ab40a6 100644
--- a/src/main/java/ui/window/JDialogAvatarModelChecker.java
+++ b/src/main/java/ui/window/JDialogAvatarModelChecker.java
@@ -1081,7 +1081,7 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
             }
         }
         
-        countertrace.setEnabled(safety.isSelected());
+        countertrace.setEnabled(safety.isSelected() || noDeadlocks.isSelected());
         countertraceField.setEnabled(countertrace.isSelected());
         generateCountertraceSelected = countertrace.isSelected();