Browse Source

Bug fix in CNF conversion (from Yuyang).

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10595 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 10 years ago
parent
commit
0f9e001645
  1. 2
      prism/etc/scripts/prism-auto
  2. 2
      prism/src/parser/BooleanUtils.java

2
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:

2
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)

Loading…
Cancel
Save