diff --git a/modeling/MicroWaveOven_SafetySecurity_fullMethodo.xml b/modeling/MicroWaveOven_SafetySecurity_fullMethodo.xml
index 3e543af08a538b72f5331402041e5ff11435e1aa..237888af9472878bd1a0f56b40f72b8dcf9982d7 100644
--- a/modeling/MicroWaveOven_SafetySecurity_fullMethodo.xml
+++ b/modeling/MicroWaveOven_SafetySecurity_fullMethodo.xml
@@ -5174,7 +5174,7 @@ or by a maintenance station
 </CONNECTOR>
 <COMPONENT type="302" id="2683" >
 <cdparam x="382" y="26" />
-<sizeparam width="616" height="97" minWidth="80" minHeight="10" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<sizeparam width="668" height="97" minWidth="80" minHeight="10" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
 <hidden value="false" />
 <cdrectangleparam minX="10" maxX="1400" minY="10" maxY="1400" />
 <infoparam name="Proverif Pragma" value="#InitialSystemKnowledge RemoteControl.PSK WirelessInterface.PSK
diff --git a/src/avatartranslator/modelchecker/AvatarModelChecker.java b/src/avatartranslator/modelchecker/AvatarModelChecker.java
index 77a4157c86829546dfda6e58707d52a650d1c11d..8c4efb953d105ee93efdc4ef17a8cdb3cb1b6064 100644
--- a/src/avatartranslator/modelchecker/AvatarModelChecker.java
+++ b/src/avatartranslator/modelchecker/AvatarModelChecker.java
@@ -239,7 +239,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
         prepareTransitionsOfState(initialState);
         blockValues = initialState.getBlockValues();
 
-        //TraceManager.addDev("initialState=" + initialState.toString());
+        //TraceManager.addDev("initialState=" + initialState.toString() + " nbOfTransitions" + initialState.transitions.size());
         initialState.computeHash(blockValues);
         states.put(initialState.hashValue, initialState);
 	statesByID.put(initialState.id, initialState);
@@ -368,7 +368,15 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
 
 
     private void computeAllStatesFrom(SpecificationState _ss) {
+	if (_ss == null) {
+	    mustStop();
+	    return;
+	}
         ArrayList<SpecificationTransition> transitions = _ss.transitions;
+	if (transitions == null) {
+	    mustStop();
+	    return;
+	}
 
         //TraceManager.addDev("Possible transitions 1:" + transitions.size());
 
@@ -977,9 +985,11 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
         }
         sb.append("\nLinks:\n");
         for(SpecificationState state: states.values()) {
-            for(SpecificationLink link: state.nexts) {
-                sb.append(link.toString() + "\n");
-            }
+	    if (state.nexts != null) {
+		for(SpecificationLink link: state.nexts) {
+		    sb.append(link.toString() + "\n");
+		}
+	    }
         }
         return sb.toString();
     }
@@ -990,9 +1000,11 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
         sb.append("des(0," + getNbOfLinks() + "," + getNbOfStates() + ")\n");
 
         for(SpecificationState state: states.values()) {
-            for(SpecificationLink link: state.nexts) {
+	     if (state.nexts != null) {
+		 for(SpecificationLink link: state.nexts) {
                 sb.append("(" + link.originState.id + ",\"" + link.action + "\"," + link.destinationState.id + ")\n");
-            }
+		 }
+	     }
         }
         return new String(sb);
     }
@@ -1002,10 +1014,12 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
         sb.append("digraph TToolAvatarGraph {\n");
 
         for(SpecificationState state: states.values()) {
-            for(SpecificationLink link: state.nexts) {
+	    if (state.nexts != null) {
+		for(SpecificationLink link: state.nexts) {
 
-                sb.append(" " + link.originState.id + " -> " + link.destinationState.id  + "[label=\"" + link.action + "\"];\n");
-            }
+		    sb.append(" " + link.originState.id + " -> " + link.destinationState.id  + "[label=\"" + link.action + "\"];\n");
+		}
+	    }
         }
         sb.append("}");
         return new String(sb);