diff --git a/NEWS b/NEWS index a86212c0f71ad1f584c233dee07982632ac2fca3..4dc6ed9966971aff652c574a2dd0e52bc2c8084d 100644 --- a/NEWS +++ b/NEWS @@ -1,6 +1,10 @@ New in spot 2.3.1.dev (not yet released) - Nothing yet. + Tools: + + - In tools that output automata the number of atomic propositions + can be output using --stats=%x (output automaton) or --stats=%X + (input automaton). New in spot 2.3.1 (2017-02-20) diff --git a/bin/common_aoutput.cc b/bin/common_aoutput.cc index ce0944b2c20b039584b9ba4c018778644a7a9b77..e8011b30fe9ee227d61a05f0315edad31e1a5010 100644 --- a/bin/common_aoutput.cc +++ b/bin/common_aoutput.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche -// et Développement de l'Epita (LRDE). +// Copyright (C) 2012-2017 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -193,6 +193,8 @@ static const argp_option io_options[] = "wall-clock time elapsed in seconds (excluding parsing)", 0 }, { "%W, %w", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, "one word accepted by the automaton", 0 }, + { "%X, %x", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, + "number of atomic propositions declared in the automaton", 0 }, { "%%", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, "a single %", 0 }, { "%<", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, @@ -228,6 +230,8 @@ static const argp_option o_options[] = "number of transitions", 0 }, { "%a", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, "number of acceptance sets", 0 }, + { "%b", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, + "number of acceptance sets", 0 }, { "%g", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, "acceptance condition (in HOA syntax)", 0 }, { "%c, %[LETTERS]c", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, @@ -250,6 +254,8 @@ static const argp_option o_options[] = "wall-clock time elapsed in seconds (excluding parsing)", 0 }, { "%w", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, "one word accepted by the output automaton", 0 }, + { "%x", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, + "number of atomic propositions declared in the automaton", 0 }, { "%%", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, "a single %", 0 }, { nullptr, 0, nullptr, 0, nullptr, 0 } @@ -361,6 +367,7 @@ hoa_stat_printer::hoa_stat_printer(std::ostream& os, const char* format, declare('S', &haut_states_); declare('T', &haut_trans_); declare('W', &haut_word_); + declare('X', &haut_ap_size_); } declare('<', &csv_prefix_); declare('>', &csv_suffix_); @@ -372,6 +379,7 @@ hoa_stat_printer::hoa_stat_printer(std::ostream& os, const char* format, declare('h', &output_aut_); declare('m', &aut_name_); declare('w', &aut_word_); + declare('x', &aut_ap_size_); } std::ostream& @@ -467,6 +475,8 @@ hoa_stat_printer::print(const spot::const_parsed_aut_ptr& haut, haut_word_.val().clear(); } } + if (has('X')) + haut_ap_size_ = haut->aut->ap().size(); } if (has('m')) @@ -490,6 +500,8 @@ hoa_stat_printer::print(const spot::const_parsed_aut_ptr& haut, aut_word_.val().clear(); } } + if (has('x')) + aut_ap_size_ = aut->ap().size(); auto& res = this->spot::stat_printer::print(aut, f, run_time); // Make sure we do not store the automaton until the next one is diff --git a/bin/common_aoutput.hh b/bin/common_aoutput.hh index 9a10b07459b3abb76c3b9bf86fc2510daf4a4163..f22244242a1ec2a79539bf7170b9bce27988092f 100644 --- a/bin/common_aoutput.hh +++ b/bin/common_aoutput.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2014-2017 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -144,6 +144,8 @@ private: spot::printable_value haut_edges_; spot::printable_value haut_trans_; spot::printable_value haut_acc_; + spot::printable_value haut_ap_size_; + spot::printable_value aut_ap_size_; spot::printable_scc_info haut_scc_; spot::printable_value haut_deterministic_; spot::printable_value haut_nondetstates_; diff --git a/tests/core/remprop.test b/tests/core/remprop.test index 09e28d7ce6e75b6e57bb6b8b47e8b16c8a3aabc9..e423c4784ffa3cc7d6a0fd6657e364e3d072af75 100755 --- a/tests/core/remprop.test +++ b/tests/core/remprop.test @@ -1,6 +1,6 @@ #! /bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement de +# Copyright (C) 2015-2017 Laboratoire de Recherche et Développement de # l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -47,6 +47,7 @@ EOF cat >expected <1" States: 4 Start: 0 AP: 1 "c" @@ -68,7 +69,7 @@ State: 3 --END-- EOF -run 0 autfilt -H --remove-ap=a,b automaton >out +run 0 autfilt -H --remove-ap=a,b --name='%X->%x' automaton >out cat out diff out expected