From 78e76eb07db04617ca8cca89c217348fae8e8ec0 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 3 Feb 2013 00:16:32 +0100 Subject: [PATCH] dbacomp: connect only back-links and generalize to tgba * src/tgbaalgos/dbacomp.cc: Here. * src/tgbaalgos/dbacomp.hh: Adjust documentation. * src/tgbatest/dbacomp.test: New file. * src/tgbatest/Makefile.am (TESTS): Add it. * src/tgbatest/det.test: Update. --- src/tgbaalgos/dbacomp.cc | 93 +++++++++++++++++++++++++++------------ src/tgbaalgos/dbacomp.hh | 10 ++--- src/tgbatest/Makefile.am | 1 + src/tgbatest/dbacomp.test | 46 +++++++++++++++++++ src/tgbatest/det.test | 25 ++++++++++- 5 files changed, 140 insertions(+), 35 deletions(-) create mode 100755 src/tgbatest/dbacomp.test diff --git a/src/tgbaalgos/dbacomp.cc b/src/tgbaalgos/dbacomp.cc index 8632c0358..c1be952d7 100644 --- a/src/tgbaalgos/dbacomp.cc +++ b/src/tgbaalgos/dbacomp.cc @@ -26,37 +26,32 @@ namespace spot namespace { - class dbacomp_iter: public tgba_reachable_iterator_depth_first + class dbacomp_iter: public tgba_reachable_iterator_depth_first_stack { bdd orig_acc_; + bdd all_neg_; bdd acc_; bdd_dict* dict_; tgba_explicit_number* out_; + int num_acc_; + typedef state_explicit_number::transition trans; public: dbacomp_iter(const tgba* a) - : tgba_reachable_iterator_depth_first(a), + : tgba_reachable_iterator_depth_first_stack(a), dict_(a->get_dict()), out_(new tgba_explicit_number(dict_)) { dict_->register_all_variables_of(a, out_); - unsigned c = a->number_of_acceptance_conditions(); orig_acc_ = a->all_acceptance_conditions(); - if (c == 1) - { - out_->copy_acceptance_conditions_of(a); - acc_ = orig_acc_; - } - else - { - // If there is no acceptance conditions in the original - // automaton, add one. - assert(c == 0); - int accvar = dict_->register_acceptance_variable - (ltl::constant::true_instance(), out_); - acc_ = bdd_ithvar(accvar); - out_->set_acceptance_conditions(acc_); - } + all_neg_ = a->neg_acceptance_conditions(); + num_acc_ = a->number_of_acceptance_conditions(); + + // Register one acceptance condition for the result. + int accvar = dict_->register_acceptance_variable + (ltl::constant::true_instance(), out_); + acc_ = bdd_ithvar(accvar); + out_->set_acceptance_conditions(acc_); } tgba_explicit_number* @@ -106,19 +101,61 @@ namespace spot trans* t1 = out_->create_transition(in, out); t1->condition = si->current_condition(); - // Negative states encode a copy of the automaton in which all - // accepting transitions have been removed, and all the - // remaining transitions are now accepting. + // Negative states encode NUM_ACC_ copies of the automaton. + // In each copy transitions labeled by one of the acceptance + // set have been removed, and all the remaining transitions + // are now accepting. + // For each state S, we have NUM_ACC_ additional copies + // labeled S*-NUM_ACC, S*-NUM_ACC+1, ... S*-NUM_ACC+(NUM_ACC-1), if (a != orig_acc_) { - trans* t2 = out_->create_transition(-in, -out); - t2->condition = si->current_condition(); - t2->acceptance_conditions = acc_; - } + bool backlink = on_stack(out); + int add = 0; + if (a == bddfalse) + a = all_neg_; + // Iterate over all the acceptance conditions in 'a'. + bdd ac = a; + while (ac != bddtrue) + { + bdd h = bdd_high(ac); + if (h == bddfalse) + { + trans* t2 = out_->create_transition(in * -num_acc_ + add, + out * -num_acc_ + add); + t2->condition = si->current_condition(); + t2->acceptance_conditions = acc_; - // A non-deterministic transition between the two copies. - trans* t3 = out_->create_transition(in, -out); - t3->condition = si->current_condition(); + if (backlink) + { + // Since we are closing a cycle, add + // a non-deterministic transition from + // the original automaton to this copy. + trans* t3 = + out_->create_transition(in, out * -num_acc_ + add); + t3->condition = si->current_condition(); + } + ac = bdd_low(ac); + } + else + { + // We know that only one variable can be positive + // on any branch, so since we have just seen such + // a variable, we want to go to explore its LOW + // branch for more positive variables. The only + // case where we will not do that is if the LOW + // branch is false. In that case we take the HIGH + // branch to enumerate all the remaining negated + // variables. + bdd tmp = bdd_low(ac); + if (tmp != bddfalse) + ac = tmp; + else + ac = h; + } + ++add; + } + assert(add == num_acc_); + } } }; diff --git a/src/tgbaalgos/dbacomp.hh b/src/tgbaalgos/dbacomp.hh index 62f45a14b..0a7ac6ee0 100644 --- a/src/tgbaalgos/dbacomp.hh +++ b/src/tgbaalgos/dbacomp.hh @@ -24,13 +24,11 @@ namespace spot { - - - /// Complement a deterministic Büchi automaton + /// \brief Complement a deterministic Büchi automaton /// - /// The automaton \a aut should be deterministic and should have at - /// most a single acceptance condition. It can be transition-based, - /// or state-based. The resulting automaton is very unlikely to be + /// The automaton \a aut should be deterministic. It does no need + /// to be complete. Acceptance can be transition-based, or + /// state-based. The resulting automaton is very unlikely to be /// deterministic. SPOT_API tgba_explicit_number* dba_complement(const tgba* aut); diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index 75b3804a4..5caa5034c 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -107,6 +107,7 @@ TESTS = \ lbttparse.test \ scc.test \ sccsimpl.test \ + dbacomp.test \ obligation.test \ wdba.test \ wdba2.test \ diff --git a/src/tgbatest/dbacomp.test b/src/tgbatest/dbacomp.test new file mode 100755 index 000000000..c529a9ca5 --- /dev/null +++ b/src/tgbatest/dbacomp.test @@ -0,0 +1,46 @@ +#!/bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) 2013 Laboratoire de Recherche et +# Développement de l'Epita (LRDE). +# +# This file is part of Spot, a model checking library. +# +# Spot is free software; you can redistribute it and/or modify it +# under the terms of the GNU General Public License as published by +# the Free Software Foundation; either version 3 of the License, or +# (at your option) any later version. +# +# Spot is distributed in the hope that it will be useful, but WITHOUT +# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +# License for more details. +# +# You should have received a copy of the GNU General Public License +# along with this program. If not, see . + +. ./defs + +# This automaton used to trigger a bug in the complementation: its +# intersection with the complement was not empty! +cat >input.tgba <ex.tgba <<'EOF' acc = "1"; "1", "2", "a",; @@ -76,13 +77,35 @@ acc = "1"; "1", "-1", "!a",; "2", "3", "a",; "2", "1", "!a",; +"2", "-1", "!a",; "-1", "-1", "!a", "1"; "3", "3", "a",; "3", "-3", "a",; "3", "1", "!a",; +"3", "-1", "!a",; "-3", "-3", "a", "1"; "-3", "-1", "!a", "1"; EOF run 0 ../ltl2tgba -b -DC -X in.tgba > out.tgba -cmp out.tgba ex.tgba +diff out.tgba ex.tgba + + +run 0 ../ltl2tgba -x -DC 'GFa & XGFb' > out.tgba +cat >ex.tgba < 1 + 1 [label="1"] + 1 -> 2 [label="1\n"] + 2 [label="2"] + 2 -> 2 [label="1\n"] + 2 -> 3 [label="!a\n"] + 2 -> 4 [label="!b\n"] + 3 [label="-4"] + 3 -> 3 [label="!a\n{Acc[1]}"] + 4 [label="-3"] + 4 -> 4 [label="!b\n{Acc[1]}"] +} +EOF +diff out.tgba ex.tgba