From a4d1e18bf31df23325ea4c62377072ac7815a584 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 23 Oct 2011 23:06:35 +0200 Subject: [PATCH] Safra: Fix usage of multiple acceptance conditions and fix text output. * src/tgba/tgbasafracomplement.cc (tgba_safra_complement::tgba_safra_complement) (tgba_safra_complement::succ_iter): Correct the declaration and use of multiple acceptance conditions. (state_complement::to_string): Output the L set, not U. The previous code caused different states to share the same names, causing issues with the text-based output (state with identical names get merged). * src/tgba/tgbasafracomplement.hh (tgba_safra_complement::acceptance_cond_vec_): Adjust type to store BDDs. * src/tgbatest/complementation.cc: Implement a new "-b" option to output automata in Spot's syntax. * src/tgbatest/complementation.test: Add a test-case supplied by Martin Dieguez Lodeiro. * THANKS: Add Martin. --- ChangeLog | 20 ++++++++++++++++++ THANKS | 1 + src/tgba/tgbasafracomplement.cc | 35 ++++++++++++++----------------- src/tgba/tgbasafracomplement.hh | 4 ++-- src/tgbatest/complementation.cc | 16 +++++++++++++- src/tgbatest/complementation.test | 24 ++++++++++++++++++++- 6 files changed, 77 insertions(+), 23 deletions(-) diff --git a/ChangeLog b/ChangeLog index 7d74d6520..470bc2b38 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,23 @@ +2011-10-23 Alexandre Duret-Lutz + + Safra: Fix usage of multiple acceptance conditions and fix text output. + + * src/tgba/tgbasafracomplement.cc + (tgba_safra_complement::tgba_safra_complement) + (tgba_safra_complement::succ_iter): Correct the declaration and + use of multiple acceptance conditions. + (state_complement::to_string): Output the L set, not U. The previous + code caused different states to share the same names, causing issues + with the text-based output (state with identical names get merged). + * src/tgba/tgbasafracomplement.hh + (tgba_safra_complement::acceptance_cond_vec_): Adjust type to + store BDDs. + * src/tgbatest/complementation.cc: Implement a new "-b" option + to output automata in Spot's syntax. + * src/tgbatest/complementation.test: Add a test-case supplied + by Martin Dieguez Lodeiro. + * THANKS: Add Martin. + 2011-10-23 Alexandre Duret-Lutz * src/tgba/tgbasafracomplement.cc: Fix two asserts. diff --git a/THANKS b/THANKS index d9eb79096..f21a498f6 100644 --- a/THANKS +++ b/THANKS @@ -5,6 +5,7 @@ Heikki Tauriainen Jean-Michel Couvreur Jean-Michel Ilié Kristin Y. Rozier +Martin Dieguez Lodeiro Michael Weber Rüdiger Ehlers Silien Hong diff --git a/src/tgba/tgbasafracomplement.cc b/src/tgba/tgbasafracomplement.cc index 9cfe57370..921f7c126 100644 --- a/src/tgba/tgbasafracomplement.cc +++ b/src/tgba/tgbasafracomplement.cc @@ -942,8 +942,7 @@ namespace spot if (other == this) return 0; const state_complement* s = down_cast(other); - if (s == 0) - return 1; + assert(s); #if TRANSFORM_TO_TBA // When we transform to TBA instead of TGBA, states depend on the U set. if (U != s->U) @@ -993,9 +992,9 @@ namespace spot ss << tree; if (use_bitset) { - ss << " - I:" << U; + ss << " - I:" << L; #if TRANSFORM_TO_TBA - ss << " J:" << L; + ss << " J:" << U; #endif } return ss.str(); @@ -1147,14 +1146,19 @@ namespace spot neg_acceptance_cond_ = bddtrue; acceptance_cond_vec_.reserve(nb_acc); for (unsigned i = 0; i < nb_acc; ++i) - { - int r = get_dict()->register_clone_acc(v, safra_); - all_acceptance_cond_ |= bdd_ithvar(r); - acceptance_cond_vec_[i] = r; - neg_acceptance_cond_ &= bdd_nithvar(r); - } + { + int r = get_dict()->register_clone_acc(v, safra_); + all_acceptance_cond_ &= bdd_nithvar(r); + all_acceptance_cond_ |= bdd_ithvar(r) & neg_acceptance_cond_; + neg_acceptance_cond_ &= bdd_nithvar(r); + acceptance_cond_vec_.push_back(bdd_ithvar(r)); + } + for (unsigned i = 0; i < nb_acc; ++i) + { + bdd c = acceptance_cond_vec_[i]; + acceptance_cond_vec_[i] = bdd_exist(neg_acceptance_cond_, c) & c; + } #endif - } tgba_safra_complement::~tgba_safra_complement() @@ -1278,15 +1282,8 @@ namespace spot } for (unsigned i = 0; i < l.size(); ++i) - { if (!S[i]) - { - if (condition == bddfalse) - condition = bdd_ithvar(acceptance_cond_vec_[i]); - else - condition &= bdd_ithvar(acceptance_cond_vec_[i]); - } - } + condition |= acceptance_cond_vec_[i]; #endif } diff --git a/src/tgba/tgbasafracomplement.hh b/src/tgba/tgbasafracomplement.hh index 5f6b41374..8e80dedae 100644 --- a/src/tgba/tgbasafracomplement.hh +++ b/src/tgba/tgbasafracomplement.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement +// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -84,7 +84,7 @@ namespace spot bdd all_acceptance_cond_; bdd neg_acceptance_cond_; // Map to i the i-th acceptance condition of the final automaton. - std::vector acceptance_cond_vec_; + std::vector acceptance_cond_vec_; #endif }; diff --git a/src/tgbatest/complementation.cc b/src/tgbatest/complementation.cc index 2f3af378b..05dfaa24d 100644 --- a/src/tgbatest/complementation.cc +++ b/src/tgbatest/complementation.cc @@ -21,6 +21,7 @@ #include #include #include "tgbaalgos/dotty.hh" +#include "tgbaalgos/save.hh" #include "tgbaparse/public.hh" #include "tgba/tgbaproduct.hh" #include "tgbaalgos/gtec/gtec.hh" @@ -40,6 +41,7 @@ void usage(const char* prog) { std::cout << "usage: " << prog << " [options]" << std::endl; std::cout << "with options" << std::endl + << "-b Output in spot's format" << std::endl << "-S Use Safra's complementation " << "instead of Kupferman&Vardi's" << std::endl << "-s buchi_automaton display the safra automaton" @@ -63,6 +65,7 @@ int main(int argc, char* argv[]) bool formula = false; bool safra = false; bool print_formula = false; + bool save_spot = false; if (argc < 3) { @@ -74,6 +77,12 @@ int main(int argc, char* argv[]) { if (argv[i][0] == '-') { + if (strcmp(argv[i] + 1, "b") == 0) + { + save_spot = true; + continue; + } + if (strcmp(argv[i] + 1, "astat") == 0) { stats = true; @@ -134,7 +143,12 @@ int main(int argc, char* argv[]) complement = new spot::tgba_kv_complement(a); if (print_automaton) - spot::dotty_reachable(std::cout, complement); + { + if (save_spot) + spot::tgba_save_reachable(std::cout, complement); + else + spot::dotty_reachable(std::cout, complement); + } if (print_safra) { diff --git a/src/tgbatest/complementation.test b/src/tgbatest/complementation.test index 578f3fee4..dfab0b884 100755 --- a/src/tgbatest/complementation.test +++ b/src/tgbatest/complementation.test @@ -1,5 +1,5 @@ #!/bin/sh -# Copyright (C) 2009 Laboratoire de Recherche et Développement +# Copyright (C) 2009, 2011 Laboratoire de Recherche et Développement # de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -42,3 +42,25 @@ GFa&&FGa [] (p2 -> ((! p0 && ! p1) U (p1 || ((p0 && ! p1) U (p1 || ((! p0 && ! p1) \ U (p1 || ((p0 && ! p1) U ((p1 || (! p0 U (p1 || [] ! p0))) || [] p0))))))))) EOF + + + +# The following test-case was supplied by Martin Dieguez Lodeiro to +# demonstrate a bug in our Safra implementation. +cat >x.tgba < nx.tgba +run 0 ../ltl2tgba -X -e nx.tgba +# however the intersection of both should not +# accept any run. +run 0 ../ltl2tgba -X -E -Pnx.tgba x.tgba