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

twa: introduce intersects() and friends

Browse source 
* spot/twa/twa.hh, spot/twa/twa.cc (intersects, intersecting_run,
intersecting_word): New functions.
* NEWS: Mention them.
* doc/org/tut51.org, tests/python/bugdet.py: Use them.
This commit is contained in:
Alexandre Duret-Lutz 2016-11-13 11:23:12 +01:00
parent bdad288c70
commit c225747749
5 changed files with 138 additions and 64 deletions
Download patch file Download diff file Expand all files Collapse all files

12
NEWS
View file

@ -47,6 +47,18 @@ New in spot 2.1.2.dev (not yet released)
to setjmp are now avoided when variable reordering is disabled
(the default).
* The twa class has three new methods:
aut->intersects(other)
aut->intersecting_run(other)
aut->intersecting_word(other)
currently these are just convenient wrappers around
!otf_product(aut, other)->is_empty()
otf_product(aut, other)->accepting_run()->project(aut)
otf_product(aut, other)->accepting_word()
with any Fin-acceptance removal performed before the
product. However the plan is that these can be implemented
more efficiently in the future.
Bugs:
* ltl2tgba was always using the highest settings for the LTL

77
doc/org/tut51.org
View file

@ -438,21 +438,12 @@ counterexample:
spot::formula f = spot::formula::Not(pf.f);
spot::twa_graph_ptr af = spot::translator(d).run(f);
// Construct an "on-the-fly product"
// Find a run of or demo_kripke that intersects af.
auto k = std::make_shared<demo_kripke>(d);
auto p = spot::otf_product(k, af);
if (auto run = p->accepting_run())
{
std::cout << "formula is violated by the following run:\n";
// "run" is an accepting run over the product. Project it on
// the Kripke structure before displaying it.
std::cout << *run->project(k);
}
if (auto run = k->intersecting_run(af))
std::cout << "formula is violated by the following run:\n" << *run;
else
{
std::cout << "formula is verified\n";
}
std::cout << "formula is verified\n";
}
#+END_SRC
@ -496,38 +487,38 @@ passing the option "~k~" to =print_dot()= will fix that.
<<demo-succ-iter-2>>
#+END_SRC
#+NAME: demo-3
#+BEGIN_SRC C++ :exports code :noweb strip-export :results verbatim
#include <spot/twaalgos/dot.hh>
#include <spot/tl/parse.hh>
#include <spot/twaalgos/translate.hh>
#include <spot/twa/twaproduct.hh>
#include <spot/twaalgos/emptiness.hh>
#include <spot/twaalgos/copy.hh>
<<demo-3-aux>>
int main()
{
auto d = spot::make_bdd_dict();
#+NAME: demo-3
#+BEGIN_SRC C++ :exports code :noweb strip-export :results verbatim
#include <spot/twaalgos/dot.hh>
#include <spot/tl/parse.hh>
#include <spot/twaalgos/translate.hh>
#include <spot/twa/twaproduct.hh>
#include <spot/twaalgos/emptiness.hh>
#include <spot/twaalgos/copy.hh>
<<demo-3-aux>>
int main()
{
auto d = spot::make_bdd_dict();
// Parse the input formula.
spot::parsed_formula pf = spot::parse_infix_psl("GF(odd_x) -> GF(odd_y)");
if (pf.format_errors(std::cerr))
return 1;
// Parse the input formula.
spot::parsed_formula pf = spot::parse_infix_psl("GF(odd_x) -> GF(odd_y)");
if (pf.format_errors(std::cerr))
return 1;
// Translate its negation.
spot::formula f = spot::formula::Not(pf.f);
spot::twa_graph_ptr af = spot::translator(d).run(f);
// Translate its negation.
spot::formula f = spot::formula::Not(pf.f);
spot::twa_graph_ptr af = spot::translator(d).run(f);
// Construct an "on-the-fly product"
auto k = spot::copy(std::make_shared<demo_kripke>(d), spot::twa::prop_set::all(), true);
auto p = spot::otf_product(k, af);
if (auto run = p->accepting_run())
{
run->project(k)->highlight(5); // 5 is a color number.
spot::print_dot(std::cout, k, ".k");
}
}
// Convert demo_kripke into an explicit graph
spot::twa_graph_ptr k = spot::copy(std::make_shared<demo_kripke>(d),
spot::twa::prop_set::all(), true);
// Find a run of or demo_kripke that intersects af.
if (auto run = k->intersecting_run(af))
{
run->highlight(5); // 5 is a color number.
spot::print_dot(std::cout, k, ".k");
}
}
#+END_SRC
#+BEGIN_SRC dot :file kripke-3.png :cmdline -Tpng :cmd circo :var txt=demo-3 :exportss results
@ -537,7 +528,7 @@ passing the option "~k~" to =print_dot()= will fix that.
#+RESULTS:
[[file:kripke-3.png]]
1
* Possible improvements
The on-the-fly interface, especially as implemented here, involves a

65
spot/twa/twa.cc
View file

@ -25,6 +25,7 @@
#include <spot/twaalgos/gtec/gtec.hh>
#include <spot/twaalgos/word.hh>
#include <spot/twaalgos/remfin.hh>
#include <spot/twa/twaproduct.hh>
#include <utility>
namespace spot
@ -44,6 +45,20 @@ namespace spot
get_dict()->unregister_all_my_variables(this);
}
namespace
{
const_twa_ptr remove_fin_maybe(const const_twa_ptr& a)
{
if (!a->acc().uses_fin_acceptance())
return a;
auto aa = std::dynamic_pointer_cast<const twa_graph>(a);
if (!aa)
aa = make_twa_graph(a, twa::prop_set::all());
return remove_fin(aa);
}
}
state*
twa::project_state(const state* s,
const const_twa_ptr& t) const
@ -59,15 +74,7 @@ namespace spot
// FIXME: This should be improved based on properties of the
// automaton. For instance we do not need couvreur99 is we know
// the automaton is weak.
auto a = shared_from_this();
if (a->acc().uses_fin_acceptance())
{
auto aa = std::dynamic_pointer_cast<const twa_graph>(a);
if (!aa)
aa = make_twa_graph(a, prop_set::all());
a = remove_fin(aa);
}
return !couvreur99(a)->check();
return !couvreur99(remove_fin_maybe(shared_from_this()))->check();
}
twa_run_ptr
@ -86,15 +93,7 @@ namespace spot
twa_word_ptr
twa::accepting_word() const
{
auto a = shared_from_this();
if (a->acc().uses_fin_acceptance())
{
auto aa = std::dynamic_pointer_cast<const twa_graph>(a);
if (!aa)
aa = make_twa_graph(a, prop_set::all());
a = remove_fin(aa);
}
if (auto run = a->accepting_run())
if (auto run = remove_fin_maybe(shared_from_this())->accepting_run())
{
auto w = make_twa_word(run->reduce());
w->simplify();
@ -106,6 +105,36 @@ namespace spot
}
}
bool
twa::intersects(const_twa_ptr other) const
{
auto a1 = remove_fin_maybe(shared_from_this());
auto a2 = remove_fin_maybe(other);
return !otf_product(a1, a2)->is_empty();
}
twa_run_ptr
twa::intersecting_run(const_twa_ptr other, bool from_other) const
{
auto a = shared_from_this();
if (from_other)
other = remove_fin_maybe(other);
else
a = remove_fin_maybe(a);
auto run = otf_product(a, other)->accepting_run();
if (!run)
return nullptr;
return run->project(from_other ? other : a);
}
twa_word_ptr
twa::intersecting_word(const_twa_ptr other) const
{
auto a1 = remove_fin_maybe(shared_from_this());
auto a2 = remove_fin_maybe(other);
return otf_product(a1, a2)->accepting_word();
}
void
twa::set_named_prop(std::string s, std::nullptr_t)
{

44
spot/twa/twa.hh
View file

@ -824,17 +824,23 @@ namespace spot
///@}
/// \brief Check whether the language of the automaton is empty.
///
/// If you are calling this method on a product of two automata,
/// consider using intersects() instead.
virtual bool is_empty() const;
/// \brief Return an accepting run if one exists.
///
/// Note that this method currently onky works for Fin-less
/// Note that this method currently only works for Fin-less
/// acceptance. For acceptance conditions that contain Fin
/// acceptance, you can either rely on is_empty() and not use any
/// accepting run, or remove Fin acceptance using remove_fin() and
/// compute an accepting run on that larger automaton.
///
/// Return nullptr if no accepting run were found.
///
/// If you are calling this method on a product of two automata,
/// consider using intersecting_run() instead.
virtual twa_run_ptr accepting_run() const;
/// \brief Return an accepting word if one exists.
@ -843,8 +849,44 @@ namespace spot
/// acceptance.
///
/// Return nullptr if no accepting word were found.
///
/// If you are calling this method on a product of two automata,
/// consider using intersecting_word() instead.
virtual twa_word_ptr accepting_word() const;
/// \brief Check whether the language of this automaton intersects
/// that of the \a other automaton.
virtual bool intersects(const_twa_ptr other) const;
/// \brief Return an accepting run recognizing a word accepted by
/// two automata.
///
/// If \a from_other is true, the returned run will be over the
/// \a other automaton. Otherwise, the run will be over this
/// automaton.
///
/// Note that this method currently only works if the automaton
/// from which the accepting run is extracted uses Fin-less acceptance.
/// (The other automaton can have any acceptance condition.)
///
/// For acceptance conditions that contain Fin acceptance, you can
/// either rely on intersects() and not use any accepting run, or
/// remove Fin acceptance using remove_fin() and compute an
/// intersecting run on this larger automaton.
///
/// Return nullptr if no accepting run were found.
virtual twa_run_ptr intersecting_run(const_twa_ptr other,
bool from_other = false) const;
/// \brief Return a word accepted by two automata.
///
/// Note that this method DOES works with Fin
/// acceptance.
///
/// Return nullptr if no accepting word were found.
virtual twa_word_ptr intersecting_word(const_twa_ptr other) const;
private:
acc_cond acc_;

4
tests/python/bugdet.py
View file

@ -82,10 +82,10 @@ print("use_simulation=True")
b1 = spot.tgba_determinize(b, False, True, True, True)
assert b1.num_states() == 5
b1 = spot.remove_fin(spot.dtwa_complement(b1))
assert spot.otf_product(a, b1).is_empty() == True
assert not a.intersects(b1);
print("\nuse_simulation=False")
b2 = spot.tgba_determinize(b, False, True, False, True)
assert b2.num_states() == 5
b2 = spot.remove_fin(spot.dtwa_complement(b2))
assert spot.otf_product(a, b1).is_empty() == True
assert not a.intersects(b1);