Commit 9d6ba3ff authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

* tests/python/word.ipynb: Typo.

parent b860bb24
...@@ -350,7 +350,7 @@ ...@@ -350,7 +350,7 @@
"cell_type": "markdown", "cell_type": "markdown",
"metadata": {}, "metadata": {},
"source": [ "source": [
"Calling `simplifify()` will produce a shorter word that is compatible with the original word. For instance in the above word, the second `a` is compatible with `!a & b`, so the prefix can be shortened by rotating the cycle." "Calling `simplify()` will produce a shorter word that is compatible with the original word. For instance, in the above word the second `a` is compatible with `!a & b`, so the prefix can be shortened by rotating the cycle."
] ]
}, },
{ {
......
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` python ``` python
import spot import spot
spot.setup() spot.setup()
``` ```
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Let's build a small automaton to use as example. Let's build a small automaton to use as example.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` python ``` python
aut = spot.translate('!a & G(Fa <-> XXb)'); aut aut = spot.translate('!a & G(Fa <-> XXb)'); aut
``` ```
%%%% Output: execute_result %%%% Output: execute_result
<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f14f57d93c0> > <spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f14f57d93c0> >
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Build an accepting run: Build an accepting run:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` python ``` python
run = aut.accepting_run() run = aut.accepting_run()
print(run) print(run)
``` ```
%%%% Output: stream %%%% Output: stream
Prefix: Prefix:
0 0
| !a | !a
1 1
| !a | !a
Cycle: Cycle:
2 2
| a & b {0} | a & b {0}
3 3
| !a & b | !a & b
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Accessing the contents of the run can be done via the `prefix` and `cycle` lists. Accessing the contents of the run can be done via the `prefix` and `cycle` lists.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` python ``` python
print(spot.bdd_format_formula(aut.get_dict(), run.prefix[0].label)) print(spot.bdd_format_formula(aut.get_dict(), run.prefix[0].label))
print(run.cycle[0].acc) print(run.cycle[0].acc)
``` ```
%%%% Output: stream %%%% Output: stream
!a !a
{0} {0}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
To convert the run into a word, using `spot.twa_word()`. Note that our runs are labeled by Boolean formulas that are not necessarily a conjunction of all involved litterals. The word is just the projection of the run on its labels. To convert the run into a word, using `spot.twa_word()`. Note that our runs are labeled by Boolean formulas that are not necessarily a conjunction of all involved litterals. The word is just the projection of the run on its labels.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` python ``` python
word = spot.twa_word(run) word = spot.twa_word(run)
print(word) # print as a string print(word) # print as a string
word # LaTeX-style representation in notebooks word # LaTeX-style representation in notebooks
``` ```
%%%% Output: stream %%%% Output: stream
!a; !a; cycle{a & b; !a & b} !a; !a; cycle{a & b; !a & b}
%%%% Output: execute_result %%%% Output: execute_result
$\lnot a; \lnot a; \mathsf{cycle}\{a \land b; \lnot a \land b\}$ $\lnot a; \lnot a; \mathsf{cycle}\{a \land b; \lnot a \land b\}$
<spot.twa_word; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_word > *' at 0x7f14f57d9ed0> > <spot.twa_word; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_word > *' at 0x7f14f57d9ed0> >
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
A word can be represented as a collection of signals (one for each atomic proposition). The cycle part is shown twice. A word can be represented as a collection of signals (one for each atomic proposition). The cycle part is shown twice.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` python ``` python
word.show() word.show()
``` ```
%%%% Output: execute_result %%%% Output: execute_result
<spot.jupyter.SVG object> <spot.jupyter.SVG object>
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Accessing the different formulas (stored as BDDs) can be done again via the `prefix` and `cycle` lists. Accessing the different formulas (stored as BDDs) can be done again via the `prefix` and `cycle` lists.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` python ``` python
print(spot.bdd_format_formula(aut.get_dict(), word.prefix[0])) print(spot.bdd_format_formula(aut.get_dict(), word.prefix[0]))
print(spot.bdd_format_formula(aut.get_dict(), word.prefix[1])) print(spot.bdd_format_formula(aut.get_dict(), word.prefix[1]))
print(spot.bdd_format_formula(aut.get_dict(), word.cycle[0])) print(spot.bdd_format_formula(aut.get_dict(), word.cycle[0]))
print(spot.bdd_format_formula(aut.get_dict(), word.cycle[1])) print(spot.bdd_format_formula(aut.get_dict(), word.cycle[1]))
``` ```
%%%% Output: stream %%%% Output: stream
!a !a
!a !a
a & b a & b
!a & b !a & b
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Calling `simplifify()` will produce a shorter word that is compatible with the original word. For instance in the above word, the second `a` is compatible with `!a & b`, so the prefix can be shortened by rotating the cycle. Calling `simplify()` will produce a shorter word that is compatible with the original word. For instance, in the above word the second `a` is compatible with `!a & b`, so the prefix can be shortened by rotating the cycle.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` python ``` python
word.simplify() word.simplify()
print(word) print(word)
``` ```
%%%% Output: stream %%%% Output: stream
!a; cycle{!a & b; a & b} !a; cycle{!a & b; a & b}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Such a simplified word can be created directly from the automaton: Such a simplified word can be created directly from the automaton:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` python ``` python
aut.accepting_word() aut.accepting_word()
``` ```
%%%% Output: execute_result %%%% Output: execute_result
$\lnot a; \mathsf{cycle}\{\lnot a \land b; a \land b\}$ $\lnot a; \mathsf{cycle}\{\lnot a \land b; a \land b\}$
<spot.twa_word; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_word > *' at 0x7f14f57d9660> > <spot.twa_word; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_word > *' at 0x7f14f57d9660> >
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Words can be created using the `parse_word` function: Words can be created using the `parse_word` function:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` python ``` python
print(spot.parse_word('a; b; cycle{a&b}')) print(spot.parse_word('a; b; cycle{a&b}'))
print(spot.parse_word('cycle{a&bb|bac&(aaa|bbb)}')) print(spot.parse_word('cycle{a&bb|bac&(aaa|bbb)}'))
print(spot.parse_word('a; b;b; qiwuei;"a;b&c;a" ;cycle{a}')) print(spot.parse_word('a; b;b; qiwuei;"a;b&c;a" ;cycle{a}'))
``` ```
%%%% Output: stream %%%% Output: stream
a; b; cycle{a & b} a; b; cycle{a & b}
cycle{(a & bb) | (aaa & bac) | (bac & bbb)} cycle{(a & bb) | (aaa & bac) | (bac & bbb)}
a; b; b; qiwuei; "a;b&c;a"; cycle{a} a; b; b; qiwuei; "a;b&c;a"; cycle{a}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` python ``` python
# make sure that we can parse a word back after it has been printed # make sure that we can parse a word back after it has been printed
w = spot.parse_word(str(spot.parse_word('a;b&a;cycle{!a&!b;!a&b}'))); w w = spot.parse_word(str(spot.parse_word('a;b&a;cycle{!a&!b;!a&b}'))); w
``` ```
%%%% Output: execute_result %%%% Output: execute_result
$a; a \land b; \mathsf{cycle}\{\lnot a \land \lnot b; \lnot a \land b\}$ $a; a \land b; \mathsf{cycle}\{\lnot a \land \lnot b; \lnot a \land b\}$
<spot.twa_word; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_word > *' at 0x7f14f5799ea0> > <spot.twa_word; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_word > *' at 0x7f14f5799ea0> >
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` python ``` python
w.show() w.show()
``` ```
%%%% Output: execute_result %%%% Output: execute_result
<spot.jupyter.SVG object> <spot.jupyter.SVG object>
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Words can be easily converted to automata Words can be easily converted to automata
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` python ``` python
w.as_automaton() w.as_automaton()
``` ```
%%%% Output: execute_result %%%% Output: execute_result
<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f14f5799ed0> > <spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f14f5799ed0> >
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment