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

Read guard of the form !(x) in neverclaims.

Browse source 
So far all neverclaims encountered would use (!(x)), but the
files from the Büchi store do not.

* src/neverparse/neverclaimscan.ll: Accept ! in front of guard,
so that we can read Promela files from Goal's Büchi store.
* src/tgbatest/neverclaimread.test: Test it.
This commit is contained in:
Alexandre Duret-Lutz 2011-02-03 22:33:47 +01:00
parent 3278844c2a
commit 91e51c4c3f
3 changed files with 15 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

11
ChangeLog
View file

@ -1,3 +1,14 @@
2011-02-03 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Read guard of the form !(x) in neverclaims.
So far all neverclaims encountered would use (!(x)), but the
files from the Büchi store do not.
* src/neverparse/neverclaimscan.ll: Accept ! in front of guard,
so that we can read Promela files from Goal's Büchi store.
* src/tgbatest/neverclaimread.test: Test it.
2011-02-03 Alexandre Duret-Lutz <adl@lrde.epita.fr> 2011-02-03 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Recognize Goal's syntax for Boolean operators. Recognize Goal's syntax for Boolean operators.

4
src/neverparse/neverclaimscan.ll
View file

@ -1,4 +1,4 @@
/* Copyright (C) 2010 Laboratoire de Recherche et Développement de /* Copyright (C) 2010, 2011 Laboratoire de Recherche et Développement de
** l'Epita (LRDE). ** l'Epita (LRDE).
** **
** This file is part of Spot, a model checking library. ** This file is part of Spot, a model checking library.
@ -56,7 +56,7 @@ eol \n|\r|\n\r|\r\n
"goto" return token::GOTO; "goto" return token::GOTO;
"false"|"0" return token::FALSE; "false"|"0" return token::FALSE;
"(".*")"|"true"|"1" { "!"?"(".*")"|"true"|"1" {
yylval->str = new std::string(yytext, yyleng); yylval->str = new std::string(yytext, yyleng);
return token::FORMULA; return token::FORMULA;
} }

2
src/tgbatest/neverclaimread.test
View file

@ -35,6 +35,7 @@ T1:
if if
:: (p1 && (! p0)) -> goto accept_all :: (p1 && (! p0)) -> goto accept_all
:: (p1) -> goto T1 :: (p1) -> goto T1
:: !(p1) -> goto T2_init
fi; fi;
accept_all: accept_all:
skip skip
@ -53,6 +54,7 @@ digraph G {
2 [label="T1"] 2 [label="T1"]
2 -> 3 [label="p1 & !p0\n"] 2 -> 3 [label="p1 & !p0\n"]
2 -> 2 [label="p1\n"] 2 -> 2 [label="p1\n"]
2 -> 1 [label="!p1\n"]
3 [label="accept_all"] 3 [label="accept_all"]
3 -> 3 [label="1\n{Acc[1]}"] 3 -> 3 [label="1\n{Acc[1]}"]
} }