From 2ae1b6a6f0ee8bd72cc865903128ed20e8fa88a0 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 15 Oct 2015 13:58:20 +0200 Subject: [PATCH] autfilt: implement --complement * src/bin/autfilt.cc: Add option --complete. * src/twaalgos/complete.cc: Better handling of 0-edge automata. * src/tests/complement.test: New file. * src/tests/Makefile.am: Add it. --- NEWS | 7 +++ src/bin/autfilt.cc | 20 ++++++++ src/tests/Makefile.am | 1 + src/tests/complement.test | 98 +++++++++++++++++++++++++++++++++++++++ src/twaalgos/complete.cc | 10 ++++ 5 files changed, 136 insertions(+) create mode 100755 src/tests/complement.test diff --git a/NEWS b/NEWS index a87401652..62e6d647e 100644 --- a/NEWS +++ b/NEWS @@ -1,5 +1,12 @@ New in spot 1.99.4a (not yet released) + Command-line tools: + + * autfilt has gained a --complement option. + It currently work only for deterministic automata. + + Library: + * Rename dtgba_complement() as dtwa_complement(), rename the header as complement.hh, and restrict the purpose of this function to just complete the automaton and complement its acceptance diff --git a/src/bin/autfilt.cc b/src/bin/autfilt.cc index 39c04d214..9ef68a3b2 100644 --- a/src/bin/autfilt.cc +++ b/src/bin/autfilt.cc @@ -55,6 +55,7 @@ #include "twaalgos/remfin.hh" #include "twaalgos/cleanacc.hh" #include "twaalgos/dtgbasat.hh" +#include "twaalgos/complement.hh" static const char argp_program_doc[] ="\ Convert, transform, and filter Büchi automata.\v\ @@ -69,6 +70,7 @@ enum { OPT_ARE_ISOMORPHIC, OPT_CLEAN_ACC, OPT_CNF_ACC, + OPT_COMPLEMENT, OPT_COMPLEMENT_ACC, OPT_COUNT, OPT_DESTUT, @@ -152,6 +154,9 @@ static const argp_option options[] = "rewrite the automaton without using Fin acceptance", 0 }, { "cleanup-acceptance", OPT_CLEAN_ACC, nullptr, 0, "remove unused acceptance sets from the automaton", 0 }, + { "complement", OPT_COMPLEMENT, nullptr, 0, + "complement each automaton (currently support only deterministic " + "automata)", 0 }, { "complement-acceptance", OPT_COMPLEMENT_ACC, nullptr, 0, "complement the acceptance condition (without touching the automaton)", 0 }, @@ -264,6 +269,7 @@ static bool opt_dnf_acc = false; static bool opt_cnf_acc = false; static bool opt_rem_fin = false; static bool opt_clean_acc = false; +static bool opt_complement = false; static bool opt_complement_acc = false; static spot::acc_cond::mark_t opt_mask_acc = 0U; static std::vector opt_keep_states = {}; @@ -324,6 +330,9 @@ parse_opt(int key, char* arg, struct argp_state*) opt_dnf_acc = false; opt_cnf_acc = true; break; + case OPT_COMPLEMENT: + opt_complement = true; + break; case OPT_COMPLEMENT_ACC: opt_complement_acc = true; break; @@ -537,6 +546,17 @@ namespace if (opt_complement_acc) aut->set_acceptance(aut->acc().num_sets(), aut->get_acceptance().complement()); + if (opt_complement) + { + if (!spot::is_deterministic(aut)) + { + std::cerr << filename << ':' + << haut->loc << (": --complement currently supports " + "only deterministic automata\n"); + exit(2); + } + aut = spot::dtwa_complement(aut); + } if (opt_rem_fin) aut = remove_fin(aut); if (opt_dnf_acc) diff --git a/src/tests/Makefile.am b/src/tests/Makefile.am index 4ff21b10d..05ab8a19b 100644 --- a/src/tests/Makefile.am +++ b/src/tests/Makefile.am @@ -174,6 +174,7 @@ TESTS_twa = \ parseaut.test \ optba.test \ complete.test \ + complement.test \ remfin.test \ dstar.test \ readsave.test \ diff --git a/src/tests/complement.test b/src/tests/complement.test new file mode 100755 index 000000000..91e4579e0 --- /dev/null +++ b/src/tests/complement.test @@ -0,0 +1,98 @@ +#!/bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) 2015 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 + +set -e + +autfilt=../../bin/autfilt +ltl2tgba=../../bin/ltl2tgba +randaut=../../bin/randaut + +$randaut -H -A 'random 0..4' -Q1..10 -D -n 50 0..2 >aut +run 0 $autfilt --complement -H aut >/dev/null + +cat >in <out +cat >expected <out +cat >expected <out && exit 1 +grep 'deterministic' out diff --git a/src/twaalgos/complete.cc b/src/twaalgos/complete.cc index 01d103837..153b399df 100644 --- a/src/twaalgos/complete.cc +++ b/src/twaalgos/complete.cc @@ -23,6 +23,11 @@ namespace spot { unsigned complete_here(twa_graph_ptr aut) { + // We do not use the initial state, but calling + // get_init_state_number() may create it and change the number of + // states. This has to be done before calling aut->num_states(). + unsigned init = aut->get_init_state_number(); + unsigned n = aut->num_states(); unsigned sink = -1U; @@ -69,6 +74,11 @@ namespace spot unsigned t = aut->num_edges(); + // If the automaton is empty, + // pretend that state + if (t == 0) + sink = init; + // Now complete all states (excluding any newly added the sink). for (unsigned i = 0; i < n; ++i) {