From fe4cd9560c7beacb6f63ed73e8a6fd311faeef43 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 14 Jun 2013 09:36:39 +0000 Subject: [PATCH] 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 | 6 ++ prism/src/parser/PrismParser.java | 26 +++--- prism/src/parser/PrismParser.jj | 2 + prism/src/parser/VarList.java | 34 ++++++- .../parser/ast/DeclarationIntUnbounded.java | 91 +++++++++++++++++++ prism/src/parser/visitor/ASTTraverse.java | 9 ++ .../src/parser/visitor/ASTTraverseModify.java | 9 ++ prism/src/parser/visitor/ASTVisitor.java | 1 + prism/src/prism/Modules2MTBDD.java | 2 + .../model/GUIMultiModelTree.java | 26 ++++-- 10 files changed, 183 insertions(+), 23 deletions(-) create mode 100644 prism/src/parser/ast/DeclarationIntUnbounded.java diff --git a/prism/src/explicit/ConstructModel.java b/prism/src/explicit/ConstructModel.java index 96f63830..f83b7c9b 100644 --- a/prism/src/explicit/ConstructModel.java +++ b/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(); diff --git a/prism/src/parser/PrismParser.java b/prism/src/parser/PrismParser.java index 62d7fc85..f9d6b2eb 100644 --- a/prism/src/parser/PrismParser.java +++ b/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,}; diff --git a/prism/src/parser/PrismParser.jj b/prism/src/parser/PrismParser.jj index a8997bb3..945d06e7 100644 --- a/prism/src/parser/PrismParser.jj +++ b/prism/src/parser/PrismParser.jj @@ -711,6 +711,8 @@ DeclarationType DeclarationVarType() : // Integer-range declaration ( low = Expression(false, false) high = Expression(false, false) { declType = new DeclarationInt(low, high); } ) + // Integer (unbounded) declaration + | ( { declType = new DeclarationIntUnbounded(); } ) // Boolean variable declaration | ( { declType = new DeclarationBool(); } ) // Array variable declaration diff --git a/prism/src/parser/VarList.java b/prism/src/parser/VarList.java index 90cf8379..cd64b3c7 100644 --- a/prism/src/parser/VarList.java +++ b/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. */ diff --git a/prism/src/parser/ast/DeclarationIntUnbounded.java b/prism/src/parser/ast/DeclarationIntUnbounded.java new file mode 100644 index 00000000..0da204f0 --- /dev/null +++ b/prism/src/parser/ast/DeclarationIntUnbounded.java @@ -0,0 +1,91 @@ +//============================================================================== +// +// Copyright (c) 2002- +// Authors: +// * Dave Parker (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; + } +} diff --git a/prism/src/parser/visitor/ASTTraverse.java b/prism/src/parser/visitor/ASTTraverse.java index ea3e86c2..6241ca7d 100644 --- a/prism/src/parser/visitor/ASTTraverse.java +++ b/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 { diff --git a/prism/src/parser/visitor/ASTTraverseModify.java b/prism/src/parser/visitor/ASTTraverseModify.java index 59826150..3c19fbbd 100644 --- a/prism/src/parser/visitor/ASTTraverseModify.java +++ b/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 { diff --git a/prism/src/parser/visitor/ASTVisitor.java b/prism/src/parser/visitor/ASTVisitor.java index 6e8b1620..9b88e193 100644 --- a/prism/src/parser/visitor/ASTVisitor.java +++ b/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; diff --git a/prism/src/prism/Modules2MTBDD.java b/prism/src/prism/Modules2MTBDD.java index 536ef43a..30500521 100644 --- a/prism/src/prism/Modules2MTBDD.java +++ b/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(); diff --git a/prism/src/userinterface/model/GUIMultiModelTree.java b/prism/src/userinterface/model/GUIMultiModelTree.java index fc727e83..a50f6a3b 100644 --- a/prism/src/userinterface/model/GUIMultiModelTree.java +++ b/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) {