Allow unbounded integer variables in model (but forbid for symbolic model construction).

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6929 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/explicit/ConstructModel.java

@@ -34,6 +34,7 @@ import java.util.List;
 
 import parser.State;
 import parser.Values;
+import parser.VarList;
 import parser.ast.ModulesFile;
 import prism.ModelType;
 import prism.Prism;
@@ -144,6 +145,11 @@ public class ConstructModel
 			throw new PrismException("Cannot do explicit-state reachability if there are multiple initial states");
 		}
 
+		// Display a warning if there are unbounded vars
+		VarList varList = modulesFile.createVarList();
+		if (varList.containsUnboundedVariables())
+			mainLog.printWarning("Model contains one or more unbounded variables: model construction may not terminate");
+		
 		// Starting reachability...
 		mainLog.print("\nComputing reachable states...");
 		mainLog.flush();

prism/src/parser/PrismParser.java

@@ -894,6 +894,10 @@ public class PrismParser implements PrismParserConstants {
       jj_consume_token(RBRACKET);
                   declType = new DeclarationInt(low, high);
       break;
+    case INT:
+      jj_consume_token(INT);
+                    declType = new DeclarationIntUnbounded();
+      break;
     case BOOL:
       jj_consume_token(BOOL);
                      declType = new DeclarationBool();
@@ -3125,16 +3129,6 @@ public class PrismParser implements PrismParserConstants {
     finally { jj_save(14, xla); }
   }
 
-  static private boolean jj_3R_51() {
-    if (jj_3R_59()) return true;
-    Token xsp;
-    while (true) {
-      xsp = jj_scanpos;
-      if (jj_3R_60()) { jj_scanpos = xsp; break; }
-    }
-    return false;
-  }
-
   static private boolean jj_3R_52() {
     if (jj_scan_token(QMARK)) return true;
     if (jj_3R_51()) return true;
@@ -4398,6 +4392,16 @@ public class PrismParser implements PrismParserConstants {
     return false;
   }
 
+  static private boolean jj_3R_51() {
+    if (jj_3R_59()) return true;
+    Token xsp;
+    while (true) {
+      xsp = jj_scanpos;
+      if (jj_3R_60()) { jj_scanpos = xsp; break; }
+    }
+    return false;
+  }
+
   static private boolean jj_initialized_once = false;
   /** Generated Token Manager. */
   static public PrismParserTokenManager token_source;
@@ -4420,7 +4424,7 @@ public class PrismParser implements PrismParserConstants {
       jj_la1_init_2();
    }
    private static void jj_la1_init_0() {
-      jj_la1_0 = new int[] {0x514404c0,0x504404c0,0x1000000,0xb01a0848,0x0,0xb01a0848,0xb01a0848,0x0,0xb01a0848,0x400,0x40000000,0x80,0x40000480,0x8000210,0x8000210,0x0,0x40,0x0,0x1000000,0x30,0x0,0x2000000,0x0,0x0,0x0,0xa0ba0808,0x0,0x0,0x0,0xa0ba0808,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0xa00000,0x0,0xa0ba0808,0xa0ba0808,0xa0ba0808,0xa0ba0808,0xa0ba0808,0x0,0x0,0x0,0x0,0x0,0x0,0xa01a0808,0x0,0x0,0x0,0x0,0x0,0x0,0xa01a0808,0xa01a0808,0x0,0xa0000000,0xa0000000,0x0,0x20000,0xa0000000,0x0,0x0,0x0,0xa0000000,0x0,0x0,0x0,0xa0000000,0x0,0x0,0xa0ba0808,0x4200100,0x1000000,0xa0000000,0x0,0xa0000000,0x0,0x0,0x0,};
+      jj_la1_0 = new int[] {0x514404c0,0x504404c0,0x1000000,0xb01a0848,0x0,0xb01a0848,0xb01a0848,0x0,0xb01a0848,0x400,0x40000000,0x80,0x40000480,0x8000210,0x8000210,0x0,0x40,0x0,0x1000000,0x8000030,0x0,0x2000000,0x0,0x0,0x0,0xa0ba0808,0x0,0x0,0x0,0xa0ba0808,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0xa00000,0x0,0xa0ba0808,0xa0ba0808,0xa0ba0808,0xa0ba0808,0xa0ba0808,0x0,0x0,0x0,0x0,0x0,0x0,0xa01a0808,0x0,0x0,0x0,0x0,0x0,0x0,0xa01a0808,0xa01a0808,0x0,0xa0000000,0xa0000000,0x0,0x20000,0xa0000000,0x0,0x0,0x0,0xa0000000,0x0,0x0,0x0,0xa0000000,0x0,0x0,0xa0ba0808,0x4200100,0x1000000,0xa0000000,0x0,0xa0000000,0x0,0x0,0x0,};
    }
    private static void jj_la1_init_1() {
       jj_la1_1 = new int[] {0x187c5,0x83c4,0x10401,0x40127ab8,0x8000000,0x40127ab8,0x40127ab8,0x8000000,0x40127ab8,0x40,0x4,0x8000,0x8144,0x0,0x0,0x280,0x280,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x4012783a,0x200000,0x40020000,0x10000000,0x4012783a,0x0,0x0,0x10000000,0x0,0x10000000,0x10000000,0x0,0x40000000,0xc2000,0x0,0xc2000,0x2,0x0,0x4012783a,0x4012783a,0x4012783a,0x4012783a,0x4012783a,0x0,0x0,0x800000,0x1000000,0x400000,0x200000,0x40127838,0x0,0x0,0x0,0x0,0x0,0x0,0x40027838,0x40027838,0x40000000,0x0,0x0,0x10000000,0x20000,0x0,0x38,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x3800,0x0,0x4012783a,0x4000,0x0,0x600000,0x10000000,0x0,0x0,0x0,0x4000000,};

prism/src/parser/PrismParser.jj

@@ -711,6 +711,8 @@ DeclarationType DeclarationVarType() :
 	// Integer-range declaration
 	( <LBRACKET> low = Expression(false, false) <DOTS> high = Expression(false, false) <RBRACKET>
 		{ declType = new DeclarationInt(low, high); } )
+	// Integer (unbounded) declaration
+	| ( <INT> { declType = new DeclarationIntUnbounded(); } )
 	// Boolean variable declaration
 	| ( <BOOL> { declType = new DeclarationBool(); } )
 	// Array variable declaration

prism/src/parser/VarList.java

@@ -142,7 +142,7 @@ public class VarList
 		var.module = module;
 
 		declType = decl.getDeclType();
-		// Variable is integer
+		// Variable is a bounded integer
 		if (declType instanceof DeclarationInt) {
 			DeclarationInt intdecl = (DeclarationInt) declType;
 			low = intdecl.getLow().evaluateInt(constantValues);
@@ -163,18 +163,29 @@ public class VarList
 				throw new PrismLangException(s, decl);
 			}
 		}
-		// Variable is boolean
+		// Variable is a Boolean
 		else if (declType instanceof DeclarationBool) {
 			low = 0;
 			high = 1;
 			start = (decl.getStartOrDefault().evaluateBoolean(constantValues)) ? 1 : 0;
 		}
-		// Otherwise (i.e. clock) create dummy info
-		else {
+		// Variable is a clock
+		else if (declType instanceof DeclarationClock) {
+			// Create dummy info
 			low = 0;
 			high = 1;
 			start = 0;
 		}
+		// Variable is an (unbounded) integer
+		else if (declType instanceof DeclarationIntUnbounded) {
+			// Create dummy range info
+			low = 0;
+			high = 1;
+			start = decl.getStartOrDefault().evaluateInt(constantValues);
+		}
+		else {
+			throw new PrismLangException("Unknown variable type \"" + declType + "\" in declaration", decl);
+		}
 
 		// Store low/high/start and return
 		var.low = low;
@@ -434,6 +445,21 @@ public class VarList
 		return state;
 	}
 
+	/**
+	 * Does the variable list contain any variables with unbounded range (e.g. "clock: or "int")?
+	 */
+	public boolean containsUnboundedVariables()
+	{
+		int n = getNumVars();
+		for (int i = 0; i < n; i++) {
+			DeclarationType declType = getDeclaration(i).getDeclType();
+			if (declType instanceof DeclarationClock || declType instanceof DeclarationIntUnbounded) {
+				return true;
+			}
+		}
+		return false;
+	}
+	
 	/**
 	 * Clone this list.
 	 */

prism/src/parser/ast/DeclarationIntUnbounded.java

@@ -0,0 +1,91 @@
+//==============================================================================
+//	
+//	Copyright (c) 2002-
+//	Authors:
+//	* Dave Parker <d.a.parker@cs.bham.ac.uk> (University of Birmingham/Oxford)
+//	
+//------------------------------------------------------------------------------
+//	
+//	This file is part of PRISM.
+//	
+//	PRISM is free software; you can redistribute it and/or modify
+//	it under the terms of the GNU General Public License as published by
+//	the Free Software Foundation; either version 2 of the License, or
+//	(at your option) any later version.
+//	
+//	PRISM is distributed in the hope that it will be useful,
+//	but WITHOUT ANY WARRANTY; without even the implied warranty of
+//	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//	GNU General Public License for more details.
+//	
+//	You should have received a copy of the GNU General Public License
+//	along with PRISM; if not, write to the Free Software Foundation,
+//	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
+//	
+//==============================================================================
+
+package parser.ast;
+
+import parser.type.*;
+import parser.visitor.ASTVisitor;
+import prism.PrismLangException;
+
+public class DeclarationIntUnbounded extends DeclarationType
+{
+	public DeclarationIntUnbounded()
+	{
+		// The type stored for a Declaration/DeclarationType object
+		// is static - it is not computed during type checking.
+		// (But we re-use the existing "type" field for this purpose)
+		setType(TypeInt.getInstance());
+	}
+
+	/**
+	 * Return the default start value for a variable of this type.
+	 */
+	public Expression getDefaultStart()
+	{
+		return Expression.Int(0);
+	}
+	
+	/* TODO:
+	@Override
+	public Expression getStart(ModulesFile parent)
+	{
+		if (parent != null && parent.getInitialStates() != null)
+			return null;
+
+		return start != null ? start : low;
+	}
+	*/
+	
+	// Methods required for ASTElement:
+	
+	/**
+	 * Visitor method.
+	 */
+	public Object accept(ASTVisitor v) throws PrismLangException
+	{
+		return v.visit(this);
+	}
+
+	/**
+	 * Convert to string.
+	 */
+	@Override
+	public String toString()
+	{
+		return "int";
+	}
+
+	/**
+	 * Perform a deep copy.
+	 */
+	@Override
+	public ASTElement deepCopy()
+	{
+		DeclarationIntUnbounded ret = new DeclarationIntUnbounded();
+		ret.setPosition(this);
+		return ret;
+	}
+}

prism/src/parser/visitor/ASTTraverse.java

@@ -187,6 +187,15 @@ public class ASTTraverse implements ASTVisitor
 	}
 	public void visitPost(DeclarationClock e) throws PrismLangException { defaultVisitPost(e); }
 	// -----------------------------------------------------------------------------------
+	public void visitPre(DeclarationIntUnbounded e) throws PrismLangException { defaultVisitPre(e); }
+	public Object visit(DeclarationIntUnbounded e) throws PrismLangException
+	{
+		visitPre(e);
+		visitPost(e);
+		return null;
+	}
+	public void visitPost(DeclarationIntUnbounded e) throws PrismLangException { defaultVisitPost(e); }
+	// -----------------------------------------------------------------------------------
 	public void visitPre(Module e) throws PrismLangException { defaultVisitPre(e); }
 	public Object visit(Module e) throws PrismLangException
 	{

prism/src/parser/visitor/ASTTraverseModify.java

@@ -199,6 +199,15 @@ public class ASTTraverseModify implements ASTVisitor
 	}
 	public void visitPost(DeclarationClock e) throws PrismLangException { defaultVisitPost(e); }
 	// -----------------------------------------------------------------------------------
+	public void visitPre(DeclarationIntUnbounded e) throws PrismLangException { defaultVisitPre(e); }
+	public Object visit(DeclarationIntUnbounded e) throws PrismLangException
+	{
+		visitPre(e);
+		visitPost(e);
+		return e;
+	}
+	public void visitPost(DeclarationIntUnbounded e) throws PrismLangException { defaultVisitPost(e); }
+	// -----------------------------------------------------------------------------------
 	public void visitPre(Module e) throws PrismLangException { defaultVisitPre(e); }
 	public Object visit(Module e) throws PrismLangException
 	{

prism/src/parser/visitor/ASTVisitor.java

@@ -43,6 +43,7 @@ public interface ASTVisitor
 	public Object visit(DeclarationBool e) throws PrismLangException;
 	public Object visit(DeclarationArray e) throws PrismLangException;
 	public Object visit(DeclarationClock e) throws PrismLangException;
+	public Object visit(DeclarationIntUnbounded e) throws PrismLangException;
 	public Object visit(Module e) throws PrismLangException;
 	public Object visit(Command e) throws PrismLangException;
 	public Object visit(Updates e) throws PrismLangException;

prism/src/prism/Modules2MTBDD.java

@@ -180,6 +180,8 @@ public class Modules2MTBDD
 		
 		// get variable info from ModulesFile
 		varList = modulesFile.createVarList();
+		if (varList.containsUnboundedVariables())
+			throw new PrismException("Cannot build a model that contains a variable with unbounded range (try the explicit engine instead)");
 		numVars = varList.getNumVars();
 		constantValues = modulesFile.getConstantValues();
 		

prism/src/userinterface/model/GUIMultiModelTree.java

@@ -836,10 +836,16 @@ public class GUIMultiModelTree extends JPanel implements MouseListener
                     Declaration notTreeDec = (Declaration)varNotInTree.get(j);
                     if(notTreeDec.getType() instanceof TypeInt)
                     {
-                    	DeclarationInt declInt = (DeclarationInt)notTreeDec.getDeclType();
-                        VarNode newVariable = new VarNode(notTreeDec.getName(), parsedModel.getSystemDefn() == null ? notTreeDec.getStartOrDefault() : null, declInt.getLow(), declInt.getHigh(), false);
-                        inTreeNode.add(newVariable);
-                        cIndices[j] = getVarTreeIndexOf(notTreeDec, inTreeNode);
+                    	if (notTreeDec.getDeclType() instanceof DeclarationInt) {
+							DeclarationInt declInt = (DeclarationInt) notTreeDec.getDeclType();
+							VarNode newVariable = new VarNode(notTreeDec.getName(), parsedModel.getSystemDefn() == null ? notTreeDec.getStartOrDefault() : null, declInt.getLow(), declInt.getHigh(), false);
+							inTreeNode.add(newVariable);
+							cIndices[j] = getVarTreeIndexOf(notTreeDec, inTreeNode);
+                    	} else {
+							VarNode newVariable = new VarNode(notTreeDec.getName(), parsedModel.getSystemDefn() == null ? notTreeDec.getStartOrDefault() : null, null, null, false);
+							inTreeNode.add(newVariable);
+							cIndices[j] = getVarTreeIndexOf(notTreeDec, inTreeNode);
+                    	}
                     }
                     else if(notTreeDec.getType() instanceof TypeBool)
                     {
@@ -849,7 +855,6 @@ public class GUIMultiModelTree extends JPanel implements MouseListener
                     }
                     else if(notTreeDec.getType() instanceof TypeClock)
                     {
-                    	DeclarationClock declClk = (DeclarationClock)notTreeDec.getDeclType();
                         VarNode newVariable = new VarNode(notTreeDec.getName(), parsedModel.getSystemDefn() == null ? notTreeDec.getStartOrDefault() : null, Expression.Int(0), null, false);
                         inTreeNode.add(newVariable);
                         cIndices[j] = getVarTreeIndexOf(notTreeDec, inTreeNode);
@@ -897,9 +902,14 @@ public class GUIMultiModelTree extends JPanel implements MouseListener
                     
                     if(aDec.getType() instanceof TypeInt)
                     {
-                    	DeclarationInt declInt = (DeclarationInt)aDec.getDeclType();
-                        VarNode newVariable = new VarNode(aDec.getName(), parsedModel.getSystemDefn() == null ? aDec.getStartOrDefault() : null, declInt.getLow(), declInt.getHigh(), false);
-                        newNode.add(newVariable);
+                    	if (aDec.getDeclType() instanceof DeclarationInt) {
+                        	DeclarationInt declInt = (DeclarationInt)aDec.getDeclType();
+                            VarNode newVariable = new VarNode(aDec.getName(), parsedModel.getSystemDefn() == null ? aDec.getStartOrDefault() : null, declInt.getLow(), declInt.getHigh(), false);
+                            newNode.add(newVariable);
+                    	} else {
+							VarNode newVariable = new VarNode(aDec.getName(), parsedModel.getSystemDefn() == null ? aDec.getStartOrDefault() : null, null, null, false);
+	                        newNode.add(newVariable);
+                    	}
                     }
                     else if(aDec.getType() instanceof TypeBool)
                     {