alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

autfilt: fix -u

Browse source 
Fixes #399.

* bin/autfilt.cc: Fix it.
* tests/core/isomorph.test: Add test case.
* NEWS: Mention the issue.
This commit is contained in:
Alexandre Duret-Lutz 2020-03-11 23:05:15 +01:00
parent 5b8dbc6549
commit e2ec711c40
3 changed files with 37 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

3
NEWS
View file

@ -9,6 +9,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:

33
bin/autfilt.cc
View file

@ -419,8 +419,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;
@ -703,8 +726,7 @@ parse_opt(int key, char* arg, struct argp_state*)
opt_max_count = to_pos_int(arg, "-n/--max-count");
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;
@ -1559,8 +1581,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;
}

8
tests/core/isomorph.test
View file

@ -1,6 +1,6 @@
#!/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`