Various utf-8 fixes.
* src/bin/ltl2tgba.cc: Add option -8. * src/tgbatest/ltl2tgba.cc, wrap/python/spot.i: Enable utf8 on sba_explicit_formula automata too.
This commit is contained in:
parent
4ed153a247
commit
f02156ebff
3 changed files with 29 additions and 3 deletions
|
|
@ -42,6 +42,7 @@
|
||||||
#include "tgbaalgos/neverclaim.hh"
|
#include "tgbaalgos/neverclaim.hh"
|
||||||
#include "tgbaalgos/postproc.hh"
|
#include "tgbaalgos/postproc.hh"
|
||||||
#include "tgbaalgos/save.hh"
|
#include "tgbaalgos/save.hh"
|
||||||
|
#include "tgba/bddprint.hh"
|
||||||
|
|
||||||
const char* argp_program_version = "\
|
const char* argp_program_version = "\
|
||||||
ltl2tgba (" SPOT_PACKAGE_STRING ")\n\
|
ltl2tgba (" SPOT_PACKAGE_STRING ")\n\
|
||||||
|
|
@ -87,6 +88,8 @@ static const argp_option options[] =
|
||||||
{ "lbtt", OPT_LBTT, 0, 0, "LBTT's format", 0 },
|
{ "lbtt", OPT_LBTT, 0, 0, "LBTT's format", 0 },
|
||||||
{ "spin", 's', 0, 0, "Spin neverclaim (implies --ba)", 0 },
|
{ "spin", 's', 0, 0, "Spin neverclaim (implies --ba)", 0 },
|
||||||
{ "spot", OPT_SPOT, 0, 0, "SPOT's format", 0 },
|
{ "spot", OPT_SPOT, 0, 0, "SPOT's format", 0 },
|
||||||
|
{ "utf8", '8', 0, 0, "enable UTF-8 characters in output "
|
||||||
|
"(works only with --spot or --dot)", 0 },
|
||||||
/**************************************************/
|
/**************************************************/
|
||||||
{ 0, 0, 0, 0, "Translation intent:", 4 },
|
{ 0, 0, 0, 0, "Translation intent:", 4 },
|
||||||
{ "small", OPT_SMALL, 0, 0, "prefer small automata (default)", 0 },
|
{ "small", OPT_SMALL, 0, 0, "prefer small automata (default)", 0 },
|
||||||
|
|
@ -121,6 +124,7 @@ spot::postprocessor::output_type type = spot::postprocessor::TGBA;
|
||||||
spot::postprocessor::output_pref pref = spot::postprocessor::Small;
|
spot::postprocessor::output_pref pref = spot::postprocessor::Small;
|
||||||
spot::postprocessor::optimization_level level = spot::postprocessor::High;
|
spot::postprocessor::optimization_level level = spot::postprocessor::High;
|
||||||
enum output_format { Dot, Lbtt, Spin, Spot } format = Dot;
|
enum output_format { Dot, Lbtt, Spin, Spot } format = Dot;
|
||||||
|
bool utf8 = false;
|
||||||
|
|
||||||
static int
|
static int
|
||||||
parse_opt(int key, char* arg, struct argp_state*)
|
parse_opt(int key, char* arg, struct argp_state*)
|
||||||
|
|
@ -128,6 +132,9 @@ parse_opt(int key, char* arg, struct argp_state*)
|
||||||
// This switch is alphabetically-ordered.
|
// This switch is alphabetically-ordered.
|
||||||
switch (key)
|
switch (key)
|
||||||
{
|
{
|
||||||
|
case '8':
|
||||||
|
spot::enable_utf8();
|
||||||
|
break;
|
||||||
case 'a':
|
case 'a':
|
||||||
pref = spot::postprocessor::Any;
|
pref = spot::postprocessor::Any;
|
||||||
break;
|
break;
|
||||||
|
|
@ -231,6 +238,17 @@ namespace
|
||||||
const spot::tgba* aut = ltl_to_tgba_fm(f, simpl.get_dict(), exprop);
|
const spot::tgba* aut = ltl_to_tgba_fm(f, simpl.get_dict(), exprop);
|
||||||
aut = post.run(aut, f);
|
aut = post.run(aut, f);
|
||||||
|
|
||||||
|
if (utf8)
|
||||||
|
{
|
||||||
|
spot::tgba* a = const_cast<spot::tgba*>(aut);
|
||||||
|
if (spot::tgba_explicit_formula* tef =
|
||||||
|
dynamic_cast<spot::tgba_explicit_formula*>(a))
|
||||||
|
tef->enable_utf8();
|
||||||
|
else if (spot::sba_explicit_formula* sef =
|
||||||
|
dynamic_cast<spot::sba_explicit_formula*>(a))
|
||||||
|
sef->enable_utf8();
|
||||||
|
}
|
||||||
|
|
||||||
switch (format)
|
switch (format)
|
||||||
{
|
{
|
||||||
case Dot:
|
case Dot:
|
||||||
|
|
|
||||||
|
|
@ -1294,9 +1294,14 @@ main(int argc, char** argv)
|
||||||
}
|
}
|
||||||
|
|
||||||
if (utf8_opt)
|
if (utf8_opt)
|
||||||
if (spot::tgba_explicit_formula* tef =
|
{
|
||||||
dynamic_cast<spot::tgba_explicit_formula*>(a))
|
if (spot::tgba_explicit_formula* tef =
|
||||||
tef->enable_utf8();
|
dynamic_cast<spot::tgba_explicit_formula*>(a))
|
||||||
|
tef->enable_utf8();
|
||||||
|
else if (spot::sba_explicit_formula* sef =
|
||||||
|
dynamic_cast<spot::sba_explicit_formula*>(a))
|
||||||
|
sef->enable_utf8();
|
||||||
|
}
|
||||||
|
|
||||||
if (output != -1)
|
if (output != -1)
|
||||||
{
|
{
|
||||||
|
|
|
||||||
|
|
@ -362,6 +362,9 @@ tgba_enable_utf8(spot::tgba* a)
|
||||||
if (spot::tgba_explicit_formula* tef =
|
if (spot::tgba_explicit_formula* tef =
|
||||||
dynamic_cast<spot::tgba_explicit_formula*>(a))
|
dynamic_cast<spot::tgba_explicit_formula*>(a))
|
||||||
tef->enable_utf8();
|
tef->enable_utf8();
|
||||||
|
else if (spot::sba_explicit_formula* sef =
|
||||||
|
dynamic_cast<spot::sba_explicit_formula*>(a))
|
||||||
|
sef->enable_utf8();
|
||||||
}
|
}
|
||||||
|
|
||||||
spot::ltl::parse_error_list
|
spot::ltl::parse_error_list
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue