s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

AcceptanceGeneric: add toRabin() and toStreett() methods 

These methods work for the case where the generic acceptance condition
has the required structure or can be easily padded to have the required
structure for Rabin / Streett.


git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11827 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Joachim Klein 9 years ago
parent
30ed75086f
commit
994b6207d9
1 changed files with 366 additions and 0 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 366
      prism/src/acceptance/AcceptanceGeneric.java

366
prism/src/acceptance/AcceptanceGeneric.java
View File

@ -32,7 +32,10 @@ import java.util.ArrayList;
import java.util.BitSet;
import java.util.Collections;
import java.util.List;
import java.util.Stack;
import acceptance.AcceptanceRabin.RabinPair;
import acceptance.AcceptanceStreett.StreettPair;
import prism.PrismException;
import prism.PrismNotSupportedException;
import jdd.JDDVars;
@ -366,6 +369,369 @@ public class AcceptanceGeneric implements AcceptanceOmega {
return this.clone();
}
/**
* Attempt to convert this generic acceptance condition
* to a Rabin condition. If this condition does not have
* the required form (top-level disjunctions with conjunctive pairs),
* returns {@code null}.
* <br>
* If the condition does not syntactically have the required
* from but can be easily converted to one (e.g., by converting
* a single Inf(S) to a Fin(emptyset) & Inf(S) etc) or by swapping
* Inf and Fin, this will be done.
* <br>
* The BitSets for the state sets are cloned, i.e., modifications of
* the state sets of the returned acceptance condition will not affect
* the original generic acceptance condition.
*
* @param numStates the number of states in the underlying model/automaton (for generating state sets for true)
* @return the generated AcceptanceRabin condition, or false on failure
*/
public AcceptanceRabin toAcceptanceRabin(int numStates)
{
AcceptanceRabin result = new AcceptanceRabin();
List<AcceptanceGeneric> disjuncts = extractDisjuncts();
for (AcceptanceGeneric term : disjuncts) {
RabinPair pair = term.toAcceptanceRabinPair(numStates);
if (pair == null) return null;
result.add(pair);
}
return result;
}
/**
* Attempt to convert this generic acceptance to a Rabin pair.
*
* @param numStates the number of states in the underlying model/automaton (for generating state sets for true)
* @return the generated RabinPair, or false on failure
*/
private RabinPair toAcceptanceRabinPair(int numStates)
{
BitSet L = null, K = null;
switch (getKind()) {
case TRUE:
L = new BitSet();
K = new BitSet();
K.set(0, numStates);
break;
case FALSE:
L = new BitSet();
L.set(0, numStates);
K = new BitSet();
break;
case AND: {
AcceptanceGeneric left = getLeft();
AcceptanceGeneric right = getRight();
if (left.getKind() == ElementType.INF || left.getKind() == ElementType.INF_NOT) {
// swap
AcceptanceGeneric tmp = left;
left = right;
right = tmp;
}
switch (left.getKind()) {
case AND:
case OR:
case FALSE:
case TRUE:
case INF:
case INF_NOT:
// not a Rabin condition
return null;
case FIN:
// Fin(A) <=> <>[]!A
// L = A
L = (BitSet) left.getStates().clone();
break;
case FIN_NOT:
// Fin(!A) <=> <>[]A
// L = !A
L = (BitSet) left.getStates().clone();
L.flip(0, numStates);
break;
}
switch (right.getKind()) {
case AND:
case OR:
case FALSE:
case TRUE:
case FIN:
case FIN_NOT:
// not a Rabin condition
return null;
case INF:
// Inf(A) <=> []<>A
// K = A
K = (BitSet) right.getStates().clone();
break;
case INF_NOT:
// Inf(!A) <=> []<>!A
// K = !A
K = (BitSet) right.getStates().clone();
K.flip(0, numStates);
break;
}
break;
}
case FIN:
// Fin(A) <=> <>[]!A & []<> true <=> RabinPair(A, true)
// L = A
L = (BitSet) getStates().clone();
// K = true
K = new BitSet();
K.set(0, numStates);
break;
case FIN_NOT:
// Fin(!A) <=> <>[]A & []<> true <=> RabinPair(!A, true)
// L = !A
L = (BitSet) getStates().clone();
L.flip(0, numStates);
// K = true
K = new BitSet();
K.set(0, numStates);
break;
case INF:
// Inf(A) <=> <>[]!false & []<> A <=> RabinPair(false, A)
// L = false
L = new BitSet();
// K = A
K = (BitSet) getStates().clone();
break;
case INF_NOT:
// Inf(!A) <=> <>[]!false & []<> !A <=> RabinPair(false, !A)
// L = false
L = new BitSet();
// K = !A
K = (BitSet) getStates().clone();
K.flip(0, numStates);
break;
case OR:
// not a Rabin pair
return null;
}
return new AcceptanceRabin.RabinPair(L, K);
}
/**
* Attempt to convert this generic acceptance condition
* to a Streett condition. If this condition does not have
* the required form (top-level conjunction with disjunctive pairs),
* returns {@code null}.
* <br>
* If the condition does not syntactically have the required
* from but can be easily converted to one (e.g., by converting
* a single Inf(S) to a Fin(true) | Inf(S) etc) or by swapping
* Inf and Fin, this will be done.
* <br>
* The BitSets for the state sets are cloned, i.e., modifications of
* the state sets of the returned acceptance condition will not affect
* the original generic acceptance condition.
*
* @param numStates the number of states in the underlying model/automaton (for generating state sets for true)
* @return the generated AcceptanceRabin condition, or false on failure
*/
public AcceptanceStreett toAcceptanceStreett(int numStates)
{
AcceptanceStreett result = new AcceptanceStreett();
List<AcceptanceGeneric> conjuncts = extractConjuncts();
for (AcceptanceGeneric term : conjuncts) {
StreettPair pair = term.toAcceptanceStreettPair(numStates);
if (pair == null) return null;
result.add(pair);
}
return result;
}
/**
* Attempt to convert this generic acceptance to a Streett pair.
*
* @param numStates the number of states in the underlying model/automaton (for generating state sets for true)
* @return the generated RabinPair, or false on failure
*/
private StreettPair toAcceptanceStreettPair(int numStates)
{
BitSet R = null, G = null;
switch (getKind()) {
case TRUE:
// true = []<> false -> []<> false
R = new BitSet();
G = new BitSet();
break;
case FALSE:
// false = []<> true -> []<> false
R = new BitSet();
R.set(0, numStates);
G = new BitSet();
break;
case OR: {
AcceptanceGeneric left = getLeft();
AcceptanceGeneric right = getRight();
if (left.getKind() == ElementType.INF || left.getKind() == ElementType.INF_NOT) {
// swap
AcceptanceGeneric tmp = left;
left = right;
right = tmp;
}
switch (left.getKind()) {
case AND:
case OR:
case FALSE:
case TRUE:
case INF:
case INF_NOT:
// not a Streett condition
return null;
case FIN:
// Fin(A) -> R = A
R = (BitSet) left.getStates().clone();
break;
case FIN_NOT:
// Fin(!A) -> R = !A
R = (BitSet) left.getStates().clone();
R.flip(0, numStates);
break;
}
switch (right.getKind()) {
case AND:
case OR:
case FALSE:
case TRUE:
case FIN:
case FIN_NOT:
// not a Streett condition
return null;
case INF:
// Inf(A) -> G = A
G = (BitSet) right.getStates().clone();
break;
case INF_NOT:
// Inf(!A) -> G = !A
G = (BitSet) right.getStates().clone();
G.flip(0, numStates);
break;
}
break;
}
case FIN:
// Fin(A) <=> []<>A -> []<>false
// R = A
R = (BitSet) getStates().clone();
// G = false
G = new BitSet();
break;
case FIN_NOT:
// Fin(!A) <=> []<>!A -> []<>false
// R = !A
R = (BitSet) getStates().clone();
R.flip(0, numStates);
// G = false
G = new BitSet();
break;
case INF:
// Inf(A) <=> []<>true -> []<>A
// R = true
R = new BitSet();
R.set(0, numStates);
// G = A
G = (BitSet) getStates().clone();
break;
case INF_NOT:
// Inf(!A) <=> []<>true -> []<>!A
// R = true
R = new BitSet();
R.set(0, numStates);
// G = !A
G = (BitSet) getStates().clone();
G.flip(0, numStates);
break;
case AND:
// not a Streett pair
return null;
}
return new AcceptanceStreett.StreettPair(R,G);
}
/**
* Extract the operands of the top-level disjunctions, e.g.,
* for (A & B) | (C | D)) would return the list [A&B,C,D].
*/
public List<AcceptanceGeneric> extractDisjuncts()
{
ArrayList<AcceptanceGeneric> result = new ArrayList<AcceptanceGeneric>();
Stack<AcceptanceGeneric> todo = new Stack<AcceptanceGeneric>();
todo.add(this);
while (!todo.isEmpty()) {
AcceptanceGeneric current = todo.pop();
switch (current.getKind()) {
case AND:
case FALSE:
case TRUE:
case FIN:
case FIN_NOT:
case INF:
case INF_NOT:
// not a top level disjunction, add to list
result.add(current);
break;
case OR:
// still a top level disjunction, recurse
todo.push(current.getRight());
todo.push(current.getLeft());
break;
}
}
return result;
}
/**
* Extract the operands of the top-level conjunctions, e.g.,
* for (A | B) & (C & D)) would return the list [A|B,C,D].
*/
public List<AcceptanceGeneric> extractConjuncts()
{
ArrayList<AcceptanceGeneric> result = new ArrayList<AcceptanceGeneric>();
Stack<AcceptanceGeneric> todo = new Stack<AcceptanceGeneric>();
todo.add(this);
while (!todo.isEmpty()) {
AcceptanceGeneric current = todo.pop();
switch (current.getKind()) {
case OR:
case FALSE:
case TRUE:
case FIN:
case FIN_NOT:
case INF:
case INF_NOT:
// not a top level conjunction, add to list
result.add(current);
break;
case AND:
// still a top level conjunction, recurse
todo.push(current.getRight());
todo.push(current.getLeft());
break;
}
}
return result;
}
@Override
public String toString() {
switch(kind) {

Write Preview
Loading…
Cancel
Save