Browse Source

JDDVars: add method allZero() for obtaining a cubeset with all the variables negated

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11940 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Joachim Klein 9 years ago
parent
commit
f155656282
  1. 15
      prism/src/jdd/JDDVars.java

15
prism/src/jdd/JDDVars.java

@ -372,6 +372,21 @@ public class JDDVars implements Iterable<JDDNode>
return result; return result;
} }
/**
* Constructs a 0/1-ADD that is the conjunction of
* the negated variables, i.e.,
* And(Not(v_1), Not(v_2), ..., Not(v_n))
* <br>[ REFS: <i>result</i>, DEREFS: <i>none</i> ]
*/
public JDDNode allZero()
{
JDDNode result = JDD.Constant(1);
for (JDDNode var : vars) {
result = JDD.And(result, JDD.Not(var.copy()));
}
return result;
}
/** Sort the variables in this container by their variable index. */ /** Sort the variables in this container by their variable index. */
public void sortByIndex() public void sortByIndex()
{ {

Loading…
Cancel
Save