Commit 124de779 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

autfilt: fix -u

Fixes #399.

* bin/autfilt.cc: Fix it.
* tests/core/isomorph.test: Add test case.
* NEWS: Mention the issue.
parent c3d7e942
......@@ -110,6 +110,9 @@ New in spot 2.8.6.dev (not yet released)
incorrectly tagged as complete, causing the print_hoa() function
to raise an exception.
- autfilt --uniq was not considering differences in acceptance
conditions or number of states when discarding automata.
New in spot 2.8.6 (2020-02-19)
Bugs fixed:
......
......@@ -427,8 +427,31 @@ static const struct argp_child children[] =
};
typedef spot::twa_graph::graph_t::edge_storage_t tr_t;
typedef std::set<std::vector<tr_t>> unique_aut_t;
struct canon_aut
{
typedef spot::twa_graph::graph_t::edge_storage_t tr_t;
unsigned num_states;
std::vector<tr_t> edges;
std::string acc;
canon_aut(const spot::const_twa_graph_ptr& aut)
: num_states(aut->num_states())
, edges(aut->edge_vector().begin() + 1,
aut->edge_vector().end())
{
std::ostringstream os;
aut->get_acceptance().to_text(os);
acc = os.str();
}
bool operator<(const canon_aut& o) const
{
return std::tie(num_states, edges, acc)
< std::tie(o.num_states, o.edges, o.acc);
};
};
typedef std::set<canon_aut> unique_aut_t;
static long int match_count = 0;
static spot::option_map extra_options;
static bool randomize_st = false;
......@@ -717,8 +740,7 @@ parse_opt(int key, char* arg, struct argp_state*)
opt_nth = parse_range(arg, 0, std::numeric_limits<int>::max());
break;
case 'u':
opt->uniq =
std::unique_ptr<unique_aut_t>(new std::set<std::vector<tr_t>>());
opt->uniq = std::unique_ptr<unique_aut_t>(new std::set<canon_aut>());
break;
case 'v':
opt_invert = true;
......@@ -1607,8 +1629,7 @@ namespace
auto tmp =
spot::canonicalize(make_twa_graph(aut,
spot::twa::prop_set::all()));
if (!opt->uniq->emplace(tmp->edge_vector().begin() + 1,
tmp->edge_vector().end()).second)
if (!opt->uniq->emplace(tmp).second)
return 0;
}
......
#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement de
# Copyright (C) 2014, 2015, 2020 Laboratoire de Recherche et Développement de
# l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
......@@ -109,3 +109,9 @@ run 0 autfilt aut3 --are-isomorphic aut4
run 0 autfilt -u aut1 aut2 aut2 aut3 -c >out
test 2 = "`cat out`"
ltl2tgba -D -G GFa > aut1
ltl2tgba -D -G FGa > aut2
test 0 = `autfilt -c --are-isomorphic aut1 aut2`
test 2 = `ltl2tgba -D -G 'GFa' 'FG!a' | autfilt -u -c`
test 1 = `ltl2tgba -D -G 'GFa' 'GFa' | autfilt -u -c`
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