Class RabinPairs
Acceptance pairs for Rabin automaton.
Each pair defines an acceptance condition. A pair (L, U) comprises
of:
-
a set L of "good" states
-
a set U of "bad" states
L,U must each be a subset of States.
A run: (q0, q1, ...) is accepted if for at least one Rabin Pair, it in
intersects L an inf number of times, but U only finitely.
Internally a list of 2-tuples of SubSet objects is maintained:
[(L1, U1), (L2, U2), ...]
where: Li, Ui, are SubSet objects, with superset the Rabin automaton's
States.
Caution
Here and in ltl2dstar documentation L denotes a "good"
set. [BK08] denote the a "bad" set with L. To
avoid ambiguity, attributes: .good, .bad were used here.
Example
>>> dra = RabinAutomaton()
>>> dra.states.add_from([1, 2, 3] )
>>> dra.states.accepting.add([1], [2] )
>>> dra.states.accepting
>>> dra.states.accepting.good(1)
>>> dra.states.accepting.bad(1)
See Also
|
|
__init__(self,
automaton_states)
x.__init__(...) initializes x; see help(type(x)) for signature |
|
|
|
|
|
|
|
|
|
|
|
|
|
__call__(self)
Get list of 2-tuples (L, U) of good-bad sets of states. |
|
|
|
|
add(self,
good_states,
bad_states)
Add new acceptance pair (L, U). |
|
|
|
|
remove(self,
good_states,
bad_states)
Delete pair (L, U) of good-bad sets of states. |
|
|
|
|
| add_states(self,
pair_index,
good_states,
bad_states) |
|
|
|
|
good(self,
index)
Return set L of "good" states for this pair. |
|
|
|
|
bad(self,
index)
Return set U of "bad" states for this pair. |
|
|
|
|
has_superset(self,
superset)
Return true if the given argument is the superset. |
|
|
|
Inherited from object:
__delattr__,
__format__,
__getattribute__,
__hash__,
__new__,
__reduce__,
__reduce_ex__,
__repr__,
__setattr__,
__sizeof__,
__subclasshook__
|
|
Inherited from object:
__class__
|
__init__(self,
automaton_states)
(Constructor)
|
|
x.__init__(...) initializes x; see help(type(x)) for signature
- Overrides:
object.__init__
- (inherited documentation)
|
__str__(self)
(Informal representation operator)
|
|
str(x)
- Overrides:
object.__str__
- (inherited documentation)
|
add(self,
good_states,
bad_states)
|
|
Add new acceptance pair (L, U).
See Also
remove, add_states, good, bad
- Parameters:
good_states (container of valid states) - set L of good states for this pairbad_states (container of valid states) - set U of bad states for this pair
|
remove(self,
good_states,
bad_states)
|
|
Delete pair (L, U) of good-bad sets of states.
Note
Removing a pair which is not last changes the indices of all other
pairs, because internally a list is used.
The sets L,U themselves (good-bad) are required for the deletion,
instead of an index, to prevent acceidental deletion of an unintended
pair.
Get the intended pair using __getitem__ first (or in any other way)
and them call remove. If the pair is corrent, then the removal will be
successful.
See Also
add
- Parameters:
good_states (iterable container) - set of good states of this pair
|
|
Return set L of "good" states for this pair.
- Parameters:
index (int <= current total number of pairs) - number of Rabin acceptance pair
|
|
Return set U of "bad" states for this pair.
- Parameters:
index (int <= current total number of pairs) - number of Rabin acceptance pair
|