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

hoa: allow dots in identifiers

Browse source 
As discussed at https://github.com/adl/hoaf/issues/56

* src/parseaut/scanaut.ll: Allow dots.
* src/tests/parseaut.test: Test it.
* NEWS: Mention it.
This commit is contained in:
Alexandre Duret-Lutz 2015-12-02 15:28:05 +01:00
parent c60c117714
commit e357c0c5bc
3 changed files with 15 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

6
NEWS
View file

@ -78,6 +78,10 @@ New in spot 1.99.5a (not yet released)
in the HOA format, and furthermore the parse_aut() function now in the HOA format, and furthermore the parse_aut() function now
has an option to read HOA file and produce them as kripke_graph. has an option to read HOA file and produce them as kripke_graph.
* The HOA parser now accepts identifier, aliases, and headernames
containing dots, as this will be allowed in the next version of
the HOA format.
* Renamings: * Renamings:
is_guarantee_automaton() -> is_terminal_automaton() is_guarantee_automaton() -> is_terminal_automaton()
tgba_run -> twa_run tgba_run -> twa_run
@ -90,7 +94,7 @@ New in spot 1.99.5a (not yet released)
* Better interface for sat_minimize(). * Better interface for sat_minimize().
Bug fixes: Bug fixes:
* automaton parser was ignoring the "unambiguous" property. * the HOA parser was ignoring the "unambiguous" property.
* --dot=Bb should work like --dot=b, allowing us to disable * --dot=Bb should work like --dot=b, allowing us to disable
a B option set via an environment variable. a B option set via an environment variable.

4
src/parseaut/scanaut.ll
View file

@ -44,7 +44,7 @@ static unsigned lbtt_states = 0;
eol \n+|\r+ eol \n+|\r+
eol2 (\n\r)+|(\r\n)+ eol2 (\n\r)+|(\r\n)+
eols ({eol}|{eol2})* eols ({eol}|{eol2})*
identifier [[:alpha:]_][[:alnum:]_-]* identifier [[:alpha:]_][[:alnum:]_.-]*
%x in_COMMENT in_STRING in_NEVER_PAR %x in_COMMENT in_STRING in_NEVER_PAR
%s in_HOA in_NEVER in_LBTT_HEADER %s in_HOA in_NEVER in_LBTT_HEADER
@ -131,7 +131,7 @@ identifier [[:alpha:]_][[:alnum:]_-]*
yylval->str = new std::string(yytext, yyleng - 1); yylval->str = new std::string(yytext, yyleng - 1);
return token::HEADERNAME; return token::HEADERNAME;
} }
"@"[[:alnum:]_-]+ { "@"[[:alnum:]_.-]+ {
yylval->str = new std::string(yytext + 1, yyleng - 1); yylval->str = new std::string(yytext + 1, yyleng - 1);
return token::ANAME; return token::ANAME;
} }

16
src/tests/parseaut.test
View file

@ -253,7 +253,7 @@ HOA: v2
HOA: w1 HOA: w1
--BODY-- --BODY--
--END-- --END--
HOA: v1_1 HOA: v1.1
--BODY-- --BODY--
--END-- --END--
EOF EOF
@ -266,7 +266,7 @@ input:12.6-7: unsupported HOA version
input:12.1-7: missing 'Acceptance:' header input:12.1-7: missing 'Acceptance:' header
input:15.6-7: unknown HOA version input:15.6-7: unknown HOA version
input:15.1-7: missing 'Acceptance:' header input:15.1-7: missing 'Acceptance:' header
input:18.6-9: we can read HOA v1 but this file uses v1_1; $t input:18.6-9: we can read HOA v1 but this file uses v1.1; $t
input:18.1-9: missing 'Acceptance:' header input:18.1-9: missing 'Acceptance:' header
EOF EOF
@ -478,7 +478,7 @@ input:17.11-13: unknown alias @bc
EOF EOF
cat >input <<EOF cat >input <<EOF
HOA: v1 HOA: v1.1
name: "GFa & GF(b & c)" name: "GFa & GF(b & c)"
States: 1 States: 1
Start: 0 Start: 0
@ -486,13 +486,13 @@ cat >input <<EOF
Acceptance: 2 (Inf(0) & Inf(1)) Acceptance: 2 (Inf(0) & Inf(1))
AP: 3 "a" "b" "c" AP: 3 "a" "b" "c"
Alias: @a 0 Alias: @a 0
Alias: @bc 1 & 2 Alias: @b.c 1 & 2
--BODY-- --BODY--
State: 0 State: 0
[!@a & !@bc] 0 [!@a & !@b.c] 0
[@a & !@bc] 0 {0} [@a & !@b.c] 0 {0}
[!@a & @bc] 0 {1} [!@a & @b.c] 0 {1}
[@a & @bc] 0 {0 1} [@a & @b.c] 0 {0 1}
--END-- --END--
/* Some comment */ /* Some comment */
HOA: v1 HOA: v1