parseaut: support multiple dstar automata
* src/parseaut/parseaut.yy, src/parseaut/scanaut.ll: All multiple dstar automata to be chained. * src/bin/dstar2tgba.cc: Loop over multiple automata in a file. * src/tests/dstar.test: Test that.
This commit is contained in:
Alexandre Duret-Lutz
parent
209e89a94c
commit
c59e994a2c
4 changed files with 98 additions and 28 deletions
|
|
@ -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;
|
||||
}
|
||||
};
|
||||
}
|
||||
|
|
|
|||
|
|
@ -228,6 +228,7 @@
|
|||
/**** LBTT tokens *****/
|
||||
// Also using INT, STRING
|
||||
%token ENDAUT "-1"
|
||||
%token ENDDSTAR "end of DSTAR automaton"
|
||||
%token <num> LBTT "LBTT header"
|
||||
%token <num> INT_S "state acceptance"
|
||||
%token <num> 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"
|
||||
{
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
}
|
||||
<<EOF>> return token::ENDDSTAR;
|
||||
}
|
||||
|
||||
<in_NEVER>{
|
||||
|
|
@ -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. */
|
||||
<in_LBTT_HEADER>{
|
||||
[0-9]+[st]* {
|
||||
|
|
|
|||
|
|
@ -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 <<EOF
|
||||
DRA v2 explicit
|
||||
|
|
@ -198,9 +198,21 @@ Acc-Sig: +0 +1
|
|||
4
|
||||
3
|
||||
4
|
||||
/* Same automaton with DSA instead of DRA, no comments, and less \n */
|
||||
DSA v2 explicit
|
||||
States: 5
|
||||
Acceptance-Pairs: 2
|
||||
Start: 0
|
||||
AP: 2 "a" "b"
|
||||
---
|
||||
State: 0 "bla" Acc-Sig: 1 2 3 4
|
||||
State: 1 "foo" Acc-Sig: -0 1 1 3 3
|
||||
State: 2 "baz" Acc-Sig: +0 1 2 3 4
|
||||
State: 3 "str\n\"ing" Acc-Sig: -0 +1 3 3 3 3
|
||||
State: 4 "more\"string\"" Acc-Sig: +0 +1 3 4 3 4
|
||||
EOF
|
||||
|
||||
run 0 ../ikwiad -XDB dra.dstar | tee stdout
|
||||
run 0 ../../bin/autfilt -B dra.dstar | tee stdout
|
||||
|
||||
cat >expected <<EOF
|
||||
digraph G {
|
||||
|
|
@ -227,12 +239,33 @@ digraph G {
|
|||
4 -> 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 <<EOF
|
||||
3 12 1 1 dra.dstar:1.1-42.70
|
||||
2 4 0 1 dra.dstar:43.1-54.1
|
||||
EOF
|
||||
|
||||
../../bin/dstar2tgba --name=%F:%L -D dra.dstar --stats '%s %t %p %d %m' > out
|
||||
cat out
|
||||
diff expected out
|
||||
|
||||
|
||||
# This has caused a crash at some point when dealing with 0-sized
|
||||
# bitsets to represent acceptance sets.
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue