diff --git a/src/avatartranslator/modelchecker/AvatarModelChecker.java b/src/avatartranslator/modelchecker/AvatarModelChecker.java
index e598f5ede678eed82326c43194168ef1a115cf57..f696d45057d444407f876c49ce1a4b319bfbc00c 100644
--- a/src/avatartranslator/modelchecker/AvatarModelChecker.java
+++ b/src/avatartranslator/modelchecker/AvatarModelChecker.java
@@ -53,7 +53,7 @@ import avatartranslator.*;
 import myutil.*;
 
 public class AvatarModelChecker implements Runnable {
-    private final static int DEFAULT_NB_OF_THREADS = 8;
+    private final static int DEFAULT_NB_OF_THREADS = 1;
     private final static int SLEEP_DURATION = 500;
 
     private AvatarSpecification spec;
@@ -309,11 +309,23 @@ public class AvatarModelChecker implements Runnable {
 
 	if (ignoreConcurrenceBetweenInternalActions) {
 	    SpecificationTransition st = null;
-	    // See whether there is at least one transition with an internal action
+	    // See whether there is at least one transition with an immediate internal action with no alternative in the same block
 	    for(SpecificationTransition tr: transitions) {
-		if (AvatarTransition.isActionType(tr.getType()) || tr.getType() == AvatarTransition.TYPE_EMPTY) {
-		    st = tr;
-		    break;
+		if ((AvatarTransition.isActionType(tr.getType()) && (tr.clockMax ==  clockMin))|| tr.getType() == AvatarTransition.TYPE_EMPTY) {
+		    // Must look for similar transitions in the the same block
+		    boolean foundSameBlock = false;
+		    for(SpecificationTransition tro: transitions) {
+			if (tro != tr) {
+			    if (tro.hasBlockOf(tr)) {
+				foundSameBlock = true;
+				break;
+			    }
+			}
+		    }
+		    if (!foundSameBlock) {
+			st = tr;
+			break;
+		    }
 		}
 	    }
 	    if (st != null) {
@@ -322,12 +334,17 @@ public class AvatarModelChecker implements Runnable {
 	    }
 	}
 
+	TraceManager.addDev("Possible transitions 4:" + transitions.size());
         // For each realizable transition
         //   Make it, reset clock of the involved blocks to 0, increase clockmin/clockhmax of each block
         //   compute new state, and compare with existing ones
         //   If not a new state, create the link rom the previous state to the new one
         //   Otherwise create the new state and its link, and add it to the pending list of states
+	int cptt = 0;
         for(SpecificationTransition tr: transitions) {
+	    TraceManager.addDev("Handling transitions #" + cptt + " type =" + tr.getType());
+	    cptt ++;
+
             // Make tr
             // to do so, must create a new state
             SpecificationState newState = _ss.advancedClone();
diff --git a/src/avatartranslator/modelchecker/SpecificationBlock.java b/src/avatartranslator/modelchecker/SpecificationBlock.java
index 89d882bd92820c970625e8c69600b1d412c79d7f..5f6b8e4974e44c52216a601c7dde8dfe1a0b380d 100644
--- a/src/avatartranslator/modelchecker/SpecificationBlock.java
+++ b/src/avatartranslator/modelchecker/SpecificationBlock.java
@@ -62,6 +62,8 @@ public class SpecificationBlock  {
     public static final int ATTR_INDEX = 3;
     
     public int [] values; // state in block, clockmin, clockmax, variables
+    public boolean hasTimedTransition;
+    public boolean timeElapsed;
 
     public SpecificationBlock() {
     }
@@ -106,4 +108,8 @@ public class SpecificationBlock  {
 	sb.values = values.clone();
 	return sb;
     }
+
+    public boolean hasTimedTransition() {
+	return true;
+    }
 }
diff --git a/src/avatartranslator/modelchecker/SpecificationState.java b/src/avatartranslator/modelchecker/SpecificationState.java
index daa93cb327f68d266bd81f39c24594a69f2907b6..1425e6e986db76e015afb987220526ead50e6504 100644
--- a/src/avatartranslator/modelchecker/SpecificationState.java
+++ b/src/avatartranslator/modelchecker/SpecificationState.java
@@ -120,14 +120,21 @@ public class SpecificationState  {
     }
 
     // Increase the clock of the blocks not in the transition
-    // and puts the one of others to 0
+    // and having a timed transition.
+    // Otherwise, puts the one of others to 0
     public void increaseClockOfBlocksExcept(SpecificationTransition _st) {
 	SpecificationBlock sb;
 	for(int i=0; i<blocks.length; i++) {
 	    sb = blocks[i];
 	    if (!(_st.hasBlockIndex(i))) {
-		sb.values[SpecificationBlock.CLOCKMIN_INDEX] += _st.clockMin;
-		sb.values[SpecificationBlock.CLOCKMAX_INDEX] += _st.clockMax;
+		if (sb.hasTimedTransition()) {
+		    sb.values[SpecificationBlock.CLOCKMIN_INDEX] += _st.clockMin;
+		    sb.values[SpecificationBlock.CLOCKMAX_INDEX] += _st.clockMax;
+		} 
+		/*else {
+		    sb.values[SpecificationBlock.CLOCKMIN_INDEX] = 0;
+		    sb.values[SpecificationBlock.CLOCKMAX_INDEX] = 0;
+		    }*/
 	    } else {
 		sb.values[SpecificationBlock.CLOCKMIN_INDEX] = 0;
 		sb.values[SpecificationBlock.CLOCKMAX_INDEX] = 0;
diff --git a/src/avatartranslator/modelchecker/SpecificationTransition.java b/src/avatartranslator/modelchecker/SpecificationTransition.java
index a103472f85db01b5ae81cbd129e1bbf3e96b5562..3af6d35fc2894706b0056b2ec43fd093d12677c6 100644
--- a/src/avatartranslator/modelchecker/SpecificationTransition.java
+++ b/src/avatartranslator/modelchecker/SpecificationTransition.java
@@ -110,6 +110,26 @@ public class SpecificationTransition  {
 	
     }
 
+    public boolean hasBlockOf(SpecificationTransition _tr) {
+	if (blocks == null) {
+	    return false;
+	}
+
+	if (_tr.blocks == null) {
+	    return false;
+	}
+
+	for (int i=0; i<blocks.length; i++) {
+	    for(int j=0; j<_tr.blocks.length; j++) {
+		if (blocks[i] == blocks[j]) {
+		    return true;
+		}
+	    }
+	}
+
+	return false;
+    }
+
     public boolean hasBlockIndex(int _index) {
 	if (blocksInt == null) {
 	    return false;