diff --git a/NEWS b/NEWS index 8f147ad35..61f7c6df7 100644 --- a/NEWS +++ b/NEWS @@ -65,6 +65,19 @@ New in spot 2.11.6.dev (not yet released) 36 seconds; it now produce an AIG circuit with 53 nodes in only 0.1 second. + - spot::contains_forq() is a implementation of the paper "FORQ-Based + Language Inclusion Formal Testing" (Doveri, Ganty, Mazzocchi; + CAV'22) contributed by Jonah Romero. + + - spot::contains() still default to the complementation-based + algorithm, however by calling + spot::containment_select_version("forq") or by setting + SPOT_CONTAINMENT_CHECK=forq in the environment, the + spot::contains_forq() implementation will be used instead when + applicable (inclusion between Büchi automata). + + The above also impacts autfilt --included-in option. + Bugs fixed: - tgba_determinize()'s use_simulation option would cause it to diff --git a/bin/autfilt.cc b/bin/autfilt.cc index eec2246b3..820b37f49 100644 --- a/bin/autfilt.cc +++ b/bin/autfilt.cc @@ -45,6 +45,7 @@ #include #include #include +#include #include #include #include @@ -984,12 +985,24 @@ parse_opt(int key, char* arg, struct argp_state*) break; case OPT_INCLUDED_IN: { - auto aut = ensure_deterministic(read_automaton(arg, opt->dict), true); - aut = spot::dualize(aut); - if (!opt->included_in) - opt->included_in = aut; + auto aut = read_automaton(arg, opt->dict); + if (spot::containment_select_version() == 0) + { + aut = spot::complement(aut); + if (!aut->is_existential()) + aut = spot::remove_alternation(aut); + if (!opt->included_in) + opt->included_in = aut; + else + opt->included_in = ::product_or(opt->included_in, aut); + } else - opt->included_in = ::product_or(opt->included_in, aut); + { + if (opt->included_in) + error(2, 0, "FORQ-based inclusion check only works " + "with one inclusion-test at a time"); + opt->included_in = aut; + } } break; case OPT_INHERENTLY_WEAK_SCCS: @@ -1519,7 +1532,12 @@ namespace if (opt->intersect) matched &= aut->intersects(opt->intersect); if (opt->included_in) - matched &= !aut->intersects(opt->included_in); + { + if (spot::containment_select_version() == 0) + matched &= !aut->intersects(opt->included_in); + else + matched &= spot::contains(opt->included_in, aut); + } if (opt->equivalent_pos) matched &= !aut->intersects(opt->equivalent_neg) && spot::contains(aut, opt->equivalent_pos); diff --git a/bin/man/spot-x.x b/bin/man/spot-x.x index c6091c339..b9e3c7166 100644 --- a/bin/man/spot-x.x +++ b/bin/man/spot-x.x @@ -51,12 +51,13 @@ If this variable is set to any value, statistics about BDD garbage collection and resizing will be output on standard error. .TP -\fSPOT_CONTAINMENT_CHECK\fR -Specifies which inclusion algorithm spot should use. This can currently -take on 1 of 2 values: 0 for the legacy implementation, and 1 for the -forq implementation [6] (See bibliography below). Forq uses buchi -automata in order to determine inclusion, and will default to the legacy -version if these constraints are not satisfied. +\fBSPOT_CONTAINMENT_CHECK\fR +Specifies which inclusion algorithm Spot should use. If the variable +is unset, or set to \fB"default"\fR, containment checks are done +using a complementation-based procedure. If the variable is set to +\fB"forq"\fR, and FORQ-based containment check is used for Büchi automata +(the default procedure is still used for non-Büchi automata). See +[6] in the bibliography below. .TP \fBSPOT_DEFAULT_FORMAT\fR @@ -335,24 +336,12 @@ disabled with \fB-x gf-guarantee=0\fR. .TP 6. -Doveri, Kyveli and Ganty, Pierre and Mazzocchi, Nicolas: +Kyveli Doveri and Pierre Ganty and Nicolas Mazzocchi: FORQ-Based Language Inclusion Formal Testing. Proceedings of CAV'22. LNCS 13372. -We propose a novel algorithm to decide the language inclusion between -(nondeterministic) Büchi automata, a PSpace-complete problem. Our approach, -like others before, leverage a notion of quasiorder to prune the search for a -counterexample by discarding candidates which are subsumed by others for the -quasiorder.Discarded candidates are guaranteed to not compromise the -completeness of the algorithm. The novelty of our work lies in the quasiorder k -used to discard candidates. We introduce FORQs (family of right quasiorders) -that we obtain by adapting the notion of family of right congruences put forward -by Maler and Staiger in 1993. We define a FORQ-based inclusion algorithm which -we prove correct and instantiate it for a specific FORQ, called the structural -FORQ, induced by the B\"uchi automaton to the right of the inclusion sign. The -resulting implementation, called Forklift, scales up better than the -state-of-the-art on a variety of benchmarks including benchmarks from program -verification and theorem proving for word combinatorics. +The containment check implemented as spot::contains_forq(), and +used for Büchi automata when \fBSPOT_CONTAINMENT_CHECK=forq\fR. [SEE ALSO] .BR ltl2tgba (1) diff --git a/spot/twa/twa.cc b/spot/twa/twa.cc index a5288ac3c..c1c113e87 100644 --- a/spot/twa/twa.cc +++ b/spot/twa/twa.cc @@ -29,6 +29,7 @@ #include #include #include +#include #include #include #include @@ -213,6 +214,7 @@ namespace spot return make_twa_graph(aut_in, twa::prop_set::all()); } } + twa_run_ptr twa::exclusive_run(const_twa_ptr other) const { @@ -235,37 +237,21 @@ namespace spot const_twa_ptr a = shared_from_this(); const_twa_ptr b = other; - enum class containment_type : unsigned { LEGACY = 0, FORQ }; - static containment_type containment = [&]() - { - char* s = getenv("SPOT_EXCLUSIVE_WORD"); - // We expect a single digit that represents a valid enumeration value - if (!s) - return containment_type::LEGACY; - else if (*s == '\0' || *(s + 1) != '\0' || *s < '0' || *s > '1') - throw std::runtime_error("Invalid value for enviroment variable: " - "SPOT_EXCLUSIVE_WORD"); - else - return static_cast(*s - '0'); - }(); - // We have to find a word in A\B or in B\A. When possible, let's // make sure the first automaton we complement, i.e., b, is deterministic. - auto a_twa_as_graph = std::dynamic_pointer_cast(a); - auto b_twa_as_graph = std::dynamic_pointer_cast(b); - if (a_twa_as_graph) + if (auto a_twa_as_graph = std::dynamic_pointer_cast(a)) if (is_deterministic(a_twa_as_graph)) std::swap(a, b); - if (containment == containment_type::FORQ - && a_twa_as_graph - && b_twa_as_graph - && a_twa_as_graph->acc().is_buchi() - && b_twa_as_graph->acc().is_buchi()) + if (containment_select_version() == 1 + && a->acc().is_buchi() + && b->acc().is_buchi()) { - if (auto word = difference_word_forq(a_twa_as_graph, b_twa_as_graph)) + auto ag = ensure_graph(a); + auto bg = ensure_graph(b); + if (auto word = difference_word_forq(ag, bg)) return word; - return difference_word_forq(b_twa_as_graph, a_twa_as_graph); + return difference_word_forq(bg, ag); } else { diff --git a/spot/twaalgos/contains.cc b/spot/twaalgos/contains.cc index d30904aa6..7170fbedf 100644 --- a/spot/twaalgos/contains.cc +++ b/spot/twaalgos/contains.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2018, 2019, 2022 Laboratoire de Recherche et Développement de -// l'Epita. +// Copyright (C) 2018, 2019, 2022, 2023 Laboratoire de Recherche et +// Développement de l'Epita. // // This file is part of Spot, a model checking library. // @@ -33,39 +33,25 @@ namespace spot { return ltl_to_tgba_fm(f, dict); } - } - static bool is_buchi_automata(const_twa_graph_ptr const& aut) - { - return spot::acc_cond::acc_code::buchi() == aut->get_acceptance(); + static const_twa_graph_ptr + ensure_graph(const const_twa_ptr& aut_in) + { + const_twa_graph_ptr aut = + std::dynamic_pointer_cast(aut_in); + if (aut) + return aut; + return make_twa_graph(aut_in, twa::prop_set::all()); + } } bool contains(const_twa_graph_ptr left, const_twa_ptr right) { - enum class containment_type : unsigned { LEGACY = 0, FORQ }; - static containment_type containment = [&]() - { - char* s = getenv("SPOT_CONTAINMENT_CHECK"); - // We expect a single digit that represents a valid enumeration value - if (!s) - return containment_type::LEGACY; - else if (*s == '\0' || *(s + 1) != '\0' || *s < '0' || *s > '1') - throw std::runtime_error("Invalid value for enviroment variable: " - "SPOT_CONTAINMENT_CHECK"); - else - return static_cast(*s - '0'); - }(); - - auto as_graph = std::dynamic_pointer_cast(right); - bool uses_buchi = is_buchi_automata(left) && is_buchi_automata(as_graph); - if (containment == containment_type::FORQ && uses_buchi && as_graph) - { - return contains_forq(left, as_graph); - } + if (containment_select_version() == 1 + && left->acc().is_buchi() && right->acc().is_buchi()) + return contains_forq(left, ensure_graph(right)); else - { - return !complement(left)->intersects(right); - } + return !complement(left)->intersects(right); } bool contains(const_twa_graph_ptr left, formula right) @@ -111,4 +97,32 @@ namespace spot { return contains(right, left) && contains(left, right); } + + int containment_select_version(const char* version) + { + static int pref = -1; + const char *env = nullptr; + if (!version && pref < 0) + version = env = getenv("SPOT_CONTAINMENT_CHECK"); + if (version) + { + if (!strcasecmp(version, "default")) + pref = 0; + else if (!strcasecmp(version, "forq")) + pref = 1; + else + { + const char* err = ("containment_select_version(): argument" + " should be one of {default,forq}"); + if (env) + err = "SPOT_CONTAINMENT_CHECK should be one of {default,forq}"; + throw std::runtime_error(err); + } + } + else if (pref < 0) + { + pref = 0; + } + return pref; + } } diff --git a/spot/twaalgos/contains.hh b/spot/twaalgos/contains.hh index a1d64f1b1..5c30a66b9 100644 --- a/spot/twaalgos/contains.hh +++ b/spot/twaalgos/contains.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2018, 2022 Laboratoire de Recherche et Développement de -// l'Epita. +// Copyright (C) 2018, 2022, 2023 Laboratoire de Recherche et +// Développement de l'Epita. // // This file is part of Spot, a model checking library. // @@ -62,4 +62,30 @@ namespace spot SPOT_API bool are_equivalent(formula left, const_twa_graph_ptr right); SPOT_API bool are_equivalent(formula left, formula right); /// @} + + /// \ingroup containment + /// + /// Query, or change the version of the containment check to use by + /// contains() or twa::exclusive_run(). + /// + /// By default those containment checks use a complementation-based + /// algorithm that is generic that work on any acceptance condition. + /// Alternative algorithms such as contains_forq() are available, + /// for Büchi automata, but are not used by default. + /// + /// When calling this function \a version can be: + /// - "default" to force the above default containment checks to be used + /// - "forq" to use contains_forq() when possible + /// - nullptr do not modify the preference. + /// + /// If the first call to containement_select_version() is done with + /// nullptr as an argument, then the value of the + /// SPOT_CONTAINMENT_CHECK environment variable is used instead. + /// + /// In all cases, the preferred containment check is returned as an + /// integer. This integer is meant to be used by Spot's algorithms + /// to select the desired containment check to apply, but it's + /// encoding (currently 1 for FORQ, 0 for default) should be + /// regarded as an implementation detail subject to change. + SPOT_API int containment_select_version(const char* version = nullptr); } diff --git a/tests/core/included.test b/tests/core/included.test index 3574af9e3..e9f2cea08 100755 --- a/tests/core/included.test +++ b/tests/core/included.test @@ -1,6 +1,6 @@ #! /bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2016, 2022 Laboratoire de Recherche et Développement +# Copyright (C) 2016, 2022, 2023 Laboratoire de Recherche et Développement # de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -38,6 +38,20 @@ run 0 autfilt -q gab.hoa --included-in fga.hoa --included-in fgb.hoa run 1 autfilt -q ga.hoa --included-in fga.hoa --included-in fgb.hoa run 0 autfilt -q false.hoa --included-in fga.hoa +SPOT_CONTAINMENT_CHECK=forq run 0 autfilt -q fga.hoa --included-in gfa.hoa +SPOT_CONTAINMENT_CHECK=forq run 0 autfilt -q fga.hoa --included-in fga.hoa +SPOT_CONTAINMENT_CHECK=forq run 1 autfilt -q gfa.hoa --included-in fga.hoa +SPOT_CONTAINMENT_CHECK=forq \ + run 2 autfilt -q gab.hoa --included-in fga.hoa --included-in fgb.hoa +SPOT_CONTAINMENT_CHECK=forq \ + run 2 autfilt -q ga.hoa --included-in fga.hoa --included-in fgb.hoa +SPOT_CONTAINMENT_CHECK=forq run 0 autfilt -q false.hoa --included-in fga.hoa + +SPOT_CONTAINMENT_CHECK=error \ + autfilt -q fga.hoa --included-in gfa.hoa >err && exit 1 +test $? -eq 2 +grep 'SPOT_CONTAINMENT_CHECK.*forq' error + run 1 autfilt -q gfa.hoa --equivalent-to fga.hoa run 1 autfilt -q fga.hoa --equivalent-to gfa.hoa @@ -61,6 +75,7 @@ ltl2tgba '!(a U c)' | autfilt --product-or a1.hoa > out.hoa ltl2tgba true | autfilt out.hoa --equivalent-to - && exit 1 # In Spot 2.10, the following was very slow. +export SPOT_CONTAINMENT_CHECK=default for n in 1 2 4 8 16 512 1024 2048 4096 8192; do genaut --cyclist-trace-nba=$n > trace.hoa genaut --cyclist-proof-dba=$n > proof.hoa @@ -68,4 +83,13 @@ for n in 1 2 4 8 16 512 1024 2048 4096 8192; do autfilt -q --included-in=proof.hoa trace.hoa && exit 1 done +# The forq-based version does not scale well on this particular test +export SPOT_CONTAINMENT_CHECK=forq +for n in 1 2 4 8 16 128; do + genaut --cyclist-trace-nba=$n > trace.hoa + genaut --cyclist-proof-dba=$n > proof.hoa + autfilt -q --included-in=trace.hoa proof.hoa || exit 1 + autfilt -q --included-in=proof.hoa trace.hoa && exit 1 +done + : diff --git a/tests/python/forq_contains.py b/tests/python/forq_contains.py index 3e47bec87..8525f3f92 100644 --- a/tests/python/forq_contains.py +++ b/tests/python/forq_contains.py @@ -324,3 +324,28 @@ State: 11 {0} --END--""") do_symmetric_test(subset, superset) + + +tba = spot.translate('GFa') +tgba = spot.translate('GFa & GFb') +tc.assertTrue(spot.contains(tba, tgba)) +try: + spot.containment_select_version("fork") +except RuntimeError as e: + tc.assertIn("forq", str(e)) +else: + raise RuntimeError("missing exception") +spot.containment_select_version("forq") +tc.assertTrue(spot.contains(tba, tgba)) # does not call contains_forq +try: + spot.contains_forq(tba, tgba) # because contains_forq wants Büchi +except RuntimeError as e: + tc.assertIn("Büchi", str(e)) +else: + raise RuntimeError("missing exception") + +# This shows that exclusive word also depend on +# containment_select_version() +tc.assertEqual(str(one.exclusive_word(both)), "!a & !b; cycle{a}") +spot.containment_select_version("default") +tc.assertEqual(str(one.exclusive_word(both)), "cycle{a}")