From de586dd2f06f3b81f588f5cfa6b81a49100d71bd Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 22 Feb 2015 18:05:57 +0100 Subject: [PATCH] stats: use %g to print the (generic) acceptance condition * src/tgbaalgos/stats.cc, src/tgbaalgos/stats.hh: Implement %g. * src/bin/common_aoutput.cc, src/bin/common_aoutput.hh: Document it, and also implement %G. * src/tgbatest/acc2.test: New file. * src/tgbatest/Makefile.am: Add it. --- src/bin/common_aoutput.cc | 4 ++++ src/bin/common_aoutput.hh | 9 +++++++++ src/tgbaalgos/stats.cc | 9 +++++++++ src/tgbaalgos/stats.hh | 5 +++-- src/tgbatest/Makefile.am | 1 + src/tgbatest/acc2.test | 31 +++++++++++++++++++++++++++++++ 6 files changed, 57 insertions(+), 2 deletions(-) create mode 100755 src/tgbatest/acc2.test diff --git a/src/bin/common_aoutput.cc b/src/bin/common_aoutput.cc index 63724d287..91b0b15d0 100644 --- a/src/bin/common_aoutput.cc +++ b/src/bin/common_aoutput.cc @@ -101,6 +101,8 @@ static const argp_option io_options[] = "number of transitions", 0 }, { "%A, %a", 0, 0, OPTION_DOC | OPTION_NO_USAGE, "number of acceptance sets", 0 }, + { "%G, %g", 0, 0, OPTION_DOC | OPTION_NO_USAGE, + "acceptance condition (in HOA syntax)", 0 }, { "%C, %c", 0, 0, OPTION_DOC | OPTION_NO_USAGE, "number of SCCs", 0 }, { "%n", 0, 0, OPTION_DOC | OPTION_NO_USAGE, "number of nondeterministic states in output", 0 }, @@ -131,6 +133,8 @@ static const argp_option o_options[] = { "%t", 0, 0, OPTION_DOC | OPTION_NO_USAGE, "number of transitions", 0 }, { "%a", 0, 0, OPTION_DOC | OPTION_NO_USAGE, "number of acceptance sets", 0 }, + { "%g", 0, 0, OPTION_DOC | OPTION_NO_USAGE, + "acceptance condition (in HOA syntax)", 0 }, { "%c", 0, 0, OPTION_DOC | OPTION_NO_USAGE, "number of SCCs", 0 }, { "%n", 0, 0, OPTION_DOC | OPTION_NO_USAGE, "number of nondeterministic states in output", 0 }, diff --git a/src/bin/common_aoutput.hh b/src/bin/common_aoutput.hh index 281ba868e..b83870863 100644 --- a/src/bin/common_aoutput.hh +++ b/src/bin/common_aoutput.hh @@ -86,6 +86,7 @@ public: declare('A', &haut_acc_); declare('C', &haut_scc_); declare('E', &haut_edges_); + declare('G', &haut_gen_acc_); declare('M', &haut_name_); declare('S', &haut_states_); declare('T', &haut_trans_); @@ -156,6 +157,13 @@ public: if (has('C')) haut_scc_ = spot::scc_info(haut->aut).scc_count(); + + if (has('G')) + { + std::ostringstream os; + os << haut->aut->get_acceptance(); + haut_gen_acc_ = os.str(); + } } if (has('m')) @@ -195,6 +203,7 @@ private: spot::printable_value haut_name_; spot::printable_value aut_name_; spot::printable_value aut_word_; + spot::printable_value haut_gen_acc_; spot::printable_value haut_states_; spot::printable_value haut_edges_; spot::printable_value haut_trans_; diff --git a/src/tgbaalgos/stats.cc b/src/tgbaalgos/stats.cc index bc1d57dc8..43b766b7b 100644 --- a/src/tgbaalgos/stats.cc +++ b/src/tgbaalgos/stats.cc @@ -21,6 +21,7 @@ // along with this program. If not, see . #include +#include #include "tgba/tgba.hh" #include "stats.hh" #include "reachiter.hh" @@ -147,6 +148,7 @@ namespace spot declare('d', &deterministic_); declare('e', &edges_); declare('f', &form_); + declare('g', &gen_acc_); declare('n', &nondetstates_); declare('p', &complete_); declare('r', &run_time_); @@ -202,6 +204,13 @@ namespace spot complete_ = is_complete(aut); } + if (has('g')) + { + std::ostringstream os; + os << aut->get_acceptance(); + gen_acc_ = os.str(); + } + return format(format_); } diff --git a/src/tgbaalgos/stats.hh b/src/tgbaalgos/stats.hh index 574db0400..6955ba875 100644 --- a/src/tgbaalgos/stats.hh +++ b/src/tgbaalgos/stats.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008, 2011, 2012, 2013, 2014 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2008, 2011, 2012, 2013, 2014, 2015 Laboratoire de +// Recherche et Développement de l'Epita (LRDE). // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -101,6 +101,7 @@ namespace spot printable_value deterministic_; printable_value complete_; printable_value run_time_; + printable_value gen_acc_; }; /// @} diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index 2eed6c2da..6384b024b 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -62,6 +62,7 @@ taatgba_SOURCES = taatgba.cc # because such failures will be easier to diagnose and fix. TESTS = \ acc.test \ + acc2.test \ intvcomp.test \ bitvect.test \ ltlcross3.test \ diff --git a/src/tgbatest/acc2.test b/src/tgbatest/acc2.test new file mode 100755 index 000000000..e367882d1 --- /dev/null +++ b/src/tgbatest/acc2.test @@ -0,0 +1,31 @@ +#!/bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) 2015 Laboratoire de Recherche et Développement +# de l'Epita (LRDE). +# +# This file is part of Spot, a model checking library. +# +# Spot is free software; you can redistribute it and/or modify it +# under the terms of the GNU General Public License as published by +# the Free Software Foundation; either version 3 of the License, or +# (at your option) any later version. +# +# Spot is distributed in the hope that it will be useful, but WITHOUT +# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +# License for more details. +# +# You should have received a copy of the GNU General Public License +# along with this program. If not, see . + + +. ./defs + +set -e + +../../bin/ltl2tgba -H 'GFa & GFb' > in +grep 'Acceptance:' in > expected +../../bin/ltl2tgba -H 'GFa & GFb' --stats='Acceptance: %a %g' > out1 +../../bin/autfilt -H in --stats='Acceptance: %A %G' > out2 +diff out1 expected +diff out2 expected