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

ltlcross: add support for reading TGBA as HOA

Browse source 
* src/bin/ltlcross.cc: Add a %H modifier.
* src/tgbatest/ltlcross2.test: Exercise it.
This commit is contained in:
Alexandre Duret-Lutz 2014-11-19 16:38:14 +01:00
parent e55bcd95aa
commit 622fe08f00
2 changed files with 38 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

35
src/bin/ltlcross.cc
View file

@ -38,6 +38,7 @@
#include "common_finput.hh" #include "common_finput.hh"
#include "neverparse/public.hh" #include "neverparse/public.hh"
#include "dstarparse/public.hh" #include "dstarparse/public.hh"
#include "hoaparse/public.hh"
#include "ltlast/unop.hh" #include "ltlast/unop.hh"
#include "ltlvisit/tostring.hh" #include "ltlvisit/tostring.hh"
#include "ltlvisit/apcollect.hh" #include "ltlvisit/apcollect.hh"
@ -709,7 +710,7 @@ namespace
public spot::printable_value<spot::temporary_file*> public spot::printable_value<spot::temporary_file*>
{ {
unsigned translator_num; unsigned translator_num;
enum output_format { None, Spin, Lbtt, Dstar }; enum output_format { None, Spin, Lbtt, Dstar, Hoa };
mutable output_format format; mutable output_format format;
printable_result_filename() printable_result_filename()
@ -744,6 +745,8 @@ namespace
format = Lbtt; format = Lbtt;
else if (*pos == 'D') else if (*pos == 'D')
format = Dstar; format = Dstar;
else if (*pos == 'H')
format = Hoa;
else else
SPOT_UNREACHABLE(); SPOT_UNREACHABLE();
@ -752,7 +755,8 @@ namespace
// It's OK to use a specified multiple time, but it's not OK // It's OK to use a specified multiple time, but it's not OK
// to mix the formats. // to mix the formats.
if (format != old_format) if (format != old_format)
error(2, 0, "you may not mix %%D, %%N, and %%T specifiers: %s", error(2, 0,
"you may not mix %%D, %%H, %%N, and %%T specifiers: %s",
translators[translator_num].spec); translators[translator_num].spec);
} }
else else
@ -796,6 +800,7 @@ namespace
declare('L', &filename_ltl_lbt); declare('L', &filename_ltl_lbt);
declare('W', &filename_ltl_wring); declare('W', &filename_ltl_wring);
declare('D', &output); declare('D', &output);
declare('H', &output);
declare('N', &output); declare('N', &output);
declare('T', &output); declare('T', &output);
@ -814,9 +819,9 @@ namespace
"one of %%f,%%s,%%l,%%w,%%F,%%S,%%L,%%W to indicate how " "one of %%f,%%s,%%l,%%w,%%F,%%S,%%L,%%W to indicate how "
"to pass the formula.", t.spec); "to pass the formula.", t.spec);
bool has_d = has['D']; bool has_d = has['D'];
if (!(has_d || has['N'] || has['T'])) if (!(has_d || has['N'] || has['T'] || has['H']))
error(2, 0, "no output %%-sequence in '%s'.\n Use one of " error(2, 0, "no output %%-sequence in '%s'.\n Use one of "
"%%D,%%N,%%T to indicate where the automaton is saved.", "%%D,%%H,%%N,%%T to indicate where the automaton is saved.",
t.spec); t.spec);
has_sr |= has_d; has_sr |= has_d;
@ -1034,6 +1039,28 @@ namespace
} }
break; break;
} }
case printable_result_filename::Hoa:
{
spot::hoa_parse_error_list pel;
std::string filename = output.val()->name();
auto aut = spot::hoa_parse(filename, pel, dict);
if (!pel.empty())
{
status_str = "parse error";
problem = true;
es = -1;
std::ostream& err = global_error();
err << "error: failed to parse the produced HOA file.\n";
spot::format_hoa_parse_errors(err, filename, pel);
end_error();
res = nullptr;
}
else
{
res = aut->aut;
}
break;
}
case printable_result_filename::None: case printable_result_filename::None:
SPOT_UNREACHABLE(); SPOT_UNREACHABLE();
} }

14
src/tgbatest/ltlcross2.test
View file

@ -27,19 +27,19 @@ ltl2tgba=../../bin/ltl2tgba
../../bin/ltlcross --products=3 --timeout=60 \ ../../bin/ltlcross --products=3 --timeout=60 \
"$ltl2tgba --lbtt --any --low %f > %T" \ "$ltl2tgba --lbtt --any --low %f > %T" \
"$ltl2tgba --lbtt --any --medium %f > %T" \ "$ltl2tgba --lbtt --any --medium %f > %T" \
"$ltl2tgba --lbtt --any --high %f > %T" \ "$ltl2tgba --hoa --any --high %f > %H" \
"$ltl2tgba --lbtt --deterministic --low %f > %T" \ "$ltl2tgba --lbtt --deterministic --low %f > %T" \
"$ltl2tgba --lbtt --deterministic --medium %f > %T" \ "$ltl2tgba --lbtt --deterministic --medium %f > %T" \
"$ltl2tgba --lbtt --deterministic --high %f > %T" \ "$ltl2tgba --lbtt --deterministic --high %f > %T" \
"$ltl2tgba --lbtt --small --low %f > %T" \ "$ltl2tgba --lbtt --small --low %f > %T" \
"$ltl2tgba --lbtt --small --medium %f > %T" \ "$ltl2tgba --hoa --small --medium %f > %H" \
"$ltl2tgba --lbtt --small --high %f > %T" \ "$ltl2tgba --lbtt --small --high %f > %T" \
"$ltl2tgba --lbtt -x comp-susp --small %f >%T" \ "$ltl2tgba --lbtt -x comp-susp --small %f >%T" \
"$ltl2tgba --lbtt -x comp-susp,!skel-wdba --lbtt --small %f >%T" \ "$ltl2tgba --lbtt -x comp-susp,!skel-wdba --small %f >%T" \
"$ltl2tgba --lbtt -x comp-susp,early-susp --lbtt --small %f >%T" \ "$ltl2tgba --lbtt -x comp-susp,early-susp --small %f >%T" \
"$ltl2tgba --lbtt -x comp-susp,!skel-wdba,!skel-simul --lbtt --small %f >%T" \ "$ltl2tgba --lbtt -x comp-susp,!skel-wdba,!skel-simul --small %f >%T" \
"$ltl2tgba --lbtt --ba -x degen-skip=0 --lbtt %f >%T" \ "$ltl2tgba --spin --ba -x degen-skip=0 %f >%N" \
"$ltl2tgba --lbtt --ba --high %f > %T" \ "$ltl2tgba --lbtt --ba --high %f > %T" \
"$ltl2tgba --lbtt -BDC %f > %T" \ "$ltl2tgba --hoa -BDC %f > %H" \
"$ltl2tgba --lbtt -BC %f > %T" \ "$ltl2tgba --lbtt -BC %f > %T" \
--json=output.json --csv=output.csv --json=output.json --csv=output.csv