bin: add %g options to print acceptance name
Fixes #289. * spot/twaalgos/stats.cc, spot/twaalgos/stats.hh, bin/common_aoutput.cc, bin/common_aoutput.hh: plug %g and %G into acc_cond::name() when arguments are given as %[arg]g. or %[arg]G. * tests/core/acc2.test: Add test case. * doc/org/randaut.org, NEWS: Document it.
This commit is contained in:
parent
bd39edde27
commit
75a1d6ac61
7 changed files with 110 additions and 18 deletions
11
NEWS
11
NEWS
|
|
@ -49,6 +49,17 @@ New in spot 2.4.1.dev (not yet released)
|
||||||
implication-based simplification rules of ltl2tgba. See the
|
implication-based simplification rules of ltl2tgba. See the
|
||||||
spot-x man-page for details.
|
spot-x man-page for details.
|
||||||
|
|
||||||
|
- The --format=%g option of tools that output automata used to
|
||||||
|
print the acceptance condition as a *formula* in the HOA format.
|
||||||
|
This %g can now take optional arguments to print the acceptance
|
||||||
|
*name* in different formats. For instance
|
||||||
|
|
||||||
|
... | autfilt -o '%[s]g.hoa'
|
||||||
|
|
||||||
|
will separate a stream of automata into different files named
|
||||||
|
by their acceptance name (Buchi, co-Buchi, Streett, etc.) or
|
||||||
|
"other" if no name is known for the acceptance condition.
|
||||||
|
|
||||||
Library:
|
Library:
|
||||||
|
|
||||||
- Rename three methods of spot::scc_info. New names are clearer. The
|
- Rename three methods of spot::scc_info. New names are clearer. The
|
||||||
|
|
|
||||||
|
|
@ -159,6 +159,21 @@ const struct argp aoutput_argp = { options, parse_opt_aoutput, nullptr, nullptr,
|
||||||
char F_doc[32] = "name of the input file";
|
char F_doc[32] = "name of the input file";
|
||||||
char L_doc[32] = "location in the input file";
|
char L_doc[32] = "location in the input file";
|
||||||
|
|
||||||
|
#define doc_g \
|
||||||
|
"acceptance condition (in HOA syntax); add brackets to print " \
|
||||||
|
"an acceptance name instead and LETTERS to tweak the format: " \
|
||||||
|
"(0) no parameters, " \
|
||||||
|
"(a) accentuated, " \
|
||||||
|
"(b) abbreviated, " \
|
||||||
|
"(d) style used in dot output, " \
|
||||||
|
"(g) no generalized parameter, " \
|
||||||
|
"(l) recognize Street-like and Rabin-like, " \
|
||||||
|
"(m) no main parameter, " \
|
||||||
|
"(p) no parity parameter, " \
|
||||||
|
"(o) name unknown acceptance as 'other', " \
|
||||||
|
"(s) shorthand for 'lo0'."
|
||||||
|
|
||||||
|
|
||||||
static const argp_option io_options[] =
|
static const argp_option io_options[] =
|
||||||
{
|
{
|
||||||
/**************************************************/
|
/**************************************************/
|
||||||
|
|
@ -180,8 +195,8 @@ static const argp_option io_options[] =
|
||||||
"number of reachable transitions", 0 },
|
"number of reachable transitions", 0 },
|
||||||
{ "%A, %a", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
|
{ "%A, %a", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
|
||||||
"number of acceptance sets", 0 },
|
"number of acceptance sets", 0 },
|
||||||
{ "%G, %g", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
|
{ "%G, %g, %[LETTERS]G, %[LETTERS]g", 0, nullptr,
|
||||||
"acceptance condition (in HOA syntax)", 0 },
|
OPTION_DOC | OPTION_NO_USAGE, doc_g, 0 },
|
||||||
{ "%C, %c, %[LETTERS]C, %[LETTERS]c", 0, nullptr,
|
{ "%C, %c, %[LETTERS]C, %[LETTERS]c", 0, nullptr,
|
||||||
OPTION_DOC | OPTION_NO_USAGE,
|
OPTION_DOC | OPTION_NO_USAGE,
|
||||||
"number of SCCs; you may filter the SCCs to count "
|
"number of SCCs; you may filter the SCCs to count "
|
||||||
|
|
@ -241,8 +256,8 @@ static const argp_option o_options[] =
|
||||||
"number of reachable transitions", 0 },
|
"number of reachable transitions", 0 },
|
||||||
{ "%a", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
|
{ "%a", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
|
||||||
"number of acceptance sets", 0 },
|
"number of acceptance sets", 0 },
|
||||||
{ "%g", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
|
{ "%g, %[LETTERS]g", 0, nullptr,
|
||||||
"acceptance condition (in HOA syntax)", 0 },
|
OPTION_DOC | OPTION_NO_USAGE, doc_g, 0 },
|
||||||
{ "%c, %[LETTERS]c", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
|
{ "%c, %[LETTERS]c", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
|
||||||
"number of SCCs; you may filter the SCCs to count "
|
"number of SCCs; you may filter the SCCs to count "
|
||||||
"using the following LETTERS, possibly concatenated: (a) accepting, "
|
"using the following LETTERS, possibly concatenated: (a) accepting, "
|
||||||
|
|
@ -464,13 +479,9 @@ hoa_stat_printer::print(const spot::const_parsed_aut_ptr& haut,
|
||||||
|
|
||||||
if (has('P'))
|
if (has('P'))
|
||||||
haut_complete_ = is_complete(haut->aut);
|
haut_complete_ = is_complete(haut->aut);
|
||||||
|
|
||||||
if (has('G'))
|
if (has('G'))
|
||||||
{
|
haut_gen_acc_ = haut->aut->acc();
|
||||||
std::ostringstream os;
|
|
||||||
os << haut->aut->get_acceptance();
|
|
||||||
haut_gen_acc_ = os.str();
|
|
||||||
}
|
|
||||||
if (has('W'))
|
if (has('W'))
|
||||||
{
|
{
|
||||||
if (auto word = haut->aut->accepting_word())
|
if (auto word = haut->aut->accepting_word())
|
||||||
|
|
|
||||||
|
|
@ -156,7 +156,7 @@ private:
|
||||||
spot::printable_value<std::string> aut_name_;
|
spot::printable_value<std::string> aut_name_;
|
||||||
spot::printable_value<std::string> aut_word_;
|
spot::printable_value<std::string> aut_word_;
|
||||||
spot::printable_value<std::string> haut_word_;
|
spot::printable_value<std::string> haut_word_;
|
||||||
spot::printable_value<std::string> haut_gen_acc_;
|
spot::printable_acc_cond haut_gen_acc_;
|
||||||
spot::printable_value<unsigned> haut_states_;
|
spot::printable_value<unsigned> haut_states_;
|
||||||
spot::printable_value<unsigned> haut_edges_;
|
spot::printable_value<unsigned> haut_edges_;
|
||||||
spot::printable_value<unsigned> haut_trans_;
|
spot::printable_value<unsigned> haut_trans_;
|
||||||
|
|
|
||||||
|
|
@ -163,7 +163,6 @@ $txt
|
||||||
#+RESULTS:
|
#+RESULTS:
|
||||||
[[file:randaut3.png]]
|
[[file:randaut3.png]]
|
||||||
|
|
||||||
|
|
||||||
* Acceptance condition
|
* Acceptance condition
|
||||||
|
|
||||||
The generation of the acceptance sets abn is controlled with the following four parameters:
|
The generation of the acceptance sets abn is controlled with the following four parameters:
|
||||||
|
|
@ -471,6 +470,30 @@ The output format can be controlled using [[file:oaut.org][the common output opt
|
||||||
like =--hoaf=, =--dot==, =--lbtt=, and =--spin=. Note that =--spin=
|
like =--hoaf=, =--dot==, =--lbtt=, and =--spin=. Note that =--spin=
|
||||||
automatically implies =--ba=.
|
automatically implies =--ba=.
|
||||||
|
|
||||||
|
Automata are send to standard output by default, by you can use =-o=
|
||||||
|
to give a filename, or even a pattern for filenames. For instance the
|
||||||
|
following generates 20 automatas, but store them in different files
|
||||||
|
according to the acceptance condition. The format =%g= represent the
|
||||||
|
formula for the acceptance condition and would not make a nice
|
||||||
|
filename, but =%[s]g= is a short name for that acceptance condition
|
||||||
|
(its is replaced by "other" if Spot does not know better).
|
||||||
|
|
||||||
|
#+BEGIN_SRC sh :results verbatim :exports both
|
||||||
|
randaut -n20 -Q10 -A 'random 3' 2 -o 'randaut-%[s]g.hoa'
|
||||||
|
wc -l randaut-*.hoa
|
||||||
|
#+END_SRC
|
||||||
|
|
||||||
|
#+RESULTS:
|
||||||
|
: 222 randaut-Rabin-like.hoa
|
||||||
|
: 380 randaut-Streett-like.hoa
|
||||||
|
: 100 randaut-generalized-Buchi.hoa
|
||||||
|
: 249 randaut-other.hoa
|
||||||
|
: 951 total
|
||||||
|
|
||||||
|
#+BEGIN_SRC sh :results silent :exports results
|
||||||
|
rm -f rautaut-*.hoa
|
||||||
|
#+END_SRC
|
||||||
|
|
||||||
* Generating a stream of automata
|
* Generating a stream of automata
|
||||||
|
|
||||||
Use option =-n= to specify a number of automata to build. A negative
|
Use option =-n= to specify a number of automata to build. A negative
|
||||||
|
|
|
||||||
|
|
@ -331,6 +331,31 @@ namespace spot
|
||||||
os << count;
|
os << count;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
void printable_acc_cond::print(std::ostream& os, const char* pos) const
|
||||||
|
{
|
||||||
|
if (*pos != '[')
|
||||||
|
{
|
||||||
|
os << val_.get_acceptance();
|
||||||
|
return;
|
||||||
|
}
|
||||||
|
const char* beg = pos;
|
||||||
|
++pos;
|
||||||
|
const char* end = strchr(pos, ']');
|
||||||
|
try
|
||||||
|
{
|
||||||
|
os << val_.name(std::string(pos, end).c_str());
|
||||||
|
}
|
||||||
|
catch (const std::runtime_error& e)
|
||||||
|
{
|
||||||
|
std::ostringstream tmp;
|
||||||
|
tmp << "while processing %"
|
||||||
|
<< std::string(beg, end + 2) << ", ";
|
||||||
|
tmp << e.what();
|
||||||
|
throw std::runtime_error(tmp.str());
|
||||||
|
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
stat_printer::stat_printer(std::ostream& os, const char* format)
|
stat_printer::stat_printer(std::ostream& os, const char* format)
|
||||||
: format_(format)
|
: format_(format)
|
||||||
|
|
@ -397,11 +422,7 @@ namespace spot
|
||||||
}
|
}
|
||||||
|
|
||||||
if (has('g'))
|
if (has('g'))
|
||||||
{
|
gen_acc_ = aut->acc();
|
||||||
std::ostringstream os;
|
|
||||||
os << aut->get_acceptance();
|
|
||||||
gen_acc_ = os.str();
|
|
||||||
}
|
|
||||||
|
|
||||||
auto& os = format(format_);
|
auto& os = format(format_);
|
||||||
// Make sure we do not hold a pointer to the automaton or the
|
// Make sure we do not hold a pointer to the automaton or the
|
||||||
|
|
|
||||||
|
|
@ -70,6 +70,20 @@ namespace spot
|
||||||
print(std::ostream& os, const char*) const override;
|
print(std::ostream& os, const char*) const override;
|
||||||
};
|
};
|
||||||
|
|
||||||
|
class SPOT_API printable_acc_cond final: public spot::printable
|
||||||
|
{
|
||||||
|
acc_cond val_;
|
||||||
|
public:
|
||||||
|
printable_acc_cond&
|
||||||
|
operator=(const acc_cond& new_val)
|
||||||
|
{
|
||||||
|
val_ = new_val;
|
||||||
|
return *this;
|
||||||
|
}
|
||||||
|
|
||||||
|
void print(std::ostream& os, const char* pos) const override;
|
||||||
|
};
|
||||||
|
|
||||||
class SPOT_API printable_scc_info final:
|
class SPOT_API printable_scc_info final:
|
||||||
public spot::printable
|
public spot::printable
|
||||||
{
|
{
|
||||||
|
|
@ -117,7 +131,7 @@ namespace spot
|
||||||
printable_value<unsigned> nondetstates_;
|
printable_value<unsigned> nondetstates_;
|
||||||
printable_value<unsigned> deterministic_;
|
printable_value<unsigned> deterministic_;
|
||||||
printable_value<unsigned> complete_;
|
printable_value<unsigned> complete_;
|
||||||
printable_value<std::string> gen_acc_;
|
printable_acc_cond gen_acc_;
|
||||||
};
|
};
|
||||||
|
|
||||||
/// @}
|
/// @}
|
||||||
|
|
|
||||||
|
|
@ -25,10 +25,22 @@ set -e
|
||||||
|
|
||||||
ltl2tgba -H 'GFa & GFb' > in
|
ltl2tgba -H 'GFa & GFb' > in
|
||||||
grep 'Acceptance:' in > expected
|
grep 'Acceptance:' in > expected
|
||||||
|
grep 'acc-name:' in > expected-b
|
||||||
ltl2tgba -H 'GFa & GFb' --stats='Acceptance: %a %g' > out1
|
ltl2tgba -H 'GFa & GFb' --stats='Acceptance: %a %g' > out1
|
||||||
|
ltl2tgba -H 'GFa & GFb' --stats='acc-name: %[]g' > out1b
|
||||||
autfilt -H in --format='Acceptance: %A %G' > out2
|
autfilt -H in --format='Acceptance: %A %G' > out2
|
||||||
|
autfilt -H in --format='acc-name: %[]G' > out2b
|
||||||
diff out1 expected
|
diff out1 expected
|
||||||
diff out2 expected
|
diff out2 expected
|
||||||
|
diff out1b expected-b
|
||||||
|
diff out2b expected-b
|
||||||
|
|
||||||
|
autfilt -H in --format='%[d]G, %[0lo]g, %[0abdglmpos]g' > out3
|
||||||
|
echo 'gen. Büchi 2, generalized-Buchi, gen. Büchi' >exp3
|
||||||
|
diff out3 exp3
|
||||||
|
|
||||||
|
autfilt -H in --format='%[bug]g' 2>err && exit 1
|
||||||
|
grep '%\[bug\]g.*: u' err
|
||||||
|
|
||||||
cat >header <<EOF
|
cat >header <<EOF
|
||||||
HOA: v1
|
HOA: v1
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue