diff --git a/src/bin/dstar2tgba.cc b/src/bin/dstar2tgba.cc index 3395ea021..8454d1227 100644 --- a/src/bin/dstar2tgba.cc +++ b/src/bin/dstar2tgba.cc @@ -46,11 +46,11 @@ #include "twaalgos/sccinfo.hh" static const char argp_program_doc[] ="\ -Convert Rabin and Streett automata into Büchi automata.\n\n\ -This reads the output format of ltl2dstar and will output a\n\ -Transition-based Generalized Büchi Automata in GraphViz's format by default.\n\ -If multiple files are supplied (one automaton per file), several automata\n\ -will be output."; +Convert automata with any acceptance condition into variants of \ +Büchi automata.\n\nThis reads automata into any supported format \ +(HOA, LBTT, ltl2dstar, never claim) and outputs a \ +Transition-based Generalized Büchi Automata in GraphViz's format by default. \ +Each supplied file may contain multiple automata."; enum { OPT_TGBA = 1, @@ -143,26 +143,53 @@ namespace SPOT_UNREACHABLE(); } + int + process_automaton(const spot::const_parsed_aut_ptr& haut, + const char* filename) + { + spot::stopwatch sw; + sw.start(); + auto nba = spot::to_generalized_buchi(haut->aut); + auto aut = post.run(nba, 0); + const double conversion_time = sw.stop(); + + printer.print(aut, nullptr, filename, -1, conversion_time, haut); + flush_cout(); + return 0; + } + + int + aborted(const spot::const_parsed_aut_ptr& h, const char* filename) + { + std::cerr << filename << ':' << h->loc << ": aborted input automaton\n"; + return 2; + } int process_file(const char* filename) { spot::parse_aut_error_list pel; - auto daut = spot::parse_aut(filename, pel, spot::make_bdd_dict()); - if (spot::format_parse_aut_errors(std::cerr, filename, pel)) - return 2; - if (!daut) - error(2, 0, "failed to read automaton from %s", filename); + auto hp = spot::automaton_stream_parser(filename); - spot::stopwatch sw; - sw.start(); - auto nba = spot::to_generalized_buchi(daut->aut); - auto aut = post.run(nba, 0); - const double conversion_time = sw.stop(); + int err = 0; - printer.print(aut, nullptr, filename, -1, conversion_time, daut); - flush_cout(); - return 0; + while (!abort_run) + { + pel.clear(); + auto haut = hp.parse(pel, spot::make_bdd_dict()); + if (!haut && pel.empty()) + break; + if (spot::format_parse_aut_errors(std::cerr, filename, pel)) + err = 2; + if (!haut) + error(2, 0, "failed to read automaton from %s", filename); + else if (haut->aborted) + err = std::max(err, aborted(haut, filename)); + else + process_automaton(haut, filename); + } + + return err; } }; } diff --git a/src/parseaut/parseaut.yy b/src/parseaut/parseaut.yy index bf817af2b..312a4e068 100644 --- a/src/parseaut/parseaut.yy +++ b/src/parseaut/parseaut.yy @@ -228,6 +228,7 @@ /**** LBTT tokens *****/ // Also using INT, STRING %token ENDAUT "-1" +%token ENDDSTAR "end of DSTAR automaton" %token LBTT "LBTT header" %token INT_S "state acceptance" %token LBTT_EMPTY "acceptance sets for empty automaton" @@ -261,10 +262,10 @@ aut: aut-1 { res.h->loc = @$; YYACCEPT; } | ENDOFFILE { YYABORT; } | error ENDOFFILE { YYABORT; } -aut-1: hoa { res.h->type = spot::parsed_aut_type::HOA; } - | never { res.h->type = spot::parsed_aut_type::NeverClaim; } - | lbtt { res.h->type = spot::parsed_aut_type::LBTT; } - | dstar /* we will set type as DSA or DRA while parsing first line */ +aut-1: hoa { res.h->type = spot::parsed_aut_type::HOA; } + | never { res.h->type = spot::parsed_aut_type::NeverClaim; } + | lbtt { res.h->type = spot::parsed_aut_type::LBTT; } + | dstar /* will set type as DSA or DRA while parsing first line */ /**********************************************************************/ /* Rules for HOA */ @@ -1101,7 +1102,7 @@ incorrectly-labeled-edge: trans-label unlabeled-edge /* Rules for LTL2DSTAR's format */ /**********************************************************************/ -dstar: dstar_header "---" dstar_states +dstar: dstar_header "---" dstar_states ENDDSTAR dstar_type: "DRA" { diff --git a/src/parseaut/scanaut.ll b/src/parseaut/scanaut.ll index 324a5bcfe..ea28676fa 100644 --- a/src/parseaut/scanaut.ll +++ b/src/parseaut/scanaut.ll @@ -43,6 +43,7 @@ static unsigned lbtt_states = 0; eol \n+|\r+ eol2 (\n\r)+|(\r\n)+ +eols ({eol}|{eol2})* identifier [[:alpha:]_][[:alnum:]_-]* %x in_COMMENT in_STRING in_NEVER_PAR @@ -150,6 +151,14 @@ identifier [[:alpha:]_][[:alnum:]_-]* "Acc-Sig:" return token::ACCSIG; "---" return token::ENDOFHEADER; [0-9]+ parse_int(); return token::INT; + /* The start of any automaton is the end of this one. + We do not try to detect LBTT automata, as that would + be too hard to distinguish from state numbers. */ + ""/{eols}("HOA:"|"never"|"DSA"|"DRA") { + BEGIN(INITIAL); + return token::ENDDSTAR; + } + <> return token::ENDDSTAR; } { @@ -185,7 +194,7 @@ identifier [[:alpha:]_][[:alnum:]_-]* If we only tokenize it as a stream of INTs, the parser will have a very hard time recognizing what is a state from what is a transitions. As a consequence we abuse the start conditions to - maintain a state an return integers with different sementic types + maintain a state an return integers with different semantic types depending on the purpose of those integers. */ { [0-9]+[st]* { diff --git a/src/tests/dstar.test b/src/tests/dstar.test index 0d7d1e003..7e161739a 100755 --- a/src/tests/dstar.test +++ b/src/tests/dstar.test @@ -154,7 +154,7 @@ test "`../../bin/dstar2tgba -DC dsa.dstar --stats '%s %t %p %d'`" = "5 11 1 0" # DRA generated with -# ltlfilt -f 'Ga | Fb' -l | ltl2dstar --ltl2nba=spin:path/ltl2tgba@-sD - - +# ltlfilt -f 'Ga | Fb' -l | ltl2dstar --ltl2nba=spin:path/ltl2tgba@-Ds - - # (State name and comments added by hand to test the parser.) cat >dra.dstar <expected < 3 [label="!a"] 4 -> 4 [label="a"] } +digraph G { + rankdir=LR + node [shape="circle"] + I [label="", style=invis, width=0] + I -> 0 + 0 [label="0"] + 0 -> 1 [label="!a & !b"] + 0 -> 2 [label="a & !b"] + 1 [label="1", peripheries=2] + 1 -> 1 [label="!b"] + 2 [label="2"] + 2 -> 1 [label="!a & !b"] + 2 -> 2 [label="a & !b"] +} EOF diff expected stdout -test "`../../bin/dstar2tgba --name=%F -D dra.dstar --stats '%s %t %p %d %m'`" \ - = "3 12 1 1 dra.dstar" +cat >expected < out +cat out +diff expected out + # This has caused a crash at some point when dealing with 0-sized # bitsets to represent acceptance sets.