From 489c7fb2b346623aecd2cd62b972a826e8244bec Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 26 Mar 2010 16:13:55 +0000 Subject: [PATCH] Removed model construction warnings when guard is "false". git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1831 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/Modules2MTBDD.java | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/prism/src/prism/Modules2MTBDD.java b/prism/src/prism/Modules2MTBDD.java index b7a74605..8f94d4cb 100644 --- a/prism/src/prism/Modules2MTBDD.java +++ b/prism/src/prism/Modules2MTBDD.java @@ -1447,8 +1447,11 @@ public class Modules2MTBDD guardDDs[l] = JDD.Apply(JDD.TIMES, guardDDs[l], range); // check for false guard if (guardDDs[l].equals(JDD.ZERO)) { - String s = "\nWarning: Guard for command " + (l+1) + " of module \"" + module.getName() + "\" is never satisfied.\n"; - mainLog.print(s); + // display a warning (unless guard is "false", in which case was probably intentional + if (!Expression.isFalse(command.getGuard())) { + String s = "\nWarning: Guard for command " + (l+1) + " of module \"" + module.getName() + "\" is never satisfied.\n"; + mainLog.print(s); + } // no point bothering to compute the mtbdds for the update // if the guard is never satisfied upDDs[l] = JDD.Constant(0);