Commit d4967f20 authored by Florian Renkin's avatar Florian Renkin
Browse files

Notebooks: correct typos

* tests/python/acc_cond.ipynb, tests/python/contains.ipynb,
tests/python/decompose.ipynb, tests/python/games.ipynb,
tests/python/randltl.ipynb, tests/python/synthesis.ipynb,
tests/python/testingaut.ipynb: here.
parent c72c2855
Pipeline #31023 passed with stages
in 160 minutes and 44 seconds
%% Cell type:code id: tags:
``` python
import spot
spot.setup()
```
%% Cell type:markdown id: tags:
# 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](http://adl.github.io/hoaf/). In HOA, acceptance conditions are given as a line of the form:
Acceptance: 3 (Inf(0)&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.
%% Cell type:code id: tags:
``` python
print(spot.mark_t())
```
%% Output
{}
%% Cell type:code id: tags:
``` python
print(spot.mark_t([0, 2, 3])) # works with lists
```
%% Output
{0,2,3}
%% Cell type:code id: tags:
``` python
print(spot.mark_t((0, 2, 3))) # works with tuples
```
%% Output
{0,2,3}
%% Cell type:markdown id: tags:
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.
%% Cell type:code id: tags:
``` python
x = spot.mark_t([0, 2, 3])
y = spot.mark_t([0, 4])
print(x | y)
print(x & y)
print(x - y)
```
%% Output
{0,2,3,4}
{0}
{2,3}
%% Cell type:markdown id: tags:
The bits can be set, cleared, and tested using the `set()`, `clear()`, and `has()` methods:
%% Cell type:code id: tags:
``` python
x.set(5)
print(x)
```
%% Output
{0,2,3,5}
%% Cell type:code id: tags:
``` python
x.clear(3)
print(x)
```
%% Output
{0,2,5}
%% Cell type:code id: tags:
``` python
print(x.has(2))
print(x.has(3))
```
%% Output
True
False
%% Cell type:markdown id: tags:
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.
%% Cell type:code id: tags:
``` python
print(x << 2)
```
%% Output
{2,4,7}
%% Cell type:markdown id: tags:
The different sets can be iterated over with the `sets()` method, that returns a tuple with the index of all bits set.
%% Cell type:code id: tags:
``` python
print(x)
print(list(x.sets()))
for s in x.sets():
print(s)
```
%% Output
{0,2,5}
[0, 2, 5]
0
2
5
%% Cell type:markdown id: tags:
`count()` return the number of sets in a `mark_t`:
%% Cell type:code id: tags:
``` python
x.count()
```
%% Output
3
%% Cell type:markdown id: tags:
`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`.
%% Cell type:code id: tags:
``` python
spot.mark_t([1,3,5]).lowest()
```
%% Output
spot.mark_t([1])
%% Cell type:code id: tags:
``` python
v = spot.mark_t([1, 3, 5])
while v: # this stops once v is empty
b = v.lowest()
v -= b
print(b)
```
%% Output
{1}
{3}
{5}
%% Cell type:markdown id: tags:
`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:
%% Cell type:code id: tags:
``` python
spot.mark_t([1, 3, 5]).max_set()
```
%% Output
6
%% Cell type:markdown id: tags:
## `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](http://en.wikipedia.org/wiki/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)&Inf(1)&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.
%% Cell type:code id: tags:
``` python
acc = spot.acc_code('(Inf(0)&Fin(1))|Inf(2)')
print(acc) # shows just the formula
acc # shows the acc_code object
```
%% Output
(Inf(0) & Fin(1)) | Inf(2)
spot.acc_code("(Inf(0) & Fin(1)) | Inf(2)")
%% Cell type:markdown id: tags:
You may also use a named acceptance condition:
%% Cell type:code id: tags:
``` python
spot.acc_code('Rabin 2')
```
%% Output
spot.acc_code("(Fin(0) & Inf(1)) | (Fin(2) & Inf(3))")
%% Cell type:markdown id: tags:
The recognized names are the valid values for `acc-name:` in the [HOA format](http://adl.github.io/hoaf/). Additionally, numbers may be replaced by ranges of the form `n..m`, in which case a random number is selected in that range.
%% Cell type:code id: tags:
``` python
print(spot.acc_code('Streett 2..4'))
print(spot.acc_code('Streett 2..4'))
```
%% Output
(Fin(0) | Inf(1)) & (Fin(2) | Inf(3)) & (Fin(4) | Inf(5)) & (Fin(6) | Inf(7))
(Fin(0) | Inf(1)) & (Fin(2) | Inf(3))
%% Cell type:markdown id: tags:
It may also be convenient to generate a random acceptance condition. Below we require between 3 and 5 acceptance sets:
%% Cell type:code id: tags:
``` python
spot.acc_code('random 3..5')
```
%% Output
spot.acc_code("(Fin(3) | Inf(1)) & Inf(4) & (Fin(0)|Fin(2))")
%% Cell type:markdown id: tags:
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.
%% Cell type:code id: tags:
``` python
a = spot.acc_code('parity min odd 5')
a
```
%% Output
spot.acc_code("Fin(0) & (Inf(1) | (Fin(2) & (Inf(3) | Fin(4))))")
%% Cell type:code id: tags:
``` python
a.to_cnf()
```
%% Output
spot.acc_code("Fin(0) & (Inf(1) | Fin(2)) & (Inf(1) | Inf(3) | Fin(4))")
%% Cell type:code id: tags:
``` python
a.to_dnf()
```
%% Output
spot.acc_code("(Fin(0) & Inf(1)) | (Fin(0) & Fin(2) & Inf(3)) | (Fin(0) & Fin(2) & Fin(4))")
%% Cell type:markdown id: tags:
The manipulation of `acc_code` objects is quite rudimentary at the moment: they are easy to build, but are harder take appart. In fact we won't attempt to disassemble an `acc_code` object in Python: those things are better done in C++
The manipulation of `acc_code` objects is quite rudimentary at the moment: they are easy to build, but are 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 `|`, `|=`, `&`, `&=`, `<<`, and `<<=` can be used with their obvious semantics.
Whenever possible, the inplace versions (`|=`, `&=`, `<<=`) should be prefered, because they create less temporary acceptance conditions.
%% Cell type:code id: tags:
``` python
x = spot.acc_code('Rabin 2')
y = spot.acc_code('Rabin 2') << 4
print(x)
print(y)
```
%% Output
(Fin(0) & Inf(1)) | (Fin(2) & Inf(3))
(Fin(4) & Inf(5)) | (Fin(6) & Inf(7))
%% Cell type:code id: tags:
``` python
print(x | y)
print(x & y)
```
%% Output
(Fin(4) & Inf(5)) | (Fin(6) & Inf(7)) | (Fin(0) & Inf(1)) | (Fin(2) & Inf(3))
((Fin(4) & Inf(5)) | (Fin(6) & Inf(7))) & ((Fin(0) & Inf(1)) | (Fin(2) & Inf(3)))
%% Cell type:markdown id: tags:
The `complement()` method returns the complemented acceptance condition:
%% Cell type:code id: tags:
``` python
print(x)
print(x.complement())
```
%% Output
(Fin(0) & Inf(1)) | (Fin(2) & Inf(3))
(Inf(0) | Fin(1)) & (Inf(2) | Fin(3))
%% Cell type:markdown id: tags:
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)&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.
%% Cell type:code id: tags:
``` python
spot.acc_code.inf([1,2]) & spot.acc_code.fin([3,4,5])
```
%% Output
spot.acc_code("(Fin(3)|Fin(4)|Fin(5)) & (Inf(1)&Inf(2))")
%% Cell type:code id: tags:
``` python
spot.acc_code.inf([])
```
%% Output
spot.acc_code("t")
%% Cell type:code id: tags:
``` python
spot.acc_code.t()
```
%% Output
spot.acc_code("t")
%% Cell type:code id: tags:
``` python
spot.acc_code.fin([])
```
%% Output
spot.acc_code("f")
%% Cell type:code id: tags:
``` python
spot.acc_code.f()
```
%% Output
spot.acc_code("f")
%% Cell type:markdown id: tags:
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.
%% Cell type:code id: tags:
``` python
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)))
```
%% Output
acc = (Fin(0) & Inf(1)) | Inf(2)
acc.accepting([0, 1, 2]) = True
acc.accepting([1, 2]) = True
acc.accepting([0, 1]) = False
acc.accepting([0, 2]) = True
acc.accepting([0]) = False
acc.accepting([1]) = True
acc.accepting([2]) = True
acc.accepting([]) = False
%% Cell type:markdown id: tags:
Finally the method `used_sets()` returns a `mark_t` with all the sets appearing in the formula:
%% Cell type:code id: tags:
``` python
acc = spot.acc_code('Fin(0) & Inf(2)')
print(acc)
print(acc.used_sets())
print(acc.used_sets().max_set())
```
%% Output
Fin(0) & Inf(2)
{0,2}
3
%% Cell type:markdown id: tags:
The `used_inf_fin_sets()` returns a pair of marks instead, the first one with all sets occuring in `Inf`, and the second one with all sets appearing in `Fin`.
%% Cell type:code id: tags:
``` python
acc.used_inf_fin_sets()
```
%% Output
(spot.mark_t([2]), spot.mark_t([0]))
%% Cell type:markdown id: tags:
If the top-level operators is a conjunct or disjunct, the following methods returns lists of clauses.
%% Cell type:code id: tags:
``` python
c = spot.acc_code('Fin(0)|(Inf(1)&Fin(2))|Fin(3)')
print(repr(c))
print(c.top_disjuncts())
c = spot.acc_code('Inf(0)&Inf(1)&(Fin(2)|Fin(3))')
print(repr(c))
print(c.top_conjuncts())
# Nothing to split here as the top operator is not a disjunction
print(c.top_disjuncts())
```
%% Output
spot.acc_code("(Fin(0)|Fin(3)) | (Inf(1) & Fin(2))")
(spot.acc_code("Fin(0)"), spot.acc_code("Fin(3)"), spot.acc_code("Inf(1) & Fin(2)"))
spot.acc_code("(Inf(0)&Inf(1)) & (Fin(2)|Fin(3))")
(spot.acc_code("Inf(0)"), spot.acc_code("Inf(1)"), spot.acc_code("Fin(2)|Fin(3)"))
(spot.acc_code("(Inf(0)&Inf(1)) & (Fin(2)|Fin(3))"),)
%% Cell type:markdown id: tags:
# `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 uses 3 sets, even if the acceptance condition formula only uses set number 1. The extra two sets will have no impact on the language, even if they are used in the automaton.
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:
%% Cell type:code id: tags:
``` python
acc = spot.acc_cond(4, spot.acc_code('Rabin 2'))
acc
```
%% Output
spot.acc_cond(4, "(Fin(0) & Inf(1)) | (Fin(2) & Inf(3))")
%% Cell type:markdown id: tags:
For convenience, you can pass the string directly:
%% Cell type:code id: tags:
``` python
acc = spot.acc_cond(4, 'Rabin 2')
acc
```
%% Output
spot.acc_cond(4, "(Fin(0) & Inf(1)) | (Fin(2) & Inf(3))")
%% Cell type:code id: tags:
``` python
acc.num_sets()
```
%% Output
4
%% Cell type:code id: tags:
``` python
acc.get_acceptance()
```
%% Output
spot.acc_code("(Fin(0) & Inf(1)) | (Fin(2) & Inf(3))")
%% Cell type:markdown id: tags:
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()`.
%% Cell type:code id: tags:
``` python
acc = spot.acc_cond(4)
acc
```
%% Output
spot.acc_cond(4, "t")
%% Cell type:code id: tags:
``` python
acc.add_sets(2)
acc
```
%% Output
spot.acc_cond(6, "t")
%% Cell type:code id: tags:
``` python
acc.set_acceptance('Streett 2')
acc
```
%% Output
spot.acc_cond(6, "(Fin(0) | Inf(1)) & (Fin(2) | Inf(3))")
%% Cell type:markdown id: tags:
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:
%% Cell type:code id: tags:
``` python
acc = spot.acc_cond('Streett 2')
acc
```
%% Output
spot.acc_cond(4, "(Fin(0) | Inf(1)) & (Fin(2) | Inf(3))")
%% Cell type:markdown id: tags:
The above is in fact just syntactic sugar for:
%% Cell type:code id: tags:
``` python
code = spot.acc_code('Streett 2')
acc = spot.acc_cond(code.used_sets().max_set(), code)
acc
```
%% Output
spot.acc_cond(4, "(Fin(0) | Inf(1)) & (Fin(2) | Inf(3))")
%% Cell type:markdown id: tags:
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:
%% Cell type:code id: tags:
``` python
acc = spot.acc_cond(4)
acc.set_generalized_buchi()
acc
```
%% Output
spot.acc_cond(4, "Inf(0)&Inf(1)&Inf(2)&Inf(3)")
%% Cell type:markdown id: tags:
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)&Inf(1)&Inf(2)&Inf(3)` is only called generalized Büchi if exactly 4 acceptance sets are used. So the following behavior should not be surprising:
%% Cell type:code id: tags:
``` python
print(acc)
print(acc.is_generalized_buchi())
acc.add_sets(1)
print(acc)
print(acc.is_generalized_buchi())
```
%% Output
(4, Inf(0)&Inf(1)&Inf(2)&Inf(3))
True
(5, Inf(0)&Inf(1)&Inf(2)&Inf(3))
False
%% Cell type:markdown id: tags:
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.
%% Cell type:code id: tags:
``` python
acc = spot.acc_cond('Rabin 2')
print(acc)
print(acc.is_rabin())
print(acc.is_streett())
```
%% Output
(4, (Fin(0) & Inf(1)) | (Fin(2) & Inf(3)))
2
-1
%% Cell type:markdown id: tags:
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.
%% Cell type:code id: tags:
``` python
acc = spot.acc_cond('parity min odd 4')
print(acc)
print(acc.is_parity())
acc.set_generalized_buchi()
print(acc)
print(acc.is_parity())
```
%% Output
(4, Fin(0) & (Inf(1) | (Fin(2) & Inf(3))))
[True, False, True]
(4, Inf(0)&Inf(1)&Inf(2)&Inf(3))
[False, False, False]
%% Cell type:markdown id: tags:
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.
%% Cell type:code id: tags:
``` python
print(acc.name())
print(acc.name("d")) # <- Style used by print_dot(aut, "a")
print(acc.name("0")) # <- no parameters
```
%% Output
generalized-Büchi 4
gen. Büchi 4
generalized-Buchi
%% Cell type:markdown id: tags:
`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`:
%% Cell type:code id: tags:
``` python
m = spot.mark_t([1, 3])
print(acc.comp(m))
```
%% Output
{0,2}
%% Cell type:markdown id: tags:
`all_sets()` returns a `mark_t` listing all the declared sets:
%% Cell type:code id: tags:
``` python
acc.all_sets()
```
%% Output
spot.mark_t([0, 1, 2, 3])
%% Cell type:markdown id: tags:
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.
%% Cell type:code id: tags:
``` python
print("acc =", acc)
for x in ([0, 1, 2, 3, 10], [1, 2]):
print("acc.accepting({}) = {}".format(x, acc.accepting(x)))
```
%% Output
acc = (4, Inf(0)&Inf(1)&Inf(2)&Inf(3))
acc.accepting([0, 1, 2, 3, 10]) = True
acc.accepting([1, 2]) = False
%% Cell type:markdown id: tags:
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.
%% Cell type:code id: tags:
``` python
print(acc)
print(acc.unsat_mark())
```
%% Output
(4, Inf(0)&Inf(1)&Inf(2)&Inf(3))
(True, spot.mark_t([]))
%% Cell type:code id: tags:
``` python
acc = spot.acc_cond(0) # use 0 acceptance sets, and the default formula (t)
print(acc)
print(acc.unsat_mark())
```
%% Output
(0, t)
(False, spot.mark_t([]))
%% Cell type:code id: tags:
``` python
acc = spot.acc_cond('Streett 2')
print(acc)
print(acc.unsat_mark())
```
%% Output
(4, (Fin(0) | Inf(1)) & (Fin(2) | Inf(3)))
(True, spot.mark_t([2]))
%% Cell type:markdown id: tags:
`top_conjuncts` and `top_disjuncts` also work on `acc_cond`. In this case they return tuple of `acc_cond` with the same number of sets.
%% Cell type:code id: tags:
``` python
print(acc.top_disjuncts())
print(acc.top_conjuncts())
```
%% Output
(spot.acc_cond(4, "(Fin(0) | Inf(1)) & (Fin(2) | Inf(3))"),)
(spot.acc_cond(4, "Fin(0) | Inf(1)"), spot.acc_cond(4, "Fin(2) | Inf(3)"))
%% Cell type:markdown id: tags:
`fin_one()` return the number of one color `x` that appears as `Fin(x)` in the formula, or `-1` if the formula is Fin-less.
The variant `fin_one_extract()` consider the acceptance condition as a disjunction (if the top-level operator is not a disjunction, we just assume the formula is a disjunction with only one disjunct), and return a pair `(x,c)` where `c` is the disjunction of all disjuncts of the original formula where `Fin(x)` appear. Also this function tries to choose an `x` such that one of the disjunct has the form `...&Fin(x)&...` if possible: this is visible in the third example, where 5 is prefered to 2.
%% Cell type:code id: tags:
``` python
print(acc)
print(acc.fin_one())
print(acc.fin_one_extract())
```
%% Output
(4, (Fin(0) | Inf(1)) & (Fin(2) | Inf(3)))
0
(0, spot.acc_cond(4, "(Fin(0) | Inf(1)) & (Fin(2) | Inf(3))"))
%% Cell type:code id: tags:
``` python
acc2 = spot.acc_cond('Rabin 3')
print(acc2)
print(acc2.fin_one())
print(acc2.fin_one_extract())
```
%% Output
(6, (Fin(0) & Inf(1)) | (Fin(2) & Inf(3)) | (Fin(4) & Inf(5)))
0
(0, spot.acc_cond(6, "Fin(0) & Inf(1)"))
%% Cell type:code id: tags:
``` python
acc3 = spot.acc_cond('Inf(0)&(Fin(2)|Inf(3)) | Inf(4)&Fin(5) | Inf(0)&Inf(5)&(Fin(5)|Fin(0))')
print(acc3)
print(acc3.fin_one())
print(acc3.fin_one_extract())
```
%% Output
(6, (Inf(0) & (Fin(2) | Inf(3))) | (Inf(4) & Fin(5)) | ((Inf(0)&Inf(5)) & (Fin(0)|Fin(5))))
2
(5, spot.acc_cond(6, "(Inf(4) & Fin(5)) | ((Inf(0)&Inf(5)) & (Fin(0)|Fin(5)))"))
......
%% Cell type:code id: tags:
``` python
import spot
from spot.jupyter import display_inline
spot.setup(show_default='.a')
```
%% Cell type:markdown id: tags:
# Containement checks
The `spot.contains()` function checks whether the language of its right argument is included in the language of its left argument. The arguments may mix automata and formulas; the latter can be given as strings.
%% Cell type:code id: tags:
``` python
f = spot.formula('GFa'); aut_f = f.translate()
g = spot.formula('FGa'); aut_g = g.translate()
```
%% Cell type:code id: tags:
``` python
spot.contains(f, g), spot.contains(g, f)
```
%% Output
(True, False)
%% Cell type:code id: tags:
``` python
spot.contains(aut_f, aut_g), spot.contains(aut_g, aut_f)
```
%% Output
(True, False)
%% Cell type:code id: tags:
``` python
spot.contains(aut_f, g), spot.contains(aut_g, f)
```
%% Output
(True, False)
%% Cell type:code id: tags:
``` python
spot.contains(f, aut_g), spot.contains(g, aut_f)
```
%% Output
(True, False)
%% Cell type:code id: tags:
``` python
spot.contains("GFa", aut_g), spot.contains("FGa", aut_f)
```
%% Output
(True, False)
%% Cell type:markdown id: tags:
Those functions are also usable as methods:
%% Cell type:code id: tags:
``` python
f.contains(aut_g), g.contains(aut_f)
```
%% Output
(True, False)
%% Cell type:code id: tags:
``` python
aut_f.contains("FGa"), aut_g.contains("GFa")
```
%% Output
(True, False)
%% Cell type:markdown id: tags:
# Equivalence checks
The `spot.are_equivalent()` tests the equivalence of the languages of its two arguments. Note that the corresponding method is called `equivalent_to()`.
%% Cell type:code id: tags:
``` python
spot.are_equivalent(f, g), spot.are_equivalent(aut_f, aut_g)
```
%% Output
(False, False)
%% Cell type:code id: tags:
``` python
f.equivalent_to(aut_g), aut_f.equivalent_to(g)
```
%% Output
(False, False)
%% Cell type:code id: tags:
``` python
aut_f.equivalent_to('XXXGFa')
```
%% Output
True
%% Cell type:markdown id: tags:
# Containement checks between formulas with cache
In the case of containement checks between formulas, `language_containement_checker` instances provide similar services, but they cache automata representing the formulas checked. This should be prefered when performing several containement checks using the same formulas.
%% Cell type:code id: tags:
``` python
lcc = spot.language_containment_checker()
```
%% Cell type:code id: tags:
``` python
lcc.contains(f, g), lcc.contains(g, f)
```
%% Output
(True, False)
%% Cell type:code id: tags:
``` python
lcc.are_equivalent(f, g)
```
%% Output
False
%% Cell type:markdown id: tags:
# Help for distinguishing languages
Assume you have computed two automata, that `are_equivalent(a1, a2)` returns `False`, and you want to know why. (This often occur when debugging some algorithm that produce an automaton that is not equivalent to which it should.) The automaton class has a method called `a1.exclusive_run(a2)` that can help with this task: it returns a run that recognizes a word is is accepted by one of the two automata but not by both. The method `a1.exclusive_run(a2)` will return just a word.
Assume you have computed two automata, that `are_equivalent(a1, a2)` returns `False`, and you want to know why. (This often occur when debugging some algorithm that produce an automaton that is not equivalent to which it should.) The automaton class has a method called `a1.exclusive_run(a2)` that can help with this task: it returns a run that recognizes a word is is accepted by one of the two automata but not by both. The method `a1.exclusive_word(a2)` will return just a word.
For instance let's find a word that is exclusive between `aut_f` and `aut_g`. (The adjective *exlusive* is a reference to the *exclusive or* operator: the word belongs to L(aut_f) "xor" it belongs to L(aut_g).)
%% Cell type:code id: tags:
``` python
aut_f.exclusive_word(aut_g)
```
%% Output
$\mathsf{cycle}\{a; \lnot a\}$
<spot.twa_word; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_word > *' at 0x7f7c7c425630> >
%% Cell type:markdown id: tags:
We can even write a small function that highlights one difference between two automata. Note that the `run` returned will belong to either `left` or `right`, so calling the `highlight()` method will colorize one of those two automata.
%% Cell type:code id: tags:
``` python
def show_one_difference(left, right):
run = left.exclusive_run(right)
if not run:
print("The two automata are equivalent.")
else:
print("The following word is only accepted by one automaton:", spot.make_twa_word(run))
run.highlight(5)
display_inline(left, right)
```
%% Cell type:code id: tags:
``` python
show_one_difference(aut_f, aut_g)
```
%% Output
The following word is only accepted by one automaton: cycle{a; !a}
......
%% Cell type:code id: tags:
``` python
from IPython.display import display
import spot
spot.setup(show_default='.bans')
```
%% Cell type:markdown id: tags:
This notebook demonstrates how to use the `decompose_scc()` function to split an automaton in up to three automata capturing different behaviors. This is based on the paper [Strength-based decomposition of the property Büchi automaton for faster model checking](https://www.lrde.epita.fr/~adl/dl/adl/renault.13.tacas.pdf) (TACAS'13).
This page uses the Python bindings, but the same decompositions can be performed from the shell using [`autfilt`](https://spot.lrde.epita.fr/autfilt.html) and its `--decompose-scc` option.
# Basics
Let's define the following strengths of accepting SCCs:
- an accepting SCC is **inherently weak** if it does not contain any rejecting cycle
- an accepting SCC is **inherently terminal** if it is *inherently weak* and complete (i.e. from any state, you can stay in the SCC by reading any word)
- an accepting SCC is **strictly inherently weak** if it is *inherently weak* and not complete (in other words: *weak* but not *terminal*)
- an accepting SCC is **strong** if it is not inherently weak.
The strengths **strong**, **stricly inherently weak**, and **inherently terminal** define a partition of all accepting SCCs. The following Büchi automaton has 4 SCCs, and its 3 accepting SCCs show an example of each strength.
Note: the reason we use the word *inherently* is that the *weak* and *terminal* properties are usually defined syntactically: an accepting SCC would be weak if all its transitions belong to the same acceptance sets. This syntactic criterion is a sufficient condition for an accepting SCC to not have any rejecting cycle, but it is not necessary. Hence a *weak* SCC is *inherently weak*; but while an *inherently weak* SCC is not necessarily *weak*, it can be modified to be *weak* without alterning the langage.
%% Cell type:code id: tags:
``` python
aut = spot.translate('(Ga -> Gb) W c')
aut
```
%% Output
<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f56404b14b0> >
%% Cell type:markdown id: tags:
The `decompose_strength()` function takes an automaton, and a string specifying which strength to preserve.
The letters used for this specification are as follows:
- `t`: (inherently) terminal
- `w`: (strictly inherently) weak
- `s`: strong
For instance if we want to preserve only the **strictly inherently weak** part of this automaton, we should get only the SCC with the self-loop on $b$, and the SCC above it so that we can reach it. However the SCC above is not stricly weak, so it should not accept any word in the new automaton.
%% Cell type:code id: tags:
``` python
spot.decompose_scc(aut, 'w')
```
%% Output
<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f56404b11b0> >
%% Cell type:markdown id: tags:
Similarly, we can extract all the behaviors captured by the **inherently terminal** part of the automaton:
%% Cell type:code id: tags:
``` python
spot.decompose_scc(aut, 't')
```
%% Output
<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f56404b1270> >
%% Cell type:markdown id: tags:
Here is the **strong** part:
%% Cell type:code id: tags:
``` python
strong = spot.decompose_scc(aut, 's'); strong
```
%% Output
<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f56404b18d0> >
%% Cell type:markdown id: tags:
The union of these three automata recognize the same language as the original automaton.
The application proposed in the aforementioned TACAS'13 paper is for parallelizing model checking. Instead of testing the emptiness of the product between `aut` and a system, one could test the emptiness **3** products in parallel: each with a sub-automaton of different strength. Model checking using weak and terminal automata can be done with much more simpler emptiness check procedures than needed for the general case. So in effect, we have isolated the "hard" (i.e. strong) part of the original automaton in a smaller automaton, and we only need to use a full-fledged emptiness check for this case.
An additional bonus is that it is possible that the simplification algorithms will do a better job at simplifying the sub-automata than at simplifying the original `aut`. For instance here the `strong` automaton can be further simplified:
%% Cell type:code id: tags:
``` python
strong.postprocess('small')
```
%% Output
<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f56404b1c00> >
%% Cell type:markdown id: tags:
# Multi-strength extraction
The string passed to `decompose_strength()` can include multiple letters to extract multiple strengths at once.
%% Cell type:code id: tags:
``` python
for opt in ('sw', 'st', 'wt'):
a = spot.decompose_scc(aut, opt)
a.set_name("option: " + opt)
display(a)
```
%% Output
%% Cell type:markdown id: tags:
# Generalized acceptance
There is nothing that prevents the above decomposition to work with other types of acceptance.
## Rabin
The following Rabin automaton was generated with
ltldo -f '(Ga -> Gb) W c' 'ltl2dstar --ltl2nba=spin:ltl2tgba@-Ds' -H | autfilt -H --merge-transitions
(The `autfilt -H --merge-transitions` pass is just here to reduce the size of the file and make the automaton more readable.)
%% Cell type:code id: tags:
``` python
aut = spot.automaton("""
HOA: v1 States: 9 Start: 2 AP: 3 "a" "b" "c" acc-name: Rabin 2 Acceptance:
4 (Fin(0) & Inf(1)) | (Fin(2) & Inf(3)) properties: trans-labels
explicit-labels state-acc complete properties: deterministic --BODY--
State: 0 {2} [0&!2] 0 [0&2] 1 [!0&!2] 5 [!0&2] 6 State: 1 {2} [0] 1 [!0]
6 State: 2 {2} [0&!1&!2] 3 [0&1&!2] 4 [!0&!2] 5 [2] 6 State: 3 {1 2}
[0&!2] 0 [0&2] 1 [!0&!2] 5 [!0&2] 6 State: 4 {1 2} [0&!1&!2] 0 [0&!1&2]
1 [!0&!2] 5 [!0&2] 6 [0&1&!2] 7 [0&1&2] 8 State: 5 {1 2} [0&!1&!2] 0
[!0&!2] 5 [2] 6 [0&1&!2] 7 State: 6 {1 2} [t] 6 State: 7 {3} [0&!1&!2]
0 [0&!1&2] 1 [!0&!2] 5 [!0&2] 6 [0&1&!2] 7 [0&1&2] 8 State: 8 {3} [0&!1]
1 [!0] 6 [0&1] 8 --END--""")
aut
```
%% Output
<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f56404b1ed0> >
%% Cell type:markdown id: tags:
Let's decompose it into three strengths:
%% Cell type:code id: tags:
``` python
for (name, opt) in (('terminal', 't'), ('strictly weak', 'w'), ('strong', 's')):
a = spot.decompose_scc(aut, opt)
a.set_name(name)
display(a)
```
%% Output
%% Cell type:markdown id: tags:
Note how the two weak automata (i.e., stricly weak and terminal) are now using a Büchi acceptance condition (because that is sufficient for weak automata) while the strong automaton inherited the original acceptance condition.
When extracting multiple strengths and one of the strength is **strong**, we preserve the original acceptance. For instance extracting **strong** and **inherently terminal** gives the following automaton, where only **stricly inherently weak** SCCs have become rejecting.
%% Cell type:code id: tags:
``` python
spot.decompose_scc(aut, "st")
```
%% Output
<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f56404b1c90> >
%% Cell type:markdown id: tags:
The weak automata seem to be good candidates for further simplification. Let's add a call to `postprocess()` to our decomposition loop, trying to preserve the determinism and state-based acceptance of the original automaton.
%% Cell type:code id: tags:
``` python
for (name, opt) in (('inherently terminal', 't'), ('strictly inherently weak', 'w'), ('strong', 's')):
a = spot.decompose_scc(aut, opt).postprocess('deterministic', 'SBAcc')
a.set_name(name)
display(a)
```
%% Output
%% Cell type:markdown id: tags:
## Streett
Since this notebook also serves as a test suite, let's try a Streett automaton. This one was generated with
ltldo -f '(Ga -> Gb) W c' 'ltl2dstar --automata=streett --ltl2nba=spin:ltl2tgba@-Ds' -H |
autfilt -H --merge-transitions
%% Cell type:code id: tags:
``` python
aut = spot.automaton("""
HOA: v1 States: 8 Start: 7 AP: 3 "a" "b" "c" acc-name: Streett
2 Acceptance: 4 (Fin(0) | Inf(1)) & (Fin(2) | Inf(3)) properties:
trans-labels explicit-labels state-acc complete properties: deterministic
--BODY-- State: 0 {2} [0&1] 0 [0&!1] 3 [!0] 4 State: 1 {2} [0&1&2]
0 [0&1&!2] 1 [0&!1&!2] 2 [0&!1&2] 3 [!0&2] 4 [!0&!2] 7 State: 2 {2}
[0&1&!2] 1 [0&!1&!2] 2 [0&2] 3 [!0&2] 4 [!0&!2] 7 State: 3 {0 3} [0] 3
[!0] 4 State: 4 {1 3} [t] 4 State: 5 {3} [0&!1] 3 [!0] 4 [0&1] 5 State:
6 {3} [0&!1&!2] 2 [0&!1&2] 3 [!0&2] 4 [0&1&2] 5 [0&1&!2] 6 [!0&!2]
7 State: 7 {3} [0&!1&!2] 2 [2] 4 [0&1&!2] 6 [!0&!2] 7 --END--""")
aut
```
%% Output
<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f5640045450> >
%% Cell type:code id: tags:
``` python
for (name, opt) in (('inherently terminal', 't'), ('strictly inherently weak', 'w'), ('strong', 's')):
a = spot.decompose_strength(aut, opt)
a.set_name(name)
display(a)
```
%% Output
%% Cell type:markdown id: tags:
The subtlety of Streett acceptance is that a path that does not visit any accepting set infinitely often *is* accepting. So when disabling SCCs, we must be careful to label them with a combination of rejecting acceptance sets.
This is easy to understand using an example. In the following extraction of the **strong** and **inherently terminal** parts, the rejecting SCCs (that were either rejecting or strictly inherently weak originally) have been labeled by the same acceptance sets, to ensure that they are rejected.
%% Cell type:code id: tags:
``` python
spot.decompose_scc(aut, 'st')
```
%% Output