From fdb157bf949812b4f77888938205ccf7e0f1f510 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 22 Aug 2013 15:49:30 +0200 Subject: [PATCH] satmin: cleanup interfaces and minimization loops * src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtbasat.hh: (dtba_sat_minimize): Split into... (dtba_sat_synthetize, dtba_sat_minimize): These. (dtba_sat_minimize_dichotomy): New function. * src/tgbaalgos/dtgbasat.cc, src/tgbaalgos/dtgbasat.hh (dtgba_sat_minimize, dtgba_sat_synthetize): Likewise. * src/tgbatest/ltl2tgba.cc: Adjust to new interface. * src/tgbaalgos/postproc.cc, src/tgbaalgos/postproc.hh: Cleanup option processing for SAT options. * src/tgbatest/satmin.test: Adjust. * src/bin/spot-x.cc, src/bin/man/spot-x.x, NEWS: Document. --- NEWS | 8 ++ src/bin/man/spot-x.x | 41 +++++++++- src/bin/spot-x.cc | 32 ++++++++ src/tgbaalgos/dtbasat.cc | 159 ++++++++++++++++++++++---------------- src/tgbaalgos/dtbasat.hh | 43 +++++++---- src/tgbaalgos/dtgbasat.cc | 154 +++++++++++++++++++----------------- src/tgbaalgos/dtgbasat.hh | 46 +++++++---- src/tgbaalgos/postproc.cc | 115 +++++++++++++++------------ src/tgbaalgos/postproc.hh | 6 +- src/tgbatest/ltl2tgba.cc | 2 +- src/tgbatest/satmin.test | 9 ++- 11 files changed, 393 insertions(+), 222 deletions(-) diff --git a/NEWS b/NEWS index 404072776..daf434273 100644 --- a/NEWS +++ b/NEWS @@ -58,6 +58,14 @@ New in spot 1.1.4a (not relased) number of seconds spent building the output automaton (excluding the time spent parsing the input). + - ltl2tgba and dstar2tgba can use a SAT-solver to minimize + deterministic automata. Doing so is only needed on properties + that are stronger than obligations (for which our + WDBA-minimization procedure will return a minimimal + deterministic automaton more efficiently) and is disabled by + default. See the spot-x(7) man page for documentation about the + related options: sat-minimize, sat-states, sat-acc, state-based. + * All the parsers implemented in Spot now use the same type to store locations. diff --git a/src/bin/man/spot-x.x b/src/bin/man/spot-x.x index 1196278a8..cbd6e2d03 100644 --- a/src/bin/man/spot-x.x +++ b/src/bin/man/spot-x.x @@ -1,11 +1,39 @@ [NAME] spot-x \- Common fine-tuning options. + [SYNOPSIS] .B \-\-extra-options STRING .br .B \-x STRING + [DESCRIPTION] .\" Add any additional description here + +[ENVIRONMENT VARIABLES] + +.TP +\fBSPOT_SATSOLVER\fR +If set, this variable should indicate how to call a SAT\-solver. This +is used by the sat\-minimize option described above. The default value +is \f(CW"glucose %I >%O"\fR. The escape sequences \f(CW%I\fR and \f(CW%O\fR +respectively denote the names of the input and output files. These +temporary files are created in the directory specified by \fBSPOT_TMPDIR\fR +or \fBTMPDIR\fR (see below). + +.TP +\fBSPOT_TMPDIR\fR, \fBTMPDIR\fR +These variables control in which directory temporary files (e.g., +those who contain the input and output when interfacing with +translators) are created. \fBTMPDIR\fR is only read if +\fBSPOT_TMPDIR\fR does not exist. If none of these environment +variables exist, or if their value is empty, files are created in the +current directory. + +.TP +\fBSPOT_TMPKEEP\fR +When this variable is defined, temporary files are not removed. +This is mostly useful for debugging. + [BIBLIOGRAPHY] .TP 1. @@ -13,7 +41,10 @@ Christian Dax, Jochen Eisinger, Felix Klaedtke: Mechanizing the Powerset Construction for Restricted Classes of ω-Automata. Proceedings of ATVA'07. LNCS 4762. -Describes the WDBA-minimization algorithm implemented in Spot. +Describes the WDBA-minimization algorithm implemented in Spot. The +algorithm used for the tba-det options is also a generalization (to +TBA instead of BA) of what they describe in sections 3.2 and 3.3. + .TP 2. Tomáš Babiak, Thomas Badie, Alexandre Duret-Lutz, Mojmír Křetínský, @@ -23,6 +54,14 @@ Improvements to LTL Translation. Proceedings of SPIN'13. LNCS 7976. Describes the compositional suspension, the simulation-based reductions, and the SCC-based simplifications. +.TP +3. +Rüdiger Ehlers: Minimising Deterministic Büchi Automata Precisely using +SAT Solving. Proceedings of SAT'10. LNCS 6175. + +Our SAT-based minimization procedures are generalizations of this +paper to deal with TBA or TGBA. + [SEE ALSO] .BR ltl2tgba (1) .BR ltl2tgta (1) diff --git a/src/bin/spot-x.cc b/src/bin/spot-x.cc index c5cbbc98e..3be50e8e6 100644 --- a/src/bin/spot-x.cc +++ b/src/bin/spot-x.cc @@ -1,3 +1,4 @@ + // -*- coding: utf-8 -*- // Copyright (C) 2013 Laboratoire de Recherche et Développement // de l'Epita (LRDE). @@ -92,6 +93,37 @@ simulation. Set to 3 to iterate both direct and reverse simulations. \ The default is 3 in --high mode, and 0 otherwise.") }, { DOC("wdba-minimize", "Set to 0 to disable WDBA-minimization. \ Enabled by default.") }, + { DOC("tba-det", "Set to 1 to attempt a powerset determinization \ +if the TGBA is not already deterministic. Doing so will degeneralize \ +the automaton. This is disabled by default, unless sat-minimize is set.") }, + { DOC("sat-minimize", + "Set to 1 to enable SAT-based minimization of deterministic \ +TGBA: it starts with the number of states of the input, and iteratively \ +tries to find a deterministic TGBA with one less state. Set to 2 to perform \ +a binary search instead. Disabled (0) by default. The sat solver to use \ +can be set with the SPOT_SATSOLVER environment variable (see below). By \ +default the procedure looks for a TGBA with the same number of acceptance \ +set; this can be changed with the sat-acc option, or of course by using -B \ +to construct a Büchi automaton. Enabling SAT-based minimization will \ +also enable tba-det.") }, + { DOC("sat-states", + "When this is set to some positive integer, the SAT-based \ +minimization will attempt to construct a TGBA with the given number of \ +states. It may however return an automaton with less states if some of \ +these are unreachable or useless. Setting sat-states automatically \ +enables sat-minimize, but no iteration is performed. If no equivalent \ +automaton could be constructed with the given number of states, the original \ +automaton is returned.") }, + { DOC("sat-acc", + "When this is set to some positive integer, the SAT-based will \ +attempt to construct a TGBA with the given number of acceptance sets. \ +states. It may however return an automaton with less acceptance sets if \ +some of these are useless. Setting sat-acc automatically \ +sets sat-minimize to 1 if not set differently.") }, + { DOC("state-based", + "Set to 1 to instruct the SAT-minimization procedure to produce \ +a TGBA where all outgoing transition of a state have the same acceptance \ +sets. By default this is only enabled when option -B is used.") }, { 0, 0, 0, 0, 0, 0 } }; diff --git a/src/tgbaalgos/dtbasat.cc b/src/tgbaalgos/dtbasat.cc index 10afe73d4..7d639061e 100644 --- a/src/tgbaalgos/dtbasat.cc +++ b/src/tgbaalgos/dtbasat.cc @@ -51,8 +51,10 @@ #define DEBUG 0 #if DEBUG #define dout out << "c " +#define trace std::cerr #else -#define dout while (0) out +#define dout while (0) std::cout +#define trace dout #endif namespace spot @@ -317,8 +319,32 @@ namespace spot #if DEBUG debug_dict = ref->get_dict(); + dout << "ref_size: " << ref_size << "\n"; + dout << "cand_size: " << d.cand_size << "\n"; #endif + // dout << "symmetry-breaking clauses\n"; + // int k = 1; + // bdd all = bddtrue; + // while (all != bddfalse) + // { + // bdd s = bdd_satoneset(all, ap, bddfalse); + // all -= s; + // for (int q1 = 1; q1 < d.cand_size; ++q1) + // for (int q2 = q1 + 2; q2 <= d.cand_size; ++q2) + // if ((q1 - 1) * d.cand_size + q2 + 2 <= k) + // { + // transition t(q1, s, q2); + // int ti = d.transid[t]; + // dout << "¬" << t << "\n"; + // out << -ti << " 0\n"; + // ++nclauses; + // } + // ++k; + // } + // if (!nclauses) + // dout << "(none)\n"; + dout << "(1) the candidate automaton is complete\n"; for (int q1 = 1; q1 <= d.cand_size; ++q1) { @@ -712,86 +738,89 @@ namespace spot } tgba_explicit_number* - dtba_sat_minimize(const tgba* a, int target_state_number, - bool state_based) + dtba_sat_synthetize(const tgba* a, int target_state_number, + bool state_based) { - int ref_states = - target_state_number == -1 - ? stats_reachable(a).states - 1 - : target_state_number; - - std::string current_solution; - std::string last_solution; - dict* last = 0; + trace << "dtba_sat_synthetize(..., states = " << target_state_number + << ", state_based = " << state_based << ")\n"; + std::string solution; dict* current = 0; temporary_file* cnf = 0; temporary_file* out = 0; - do - { - if (DEBUG && current) - { - xrename(out->name(), "dtba-sat.out"); - xrename(cnf->name(), "dtba-sat.cnf"); - } - delete out; - delete cnf; - std::swap(current_solution, last_solution); - delete last; - last = current; - current = new dict; - current->cand_size = ref_states--; + current = new dict; + current->cand_size = target_state_number; - cnf = create_tmpfile("dtba-sat-", ".cnf"); + cnf = create_tmpfile("dtba-sat-", ".cnf"); + std::fstream cnfs(cnf->name(), + std::ios_base::trunc | std::ios_base::out); + dtba_to_sat(cnfs, a, *current, state_based); + cnfs.close(); - std::fstream cnfs(cnf->name(), - std::ios_base::trunc | std::ios_base::out); - dtba_to_sat(cnfs, a, *current, state_based); - cnfs.close(); + out = create_tmpfile("dtba-sat-", ".out"); + satsolver(cnf, out); - out = create_tmpfile("dtba-sat-", ".out"); - satsolver(cnf, out); - current_solution = get_solution(out->name()); - } - while (target_state_number == -1 && !current_solution.empty()); + solution = get_solution(out->name()); - if (target_state_number != -1) - { - std::swap(current_solution, last_solution); - if (last_solution.empty()) - { - last = 0; - delete current; - } - else - { - last = current; - } - } - else - { - delete current; - } + tgba_explicit_number* res = 0; + if (!solution.empty()) + res = sat_build(solution, *current, a, state_based); - tgba_explicit_number* res; - if (last == 0) + delete current; + + if (DEBUG) { - res = 0; - if (DEBUG) - { - xrename(out->name(), "dtba-sat.out"); - xrename(cnf->name(), "dtba-sat.cnf"); - } - } - else - { - res = sat_build(last_solution, *last, a, state_based); - delete last; + xrename(out->name(), "dtba-sat.out"); + xrename(cnf->name(), "dtba-sat.cnf"); } delete out; delete cnf; + trace << "dtba_sat_synthetize(...) = " << res << "\n"; return res; } + tgba_explicit_number* + dtba_sat_minimize(const tgba* a, bool state_based) + { + int n_states = stats_reachable(a).states; + + tgba_explicit_number* prev = 0; + for (;;) + { + tgba_explicit_number* next = + dtba_sat_synthetize(prev ? prev : a, --n_states, state_based); + if (next == 0) + break; + delete prev; + prev = next; + } + return prev; + } + + tgba_explicit_number* + dtba_sat_minimize_dichotomy(const tgba* a, bool state_based) + { + int max_states = stats_reachable(a).states - 1; + int min_states = 1; + + tgba_explicit_number* prev = 0; + while (min_states <= max_states) + { + int target = (max_states + min_states) / 2; + tgba_explicit_number* next = + dtba_sat_synthetize(prev ? prev : a, target, state_based); + if (next == 0) + { + min_states = target + 1; + } + else + { + delete prev; + prev = next; + max_states = target - 1; + } + } + return prev; + } } diff --git a/src/tgbaalgos/dtbasat.hh b/src/tgbaalgos/dtbasat.hh index 99f82096a..7393944ea 100644 --- a/src/tgbaalgos/dtbasat.hh +++ b/src/tgbaalgos/dtbasat.hh @@ -20,32 +20,47 @@ #ifndef SPOT_TGBAALGOS_DTBASAT_HH # define SPOT_TGBAALGOS_DTBASAT_HH -#include -#include "tgba/tgba.hh" #include "tgba/tgbaexplicit.hh" namespace spot { - /// \brief Attempt to reduce a deterministic TBA with a SAT solver. + /// \brief Attempt to synthetize an equivalent deterministic TBA + /// with a SAT solver. /// - /// \param a the TGBA to reduce. It should have only one acceptance - /// set and be deterministic. I.e., it should be a deterministic TBA. + /// \param a the input TGBA. It should have only one acceptance + /// set and be deterministic. I.e., it should be a deterministic TBA. /// - /// \param target_state_number the expected number of states wanted - /// in the resulting automaton. If \a target_state_number is left - /// to its default value of -1, this function will attempt to build - /// the smallest possible deterministic TBA is can produce. + /// \param target_state_number the desired number of states wanted + /// in the resulting automaton. The result may have less than \a + /// target_state_number reachable states. /// /// \param state_based set to true to force all outgoing transitions /// of a state to share the same acceptance condition, effectively /// turning the TBA into a BA. /// - /// If no automaton with \a target_state_number states is found, or - /// (in case target_state_number == -1) if no smaller - /// automaton is found, then a null pointer is returned. + /// If no equivalent deterministic TBA with \a target_state_number + /// states is found, a null pointer SPOT_API tgba_explicit_number* - dtba_sat_minimize(const tgba* a, int target_state_number = -1, - bool state_based = false); + dtba_sat_synthetize(const tgba* a, int target_state_number, + bool state_based = false); + + /// \brief Attempt to minimize a deterministic TBA with a SAT solver. + /// + /// This calls dtba_sat_synthetize() in a loop, with a decreasing + /// number of states, and returns the last successfully built TBA. + /// + /// If no smaller TBA exist, this returns a null pointer. + SPOT_API tgba_explicit_number* + dtba_sat_minimize(const tgba* a, bool state_based = false); + + /// \brief Attempt to minimize a deterministic TBA with a SAT solver. + /// + /// This calls dtba_sat_synthetize() in a loop, but attempting to + /// find the minimum number of states using a binary search. + // + /// If no smaller TBA exist, this returns a null pointer. + SPOT_API tgba_explicit_number* + dtba_sat_minimize_dichotomy(const tgba* a, bool state_based = false); } #endif // SPOT_TGBAALGOS_DTBASAT_HH diff --git a/src/tgbaalgos/dtgbasat.cc b/src/tgbaalgos/dtgbasat.cc index 4986882e2..8a120934b 100644 --- a/src/tgbaalgos/dtgbasat.cc +++ b/src/tgbaalgos/dtgbasat.cc @@ -52,16 +52,16 @@ #define DEBUG 0 #if DEBUG #define dout out << "c " +#define trace std::cerr #else -#define dout while (0) out +#define dout while (0) std::cout +#define trace dout #endif - namespace spot { namespace { - static bdd_dict* debug_dict = 0; struct transition @@ -477,9 +477,6 @@ namespace spot sm.build_map(); bdd ap = sm.aprec_set_of(sm.initial()); -#if DEBUG - debug_dict = ref->get_dict(); -#endif // Number all the SAT variable we may need. { @@ -488,6 +485,12 @@ namespace spot ref_size = f.size(); } +#if DEBUG + debug_dict = ref->get_dict(); + dout << "ref_size: " << ref_size << "\n"; + dout << "cand_size: " << d.cand_size << "\n"; +#endif + // empty automaton is impossible if (d.cand_size == 0) { @@ -937,87 +940,96 @@ namespace spot } tgba_explicit_number* - dtgba_sat_minimize(const tgba* a, unsigned cand_nacc, - int target_state_number, bool state_based) + dtgba_sat_synthetize(const tgba* a, unsigned target_acc_number, + int target_state_number, bool state_based) { - int ref_states = - target_state_number == -1 - ? stats_reachable(a).states - 1 - : target_state_number; - - std::string current_solution; - std::string last_solution; - dict* last = 0; + trace << "dtgba_sat_synthetize(..., acc = " << target_acc_number + << ", states = " << target_state_number + << ", state_based = " << state_based << ")\n"; + std::string solution; dict* current = 0; temporary_file* cnf = 0; temporary_file* out = 0; - do - { - if (DEBUG && current) - { - xrename(out->name(), "dtgba-sat.out"); - xrename(cnf->name(), "dtgba-sat.cnf"); - } - delete out; - delete cnf; - std::swap(current_solution, last_solution); - delete last; - last = current; - current = new dict(a); - current->cand_size = ref_states--; - current->cand_nacc = cand_nacc; + current = new dict(a); + current->cand_size = target_state_number; + current->cand_nacc = target_acc_number; - cnf = create_tmpfile("dtgba-sat-", ".cnf"); + cnf = create_tmpfile("dtgba-sat-", ".cnf"); + std::fstream cnfs(cnf->name(), + std::ios_base::trunc | std::ios_base::out); + dtgba_to_sat(cnfs, a, *current, state_based); + cnfs.close(); - std::fstream cnfs(cnf->name(), - std::ios_base::trunc | std::ios_base::out); - dtgba_to_sat(cnfs, a, *current, state_based); - cnfs.close(); + out = create_tmpfile("dtgba-sat-", ".out"); + satsolver(cnf, out); - out = create_tmpfile("dtgba-sat-", ".out"); - satsolver(cnf, out); - current_solution = get_solution(out->name()); - } - while (target_state_number == -1 && !current_solution.empty()); + solution = get_solution(out->name()); - if (target_state_number != -1) - { - std::swap(current_solution, last_solution); - if (last_solution.empty()) - { - last = 0; - delete current; - } - else - { - last = current; - } - } - else - { - delete current; - } + tgba_explicit_number* res = 0; + if (!solution.empty()) + res = sat_build(solution, *current, a, state_based); - tgba_explicit_number* res; - if (last == 0) + delete current; + + if (DEBUG) { - res = 0; - if (DEBUG) - { - xrename(out->name(), "dtgba-sat.out"); - xrename(cnf->name(), "dtgba-sat.cnf"); - } - } - else - { - res = sat_build(last_solution, *last, a, state_based); - delete last; + xrename(out->name(), "dtgba-sat.out"); + xrename(cnf->name(), "dtgba-sat.cnf"); } delete out; delete cnf; + trace << "dtgba_sat_synthetize(...) = " << res << "\n"; return res; } + tgba_explicit_number* + dtgba_sat_minimize(const tgba* a, unsigned target_acc_number, + bool state_based) + { + int n_states = stats_reachable(a).states; + + tgba_explicit_number* prev = 0; + for (;;) + { + tgba_explicit_number* next = + dtgba_sat_synthetize(prev ? prev : a, target_acc_number, + --n_states, state_based); + if (next == 0) + break; + delete prev; + prev = next; + } + return prev; + } + + tgba_explicit_number* + dtgba_sat_minimize_dichotomy(const tgba* a, unsigned target_acc_number, + bool state_based) + { + int max_states = stats_reachable(a).states - 1; + int min_states = 1; + + tgba_explicit_number* prev = 0; + while (min_states <= max_states) + { + int target = (max_states + min_states) / 2; + tgba_explicit_number* next = + dtgba_sat_synthetize(prev ? prev : a, target_acc_number, target, + state_based); + if (next == 0) + { + min_states = target + 1; + } + else + { + delete prev; + prev = next; + max_states = target - 1; + } + } + return prev; + } + } diff --git a/src/tgbaalgos/dtgbasat.hh b/src/tgbaalgos/dtgbasat.hh index e4bc8416f..c66810e0c 100644 --- a/src/tgbaalgos/dtgbasat.hh +++ b/src/tgbaalgos/dtgbasat.hh @@ -20,36 +20,54 @@ #ifndef SPOT_TGBAALGOS_DTGBASAT_HH # define SPOT_TGBAALGOS_DTGBASAT_HH -#include -#include "tgba/tgba.hh" #include "tgba/tgbaexplicit.hh" namespace spot { - /// \brief Attempt to reduce a deterministic TGBA with a SAT solver. + /// \brief Attempt to synthetize am equivalent deterministic TGBA + /// with a SAT solver. /// - /// \param a the TGBA to reduce. It should have only one acceptance - /// set and be deterministic. I.e., it should be a deterministic TBA. + /// \param a the input TGBA. It should be a deterministic TGBA. /// - /// \param cand_nacc is the number of acceptance sets in the result. + /// \param target_acc_number is the number of acceptance sets wanted + /// in the result. + /// + /// \param target_state_number is the desired number of states in + /// the result. The output may have less than \a + /// target_state_number reachable states. /// /// \param state_based set to true to force all outgoing transitions /// of a state to share the same acceptance conditions, effectively /// turning the TGBA into a TBA. /// - /// \param target_state_number the expected number of states wanted - /// in the resulting automaton. If \a target_state_number is left - /// to its default value of -1, this function will attempt to build - /// the smallest possible deterministic TGBA is can produce. - /// - /// This functions attempts to find a TGBA with \a cand_nacc + /// This functions attempts to find a TGBA with \a target_acc_number /// acceptance sets and target_state_number states that is /// equivalent to \a a. If no such TGBA is found, a null pointer is /// returned. SPOT_API tgba_explicit_number* - dtgba_sat_minimize(const tgba* a, unsigned cand_nacc, - int target_state_number = -1, + dtgba_sat_synthetize(const tgba* a, unsigned target_acc_number, + int target_state_number, + bool state_based = false); + + /// \brief Attempt to minimize a deterministic TGBA with a SAT solver. + /// + /// This calls dtgba_sat_synthetize() in a loop, with a decreasing + /// number of states, and returns the last successfully built TGBA. + /// + /// If no smaller TGBA exist, this returns a null pointer. + SPOT_API tgba_explicit_number* + dtgba_sat_minimize(const tgba* a, unsigned target_acc_number, bool state_based = false); + + /// \brief Attempt to minimize a deterministic TGBA with a SAT solver. + /// + /// This calls dtgba_sat_synthetize() in a loop, but attempting to + /// find the minimum number of states using a binary search. + // + /// If no smaller TBA exist, this returns a null pointer. + SPOT_API tgba_explicit_number* + dtgba_sat_minimize_dichotomy(const tgba* a, unsigned target_acc_number, + bool state_based = false); } #endif // SPOT_TGBAALGOS_DTGBASAT_HH diff --git a/src/tgbaalgos/postproc.cc b/src/tgbaalgos/postproc.cc index 22b3b19b8..17254bb1a 100644 --- a/src/tgbaalgos/postproc.cc +++ b/src/tgbaalgos/postproc.cc @@ -51,15 +51,24 @@ namespace spot scc_filter_ = opt->get("scc-filter", -1); ba_simul_ = opt->get("ba-simul", -1); tba_determinisation_ = opt->get("tba-det", 0); - dtba_sat_minimize_ = opt->get("dtba-sat-minimize", -1); - dtgba_sat_minimize_ = opt->get("dtgba-sat-minimize", -1); - dtgba_sat_minimize_acc_ = opt->get("dtgba-sat-minimize-acc", -1); - if (dtgba_sat_minimize_ >= 0 && dtgba_sat_minimize_acc_ == -1) - dtgba_sat_minimize_acc_ = 0; - if (dtgba_sat_minimize_ == -1 && dtgba_sat_minimize_acc_ >= 0) - dtgba_sat_minimize_ = 0; + sat_minimize_ = opt->get("sat-minimize", 0); + sat_states_ = opt->get("sat-states", 0); + sat_acc_ = opt->get("sat-acc", 0); state_based_ = opt->get("state-based", 0); wdba_minimize_ = opt->get("wdba-minimize", 1); + + if (sat_acc_ && sat_minimize_ == 0) + sat_minimize_ = 1; // 2? + if (sat_states_ && sat_minimize_ == 0) + sat_minimize_ = 1; + if (sat_minimize_) + { + tba_determinisation_ = 1; + if (sat_acc_ <= 0) + sat_acc_ = -1; + if (sat_states_ <= 0) + sat_states_ = -1; + } } } @@ -128,6 +137,8 @@ namespace spot ba_simul_ = (level_ == High) ? 3 : 0; if (scc_filter_ < 0) scc_filter_ = 1; + if (type_ == BA) + state_based_ = true; // Remove useless SCCs. if (type_ == Monitor) @@ -198,6 +209,7 @@ namespace spot bool dba_is_minimal = false; const tgba* dba = 0; const tgba* sim = 0; + int original_acc = a->number_of_acceptance_conditions(); // (Small,Low) is the only configuration where we do not run // WDBA-minimization. @@ -287,56 +299,60 @@ namespace spot // that case dba_is_wdba=true), or some deterministic automaton // that is either the result of the simulation or of the // TBA-determinization (dba_is_wdba=false in both cases). - - // Attempt SAT-minimization if requested. - if (dtba_sat_minimize_ >= 0 && dba && !dba_is_wdba) + if (sat_minimize_ && dba && !dba_is_wdba) { - // This only work on deterministic TBA, so degeneralize - // if needed. - const tgba* tmpd = 0; - if (dba->number_of_acceptance_conditions() != 1) + unsigned target_acc; + if (type_ == BA) + target_acc = 1; + else if (sat_acc_ != -1) + target_acc = sat_acc_; + else + // Take the number of acceptance conditions from the input + // automaton, not from dba, because dba has always one. + target_acc = original_acc; + + const tgba* in = 0; + const tgba* to_free = 0; + if (target_acc == 1) { // If we are seeking a minimal DBA with unknown number of // states, then we should start from the degeneralized, // because the input TBA might be smaller. - if (state_based_ && dtba_sat_minimize_ == 0) - tmpd = degeneralize(dba); + if (state_based_) + to_free = in = degeneralize(dba); + else if (dba->number_of_acceptance_conditions() != 1) + to_free = in = new tgba_tba_proxy(dba); else - tmpd = new tgba_tba_proxy(dba); + in = dba; + } + else + { + in = dba; } - - const tgba* in = tmpd ? tmpd : dba; const tgba* cmp = tgba_complete(in); - const tgba* res = dtba_sat_minimize(cmp, - dtba_sat_minimize_ == 0 - ? -1 : dtba_sat_minimize_, - state_based_); - delete cmp; - delete tmpd; - if (res != 0) + const tgba* res = 0; + if (target_acc == 1) { - delete dba; - if (state_based_) - dba = scc_filter_states(res); - else - dba = scc_filter(res, true); - delete res; - dba_is_minimal = true; + if (sat_states_ != -1) + res = dtba_sat_synthetize(cmp, sat_states_, state_based_); + else if (sat_minimize_ == 1) + res = dtba_sat_minimize(cmp, state_based_); + else // sat_minimize_ == 2 + res = dtba_sat_minimize_dichotomy(cmp, state_based_); + } + else + { + if (sat_states_ != -1) + res = dtgba_sat_synthetize(cmp, target_acc, sat_states_, + state_based_); + else if (sat_minimize_ == 1) + res = dtgba_sat_minimize(cmp, target_acc, state_based_); + else // sat_minimize_ == 2 + res = dtgba_sat_minimize_dichotomy(cmp, target_acc, state_based_); } - } - else if (dtgba_sat_minimize_ >= 0 && dba && !dba_is_wdba) - { - const tgba* cmp = tgba_complete(dba); - const tgba* res = - dtgba_sat_minimize(cmp, - dtgba_sat_minimize_acc_ - ? dtgba_sat_minimize_acc_ - : dba->number_of_acceptance_conditions(), - dtgba_sat_minimize_ == 0 - ? -1 : dtgba_sat_minimize_, - state_based_); delete cmp; + delete to_free; if (res != 0) { delete dba; @@ -353,10 +369,11 @@ namespace spot } } - - // Degeneralize the dba resulting from tba-determinization - // or sat-minimization (which is a TBA) if requested. - if (dba && !dba_is_wdba && type_ == BA) + // Degeneralize the dba resulting from tba-determinization or + // sat-minimization (which is a TBA) if requested and needed. + if (dba && !dba_is_wdba && type_ == BA + && !(dba_is_minimal && state_based_ + && dba->number_of_acceptance_conditions() == 1)) { const tgba* d = degeneralize(dba); delete dba; diff --git a/src/tgbaalgos/postproc.hh b/src/tgbaalgos/postproc.hh index 915376d77..947a4761b 100644 --- a/src/tgbaalgos/postproc.hh +++ b/src/tgbaalgos/postproc.hh @@ -106,9 +106,9 @@ namespace spot int scc_filter_; int ba_simul_; bool tba_determinisation_; - int dtba_sat_minimize_; - int dtgba_sat_minimize_; - int dtgba_sat_minimize_acc_; + int sat_minimize_; + int sat_acc_; + int sat_states_; bool state_based_; bool wdba_minimize_; }; diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index d15dfd12a..f52b41bb1 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -1528,7 +1528,7 @@ main(int argc, char** argv) if (opt_dtbasat >= 0) { tm.start("dtbasat"); - satminimized = dtba_sat_minimize(a, opt_dtbasat); + satminimized = dtba_sat_synthetize(a, opt_dtbasat); tm.stop("dtbasat"); if (satminimized) a = satminimized; diff --git a/src/tgbatest/satmin.test b/src/tgbatest/satmin.test index 5dd8c396b..1883204aa 100755 --- a/src/tgbatest/satmin.test +++ b/src/tgbatest/satmin.test @@ -89,8 +89,9 @@ $ltlcross -F formulas \ --timeout=60 \ "$ltl2tgba --det --lbtt %f >%T" \ "$ltl2tgba --det --lbtt -x tba-det %f >%T" \ - "$ltl2tgba --det --lbtt -x tba-det,dtba-sat-minimize=0 %f >%T" \ - "$ltl2tgba --det --lbtt -x tba-det,dtgba-sat-minimize-acc=0 %f >%T" \ - "$ltl2tgba --det --lbtt -x dtgba-sat-minimize-acc=0 %f >%T" \ - "$ltl2tgba --det --lbtt -x tba-det,dtgba-sat-minimize-acc=3 %f >%T" \ + "$ltl2tgba --det --lbtt -x sat-acc=1 %f >%T" \ + "$ltl2tgba --det --lbtt -x sat-acc=3 %f >%T" \ + "$ltl2tgba --det --lbtt -x sat-states=3 %f >%T" \ + "$ltl2tgba --det --lbtt -x sat-minimize %f >%T" \ + "$ltl2tgba --det --lbtt -x sat-minimize=2 %f >%T" \ --json=det.json