From eb7d617c0e0492514f6c96122a3db52034db8221 Mon Sep 17 00:00:00 2001
From: Vojtech Forejt <forejtv@gmail.com>
Date: Wed, 11 May 2011 20:21:33 +0000
Subject: [PATCH] added a random comment about a need to call
 initialiseIterators

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2863 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/prism/UndefinedConstants.java | 30 +++++++++++++++++++------
 1 file changed, 23 insertions(+), 7 deletions(-)

diff --git a/prism/src/prism/UndefinedConstants.java b/prism/src/prism/UndefinedConstants.java
index 815af811..04154075 100644
--- a/prism/src/prism/UndefinedConstants.java
+++ b/prism/src/prism/UndefinedConstants.java
@@ -228,18 +228,34 @@ public class UndefinedConstants
 		}
 	}
 
-	// define value for a single undefined constant
-	// returns whether or not an existing definition was overwritten
-	// actually just helper method for more general method below
-	
+	/** Define value for a single undefined constant.
+	 *  Returns whether or not an existing definition was overwritten.
+     *	Actually just helper method for more general method {@link #defineConstant(String, String, String, String) below}.
+     *  
+     *  The method {@link #initialiseIterators() initialiseIterators} must be called after all constants are defined.
+	 *
+	 *  @param name The name of the constant.
+	 *  @param val The value to be assigned.
+	 *  
+	 *  @return True if the constant was defined before.
+	 */
 	public boolean defineConstant(String name, String val) throws PrismException
 	{
 		return defineConstant(name, val, null, null);
 	}
 
-	// define value for a single undefined constant
-	// returns whether or not an existing definition was overwritten
-	
+	/** Define value for a single undefined constant.
+	 *  Returns whether or not an existing definition was overwritten.
+	 *
+	 *  The method {@link #initialiseIterators() initialiseIterators} must be called after all constants are defined.
+	 *	
+	 *  @param name The name of the constant.
+	 *  @param sl If sh are sl are null, this is the value to be assigned. Otherwise, it is the lower bound for the range.
+	 *  @param sh The upper bound for the range.
+	 *  @param ss The step for the values. Null means 1.
+	 *  
+	 *  @return True if the constant was defined before.
+	 */
 	public boolean defineConstant(String name, String sl, String sh, String ss) throws PrismException
 	{
 		int index = 0;