From ad22eb3e650549ec66a9fa7f2631f504427a7f15 Mon Sep 17 00:00:00 2001 From: Jonah Romero Date: Tue, 8 Aug 2023 12:08:28 +0200 Subject: [PATCH] add enviroment variables for FORQ algorithm * AUTHORS: added Jonah Romero * bin/man/spot-x.x: Added the enviroment variables, SPOT_EXCLUSIVE_WORD and SPOT_CONTAINMENT_CHECK * doc/spot.bib: Added paper citation for FORQ inclusion algorithm * spot/twa/twa.cc: Modified exclusive_word to also use FORQ * spot/twaalgos/contains.cc: Modified contains to also use FORQ --- AUTHORS | 1 + bin/man/spot-x.x | 36 +++++++++++++++++++++++++++++ doc/spot.bib | 13 +++++++++++ spot/twa/twa.cc | 48 +++++++++++++++++++++++++++++++++++---- spot/twaalgos/contains.cc | 31 ++++++++++++++++++++++++- 5 files changed, 123 insertions(+), 6 deletions(-) diff --git a/AUTHORS b/AUTHORS index b9b029f9c..d33ca89e1 100644 --- a/AUTHORS +++ b/AUTHORS @@ -18,6 +18,7 @@ Guillaume Sadegh Heikki Tauriainen Henrich Lauko Jérôme Dubois +Jonah Romero Laurent Xu Maximilien Colange Philipp Schlehuber diff --git a/bin/man/spot-x.x b/bin/man/spot-x.x index b961a8ba3..c6091c339 100644 --- a/bin/man/spot-x.x +++ b/bin/man/spot-x.x @@ -50,6 +50,14 @@ time. Note that it restarts all the encoding each time. 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. + .TP \fBSPOT_DEFAULT_FORMAT\fR Set to a value of \fBdot\fR or \fBhoa\fR to override the default @@ -95,6 +103,14 @@ The contents of this variable is added to any dot output, immediately before the first state is output. This makes it easy to override global attributes of the graph. +.TP +\fSPOT_EXCLUSIVE_WORD\fR +Specifies which algorithm spot should use for exclusive_word. 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 assumes buchi +automata in order to find an exclusive word, and will default to the legacy +version if these constraints are not satisfied with the automata passed. + .TP \fBSPOT_HOA_TOLERANT\fR If this variable is set, a few sanity checks performed by the HOA @@ -317,6 +333,26 @@ Describes (among other things) the constructions used for translating formulas of the form GF(guarantee) or FG(safety), that can be disabled with \fB-x gf-guarantee=0\fR. +.TP +6. +Doveri, Kyveli and Ganty, Pierre and Mazzocchi, Nicolas: +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. [SEE ALSO] .BR ltl2tgba (1) diff --git a/doc/spot.bib b/doc/spot.bib index 6193cb1a2..2ca89c721 100644 --- a/doc/spot.bib +++ b/doc/spot.bib @@ -336,6 +336,19 @@ month = aug } +@inproceedings{doveriFORQBasedLanguageInclusion2022, + title = {{{FORQ-Based Language Inclusion Formal Testing}}}, + booktitle = {{{CAV}}'22: {{Proc}}. 32nd {{Int}}. {{Conf}}. on {{Computer Aided Verification}}}, + author = {Doveri, Kyveli and Ganty, Pierre and Mazzocchi, Nicolas}, + year = {2022}, + volume = {13372}, + pages = {109--129}, + publisher = {{Springer International Publishing}}, + doi = {10.1007/978-3-031-13188-2_6}, + urldate = {2022-09-15}, + isbn = {978-3-031-13187-5 978-3-031-13188-2} +} + @InProceedings{ duret.11.vecos, author = {Alexandre Duret-Lutz}, title = {{LTL} Translation Improvements in {Spot}}, diff --git a/spot/twa/twa.cc b/spot/twa/twa.cc index a2ffbc70d..8ebb761f7 100644 --- a/spot/twa/twa.cc +++ b/spot/twa/twa.cc @@ -28,6 +28,7 @@ #include #include #include +#include #include #include #include @@ -228,20 +229,57 @@ namespace spot return b->intersecting_run(complement(ensure_graph(a))); } + static bool + is_buchi_automata(const_twa_graph_ptr const& aut) + { + return spot::acc_cond::acc_code::buchi() == aut->get_acceptance(); + } + twa_word_ptr twa::exclusive_word(const_twa_ptr other) const { 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 is deterministic. - if (auto aa = std::dynamic_pointer_cast(a)) - if (is_deterministic(aa)) + auto a_twa_as_graph = std::dynamic_pointer_cast(a); + auto b_twa_as_graph = std::dynamic_pointer_cast(a); + if (a_twa_as_graph) + if (is_deterministic(a_twa_as_graph)) std::swap(a, b); - if (auto word = a->intersecting_word(complement(ensure_graph(b)))) - return word; - return b->intersecting_word(complement(ensure_graph(a))); + + bool uses_buchi = is_buchi_automata(a_twa_as_graph) + && is_buchi_automata(b_twa_as_graph); + if (containment == containment_type::FORQ + && uses_buchi + && a_twa_as_graph + && b_twa_as_graph) + { + if (auto word = difference_word_forq(a_twa_as_graph, b_twa_as_graph)) + return word; + return difference_word_forq(b_twa_as_graph, a_twa_as_graph); + } + else + { + if (auto word = a->intersecting_word(complement(ensure_graph(b)))) + return word; + return b->intersecting_word(complement(ensure_graph(a))); + } } void diff --git a/spot/twaalgos/contains.cc b/spot/twaalgos/contains.cc index cf2680d01..d30904aa6 100644 --- a/spot/twaalgos/contains.cc +++ b/spot/twaalgos/contains.cc @@ -19,6 +19,7 @@ #include "config.h" #include +#include #include #include #include @@ -34,9 +35,37 @@ namespace spot } } + static bool is_buchi_automata(const_twa_graph_ptr const& aut) + { + return spot::acc_cond::acc_code::buchi() == aut->get_acceptance(); + } + bool contains(const_twa_graph_ptr left, const_twa_ptr right) { - return !complement(left)->intersects(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); + } + else + { + return !complement(left)->intersects(right); + } } bool contains(const_twa_graph_ptr left, formula right)