LTLModelChecker: add support for EC computations against Büchi acceptance

For symbolic, including support for fairness.


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

prism/src/explicit/LTLModelChecker.java

@@ -56,6 +56,7 @@ import prism.PrismException;
 import prism.PrismLangException;
 import prism.PrismNotSupportedException;
 import prism.PrismUtils;
+import acceptance.AcceptanceBuchi;
 import acceptance.AcceptanceGenRabin;
 import acceptance.AcceptanceOmega;
 import acceptance.AcceptanceRabin;
@@ -618,7 +619,9 @@ public class LTLModelChecker extends PrismComponent
 	 */
 	public BitSet findAcceptingECStates(NondetModel model, AcceptanceOmega acceptance) throws PrismException
 	{
-		if (acceptance instanceof AcceptanceRabin) {
+		if (acceptance instanceof AcceptanceBuchi) {
+			return findAcceptingECStatesForBuchi(model, (AcceptanceBuchi) acceptance);
+		} else if (acceptance instanceof AcceptanceRabin) {
 			return findAcceptingECStatesForRabin(model, (AcceptanceRabin) acceptance);
 		} else if (acceptance instanceof AcceptanceStreett) {
 			return findAcceptingECStatesForStreett(model, (AcceptanceStreett) acceptance);
@@ -628,6 +631,33 @@ public class LTLModelChecker extends PrismComponent
 		throw new PrismNotSupportedException("Computing end components for acceptance type '"+acceptance.getType()+"' currently not supported (explicit engine).");
 	}
 
+	/**
+	 * Find the set of states in accepting end components (ECs) in a nondeterministic model wrt a Büchi acceptance condition.
+	 * @param model The model
+	 * @param acceptance The acceptance condition
+	 */
+	public BitSet findAcceptingECStatesForBuchi(NondetModel model, AcceptanceBuchi acceptance) throws PrismException
+	{
+		BitSet allAcceptingStates = new BitSet();
+
+		if (acceptance.getAcceptingStates().isEmpty()) {
+			return allAcceptingStates;
+		}
+
+		// Compute accepting maximum end components (MECs)
+		ECComputer ecComputer = ECComputer.createECComputer(this, model);
+		ecComputer.computeMECStates();
+		List<BitSet> mecs = ecComputer.getMECStates();
+		// Union of accepting MEC states
+		for (BitSet mec : mecs) {
+			if (mec.intersects(acceptance.getAcceptingStates())) {
+				allAcceptingStates.or(mec);
+			}
+		}
+
+		return allAcceptingStates;
+	}
+
 	/**
 	 * Find the set of states in accepting end components (ECs) in a nondeterministic model wrt a Rabin acceptance condition.
 	 * @param model The model

prism/src/prism/LTLModelChecker.java

@@ -33,6 +33,7 @@ import java.util.BitSet;
 import java.util.List;
 import java.util.Vector;
 
+import acceptance.AcceptanceBuchiDD;
 import acceptance.AcceptanceGenRabinDD;
 import acceptance.AcceptanceOmega;
 import acceptance.AcceptanceOmegaDD;
@@ -735,6 +736,8 @@ public class LTLModelChecker extends PrismComponent
 			throws PrismException
 	{
 		switch (acceptance.getType()) {
+		case BUCHI:
+			return findAcceptingECStatesForBuchi((AcceptanceBuchiDD) acceptance, model, fairness);
 		case RABIN:
 			return findAcceptingECStatesForRabin((AcceptanceRabinDD) acceptance, model, daDDRowVars, daDDColVars, fairness);
 		case GENERALIZED_RABIN:
@@ -744,6 +747,35 @@ public class LTLModelChecker extends PrismComponent
 		}
 	}
 
+	/**
+	 * Find the set of states in accepting end components (ECs) in a nondeterministic model wrt a Büchi acceptance condition.
+	 * @param acceptance the Büchi acceptance condition
+	 * @param model The model
+	 * @param fairness Consider fairness?
+	 * @return A referenced BDD for the union of all states in accepting MECs
+	 */
+	public JDDNode findAcceptingECStatesForBuchi(AcceptanceBuchiDD acceptance, NondetModel model, boolean fairness) throws PrismException
+	{
+		JDDNode acceptingStates = null;
+
+		// Normal case (no fairness): find accepting MECs
+		if (!fairness) {
+			List<JDDNode> ecs = findMECStates(model, model.getReach().copy());
+			acceptingStates = filteredUnion(ecs, acceptance.getAcceptingStates());
+		}
+		// For case of fairness...
+		else {
+			// Compute the backward set of F, i.e., all states that can reach F
+			JDDNode edges = model.getTransReln().copy();
+			JDDNode filterStates = backwardSet(model, acceptance.getAcceptingStates(), edges);
+			// Find the accepting states under fairness: the fair ECs that
+			// can stay in filterStates, as those can infinitely often visit F
+			acceptingStates = findFairECs(model, filterStates);
+		}
+
+		return acceptingStates;
+	}
+
 	/**
 	 * Find the set of states in accepting end components (ECs) in a nondeterministic model wrt a Rabin acceptance condition.
 	 * @param acceptance the Rabin acceptance condition