diff --git a/NEWS b/NEWS index d3849af72..e1cf16b98 100644 --- a/NEWS +++ b/NEWS @@ -18,6 +18,11 @@ New in spot 2.6.3.dev (not yet released) - ltlfilt learned --liveness to match formulas representing liveness properties. + - the --stats= option of tools producing automata learned how to + tell if an automaton uses universal branching (%u), or more + precisely how many states (%[s]u) or edges (%[e]u) use universal + branching. + Python: - spot.translate() and spot.postprocess() now take an xargs= @@ -75,6 +80,10 @@ New in spot 2.6.3.dev (not yet released) used to check whether a formula or an automaton represents a liveness property. + - Two new functions count_univbranch_states() and + count_univbranch_edges() can help measuring the amount of + universal branching in alternating automata. + Bugs fixed: - The pair of acc_cond::mark_t returned by diff --git a/bin/common_aoutput.cc b/bin/common_aoutput.cc index b844b3d18..dd6dd8a70 100644 --- a/bin/common_aoutput.cc +++ b/bin/common_aoutput.cc @@ -218,6 +218,10 @@ static const argp_option io_options[] = "1 if the automaton is complete, 0 otherwise", 0 }, { "%r", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, "wall-clock time elapsed in seconds (excluding parsing)", 0 }, + { "%U, %u, %[LETTER]U, %[LETTER]u", 0, nullptr, + OPTION_DOC | OPTION_NO_USAGE, + "1 if the automaton contains some universal branching " + "(or a number of [s]tates or [e]dges with universal branching)", 0 }, { "%W, %w", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, "one word accepted by the automaton", 0 }, { "%X, %x, %[LETTERS]X, %[LETTERS]x", 0, nullptr, @@ -272,6 +276,11 @@ static const argp_option o_options[] = "or (c) children processes.", 0 }, { "%n", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, "number of nondeterministic states in output", 0 }, + { "%u, %[LETTER]u", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, + "1 if the automaton contains some universal branching " + "(or a number of [s]tates or [e]dges with universal branching)", 0 }, + { "%u, %[e]u", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, + "number of states (or [e]dges) with universal branching", 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, @@ -393,6 +402,7 @@ hoa_stat_printer::hoa_stat_printer(std::ostream& os, const char* format, declare('P', &haut_complete_); declare('S', &haut_states_); declare('T', &haut_trans_); + declare('U', &haut_univbranch_); declare('W', &haut_word_); declare('X', &haut_ap_); } @@ -406,6 +416,7 @@ hoa_stat_printer::hoa_stat_printer(std::ostream& os, const char* format, declare('f', &filename_); // Override the formula printer. declare('h', &output_aut_); declare('m', &aut_name_); + declare('u', &aut_univbranch_); declare('w', &aut_word_); declare('x', &aut_ap_); } @@ -478,6 +489,8 @@ hoa_stat_printer::print(const spot::const_parsed_aut_ptr& haut, // This is more efficient than calling count_nondet_state(). haut_deterministic_ = is_deterministic(haut->aut); } + if (has('U')) + haut_univbranch_ = haut->aut; if (has('P')) haut_complete_ = is_complete(haut->aut); @@ -509,6 +522,8 @@ hoa_stat_printer::print(const spot::const_parsed_aut_ptr& haut, else aut_name_.val().clear(); } + if (has('u')) + aut_univbranch_ = aut; if (has('w')) { if (auto word = aut->accepting_word()) @@ -532,6 +547,8 @@ hoa_stat_printer::print(const spot::const_parsed_aut_ptr& haut, output_aut_ = nullptr; input_aut_ = nullptr; haut_scc_.reset(); + aut_univbranch_ = nullptr; + haut_univbranch_ = nullptr; aut_ap_.clear(); haut_ap_.clear(); return res; @@ -661,6 +678,26 @@ namespace } } +void printable_univbranch::print(std::ostream& os, const char* pos) const +{ + std::string options = "l"; + if (pos[0] == '[' && pos[1] != ']') + { + if (pos[1] == 'e' && pos[2] == ']') + { + os << spot::count_univbranch_edges(val_); + return; + } + else if (pos[1] == 's' && pos[2] == ']') + { + os << spot::count_univbranch_states(val_); + return; + } + percent_error(pos, pos + 1); + } + os << (spot::count_univbranch_edges(val_) ? 1 : 0); +} + void printable_timer::print(std::ostream& os, const char* pos) const { double res = 0; diff --git a/bin/common_aoutput.hh b/bin/common_aoutput.hh index 98724b61b..0f1103152 100644 --- a/bin/common_aoutput.hh +++ b/bin/common_aoutput.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014-2017 Laboratoire de Recherche et Développement +// Copyright (C) 2014-2018 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -74,6 +74,14 @@ struct printable_automaton final: void print(std::ostream& os, const char* pos) const override; }; +struct printable_univbranch final: + public spot::printable_value +{ + using spot::printable_value::operator=; + void print(std::ostream& os, const char* pos) const override; +}; + + struct printable_timer final: public spot::printable { protected: @@ -169,6 +177,8 @@ private: spot::printable_value haut_complete_; spot::printable_value csv_prefix_; spot::printable_value csv_suffix_; + printable_univbranch haut_univbranch_; + printable_univbranch aut_univbranch_; printable_timer timer_; printable_automaton input_aut_; printable_automaton output_aut_; diff --git a/spot/twaalgos/isdet.cc b/spot/twaalgos/isdet.cc index 37d8ee0dd..b7b6df0be 100644 --- a/spot/twaalgos/isdet.cc +++ b/spot/twaalgos/isdet.cc @@ -310,4 +310,33 @@ namespace spot check_semi_determism(aut, true); } + unsigned + count_univbranch_states(const const_twa_graph_ptr& aut) + { + if (aut->is_existential()) + return 0; + unsigned res = 0; + unsigned ns = aut->num_states(); + for (unsigned s = 0; s < ns; ++s) + for (auto& e: aut->out(s)) + if (aut->is_univ_dest(e)) + { + ++res; + break; + } + return res; + } + + unsigned + count_univbranch_edges(const const_twa_graph_ptr& aut) + { + if (aut->is_existential()) + return 0; + unsigned res = aut->is_univ_dest(aut->get_init_state_number()); + for (auto& e: aut->edges()) + if (aut->is_univ_dest(e)) + ++res; + return res; + } + } diff --git a/spot/twaalgos/isdet.hh b/spot/twaalgos/isdet.hh index 6cb020fb5..2717c877f 100644 --- a/spot/twaalgos/isdet.hh +++ b/spot/twaalgos/isdet.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2014, 2015, 2016, 2017 Laboratoire de Recherche -// et Développement de l'Epita (LRDE). +// Copyright (C) 2012-2018 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -109,4 +109,33 @@ namespace spot /// \brief Set the deterministic and semi-deterministic properties /// appropriately. SPOT_API void check_determinism(twa_graph_ptr aut); + + // \brief Count states with some universal branching. + // + // This counts the number of states that have edges going to several + // destinations at once (as reported by aut->is_univ_dest(...)). + // + // Note that nondeterministic automata (which include deterministic + // automata) have 0 such state, but additionally they also have + // "singleton" initial state (which this function does not check). + // + // \see count_univbranch_edges() + SPOT_API unsigned + count_univbranch_states(const const_twa_graph_ptr& aut); + + // \brief Count edges with universal branching. + // + // This counts the number of edges going to several destination at + // once (as reported by aut->is_univ_dest(...)). + // + // If the automaton starts in multiple initial states at once, this + // is considered as a universal "initial edge", and adds one to the + // total count. + // + // Nondeterministic automata (which include deterministic automata) + // have 0 edges with universal branching. + // + // \see count_univbranch_states() + SPOT_API unsigned + count_univbranch_edges(const const_twa_graph_ptr& aut); } diff --git a/tests/core/alternating.test b/tests/core/alternating.test index 270ccd650..c4dd98298 100755 --- a/tests/core/alternating.test +++ b/tests/core/alternating.test @@ -53,6 +53,8 @@ State: 6 "t" --END-- EOF +test "1 2 4" = "`autfilt --stats='%u %[s]u %[e]u' alt.hoa`" + autfilt --has-univ-branch --has-exist-branch --dot=bans alt.hoa >alt.dot cat >expect.dot <stderr && exit2 +grep '%\[x\]U' stderr