diff --git a/NEWS b/NEWS index 1dcf7f564..f5538ee54 100644 --- a/NEWS +++ b/NEWS @@ -36,6 +36,9 @@ New in spot 2.10.4.dev (net yet released) alphabet, in applications where using atomic propositions is inconvenient. + - print_dot() learned option "@" to display aliases, as discussed + above. + New in spot 2.10.4 (2022-02-01) Bug fixed: diff --git a/doc/org/hoa.org b/doc/org/hoa.org index b9116eb65..26969e4ed 100644 --- a/doc/org/hoa.org +++ b/doc/org/hoa.org @@ -694,10 +694,11 @@ named properties of any type. When attaching a property to a TωA, you only supply a name for the property, a pointer, and an optional destructor function. -There are currently two [[file:concepts.org::#named-properties][named properties]] related to the HOA format. +There are currently three [[file:concepts.org::#named-properties][named properties]] related to the HOA format. - =automaton-name= :: Is a string that stores the name of the automaton (the one given after =name:= in the HOA format) -- =state-names= :: is a vector of strings that stores the name of the states (in case states are named in the HOA format) +- =state-names= :: Is a vector of strings that stores the name of the states (in case states are named in the HOA format) +- =aliases= :: Is a vector of pairs (name, BDD) that declares aliases to use in the HOA format You can see these properties being preserved when an automaton is read and then immediately output: @@ -710,14 +711,15 @@ States: 3 Start: 0 AP: 2 "a" "b" Acceptance: 2 Inf(0)&Inf(1) +Alias: @x 0&1 --BODY-- State: 0 {0} [0&!1] 0 -[0&1] 1 +[@x] 1 [!0] 2 State: 1 "I am a state" [0] 1 {1} -[0&1] 2 {1} +[@x] 2 {1} State: 2 "so am I" [!0] 1 {0 1} [0] 2 {0 1} @@ -727,7 +729,7 @@ autfilt hw.hoa #+END_SRC #+RESULTS: hello-world -#+BEGIN_SRC hoa +#+begin_SRC hoa HOA: v1 name: "hello world!" States: 3 @@ -736,27 +738,29 @@ AP: 2 "a" "b" acc-name: generalized-Buchi 2 Acceptance: 2 Inf(0)&Inf(1) properties: trans-labels explicit-labels state-acc +Alias: @x 0&1 --BODY-- State: 0 {0} [0&!1] 0 -[0&1] 1 +[@x] 1 [!0] 2 State: 1 "I am a state" {1} -[0] 1 -[0&1] 2 +[@x | 0&!1] 1 +[@x] 2 State: 2 "so am I" {0 1} [!0] 1 -[0] 2 +[@x | 0&!1] 2 --END-- -#+END_SRC +#+end_SRC -However if =autfilt= performs some transformation, and actually has to +However when Spot performs some transformation, and actually has to construct a new automaton, those properties will not be quarried over to the new automaton. First because it is not obvious that the new automaton should have the same name, and second because if a new automaton is created, there might not be clear correspondence between -the old states and the new ones. - +the old states and the new ones. =autfilt= tries to preserve aliases +by reintroducing them to the automaton before it is outputs it (unless +option =--aliases=drop= is used). Here is for instance the result when =autfilt= is instructed to simplify the automaton: @@ -766,7 +770,7 @@ autfilt --small hw.hoa #+END_SRC #+RESULTS: -#+BEGIN_SRC hoa +#+begin_SRC hoa HOA: v1 States: 3 Start: 0 @@ -774,20 +778,20 @@ AP: 2 "a" "b" acc-name: Buchi Acceptance: 1 Inf(0) properties: trans-labels explicit-labels state-acc deterministic +Alias: @x 0&1 --BODY-- State: 0 [0&!1] 0 -[0&1] 1 +[@x] 1 [!0] 2 State: 1 [0&!1] 1 -[0&1] 2 +[@x] 2 State: 2 {0} [!0] 1 -[0] 2 +[@x | 0&!1] 2 --END-- -#+END_SRC - +#+end_SRC Note that if the name of the automaton is important to you, it can be fixed via the =--name= option. For instance =--name=%M= will @@ -822,9 +826,10 @@ State: 2 {0} --END-- #+END_SRC -The page about [[file:oaut.org][common output option for automata]] has a section showing -how =--name= can be used to construct complex pipelines with automata that -preserve their equivalent LTL formula in the =name:= field. +The page about [[file:oaut.org][common output options for automata]] has a section +showing how =--name= can be used to construct complex pipelines with +automata that preserve their equivalent LTL formula in the =name:= +field. * Streaming support diff --git a/doc/org/tut.org b/doc/org/tut.org index 12c700a3f..598276f38 100644 --- a/doc/org/tut.org +++ b/doc/org/tut.org @@ -93,6 +93,7 @@ real notebooks instead. - [[https://spot.lrde.epita.fr/ipynb/stutter-inv.html][=stutter-inv.ipynb=]] working with stutter-invariant formulas properties. - [[https://spot.lrde.epita.fr/ipynb/satmin.html][=satmin.ipynb=]] Python interface for [[file:satmin.org][SAT-based minimization of deterministic ω-automata]]. - [[https://spot.lrde.epita.fr/ipynb/twagraph-internals.html][=twagraph-internals.ipynb=]] Inner workings of the =twa_graph= class. +- [[https://spot.lrde.epita.fr/ipynb/aliases.html][=aliases.ipynb=]] Support for HOA aliases. - [[https://spot.lrde.epita.fr/ipynb/zlktree.html][=zlktree.ipynb=]] demonstration of Zielonka Trees and ACD # LocalWords: utf html bdd IPython ipynb io randaut accparse acc diff --git a/spot/twaalgos/dot.cc b/spot/twaalgos/dot.cc index 7f2511f28..66804f304 100644 --- a/spot/twaalgos/dot.cc +++ b/spot/twaalgos/dot.cc @@ -32,6 +32,7 @@ #include #include #include +#include #include #include #include @@ -83,6 +84,7 @@ namespace spot std::map, int> univ_done; std::vector true_states_; std::vector* state_player_; + std::unique_ptr haf_ = nullptr; acc_cond::mark_t inf_sets_ = {}; acc_cond::mark_t fin_sets_ = {}; @@ -112,6 +114,7 @@ namespace spot bool max_states_given_ = false; // related to max_states_ bool opt_latex_ = false; bool opt_showlabel_ = true; + bool opt_aliases_ = false; const char* nl_ = "\\n"; const char* label_pre_ = "label=\""; char label_post_ = '"'; @@ -225,6 +228,9 @@ namespace spot case '1': inline_state_names_ = false; break; + case '@': + opt_aliases_ = true; + break; case 'a': opt_show_acc_ = true; break; @@ -479,6 +485,11 @@ namespace spot std::ostream& format_label(std::ostream& os, bdd label) const { + if (haf_) + { + os << haf_->encode_label(label); + return os; + } return format_label(os, bdd_to_formula(label, aut_->get_dict())); } @@ -970,6 +981,37 @@ namespace spot if (opt_hide_true_states_) find_true_states(); + if (opt_aliases_ && + aut->get_named_prop + >>("aliases")) + { + const char* falsestr = "0"; + const char* truestr = "1"; + const char* orstr = " | "; + const char* andstr = " & "; + const char* notstr = "!"; + const char* lparstr = "("; + const char* rparstr = ")"; + if (opt_html_labels_) + { + andstr = " & "; + } + + haf_.reset(new hoa_alias_formater + (aut, falsestr, truestr, orstr, andstr, + notstr, lparstr, rparstr, + [this, d=aut->get_dict()](int var)->std::string + { + const bdd_dict::bdd_info& i = d->bdd_map[var]; + if (SPOT_UNLIKELY(i.type != bdd_dict::var)) + throw std::runtime_error + ("print_dot(): unknown BDD variable"); + std::ostringstream os; + format_label(os, i.f); + return os.str(); + })); + } + sn_ = aut->get_named_prop>("state-names"); // We have no names. Do we have product sources? if (!sn_) diff --git a/tests/Makefile.am b/tests/Makefile.am index af87ad6cb..86802f75b 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -351,6 +351,7 @@ if USE_PYTHON TESTS_ipython = \ python/acc_cond.ipynb \ python/accparse.ipynb \ + python/aliases.ipynb \ python/alternation.ipynb \ python/atva16-fig2a.ipynb \ python/atva16-fig2b.ipynb \ diff --git a/tests/core/ltl2tgba.test b/tests/core/ltl2tgba.test index 8417df485..c3491c412 100755 --- a/tests/core/ltl2tgba.test +++ b/tests/core/ltl2tgba.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2009-2019 Laboratoire de Recherche et Développement de +# Copyright (C) 2009-2019, 2022 Laboratoire de Recherche et Développement de # l'Epita (LRDE). # Copyright (C) 2003-2004 Laboratoire d'Informatique de Paris 6 # (LIP6), département Systèmes Répartis Coopératifs (SRC), Université @@ -230,8 +230,8 @@ for a in 'a1;a2' 'a1[*];a2[*]'; do done # test unknown dot options -ltl2tgba --dot=@ a 2>stderr && exit 1 -grep 'ltl2tgba: unknown option.*@' stderr +ltl2tgba --dot='~' a 2>stderr && exit 1 +grep 'ltl2tgba: unknown option.*~' stderr # Make sure the count of AP is correct through never claims or LBTT ltl2tgba -f a -s | autfilt -q --ap=1 --lbtt | autfilt -q --ap=1 diff --git a/tests/core/randaut.test b/tests/core/randaut.test index 67edd1d4c..7ff851646 100755 --- a/tests/core/randaut.test +++ b/tests/core/randaut.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2014-2018, 2020 Laboratoire de Recherche et +# Copyright (C) 2014-2018, 2020, 2022 Laboratoire de Recherche et # Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -79,8 +79,8 @@ diff out expected randaut -n 5 --stats='name: "%F-%L-%s-%c-%e"' a >out2 diff out2 expected -randaut -n 5 --dot=@ a 2>stderr && exit 1 -grep 'randaut: unknown option.*@' stderr +randaut -n 5 --dot='~' a 2>stderr && exit 1 +grep 'randaut: unknown option.*~' stderr randaut -n -1 -Q2 2 -H | autfilt -H --is-deterministic -n 3 -o out.hoa randaut -n -1 -Q2 2 -H | autfilt -H -v --is-deterministic -n 4 -o '>>out.hoa' diff --git a/tests/python/aliases.ipynb b/tests/python/aliases.ipynb new file mode 100644 index 000000000..4cca2fa86 --- /dev/null +++ b/tests/python/aliases.ipynb @@ -0,0 +1,992 @@ +{ + "cells": [ + { + "cell_type": "code", + "execution_count": 1, + "id": "4ea4978c", + "metadata": {}, + "outputs": [], + "source": [ + "import spot\n", + "from spot.jupyter import display_inline\n", + "from buddy import bdd_ithvar\n", + "spot.setup()" + ] + }, + { + "cell_type": "markdown", + "id": "4dc12445", + "metadata": {}, + "source": [ + "Aliases is a feature of the HOA format that allows Boolean formulas to be named and reused to label automata. This can be helpful to reduce the size of a file, but it can also be abused to \"fake\" arbritary alphabets by using an alphabet of $n$ aliases encoded over $\\log_2(n)$ atomic propositions. \n", + "\n", + "Spot knows how to read HOA files containing aliases since version 2.0. However support for producing files with aliases was only added in version 2.11.\n", + "\n", + "When a HOA file containing aliases is read, the aliases are automatically expanded to define the automaton." + ] + }, + { + "cell_type": "code", + "execution_count": 2, + "id": "09bc3560", + "metadata": {}, + "outputs": [ + { + "data": { + "text/html": [ + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "⓿\n", + ")&Inf(\n", + "❶\n", + ")\n", + "[gen. Büchi 2]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "p0 & !p1\n", + "⓿\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!p0 & p1\n", + "❶\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "p0 & p1\n", + "⓿\n", + "❶\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "g\n", + "\n", + "\n", + "\n", + "states\n", + "\n", + "\n", + "states\n", + "\n", + "\n", + "0\n", + "\n", + "succ\n", + "\n", + "\n", + "1\n", + "\n", + "succ_tail\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "\n", + "edges\n", + "\n", + "\n", + "edges\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "cond\n", + "\n", + "!p0 & !p1\n", + "\n", + "p0 & !p1\n", + "\n", + "!p0 & p1\n", + "\n", + "p0 & p1\n", + "\n", + "acc\n", + "\n", + "{}\n", + "\n", + "{0}\n", + "\n", + "{1}\n", + "\n", + "{0,1}\n", + "\n", + "dst\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "next_succ\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "0\n", + "\n", + "src\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "meta\n", + "init_state:\n", + "\n", + "0\n", + "num_sets:\n", + "2\n", + "acceptance:\n", + "Inf(0)&Inf(1)\n", + "ap_vars:\n", + "p0 p1\n", + "\n", + "\n", + "\n", + "\n", + "props\n", + "prop_state_acc:\n", + "maybe\n", + "prop_inherently_weak:\n", + "maybe\n", + "prop_terminal:\n", + "maybe\n", + "prop_weak:\n", + "maybe\n", + "prop_very_weak:\n", + "maybe\n", + "prop_complete:\n", + "yes\n", + "prop_universal:\n", + "yes\n", + "prop_unambiguous:\n", + "yes\n", + "prop_semi_deterministic:\n", + "yes\n", + "prop_stutter_invariant:\n", + "maybe\n", + "\n", + "\n", + "\n", + "\n", + "namedprops\n", + "named properties:\n", + "aliases\n", + "\n", + "\n", + "\n", + "\n", + "
" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "a = spot.automaton(\"\"\"HOA: v1\n", + "States: 1\n", + "Start: 0\n", + "AP: 2 \"p0\" \"p1\"\n", + "Acceptance: 2 Inf(0)&Inf(1)\n", + "Alias: @a !0&!1\n", + "Alias: @b 0&!1\n", + "Alias: @c !0&1\n", + "Alias: @d 0&1\n", + "--BODY--\n", + "State: 0\n", + "[@a] 0\n", + "[@b] 0 {0}\n", + "[@c] 0 {1}\n", + "[@d] 0 {0 1}\n", + "--END--\n", + "\"\"\")\n", + "display_inline(a, a.show_storage(), per_row=2)" + ] + }, + { + "cell_type": "markdown", + "id": "593d8b93", + "metadata": {}, + "source": [ + "For more information about how to interpret the output of `show_storage()`, please see the `twagraph-internals.ipynb` notebook.\n", + "\n", + "Here, observe that the edges, labeled with aliases `@a`, `@b`, `@c`, and `@d` in the input file, actually store the expanded values of the aliases. Algorithms in Spot know nothing about the aliases, and only work with edges labeled by Boolean formulas of atomic propositions.\n", + "\n", + "However since Spot 2.11, the automaton now stores an `aliases` named-property. This property is used by the HOA printer to *attempt* to recreate edge labels using those aliases." + ] + }, + { + "cell_type": "code", + "execution_count": 3, + "id": "49b2efcb", + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "HOA: v1\n", + "States: 1\n", + "Start: 0\n", + "AP: 2 \"p0\" \"p1\"\n", + "acc-name: generalized-Buchi 2\n", + "Acceptance: 2 Inf(0)&Inf(1)\n", + "properties: trans-labels explicit-labels trans-acc complete\n", + "properties: deterministic\n", + "Alias: @a !0&!1\n", + "Alias: @b 0&!1\n", + "Alias: @c !0&1\n", + "Alias: @d !@c&!@b&!@a\n", + "--BODY--\n", + "State: 0\n", + "[@a] 0\n", + "[@b] 0 {0}\n", + "[@c] 0 {1}\n", + "[@d] 0 {0 1}\n", + "--END--\n" + ] + } + ], + "source": [ + "print(a.to_str('hoa'))" + ] + }, + { + "cell_type": "markdown", + "id": "6f93a48e", + "metadata": {}, + "source": [ + "Additionally, passing option `@` to the Dot printer will ask it to use aliases as well." + ] + }, + { + "cell_type": "code", + "execution_count": 4, + "id": "9802e266", + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "⓿\n", + ")&Inf(\n", + "❶\n", + ")\n", + "[gen. Büchi 2]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "@a\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "@b\n", + "⓿\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "@c\n", + "❶\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "@d\n", + "⓿\n", + "❶\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + "" + ] + }, + "execution_count": 4, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "a.show('.@')" + ] + }, + { + "cell_type": "markdown", + "id": "3b9c1b57", + "metadata": {}, + "source": [ + "It should be noted that aside from input and output functions, algorithm do not care about aliases. In particular, they will not preserve the `aliases` property while creating a new automaton:" + ] + }, + { + "cell_type": "code", + "execution_count": 5, + "id": "e36d1446", + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "⓿\n", + ")\n", + "[Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!p1\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "p0 & p1\n", + "⓿\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "p0\n", + "⓿\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!p0\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + "" + ] + }, + "execution_count": 5, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "b = spot.degeneralize_tba(a)\n", + "b.show('.@')" + ] + }, + { + "cell_type": "markdown", + "id": "32483b2e", + "metadata": {}, + "source": [ + "This situation can be fixed by copying the aliases manually from the input automaton to the output automaton. (This is something that `autfilt` does by default, unless `--aliases=drop` is passed.)" + ] + }, + { + "cell_type": "code", + "execution_count": 6, + "id": "a9c0578c", + "metadata": {}, + "outputs": [], + "source": [ + "spot.set_aliases(b, spot.get_aliases(a))" + ] + }, + { + "cell_type": "code", + "execution_count": 7, + "id": "d3958e30", + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "⓿\n", + ")\n", + "[Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "@b | @a\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "@d\n", + "⓿\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "@c\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "@d | @b\n", + "⓿\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "@c | @a\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + "" + ] + }, + "execution_count": 7, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "b.show('.@')" + ] + }, + { + "cell_type": "markdown", + "id": "9a51f316", + "metadata": {}, + "source": [ + "Notice how `p0` and `!p0` were rewritten as disjunction of aliases because no direct aliases could be found for them. \n", + "\n", + "Generaly, the display code tries to format formulas as a sum of product. It wil recognize conjunctions and disjunctions of aliases, but if it fails, it will resort to printing the original atomic propositions (maybe mixed with aliases)." + ] + }, + { + "cell_type": "code", + "execution_count": 8, + "id": "f0dc410f", + "metadata": {}, + "outputs": [], + "source": [ + "a = spot.automaton(\"\"\"HOA: v1\n", + "States: 3\n", + "Start: 0\n", + "AP: 4 \"p0\" \"p1\" \"p2\" \"p3\"\n", + "Acceptance: 0 t\n", + "Alias: @a !0&!1\n", + "Alias: @b 0&!1\n", + "Alias: @c !0&1\n", + "Alias: @x 2&3\n", + "Alias: @y !2&!3\n", + "Alias: @z !2&3\n", + "--BODY--\n", + "State: 0\n", + "[@a&@x] 0\n", + "[@b&!@x] 1 \n", + "State: 1\n", + "[@c&@y] 0 \n", + "[!@c&!@y] 2 \n", + "State: 2\n", + "[(@a|@b)&@x] 2\n", + "[(@b|@c)&@x] 2\n", + "[@a|@b|@c] 0\n", + "--END--\n", + "\"\"\")" + ] + }, + { + "cell_type": "code", + "execution_count": 9, + "id": "d5366983", + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "t\n", + "[all]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "@x & @a\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "@b & !@x\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "@y & @c\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!@y & !@c\n", + "\n", + "\n", + "\n", + "2->0\n", + "\n", + "\n", + "@c | @b | @a\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "@x & !p1\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "(@x & @c) | (@x & @b)\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + "" + ] + }, + "execution_count": 9, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "a.show('.@')" + ] + }, + { + "cell_type": "markdown", + "id": "e1e89823", + "metadata": {}, + "source": [ + "The above shows that the aliasing may fail to recover some non-trivial aliases combinations. Look in particular at the loops above state 2. `(@b|@c)&@x`, was recovered as `(@x&@c)|(@x&@b)`, but for\n", + "`(@a|@b)&@x`, which is equivalent to `!p1&p2&p3`, the code failed to translate `!p1` as `@a|@b`, so it kept `!p1`.\n", + "\n", + "\n", + "When the automaton uses the `synthesis-outputs` property to distinguish in and out variables (see the `synthesis.ipnb` notebook for more details), aliasing is done on inputs and output separately." + ] + }, + { + "cell_type": "code", + "execution_count": 10, + "id": "0947b601", + "metadata": {}, + "outputs": [], + "source": [ + "spot.set_synthesis_outputs(a, bdd_ithvar(a.register_ap('p2')) & bdd_ithvar(a.register_ap('p3')))" + ] + }, + { + "cell_type": "code", + "execution_count": 11, + "id": "4290d8ca", + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "\n", + "@a\n", + "/\n", + "\n", + "@x\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "\n", + "@b\n", + "/\n", + "\n", + "!@x\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "\n", + "@c\n", + "/\n", + "\n", + "@y\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "\n", + "!@c\n", + "/\n", + "\n", + "!@y\n", + "\n", + "\n", + "\n", + "2->0\n", + "\n", + "\n", + "\n", + "@c | @b | @a\n", + "/\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "\n", + "@b | @a\n", + "/\n", + "\n", + "@x\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "\n", + "@c | @b\n", + "/\n", + "\n", + "@x\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + "" + ] + }, + "execution_count": 11, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "a.show('.@')" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "id": "bcba9188", + "metadata": {}, + "outputs": [], + "source": [] + } + ], + "metadata": { + "kernelspec": { + "display_name": "Python 3 (ipykernel)", + "language": "python", + "name": "python3" + }, + "language_info": { + "codemirror_mode": { + "name": "ipython", + "version": 3 + }, + "file_extension": ".py", + "mimetype": "text/x-python", + "name": "python", + "nbconvert_exporter": "python", + "pygments_lexer": "ipython3", + "version": "3.9.2" + } + }, + "nbformat": 4, + "nbformat_minor": 5 +}