Commit de586dd2 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

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.
parent 33c496a4
......@@ -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 },
......
......@@ -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<std::string> haut_name_;
spot::printable_value<std::string> aut_name_;
spot::printable_value<std::string> aut_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_;
......
......@@ -21,6 +21,7 @@
// along with this program. If not, see <http://www.gnu.org/licenses/>.
#include <iostream>
#include <sstream>
#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_);
}
......
// -*- 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<unsigned> deterministic_;
printable_value<unsigned> complete_;
printable_value<double> run_time_;
printable_value<std::string> gen_acc_;
};
/// @}
......
......@@ -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 \
......
#!/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 <http://www.gnu.org/licenses/>.
. ./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
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