Skip to content
GitLab
Commit 4ecd066c authored by Clément Gillard's avatar Clément Gillard Committed by Alexandre Duret-Lutz
Browse files

Several typos 

* HACKING: Missing "to", extraneous 's'.
* spot/misc/timer.hh: Extraneous space.
* spot/twa/acc.hh: Extraneous 's', typos.
* spot/twaalgos/genem.hh: Typo.
* spot/twaalgos/sccinfo.cc: Fix indentation.
* spot/twaalgos/sccinfo.hh: Missing 's'.
* tests/python/acc_cond.ipynb: Extraneous 'e', missing comma.
* tests/python/decompose.ipynb: Extraneous 't'.
* tests/python/ltsmin-dve.ipynb: Extraneous verb.
parent 0c32f6b7
Hide whitespace changes
Inline Side-by-side
HACKING
View file @ 4ecd066c
......@@ -354,7 +354,7 @@ Exporting symbols
header.
* The directory src/priv/ can be used to store files that are
globaly private the library, and that do not really belongs to
globaly private to the library, and that do not really belong to
other directories.
* Functions and classes that are public should be marked with
......
spot/misc/timer.hh
View file @ 4ecd066c
......@@ -290,7 +290,7 @@ namespace spot
tm_type tm;
};
/// \brief Struct used to start and stop both timer and stopwatch clocks.
/// \brief Struct used to start and stop both timer and stopwatch clocks.
typedef struct process_timer
{
void start()
......
spot/twa/acc.hh
View file @ 4ecd066c
......@@ -429,7 +429,7 @@ namespace spot
} sub;
};
/// \brief An acceptance formulas.
/// \brief An acceptance formula.
///
/// Acceptance formulas are stored as a vector of acc_word in a
/// kind of reverse polish notation. The motivation for this
......@@ -1356,13 +1356,13 @@ namespace spot
uses_fin_acceptance_ = check_fin_acceptance();
}
/// \brief Retrieve teh acceptance formula
/// \brief Retrieve the acceptance formula
const acc_code& get_acceptance() const
{
return code_;
}
/// \brief Retrieve teh acceptance formula
/// \brief Retrieve the acceptance formula
acc_code& get_acceptance()
{
return code_;
......@@ -1793,7 +1793,7 @@ namespace spot
/// \brief Check potential acceptance of an SCC.
///
/// Assuming that an SCC intersects all sets in \a
/// infinitely_often (i.e., for each set in \a infinetely_often,
/// infinitely_often (i.e., for each set in \a infinitely_often,
/// there exist one marked transition in the SCC), and is
/// included in all sets in \a always_present (i.e., all
/// transitions are marked with \a always_present), this returns
......@@ -1809,7 +1809,7 @@ namespace spot
/// \brief Return an accepting subset of \a inf
///
/// This function works only on Fin-less acceptance, and returns a
/// subset of \a inf that is enough to satisfies the acceptance
/// subset of \a inf that is enough to satisfy the acceptance
/// condition. This is typically used when an accepting SCC that
/// visits all sets in \a inf has been found, and we want to find
/// an accepting cycle: maybe it is not necessary for the accepting
......
spot/twaalgos/genem.hh
View file @ 4ecd066c
......@@ -24,7 +24,7 @@
namespace spot
{
/// \ingroup emptiness_check_algorithms
/// \brief Emptiness check of on automaton, for any acceptance condition.
/// \brief Emptiness check of an automaton, for any acceptance condition.
SPOT_API bool
generic_emptiness_check(const const_twa_graph_ptr& aut);
......
spot/twaalgos/sccinfo.cc
View file @ 4ecd066c
......@@ -185,7 +185,7 @@ namespace spot
if (accept)
one_acc_scc_ = num;
bool reject = triv ||
aut->acc().maybe_accepting(acc, common).is_false();
aut->acc().maybe_accepting(acc, common).is_false();
node_.back().rejecting_ = reject;
root_.pop_back();
}
......
spot/twaalgos/sccinfo.hh
View file @ 4ecd066c
......@@ -364,7 +364,7 @@ namespace spot
///
/// Additionally this class can be used on alternating automata, but
/// in this case, universal transitions are handled like existential
/// transitions. It still make sense to check which states belong
/// transitions. It still makes sense to check which states belong
/// to the same SCC, but the acceptance information computed by
/// this class is meaningless.
class SPOT_API scc_info
......
tests/python/acc_cond.ipynb
View file @ 4ecd066c
%% 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 valide 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.
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++
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:
# `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]))
......
tests/python/decompose.ipynb
View file @ 4ecd066c
%% 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.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fd3d85c40f0> >
%% 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.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fd3d85c40c0> >
%% 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.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fd3d860a060> >
%% 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.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fd3d85c4120> >
%% 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.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fd3d8571690> >
%% 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.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fd3d8571540> >
%% 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.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fd3d8571a80> >
%% 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