From 8b8633de8cb12932ba68552b618244587bd45d06 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 9 Mar 2010 16:08:38 +0100 Subject: [PATCH] Use [*0] instead of #e, and support [*] in addition to *. * src/ltlparse/ltlscan.ll: Recognize [*] as *, and use [*0] instead of #e for the empty word. * src/ltlast/binop.cc, src/ltlast/constant.cc, src/ltlast/multop.cc, src/ltlast/multop.hh, src/ltlast/unop.cc, src/ltlast/unop.hh, src/ltltest/consterm.test, src/ltltest/equals.test: Adjust all occurrences of #e to [*0]. * src/tgbatest/ltl2tgba.test: Also use [*]. --- src/ltlast/binop.cc | 4 ++-- src/ltlast/constant.cc | 2 +- src/ltlast/multop.cc | 6 +++--- src/ltlast/multop.hh | 2 +- src/ltlast/unop.cc | 8 ++++---- src/ltlast/unop.hh | 12 ++++++------ src/ltlparse/ltlscan.ll | 6 +++--- src/ltltest/consterm.test | 18 +++++++++--------- src/ltltest/equals.test | 20 ++++++++++---------- src/tgbatest/ltl2tgba.test | 5 ++--- 10 files changed, 41 insertions(+), 42 deletions(-) diff --git a/src/ltlast/binop.cc b/src/ltlast/binop.cc index a6eeddae0..edb378b63 100644 --- a/src/ltlast/binop.cc +++ b/src/ltlast/binop.cc @@ -261,7 +261,7 @@ namespace spot case EConcatMarked: // - 0 <>-> Exp = 0 // - 1 <>-> Exp = Exp - // - #e <>-> Exp = 0 + // - [*0] <>-> Exp = 0 // - Exp <>-> 0 = 0 if (first == constant::true_instance()) return second; @@ -280,7 +280,7 @@ namespace spot case UConcat: // - 0 []-> Exp = 1 // - 1 []-> Exp = Exp - // - #e []-> Exp = 1 + // - [*0] []-> Exp = 1 // - Exp []-> 1 = 1 if (first == constant::true_instance()) return second; diff --git a/src/ltlast/constant.cc b/src/ltlast/constant.cc index c3d13ab53..96025c3bf 100644 --- a/src/ltlast/constant.cc +++ b/src/ltlast/constant.cc @@ -87,7 +87,7 @@ namespace spot case False: return "0"; case EmptyWord: - return "#e"; + return "[*0]"; } // Unreachable code. assert(0); diff --git a/src/ltlast/multop.cc b/src/ltlast/multop.cc index 7025e04ff..0f6093725 100644 --- a/src/ltlast/multop.cc +++ b/src/ltlast/multop.cc @@ -239,9 +239,9 @@ namespace spot ++i; } } - // We have a* & #e & 0 = 0 // already checked above - // but a* & #e & c* = #e - // So if #e has been seen, check if all term recognize the + // We have a* & [*0] & 0 = 0 // already checked above + // but a* & [*0] & c* = [*0] + // So if [*0] has been seen, check if all term recognize the // empty word. if (weak_abs_seen) { diff --git a/src/ltlast/multop.hh b/src/ltlast/multop.hh index db74e8e3a..e9fa0f88b 100644 --- a/src/ltlast/multop.hh +++ b/src/ltlast/multop.hh @@ -80,7 +80,7 @@ namespace spot /// are also taken care of. The following rewriting are performed /// (the left patterns are rewritten as shown on the right): /// - /// - Concat(Exps1...,#e,Exps2...) = Concat(Exps1...,Exps2...) + /// - Concat(Exps1...,[*0],Exps2...) = Concat(Exps1...,Exps2...) /// - Concat(Exps1...,0,Exps2...) = 0 /// - Concat(Exp) = Exp /// - And(Exps1...,1,Exps2...) = And(Exps1...,Exps2...) diff --git a/src/ltlast/unop.cc b/src/ltlast/unop.cc index 5240cb2b9..bc67c2ea9 100644 --- a/src/ltlast/unop.cc +++ b/src/ltlast/unop.cc @@ -120,8 +120,8 @@ namespace spot // Some trivial simplifications. switch (op) { - // We have (0*) == (#e) - // (#e*) == (#e) + // We have (0*) == ([*0]) + // ([*0]*) == ([*0]) case Star: if (child == constant::false_instance() || child == constant::empty_word_instance()) @@ -145,7 +145,7 @@ namespace spot if (child == constant::false_instance() || child == constant::true_instance()) return child; - // F(#e) = G(#e) = 1 + // F([*0]) = G([*0]) = 1 if (child == constant::empty_word_instance()) return constant::true_instance(); } @@ -192,7 +192,7 @@ namespace spot if (child == constant::true_instance() || child == constant::false_instance()) return child; - // X(#e) = 1 + // X([*0]) = 1 if (child == constant::empty_word_instance()) return constant::true_instance(); break; diff --git a/src/ltlast/unop.hh b/src/ltlast/unop.hh index 2ac1ad471..37c40ea6b 100644 --- a/src/ltlast/unop.hh +++ b/src/ltlast/unop.hh @@ -57,8 +57,8 @@ namespace spot /// The following trivial simplifications are performed /// automatically (the left expression is rewritten as the right /// expression): - /// - 0* = #e - /// - #e* = #e + /// - 0* = [*0] + /// - [*0]* = [*0] /// - Exp** = Exp* /// - FF(Exp) = F(Exp) /// - GG(Exp) = G(Exp) @@ -66,17 +66,17 @@ namespace spot /// - G(0) = 0 /// - F(1) = 1 /// - G(1) = 1 - /// - F(#e) = 1 - /// - G(#e) = 1 + /// - F([*0]) = 1 + /// - G([*0]) = 1 /// - !1 = 0 /// - !0 = 1 /// - !!Exp = Exp /// - !Closure(Exp) = NegClosure(Exp) /// - !NegClosure(Exp) = Closure(Exp) - /// - Closure(#e) = 1 + /// - Closure([*0]) = 1 /// - Closure(1) = 1 /// - Closure(0) = 0 - /// - NegClosure(#e) = 0 + /// - NegClosure([*0]) = 0 /// - NegClosure(1) = 0 /// - NegClosure(0) = 1 /// diff --git a/src/ltlparse/ltlscan.ll b/src/ltlparse/ltlscan.ll index 01f6a2ed9..0e90862bc 100644 --- a/src/ltlparse/ltlscan.ll +++ b/src/ltlparse/ltlscan.ll @@ -1,7 +1,7 @@ /* Copyright (C) 2010, 2011, Laboratoire de Recherche et Développement de ** l'Epita (LRDE). ** Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), -** département Syst�mes R�partis Coop�ratifs (SRC), Université Pierre +** département Systèmes Répartis Coopératifs (SRC), Université Pierre ** et Marie Curie. ** ** This file is part of Spot, a model checking library. @@ -85,7 +85,7 @@ flex_set_buffer(const char* buf, int start_tok) /* ~ comes from Goal, ! from everybody else */ "!"|"~" BEGIN(0); return token::OP_NOT; -"#e" BEGIN(0); return token::CONST_EMPTYWORD; +"[*0]" BEGIN(0); return token::CONST_EMPTYWORD; /* & and | come from Spin. && and || from LTL2BA. /\, \/, and xor are from LBTT. @@ -95,7 +95,7 @@ flex_set_buffer(const char* buf, int start_tok) "^"|"xor" BEGIN(0); return token::OP_XOR; "=>"|"->"|"-->" BEGIN(0); return token::OP_IMPLIES; "<=>"|"<->"|"<-->" BEGIN(0); return token::OP_EQUIV; -"*" BEGIN(0); return token::OP_STAR; +"*"|"[*]" BEGIN(0); return token::OP_STAR; ";" BEGIN(0); return token::OP_CONCAT; ":" BEGIN(0); return token::OP_FUSION; "[]->" BEGIN(0); return token::OP_UCONCAT; diff --git a/src/ltltest/consterm.test b/src/ltltest/consterm.test index cb2e5fcb2..c01f92f4e 100755 --- a/src/ltltest/consterm.test +++ b/src/ltltest/consterm.test @@ -29,15 +29,15 @@ set -e run 0 ../consterm 'a' run 0 ../consterm '1' run 0 ../consterm '0' -run 1 ../consterm '#e' +run 1 ../consterm '[*0]' run 1 ../consterm 'a*' run 1 ../consterm '0*' run 0 ../consterm '((a ; b) + c)' -run 1 ../consterm '((a ; b) + #e)' -run 0 ../consterm '((a ; b) + #e) & e' -run 1 ../consterm '((a ; b) + #e) & #e' -run 1 ../consterm '((a ; b) + #e) & (a* + b)' -run 1 ../consterm '{{a ; b} + {#e}} & {a* + b}' # test braces -run 1 ../consterm '(a + #e);(b + #e);(c + #e)' -run 0 ../consterm '(a + #e);(b + e);(c + #e)' -run 1 ../consterm '(a + #e);(b + e)*;(c + #e)' +run 1 ../consterm '((a ; b) + [*0])' +run 0 ../consterm '((a ; b) + [*0]) & e' +run 1 ../consterm '((a ; b) + [*0]) & [*0]' +run 1 ../consterm '((a ; b) + [*0]) & (a* + b)' +run 1 ../consterm '{{a ; b} + {[*0]}} & {a* + b}' # test braces +run 1 ../consterm '(a + [*0]);(b + [*0]);(c + [*0])' +run 0 ../consterm '(a + [*0]);(b + e);(c + [*0])' +run 1 ../consterm '(a + [*0]);(b + e)*;(c + [*0])' diff --git a/src/ltltest/equals.test b/src/ltltest/equals.test index ea6983db2..53d6dcd31 100755 --- a/src/ltltest/equals.test +++ b/src/ltltest/equals.test @@ -70,8 +70,8 @@ run 0 ../equals 'a & b ^ c | d' 'd | c ^ b & a' run 0 ../equals 'FFG__GFF' 'F(F(G("__GFF")))' # Trivial simplifications -run 0 ../equals '{0*}<>->a' '{#e}<>->a' -run 0 ../equals '{#e*}<>->a' '{#e}<>->a' +run 0 ../equals '{0*}<>->a' '{[*0]}<>->a' +run 0 ../equals '{[*0]*}<>->a' '{[*0]}<>->a' run 0 ../equals '{Exp**}<>->a' '{Exp*}<>->a' run 0 ../equals 'FF(Exp)' 'F(Exp)' run 0 ../equals 'GG(Exp)' 'G(Exp)' @@ -79,8 +79,8 @@ run 0 ../equals 'F(0)' '0' run 0 ../equals 'G(0)' '0' run 0 ../equals 'F(1)' '1' run 0 ../equals 'G(1)' '1' -run 0 ../equals 'F({#e}<>->1)' 'F({#e}<>->1)' -run 0 ../equals 'G({#e}<>->1)' 'G({#e}<>->1)' +run 0 ../equals 'F({[*0]}<>->1)' 'F({[*0]}<>->1)' +run 0 ../equals 'G({[*0]}<>->1)' 'G({[*0]}<>->1)' run 0 ../equals 'F({1}<>->1)' '1' run 0 ../equals 'G({1}<>->1)' '1' run 0 ../equals '!1' '0' @@ -107,15 +107,15 @@ run 0 ../equals GGx Gx run 0 ../equals GGGGGx Gx run 0 ../equals '!!x' x run 0 ../equals '!!!!!x' '!x' -run 0 ../equals '{#e;x}<>->1' '{x}<>->1' -run 0 ../equals '{x;#e}<>->1' '{x}<>-> 1' -run 0 ../equals '{#e;x;#e;#e}<>->1' '{x}<>->1' -run 0 ../equals '{#e;x;#e;x;#e}<>->1' '{x;x}<>->1' -run 0 ../equals '{x;x;x;#e;x;x}<>->1' '{x;x;x;x;x}<>->1' +run 0 ../equals '{[*0];x}<>->1' '{x}<>->1' +run 0 ../equals '{x;[*0]}<>->1' '{x}<>-> 1' +run 0 ../equals '{[*0];x;[*0];[*0]}<>->1' '{x}<>->1' +run 0 ../equals '{[*0];x;[*0];x;[*0]}<>->1' '{x;x}<>->1' +run 0 ../equals '{x;x;x;[*0];x;x}<>->1' '{x;x;x;x;x}<>->1' run 0 ../equals '{x;0;x;x;x}<>->1' '0' run 0 ../equals '{x;0;x;x;x}[]->1' '1' run 0 ../equals '{0*;1}<>->x' 'x' -run 0 ../equals '{#e*;1}<>->x' 'x' +run 0 ../equals '{[*0]*;1}<>->x' 'x' run 0 ../equals '{x;x}<>->FF(0)' '0' run 0 ../equals '{x;x}<>->GX(1)' '{x;x}<>->1' run 0 ../equals '{x;x}[]->GX(1)' '1' diff --git a/src/tgbatest/ltl2tgba.test b/src/tgbatest/ltl2tgba.test index 06fab7e81..a481a4773 100755 --- a/src/tgbatest/ltl2tgba.test +++ b/src/tgbatest/ltl2tgba.test @@ -67,7 +67,7 @@ check_psl '{(g;y;r)*}<>->x' check_psl 'G({(g;y;r)*}<>->x)' check_psl 'G({(a;b)*}<>->x)&G({(c;d)*}<>->y)' check_psl 'G({{a;b}*}[]->x)&G({{c;d}*}[]->y)' # try sub-braces -check_psl '{(#e + a):c*:(#e + b)}<>->d' +check_psl '{([*0] + a):c*:([*0] + b)}<>->d' check_psl '{a;e;f:(g*);h}<>->d' check_psl '{(a:b)* & (c*:d)}<>->e' check_psl '{(a:b)*}' @@ -76,10 +76,9 @@ check_psl '{a;b}' check_psl '{(a;b)*}' check_psl 'G{(a;b)*}' check_psl '{a*}[]->{b*}' - # Example from "Beyond Hardware Verification" by Glazberg, Moulin, Orni, # Ruah, Zarpas (2007). -check_psl '{1*;req;ack;1}[]->{start;busy*;done}' +check_psl '{1[*];req;ack;1}[]->{start;busy[*];done}' # Make sure 'a U (b U c)' has 3 states and 6 transitions, # before and after degeneralization.