From f9e859d7659fc5d4c9238b9075609c4766d627b6 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 11 Dec 2014 21:43:08 +0100
Subject: [PATCH] ltlparse: allow comments

* src/ltlparse/ltlscan.ll: Skip comments.
* src/ltltest/ltlfilt.test: Test this.
* NEWS: Mention it.
---
 NEWS                     |  2 ++
 src/ltlparse/ltlscan.ll  | 30 +++++++++++++++++++++++++++++-
 src/ltltest/ltlfilt.test |  6 +++---
 3 files changed, 34 insertions(+), 4 deletions(-)

diff --git a/NEWS b/NEWS
index d60777c02..b783f18ea 100644
--- a/NEWS
+++ b/NEWS
@@ -63,6 +63,8 @@ New in spot 1.99a (not yet released)
       either by Divine (as patched by the LTSmin people) or by
       Spins (the LTSmin compiler for Promela).
 
+    - LTL formulas can include /* comments */.
+
     - Spot is now compiling in C++11 mode.  The set of features we use
       requires GCC >= 4.6 or Clang >= 3.1.  These minimum versions
       are old enough that it should not be an issue to most people.
diff --git a/src/ltlparse/ltlscan.ll b/src/ltlparse/ltlscan.ll
index b7c6291d4..0e014c0fa 100644
--- a/src/ltlparse/ltlscan.ll
+++ b/src/ltlparse/ltlscan.ll
@@ -40,6 +40,8 @@ static int start_token = 0;
 static int parent_level = 0;
 static bool missing_parent = false;
 static bool lenient_mode = false;
+static int orig_cond = 0;
+static unsigned comment_level = 0;
 
 typedef ltlyy::parser::token token;
 
@@ -50,6 +52,7 @@ typedef ltlyy::parser::token token;
 %x in_bra
 %x sqbracket
 %x lbt
+%x in_COMMENT
 
 BOX       "[]"|"□"|"⬜"|"◻"
 DIAMOND   "<>"|"◇"|"⋄"|"♢"
@@ -61,6 +64,8 @@ CIRCLE    "()"|"○"|"◯"
 NOT       "!"|"~"|"¬"
 BOXARROW  {BOX}{ARROWL}|"|"{ARROWL}|"↦"
 BOXDARROW {BOX}{DARROWL}|"|"{DARROWL}|"⤇"
+eol         \n+|\r+
+eol2        (\n\r)+|(\r\n)+
 
 %%
 
@@ -74,6 +79,30 @@ BOXDARROW {BOX}{DARROWL}|"|"{DARROWL}|"⤇"
   yylloc->step();
 %}
 
+<*>"/""*"+		{
+			  if (YY_START != in_COMMENT)
+			    {
+                              orig_cond = YY_START;
+                              BEGIN(in_COMMENT);
+			      comment_level = 0;
+			    }
+			  ++comment_level;
+			}
+<in_COMMENT>{
+  [^*/\n\r]*		continue;
+  "/"[^*\n\r]*		continue;
+  "*"+[^*/\n\r]*	continue;
+  {eol}			yylloc->lines(yyleng); yylloc->end.column = 1;
+  {eol2}		yylloc->lines(yyleng / 2); yylloc->end.column = 1;
+  "*"+"/"		if (--comment_level == 0) BEGIN(orig_cond);
+  <<EOF>>		{
+                           BEGIN(orig_cond);
+                           error_list.push_back(
+			     spot::ltl::one_parse_error(*yylloc,
+			       "unclosed comment"));
+			   return 0;
+                        }
+}
 
 "("				{
 				  if (!lenient_mode)
@@ -308,7 +337,6 @@ BOXDARROW {BOX}{DARROWL}|"|"{DARROWL}|"⤇"
 			  return token::ATOMIC_PROP;
 			}
 
-
 <*>.			return *yytext;
 
 <<EOF>>			return token::END_OF_INPUT;
diff --git a/src/ltltest/ltlfilt.test b/src/ltltest/ltlfilt.test
index d8751d364..455b2d1d9 100755
--- a/src/ltltest/ltlfilt.test
+++ b/src/ltltest/ltlfilt.test
@@ -34,14 +34,14 @@ checkopt()
 # The empty lines in the file are meant, we want to make sure that
 # they are ignored.
 cat >formulas <<EOF
-GFa | FGb
-F(GFa | Gb)
+GFa | FGb /* comment to ignore */
+F(GFa | /* tricky /* comment */)*/ Gb)
 
 F(b W GFa)
 GFa | Gb
 b W GFa
 !{a;b*;c}!
-!{a:b*:c}
+!{a:b[*/*ignore me*/]:c/*ignore this comment*/}
 a U Fb
 G(a & Xb)
 Xa