Commit 82533202 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

autfilt: implement %D, %N, %P, %W

* bin/common_aoutput.cc, bin/common_aoutput.hh: Implement.
* tests/core/format.test: Test.
* NEWS: Mention.
parent 926ffbf9
......@@ -10,6 +10,9 @@ New in spot 2.1.0a (not yet released)
or to group formulas by number of atomic propositions:
genltl --dac --output='ap-%a.ltl'
* autfilt --stats learned the missing %D, %N, %P, and %W sequences,
to complete the existing %d, %n, %p, and %w.
Bugs fixed:
* Fix several cases where command-line tools would fail to diagnose
......
......@@ -169,16 +169,16 @@ static const argp_option io_options[] =
"acceptance condition (in HOA syntax)", 0 },
{ "%C, %c", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
"number of SCCs", 0 },
{ "%n", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
"number of nondeterministic states in output", 0 },
{ "%d", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
"1 if the output is deterministic, 0 otherwise", 0 },
{ "%p", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
"1 if the output is complete, 0 otherwise", 0 },
{ "%N, %n", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
"number of nondeterministic states", 0 },
{ "%D, %d", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
"1 if the automaton is deterministic, 0 otherwise", 0 },
{ "%P, %p", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
"1 if the automaton is complete, 0 otherwise", 0 },
{ "%r", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
"processing time (excluding parsing) in seconds", 0 },
{ "%w", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
"one word accepted by the output automaton", 0 },
{ "%W, %w", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
"one word accepted by the automaton", 0 },
{ "%%", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
"a single %", 0 },
{ "%<", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
......
......@@ -90,12 +90,16 @@ public:
{
declare('A', &haut_acc_);
declare('C', &haut_scc_);
declare('D', &haut_deterministic_);
declare('E', &haut_edges_);
declare('G', &haut_gen_acc_);
declare('H', &input_aut_);
declare('M', &haut_name_);
declare('N', &haut_nondetstates_);
declare('P', &haut_complete_);
declare('S', &haut_states_);
declare('T', &haut_trans_);
declare('W', &haut_word_);
}
declare('<', &csv_prefix_);
declare('>', &csv_suffix_);
......@@ -172,12 +176,39 @@ public:
if (has('C'))
haut_scc_ = spot::scc_info(haut->aut).scc_count();
if (has('N'))
{
haut_nondetstates_ = count_nondet_states(haut->aut);
haut_deterministic_ = (haut_nondetstates_ == 0);
}
else if (has('D'))
{
// This is more efficient than calling count_nondet_state().
haut_deterministic_ = is_deterministic(haut->aut);
}
if (has('p'))
haut_complete_ = is_complete(haut->aut);
if (has('G'))
{
std::ostringstream os;
os << haut->aut->get_acceptance();
haut_gen_acc_ = os.str();
}
if (has('W'))
{
if (auto word = haut->aut->accepting_word())
{
std::ostringstream out;
out << *word;
haut_word_ = out.str();
}
else
{
haut_word_.val().clear();
}
}
}
if (has('m'))
......@@ -217,12 +248,16 @@ private:
spot::printable_value<std::string> haut_name_;
spot::printable_value<std::string> aut_name_;
spot::printable_value<std::string> aut_word_;
spot::printable_value<std::string> haut_word_;
spot::printable_value<std::string> haut_gen_acc_;
spot::printable_value<unsigned> haut_states_;
spot::printable_value<unsigned> haut_edges_;
spot::printable_value<unsigned> haut_trans_;
spot::printable_value<unsigned> haut_acc_;
spot::printable_value<unsigned> haut_scc_;
spot::printable_value<unsigned> haut_deterministic_;
spot::printable_value<unsigned> haut_nondetstates_;
spot::printable_value<unsigned> haut_complete_;
spot::printable_value<const char*> csv_prefix_;
spot::printable_value<const char*> csv_suffix_;
printable_automaton input_aut_;
......
#! /bin/sh
#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2016 Laboratoire de Recherche et Développement de
# l'Epita (LRDE).
......@@ -50,3 +50,9 @@ genltl --dac --output='ap-%a.ltl2'
for i in 1 2 3 4 5 6; do
cmp ap-$i.ltl ap-$i.ltl2 || exit 1
done
out=`ltl2tgba -f 'GFa' | autfilt --stats='%W,%w' --complement`
test "$out" = "cycle{a},cycle{!a}"
test "0,1,0,1" = "`ltl2tgba FGa | autfilt -D --stats='%D,%d,%P,%p'`"
test "0,0,0,1" = "`ltl2tgba FGa | autfilt -C --stats='%D,%d,%P,%p'`"
test "1,0" = "`ltl2tgba FGa | autfilt -D --stats='%N,%n'`"
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