From 93c042d0fa82e7b664bb0b2e681022618d2198a3 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 10 Mar 2010 16:01:27 +0100
Subject: [PATCH] Recognize and use "*" (or "[*]") as an abbreviation for 1*.

* src/ltlparse/ltlparse.yy: Recognize "*" as "1*".
* src/ltlvisit/tostring.cc: Abbreviate "1*" as "*".
* src/tgbatest/ltl2tgba.test: Use the new syntax.
---
 src/ltlparse/ltlparse.yy   |  2 ++
 src/ltlvisit/tostring.cc   | 12 ++++++++++++
 src/tgbatest/ltl2tgba.test |  2 +-
 3 files changed, 15 insertions(+), 1 deletion(-)

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.