diff --git a/src/ltlparse/ltlparse.yy b/src/ltlparse/ltlparse.yy index 25afbe18c..24193cc1e 100644 --- a/src/ltlparse/ltlparse.yy +++ b/src/ltlparse/ltlparse.yy @@ -283,6 +283,8 @@ rationalexp: booleanatom { missing_right_binop($$, $1, @2, "fusion operator"); } | rationalexp OP_STAR { $$ = unop::instance(unop::Star, $1); } + | OP_STAR + { $$ = unop::instance(unop::Star, constant::true_instance()); } bracedrationalexp: BRACE_OPEN rationalexp BRACE_CLOSE { $$ = $2; } diff --git a/src/ltlvisit/tostring.cc b/src/ltlvisit/tostring.cc index cfe51f5c6..7c15b6928 100644 --- a/src/ltlvisit/tostring.cc +++ b/src/ltlvisit/tostring.cc @@ -226,6 +226,12 @@ namespace spot top_level_ = true; break; case unop::Star: + // Abbreviate "1*" as "*". + if (uo->child() == constant::true_instance()) + { + os_ << "*"; + return; + } // 1* is OK, no need to print {1}*. need_parent = false; // Do not output anything yet, star is a postfix operator. @@ -469,6 +475,12 @@ namespace spot in_ratexp_ = true; break; case unop::Star: + // Abbreviate "1*" as "*". + if (uo->child() == constant::true_instance()) + { + os_ << "*"; + return; + } // Do not output anything yet, star is a postfix operator. need_parent = false; break; diff --git a/src/tgbatest/ltl2tgba.test b/src/tgbatest/ltl2tgba.test index 52e872601..72a155fea 100755 --- a/src/tgbatest/ltl2tgba.test +++ b/src/tgbatest/ltl2tgba.test @@ -83,7 +83,7 @@ check_psl '{((!c;b*) & d);e}' check_psl '{(a* & (c;b*) & d);e}' # Example from "Beyond Hardware Verification" by Glazberg, Moulin, Orni, # Ruah, Zarpas (2007). -check_psl '{1[*];req;ack}|=>{start;busy[*];done}' +check_psl '{[*];req;ack}|=>{start;busy[*];done}' # Make sure 'a U (b U c)' has 3 states and 6 transitions, # before and after degeneralization.