diff --git a/src/ltlast/bunop.cc b/src/ltlast/bunop.cc index b2f146704..66a3ed592 100644 --- a/src/ltlast/bunop.cc +++ b/src/ltlast/bunop.cc @@ -119,6 +119,14 @@ namespace spot bunop::format() const { std::ostringstream out; + + // Syntactic sugaring + if (min_ == 1 && max_ == unbounded) + { + out << "[+]"; + return out.str(); + } + out << "[*"; if (min_ != 0 || max_ != unbounded) { diff --git a/src/ltlparse/ltlparse.yy b/src/ltlparse/ltlparse.yy index 56cf7c374..556f1e0a7 100644 --- a/src/ltlparse/ltlparse.yy +++ b/src/ltlparse/ltlparse.yy @@ -90,6 +90,7 @@ using namespace spot::ltl; %token OP_W "weak until operator" OP_M "strong release operator" %token OP_F "sometimes operator" OP_G "always operator" %token OP_X "next operator" OP_NOT "not operator" OP_STAR "star operator" +%token OP_PLUS "plus operator" %token OP_STAR_OPEN "opening bracket for star operator" %token OP_STAR_CLOSE "closing bracket for star operator" %token OP_STAR_NUM "number for star operator" @@ -123,7 +124,7 @@ using namespace spot::ltl; %nonassoc OP_X /* High priority regex operator. */ -%nonassoc OP_STAR OP_STAR_OPEN +%nonassoc OP_STAR OP_STAR_OPEN OP_PLUS /* Not has the most important priority after Wring's `=0' and `=1'. */ %nonassoc OP_NOT @@ -191,6 +192,8 @@ error_opt: | error starargs: OP_STAR { $$.min = 0U; $$.max = bunop::unbounded; } + | OP_PLUS + { $$.min = 1U; $$.max = bunop::unbounded; } | OP_STAR_OPEN OP_STAR_NUM OP_STAR_SEP OP_STAR_NUM OP_STAR_CLOSE { $$.min = $2; $$.max = $4; } | OP_STAR_OPEN OP_STAR_NUM OP_STAR_SEP OP_STAR_CLOSE @@ -200,7 +203,7 @@ starargs: OP_STAR | OP_STAR_OPEN OP_STAR_SEP_opt OP_STAR_CLOSE { $$.min = 0U; $$.max = bunop::unbounded; } | OP_STAR_OPEN OP_STAR_NUM OP_STAR_CLOSE - { $$.min = $2; $$.max = $2; } + { $$.min = $$.max = $2; } | OP_STAR_OPEN error OP_STAR_CLOSE { error_list.push_back(parse_error(@$, "treating this star block as [*]")); diff --git a/src/ltlparse/ltlscan.ll b/src/ltlparse/ltlscan.ll index 64d734973..9a1a315c9 100644 --- a/src/ltlparse/ltlscan.ll +++ b/src/ltlparse/ltlscan.ll @@ -95,6 +95,7 @@ flex_set_buffer(const char* buf, int start_tok) ";" BEGIN(0); return token::OP_CONCAT; ":" BEGIN(0); return token::OP_FUSION; "*"|"[*]" BEGIN(0); return token::OP_STAR; +"[+]" BEGIN(0); return token::OP_PLUS; "[*" BEGIN(star); return token::OP_STAR_OPEN; "]" BEGIN(0); return token::OP_STAR_CLOSE; [0-9]+ { diff --git a/src/ltltest/equals.test b/src/ltltest/equals.test index b91851bfc..a2cc0f48b 100755 --- a/src/ltltest/equals.test +++ b/src/ltltest/equals.test @@ -134,3 +134,8 @@ run 0 ../equals '{a[*..3][*2]}' '{a[*..6]}' run 0 ../equals '{a[*..3][*..2]}' '{a[*..6]}' run 0 ../equals '{a[*..3][*2..]}' '{a[*]}' run 0 ../equals '{a[*..3][*2..]}' '{a[*]}' +run 0 ../equals '{a[*1..]}' '{a[+]}' +run 0 ../equals '{a[+][*1..3]}' '{a[+]}' +run 0 ../equals '{a[*1..3][+]}' '{a[+]}' +run 0 ../equals '{[*2][+]}' '{[*2][+]}' +run 0 ../equals '{[+][*2]}' '{[*2..]}' diff --git a/src/ltltest/tostring.test b/src/ltltest/tostring.test index 9f0e9f39d..fa3e1c252 100755 --- a/src/ltltest/tostring.test +++ b/src/ltltest/tostring.test @@ -66,4 +66,6 @@ run 0 ../tostring '{a[*0..1]}' run 0 ../tostring '{a[*0..]}' run 0 ../tostring '{a[*..]}' run 0 ../tostring '{a[*1..]}' +run 0 ../tostring '{a[+]}' +run 0 ../tostring '{[+]}' run 0 ../tostring '{a[*2..3][*4..5]}' diff --git a/src/ltlvisit/tostring.cc b/src/ltlvisit/tostring.cc index af55339db..e22957770 100644 --- a/src/ltlvisit/tostring.cc +++ b/src/ltlvisit/tostring.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2008, 2010, 2011 Laboratoire de Recherche et Développement +// Copyright (C) 2008, 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 @@ -182,12 +182,12 @@ namespace spot void visit(const bunop* bo) { - // Abbreviate "1*" as "*". + // Abbreviate "1[*]" as "[*]". if (bo->child() != constant::true_instance()) { - // a* is OK, no need to print {a}*. - // However want braces for {!a}*, the only unary - // operator that can be nested with *. + // a[*] is OK, no need to print {a}[*]. + // However want braces for {!a}[*], the only unary + // operator that can be nested with [*]. bool need_parent = !!dynamic_cast(bo->child()); if (need_parent || full_parent_) @@ -197,11 +197,7 @@ namespace spot closep(); } - // Output "*" instead of "[*]". - if (bo->min() == 0 && bo->max() == bunop::unbounded) - os_ << "*"; - else - os_ << bo->format(); + os_ << bo->format(); } void diff --git a/src/tgbatest/ltl2tgba.test b/src/tgbatest/ltl2tgba.test index ffb33b80f..e040f9b19 100755 --- a/src/tgbatest/ltl2tgba.test +++ b/src/tgbatest/ltl2tgba.test @@ -83,6 +83,7 @@ check_psl '{((!c;b*) & d);e}' check_psl '{(a* & (c;b*) & d);e}' check_psl '{[*2];a[*2..4]}|->b' check_psl '{a[*2..5] && b[*..3]}|->c' +check_psl '{{[+];a;[+]} && {[+];b;[+]}}<>->c' # Example from "Beyond Hardware Verification" by Glazberg, Moulin, Orni, # Ruah, Zarpas (2007). check_psl '{[*];req;ack}|=>{start;busy[*];done}'