Method name typo: JDD.AreInterecting -> JDD.AreIntersecting.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10236 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/acceptance/AcceptanceGenRabinDD.java

@@ -110,14 +110,14 @@ public class AcceptanceGenRabinDD
 		 */
 		public boolean isBSCCAccepting(JDDNode bscc_states)
 		{
-			if (JDD.AreInterecting(L, bscc_states)) {
+			if (JDD.AreIntersecting(L, bscc_states)) {
 				// there is some state in bscc_states that is
 				// forbidden by L
 				return false;
 			}
 
 			for (JDDNode K_j : K_list) {
-				if (!JDD.AreInterecting(K_j, bscc_states)) {
+				if (!JDD.AreIntersecting(K_j, bscc_states)) {
 					// there is some state in bscc_states that is
 					// contained in K_j -> infinitely often visits to K_j
 					return false;

prism/src/acceptance/AcceptanceGenericDD.java

@@ -124,21 +124,21 @@ public class AcceptanceGenericDD implements AcceptanceOmegaDD {
 		case INF:
 			// bscc |= G F states?
 			// there exists a state in bscc and states
-			return JDD.AreInterecting(states, bscc);
+			return JDD.AreIntersecting(states, bscc);
 		case INF_NOT:
 			// bscc_state |= G F !states?
 			// the BSCC intersects Not(states)
 			JDD.Ref(states);
-			return JDD.AreInterecting(JDD.Not(states), bscc);
+			return JDD.AreIntersecting(JDD.Not(states), bscc);
 		case FIN:
 			// bscc |= F G !states?
 			// the BSCC consists only of !states
-			return !JDD.AreInterecting(states, bscc);
+			return !JDD.AreIntersecting(states, bscc);
 		case FIN_NOT:
 			// bscc |= F G states?
 			// the BSCC consists entirely of states
 			JDD.Ref(states);
-			return !JDD.AreInterecting(JDD.Not(states), bscc);
+			return !JDD.AreIntersecting(JDD.Not(states), bscc);
 		}
 		throw new UnsupportedOperationException("Unsupported operator in generic acceptance expression");
 	}

prism/src/acceptance/AcceptanceRabinDD.java

@@ -102,13 +102,13 @@ public class AcceptanceRabinDD
 		 */
 		public boolean isBSCCAccepting(JDDNode bscc_states)
 		{
-			if (JDD.AreInterecting(L, bscc_states)) {
+			if (JDD.AreIntersecting(L, bscc_states)) {
 				// there is some state in bscc_states that is
 				// forbidden by L
 				return false;
 			}
 
-			if (JDD.AreInterecting(K, bscc_states)) {
+			if (JDD.AreIntersecting(K, bscc_states)) {
 				// there is some state in bscc_states that is
 				// contained in K -> infinitely often visits to K
 				return true;

prism/src/acceptance/AcceptanceReachDD.java

@@ -89,7 +89,7 @@ public class AcceptanceReachDD implements AcceptanceOmegaDD
 	@Override
 	public boolean isBSCCAccepting(JDDNode bscc_states)
 	{
-		return JDD.AreInterecting(goalStates, bscc_states);
+		return JDD.AreIntersecting(goalStates, bscc_states);
 	}
 
 	@Override

prism/src/acceptance/AcceptanceStreettDD.java

@@ -102,11 +102,11 @@ public class AcceptanceStreettDD
 		 */
 		public boolean isBSCCAccepting(JDDNode bscc_states)
 		{
-			if (JDD.AreInterecting(R, bscc_states)) {
+			if (JDD.AreIntersecting(R, bscc_states)) {
 				// there is some state in bscc_states
 				// that is in R, requiring that G is visited
 				// as well:
-				if (!JDD.AreInterecting(G, bscc_states)) {
+				if (!JDD.AreIntersecting(G, bscc_states)) {
 					return false;
 				} else {
 					// G is visited as well

prism/src/jdd/JDD.java

@@ -440,7 +440,7 @@ public class JDD
 	 * Returns true if the two BDDs intersect (i.e. conjunction is non-empty).
 	 * [ REFS: <i>none</i>, DEREFS: <i>none</i> ]
 	 */
-	public static boolean AreInterecting(JDDNode dd1, JDDNode dd2)
+	public static boolean AreIntersecting(JDDNode dd1, JDDNode dd2)
 	{
 		JDDNode tmp;
 		boolean res;

prism/src/prism/LTLModelChecker.java

@@ -799,7 +799,7 @@ public class LTLModelChecker extends PrismComponent
 					// find ECs in acceptingStates that are accepting under K_i
 					acceptingStates = JDD.Constant(0);
 					for (JDDNode set : ecs) {
-						if (JDD.AreInterecting(set, acceptanceVector_K))
+						if (JDD.AreIntersecting(set, acceptanceVector_K))
 							acceptingStates = JDD.Or(acceptingStates, set);
 						else
 							JDD.Deref(set);
@@ -960,7 +960,7 @@ public class LTLModelChecker extends PrismComponent
 				//int count = 0;
 				acceptingStates = JDD.Constant(0);
 				for (JDDNode set : ecs) {
-					if (JDD.AreInterecting(set, acceptanceVector_L))
+					if (JDD.AreIntersecting(set, acceptanceVector_L))
 						acceptingStates = JDD.Or(acceptingStates, set);
 					else
 						JDD.Deref(set);
@@ -1068,7 +1068,7 @@ public class LTLModelChecker extends PrismComponent
 					if (ecs != null) {
 						boolean valid = false;
 						for (JDDNode set : ecs) {
-							if (JDD.AreInterecting(set, acceptanceVector_L)) {
+							if (JDD.AreIntersecting(set, acceptanceVector_L)) {
 								allAcceptingStates = JDD.Or(allAcceptingStates, set);
 								valid = true;
 							} else
@@ -1288,7 +1288,7 @@ public class LTLModelChecker extends PrismComponent
 	{
 		JDDNode union = JDD.Constant(0);
 		for (JDDNode set : sets) {
-			if (JDD.AreInterecting(set, filter))
+			if (JDD.AreIntersecting(set, filter))
 				union = JDD.Or(union, set);
 			else
 				JDD.Deref(set);

prism/src/prism/MultiObjModelChecker.java

@@ -218,7 +218,7 @@ public class MultiObjModelChecker extends PrismComponent
 		// TODO: check if the model satisfies the LTL constraints 
 		if (!rmecs.equals(JDD.ZERO)) {
 			boolean constraintViolated = false;
-			if (JDD.AreInterecting(modelProduct.getStart(), rmecs)) {
+			if (JDD.AreIntersecting(modelProduct.getStart(), rmecs)) {
 				constraintViolated = true;
 				JDD.Deref(rmecs);
 			} else {

prism/src/prism/NonProbModelChecker.java

@@ -278,7 +278,7 @@ public class NonProbModelChecker extends StateModelChecker
 				JDD.Ref(tmp2);
 				cexDDs.add(JDD.And(tmp2, JDD.Not(tmp)));
 				// See if we have found the initial state yet, and if so, don't store any more info
-				if (JDD.AreInterecting(tmp2, init)) {
+				if (JDD.AreIntersecting(tmp2, init)) {
 					cexDone = true;
 					// Choose an initial state (in case there are several) which intersects
 					JDD.Ref(tmp2);
@@ -420,7 +420,7 @@ public class NonProbModelChecker extends StateModelChecker
 		for (i = 0; i < numSCCs; i++) {
 			JDDNode scc = sccs.get(i);
 			if (scc != null) {
-				if (JDD.AreInterecting(scc, transRel)) {
+				if (JDD.AreIntersecting(scc, transRel)) {
 					JDD.Ref(scc);
 					target = JDD.Or(target, scc);
 				}

prism/src/prism/ProbModelChecker.java

@@ -1546,7 +1546,7 @@ public class ProbModelChecker extends NonProbModelChecker
 		JDDNode trrNonZero = JDD.GreaterThan(trr, 0);
 		JDDNode bsccsNonZero = JDD.Constant(0);
 		for (int b = 0; b < numBSCCs; b++) {
-			if (JDD.AreInterecting(bsccs.get(b), srNonZero) || JDD.AreInterecting(bsccs.get(b), trrNonZero)) {
+			if (JDD.AreIntersecting(bsccs.get(b), srNonZero) || JDD.AreIntersecting(bsccs.get(b), trrNonZero)) {
 				JDD.Ref(bsccs.get(b));
 				bsccsNonZero = JDD.Or(bsccsNonZero, bsccs.get(b));
 			}

prism/src/prism/SCCComputerLockstep.java

@@ -511,7 +511,7 @@ public class SCCComputerLockstep extends SCCComputer
 		//JDD.Ref(scc);
 		JDD.Ref(convergedSet);
 		JDDNode newNodes1 = JDD.And(convergedSet, JDD.Not(scc));
-		if (JDD.AreInterecting(newNodes1, filter)) {
+		if (JDD.AreIntersecting(newNodes1, filter)) {
 			// newEdges1 = edges \intersect (newNodes x newNodes^t)
 			JDD.Ref(edges);
 			JDD.Ref(newNodes1);
@@ -528,7 +528,7 @@ public class SCCComputerLockstep extends SCCComputer
 		//JDD.Ref(nodes);
 		//JDD.Ref(convergedSet);
 		JDDNode newNodes2 = JDD.And(nodes, JDD.Not(convergedSet));
-		if (JDD.AreInterecting(newNodes2, filter)) {
+		if (JDD.AreIntersecting(newNodes2, filter)) {
 			// newEdges2 = edges \intersect (newNodes x newNodes^t)
 			JDD.Ref(edges);
 			JDD.Ref(newNodes2);

prism/src/prism/SCCComputerSCCFind.java

@@ -441,7 +441,7 @@ public class SCCComputerSCCFind extends SCCComputer
 		JDD.Ref(nodes);
 		JDD.Ref(forwardSet);
 		JDDNode newNodes1 = JDD.And(nodes, JDD.Not(forwardSet));
-		if (JDD.AreInterecting(newNodes1, filter)) {
+		if (JDD.AreIntersecting(newNodes1, filter)) {
 			// newEdges1 = edges \intersect (newNodes1 x newNodes1^t)
 			JDD.Ref(edges);
 			JDD.Ref(newNodes1);
@@ -467,7 +467,7 @@ public class SCCComputerSCCFind extends SCCComputer
 		//JDD.Ref(forwardSet);
 		JDD.Ref(scc);
 		JDDNode newNodes2 = JDD.And(forwardSet, JDD.Not(scc));
-		if (JDD.AreInterecting(newNodes2, filter)) {
+		if (JDD.AreIntersecting(newNodes2, filter)) {
 			// newEdges2 = edges \intersect (newNodes2 x newNodes2^t)
 			JDD.Ref(edges);
 			JDD.Ref(newNodes2);