diff --git a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
index 63644f70c13539ae69a8f731223a27edf5502bfd..ec4030e05e37455790088345f1401b58275b617e 100644
--- a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
+++ b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
@@ -97,6 +97,11 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
     private boolean livenessDone;
     private boolean studyLiveness;
     private SpecificationLiveness livenessInfo;
+    
+    //RG limits
+    private boolean stateLimitRG;
+    private boolean stateLimitReached;
+    private int stateLimit;
 
 
     public AvatarModelChecker(AvatarSpecification _spec) {
@@ -114,6 +119,8 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
         ignoreInternalStates = true;
         studyReachability = false;
         computeRG = false;
+        stateLimitRG = false; //No state limit in RG computation
+        stateLimit = Integer.MAX_VALUE;
         freeIntermediateStateCoding = true;
     }
 
@@ -234,6 +241,14 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
     public void setComputeRG(boolean _rg) {
         computeRG = _rg;
     }
+    
+    public void setStateLimit(boolean _stateLimitRG) {
+    	stateLimitRG = _stateLimitRG; //_stateLimitRG;
+    }
+    
+    public void setStateLimitValue(int _stateLimit) {
+    	stateLimit = _stateLimit;
+    }
 
     /*private synchronized boolean startMC() {
 	
@@ -255,6 +270,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
         livenessDone = false;
         studyReachability = false;
         computeRG = false;
+        stateLimitRG = false;
 
 
         startModelChecking();
@@ -269,6 +285,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
         }
 
         stoppedBeforeEnd = false;
+        stateLimitReached = false;
         stateID = 0;
         nbOfDeadlocks = 0;
 
@@ -641,6 +658,15 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
                 //newState.id = getStateID();
                 //TraceManager.addDev("Putting new state with id = " +  newState.id + " stateID = " + stateID + " states size = " + states.size() + " states by id size = " + statesByID.size());
                 //statesByID.put(newState.id, newState);
+            	
+            	if (stateLimitRG && stateID >= stateLimit) {
+            		if (stateLimitReached) {
+            			continue;
+            		}
+            		stateLimitReached = true;
+            	}
+
+            	
                 if ((studyLiveness == false) || (studyLiveness && !(tr.livenessFound))) {
                     pendingStates.add(newState);
                 }
@@ -780,7 +806,14 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
                 action += " [" +  "0...0" +  "]";
                 link.action = action;
                 link.destinationState = newState;
-                addStateIfNotExisting(newState);
+                similar = addStateIfNotExisting(newState);
+                if (similar == null && stateLimitRG && (stateID >= stateLimit)) {
+            		// Reached limit in number of states
+                	if (stateLimitReached) {
+                		break;
+                	}
+                	stateLimitReached = true;
+            	}
                 pendingStates.add(newState);
                 nbOfLinks++;
                 _ss.addNext(link);
@@ -1435,7 +1468,11 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
     private synchronized SpecificationState addStateIfNotExisting(SpecificationState newState) {
         SpecificationState similar = states.get(newState.getHash(blockValues));
         if (similar == null) {
-            addState(newState);
+        	if (!(stateLimitRG && stateID >= stateLimit)) {
+        		addState(newState);
+        	} else {
+        		return null;
+    	    }
         }
         return similar;
     }
diff --git a/src/main/java/ui/window/JDialogAvatarModelChecker.java b/src/main/java/ui/window/JDialogAvatarModelChecker.java
index 51ddb00ca1bf39c0641cb666e8446bfcb7ec3758..3995567f676d4ba271eb1caf6691654989318754 100644
--- a/src/main/java/ui/window/JDialogAvatarModelChecker.java
+++ b/src/main/java/ui/window/JDialogAvatarModelChecker.java
@@ -94,6 +94,8 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
     protected static boolean generateDesignSelected = false;
     protected static int reachabilitySelected = REACHABILITY_NONE;
     protected static int livenessSelected = LIVENESS_NONE;
+    protected static boolean limitStatesSelected = false;
+    protected static String stateLimitValue;
 
     protected MainGUI mgui;
 
@@ -135,6 +137,8 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
     protected JRadioButton noLiveness, livenessCheckable, livenessAllStates;
     protected ButtonGroup liveness;
     protected boolean showLiveness;
+    protected JCheckBox stateLimit;
+    protected JTextField stateLimitField;
 
     protected JCheckBox saveGraphAUT, saveGraphDot, ignoreEmptyTransitions, ignoreInternalStates,
             ignoreConcurrenceBetweenInternalActions, generateDesign;
@@ -281,6 +285,13 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
         livenessCheckable.setSelected(livenessSelected == LIVENESS_SELECTED);
         livenessAllStates.setSelected(livenessSelected == LIVENESS_ALL);
 
+        //Limitations
+        stateLimit = new JCheckBox("Limit number of states in GF", limitStatesSelected);
+        stateLimit.addActionListener(this);
+        jp01.add(stateLimit, c01);
+        stateLimitField = new JTextField(stateLimitValue);
+        jp01.add(stateLimitField, c01);
+
 
         // RG
         saveGraphAUT = new JCheckBox("Reachability Graph Generation", graphSelected);
@@ -574,6 +585,22 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
                 amc.setComputeRG(true);
                 jta.append("Computation of Reachability Graph activated\n");
             }
+            
+            
+            if (stateLimit.isSelected()) {
+            	amc.setStateLimit(true);
+				try{
+					int stateLimitInt = Integer.parseInt(stateLimitField.getText());
+					if (stateLimitInt < 0) {
+						jta.append("State Limit field is not valid, insert a positive number\n");
+						go = false;
+					}
+					amc.setStateLimitValue(stateLimitInt);
+				} catch (NumberFormatException e) {
+					jta.append("State Limit field is not valid\n");
+					go = false;
+				}
+            }
 
             // Starting model checking
             testGo();
@@ -721,6 +748,8 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
         } else {
             reachabilitySelected = REACHABILITY_ALL;
         }
+        
+        stateLimitField.setEnabled(stateLimit.isSelected());
 
         switch (mode) {
             case NOT_STARTED: