From 0f9e001645d73a3e44a1c190d3fff56f5655929a Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 27 Aug 2015 12:44:55 +0000 Subject: [PATCH] Bug fix in CNF conversion (from Yuyang). git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10595 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/etc/scripts/prism-auto | 2 ++ prism/src/parser/BooleanUtils.java | 2 +- 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/prism/etc/scripts/prism-auto b/prism/etc/scripts/prism-auto index 6251d49d..0189926d 100755 --- a/prism/etc/scripts/prism-auto +++ b/prism/etc/scripts/prism-auto @@ -668,6 +668,8 @@ if options.logDir and not os.path.isdir(options.logDir): print "Log directory \"" + options.logDir + "\" does not exist" sys.exit(1) if options.nailgun: + exitCode = subprocess.Popen([options.ngprism, "--nailgun-help"], stderr=open(os.devnull, 'w')).wait() + print exitCode os.system(options.prismExec + " -ng &") time.sleep(0.5) for arg in args: diff --git a/prism/src/parser/BooleanUtils.java b/prism/src/parser/BooleanUtils.java index e5c3183e..31e2ea27 100644 --- a/prism/src/parser/BooleanUtils.java +++ b/prism/src/parser/BooleanUtils.java @@ -133,7 +133,7 @@ public class BooleanUtils return Expression.Or(Expression.Not(a), b); } // Remove iff: a <=> b - if (Expression.isImplies(e)) { + if (Expression.isIff(e)) { Expression a = (Expression)(e.getOperand1().accept(this)); Expression b = (Expression)(e.getOperand2().accept(this)); // a <=> b == (a | !b) & (!a | b)