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 [*].
This commit is contained in:
Alexandre Duret-Lutz
parent
4e7233d9fa
commit
8b8633de8c
10 changed files with 41 additions and 42 deletions
|
|
@ -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;
|
||||
|
|
|
|||
|
|
@ -87,7 +87,7 @@ namespace spot
|
|||
case False:
|
||||
return "0";
|
||||
case EmptyWord:
|
||||
return "#e";
|
||||
return "[*0]";
|
||||
}
|
||||
// Unreachable code.
|
||||
assert(0);
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
{
|
||||
|
|
|
|||
|
|
@ -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...)
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
|
|
|||
|
|
@ -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
|
||||
///
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
|
|
|||
|
|
@ -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])'
|
||||
|
|
|
|||
|
|
@ -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'
|
||||
|
|
|
|||
|
|
@ -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.
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue