diff --git a/NEWS b/NEWS index d421d16ae..28a6d6305 100644 --- a/NEWS +++ b/NEWS @@ -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 diff --git a/bin/common_aoutput.cc b/bin/common_aoutput.cc index fdc288920..3083d1ecf 100644 --- a/bin/common_aoutput.cc +++ b/bin/common_aoutput.cc @@ -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, diff --git a/bin/common_aoutput.hh b/bin/common_aoutput.hh index 4508b8f69..a56411ea2 100644 --- a/bin/common_aoutput.hh +++ b/bin/common_aoutput.hh @@ -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 haut_name_; spot::printable_value aut_name_; spot::printable_value aut_word_; + spot::printable_value haut_word_; spot::printable_value haut_gen_acc_; spot::printable_value haut_states_; spot::printable_value haut_edges_; spot::printable_value haut_trans_; spot::printable_value haut_acc_; spot::printable_value haut_scc_; + spot::printable_value haut_deterministic_; + spot::printable_value haut_nondetstates_; + spot::printable_value haut_complete_; spot::printable_value csv_prefix_; spot::printable_value csv_suffix_; printable_automaton input_aut_; diff --git a/tests/core/format.test b/tests/core/format.test index 157953e6c..9463a425d 100644 --- a/tests/core/format.test +++ b/tests/core/format.test @@ -1,4 +1,4 @@ -#! /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'`"