Browse Source

JDD: add Equiv BDD operation (dd1 <=> dd2)

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11219 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Joachim Klein 10 years ago
parent
commit
71183e47e7
  1. 9
      prism/src/jdd/JDD.java

9
prism/src/jdd/JDD.java

@ -421,6 +421,15 @@ public class JDD
return ptrToNode(DD_Implies(dd1.ptr(), dd2.ptr())); return ptrToNode(DD_Implies(dd1.ptr(), dd2.ptr()));
} }
/**
* equivalence of dd1, dd2 (have to be 0/1-MTBDDs)
* [ REFS: <i>result</i>, DEREFS: dd1, dd2 ]
*/
public static JDDNode Equiv(JDDNode dd1, JDDNode dd2)
{
return Not(Xor(dd1, dd2));
}
/** /**
* generic apply operation * generic apply operation
* <br>[ REFS: <i>result</i>, DEREFS: dd1, dd2 ] * <br>[ REFS: <i>result</i>, DEREFS: dd1, dd2 ]

Loading…
Cancel
Save