diff --git a/src/main/java/avatartranslator/AvatarExpressionAttribute.java b/src/main/java/avatartranslator/AvatarExpressionAttribute.java
index 0ca60b084df1368030ff3bcd047b6b5467ef5ac4..bcf8ffe0352006892e0d729fbd5b6d457ca87413 100644
--- a/src/main/java/avatartranslator/AvatarExpressionAttribute.java
+++ b/src/main/java/avatartranslator/AvatarExpressionAttribute.java
@@ -78,6 +78,8 @@ public class AvatarExpressionAttribute {
         isState = true;
         state = asme;
         error = false;
+        accessIndex = -1;
+        block = null;
     }
 
     
@@ -116,8 +118,10 @@ public class AvatarExpressionAttribute {
                 return false;
             }
             isState = true;
+            accessIndex = block.getStateMachine().getIndexOfState((AvatarStateElement) state);
+        } else {
+            accessIndex = attributeIndex + SpecificationBlock.ATTR_INDEX;
         }
-        accessIndex = attributeIndex + SpecificationBlock.ATTR_INDEX;
         return true;
     }
     
@@ -139,9 +143,10 @@ public class AvatarExpressionAttribute {
                 return false;
             }
             isState = true;
+            accessIndex = block.getStateMachine().getIndexOfState((AvatarStateElement) state);
+        } else {
+            accessIndex = attributeIndex + SpecificationBlock.ATTR_INDEX;
         }
-        
-        accessIndex = attributeIndex + SpecificationBlock.ATTR_INDEX;
         return true;
     }
     
@@ -153,7 +158,14 @@ public class AvatarExpressionAttribute {
         int value;
         
         if (isState) {
-            return 0;
+            if (ss.blocks == null || accessIndex == -1) {
+                return 0;
+            }
+            if (ss.blocks[blockIndex].values[SpecificationBlock.STATE_INDEX] == accessIndex) {
+                return 1;
+            } else {
+                return 0;
+            }
         }
         
         value = ss.blocks[blockIndex].values[accessIndex];
@@ -177,7 +189,14 @@ public class AvatarExpressionAttribute {
         int value;
         
         if (isState) {
-            return 0;
+            if (sb == null || accessIndex == -1) {
+                return 0;
+            }     
+            if (sb.values[SpecificationBlock.STATE_INDEX] == accessIndex) {
+                return 1;
+            } else {
+                return 0;
+            }
         }
         
         value = sb.values[accessIndex];
@@ -209,6 +228,17 @@ public class AvatarExpressionAttribute {
         sb.values[accessIndex] = v;
     }
     
+    //Link state to access index in the state machine
+    public void linkState() {
+        if (isState) {
+            if (block != null) {
+                accessIndex = block.getStateMachine().getIndexOfState((AvatarStateElement) state);
+            } else {
+                accessIndex = -1;
+            }
+        }
+    }
+    
     public boolean isState() {
         return isState;
     }
diff --git a/src/main/java/avatartranslator/AvatarExpressionSolver.java b/src/main/java/avatartranslator/AvatarExpressionSolver.java
index bc7ee7060e894a6c7696e72abc02d999a72573e1..e73a5c237c823a4d6816b7a2cd46ed9b4b5e9ee9 100644
--- a/src/main/java/avatartranslator/AvatarExpressionSolver.java
+++ b/src/main/java/avatartranslator/AvatarExpressionSolver.java
@@ -635,6 +635,17 @@ public class AvatarExpressionSolver {
         }
     }
     
+    public void linkStates() {
+        if (isLeaf) {
+            if (isImmediateValue == IMMEDIATE_NO) {
+                leaf.linkState();
+            }
+        } else {
+            left.linkStates();
+            right.linkStates();
+        }
+    }
+    
     private void removeUselessBrackets() {
         while (expression.startsWith("(") && expression.endsWith(")")) {
             if (getClosingBracket(1) == expression.length() - 1) {
diff --git a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
index 58121c23abfc3c33c04e5ff8d90d3292fd7e93c2..e85496731c133710d27fe8c766ec90338fab25bd 100644
--- a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
+++ b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
@@ -590,15 +590,9 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
         }
         
         int cpt = 0;
-        for (AvatarBlock block : spec.getListOfBlocks()) {
-            AvatarStateMachine asm = block.getStateMachine();
-            SpecificationBlock sb = initialState.blocks[cpt];
-            AvatarStateMachineElement asme = asm.allStates[sb.values[SpecificationBlock.STATE_INDEX]];
-            if (studySafety && safety.propertyType == SafetyProperty.BLOCK_STATE) {
-                initialState.property |= safety.getSolverResult(initialState, asme);
-            }
-            cpt++;
-        }
+        
+        initialState.property |= safety.getSolverResult(initialState);
+
         if (studySafety && safety.propertyType == SafetyProperty.BLOCK_STATE) {
                 if (safety.safetyType == SafetyProperty.ALLTRACES_ALLSTATES || safety.safetyType == SafetyProperty.ONETRACE_ALLSTATES) {
                     initialState.property = !initialState.property;
@@ -662,11 +656,12 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
         if (ignoreEmptyTransitions) {
             spec.removeEmptyTransitions(!(studyReachability || studyLiveness || studySafety));
         }
-        
-        initExpressionSolvers();
 
         //TraceManager.addDev("Preparing Avatar specification :" + spec.toString());
         prepareStates();
+
+        initExpressionSolvers();
+
         prepareTransitions();
         prepareBlocks();
 
@@ -866,6 +861,13 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
                 }
             }
         }
+        
+        //To have all the leadsTo functionalities allStates in stateMachines must be filled with states
+        if (studySafety && safeties != null) {
+            for (SafetyProperty sp : safeties) {
+               sp.linkSolverStates();
+            }
+        }
     }
 
     private void prepareTransitionsOfState(SpecificationState _ss) {
@@ -1800,19 +1802,23 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
     
     private boolean evaluateSafetyOfProperty(SpecificationState newState, SpecificationTransition tr, boolean precProperty) {
         AvatarStateMachineElement asme;
-        boolean result = false;
+        boolean result;
         
         if (safety.propertyType == SafetyProperty.BLOCK_STATE) {
-            for (int i = 0; i < tr.transitions.length; i++) {
-                int k = 10;
-                asme = tr.transitions[i].getNext(0);
-                while (k > 0) {
-                    result |= safety.getSolverResult(newState, asme);
-                    if (asme instanceof AvatarStateElement || result == true) {
-                        break;
+            result = safety.getSolverResult(newState);
+            
+            if (!result) {
+                for (int i = 0; i < tr.transitions.length; i++) {
+                    int k = 10;
+                    asme = tr.transitions[i].getNext(0);
+                    while (k > 0) {
+                        result |= safety.getSolverResult(newState, asme);
+                        if (asme instanceof AvatarStateElement || result == true) {
+                            break;
+                        }
+                        asme = asme.getNext(0);
+                        k--;
                     }
-                    asme = asme.getNext(0);
-                    k--;
                 }
             }
         } else {
diff --git a/src/main/java/avatartranslator/modelchecker/SafetyProperty.java b/src/main/java/avatartranslator/modelchecker/SafetyProperty.java
index 0fff8d9062bb7c0aede741eaf725b73c05bb02a1..9c5c08638739b6bae2d300461e40aa0e609c58a2 100644
--- a/src/main/java/avatartranslator/modelchecker/SafetyProperty.java
+++ b/src/main/java/avatartranslator/modelchecker/SafetyProperty.java
@@ -193,6 +193,17 @@ public class SafetyProperty  {
     }
     
     
+    public void linkSolverStates() {
+        //linking to states so that normal bool elaborations are possible
+        if (safetySolver != null) {
+            safetySolver.linkStates();
+        }
+        if (safetySolverLead != null) {
+            safetySolverLead.linkStates();
+        }
+    }
+    
+    
     public String toString() {
         String ret = rawProperty;
         switch(phase) {