From 91e51c4c3f1d111a08b07599533bc6324542a511 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 3 Feb 2011 22:33:47 +0100 Subject: [PATCH] Read guard of the form !(x) in neverclaims. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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. --- ChangeLog | 11 +++++++++++ src/neverparse/neverclaimscan.ll | 4 ++-- src/tgbatest/neverclaimread.test | 2 ++ 3 files changed, 15 insertions(+), 2 deletions(-) diff --git a/ChangeLog b/ChangeLog index 2ce235a6d..087bbeba9 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,14 @@ +2011-02-03 Alexandre Duret-Lutz + + 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 Recognize Goal's syntax for Boolean operators. diff --git a/src/neverparse/neverclaimscan.ll b/src/neverparse/neverclaimscan.ll index 64b880aad..d92e780bd 100644 --- a/src/neverparse/neverclaimscan.ll +++ b/src/neverparse/neverclaimscan.ll @@ -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). ** ** 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; "false"|"0" return token::FALSE; -"(".*")"|"true"|"1" { +"!"?"(".*")"|"true"|"1" { yylval->str = new std::string(yytext, yyleng); return token::FORMULA; } diff --git a/src/tgbatest/neverclaimread.test b/src/tgbatest/neverclaimread.test index 3aac302be..1fbc0182e 100755 --- a/src/tgbatest/neverclaimread.test +++ b/src/tgbatest/neverclaimread.test @@ -35,6 +35,7 @@ T1: if :: (p1 && (! p0)) -> goto accept_all :: (p1) -> goto T1 +:: !(p1) -> goto T2_init fi; accept_all: skip @@ -53,6 +54,7 @@ digraph G { 2 [label="T1"] 2 -> 3 [label="p1 & !p0\n"] 2 -> 2 [label="p1\n"] + 2 -> 1 [label="!p1\n"] 3 [label="accept_all"] 3 -> 3 [label="1\n{Acc[1]}"] }