diff --git a/prism/src/acceptance/AcceptanceGenRabinDD.java b/prism/src/acceptance/AcceptanceGenRabinDD.java
index dd7ba084..7c8e51d5 100644
--- a/prism/src/acceptance/AcceptanceGenRabinDD.java
+++ b/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;
diff --git a/prism/src/acceptance/AcceptanceGenericDD.java b/prism/src/acceptance/AcceptanceGenericDD.java
index 3c7e7c67..89797ddd 100644
--- a/prism/src/acceptance/AcceptanceGenericDD.java
+++ b/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");
}
diff --git a/prism/src/acceptance/AcceptanceRabinDD.java b/prism/src/acceptance/AcceptanceRabinDD.java
index 035b6a9b..13cc387e 100644
--- a/prism/src/acceptance/AcceptanceRabinDD.java
+++ b/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;
diff --git a/prism/src/acceptance/AcceptanceReachDD.java b/prism/src/acceptance/AcceptanceReachDD.java
index 134525ec..9463fb22 100644
--- a/prism/src/acceptance/AcceptanceReachDD.java
+++ b/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
diff --git a/prism/src/acceptance/AcceptanceStreettDD.java b/prism/src/acceptance/AcceptanceStreettDD.java
index a643f022..acce146f 100644
--- a/prism/src/acceptance/AcceptanceStreettDD.java
+++ b/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
diff --git a/prism/src/jdd/JDD.java b/prism/src/jdd/JDD.java
index e2284547..def08360 100644
--- a/prism/src/jdd/JDD.java
+++ b/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: none, DEREFS: none ]
*/
- public static boolean AreInterecting(JDDNode dd1, JDDNode dd2)
+ public static boolean AreIntersecting(JDDNode dd1, JDDNode dd2)
{
JDDNode tmp;
boolean res;
diff --git a/prism/src/prism/LTLModelChecker.java b/prism/src/prism/LTLModelChecker.java
index 3dab3277..4d61af1b 100644
--- a/prism/src/prism/LTLModelChecker.java
+++ b/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);
diff --git a/prism/src/prism/MultiObjModelChecker.java b/prism/src/prism/MultiObjModelChecker.java
index 6c0e27f4..60e12fd4 100644
--- a/prism/src/prism/MultiObjModelChecker.java
+++ b/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 {
diff --git a/prism/src/prism/NonProbModelChecker.java b/prism/src/prism/NonProbModelChecker.java
index 58099450..1fc936c2 100644
--- a/prism/src/prism/NonProbModelChecker.java
+++ b/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);
}
diff --git a/prism/src/prism/ProbModelChecker.java b/prism/src/prism/ProbModelChecker.java
index 241c3d64..59691de4 100644
--- a/prism/src/prism/ProbModelChecker.java
+++ b/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));
}
diff --git a/prism/src/prism/SCCComputerLockstep.java b/prism/src/prism/SCCComputerLockstep.java
index af63794c..20aa3708 100644
--- a/prism/src/prism/SCCComputerLockstep.java
+++ 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);
diff --git a/prism/src/prism/SCCComputerSCCFind.java b/prism/src/prism/SCCComputerSCCFind.java
index 24c19e68..3fab6cde 100644
--- a/prism/src/prism/SCCComputerSCCFind.java
+++ b/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);