|
|
@ -145,7 +145,7 @@ public class SCCComputerLockstep implements SCCComputer |
|
|
JDDNode current; |
|
|
JDDNode current; |
|
|
JDDNode img; |
|
|
JDDNode img; |
|
|
JDDNode pre; |
|
|
JDDNode pre; |
|
|
int i = 1; |
|
|
|
|
|
|
|
|
//int i = 1; |
|
|
|
|
|
|
|
|
JDD.Ref(nodes); |
|
|
JDD.Ref(nodes); |
|
|
current = nodes; |
|
|
current = nodes; |
|
|
@ -158,11 +158,11 @@ public class SCCComputerLockstep implements SCCComputer |
|
|
JDD.Ref(edges); |
|
|
JDD.Ref(edges); |
|
|
pre = preimage(current, edges); |
|
|
pre = preimage(current, edges); |
|
|
current = JDD.And(current, JDD.And(img, pre)); |
|
|
current = JDD.And(current, JDD.And(img, pre)); |
|
|
if (prism.getVerbose()) { |
|
|
|
|
|
|
|
|
/*if (prism.getVerbose()) { |
|
|
log.println("Trimming pass " + i + ":"); |
|
|
log.println("Trimming pass " + i + ":"); |
|
|
JDD.PrintVector(current, rows); |
|
|
JDD.PrintVector(current, rows); |
|
|
i++; |
|
|
i++; |
|
|
} |
|
|
|
|
|
|
|
|
}*/ |
|
|
} while (!current.equals(old)); |
|
|
} while (!current.equals(old)); |
|
|
JDD.Deref(nodes); |
|
|
JDD.Deref(nodes); |
|
|
JDD.Deref(edges); |
|
|
JDD.Deref(edges); |
|
|
|