spot.mark_t()

spot.mark_t([0, 2, 3])

spot.mark_t((0, 2, 3))

"""
Explanation: Acceptance conditions
The acceptance condition of an automaton specifies which of its paths are accepting.
The way acceptance conditions are stored in Spot is derived from the way acceptance conditions are specified in the HOA format.  In HOA, acceptance conditions are given as a line of the form:
Acceptance: 3 (Inf(0)&amp;Fin(1))|Inf(2)

The number 3 gives the number of acceptance sets used (numbered from 0 to 2 in that case), while the rest of the line is a positive Boolean formula over terms of the form:
- Inf(n), that is true if and only if the set n is seen infinitely often,
- Fin(n), that is true if and only if the set n should be seen finitely often,
- t, always true,
- f, always false.
The HOA specifications additionally allows terms of the form Inf(!n) or Fin(!n) but Spot automatically rewrites those away when reading an HOA file.
Note that the number of sets given can be larger than what is actually needed by the acceptance formula.
Transitions in automata can be tagged as being part of some member sets, and a path in the automaton is accepting if the set of acceptance sets visited along this path satify the acceptance condition.
Definining acceptance conditions in Spot involves three different types of C++ objects:

spot::acc_cond is used to represent an acceptance condition, that is: a number of sets and a formula.
spot::acc_cond::acc_code, is used to represent Boolean formula for the acceptance condition using a kind of byte code (hence the name)
spot::acc_cond::mark_t, is a type of bit-vector used to represent membership to acceptance sets.

In because Swig's support for nested class is limited, these types are available respectively as spot.acc_cond, spot.acc_code, and spot.mark_t in Python.
mark_t
Let's start with the simpler of these three objects. mark_t is a type of bit vector.  Its main constructor takes a sequence of set numbers.
End of explanation
"""


x = spot.mark_t([0, 2, 3])
y = spot.mark_t([0, 4])
print(x | y)
print(x & y)
print(x - y)

"""
Explanation: As seen above, the sequence of set numbers can be specified using a list or a tuple.  While from the Python language point of view, using a tuple is faster than using a list, the overhead to converting all the arguments from Python to C++ and then converting the resuslting back from C++ to Python makes this difference completely negligeable.  In the following, we opted to use lists, because brackets are more readable than nested parentheses.
End of explanation
"""


x.set(5)
print(x)

x.clear(3)
print(x)

print(x.has(2))
print(x.has(3))

"""
Explanation: The bits can be set, cleared, and tested using the set(), clear(), and has() methods:
End of explanation
"""


x << 2

"""
Explanation: Left-shifting will increment all set numbers.
This operation is useful when building the product of two automata: all the set number of one automaton have to be shift by the number of sets used in the other automaton.
End of explanation
"""


print(x)
print(x.id)
print(bin(x.id))

"""
Explanation: Internally, the mark_t stores the bit-vector as an integer.  This also implies that we currently do not support more than 32 acceptance sets.  The underlaying integer can be retrieved using .id.
End of explanation
"""


# compare
print(spot.mark_t([5]))
# with
print(spot.mark_t(5))
print(spot.mark_t(0b10101))

"""
Explanation: mark_t can also be initialized using an integer: in that case the integer is interpreted as a bit vector.
A frequent error is to use mark_t(n) when we really mean mark_t([n]) or mark_t((n,)).
End of explanation
"""


print(x)
print(list(x.sets()))
for s in x.sets():
    print(s)

"""
Explanation: The different sets can be iterated over with the sets() method, that returns a tuble with the index of all bits set.
End of explanation
"""


x.count()

"""
Explanation: count() return the number of sets in a mark_t:
End of explanation
"""


spot.mark_t([1,3,5]).lowest()

v = spot.mark_t([1, 3, 5])
while v:               # this stops once v is empty
    b = v.lowest()
    v -= b
    print(b)

"""
Explanation: lowest() returns a mark_t containing only the lowest set number.  This provides another way to iterate overs all set numbers in cases where you need the result as a mark_t.
End of explanation
"""


spot.mark_t([1, 3, 5]).max_set()

"""
Explanation: max_set() returns the number of the highest set plus one.  This is usually used to figure out how many sets we need to declare on the Acceptance: line of the HOA format:
End of explanation
"""


spot.acc_code('(Inf(0)&Fin(1))|Inf(2)')

"""
Explanation: acc_code
acc_code encodes the formula of the acceptance condition using a kind of bytecode that basically corresponds to an encoding in reverse Polish notation in which conjunctions of Inf(n) terms, and disjunctions of Fin(n) terms are grouped.  In particular, the frequently-used genaralized-Büchi acceptance conditions (like Inf(0)&amp;Inf(1)&amp;Inf(2)) are always encoded as a single term (like Inf({0,1,2})).
The simplest way to construct an acc_code by passing a string that represent the formula to build.
End of explanation
"""


spot.acc_code('Rabin 2')

"""
Explanation: You may also use a named acceptance condition:
End of explanation
"""


print(spot.acc_code('Streett 2..4'))
print(spot.acc_code('Streett 2..4'))

"""
Explanation: The recognized names are the valide values for acc-name: in the HOA format.  Additionally numbers may be replaced by ranges of the form n..m, in which case a random number is selected in that range.
End of explanation
"""


spot.acc_code('random 3..5')

"""
Explanation: It may also be convenient to generate a random acceptance condition:
End of explanation
"""


a = spot.acc_code('parity min odd 5')
a

a.to_cnf()

a.to_dnf()

"""
Explanation: The to_cnf() and to_dnf() functions can be used to rewrite the formula into Conjunctive or Disjunctive normal forms.  This functions will simplify the resulting formulas to make them irredundant.
End of explanation
"""


x = spot.acc_code('Rabin 2')
y = spot.acc_code('Rabin 2') << 4
print(x)
print(y)

print(x | y)
print(x & y)

"""
Explanation: The manipulation of acc_code objects is quite rudimentary at the moment: it easy to build, but it's harder take appart.  In fact we won't attempt to disassemble an acc_code object in Python: those things are better done in C++
Operators |, |=, &amp;, &amp;=, &lt;&lt;, and &lt;&lt;= can be used with their obvious semantics.
Whenever possible, the inplace versions (|=, &amp;=, &lt;&lt;=) should be prefered, because they create less temporary acceptance conditions.
End of explanation
"""


print(x)
print(x.complement())

"""
Explanation: The complement() method returns the complemented acceptance condition:
End of explanation
"""


spot.acc_code.inf([1,2]) & spot.acc_code.fin([3,4,5])

spot.acc_code.inf([])

spot.acc_code.t()

spot.acc_code.fin([])

spot.acc_code.f()

"""
Explanation: Instead of using acc_code('string'), it is also possible to build an acceptance formula from atoms like Inf({...}), Fin({...}), t, or f.
Remember that in our encoding for the formula, terms like Inf(1)&amp;Inf(2) and Fin(3)|Fin(4)|Fin(5) are actually stored as Inf({1,2}) and Fin({3,4,5}), where {1,2} and {3,4,5} are instance of mark_t.  These terms can be generated with the
functions spot.acc_code.inf(mark) and spot.acc_code.fin(mark).
Inf({}) is equivalent to t, and Fin({}) is equivalent to f, but it's better to use the functions spot.acc_code.t() or spot.acc_code.f() directly.
End of explanation
"""


acc = spot.acc_code('Fin(0) & Inf(1) | Inf(2)')
print("acc =", acc)
for x in ([0, 1, 2], [1, 2], [0, 1], [0, 2], [0], [1], [2], []):
    print("acc.accepting({}) = {}".format(x, acc.accepting(x)))

"""
Explanation: To evaluate an acceptance condition formula on a run, build a mark_t containing all the acceptance sets that are seen infinitely often along this run, and call the accepting() method.
End of explanation
"""


acc = spot.acc_code('Fin(0) & Inf(2)')
print(acc)
print(acc.used_sets())
print(acc.used_sets().max_set())

"""
Explanation: Finally the method used_sets() returns a mark_t with all the sets appearing in the formula:
End of explanation
"""


acc = spot.acc_cond(4, spot.acc_code('Rabin 2'))
acc

"""
Explanation: acc_cond
Automata store their acceptance condition as an instance of the acc_cond class.
This class can be thought of as a pair (n, code), where n is an integer that tells how many acceptance sets are used, while the code is an instance of acc_code and encodes the formula over a subset of these acceptance sets.  We usually have n == code.used_sets().max_set()), but n can be larger.
It is OK if an automaton declares that is used 3 sets, even if the acceptance condition formula only uses set number 1.
The acc_cond objects are usually not created by hand: automata have dedicated methods for that.  But for the purpose of this notebook, let's do it:
End of explanation
"""


acc = spot.acc_cond(4, 'Rabin 2')
acc

acc.num_sets()

acc.get_acceptance()

"""
Explanation: For convenience, you can pass the string directly:
End of explanation
"""


acc = spot.acc_cond(4)
acc

acc.add_sets(2)
acc

acc.set_acceptance('Streett 2')
acc

"""
Explanation: The acc_cond object can also be constructed using only a number of sets.  In that case, the acceptance condition defaults to t, and it can be changed to something else later (using set_acceptance()).  The number of acceptance sets can also be augmented with add_sets().
End of explanation
"""


acc = spot.acc_cond('Streett 2')
acc

"""
Explanation: Calling the constructor of acc_cond by passing just an instance of acc_code (or a string that will be passed to the acc_code constructor) will automatically set the number of acceptance sets to the minimum needed by the formula:
End of explanation
"""


code = spot.acc_code('Streett 2')
acc = spot.acc_cond(code.used_sets().max_set(), code)
acc

"""
Explanation: The above is in fact just syntactic sugar for:
End of explanation
"""


acc = spot.acc_cond(4)
acc.set_generalized_buchi()
acc

"""
Explanation: The common scenario of setting generalized Büchi acceptance can be achieved more efficiently by first setting the number of acceptance sets, and then requiring generalized Büchi acceptance:
End of explanation
"""


print(acc)
print(acc.is_generalized_buchi())
acc.add_sets(1)
print(acc)
print(acc.is_generalized_buchi())

"""
Explanation: The acc_cond class has several methods for detecting acceptance conditions that match the named acceptance conditions of the HOA format.  Note that in the HOA format, Inf(0)&amp;Inf(1)&amp;Inf(2)&amp;Inf(3) is only called generalized Büchi if exactly 4 acceptance sets are used.  So the following behavior should not be surprising:
End of explanation
"""


acc = spot.acc_cond('Rabin 2')
print(acc)
print(acc.is_rabin())
print(acc.is_streett())

"""
Explanation: Similar methods like is_t(), is_f(), is_buchi(), is_co_buchi(), is_generalized_co_buchi() all return a Boolean.
The is_rabin() and is_streett() methods, however, return a number of pairs.  The number of pairs is always num_sets()/2 on success, or -1 on failure.
End of explanation
"""


acc = spot.acc_cond('parity min odd 4')
print(acc)
print(acc.is_parity())
acc.set_generalized_buchi()
print(acc)
print(acc.is_parity())

"""
Explanation: The check for parity acceptance returns three Boolean in a list of the form [matched, max?, odd?].  If matched is False, the other values should be ignored.
End of explanation
"""


print(acc.name())
print(acc.name("d"))  # <- Style used by print_dot(aut, "a")
print(acc.name("0"))  # <- no parameters

"""
Explanation: If the acceptance condition has some known name, it can be retrieved using the name() method.  By default the name given is a human-readable string close that used in the HOA format, but with proper accents, and support for name like Streett-like or Rabin-like.  The argument arg can specify a different style using the same syntax as in --format='%[arg]g' when using the command-line tools.
End of explanation
"""


m = spot.mark_t([1, 3])
print(acc.comp(m))

"""
Explanation: acc_cond contains a few functions for manipulating mark_t instances, these are typically functions that require known the total number of accepting sets declared.
For instance complementing a mark_t:
End of explanation
"""


acc.all_sets()

"""
Explanation: all_sets() returns a mark_t listing all the declared sets:
End of explanation
"""


print("acc =", acc)
for x in ([0, 1, 2, 3, 10], [1, 2]):
    print("acc.accepting({}) = {}".format(x, acc.accepting(x)))

"""
Explanation: For convencience, the accepting() method of acc_cond delegates to that of the acc_code.
Any set passed to accepting() that is not used by the acceptance formula has no influence.
End of explanation
"""


print(acc)
print(acc.unsat_mark())

acc = spot.acc_cond(0)   # use 0 acceptance sets, and the default formula (t)
print(acc)
print(acc.unsat_mark())

acc = spot.acc_cond('Streett 2')
print(acc)
print(acc.unsat_mark())

"""
Explanation: Finally the unsat_mark() method of acc_cond computes an instance of mark_t that is unaccepting (i.e., passing this value to acc.accepting(...) will return False when such a value exist.  Not all acceptance conditions have an satisfiable mark.  Obviously the t acceptance is always satisfiable, and so are all equivalent acceptances (for instance Fin(1)|Inf(1)).
For this reason, unsat_mark() actually returns a pair: (bool, mark_t) where the Boolean is False iff the acceptance is always satisfiable.  When the Boolean is True, then the second element of the pair gives a non-accepting mark.
End of explanation
"""


