Allow atomic propositions negated with a combining overline.

* src/ltlparse/ltlscan.ll: Understand the combining overline, and
combining overbar as synonym for =0.
* src/ltlvisit/tostring.cc: Emit a combining overline for
single-letter atomic propositions.
* src/ltlast/atomic_prop.hh (is_atomic_prop): New function.
* doc/tl/tl.tex: Document these two characters.

doc/tl/tl.tex

@@ -381,6 +381,12 @@ syntax \samp{$a$=0}, which is equivalent to \samp{$\NOT a$}.  Also
 \samp{$a$=1} is equivalent to just \samp{a}.  These two syntaxes help
 us read formul\ae{} written using Wring's syntax.
 
+When using UTF-8 input, a \samp{=0} that follow a single-letter atomic
+proposition may be replaced by a combining overline \uni{0305} or a
+combining overbar \uni{0304}.  When instructed to emit UTF-8, Spot
+will output \samp{$\bar{\mathtt{a}}$} using a combining overline
+instead of \samp{$\lnot$a} for any single-letter atomic proposition.
+
 \label{def:boolform}
 When a formula is built using only Boolean constants
 (section~\ref{sec:bool}), atomic proposition (section~\ref{sec:ap}),

src/ltlast/atomic_prop.hh

@@ -1,7 +1,8 @@
-// Copyright (C) 2009 Laboratoire de Recherche et Développement
+// -*- coding: utf-8 -*-
+// Copyright (C) 2009, 2012 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.
@@ -75,6 +76,14 @@ namespace spot
       environment* env_;
     };
 
+    inline
+    const atomic_prop*
+    is_atomic_prop(const formula* f)
+    {
+      if (f->kind() != formula::AtomicProp)
+	return 0;
+      return static_cast<const atomic_prop*>(f);
+    }
   }
 }
 

src/ltlparse/ltlscan.ll

@@ -158,7 +158,9 @@ BOXDARROW {BOX}{DARROWL}|"|"{DARROWL}|"⤇"
 "W"				BEGIN(0); return token::OP_W;
 "M"				BEGIN(0); return token::OP_M;
 
-"=0"				return token::OP_POST_NEG;
+  /* The combining overline or macron (overbar) should normally
+     occur only after a single letter, but we do not check that. */
+"=0"|"̅"|"̄"			return token::OP_POST_NEG;
 "=1"				return token::OP_POST_POS;
 
 <*>[ \t\n]+			/* discard whitespace */ yylloc->step ();

src/ltlvisit/tostring.cc

@@ -66,7 +66,7 @@ namespace spot
 	KAndRat,
 	KAndNLM,
 	KConcat,
-	KFusion
+	KFusion,
       };
 
       const char* spot_kw[] = {
@@ -96,7 +96,7 @@ namespace spot
 	" && ",
 	" & ",
 	";",
-	":"
+	":",
       };
 
       const char* spin_kw[] = {
@@ -488,6 +488,7 @@ namespace spot
 	  // propositions.  So make sure we output F(0), G(1), etc.
 	  bool need_parent = (uo->child()->kind() == formula::Constant);
 	  bool top_level = top_level_;
+	  bool overline = false;
 
 	  if (full_parent_)
 	    {
@@ -500,8 +501,18 @@ namespace spot
 	  switch (uo->op())
 	    {
 	    case unop::Not:
-	      emit(KNot);
 	      need_parent = false;
+	      // If we negate a single letter in UTF-8, use a
+	      // combining overline.
+	      if (!full_parent_ && kw_ == utf8_kw)
+		if (const ltl::atomic_prop* ap = is_atomic_prop(uo->child()))
+		  if (ap->name().size() == 1
+		      && is_bare_word(ap->name().c_str()))
+		    {
+		      overline = true;
+		      break;
+		    }
+	      emit(KNot);
 	      break;
 	    case unop::X:
 	      emit(KX);
@@ -549,6 +560,11 @@ namespace spot
 
 	  if (full_parent_ && !top_level)
 	    closep();
+	  else if (overline)
+	    // The following string contains only the character U+0305
+	    // (a combining overline).  It looks better than U+0304 (a
+	    // combining overbar).
+	    os_ << "̅";
 	}
 
 	void