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

ltlsynt: implement --csv-without-formula

Browse source 
* bin/ltlsynt.cc: Implement that new option.
* tests/core/ltlsynt2.test: Test it.
* NEWS: Mention the change.
This commit is contained in:
Alexandre Duret-Lutz 2024-09-04 16:33:48 +02:00
parent 6e5592fe6a
commit a22a05b8ec
3 changed files with 40 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

7
NEWS
View file

@ -5,8 +5,11 @@ New in spot 2.12.0.dev (not yet released)
- ltlmix is a new tool that generates formulas by combining existing
ones. See https://spot.lre.epita.fr/ltlmix.html for examples.
- ltlsynt --csv=FILENAME will now save the source filename for
the processed formulas as the first column of the CSV file.
- ltlsynt --csv=FILENAME will now save the source filename for the
processed formulas as the first column of the CSV file. A new
option --csv-without-formula=FILENAME can be used to save
everything but the formula column (as it can be very large, and
can be found from the source filename).
- ltlsynt learned a --part-file option, to specify the partition of
input/output proposition from a *.part file, as used in several

30
bin/ltlsynt.cc
View file

@ -50,6 +50,7 @@ enum
OPT_ALGO = 256,
OPT_BYPASS,
OPT_CSV,
OPT_CSV_NO_FORMULA,
OPT_DECOMPOSE,
OPT_DOT,
OPT_FROM_PGAME,
@ -153,6 +154,9 @@ static const argp_option options[] =
"output statistics as CSV in FILENAME or on standard output "
"(if '>>' is used to request append mode, the header line is "
"not output)", 0 },
{ "csv-without-formula", OPT_CSV_NO_FORMULA, "[>>]FILENAME",
OPTION_ARG_OPTIONAL, "like --csv, but without 'fomula' column", 0 },
{ "csv-no-formula", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
{ "hide-status", OPT_HIDE, nullptr, 0,
"Hide the REALIZABLE or UNREALIZABLE line. (Hint: exit status "
"is enough of an indication.)", 0 },
@ -182,6 +186,7 @@ Exit status:\n\
2 if any error has been reported";
static const char* opt_csv = nullptr;
static bool opt_csv_with_formula = true;
static bool opt_print_pg = false;
static bool opt_print_hoa = false;
static const char* opt_print_hoa_args = nullptr;
@ -358,7 +363,10 @@ namespace
// (Even if that file was empty initially.)
if (!outf.append())
{
out << ("\"source\",\"formula\",\"algo\",\"tot_time\",\"trans_time\","
out << "\"source\",";
if (opt_csv_with_formula)
out << "\"formula\",";
out << ("\"algo\",\"tot_time\",\"trans_time\","
"\"split_time\",\"todpa_time\"");
if (!opt_print_pg && !opt_print_hoa)
{
@ -385,11 +393,14 @@ namespace
os.clear();
}
out << ',';
if (was_game)
os << filename;
else
os << f;
spot::escape_rfc4180(out << '"', os.str()) << "\",";
if (opt_csv_with_formula)
{
if (was_game)
os << filename;
else
os << f;
spot::escape_rfc4180(out << '"', os.str()) << "\",";
}
}
if (!was_game)
out << '"' << algo_names[(int) gi->s] << '"';
@ -763,7 +774,7 @@ namespace
int res = solve_formula(f, input_aps, output_aps);
if (opt_csv)
{
if (filename == 0 || linenum <= 0)
if (!filename || linenum <= 0)
{
print_csv(f, filename, false);
}
@ -996,6 +1007,11 @@ parse_opt(int key, char *arg, struct argp_state *)
break;
case OPT_CSV:
opt_csv = arg ? arg : "-";
opt_csv_with_formula = true;
break;
case OPT_CSV_NO_FORMULA:
opt_csv = arg ? arg : "-";
opt_csv_with_formula = false;
break;
case OPT_DECOMPOSE:
opt_decompose_ltl = XARGMATCH("--decompose", arg,

13
tests/core/ltlsynt2.test
View file

@ -82,7 +82,7 @@ EOF
diff filtered.csv expected
grep -v 0,0 filtered.csv >input.csv
ltlsynt -F input.csv/-2 --csv=out.csv -q || exit 2
ltlsynt -F input.csv/-2 --csv=out.csv -q
$PYTHON test.py
cat >expected <<EOF
source,formula,algo,realizable,strat_num_states
@ -92,3 +92,14 @@ input.csv:4,i1 <-> F(o1 xor o2),lar,1,3
input.csv:5,o1 & F(i1 <-> o2),lar,1,2
EOF
diff filtered.csv expected
ltlsynt -F input.csv/-2 --csv-without-formula=out.csv -q
cut out.csv -d, -f1,2 >filtered.csv
cat >expected <<EOF
"source","algo"
"input.csv:2","lar"
"input.csv:3","lar"
"input.csv:4","lar"
"input.csv:5","lar"
EOF
diff filtered.csv expected