Commit e1bba500 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

hoa: swallow the neverclaim parser

This way we can easily parse a stream of HOAs intermixed with
neverclaims.

* src/hoaparse/hoaparse.yy, src/hoaparse/hoascan.ll: Add rules
for neverclaims, adjusted from src/neverparse/neverclaimparse.yy
and src/neverparse/neverclaimparse.ll.
* src/hoaparse/public.hh, NEWS: Update documentation.
* src/neverparse/: Remove this directory.
* README, configure.ac, src/Makefile.am: Adjust accordingly.
* src/tgbatest/ltl2tgba.cc, src/bin/ltlcross.cc: Use HOA
parser to read neverclaims.
* src/tgbatest/hoaparse.test, src/tgbatest/neverclaimread.test: Adjust.
parent 39eefd0c
......@@ -43,6 +43,12 @@ New in spot 1.99a (not yet released)
used in a stream. The parser currently ignore all optional
headers (starting with a lowercase letter).
- The above HOA parser can also parse neverclaims, so the
neverclaim parser has been removed. This implies that
autfilt can input a mix of HOA and neverclaims, and that
ltlcross' %N and %H specifiers (used to indicate whether
a tool produces neverclaims or HOA) are now synonyms.
- randomize() is a new algorithm that reorder the states
and transition of an automaton at random. It can be
used from the command-line using "autfilt --randomize".
......
......@@ -142,7 +142,7 @@ src/ Sources for libspot.
dstarparse/ Parser for the output of ltl2dstar.
graph/ Graph representations.
graphtest/ Graph representations.
hoaparse/ Parser for the HOA format.
hoaparse/ Parser for HOA automata and Spin's never claims.
kripke/ Kripke Structure interface.
kripkeparse/ Parser for explicit Kripke.
kripketest/ Tests for kripke explicit.
......@@ -152,7 +152,6 @@ src/ Sources for libspot.
ltlvisit/ Visitors of LTL formulae.
ltltest/ Tests for ltlast/, ltlenv/, ltlparse/, and ltlvisit/.
misc/ Miscellaneous support files.
neverparse/ Parser for SPIN never claims.
priv/ Private algorithms, used internally but not exported.
tgba/ TGBA objects and cousins.
tgbaalgos/ Algorithms on TGBA.
......
......@@ -192,7 +192,6 @@ AC_CONFIG_FILES([
src/ltlvisit/Makefile
src/Makefile
src/misc/Makefile
src/neverparse/Makefile
src/priv/Makefile
src/sanity/Makefile
src/tgbaalgos/gtec/Makefile
......
......@@ -26,9 +26,9 @@ AUTOMAKE_OPTIONS = subdir-objects
# end, after building '.' (since the current directory contains
# libspot.la needed by the tests)
SUBDIRS = misc priv ltlenv ltlast ltlvisit ltlparse graph tgba \
tgbaalgos tgbaparse ta taalgos kripke neverparse \
kripkeparse dstarparse hoaparse . bin ltltest graphtest \
tgbatest kripketest sanity
tgbaalgos tgbaparse ta taalgos kripke kripkeparse \
dstarparse hoaparse . bin ltltest graphtest tgbatest \
kripketest sanity
lib_LTLIBRARIES = libspot.la
libspot_la_SOURCES =
......@@ -43,7 +43,6 @@ libspot_la_LIBADD = \
ltlparse/libltlparse.la \
ltlvisit/libltlvisit.la \
misc/libmisc.la \
neverparse/libneverparse.la \
priv/libpriv.la \
taalgos/libtaalgos.la \
ta/libta.la \
......
......@@ -36,7 +36,6 @@
#include "common_setup.hh"
#include "common_cout.hh"
#include "common_finput.hh"
#include "neverparse/public.hh"
#include "dstarparse/public.hh"
#include "hoaparse/public.hh"
#include "ltlast/unop.hh"
......@@ -115,9 +114,9 @@ static const argp_option options[] =
0 },
{ "%F,%S,%L,%W", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
"the formula as a file in Spot, Spin, LBT, or Wring's syntax", 0 },
{ "%N,%T,%D", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
"the output automaton as a Never claim, in LBTT's or in LTL2DSTAR's "
"format", 0 },
{ "%N,%T,%D,%H", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
"the automaton is output as a Never claim, or in LBTT's, in LTL2DSTAR's,"
"or in the HOA format", 0 },
{ 0, 0, 0, 0,
"If either %l, %L, or %T are used, any input formula that does "
"not use LBT-style atomic propositions (i.e. p0, p1, ...) will be "
......@@ -710,7 +709,7 @@ namespace
public spot::printable_value<spot::temporary_file*>
{
unsigned translator_num;
enum output_format { None, Spin, Lbtt, Dstar, Hoa };
enum output_format { None, Lbtt, Dstar, Hoa };
mutable output_format format;
printable_result_filename()
......@@ -740,7 +739,7 @@ namespace
{
output_format old_format = format;
if (*pos == 'N')
format = Spin;
format = Hoa; // The HOA parse also reads neverclaims
else if (*pos == 'T')
format = Lbtt;
else if (*pos == 'D')
......@@ -939,24 +938,6 @@ namespace
es = 0;
switch (output.format)
{
case printable_result_filename::Spin:
{
spot::neverclaim_parse_error_list pel;
std::string filename = output.val()->name();
res = spot::neverclaim_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 neverclaim.\n";
spot::format_neverclaim_parse_errors(err, filename, pel);
end_error();
res = nullptr;
}
break;
}
case printable_result_filename::Lbtt:
{
std::string error;
......@@ -1039,7 +1020,7 @@ namespace
}
break;
}
case printable_result_filename::Hoa:
case printable_result_filename::Hoa: // Will also read neverclaims
{
spot::hoa_parse_error_list pel;
std::string filename = output.val()->name();
......@@ -1050,7 +1031,7 @@ namespace
problem = true;
es = -1;
std::ostream& err = global_error();
err << "error: failed to parse the produced HOA file.\n";
err << "error: failed to parse the produced automaton.\n";
spot::format_hoa_parse_errors(err, filename, pel);
end_error();
res = nullptr;
......
......@@ -35,8 +35,18 @@
#include <unordered_map>
#include <algorithm>
#include "ltlast/constant.hh"
#include "tgba/formula2bdd.hh"
#include "public.hh"
/* Cache parsed formulae. Labels on arcs are frequently identical
and it would be a waste of time to parse them to formula* over and
over, and to register all their atomic_propositions in the
bdd_dict. Keep the bdd result around so we can reuse it. */
typedef std::map<std::string, bdd> formula_cache;
typedef std::pair<int, std::string*> pair;
typedef typename spot::tgba_digraph::namer<std::string>::type named_tgba_t;
// Note: because this parser is meant to be used on a stream of
// automata, it tries hard to recover from errors, so that we get a
// chance to reach the end of the current automaton in order to
......@@ -46,6 +56,8 @@
{
spot::hoa_aut_ptr h;
spot::ltl::environment* env;
formula_cache fcache;
named_tgba_t* namer = nullptr;
std::vector<int> ap;
std::vector<bdd> guards;
std::vector<bdd>::const_iterator cur_guard;
......@@ -73,6 +85,15 @@
bool ignore_acc_silent = false;
bool ignore_more_acc = false; // Set to true after the first
// "Acceptance:" line has been read.
bool accept_all_needed = false;
bool accept_all_seen = false;
std::map<std::string, spot::location> labels;
~result_()
{
delete namer;
}
};
}
......@@ -88,12 +109,17 @@
unsigned int num;
int b;
spot::acc_cond::mark_t mark;
pair* p;
std::list<pair>* list;
}
%code
{
#include <sstream>
/* hoaparse.hh and parsedecl.hh include each other recursively.
#include "ltlast/constant.hh"
#include "ltlparse/public.hh"
/* hoaparse.hh and parsedecl.hh include each other recursively.
We must ensure that YYSTYPE is declared (by the above %union)
before parsedecl.hh uses it. */
#include "parsedecl.hh"
......@@ -101,6 +127,7 @@
static void fill_guards(result_& res);
}
/**** HOA tokens ****/
%token HOA "HOA:"
%token STATES "States:"
%token START "Start:"
......@@ -114,7 +141,7 @@
%token BODY "--BODY--"
%token END "--END--"
%token STATE "State:";
%token <str> IDENTIFIER "identifier";
%token <str> IDENTIFIER "identifier"; // also used by neverclaim
%token <str> HEADERNAME "header name";
%token <str> ANAME "alias name";
%token <str> STRING "string";
......@@ -129,8 +156,42 @@
%type <b> label-expr
%type <mark> acc-sig_opt acc-sets
/**** NEVERCLAIM tokens ****/
%token NEVER "never"
%token SKIP "skip"
%token IF "if"
%token FI "fi"
%token DO "do"
%token OD "od"
%token ARROW "->"
%token GOTO "goto"
%token FALSE "false"
%token ATOMIC "atomic"
%token ASSERT "assert"
%token <str> FORMULA "boolean formula"
%type <b> nc-formula
%type <str> nc-opt-dest nc-formula-or-ident
%type <p> nc-transition nc-src-dest
%type <list> nc-transitions nc-transition-block
%type <str> nc-one-ident nc-ident-list
%destructor { delete $$; } <str>
%destructor { bdd_delref($$); } <b>
%destructor { bdd_delref($$->first); delete $$->second; delete $$; } <p>
%destructor {
for (std::list<pair>::iterator i = $$->begin();
i != $$->end(); ++i)
{
bdd_delref(i->first);
delete i->second;
}
delete $$;
} <list>
%printer {
if ($$)
debug_stream() << *$$;
......@@ -139,22 +200,18 @@
%printer { debug_stream() << $$; } <num>
%%
aut: aut-1 { res.h->loc = @$; YYACCEPT; }
| ENDOFFILE { YYABORT; }
aut-1: hoa | never
/**********************************************************************/
/* Rules for HOA */
/**********************************************************************/
hoa: header "--BODY--" body "--END--"
{
res.h->loc = @$;
YYACCEPT;
}
hoa: error "--END--"
{
res.h->loc = @$;
YYACCEPT;
}
hoa: error ENDOFFILE
{
res.h->loc = @$;
YYACCEPT;
}
hoa: ENDOFFILE { YYABORT; }
string_opt: | STRING
BOOLEAN: 't' | 'f'
......@@ -660,6 +717,200 @@ incorrectly-labeled-edge: trans-label unlabeled-edge
" edge has no label");
}
/**********************************************************************/
/* Rules for neverclaims */
/**********************************************************************/
never: "never" { res.namer = res.h->aut->create_namer<std::string>();
res.h->aut->set_single_acceptance_set();
res.h->aut->prop_state_based_acc(); }
'{' nc-states '}'
{
// Add an accept_all state if needed.
if (res.accept_all_needed && !res.accept_all_seen)
{
unsigned n = res.namer->new_state("accept_all");
res.h->aut->new_acc_transition(n, n, bddtrue);
}
}
nc-states:
/* empty */
| nc-state
| nc-states ';' nc-state
| nc-states ';'
nc-one-ident: IDENTIFIER ':'
{
unsigned n = res.namer->new_state(*$1);
if (res.labels.empty())
{
// The first state is initial.
res.start.emplace_back(@$, n);
}
auto r = res.labels.insert(std::make_pair(*$1, @1));
if (!r.second)
{
error(@1, std::string("redefinition of ") + *$1 + "...");
error(r.first->second, std::string("... ") + *$1
+ " previously defined here");
}
$$ = $1;
}
nc-ident-list: nc-one-ident
| nc-ident-list nc-one-ident
{
res.namer->alias_state(res.namer->get_state(*$1), *$2);
// Keep any identifier that starts with accept.
if (strncmp("accept", $1->c_str(), 6))
{
delete $1;
$$ = $2;
}
else
{
delete $2;
$$ = $1;
}
}
nc-transition-block:
"if" nc-transitions "fi"
{
$$ = $2;
}
| "do" nc-transitions "od"
{
$$ = $2;
}
nc-state:
nc-ident-list "skip"
{
if (*$1 == "accept_all")
res.accept_all_seen = true;
res.namer->new_transition(*$1, *$1, bddtrue,
!strncmp("accept", $1->c_str(), 6) ?
res.h->aut->acc().all_sets() :
spot::acc_cond::mark_t(0U));
delete $1;
}
| nc-ident-list { delete $1; }
| nc-ident-list "false" { delete $1; }
| nc-ident-list nc-transition-block
{
auto acc = !strncmp("accept", $1->c_str(), 6) ?
res.h->aut->acc().all_sets() : spot::acc_cond::mark_t(0U);
for (auto& p: *$2)
{
bdd c = bdd_from_int(p.first);
bdd_delref(p.first);
res.namer->new_transition(*$1, *p.second, c, acc);
delete p.second;
}
delete $1;
delete $2;
}
nc-transitions:
/* empty */ { $$ = new std::list<pair>; }
| nc-transitions nc-transition
{
if ($2)
{
$1->push_back(*$2);
delete $2;
}
$$ = $1;
}
nc-formula-or-ident: FORMULA | IDENTIFIER
nc-formula: nc-formula-or-ident
{
auto i = res.fcache.find(*$1);
if (i == res.fcache.end())
{
spot::ltl::parse_error_list pel;
auto f = spot::ltl::parse_boolean(*$1, pel, *res.env,
debug_level(), true);
for (auto& j: pel)
{
// Adjust the diagnostic to the current position.
spot::location here = @1;
here.end.line = here.begin.line + j.first.end.line - 1;
here.end.column = here.begin.column + j.first.end.column;
here.begin.line += j.first.begin.line - 1;
here.begin.column += j.first.begin.column;
error_list.emplace_back(here, j.second);
}
bdd cond = bddfalse;
if (f)
{
cond = spot::formula_to_bdd(f, res.h->aut->get_dict(),
res.h->aut);
f->destroy();
}
$$ = (res.fcache[*$1] = cond).id();
}
else
{
$$ = i->second.id();
}
bdd_addref($$);
delete $1;
}
| "false"
{
$$ = 0;
}
nc-opt-dest:
/* empty */
{
$$ = 0;
}
| "->" "goto" IDENTIFIER
{
$$ = $3;
}
| "->" "assert" FORMULA
{
delete $3;
$$ = new std::string("accept_all");
res.accept_all_needed = true;
}
nc-src-dest: nc-formula nc-opt-dest
{
// If there is no destination, do ignore the transition.
// This happens for instance with
// if
// :: false
// fi
if (!$2)
{
$$ = 0;
}
else
{
$$ = new pair($1, $2);
res.namer->new_state(*$2);
}
}
nc-transition:
':' ':' "atomic" '{' nc-src-dest '}'
{
$$ = $5;
}
| ':' ':' nc-src-dest
{
$$ = $3;
}
%%
static void fill_guards(result_& r)
......
......@@ -25,12 +25,16 @@
%{
#include <string>
#include "hoaparse/parsedecl.hh"
#include "misc/escape.hh"
#define YY_USER_ACTION yylloc->columns(yyleng);
#define YY_NEVER_INTERACTIVE 1
typedef hoayy::parser::token token;
static unsigned comment_level = 0;
static unsigned parent_level = 0;
static int orig_cond = 0;
static bool missing_parent = false;
%}
......@@ -38,7 +42,8 @@ eol \n+|\r+
eol2 (\n\r)+|(\r\n)+
identifier [[:alpha:]_][[:alnum:]_-]*
%x in_COMMENT in_STRING
%x in_COMMENT in_STRING in_NEVER_PAR
%s in_HOA in_NEVER
%%
......@@ -52,38 +57,48 @@ identifier [[:alpha:]_][[:alnum:]_-]*
{eol} yylloc->lines(yyleng); yylloc->step();
{eol2} yylloc->lines(yyleng / 2); yylloc->step();
[ \t\v\f]+ yylloc->step();
"/""*"+ BEGIN(in_COMMENT); comment_level = 1;
"\"" BEGIN(in_STRING);
"HOA:" return token::HOA;
"States:" return token::STATES;
"Start:" return token::START;
"AP:" return token::AP;
"Alias:" return token::ALIAS;
"Acceptance:" return token::ACCEPTANCE;
"acc-name:" return token::ACCNAME;
"tool:" return token::TOOL;
"name:" return token::NAME;
"properties:" return token::PROPERTIES;
"--BODY--" return token::BODY;
"--ABORT--" throw spot::hoa_abort{*yylloc};
"--END--" return token::END;
"State:" return token::STATE;
[tf{}()\[\]&|!] return *yytext;
{identifier} {
"/""*"+ {
orig_cond = YY_START;
BEGIN(in_COMMENT);
comment_level = 1;
}
"\"" {
orig_cond = YY_START;
BEGIN(in_STRING);
comment_level = 1;
}
"HOA:" BEGIN(in_HOA); return token::HOA;
<INITIAL,in_HOA>"--ABORT--" BEGIN(INITIAL); throw spot::hoa_abort{*yylloc};
"never" BEGIN(in_NEVER); return token::NEVER;
<in_HOA>{
"States:" return token::STATES;
"Start:" return token::START;
"AP:" return token::AP;
"Alias:" return token::ALIAS;
"Acceptance:" return token::ACCEPTANCE;
"acc-name:" return token::ACCNAME;
"tool:" return token::TOOL;
"name:" return token::NAME;
"properties:" return token::PROPERTIES;
"--BODY--" return token::BODY;
"--END--" BEGIN(INITIAL); return token::END;
"State:" return token::STATE;
[tf{}()\[\]&|!] return *yytext;
{identifier} {
yylval->str = new std::string(yytext, yyleng);
return token::IDENTIFIER;
}
{identifier}":" {
{identifier}":" {
yylval->str = new std::string(yytext, yyleng - 1);
return token::HEADERNAME;
}
"@"[[:alnum:]_-]+ {
"@"[[:alnum:]_-]+ {
yylval->str = new std::string(yytext + 1, yyleng - 1);
return token::ANAME;
}
[0-9]+ {
[0-9]+ {
errno = 0;
unsigned long n = strtoul(yytext, 0, 10);
yylval->num = n;
......@@ -96,6 +111,38 @@ identifier [[:alpha:]_][[:alnum:]_-]*
}
return token::INT;
}
}
<in_NEVER>{
"skip" return token::SKIP;
"if" return token::IF;
"fi" return token::FI;
"do" return token::DO;
"od" return token::OD;
"->" return token::ARROW;
"goto" return token::GOTO;
"false"|"0" return token::FALSE;
"atomic" return token::ATOMIC;
"assert" return token::ASSERT;
("!"[ \t]*)?"(" {
parent_level = 1;
BEGIN(in_NEVER_PAR);
yylval->str = new std::string(yytext, yyleng);
}
"true"|"1" {
yylval->str = new std::string(yytext, yyleng);
return token::FORMULA;
}
[a-zA-Z][a-zA-Z0-9_]* {
yylval->str = new std::string(yytext, yyleng);
return token::IDENTIFIER;
}
}
<in_COMMENT>{
"/""*"+ ++comment_level;
......@@ -103,7 +150,7 @@ identifier [[:alpha:]_][[:alnum:]_-]*
"/"[^*\n]* continue;
"*"+[^*/\n]* continue;
"\n"+ yylloc->end.column = 1; yylloc->lines(yyleng);
"*"+"/" if (--comment_level == 0) BEGIN(INITIAL);
"*"+"/" if (--comment_level == 0) BEGIN(orig_cond);
<<EOF>> {
error_list.push_back(
spot::hoa_parse_error(*yylloc,
......@@ -114,7 +161,7 @@ identifier [[:alpha:]_][[:alnum:]_-]*
<in_STRING>{
\" {
BEGIN(INITIAL);
BEGIN(orig_cond);
yylval->str = new std::string(s);
return token::STRING;
}
......@@ -128,6 +175,35 @@ identifier [[:alpha:]_][[:alnum:]_-]*
}
}
<in_NEVER_PAR>{
"(