diff --git a/NEWS b/NEWS index dfbb36451..7bf8994f2 100644 --- a/NEWS +++ b/NEWS @@ -8,6 +8,9 @@ New in spot 2.3.2.dev (not yet released) - In autfilt, the options --sum(--sum-or) and --sum-and are implemented. + - In autfilt, the option --dualize is now available to obtain the dual + of any automaton. + - genltl learned --spec-patterns as an alias for --dac-patterns; it also learned two new sets of LTL formulas under --hkrss-patterns (a.k.a. --liberouter-patterns) and --p-patterns diff --git a/bin/autfilt.cc b/bin/autfilt.cc index ce24b1c4f..5ecbf8a87 100644 --- a/bin/autfilt.cc +++ b/bin/autfilt.cc @@ -91,6 +91,7 @@ enum { OPT_DECOMPOSE_STRENGTH, OPT_DECOMPOSE_SCC, OPT_DESTUT, + OPT_DUALIZE, OPT_DNF_ACC, OPT_EDGES, OPT_EQUIVALENT_TO, @@ -301,6 +302,8 @@ static const argp_option options[] = " (letters may be combined to combine more strengths in the output)", 0 }, { "decompose-scc", OPT_DECOMPOSE_SCC, "N", 0, "keep only the Nth accepting" " SCC as accepting", 0 }, + { "dualize", OPT_DUALIZE, nullptr, 0, + "dualize each automaton", 0 }, { "exclusive-ap", OPT_EXCLUSIVE_AP, "AP,AP,...", 0, "if any of those APs occur in the automaton, restrict all edges to " "ensure two of them may not be true at the same time. Use this option " @@ -485,6 +488,7 @@ static bool opt_complement = false; static bool opt_complement_acc = false; static char* opt_decompose_strength = nullptr; static int opt_decompose_scc = -1; +static bool opt_dualize = false; static spot::acc_cond::mark_t opt_mask_acc = 0U; static std::vector opt_keep_states = {}; static unsigned int opt_keep_states_initial = 0; @@ -572,6 +576,9 @@ parse_opt(int key, char* arg, struct argp_state*) opt_cnf_acc = true; break; case OPT_COMPLEMENT: + if (opt_dualize) + error(2, 0, "either --complement or --dualize options" + " can be given, not both"); opt_complement = true; break; case OPT_COMPLEMENT_ACC: @@ -586,6 +593,12 @@ parse_opt(int key, char* arg, struct argp_state*) case OPT_DESTUT: opt_destut = true; break; + case OPT_DUALIZE: + if (opt_complement) + error(2, 0, "either --complement or --dualize options" + " can be given, not both"); + opt_dualize = true; + break; case OPT_DNF_ACC: opt_dnf_acc = true; opt_cnf_acc = false; @@ -1249,6 +1262,9 @@ namespace if (opt_complement) aut = spot::dualize(ensure_deterministic(aut)); + if (opt_dualize) + aut = spot::dualize(aut); + aut = post.run(aut, nullptr); if (opt_gra) diff --git a/tests/Makefile.am b/tests/Makefile.am index da132b2f2..dcdf3b65e 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -232,6 +232,7 @@ TESTS_twa = \ core/explpro3.test \ core/explpro4.test \ core/explsum.test \ + core/dualize.test \ core/tripprod.test \ core/dupexp.test \ core/exclusive-tgba.test \ diff --git a/tests/core/dualize.test b/tests/core/dualize.test new file mode 100755 index 000000000..58ffa68d7 --- /dev/null +++ b/tests/core/dualize.test @@ -0,0 +1,67 @@ +#!/bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) 2017 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 + +cat >input1 <expected <