diff --git a/NEWS b/NEWS index 48b5d1bfd..0aa3e31f0 100644 --- a/NEWS +++ b/NEWS @@ -40,6 +40,15 @@ New in spot 2.5.2.dev (not yet released) example, the translation of GF(a <-> XXb) to transition-based Büchi went from 9 to 5 states using that construction. + - Slightly improved log output for the SAT-based minimization + functions. The CSV log files now include an additional column + with the size of the reference automaton, and they now have a + header line. These log files give more details and are more + accurate in the case of incremental SAT-solving. The python + bindings for sat_minimize() now have a display_log and return_log + options; there are demonstrated on the new + https://spot.lrde.epita.fr/ipynb/satmin.html page. + Bugs fixed: - "autfilt --cobuchi --small/--det" would turn a transition-based diff --git a/bench/dtgbasat/gen.py b/bench/dtgbasat/gen.py index f581506db..e96bf2825 100755 --- a/bench/dtgbasat/gen.py +++ b/bench/dtgbasat/gen.py @@ -1,5 +1,5 @@ #!/usr/bin/env python3 -# Copyright (C) 2016, 2017 Laboratoire de Recherche et Développement de +# Copyright (C) 2016-2018 Laboratoire de Recherche et Développement de # l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -272,7 +272,7 @@ def get_last_successful(n, category, pattern): + '.satlog', 'r') log_csv = csv.reader(log) for line in log_csv: - min_val = line[1] + min_val = line[2] return '$\\le$' + min_val except Exception: return '' diff --git a/bench/dtgbasat/tabl.pl b/bench/dtgbasat/tabl.pl index 2a6d644ed..7a6a8d050 100755 --- a/bench/dtgbasat/tabl.pl +++ b/bench/dtgbasat/tabl.pl @@ -79,7 +79,7 @@ sub getlastsuccesful($$) while (my $line = ) { my @f = split(/,/, $line); - $min = $f[1] if $f[1] ne ''; + $min = $f[2] if $f[2] ne ''; } $min = ", \$\\le\$$min" if $min ne ""; return $min; diff --git a/bench/dtgbasat/tabl1.pl b/bench/dtgbasat/tabl1.pl index 6e1a2f04f..d1a0b5dca 100755 --- a/bench/dtgbasat/tabl1.pl +++ b/bench/dtgbasat/tabl1.pl @@ -72,7 +72,7 @@ sub getlastsuccesful($$) while (my $line = ) { my @f = split(/,/, $line); - $min = $f[1] if $f[1] ne ''; + $min = $f[2] if $f[2] ne ''; } $min = ", \$\\le\$$min" if $min ne ""; return $min; diff --git a/bench/dtgbasat/tabl2.pl b/bench/dtgbasat/tabl2.pl index da8cfbedb..b63254a74 100755 --- a/bench/dtgbasat/tabl2.pl +++ b/bench/dtgbasat/tabl2.pl @@ -91,7 +91,7 @@ sub getlastsuccesful($$) while (my $line = ) { my @f = split(/,/, $line); - $min = $f[1] if $f[1] ne ''; + $min = $f[2] if $f[2] ne ''; } $min = ", \$\\le\$$min" if $min ne ""; return $min; diff --git a/bench/dtgbasat/tabl3.pl b/bench/dtgbasat/tabl3.pl index 636c253a8..74dd8ed38 100755 --- a/bench/dtgbasat/tabl3.pl +++ b/bench/dtgbasat/tabl3.pl @@ -93,7 +93,7 @@ sub getlastsuccesful($$) while (my $line = ) { my @f = split(/,/, $line); - $min = $f[1] if $f[1] ne ''; + $min = $f[2] if $f[2] ne ''; } $min = ", \$\\le\$$min" if $min ne ""; return $min; diff --git a/bench/dtgbasat/tabl4.pl b/bench/dtgbasat/tabl4.pl index c28179101..f2c9933a2 100755 --- a/bench/dtgbasat/tabl4.pl +++ b/bench/dtgbasat/tabl4.pl @@ -92,7 +92,7 @@ sub getlastsuccesful($$) while (my $line = ) { my @f = split(/,/, $line); - $min = $f[1] if $f[1] ne ''; + $min = $f[2] if $f[2] ne ''; } $min = ", \$\\le\$$min" if $min ne ""; return $min; diff --git a/bin/man/spot-x.x b/bin/man/spot-x.x index 3f156ec28..881265282 100644 --- a/bin/man/spot-x.x +++ b/bin/man/spot-x.x @@ -150,13 +150,14 @@ to the recurrence (or the persistence) class. \fBSPOT_SATLOG\fR If set to a filename, the SAT-based minimization routines will append statistics about each iteration to the named file. Each line lists -the following comma-separated values: requested number of states, -number of reachable states in the output, number of edges in the -output, number of transitions in the output, number of variables in -the SAT problem, number of clauses in the SAT problem, user time for -encoding the SAT problem, system time for encoding the SAT problem, -user time for solving the SAT problem, system time for solving the SAT -problem. +the following comma-separated values: input number of states, target +number of states, number of reachable states in the output, number of +edges in the output, number of transitions in the output, number of +variables in the SAT problem, number of clauses in the SAT problem, +user time for encoding the SAT problem, system time for encoding the +SAT problem, user time for solving the SAT problem, system time for +solving the SAT problem, automaton produced at this step in HOA +format. .TP \fBSPOT_SATSOLVER\fR diff --git a/doc/org/satmin.org b/doc/org/satmin.org index a91207488..88ce426fa 100644 --- a/doc/org/satmin.org +++ b/doc/org/satmin.org @@ -29,7 +29,7 @@ Let us first state a few facts about this minimization procedure. use state-based acceptance. (They simply restrict all the outgoing transitions of a state to belong to the same acceptance sets.) 4) Spot is built using PicoSAT call_version()[:results raw]. - This solver was chosen for its performances, simplicity of + This solver was chosen for its performance, simplicity of integration and license compatibility. However, it is still possible to use an external SAT solver (as described below). 5) [[file:ltl2tgba.org][=ltl2tgba=]] and [[file:dstar2tgba.org][=dstar2tgba=]] will always try to output an automaton. @@ -730,48 +730,52 @@ export SPOT_SATLOG=stats.csv ltlfilt -f 'Ga R (F!b & (c U b))' -l | ltl2dstar --ltl2nba=spin:ltl2tgba@-Ds - - | dstar2tgba -D -x sat-minimize,sat-acc=2 --stats='input(states=%S) output(states=%s, acc-sets=%a, det=%d)' +echo ==== stats.csv ==== cat stats.csv #+END_SRC #+RESULTS: : input(states=11) output(states=5, acc-sets=2, det=1) -: 9,9,36,72,44064,9043076,616,18,258,24 -: 8,7,29,56,19712,3493822,236,9,135,6 -: 6,6,25,48,10512,1362749,97,4,42,2 -: 5,,,,7200,784142,65,2,40,2 +: ==== stats.csv ==== +: input.states,target.states,reachable.states,edges,transitions,variables,clauses,enc.user,enc.sys,sat.user,sat.sys,automaton +: 10,5,,,,13600,1543042,59,3,187,0, +: 10,7,7,33,56,26656,4247441,162,7,775,0,"HOA: v1 States: 7 Start: 0 AP: 3 ""a"" ""b"" ""c"" acc-name: generalized-Buchi 2 Acceptance: 2 Inf(0)&Inf(1) properties: trans-labels explicit-labels trans-acc complete deterministic --BODY-- State: 0 [!0&!1&2] 0 {1} [!0&1] 0 {0} [!0&!1&!2] 1 {0} [0&!1&!2] 1 [0&!1&2] 2 {1} [0&1&!2] 4 [0&1&2] 4 {0} State: 1 [0&!1] 1 {0} [!0&!1&!2 | 0&1] 1 [!0&1 | !0&2] 3 {0} State: 2 [!0&!1&2] 0 {1} [!0&1] 0 {0 1} [!0&!1&!2] 1 [0&!1&2] 2 [0&!1&!2] 3 {1} [0&1] 5 {0 1} State: 3 [!1&!2] 3 [1 | 2] 3 {0} State: 4 [!0&!1&2] 0 {0 1} [!0&1] 0 {0} [!0&!1&!2] 1 [0&1] 4 {0} [0&!1&2] 5 {0} [0&!1&!2] 6 State: 5 [!0&1 | !0&2] 0 {0 1} [!0&!1&!2] 1 [0&1 | 0&2] 5 {0 1} [0&!1&!2] 6 {0} State: 6 [!0&!1&!2] 1 [!0&1&!2] 1 {0 1} [!0&1&2] 1 {1} [!0&!1&2] 3 {0 1} [0] 6 {0 1} --END--" +: 7,6,6,26,48,10512,1376507,50,0,269,0,"HOA: v1 States: 6 Start: 0 AP: 3 ""a"" ""b"" ""c"" acc-name: generalized-Buchi 2 Acceptance: 2 Inf(0)&Inf(1) properties: trans-labels explicit-labels trans-acc complete deterministic --BODY-- State: 0 [!0&!1&2] 0 {1} [!0&1] 0 {0} [!0&!1&!2] 1 [0&!1&!2] 1 {0 1} [0&!1&2] 2 {1} [0&1] 3 {0} State: 1 [t] 1 State: 2 [!0&!1&2] 0 {1} [!0&1] 0 {0} [!1&!2] 1 [0&!1&2] 2 {1} [0&1] 4 {1} State: 3 [!0&!1&2] 0 {1} [!0&1] 0 [!0&!1&!2] 1 [0&1] 3 [0&!1&2] 4 {1} [0&!1&!2] 5 {1} State: 4 [!0&!1&2 | !0&1&!2] 0 {0 1} [!0&1&2] 0 {0} [!0&!1&!2] 1 [0&1 | 0&2] 4 {0 1} [0&!1&!2] 5 State: 5 [!0&!1&!2] 1 [!0&1 | !0&2] 1 {0 1} [0] 5 {0 1} --END--" The generated CSV file use the following columns: -- the n passed to the SAT-based minimization algorithm +- =input.states=: the number of states of the reference automaton at this step +- =target.states=: the n passed to the SAT-based minimization algorithm (it means the input automaton had n+1 states) -- number of reachable states in the output of - the minimization. -- number of edges in the output -- number of transitions -- number of variables in the SAT problem -- number of clauses in the SAT problem -- user time for encoding the SAT problem -- system time for encoding the SAT problem -- user time for solving the SAT problem -- system time for solving the SAT problem -- automaton produced +- =reachable.states=: number of reachable states in the output of + the minimization (with any luck this can be smaller than =target.states=) +- =edges=, =transitions=: number of edges or transitions in the output +- =variables=, =clauses=: size of the SAT problem +- =enc.user=, =enc.sys=: user and system time for encoding the SAT problem +- =sat.user=, =sat.sys=: user and system time for solving the SAT problem +- =automaton=: the automaton produced in HOA format. -Times are measured with the times() function, and expressed -in ticks (usually: 1/100 of seconds). +Times are measured with the times() function, and expressed in ticks +(usually: 1/100 of seconds). The encoding of the automaton in the CSV +file follows RFC4180 in escaping double-quote by doubling them. -In the above example, the input DRA had 11 -states. In the first line of the =stats.csv= file, you can see the -minimization function searching for a 9 state DTBA and obtaining a -8-state solution. (Since the minimization function searched for a -9-state DTBA, it means it received a 10-state complete DTBA, so the -processings performed before the minimization procedure managed to -convert the 11-state DRA into a 10-state DTBA.) Starting from the -8-state solution, it looked for (and found) a 7-state solution, and -then a 6-state solution. The search for a 5-state complete DTBA -failed. The final output is reported with 5 states, because by -default we output trim automata. If the =--complete= option had been -given, the useless sink state would have been kept and the output -automaton would have 6 states. +In the above example, the DRA produced by =ltl2dstar= had 11 states. +In the first line of the =stats.csv= file, you can see the +minimization function had a 10-state input, which means that +=dstar2tgba= first reduced the 11-state (complete) DRA into a 10-state +(complete) DBA before calling the SAT-based minimization. This first +line shows the SAT-based minimization for a (complete) 5-state DTGBA +and failing to find one. Then on the next line it looks for a 7-state +solution, finds one. Finally, it finds a (complete) 6-state solution, +now using the 7-state version as reference automaton to further +simplify the problem. +The final output is reported with 5 states, because by default we +output trim automata. If the =--complete= option had been given, the +useless sink state would have been kept and the output automaton would +have 6 states. #+BEGIN_SRC sh :results silent :exports results rm -f output.hoa output2.hoa #+END_SRC +* Python interface + +See the [[https://spot.lrde.epita.fr/ipynb/satmin.html][=satmin.ipynb=]] notebook. diff --git a/doc/org/tut.org b/doc/org/tut.org index c0b4064c7..f290cbe91 100644 --- a/doc/org/tut.org +++ b/doc/org/tut.org @@ -82,3 +82,4 @@ real notebooks instead. - [[https://spot.lrde.epita.fr/ipynb/atva16-fig2b.html][=atva16-fig2b.ipynb=]] second example from our [[https://www.lrde.epita.fr/~adl/dl/adl/duret.16.atva2.pdf][ATVA'16 tool paper]]. - [[https://spot.lrde.epita.fr/ipynb/alternation.html][=alternation.ipynb=]] examples of alternating automata. - [[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]]. diff --git a/python/spot/__init__.py b/python/spot/__init__.py index 5c64cc104..6621d4767 100644 --- a/python/spot/__init__.py +++ b/python/spot/__init__.py @@ -33,7 +33,7 @@ from spot.aux import \ import subprocess import os import signal - +import tempfile # The parrameters used by default when show() is called on an automaton. _show_default = None @@ -927,7 +927,8 @@ for fun in ['remove_x', 'relabel', 'relabel_bse', def sat_minimize(aut, acc=None, colored=False, state_based=False, states=0, max_states=0, sat_naive=False, sat_langmap=False, - sat_incr=0, sat_incr_steps=0): + sat_incr=0, sat_incr_steps=0, + display_log=False, return_log=False): args='' if acc is not None: if type(acc) is not str: @@ -950,9 +951,25 @@ def sat_minimize(aut, acc=None, colored=False, if sat_incr: args += ',sat-incr=' + str(sat_incr) args += ',sat-incr-steps=' + str(sat_incr_steps) - from spot.impl import sat_minimize as sm - return sm(aut, args, state_based) + + if display_log or return_log: + import pandas as pd + with tempfile.NamedTemporaryFile(dir='.', suffix='.satlog') as t: + args += ',log="{}"'.format(t.name) + aut = sm(aut, args, state_based) + dfrm = pd.read_csv(t.name, dtype=object) + if display_log: + # old versions of ipython do not import display by default + from IPython.display import display + del dfrm['automaton'] + display(dfrm) + if return_log: + return aut, dfrm + else: + return aut + else: + return sm(aut, args, state_based) def parse_word(word, dic=_bdd_dict): diff --git a/spot/misc/satsolver.cc b/spot/misc/satsolver.cc index fd61b76b1..3ef31dbb8 100644 --- a/spot/misc/satsolver.cc +++ b/spot/misc/satsolver.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014, 2015, 2016, 2017 Laboratoire de Recherche et -// Développement de l'Epita. +// Copyright (C) 2013-2018 Laboratoire de Recherche et Développement +// de l'Epita. // // This file is part of Spot, a model checking library. // @@ -209,7 +209,7 @@ namespace spot return nvars_; } - std::pair satsolver::stats() + std::pair satsolver::stats() const { return std::make_pair(get_nb_vars(), get_nb_clauses()); } diff --git a/spot/misc/satsolver.hh b/spot/misc/satsolver.hh index 4a850d30b..51d931373 100644 --- a/spot/misc/satsolver.hh +++ b/spot/misc/satsolver.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013, 2017 Laboratoire de Recherche et Développement -// de l'Epita. +// Copyright (C) 2013, 2017, 2018 Laboratoire de Recherche et +// Développement de l'Epita. // // This file is part of Spot, a model checking library. // @@ -95,7 +95,7 @@ namespace spot int get_nb_vars() const; /// \brief Returns std::pair; - std::pair stats(); + std::pair stats() const; /// \brief Add a comment. /// It should be used only in debug mode after providing a satsolver. diff --git a/spot/priv/satcommon.cc b/spot/priv/satcommon.cc index 6d9e0a675..53f9a81cc 100644 --- a/spot/priv/satcommon.cc +++ b/spot/priv/satcommon.cc @@ -142,50 +142,63 @@ namespace spot return buffer.str(); } + static std::string satlog_filename; + void - print_log(timer_map& t, int target_state_number, - twa_graph_ptr& res, satsolver& solver) + set_satlog_filename(const std::string& filename) + { + satlog_filename = filename; + } + + void + print_log(timer_map& t, + int input_state_number, int target_state_number, + const twa_graph_ptr& res, const satsolver& solver) { // Always copy the environment variable into a static string, // so that we (1) look it up once, but (2) won't crash if the // environment is changed. - static std::string log = []() + static std::string envlog = []() { auto s = getenv("SPOT_SATLOG"); return s ? s : ""; }(); - if (!log.empty()) + const std::string log = satlog_filename.empty() ? envlog : satlog_filename; + if (log.empty()) + return; + + std::ofstream out(log, std::ios_base::ate | std::ios_base::app); + out.exceptions(std::ifstream::failbit | std::ifstream::badbit); + if (out.tellp() == 0) + out << + ("input.states,target.states,reachable.states,edges,transitions," + "variables,clauses,enc.user,enc.sys,sat.user,sat.sys,automaton\n"); + + const timer& te = t.timer("encode"); + const timer& ts = t.timer("solve"); + out << input_state_number << ',' << target_state_number << ','; + if (res) { - std::fstream out(log, - std::ios_base::app | std::ios_base::out); - out.exceptions(std::ifstream::failbit | std::ifstream::badbit); - const timer& te = t.timer("encode"); - const timer& ts = t.timer("solve"); - out << target_state_number << ','; - if (res) - { - twa_sub_statistics st = sub_stats_reachable(res); - out << st.states << ',' << st.edges << ',' << st.transitions; - } - else - { - out << ",,"; - } - std::pair s = solver.stats(); // sat_stats - out << ',' - << s.first << ',' << s.second << ',' - << te.utime() + te.cutime() << ',' - << te.stime() + te.cstime() << ',' - << ts.utime() + ts.cutime() << ',' - << ts.stime() + ts.cstime() << ",\""; - if (res) - { - std::ostringstream f; - print_hoa(f, res, "l"); - escape_rfc4180(out, f.str()); - } - out << "\"\n"; + twa_sub_statistics st = sub_stats_reachable(res); + out << st.states << ',' << st.edges << ',' << st.transitions; } + else + { + out << ",,"; + } + std::pair s = solver.stats(); + out << ',' << s.first << ',' << s.second << ',' + << te.utime() + te.cutime() << ',' + << te.stime() + te.cstime() << ',' + << ts.utime() + ts.cutime() << ',' + << ts.stime() + ts.cstime() << ','; + if (res) + { + std::ostringstream f; + print_hoa(f, res, "l"); + escape_rfc4180(out << '"', f.str()) << '"'; + } + out << std::endl; } int diff --git a/spot/priv/satcommon.hh b/spot/priv/satcommon.hh index 664019b35..b07d2efe6 100644 --- a/spot/priv/satcommon.hh +++ b/spot/priv/satcommon.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et +// Copyright (C) 2013-2016, 2018 Laboratoire de Recherche et // Développement de l'Epita. // // This file is part of Spot, a model checking library. @@ -231,11 +231,17 @@ public: unsigned dst_ref); }; - /// \brief Good old function that prints log is SPOT_SATLOG. It has been - /// moved from spot/twaalgos/dt*asat.cc files. - void - print_log(timer_map& t, int target_state_number, twa_graph_ptr& res, - satsolver& solver); + /// \brief Give a filename to save the log of the SAT minimization. + /// + /// This has priority over the SPOT_SATLOG environment variable. + /// Pass en empty string to reset it. + void set_satlog_filename(const std::string& filename); + + /// \brief Prints a line in the SPOT_SATLOG file. + void print_log(timer_map& t, + int input_state_number, + int target_state_number, const twa_graph_ptr& res, + const satsolver& solver); /// \brief Returns the number of distinct values containted in a vector. int diff --git a/spot/twaalgos/dtbasat.cc b/spot/twaalgos/dtbasat.cc index e765fae3d..045970f5f 100644 --- a/spot/twaalgos/dtbasat.cc +++ b/spot/twaalgos/dtbasat.cc @@ -28,7 +28,6 @@ #include #include #include -#include // If you set the SPOT_TMPKEEP environment variable the temporary // file used to communicate with the sat solver will be left in @@ -708,6 +707,7 @@ namespace spot } #endif a->merge_edges(); + a->purge_unreachable_states(); return a; } } @@ -744,7 +744,8 @@ namespace spot if (!solution.second.empty()) res = sat_build(solution.second, d, a, state_based); - print_log(t, target_state_number, res, solver); // If SPOT_SATLOG is set. + print_log(t, a->num_states(), + target_state_number, res, solver); // If SPOT_SATLOG is set. trace << "dtba_sat_synthetize(...) = " << res << '\n'; return res; @@ -754,7 +755,6 @@ namespace spot dichotomy_dtba_research(int max, dict& d, satsolver& solver, - timer_map& t1, const_twa_graph_ptr& prev, bool state_based) { @@ -768,36 +768,47 @@ namespace spot target = (max + min) / 2; trace << "min:" << min << ", max:" << max << ", target:" << target << '\n'; - + timer_map t1; + t1.start("encode"); solver.assume(d.nvars + target); + t1.stop("encode"); trace << "solver.assume(" << d.nvars + target << ")\n"; - + t1.start("solve"); satsolver::solution_pair solution = solver.get_solution(); + t1.stop("solve"); if (solution.second.empty()) { trace << "UNSAT\n"; max = target; + print_log(t1, prev->num_states(), d.cand_size - target, + nullptr, solver); } else { trace << "SAT\n"; res = sat_build(solution.second, d, prev, state_based); - min = d.cand_size - stats_reachable(res).states + 1; + min = d.cand_size - res->num_states() + 1; + print_log(t1, prev->num_states(), d.cand_size - target, + res, solver); } } trace << "End with max:" << max << ", min:" << min << '\n'; if (!res) { - trace << "All assumptions are UNSAT, let's try without..."; + trace << "All assumptions are UNSAT, let's try without...\n"; + timer_map t1; + t1.start("encode"); + t1.stop("encode"); + t1.start("solve"); + t1.stop("solve"); satsolver::solution_pair solution = solver.get_solution(); trace << (solution.second.empty() ? "UNSAT!\n" : "SAT\n"); res = solution.second.empty() ? nullptr : sat_build(solution.second, d, prev, state_based); + print_log(t1, prev->num_states(), d.cand_size - target, res, solver); } - t1.stop("solve"); - print_log(t1, d.cand_size - target, res, solver); // SPOT_SATLOG. return res ? res : std::const_pointer_cast(prev); } @@ -816,8 +827,7 @@ namespace spot const_twa_graph_ptr prev = a; dict d; - d.cand_size = (max_states < 0) ? - stats_reachable(prev).states - 1 : max_states; + d.cand_size = (max_states < 0) ? prev->num_states() - 1 : max_states; if (d.cand_size == 0) return nullptr; @@ -829,7 +839,7 @@ namespace spot while (next && d.cand_size > 0) { // Warns the satsolver of the number of assumptions. - int n_assumptions = (int) d.cand_size < sat_incr_steps ? + int n_assumptions = (int) d.cand_size <= sat_incr_steps ? d.cand_size - 1 : sat_incr_steps; trace << "number of assumptions:" << n_assumptions << '\n'; satsolver solver; @@ -867,34 +877,36 @@ namespace spot solver.add({-assume_lit, assume_lit - 1, 0}); } } - t1.stop("encode"); - - t1.start("solve"); if (n_assumptions) { trace << "solver.assume(" << d.nvars + n_assumptions << ")\n"; solver.assume(d.nvars + n_assumptions); } + t1.stop("encode"); + t1.start("solve"); satsolver::solution_pair solution = solver.get_solution(); + t1.stop("solve"); if (solution.second.empty() && n_assumptions) // UNSAT { + print_log(t1, prev->num_states(), + d.cand_size - n_assumptions, nullptr, solver); trace << "UNSAT\n"; - return dichotomy_dtba_research(n_assumptions, d, solver, t1, prev, - state_based); + return dichotomy_dtba_research(n_assumptions, d, solver, + prev, state_based); } - t1.stop("solve"); trace << "SAT, restarting from zero\n"; next = solution.second.empty() ? nullptr : sat_build(solution.second, d, prev, state_based); - print_log(t1, d.cand_size - n_assumptions, next, solver); // SPOT_SATLOG. + print_log(t1, prev->num_states(), + d.cand_size - n_assumptions, next, solver); if (next) { prev = next; d = dict(); - d.cand_size = stats_reachable(prev).states - 1; + d.cand_size = prev->num_states() - 1; if (d.cand_size == 0) next = nullptr; } @@ -912,8 +924,7 @@ namespace spot (": dtba_sat_minimize_incr() can only work with Büchi acceptance."); const_twa_graph_ptr prev = a; dict d; - d.cand_size = (max_states < 0) ? - stats_reachable(prev).states - 1 : max_states; + d.cand_size = (max_states < 0) ? prev->num_states() - 1 : max_states; if (d.cand_size == 0) return nullptr; @@ -937,7 +948,7 @@ namespace spot t1.stop("solve"); next = solution.second.empty() ? nullptr : sat_build(solution.second, d, prev, state_based); - print_log(t1, d.cand_size, next, solver); // If SPOT_SATLOG is set. + print_log(t1, prev->num_states(), d.cand_size, next, solver); trace << "First iteration done\n"; @@ -950,27 +961,27 @@ namespace spot for (int k = 0; next && d.cand_size > 0 && (naive || k < sat_incr_steps); ++k) { - t1.start("encode"); prev = next; - int reach_states = stats_reachable(prev).states; + int reach_states = prev->num_states(); cnf_comment("Next iteration: ", reach_states - 1, "\n"); - trace << "Encoding the deletion of state " << reach_states - 1 << '\n'; + timer_map t2; + t2.start("encode"); // Add new constraints. for (unsigned i = reach_states - 1; i < d.cand_size; ++i) for (unsigned l = 0; l < alpha_size; ++l) for (unsigned j = 0; j < orig_cand_size; ++j) solver.add({-d.transid(j, l, i), 0}); - + t2.stop("encode"); d.cand_size = reach_states - 1; - t1.stop("encode"); - t1.start("solve"); + t2.start("solve"); satsolver::solution_pair solution = solver.get_solution(); - t1.stop("solve"); + t2.stop("solve"); next = solution.second.empty() ? nullptr : sat_build(solution.second, d, prev, state_based); - print_log(t1, d.cand_size, next, solver); // If SPOT_SATLOG is set. + print_log(t2, prev->num_states(), + d.cand_size, next, solver); } if (next) @@ -978,7 +989,7 @@ namespace spot trace << "Starting from scratch\n"; prev = next; d = dict(); - d.cand_size = stats_reachable(prev).states - 1; + d.cand_size = prev->num_states() - 1; if (d.cand_size == 0) next = nullptr; } @@ -991,8 +1002,7 @@ namespace spot dtba_sat_minimize(const const_twa_graph_ptr& a, bool state_based, int max_states) { - int n_states = (max_states < 0) ? - stats_reachable(a).states : max_states + 1; + int n_states = (max_states < 0) ? a->num_states() : max_states + 1; twa_graph_ptr prev = nullptr; for (;;) @@ -1002,7 +1012,7 @@ namespace spot if (!next) return prev; else - n_states = stats_reachable(next).states; + n_states = next->num_states(); prev = next; } SPOT_UNREACHABLE(); @@ -1014,7 +1024,7 @@ namespace spot { trace << "Dichomoty\n"; if (max_states < 0) - max_states = stats_reachable(a).states - 1; + max_states = a->num_states() - 1; int min_states = 1; if (langmap) { @@ -1036,7 +1046,7 @@ namespace spot else { prev = next; - max_states = stats_reachable(next).states - 1; + max_states = next->num_states() - 1; } } return prev; diff --git a/spot/twaalgos/dtwasat.cc b/spot/twaalgos/dtwasat.cc index ecde78e44..62cf5a821 100644 --- a/spot/twaalgos/dtwasat.cc +++ b/spot/twaalgos/dtwasat.cc @@ -36,7 +36,6 @@ #include #include #include -#include // If you set the SPOT_TMPKEEP environment variable the temporary // file used to communicate with the sat solver will be left in @@ -624,7 +623,7 @@ namespace spot { unsigned nacc = d.cand_nacc; cnf_comment("transitions belong to exactly one of the", nacc, - "acceptance set\n"); + "acceptance sets\n"); for (unsigned l = 0; l < alpha_size; ++l) for (unsigned q1 = 0; q1 < d.cand_size; ++q1) for (unsigned q2 = 0; q2 < d.cand_size; ++q2) @@ -982,6 +981,7 @@ namespace spot #endif a->merge_edges(); + a->purge_unreachable_states(); return a; } } @@ -1023,7 +1023,7 @@ namespace spot if (!solution.second.empty()) res = sat_build(solution.second, d, a, state_based); - print_log(t, target_state_number, res, solver); // if SPOT_SATLOG is set. + print_log(t, a->num_states(), target_state_number, res, solver); trace << "dtwa_sat_synthetize(...) = " << res << '\n'; return res; @@ -1066,7 +1066,6 @@ namespace spot dichotomy_dtwa_research(int max, dict& d, satsolver& solver, - timer_map& t1, const_twa_graph_ptr& prev, bool state_based) { @@ -1081,35 +1080,46 @@ namespace spot trace << "min:" << min << ", max:" << max << ", target:" << target << '\n'; + timer_map t1; + t1.start("encode"); solver.assume(d.nvars + target); + t1.stop("encode"); trace << "solver.assume(" << d.nvars + target << ")\n"; - + t1.start("solve"); satsolver::solution_pair solution = solver.get_solution(); + t1.stop("solve"); if (solution.second.empty()) { trace << "UNSAT\n"; max = target; + print_log(t1, prev->num_states(), d.cand_size - target, + nullptr, solver); } else { trace << "SAT\n"; res = sat_build(solution.second, d, prev, state_based); - min = d.cand_size - stats_reachable(res).states + 1; + min = d.cand_size - res->num_states() + 1; + print_log(t1, prev->num_states(), d.cand_size - target, + res, solver); } } trace << "End with max:" << max << ", min:" << min << '\n'; if (!res) { - trace << "All assumptions are UNSAT, let's try without..."; + trace << "All assumptions are UNSAT, let's try without...\n"; + timer_map t1; + t1.start("encode"); + t1.stop("encode"); + t1.start("solve"); satsolver::solution_pair solution = solver.get_solution(); + t1.stop("solve"); trace << (solution.second.empty() ? "UNSAT!\n" : "SAT\n"); res = solution.second.empty() ? nullptr : sat_build(solution.second, d, prev, state_based); + print_log(t1, prev->num_states(), d.cand_size - target, res, solver); } - - t1.stop("solve"); - print_log(t1, d.cand_size - target , res, solver); // SPOT_SATLOG. return res ? res : std::const_pointer_cast(prev); } @@ -1128,8 +1138,7 @@ namespace spot const_twa_graph_ptr prev = a; dict d(prev); - d.cand_size = (max_states < 0) ? - stats_reachable(prev).states - 1 : max_states; + d.cand_size = (max_states < 0) ? prev->num_states() - 1 : max_states; d.cand_nacc = target_acc_number; d.cand_acc = target_acc; if (d.cand_size == 0) @@ -1144,9 +1153,9 @@ namespace spot while (next && d.cand_size > 0) { // Warns the satsolver of the number of assumptions. - int n_assumptions = (int) d.cand_size < sat_incr_steps ? + int n_assumptions = (int) d.cand_size <= sat_incr_steps ? d.cand_size - 1 : sat_incr_steps; - trace << "number of assumptions:" << n_assumptions << '\n'; + trace << "number of assumptions: " << n_assumptions << '\n'; satsolver solver; solver.set_nassumptions_vars(n_assumptions); @@ -1182,35 +1191,39 @@ namespace spot solver.add({-assume_lit, assume_lit - 1, 0}); } } - t1.stop("encode"); - t1.start("solve"); if (n_assumptions) { trace << "solver.assume(" << d.nvars + n_assumptions << ")\n"; solver.assume(d.nvars + n_assumptions); } + t1.stop("encode"); + t1.start("solve"); satsolver::solution_pair solution = solver.get_solution(); + t1.stop("solve"); if (solution.second.empty() && n_assumptions) // UNSAT { + print_log(t1, prev->num_states(), + d.cand_size - n_assumptions, nullptr, solver); trace << "UNSAT\n"; twa_graph_ptr res = dichotomy_dtwa_research(n_assumptions, d, solver, - t1, prev, state_based); + prev, state_based); return res == a ? nullptr : res; } - t1.stop("solve"); trace << "SAT, restarting from zero\n"; next = solution.second.empty() ? nullptr : sat_build(solution.second, d, prev, state_based); - print_log(t1, d.cand_size - n_assumptions, next, solver); // SPOT_SATLOG. + print_log(t1, prev->num_states(), + d.cand_size - n_assumptions, next, solver); if (next) { prev = next; + trace << "prev has " << prev->num_states() << '\n'; d = dict(prev); - d.cand_size = stats_reachable(prev).states - 1; + d.cand_size = prev->num_states() - 1; d.cand_nacc = target_acc_number; d.cand_acc = target_acc; if (d.cand_size == 0) @@ -1233,7 +1246,7 @@ namespace spot dict d(prev); d.cand_size = (max_states < 0) ? - stats_reachable(prev).states - 1 : max_states; + prev->num_states() - 1 : max_states; d.cand_nacc = target_acc_number; d.cand_acc = target_acc; if (d.cand_size == 0) @@ -1260,9 +1273,9 @@ namespace spot t1.stop("solve"); next = solution.second.empty() ? nullptr : sat_build(solution.second, d, prev, state_based); - print_log(t1, d.cand_size, next, solver); // If SPOT_SATLOG is set. + print_log(t1, prev->num_states(), d.cand_size, next, solver); - trace << "First iteraton done\n"; + trace << "First iteration done\n"; // Compute the AP used. bdd ap = prev->ap_vars(); @@ -1273,27 +1286,25 @@ namespace spot for (int k = 0; next && d.cand_size > 0 && (naive || k < sat_incr_steps); ++k) { - t1.start("encode"); prev = next; - int reach_states = stats_reachable(prev).states; - cnf_comment("Next iteration:", reach_states - 1, "\n"); - + int reach_states = prev->num_states(); trace << "Encoding the deletion of state " << reach_states - 1 << '\n'; - + cnf_comment("Next iteration:", reach_states - 1, "\n"); + timer_map t2; + t2.start("encode"); // Add new constraints. for (unsigned i = reach_states - 1; i < d.cand_size; ++i) for (unsigned l = 0; l < alpha_size; ++l) for (unsigned j = 0; j < orig_cand_size; ++j) solver.add({-d.transid(j, l, i), 0}); - + t2.stop("encode"); d.cand_size = reach_states - 1; - t1.stop("encode"); - t1.start("solve"); + t2.start("solve"); solution = solver.get_solution(); - t1.stop("solve"); + t2.stop("solve"); next = solution.second.empty() ? nullptr : sat_build(solution.second, d, prev, state_based); - print_log(t1, d.cand_size, next, solver); // If SPOT_SATLOG is set. + print_log(t2, prev->num_states(), d.cand_size, next, solver); } if (next) @@ -1301,7 +1312,7 @@ namespace spot trace << "Starting from scratch\n"; prev = next; d = dict(prev); - d.cand_size = stats_reachable(prev).states - 1; + d.cand_size = prev->num_states() - 1; d.cand_nacc = target_acc_number; d.cand_acc = target_acc; if (d.cand_size == 0) @@ -1320,8 +1331,7 @@ namespace spot bool state_based, int max_states, bool colored) { - int n_states = (max_states < 0) ? - stats_reachable(a).states : max_states + 1; + int n_states = (max_states < 0) ? a->num_states() : max_states + 1; twa_graph_ptr prev = nullptr; for (;;) @@ -1333,7 +1343,7 @@ namespace spot if (!next) return prev; else - n_states = stats_reachable(next).states; + n_states = next->num_states(); prev = next; } SPOT_UNREACHABLE(); @@ -1348,7 +1358,7 @@ namespace spot { trace << "Dichotomy\n"; if (max_states < 1) - max_states = stats_reachable(a).states - 1; + max_states = a->num_states() - 1; int min_states = 1; if (langmap) { @@ -1373,7 +1383,7 @@ namespace spot else { prev = next; - max_states = stats_reachable(next).states - 1; + max_states = next->num_states() - 1; } } return prev; @@ -1401,10 +1411,10 @@ namespace spot bool sat_langmap = om.get("sat-langmap", 0); int states = om.get("states", -1); int max_states = om.get("max-states", -1); - auto accstr = om.get_str("acc"); + std::string accstr = om.get_str("acc"); bool colored = om.get("colored", 0); int preproc = om.get("preproc", 3); - + set_satlog_filename(om.get_str("log")); // Set default sat-incr-steps value if not provided and used. if (sat_incr == 1 && !sat_incr_steps) // Assume @@ -1551,7 +1561,7 @@ namespace spot if (a) { - if (state_based) + if (state_based || colored) a = scc_filter_states(a); else a = scc_filter(a); diff --git a/spot/twaalgos/dtwasat.hh b/spot/twaalgos/dtwasat.hh index 1399d9b05..ac5837741 100644 --- a/spot/twaalgos/dtwasat.hh +++ b/spot/twaalgos/dtwasat.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et +// Copyright (C) 2013, 2014, 2015, 2018 Laboratoire de Recherche et // Développement de l'Epita. // // This file is part of Spot, a model checking library. @@ -140,6 +140,7 @@ namespace spot /// fixed number of states before starting from scratch /// incr < 0 // use satsolver incrementally, never restart /// colored = 1 // build a colored TωA + /// log = "filename" /// SPOT_API twa_graph_ptr sat_minimize(twa_graph_ptr aut, const char* opt, bool state_based = false); diff --git a/tests/Makefile.am b/tests/Makefile.am index 9cb4ac44b..68d171743 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -342,6 +342,7 @@ TESTS_ipython = \ python/product.ipynb \ python/randaut.ipynb \ python/randltl.ipynb \ + python/satmin.ipynb \ python/stutter-inv.ipynb \ python/testingaut.ipynb \ python/word.ipynb diff --git a/tests/python/ipnbdoctest.py b/tests/python/ipnbdoctest.py index 307cfccf1..3f3bab32f 100755 --- a/tests/python/ipnbdoctest.py +++ b/tests/python/ipnbdoctest.py @@ -118,6 +118,10 @@ def canonicalize(s, type, ignores): # Different Pandas versions produce different CSS styles (when there is a # style). s = re.sub(r'.*\n', '', s, flags=re.DOTALL) + # Table that contains enc.user are log from the SAT-solver. They contain + # timing result we cannot compare between runs. + s = re.sub(r'', '
', s, + flags=re.DOTALL) for n, p in enumerate(ignores): s = re.sub(p, 'IGN{}'.format(n), s) @@ -134,8 +138,11 @@ def canonical_dict(dict, ignores): dict['text'] = canonicalize(dict['text'], 'text', ignores) if 'data' in dict: - for k in dict['data']: - dict['data'][k] = canonicalize(dict['data'][k], k, ignores) + d = dict['data'] + if "text/html" in d and "text/plain" in d: + del d["text/plain"] + for k in d: + d[k] = canonicalize(d[k], k, ignores) if ('ename' in dict and dict['ename'] == 'SystemExit' and dict['evalue'] == '77'): diff --git a/tests/python/satmin.ipynb b/tests/python/satmin.ipynb new file mode 100644 index 000000000..9958a18d4 --- /dev/null +++ b/tests/python/satmin.ipynb @@ -0,0 +1,4819 @@ +{ + "cells": [ + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "# SAT-based minimization of deterministic ω-automata\n", + "\n", + "The `spot.sat_minimize()` Python function is the main entry point for minimizing any **deterministic** ω-automaton. This notebook demonstrates how to use that function.\n", + "\n", + "**Warning:** while the automata used in this notebook are quite small, working with large automata can require a lot of RAM and take huge amount of time. In its most straightforward variant, `sat_minimize()` takes a input automaton (called *reference*) and then makes a loop to ask a SAT-solver for an equivalent automaton (called *candidate*) with 1 fewer state at each iteration. If the reference has size ($n_i$, $s_i$), i.e. $n_i$ states, $s_i$ acceptance sets, and the candidate has size $(n_o, s_o)$, the SAT encoding uses $\\mathrm{O}(n_i^2\\times n_o^2\\times 2^{s_i+s_o})$ variables and $\\mathrm{O}(n_i^2 \\times n_o^3\\times 2^{s_i+2s_o}\\times |\\Sigma|)$ clauses. Reducing the number of acceptance set the therefore the most important way to simplify a problem." + ] + }, + { + "cell_type": "code", + "execution_count": 1, + "metadata": {}, + "outputs": [], + "source": [ + "import spot\n", + "spot.setup(show_default='.b')\n", + "from IPython.display import display" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "## Minimizing DBA\n", + "\n", + "Let's take a simple formula and translate it into a DBA:" + ] + }, + { + "cell_type": "code", + "execution_count": 2, + "metadata": {}, + "outputs": [ + { + "data": { + "text/latex": [ + "$\\mathsf{G} \\mathsf{F} (a \\leftrightarrow \\mathsf{X} \\mathsf{X} b)$" + ], + "text/plain": [ + "GF(a <-> XXb)" + ] + }, + "execution_count": 2, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "f = spot.formula('GF(a <-> XXb)'); f" + ] + }, + { + "cell_type": "code", + "execution_count": 3, + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "Inf(\n", + "⓿\n", + ")\n", + "[Büchi]\n", + "\n", + "\n", + "\n", + "6\n", + "\n", + "6\n", + "⓿\n", + "\n", + "\n", + "\n", + "I->6\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "6->0\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "6->1\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "\n", + "0->4\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "5\n", + "\n", + "5\n", + "\n", + "\n", + "\n", + "0->5\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "\n", + "4->6\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "4->5\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "\n", + "5->6\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "5->2\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "5->3\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "\n", + "2->6\n", + "\n", + "\n", + "!b\n", + "\n", + "\n", + "\n", + "2->4\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "2->5\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", + "\n", + "3->6\n", + "\n", + "\n", + "!b\n", + "\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x14faa9c91bd0> >" + ] + }, + "execution_count": 3, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "aut = f.translate('det', 'BA'); aut" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "The above automaton is not minimal and is easily reduced by `sat_minimize()`:" + ] + }, + { + "cell_type": "code", + "execution_count": 4, + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "G\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", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!a & b\n", + "⓿\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "a & b\n", + "⓿\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "!b\n", + "⓿\n", + "\n", + "\n", + "\n", + "2->0\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "\n", + "2->0\n", + "\n", + "\n", + "!a & b\n", + "⓿\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "a & b\n", + "⓿\n", + "\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "!a & !b\n", + "⓿\n", + "\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "a & !b\n", + "⓿\n", + "\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x14faa9f5fe70> >" + ] + }, + "execution_count": 4, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "spot.sat_minimize(aut)" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Note that by default SAT-minimize produces a transition-based automaton with the same acceptance condition. State-based acceptance can be requested with the `state_based` option:" + ] + }, + { + "cell_type": "code", + "execution_count": 5, + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "G\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", + "!a & b\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "⓿\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a | !b\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "5\n", + "\n", + "5\n", + "\n", + "\n", + "\n", + "1->5\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "\n", + "2->0\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "2->5\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "\n", + "5->0\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", + "\n", + "5->1\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "5->3\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "\n", + "5->4\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "3->1\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "3->5\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", + "\n", + "4->0\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "\n", + "4->1\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "4->3\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x14faa9c9fa20> >" + ] + }, + "execution_count": 5, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "spot.sat_minimize(aut, state_based=True)" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "## Minimizing deterministic ω-automata with arbitrary acceptance condition\n", + "\n", + "Now let's look at examples with more complicated acceptance conditions. \n", + "The following Rabin automaton was produced using ltl2dstar 0.5.4 and spot 2.5.2 with\n", + "```\n", + "ltlfilt --lbt -f '(FGa | Fb) & FGc' | ltl2dstar -H --ltl2nba=spin:ltl2tgba@-Ds - -\n", + "```\n", + "however we hardcode it so that the notebook can be used even with `ltl2dstar` installed." + ] + }, + { + "cell_type": "code", + "execution_count": 6, + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "(Fin(\n", + "⓿\n", + ") & Inf(\n", + "❶\n", + ")) | (Fin(\n", + "❷\n", + ") & Inf(\n", + "❸\n", + "))\n", + "[Rabin 2]\n", + "\n", + "\n", + "\n", + "5\n", + "\n", + "5\n", + "⓿\n", + "❷\n", + "\n", + "\n", + "\n", + "I->5\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "5->5\n", + "\n", + "\n", + "(!a & !b) | (!b & !c)\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "⓿\n", + "❷\n", + "\n", + "\n", + "\n", + "5->4\n", + "\n", + "\n", + "b & !c\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "❶\n", + "❷\n", + "\n", + "\n", + "\n", + "5->2\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "❶\n", + "❷\n", + "\n", + "\n", + "\n", + "5->3\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "❶\n", + "❸\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & c\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "⓿\n", + "❸\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!a & c\n", + "\n", + "\n", + "\n", + "0->4\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "1->4\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "4->2\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "2->4\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "3->5\n", + "\n", + "\n", + "(!a & !b) | (!b & !c)\n", + "\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "a & b & c\n", + "\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "(!a & b) | (b & !c)\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x14faa9c9f690> >" + ] + }, + "execution_count": 6, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "large = spot.automaton('''\n", + "HOA: v1 States: 6 properties: implicit-labels trans-labels no-univ-branch\n", + "deterministic complete stutter-invariant tool: \"ltl2dstar\" \"0.5.4\"\n", + "name: \"& | F G a F b F G c\" comment: \"Safra[NBA=4]\" acc-name: Rabin 2\n", + "Acceptance: 4 (Fin(0)&Inf(1))|(Fin(2)&Inf(3)) Start: 5 AP: 3 \"a\" \"b\"\n", + "\"c\" --BODY-- State: 0 {1 3} 4 4 4 4 1 0 1 0 State: 1 {0 3} 4 4 4 4 1 1\n", + "1 1 State: 2 {1 2} 4 4 4 4 2 2 2 2 State: 3 {1 2} 5 5 4 4 5 3 4 0 State:\n", + "4 {0 2} 4 4 4 4 2 2 2 2 State: 5 {0 2} 5 5 4 4 5 3 2 2 --END--''')\n", + "large.merge_edges()\n", + "large" + ] + }, + { + "cell_type": "code", + "execution_count": 7, + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "HOA: v1\n", + "name: \"& | F G a F b F G c\"\n", + "States: 6\n", + "Start: 5\n", + "AP: 3 \"a\" \"c\" \"b\"\n", + "acc-name: Rabin 2\n", + "Acceptance: 4 (Fin(0) & Inf(1)) | (Fin(2) & Inf(3))\n", + "properties: trans-labels explicit-labels state-acc complete\n", + "properties: deterministic stutter-invariant\n", + "--BODY--\n", + "State: 0 {1 3}\n", + "[0&1] 0\n", + "[!0&1] 1\n", + "[!1] 4\n", + "State: 1 {0 3}\n", + "[1] 1\n", + "[!1] 4\n", + "State: 2 {1 2}\n", + "[1] 2\n", + "[!1] 4\n", + "State: 3 {1 2}\n", + "[0&1&2] 0\n", + "[0&1&!2] 3\n", + "[!0&2 | !1&2] 4\n", + "[!0&!2 | !1&!2] 5\n", + "State: 4 {0 2}\n", + "[1] 2\n", + "[!1] 4\n", + "State: 5 {0 2}\n", + "[1&2] 2\n", + "[0&1&!2] 3\n", + "[!1&2] 4\n", + "[!0&!2 | !1&!2] 5\n", + "--END--\n" + ] + } + ], + "source": [ + "print(large.to_str())" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "It can be minimized as a 2-state transition-based Rabin:" + ] + }, + { + "cell_type": "code", + "execution_count": 8, + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "(Fin(\n", + "⓿\n", + ") & Inf(\n", + "❶\n", + ")) | (Fin(\n", + "❷\n", + ") & Inf(\n", + "❸\n", + "))\n", + "[Rabin 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 & !b & c\n", + "❷\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & !c\n", + "⓿\n", + "❷\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & !b & c\n", + "❸\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & !c\n", + "⓿\n", + "❷\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & c\n", + "❶\n", + "❸\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!c\n", + "⓿\n", + "❷\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & !b & c\n", + "❶\n", + "❷\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "(!a & c) | (b & c)\n", + "❶\n", + "❸\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x14faa9c9f480> >" + ] + }, + "execution_count": 8, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "small = spot.sat_minimize(large); small" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Or as a 4-state state-based Rabin:" + ] + }, + { + "cell_type": "code", + "execution_count": 9, + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "(Fin(\n", + "⓿\n", + ") & Inf(\n", + "❶\n", + ")) | (Fin(\n", + "❷\n", + ") & Inf(\n", + "❸\n", + "))\n", + "[Rabin 2]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "⓿\n", + "❷\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "(!a & !b) | (!b & !c)\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "❷\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "⓿\n", + "❸\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "b & !c\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "❶\n", + "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!a & b & !c\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a | !b | c\n", + "\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "(!a & !b) | (!b & !c)\n", + "\n", + "\n", + "\n", + "3->1\n", + "\n", + "\n", + "b & !c\n", + "\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x14faa9cbc060> >" + ] + }, + "execution_count": 9, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "spot.sat_minimize(large, state_based=True)" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "But do we really need 2 rabin pairs? Let's ask if we can get an equivalent with only one pair. (Note that reducing the number of pairs might require more state, but the `sat_minimize()` function will never attempt to add state unless explicitely instructed to do so. In this case we are therefore looking for a state-based Rabin-1 automaton with at most 4 states.)" + ] + }, + { + "cell_type": "code", + "execution_count": 10, + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "Fin(\n", + "⓿\n", + ") & Inf(\n", + "❶\n", + ")\n", + "[Rabin 1]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "⓿\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "(!a & !b) | (!b & !c)\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "❶\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "(!a & b) | (b & c)\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "❶\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "⓿\n", + "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "2->0\n", + "\n", + "\n", + "(!a & !b) | (!b & !c)\n", + "\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "b & !c\n", + "\n", + "\n", + "\n", + "3->1\n", + "\n", + "\n", + "!a | b | c\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x14faa9cbc720> >" + ] + }, + "execution_count": 10, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "spot.sat_minimize(large, state_based=True, acc='Rabin 1')" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Using the `display_log` option, we can have a hint of what is going on under the hood. Each line in the table shows one call to the SAT solver. The column labeled `target.states` gives the size of the equivalent automaton we ask the SAT-solver to produce, but some of these states may actually be unreachable in the result. The `variables` and `clauses` columns give an indication of the size of the SAT problem. The `enc.*` and `sat.*` columns give the user and system time taken to encode and solve the SAT problem (the unit is \"ticks\", which usually is 1/100 of seconds).\n", + "\n", + "Below we see that the minimization procedure first tried to squeeze the 6-state input into a 3-state automaton, which failed, and then into a 5-state automaton, which was successful. This 5-state automaton was used as input to produce a smaller 4-state automaton.. Essentially this procedure is doing a binary search towards the minimal size. \n", + "\n", + "(In this case it does not matter, but be aware that the number of states displayed in the log table are those of complete automata, while the output of `sat_minimize()` is trimmed by default.)" + ] + }, + { + "cell_type": "code", + "execution_count": 11, + "metadata": {}, + "outputs": [ + { + "data": { + "text/html": [ + "
\n", + "\n", + "\n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + "
input.statestarget.statesreachable.statesedgestransitionsvariablesclausesenc.userenc.syssat.usersat.sys
063NaNNaNNaN14287343058010
1655164039603363072681180
25441232200811637292040
\n", + "
" + ], + "text/plain": [ + " input.states target.states reachable.states edges transitions variables \\\n", + "0 6 3 NaN NaN NaN 1428 \n", + "1 6 5 5 16 40 3960 \n", + "2 5 4 4 12 32 2008 \n", + "\n", + " clauses enc.user enc.sys sat.user sat.sys \n", + "0 73430 58 0 1 0 \n", + "1 336307 268 1 18 0 \n", + "2 116372 92 0 4 0 " + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "Fin(\n", + "⓿\n", + ") & Inf(\n", + "❶\n", + ")\n", + "[Rabin 1]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "⓿\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "(!a & !b) | (!b & !c)\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "❶\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "(!a & b) | (b & c)\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "❶\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "⓿\n", + "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "2->0\n", + "\n", + "\n", + "(!a & !b) | (!b & !c)\n", + "\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "b & !c\n", + "\n", + "\n", + "\n", + "3->1\n", + "\n", + "\n", + "!a | b | c\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x14faae293780> >" + ] + }, + "execution_count": 11, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "spot.sat_minimize(large, state_based=True, acc='Rabin 1', display_log=True)" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Note that we already had a smaller transition-based automaton for this language (in the `small` variable), and that it actually is more efficient to work from that, as seen in problem sizes displayed in the following log." + ] + }, + { + "cell_type": "code", + "execution_count": 12, + "metadata": {}, + "outputs": [ + { + "data": { + "text/html": [ + "
\n", + "\n", + "\n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + "
input.statestarget.statesreachable.statesedgestransitionsvariablesclausesenc.userenc.syssat.usersat.sys
023NaNNaNNaN4832447020000
12551640133511118788030
224412328565733246010
\n", + "
" + ], + "text/plain": [ + " input.states target.states reachable.states edges transitions variables \\\n", + "0 2 3 NaN NaN NaN 483 \n", + "1 2 5 5 16 40 1335 \n", + "2 2 4 4 12 32 856 \n", + "\n", + " clauses enc.user enc.sys sat.user sat.sys \n", + "0 24470 20 0 0 0 \n", + "1 111187 88 0 3 0 \n", + "2 57332 46 0 1 0 " + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "Fin(\n", + "⓿\n", + ") & Inf(\n", + "❶\n", + ")\n", + "[Rabin 1]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "❶\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "⓿\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "(!a & !b) | (!b & !c)\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "❶\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "(!a & b) | (b & c)\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "⓿\n", + "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!b & c\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!b & !c\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "b & !c\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "b | c\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "!b & !c\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x14faae293d20> >" + ] + }, + "execution_count": 12, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "spot.sat_minimize(small, state_based=True, acc='Rabin 1', display_log=True)" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "How did the procedure look for a complete automaton of size 5 when the input had only 2 states? It's because the input uses transition-based acceptance: to estimate an upper bound of the size of the state-based output, the `sat_minimize()` procedure converted its transition-based input to state-based acceptance (using the `spot.sbacc()` function) and counted the number of states in the result.\n", + "\n", + "Such an estimate is not necessarily correct of we request a different acceptance condition. In that case We can actually change the upper-bound using `max_states`. Below we additionally demonstrate the use of the `colored` option, to request all transition to belong to exactly one set, as customary in parity automata." + ] + }, + { + "cell_type": "code", + "execution_count": 13, + "metadata": {}, + "outputs": [ + { + "data": { + "text/html": [ + "
\n", + "\n", + "\n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + "
input.statestarget.statesreachable.statesedgestransitionsvariablesclausesenc.userenc.syssat.usersat.sys
0255184030504370374411161
12226164882844929000
221NaNNaNNaN6812851000
\n", + "
" + ], + "text/plain": [ + " input.states target.states reachable.states edges transitions variables \\\n", + "0 2 5 5 18 40 3050 \n", + "1 2 2 2 6 16 488 \n", + "2 2 1 NaN NaN NaN 68 \n", + "\n", + " clauses enc.user enc.sys sat.user sat.sys \n", + "0 437037 441 1 16 1 \n", + "1 28449 29 0 0 0 \n", + "2 1285 1 0 0 0 " + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "Fin(\n", + "⓿\n", + ") & (Inf(\n", + "❶\n", + ") | Fin(\n", + "❷\n", + "))\n", + "[parity min odd 3]\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 & !b) | (!b & !c)\n", + "⓿\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & !b & c\n", + "❶\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & !c\n", + "⓿\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b & c\n", + "❶\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!c\n", + "⓿\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "c\n", + "❶\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x14faae293cf0> >" + ] + }, + "execution_count": 13, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "spot.sat_minimize(small, max_states=9, acc='parity min odd 3', colored=True, display_log=True)" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "There are a couple of ways in which we can influence the search for the minimum automaton. We can disable the binary search with `sat_naive`. In this case, the procedure will try to remove one state at a time. This is not necessary slower than the default binary search, because satisfiable problems are often solved more quickly than unsatisfiable ones." + ] + }, + { + "cell_type": "code", + "execution_count": 14, + "metadata": {}, + "outputs": [ + { + "data": { + "text/html": [ + "
\n", + "\n", + "\n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + "
input.statestarget.statesreachable.statesedgestransitionsvariablesclausesenc.userenc.syssat.usersat.sys
066619483894258719148150
16551540200510630262010
254411326762463214000
343NaNNaNNaN363105537000
\n", + "
" + ], + "text/plain": [ + " input.states target.states reachable.states edges transitions variables \\\n", + "0 6 6 6 19 48 3894 \n", + "1 6 5 5 15 40 2005 \n", + "2 5 4 4 11 32 676 \n", + "3 4 3 NaN NaN NaN 363 \n", + "\n", + " clauses enc.user enc.sys sat.user sat.sys \n", + "0 258719 148 1 5 0 \n", + "1 106302 62 0 1 0 \n", + "2 24632 14 0 0 0 \n", + "3 10553 7 0 0 0 " + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "Fin(\n", + "⓿\n", + ")\n", + "[co-Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "⓿\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!b\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "(!a & b) | (b & c)\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "⓿\n", + "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "(!a & !b) | (!b & !c)\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "(!a & b) | (b & c)\n", + "\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "b | c\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "!b & !c\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x14faae293e70> >" + ] + }, + "execution_count": 14, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "spot.sat_minimize(large, acc='co-Buchi', sat_naive=True, state_based=True, display_log=True)" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "## Variant for incremental SAT solving\n", + "\n", + "Using `sat_incr=1`, we encode the problem of finding an equivalent automaton with $n$ states, and add 6 additional variables and some additional constraints to the problem:\n", + "\n", + "| variable | implied constraints |\n", + "| :--- | ---: |\n", + "| $v_1$ | transitions to state $(n-1)$ must not be used | \n", + "| $v_2$ | $v_1\\land{}$ transitions to state $(n-2)$ must not be used |\n", + "| ... | |\n", + "| $v_6$ | $v_5\\land{}$ transitions to state $(n-5)$ must not be used |\n", + "\n", + "Now using `assume` directives on variable $v_i$ amounts to testing whether the problem is solved with $n-i$ states, but we do not have to reencode the problem for each test, and the solver can (probably) reuse some of the knowledge it gathered during a previous attempt. We do a binary search on these 6 assumptions, to find some $i$ such that the problem is satisfiable with assumption $v_i$ but not with $v_{i+1}$. If such cast exists, we have found the minimal automaton. If assumption $v_6$ is satisfiable, we re-encode the problem with $n-7$ states and start over. Watch how the number of variables and clauses do not change in the following log.\n", + "\n", + "The number of assumption variables to use in a one encoding can be set with the `sat_incr_steps` argument. Its default value of 6 was chosen empirically by benchmarking different values." + ] + }, + { + "cell_type": "code", + "execution_count": 15, + "metadata": {}, + "outputs": [ + { + "data": { + "text/html": [ + "
\n", + "\n", + "\n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + "
input.statestarget.statesreachable.statesedgestransitionsvariablesclausesenc.userenc.syssat.usersat.sys
061NaNNaNNaN3899258963151130
163NaNNaNNaN38992589630000
2644113238992589630010
\n", + "
" + ], + "text/plain": [ + " input.states target.states reachable.states edges transitions variables \\\n", + "0 6 1 NaN NaN NaN 3899 \n", + "1 6 3 NaN NaN NaN 3899 \n", + "2 6 4 4 11 32 3899 \n", + "\n", + " clauses enc.user enc.sys sat.user sat.sys \n", + "0 258963 151 1 3 0 \n", + "1 258963 0 0 0 0 \n", + "2 258963 0 0 1 0 " + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "Fin(\n", + "⓿\n", + ")\n", + "[co-Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "⓿\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "(!a & !b) | (!b & !c)\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!a & b & !c\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "⓿\n", + "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "(a & b) | (b & c)\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "(!a & !b) | (!b & !c)\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "a | !b | c\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "!a & b & !c\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x14faae293ed0> >" + ] + }, + "execution_count": 15, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "spot.sat_minimize(large, acc='co-Buchi', sat_incr=1, state_based=True, display_log=True)" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Another incremental variant consists is the equivalent of forcing $v_1$, $v_2$, ... in order. But to do that we do not need to use any assumption. We just add the constraints that transitions going to state $n-i$ are forbidden. This variant is enabled by option `sat_incr=2`. As in the previous case, we do a few of those incremental steps (2 by default, but that can be changed with the `sat_incr_steps` parameter) and then we reencode the problem to reduce its size.\n", + "\n", + "In the log below, line 0 corresponds to the search of an equivalent automaton with the same size, but the simpler co-Büchi acceptance. It works, and most of the time was spent encoding the problem. Then for the next two lines, the minimization function looks for automata of size 5 and 4 without reencoding the problem but simply adding a few constraints to disable the relevant transitions." + ] + }, + { + "cell_type": "code", + "execution_count": 16, + "metadata": {}, + "outputs": [ + { + "data": { + "text/html": [ + "
\n", + "\n", + "\n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + "
input.statestarget.statesreachable.statesedgestransitionsvariablesclausesenc.userenc.syssat.usersat.sys
066619483894258719150050
1655144038942587670000
2544103238942588150000
343NaNNaNNaN363103256010
\n", + "
" + ], + "text/plain": [ + " input.states target.states reachable.states edges transitions variables \\\n", + "0 6 6 6 19 48 3894 \n", + "1 6 5 5 14 40 3894 \n", + "2 5 4 4 10 32 3894 \n", + "3 4 3 NaN NaN NaN 363 \n", + "\n", + " clauses enc.user enc.sys sat.user sat.sys \n", + "0 258719 150 0 5 0 \n", + "1 258767 0 0 0 0 \n", + "2 258815 0 0 0 0 \n", + "3 10325 6 0 1 0 " + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "Fin(\n", + "⓿\n", + ")\n", + "[co-Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "⓿\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "(!a & !b) | (!b & !c)\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "⓿\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "(!a & !c) | (!b & !c)\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "c | (a & b)\n", + "\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "(!a & !b) | (!b & !c)\n", + "\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x14faae26a120> >" + ] + }, + "execution_count": 16, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "spot.sat_minimize(large, acc='co-Buchi', sat_incr=2, state_based=True, display_log=True)" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "## Miscellaneous options\n", + "\n", + "### `return_log`\n", + "\n", + "The `return_log` can be used to obtain the log table as an object. In that case, `sat_minimize()` returns a pair, `(aut,log)` where `aut` can be `None` if the minimization failed. Also, the `log` table contains an extra column that is hidden by `display_log`: it contains the corresponding automaton in HOA format." + ] + }, + { + "cell_type": "code", + "execution_count": 17, + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "Fin(\n", + "⓿\n", + ")\n", + "[co-Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "⓿\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "(!a & !b) | (!b & !c)\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "⓿\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "(!a & !c) | (!b & !c)\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "c | (a & b)\n", + "\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "(!a & !b) | (!b & !c)\n", + "\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x14faae293b40> >" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/html": [ + "
\n", + "\n", + "\n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + "
input.statestarget.statesreachable.statesedgestransitionsvariablesclausesenc.userenc.syssat.usersat.sysautomaton
066619483894258719150250HOA: v1 States: 6 Start: 0 AP: 3 \"a\" \"c\" \"b\" a...
1655144038942587670010HOA: v1 States: 5 Start: 0 AP: 3 \"a\" \"c\" \"b\" a...
2544103238942588150000HOA: v1 States: 4 Start: 0 AP: 3 \"a\" \"c\" \"b\" a...
343NaNNaNNaN363103257000NaN
\n", + "
" + ], + "text/plain": [ + " input.states target.states reachable.states edges transitions variables \\\n", + "0 6 6 6 19 48 3894 \n", + "1 6 5 5 14 40 3894 \n", + "2 5 4 4 10 32 3894 \n", + "3 4 3 NaN NaN NaN 363 \n", + "\n", + " clauses enc.user enc.sys sat.user sat.sys \\\n", + "0 258719 150 2 5 0 \n", + "1 258767 0 0 1 0 \n", + "2 258815 0 0 0 0 \n", + "3 10325 7 0 0 0 \n", + "\n", + " automaton \n", + "0 HOA: v1 States: 6 Start: 0 AP: 3 \"a\" \"c\" \"b\" a... \n", + "1 HOA: v1 States: 5 Start: 0 AP: 3 \"a\" \"c\" \"b\" a... \n", + "2 HOA: v1 States: 4 Start: 0 AP: 3 \"a\" \"c\" \"b\" a... \n", + "3 NaN " + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "aut, log = spot.sat_minimize(large, acc='co-Buchi', sat_incr=2, state_based=True, return_log=True)\n", + "display(aut)\n", + "display(log)" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Here is how we can extract the automata from that log:" + ] + }, + { + "cell_type": "code", + "execution_count": 18, + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "automaton from line 0:\n" + ] + }, + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "Fin(\n", + "⓿\n", + ")\n", + "[co-Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "⓿\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "(!a & !b) | (!b & !c)\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "⓿\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "⓿\n", + "\n", + "\n", + "\n", + "0->4\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "c | (a & b)\n", + "\n", + "\n", + "\n", + "5\n", + "\n", + "5\n", + "\n", + "\n", + "\n", + "2->5\n", + "\n", + "\n", + "(!a & !c) | (!b & !c)\n", + "\n", + "\n", + "\n", + "4->0\n", + "\n", + "\n", + "!a & !b & c\n", + "\n", + "\n", + "\n", + "4->2\n", + "\n", + "\n", + "(!a & b) | (b & !c)\n", + "\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "!b & !c\n", + "\n", + "\n", + "\n", + "4->5\n", + "\n", + "\n", + "a & b & c\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "4->3\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "5->2\n", + "\n", + "\n", + "(!a & !c) | (b & !c)\n", + "\n", + "\n", + "\n", + "5->1\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "\n", + "5->5\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "b & !c\n", + "\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "(!a & !b) | (!b & !c)\n", + "\n", + "\n", + "\n", + "3->5\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x14faae26a270> >" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "name": "stdout", + "output_type": "stream", + "text": [ + "automaton from line 1:\n" + ] + }, + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "Fin(\n", + "⓿\n", + ")\n", + "[co-Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "⓿\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "(!a & !b) | (!b & !c)\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "⓿\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "⓿\n", + "\n", + "\n", + "\n", + "0->4\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "(!a & !c) | (!b & !c)\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "c | (a & b)\n", + "\n", + "\n", + "\n", + "4->0\n", + "\n", + "\n", + "!a & !b & c\n", + "\n", + "\n", + "\n", + "4->2\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "!b & !c\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "4->3\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "(!a & !b) | (!b & !c)\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x14faae26a300> >" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "name": "stdout", + "output_type": "stream", + "text": [ + "automaton from line 2:\n" + ] + }, + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "Fin(\n", + "⓿\n", + ")\n", + "[co-Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "⓿\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "(!a & !b) | (!b & !c)\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "⓿\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "(!a & !c) | (!b & !c)\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "c | (a & b)\n", + "\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "(!a & !b) | (!b & !c)\n", + "\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x14faae26a1e0> >" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "for line, data in log.iterrows():\n", + " if type(data.automaton) is str:\n", + " print(\"automaton from line {}:\".format(line))\n", + " display(spot.automaton(data.automaton + \"\\n\"))" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "## `sat_langmap`\n", + "\n", + "When using the default binary search approach, the `sat_langmap=True` can help refine the lower bound by first testing the language-equivalence of all states in the automaton. This allows to form equivalence classes of states, and clearly the minimal automaton needs at least as many states as the number of equivalence states.\n", + "\n", + "For instance in the `large` automaton we use as example, the 6 states correspond to only two different languages. This can be seen with the `highlight_language()` function, which colors states with identical languages. This information can be used by the minimization function to search a minimal automaton between 2 and 6 states." + ] + }, + { + "cell_type": "code", + "execution_count": 19, + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "(Fin(\n", + "⓿\n", + ") & Inf(\n", + "❶\n", + ")) | (Fin(\n", + "❷\n", + ") & Inf(\n", + "❸\n", + "))\n", + "[Rabin 2]\n", + "\n", + "\n", + "\n", + "5\n", + "\n", + "5\n", + "⓿\n", + "❷\n", + "\n", + "\n", + "\n", + "I->5\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "5->5\n", + "\n", + "\n", + "(!a & !b) | (!b & !c)\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "⓿\n", + "❷\n", + "\n", + "\n", + "\n", + "5->4\n", + "\n", + "\n", + "b & !c\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "❶\n", + "❷\n", + "\n", + "\n", + "\n", + "5->2\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "❶\n", + "❷\n", + "\n", + "\n", + "\n", + "5->3\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "❶\n", + "❸\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & c\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "⓿\n", + "❸\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!a & c\n", + "\n", + "\n", + "\n", + "0->4\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "1->4\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "4->2\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "2->4\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "3->5\n", + "\n", + "\n", + "(!a & !b) | (!b & !c)\n", + "\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "a & b & c\n", + "\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "(!a & b) | (b & !c)\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x14faa9c9f690> >" + ] + }, + "execution_count": 19, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "spot.highlight_languages(large); large" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Compare the next two logs, with and without `sat_langmap`." + ] + }, + { + "cell_type": "code", + "execution_count": 20, + "metadata": {}, + "outputs": [ + { + "data": { + "text/html": [ + "
\n", + "\n", + "\n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + "
input.statestarget.statesreachable.statesedgestransitionsvariablesclausesenc.userenc.syssat.usersat.sys
063NaNNaNNaN9753291220100
16541032270515025787020
\n", + "
" + ], + "text/plain": [ + " input.states target.states reachable.states edges transitions variables \\\n", + "0 6 3 NaN NaN NaN 975 \n", + "1 6 5 4 10 32 2705 \n", + "\n", + " clauses enc.user enc.sys sat.user sat.sys \n", + "0 32912 20 1 0 0 \n", + "1 150257 87 0 2 0 " + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "Fin(\n", + "⓿\n", + ")\n", + "[co-Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "⓿\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!a & !b & !c\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "(a & !b) | (!b & c)\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "⓿\n", + "\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "2->0\n", + "\n", + "\n", + "(!a & !b) | (!b & !c)\n", + "\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "\n", + "3->1\n", + "\n", + "\n", + "a | c\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x14faae26a6c0> >" + ] + }, + "execution_count": 20, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "# Binary search between 1 and 6\n", + "spot.sat_minimize(large, acc='co-Buchi', state_based=True, display_log=True)" + ] + }, + { + "cell_type": "code", + "execution_count": 21, + "metadata": {}, + "outputs": [ + { + "data": { + "text/html": [ + "
\n", + "\n", + "\n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + "
input.statestarget.statesreachable.statesedgestransitionsvariablesclausesenc.userenc.syssat.usersat.sys
0644123217327734045010
142NaNNaNNaN16231292000
243NaNNaNNaN363104966000
\n", + "
" + ], + "text/plain": [ + " input.states target.states reachable.states edges transitions variables \\\n", + "0 6 4 4 12 32 1732 \n", + "1 4 2 NaN NaN NaN 162 \n", + "2 4 3 NaN NaN NaN 363 \n", + "\n", + " clauses enc.user enc.sys sat.user sat.sys \n", + "0 77340 45 0 1 0 \n", + "1 3129 2 0 0 0 \n", + "2 10496 6 0 0 0 " + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "Fin(\n", + "⓿\n", + ")\n", + "[co-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", + "a & !b & c\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "⓿\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "(!a & !b) | (!b & !c)\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "⓿\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "b & !c\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "(!a & !b) | (!b & c)\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "b & !c\n", + "\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "b & !c\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "!b | c\n", + "\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x14faae26a480> >" + ] + }, + "execution_count": 21, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "# Binary search between 2 and 6 thanks to sat_langmap\n", + "spot.sat_minimize(large, acc='co-Buchi', sat_langmap=True, state_based=True, display_log=True)" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "### `states`\n", + "\n", + "Sometimes we do not want a minimization loop, we just want to generate an equivalent automaton with a given number of states. In that case, we use the `states` option. However there is no constraint that all state should be reachable, so in the end, you could end with an automaton with fewer states than requested." + ] + }, + { + "cell_type": "code", + "execution_count": 22, + "metadata": {}, + "outputs": [ + { + "data": { + "text/html": [ + "
\n", + "\n", + "\n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + "
input.statestarget.statesreachable.statesedgestransitionsvariablesclausesenc.userenc.syssat.usersat.sys
02751440186913503280120
\n", + "
" + ], + "text/plain": [ + " input.states target.states reachable.states edges transitions variables \\\n", + "0 2 7 5 14 40 1869 \n", + "\n", + " clauses enc.user enc.sys sat.user sat.sys \n", + "0 135032 80 1 2 0 " + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "Fin(\n", + "⓿\n", + ")\n", + "[co-Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "⓿\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "(!a & !b) | (!b & !c)\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "⓿\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!a & b & !c\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "⓿\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!a & b & c\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "\n", + "0->4\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!a & !b & !c\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!b & c\n", + "\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "b | (a & !c)\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "!c\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "4->0\n", + "\n", + "\n", + "(!a & !b) | (!b & !c)\n", + "\n", + "\n", + "\n", + "4->3\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x14faae26a3f0> >" + ] + }, + "execution_count": 22, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "spot.sat_minimize(small, acc=\"co-Buchi\", states=7, state_based=True, display_log=True)" + ] + } + ], + "metadata": { + "kernelspec": { + "display_name": "Python 3", + "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.6.5" + } + }, + "nbformat": 4, + "nbformat_minor": 2 +}