Commit 2ae1b6a6 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

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.
parent 6cf807da
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
......
......@@ -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<bool> 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)
......
......@@ -174,6 +174,7 @@ TESTS_twa = \
parseaut.test \
optba.test \
complete.test \
complement.test \
remfin.test \
dstar.test \
readsave.test \
......
#!/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 <http://www.gnu.org/licenses/>.
. ./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 <<EOF
HOA: v1
States: 0
Acceptance: 0 t
--BODY--
--END--
EOF
$autfilt --complement -H in >out
cat >expected <<EOF
HOA: v1
States: 1
Start: 0
AP: 0
acc-name: all
Acceptance: 0 t
properties: trans-labels explicit-labels state-acc complete
properties: deterministic
--BODY--
State: 0
[t] 0
--END--
EOF
diff out expected
$ltl2tgba -H 'GFa & GFb' Xa | $autfilt --complement -H >out
cat >expected <<EOF
HOA: v1
States: 1
Start: 0
AP: 2 "a" "b"
acc-name: generalized-co-Buchi 2
Acceptance: 2 Fin(0)|Fin(1)
properties: trans-labels explicit-labels trans-acc complete
properties: deterministic
--BODY--
State: 0
[0&1] 0 {0 1}
[!0&!1] 0
[!0&1] 0 {1}
[0&!1] 0 {0}
--END--
HOA: v1
States: 4
Start: 1
AP: 1 "a"
acc-name: co-Buchi
Acceptance: 1 Fin(0)
properties: trans-labels explicit-labels state-acc complete
properties: deterministic
--BODY--
State: 0
[0] 2
[!0] 3
State: 1
[t] 0
State: 2 {0}
[t] 2
State: 3
[t] 3
--END--
EOF
diff out expected
$ltl2tgba -H 'FGa' | $autfilt --complement 2>out && exit 1
grep 'deterministic' out
......@@ -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)
{
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment