alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

add options to %x to list atomic propositions

Browse source 
* bin/common_aoutput.cc, bin/common_aoutput.hh, bin/common_output.cc,
bin/common_output.hh: Add options to %x to list atomic propositions
with various quoting scheme.  Deprecate --format=%a in favor of the
new --format=%x for consistency with --stats=%x.
* tests/core/format.test, tests/core/remprop.test: Adjust and add more
tests.
* NEWS: Mention these changes.
This commit is contained in:
Alexandre Duret-Lutz 2017-03-01 16:02:09 +01:00
parent 68ad391948
commit 18283d6907
7 changed files with 169 additions and 39 deletions
Download patch file Download diff file Expand all files Collapse all files

12
NEWS
View file

@ -4,7 +4,9 @@ New in spot 2.3.1.dev (not yet released)
- In tools that output automata the number of atomic propositions
can be output using --stats=%x (output automaton) or --stats=%X
(input automaton).
(input automaton). Additional options can be passed to list
atomic propositions instead of conting them. Tools that output
formulas also support --format=%x for this purpose.
Bugs fixed:
@ -14,6 +16,14 @@ New in spot 2.3.1.dev (not yet released)
- Because of a typo, the output of --stats='...%P...' was correct
only if %p was used as well.
Deprecation notices:
- Using --format=%a to print the number of atomic propositions in
ltlfilt, genltl, and randltl still works, but it is not documented
anymore and should be replaced by the newly-introduced --format=%x
for consistency with tools producing automata.
New in spot 2.3.1 (2017-02-20)
Tools:

116
bin/common_aoutput.cc
View file

@ -20,12 +20,15 @@
#include "common_sys.hh"
#include "error.h"
#include "argmatch.h"
#include "common_output.hh"
#include "common_aoutput.hh"
#include "common_post.hh"
#include "common_cout.hh"
#include <unistd.h>
#include <ctime>
#include <ctype.h>
#include <spot/misc/escape.hh>
#include <spot/twa/bddprint.hh>
#include <spot/twaalgos/dot.hh>
#include <spot/twaalgos/hoa.hh>
@ -193,8 +196,9 @@ 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 },
{ "%X, %x, %[LETTERS]X, %[LETTERS]x", 0, nullptr,
OPTION_DOC | OPTION_NO_USAGE,
COMMON_X_OUTPUT_SPECS(declared in the automaton), 0 },
{ "%%", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
"a single %", 0 },
{ "%<", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
@ -254,8 +258,9 @@ 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 },
{ "%x, %[LETTERS]x", 0, nullptr,
OPTION_DOC | OPTION_NO_USAGE,
COMMON_X_OUTPUT_SPECS(declared in the automaton), 0 },
{ "%%", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
"a single %", 0 },
{ nullptr, 0, nullptr, 0, nullptr, 0 }
@ -367,7 +372,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('X', &haut_ap_);
}
declare('<', &csv_prefix_);
declare('>', &csv_suffix_);
@ -379,7 +384,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_);
declare('x', &aut_ap_);
}
std::ostream&
@ -476,7 +481,7 @@ hoa_stat_printer::print(const spot::const_parsed_aut_ptr& haut,
}
}
if (has('X'))
haut_ap_size_ = haut->aut->ap().size();
haut_ap_ = haut->aut->ap();
}
if (has('m'))
@ -501,7 +506,7 @@ hoa_stat_printer::print(const spot::const_parsed_aut_ptr& haut,
}
}
if (has('x'))
aut_ap_size_ = aut->ap().size();
aut_ap_ = aut->ap();
auto& res = this->spot::stat_printer::print(aut, f, run_time);
// Make sure we do not store the automaton until the next one is
@ -625,6 +630,19 @@ void printable_automaton::print(std::ostream& os, const char* pos) const
print_hoa(os, val_, options.c_str());
}
namespace
{
static void percent_error(const char* beg, const char* pos)
{
std::ostringstream tmp;
const char* end = std::strchr(pos, ']');
tmp << "unknown option '" << *pos << "' in '%"
<< std::string(beg, end + 2) << '\'';
throw std::runtime_error(tmp.str());
}
}
void printable_timer::print(std::ostream& os, const char* pos) const
{
double res = 0;
@ -652,19 +670,8 @@ void printable_timer::print(std::ostream& os, const char* pos) const
bool children = false;
const char* beg = pos;
auto error = [&](std::string str)
{
std::ostringstream tmp;
const char* end = std::strchr(pos, ']');
tmp << "unknown option '" << str << "' in '%" << std::string(beg, end + 2)
<< '\'';
throw std::runtime_error(tmp.str());
};
do
{
++pos;
switch (*pos)
switch (*++pos)
{
case 'u':
user = true;
@ -685,9 +692,9 @@ void printable_timer::print(std::ostream& os, const char* pos) const
case ']':
break;
default:
error(std::string(pos, pos + 1));
percent_error(beg, pos);
}
} while (*pos != ']');
while (*pos != ']');
if (!parent && !children)
parent = children = true;
@ -697,3 +704,68 @@ void printable_timer::print(std::ostream& os, const char* pos) const
res = val_.get_uscp(user, system, children, parent);
os << res / clocks_per_sec;
}
void printable_varset::print(std::ostream& os, const char* pos) const
{
if (*pos != '[')
{
os << val_.size();
return;
}
char qstyle = 's'; // quote style
bool parent = false;
std::string sep;
const char* beg = pos;
do
switch (int c = *++pos)
{
case 'p':
parent = true;
break;
case 'c':
case 'd':
case 's':
case 'n':
qstyle = c;
break;
case ']':
break;
default:
if (isalnum(c))
percent_error(beg, pos);
sep += c;
}
while (*pos != ']');
if (sep.empty())
sep = " ";
bool first = true;
for (auto f: val_)
{
if (first)
first = false;
else
os << sep;
if (parent)
os << '(';
switch (qstyle)
{
case 's':
os << f;
break;
case 'n':
os << f.ap_name();
break;
case 'd':
spot::escape_str(os << '"', f.ap_name()) << '"';
break;
case 'c':
spot::escape_rfc4180(os << '"', f.ap_name()) << '"';
break;
}
if (parent)
os << ')';
}
}

37
bin/common_aoutput.hh
View file

@ -31,6 +31,7 @@
#include <spot/twaalgos/sccinfo.hh>
#include <spot/twaalgos/stats.hh>
#include <spot/twaalgos/word.hh>
#include <spot/tl/formula.hh>
// Format for automaton output
@ -107,6 +108,38 @@ struct printable_timer final:
void print(std::ostream& os, const char* pos) const override;
};
struct printable_varset final: public spot::printable
{
protected:
std::vector<spot::formula> val_;
void sort()
{
std::sort(val_.begin(), val_.end(),
[](spot::formula f, spot::formula g)
{
return strverscmp(f.ap_name().c_str(), g.ap_name().c_str()) < 0;
});
}
public:
template<class T>
void set(T begin, T end)
{
val_.clear();
val_.insert(val_.end(), begin, end);
sort();
}
printable_varset& operator=(const std::vector<spot::formula>& val)
{
val_ = val;
sort();
return *this;
}
void print(std::ostream& os, const char* pos) const override;
};
/// \brief prints various statistics about a TGBA
///
/// This object can be configured to display various statistics
@ -144,8 +177,8 @@ private:
spot::printable_value<unsigned> haut_edges_;
spot::printable_value<unsigned> haut_trans_;
spot::printable_value<unsigned> haut_acc_;
spot::printable_value<unsigned> haut_ap_size_;
spot::printable_value<unsigned> aut_ap_size_;
printable_varset haut_ap_;
printable_varset aut_ap_;
spot::printable_scc_info haut_scc_;
spot::printable_value<unsigned> haut_deterministic_;
spot::printable_value<unsigned> haut_nondetstates_;

10
bin/common_output.cc
View file

@ -19,6 +19,7 @@
#include "common_sys.hh"
#include "common_output.hh"
#include "common_aoutput.hh"
#include <iostream>
#include <sstream>
#include <spot/tl/print.hh>
@ -203,13 +204,14 @@ namespace
formula_printer(std::ostream& os, const char* format)
: format_(format)
{
declare('a', &ap_num_);
declare('a', &ap_); // deprecated in 2.3.2
declare('b', &bool_size_);
declare('f', &fl_);
declare('F', &filename_);
declare('L', &line_);
declare('s', &size_);
declare('h', &class_);
declare('x', &ap_);
declare('<', &prefix_);
declare('>', &suffix_);
set_output(os);
@ -225,10 +227,10 @@ namespace
prefix_ = fl.prefix ? fl.prefix : "";
suffix_ = fl.suffix ? fl.suffix : "";
auto f = fl_.val()->f;
if (has('a'))
if (has('a') || has('x'))
{
auto s = spot::atomic_prop_collect(f);
ap_num_ = s->size();
ap_.set(s->begin(), s->end());
delete s;
}
if (has('b'))
@ -250,7 +252,7 @@ namespace
spot::printable_value<int> size_;
printable_formula_class class_;
spot::printable_value<int> bool_size_;
spot::printable_value<int> ap_num_;
printable_varset ap_;
};
}

18
bin/common_output.hh
View file

@ -36,9 +36,18 @@ extern output_format_t output_format;
extern bool full_parenth;
extern bool escape_csv;
#define COMMON_X_OUTPUT_SPECS(where) \
"number of atomic propositions " #where "; " \
" add LETTERS to list atomic propositions with " \
"(n) no quoting, " \
"(s) occasional double-quotes with C-style escape, " \
"(d) double-quotes with C-style escape, " \
"(c) double-quotes with CSV-style escape, " \
"(p) between parentheses, " \
"any extra non-alphanumeric character will be used to " \
"separate propositions"
#define COMMON_LTL_OUTPUT_SPECS \
{ "%a", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, \
"number of atomic propositions used in the formula", 0 }, \
{ "%s", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, \
"the length (or size) of the formula", 0 }, \
{ "%b", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, \
@ -47,7 +56,10 @@ extern bool escape_csv;
{ "%h, %[vw]h", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, \
"the class of the formula is the Manna-Pnueli hierarchy " \
"([v] replaces abbreviations by class names, [w] for all " \
"compatible classes)", 0 }
"compatible classes)", 0 }, \
{ "%x, %[LETTERS]X, %[LETTERS]x", 0, nullptr, \
OPTION_DOC | OPTION_NO_USAGE, \
COMMON_X_OUTPUT_SPECS(used in the formula), 0 }
extern const struct argp output_argp;

8
tests/core/format.test
View file

@ -23,7 +23,7 @@
set -e
genltl --dac=1..10 --format='%s,%b,%a,%f' > output
genltl --dac=1..10 --format='%s,%b,%x,%f' > output
cat >expected <<EOF
3,2,1,G!p0
7,6,2,Fp0 -> (!p1 U p0)
@ -38,7 +38,7 @@ cat >expected <<EOF
EOF
diff output expected
genltl --dac | ltlfilt --output='ap-%a.ltl'
genltl --dac | ltlfilt --output='ap-%x.ltl'
test 4 = `wc -l<ap-1.ltl`
test 10 = `wc -l<ap-2.ltl`
test 16 = `wc -l<ap-3.ltl`
@ -46,7 +46,7 @@ test 13 = `wc -l<ap-4.ltl`
test 10 = `wc -l<ap-5.ltl`
test 2 = `wc -l<ap-6.ltl`
genltl --dac --output='ap-%a.ltl2'
genltl --dac --output='ap-%x.ltl2'
for i in 1 2 3 4 5 6; do
cmp ap-$i.ltl ap-$i.ltl2 || exit 1
done
@ -56,7 +56,7 @@ out=`<GFa autfilt --stats='%W,%w' --complement`
test "$out" = "cycle{a},cycle{!a}"
ltl2tgba FGa > FGa
test "0,1,0,1" = "`<FGa autfilt -D --stats='%D,%d,%P,%p'`"
test "0,0,0,1" = "`<FGa autfilt -C --stats='%D,%d,%P,%p'`"
test '0,0,0,1,"a"' = "`<FGa autfilt -C --stats='%D,%d,%P,%p,%[d]x'`"
# We had some issues in the pase where %P was set only if %p was used
# as well. So we make separate tests for this.
test "0,0" = "`<FGa autfilt -C --stats='%D,%P'`"

3
tests/core/remprop.test
View file

@ -75,6 +75,7 @@ diff out expected
cat >expected <<EOF
HOA: v1
name: "\"a\", \"b\", \"c\"->(c)"
States: 3
Start: 0
AP: 1 "c"
@ -90,7 +91,7 @@ State: 2
--END--
EOF
run 0 autfilt -H --remove-ap=a=1,b=0 automaton >out
run 0 autfilt -H --remove-ap=a=1,b=0 --name='%[d, ]X->%[p]x' automaton >out
cat out
diff out expected