Commit 0d884d4a authored by Thomas Medioni's avatar Thomas Medioni

autfilt: Add --dualize option

* NEWS: Mention this addition.
* bin/autfilt.cc: Add dualize option
* tests/Makefile.am: Add dualize option test file to the suite.
* tests/core/dualize.test: Test the dualize option.
parent 152b5d0d
......@@ -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
......
......@@ -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<bool> 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)
......
......@@ -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 \
......
#!/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 <http://www.gnu.org/licenses/>.
. ./defs
set -e
cat >input1 <<EOF
HOA: v1
States: 4
Start: 0
AP: 2 "a" "b"
acc-name: Buchi
Acceptance: 3 Inf(0) & Inf(1) & Fin(2)
properties: trans-labels explicit-labels trans-acc
--BODY--
State: 0
[0] 1&2&3
[1] 0&1
State: 1
[t] 1 {0}
State: 2
[t] 2 {1}
State: 3
[0] 2
[!0&!1] 0 {2}
--END--
EOF
cat >expected <<EOF
HOA: v1
States: 2
Start: 0
AP: 2 "a" "b"
acc-name: all
Acceptance: 0 t
properties: trans-labels explicit-labels trans-acc complete
properties: deterministic
--BODY--
State: 0
[t] 1
State: 1
[t] 1
--END--
EOF
run 0 autfilt input1 --dualize --hoaf=t | tee stdout
diff stdout expected
rm input1 expected stdout
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