Support reading the new style of neverclaim output by Spin 6.24+.
* src/neverparse/neverclaimparse.yy, src/neverparse/neverclaimscan.ll: Allow transitions between do..od, recognize atomic and assert. * src/neverparse/parsedecl.hh: Pass the error_list to the lexer. * src/tgbatest/neverclaimread.test: Add a test case.
This commit is contained in:
Alexandre Duret-Lutz
parent
ff102d3d94
commit
327bd2d621
4 changed files with 162 additions and 28 deletions
|
|
@ -1,5 +1,5 @@
|
|||
/* -*- coding: utf-8 -*-
|
||||
** Copyright (C) 2010, 2011, 2012 Laboratoire de Recherche et
|
||||
** Copyright (C) 2010, 2011, 2012, 2013 Laboratoire de Recherche et
|
||||
** Développement de l'Epita (LRDE).
|
||||
**
|
||||
** This file is part of Spot, a model checking library.
|
||||
|
|
@ -25,6 +25,7 @@
|
|||
%name-prefix "neverclaimyy"
|
||||
%debug
|
||||
%error-verbose
|
||||
%lex-param { spot::neverclaim_parse_error_list& error_list }
|
||||
|
||||
%code requires
|
||||
{
|
||||
|
|
@ -59,20 +60,26 @@
|
|||
before parsedecl.hh uses it. */
|
||||
#include "parsedecl.hh"
|
||||
using namespace spot::ltl;
|
||||
static bool accept_all_needed = false;
|
||||
static bool accept_all_seen = false;
|
||||
}
|
||||
|
||||
%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"
|
||||
%token <str> IDENT "identifier"
|
||||
%type <str> formula opt_dest
|
||||
%type <p> transition
|
||||
%type <list> transitions
|
||||
%type <p> transition src_dest
|
||||
%type <list> transitions transition_block
|
||||
%type <str> ident_list
|
||||
|
||||
|
||||
|
|
@ -112,7 +119,7 @@ ident_list:
|
|||
| ident_list IDENT ':'
|
||||
{
|
||||
result->add_state_alias(*$2, *$1);
|
||||
// Keep any identifier that start with accept.
|
||||
// Keep any identifier that starts with accept.
|
||||
if (strncmp("accept", $1->c_str(), 6))
|
||||
{
|
||||
delete $1;
|
||||
|
|
@ -125,9 +132,23 @@ ident_list:
|
|||
}
|
||||
}
|
||||
|
||||
|
||||
transition_block:
|
||||
"if" transitions "fi"
|
||||
{
|
||||
$$ = $2;
|
||||
}
|
||||
| "do" transitions "od"
|
||||
{
|
||||
$$ = $2;
|
||||
}
|
||||
|
||||
state:
|
||||
ident_list "skip"
|
||||
{
|
||||
if (*$1 == "accept_all")
|
||||
accept_all_seen = true;
|
||||
|
||||
spot::state_explicit_string::transition* t = result->create_transition(*$1, *$1);
|
||||
bool acc = !strncmp("accept", $1->c_str(), 6);
|
||||
if (acc)
|
||||
|
|
@ -137,11 +158,11 @@ state:
|
|||
}
|
||||
| ident_list { delete $1; }
|
||||
| ident_list "false" { delete $1; }
|
||||
| ident_list "if" transitions "fi"
|
||||
| ident_list transition_block
|
||||
{
|
||||
std::list<pair>::iterator it;
|
||||
bool acc = !strncmp("accept", $1->c_str(), 6);
|
||||
for (it = $3->begin(); it != $3->end(); ++it)
|
||||
for (it = $2->begin(); it != $2->end(); ++it)
|
||||
{
|
||||
spot::state_explicit_string::transition* t =
|
||||
result->create_transition(*$1, *it->second);
|
||||
|
|
@ -153,10 +174,10 @@ state:
|
|||
}
|
||||
// Free the list
|
||||
delete $1;
|
||||
for (std::list<pair>::iterator it = $3->begin();
|
||||
it != $3->end(); ++it)
|
||||
for (std::list<pair>::iterator it = $2->begin();
|
||||
it != $2->end(); ++it)
|
||||
delete it->second;
|
||||
delete $3;
|
||||
delete $2;
|
||||
}
|
||||
|
||||
|
||||
|
|
@ -184,41 +205,57 @@ opt_dest:
|
|||
{
|
||||
$$ = $3;
|
||||
}
|
||||
| "->" "assert" FORMULA
|
||||
{
|
||||
delete $3;
|
||||
$$ = new std::string("accept_all");
|
||||
accept_all_needed = true;
|
||||
}
|
||||
|
||||
transition:
|
||||
':' ':' formula opt_dest
|
||||
src_dest: formula opt_dest
|
||||
{
|
||||
// If there is no destination, do ignore the transition.
|
||||
// This happens for instance with
|
||||
// if
|
||||
// :: false
|
||||
// fi
|
||||
if (!$4)
|
||||
if (!$2)
|
||||
{
|
||||
delete $3;
|
||||
delete $1;
|
||||
$$ = 0;
|
||||
}
|
||||
else
|
||||
{
|
||||
spot::ltl::parse_error_list pel;
|
||||
const spot::ltl::formula* f =
|
||||
spot::ltl::parse_boolean(*$3, pel, parse_environment,
|
||||
spot::ltl::parse_boolean(*$1, pel, parse_environment,
|
||||
debug_level(), true);
|
||||
delete $3;
|
||||
delete $1;
|
||||
for(spot::ltl::parse_error_list::const_iterator i = pel.begin();
|
||||
i != pel.end(); ++i)
|
||||
{
|
||||
// Adjust the diagnostic to the current position.
|
||||
location here = @3;
|
||||
location here = @1;
|
||||
here.end.line = here.begin.line + i->first.end.line - 1;
|
||||
here.end.column = here.begin.column + i->first.end.column -1;
|
||||
here.begin.line += i->first.begin.line - 1;
|
||||
here.begin.column += i->first.begin.column - 1;
|
||||
error(here, i->second);
|
||||
}
|
||||
$$ = new pair(f, $4);
|
||||
$$ = new pair(f, $2);
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
transition:
|
||||
':' ':' "atomic" '{' src_dest '}'
|
||||
{
|
||||
$$ = $5;
|
||||
}
|
||||
| ':' ':' src_dest
|
||||
{
|
||||
$$ = $3;
|
||||
}
|
||||
%%
|
||||
|
||||
void
|
||||
|
|
@ -250,6 +287,17 @@ namespace spot
|
|||
parser.set_debug_level(debug);
|
||||
parser.parse();
|
||||
neverclaimyyclose();
|
||||
|
||||
if (accept_all_needed && !accept_all_seen)
|
||||
{
|
||||
spot::state_explicit_string::transition* t =
|
||||
result->create_transition("accept_all", "accept_all");
|
||||
result->add_acceptance_condition
|
||||
(t, spot::ltl::constant::true_instance());
|
||||
}
|
||||
accept_all_needed = false;
|
||||
accept_all_seen = false;
|
||||
|
||||
return result;
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
/* Copyright (C) 2010, 2011 Laboratoire de Recherche et Développement de
|
||||
** l'Epita (LRDE).
|
||||
/* Copyright (C) 2010, 2011, 2013 Laboratoire de Recherche et
|
||||
** Développement de l'Epita (LRDE).
|
||||
**
|
||||
** This file is part of Spot, a model checking library.
|
||||
**
|
||||
|
|
@ -23,6 +23,7 @@
|
|||
%{
|
||||
#include <string>
|
||||
#include "neverparse/parsedecl.hh"
|
||||
#include "misc/escape.hh"
|
||||
|
||||
#define YY_USER_ACTION \
|
||||
yylloc->columns(yyleng);
|
||||
|
|
@ -30,9 +31,13 @@
|
|||
#define YY_NEVER_INTERACTIVE 1
|
||||
|
||||
typedef neverclaimyy::parser::token token;
|
||||
static int parent_level = 0;
|
||||
static bool missing_parent = false;
|
||||
|
||||
%}
|
||||
|
||||
%x in_par
|
||||
|
||||
eol \n|\r|\n\r|\r\n
|
||||
|
||||
%%
|
||||
|
|
@ -50,11 +55,46 @@ eol \n|\r|\n\r|\r\n
|
|||
"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]*)?"(".*")"|"true"|"1" {
|
||||
("!"[ \t]*)?"(" {
|
||||
parent_level = 1;
|
||||
BEGIN(in_par);
|
||||
yylval->str = new std::string(yytext,yyleng);
|
||||
}
|
||||
|
||||
<in_par>{
|
||||
"(" {
|
||||
++parent_level;
|
||||
yylval->str->append(yytext, yyleng);
|
||||
}
|
||||
")" {
|
||||
yylval->str->append(yytext, yyleng);
|
||||
if (!--parent_level)
|
||||
{
|
||||
BEGIN(0);
|
||||
spot::trim(*yylval->str);
|
||||
return token::FORMULA;
|
||||
}
|
||||
}
|
||||
[^()]+ yylval->str->append(yytext, yyleng);
|
||||
<<EOF>> {
|
||||
unput(')');
|
||||
if (!missing_parent)
|
||||
error_list.push_back(
|
||||
spot::neverclaim_parse_error(*yylloc,
|
||||
"missing closing parenthese"));
|
||||
missing_parent = true;
|
||||
}
|
||||
}
|
||||
|
||||
"true"|"1" {
|
||||
yylval->str = new std::string(yytext, yyleng);
|
||||
return token::FORMULA;
|
||||
}
|
||||
|
|
@ -95,5 +135,6 @@ namespace spot
|
|||
neverclaimyyclose()
|
||||
{
|
||||
fclose(yyin);
|
||||
missing_parent = false;
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
// Copyright (C) 2010 Laboratoire de Recherche et Développement de
|
||||
// l'EPITA.
|
||||
// Copyright (C) 2010, 2013 Laboratoire de Recherche et Développement
|
||||
// de l'EPITA.
|
||||
//
|
||||
// This file is part of Spot, a model checking library.
|
||||
//
|
||||
|
|
@ -24,8 +24,9 @@
|
|||
#include "location.hh"
|
||||
|
||||
# define YY_DECL \
|
||||
int neverclaimyylex (neverclaimyy::parser::semantic_type *yylval, \
|
||||
neverclaimyy::location *yylloc)
|
||||
int neverclaimyylex(neverclaimyy::parser::semantic_type *yylval, \
|
||||
neverclaimyy::location *yylloc, \
|
||||
spot::neverclaim_parse_error_list& error_list)
|
||||
YY_DECL;
|
||||
|
||||
namespace spot
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
#!/bin/sh
|
||||
# -*- coding: utf-8 -*-
|
||||
# Copyright (C) 2010, 2011, 2012 Laboratoire de Recherche et
|
||||
# Copyright (C) 2010, 2011, 2012, 2013 Laboratoire de Recherche et
|
||||
# Développement de l'Epita (LRDE).
|
||||
#
|
||||
# This file is part of Spot, a model checking library.
|
||||
|
|
@ -68,6 +68,51 @@ diff stdout expected
|
|||
rm input stdout expected
|
||||
|
||||
|
||||
# Same test, but with the newer syntax output since Spin 6.24
|
||||
cat >input <<EOF
|
||||
never {
|
||||
T2_init:
|
||||
do
|
||||
:: (1) -> goto T2_init
|
||||
:: (p1 && p0) -> goto T1
|
||||
od;
|
||||
T1:
|
||||
do
|
||||
:: atomic { (p1 && (! p0)) -> assert(!(p1 && (! p0))) }
|
||||
:: !(p1) -> goto T1
|
||||
:: ! (p1) -> goto T2_init
|
||||
od;
|
||||
}
|
||||
EOF
|
||||
|
||||
run 0 ../ltl2tgba -XN input > stdout
|
||||
|
||||
cat >expected <<EOF
|
||||
digraph G {
|
||||
0 [label="", style=invis, height=0]
|
||||
0 -> 1
|
||||
1 [label="T2_init"]
|
||||
1 -> 1 [label="1\n"]
|
||||
1 -> 2 [label="p0 & p1\n"]
|
||||
2 [label="T1"]
|
||||
2 -> 3 [label="p1 & !p0\n"]
|
||||
2 -> 2 [label="!p1\n"]
|
||||
2 -> 1 [label="!p1\n"]
|
||||
3 [label="accept_all", peripheries=2]
|
||||
3 -> 3 [label="1\n{Acc[1]}"]
|
||||
}
|
||||
EOF
|
||||
|
||||
# Sort out some possible inversions in the output.
|
||||
# (The order is not guaranteed by SPOT.)
|
||||
sed -e 's/!p0 & p1/p1 \& !p0/g' -e 's/p1 & p0/p0 \& p1/g' stdout \
|
||||
> tmp_ && mv tmp_ stdout
|
||||
diff stdout expected
|
||||
|
||||
rm input stdout expected
|
||||
|
||||
|
||||
|
||||
# Test broken guards in input
|
||||
cat >input <<EOF
|
||||
never {
|
||||
|
|
@ -93,9 +138,8 @@ EOF
|
|||
# that "p1 && " is an atomic property.
|
||||
|
||||
run 2 ../ltl2tgba -XN input > stdout 2>stderr
|
||||
cat >expected <<EOF
|
||||
input:9.16: syntax error, unexpected closing parenthesis
|
||||
input:9.16: ignoring trailing garbage
|
||||
cat >expected <<\EOF
|
||||
input:9.16: syntax error, unexpected $undefined, expecting fi or ':'
|
||||
EOF
|
||||
grep input: stderr >> stderrfilt
|
||||
diff stderrfilt expected
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue