alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

forq: make it easier to select contains's version

Browse source 
* spot/twaalgos/contains.hh, spot/twaalgos/contains.cc
(containment_select_version): New function.
(contains): Use it.
* spot/twa/twa.cc (exclusive_word): Likewise.
* bin/autfilt.cc (--included-in): Adjust to use forq depending
on containement_select_version.
* bin/man/spot-x.x: Adjust documentation of
CONTAINMENT_SELECT_VERSION.
* tests/core/included.test, tests/python/forq_contains.py: Add more
tests.
* NEWS: Mention the new feature.
This commit is contained in:
Alexandre Duret-Lutz 2023-09-07 17:36:09 +02:00
parent ca4e6c4b48
commit 05d7622f8f
8 changed files with 178 additions and 83 deletions
Download patch file Download diff file Expand all files Collapse all files

13
NEWS
View file

@ -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

22
bin/autfilt.cc
View file

@ -45,6 +45,7 @@
#include <spot/misc/timer.hh>
#include <spot/parseaut/public.hh>
#include <spot/tl/exclusive.hh>
#include <spot/twaalgos/alternation.hh>
#include <spot/twaalgos/are_isomorphic.hh>
#include <spot/twaalgos/canonicalize.hh>
#include <spot/twaalgos/cobuchi.hh>
@ -984,13 +985,25 @@ 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);
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
{
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:
opt_inhweak_sccs = parse_range(arg, 0, std::numeric_limits<int>::max());
@ -1519,7 +1532,12 @@ namespace
if (opt->intersect)
matched &= aut->intersects(opt->intersect);
if (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);

31
bin/man/spot-x.x
View file

@ -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)

34
spot/twa/twa.cc
View file

@ -29,6 +29,7 @@
#include <spot/twaalgos/alternation.hh>
#include <spot/twa/twaproduct.hh>
#include <spot/twaalgos/forq_contains.hh>
#include <spot/twaalgos/contains.hh>
#include <spot/twaalgos/complement.hh>
#include <spot/twaalgos/isdet.hh>
#include <spot/twaalgos/product.hh>
@ -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<containment_type>(*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<const twa_graph>(a);
auto b_twa_as_graph = std::dynamic_pointer_cast<const twa_graph>(b);
if (a_twa_as_graph)
if (auto a_twa_as_graph = std::dynamic_pointer_cast<const twa_graph>(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
{

68
spot/twaalgos/contains.cc
View file

@ -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,40 +33,26 @@ namespace spot
{
return ltl_to_tgba_fm(f, dict);
}
}
static bool is_buchi_automata(const_twa_graph_ptr const& aut)
static const_twa_graph_ptr
ensure_graph(const const_twa_ptr& aut_in)
{
return spot::acc_cond::acc_code::buchi() == aut->get_acceptance();
const_twa_graph_ptr aut =
std::dynamic_pointer_cast<const twa_graph>(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");
if (containment_select_version() == 1
&& left->acc().is_buchi() && right->acc().is_buchi())
return contains_forq(left, ensure_graph(right));
else
return static_cast<containment_type>(*s - '0');
}();
auto as_graph = std::dynamic_pointer_cast<const twa_graph>(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)
{
@ -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;
}
}

30
spot/twaalgos/contains.hh
View file

@ -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);
}

26
tests/core/included.test
View file

@ -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
:

25
tests/python/forq_contains.py
View file

@ -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}")