neverparse: build a tgba_digraph

* src/neverparse/neverclaimparse.yy, src/neverparse/public.hh,
src/tgbatest/ltl2tgba.cc, src/tgbatest/neverclaimread.test: Adjust.

src/neverparse/neverclaimparse.yy

@@ -33,18 +33,29 @@
 #include <cstring>
 #include "ltlast/constant.hh"
 #include "public.hh"
+#include "tgba/formula2bdd.hh"
 
-  typedef std::pair<const spot::ltl::formula*, std::string*> pair;
+/* Cache parsed formulae.  Labels on arcs are frequently identical and
+   it would be a waste of time to parse them to formula* over and
+   over, and to register all their atomic_propositions in the
+   bdd_dict.  Keep the bdd result around so we can reuse it.  */
+  typedef std::map<std::string, bdd> formula_cache;
+
+  typedef std::pair<const bdd*, std::string*> pair;
+  typedef typename spot::tgba_digraph::namer<std::string>::type named_tgba_t;
 }
 
 %parse-param {spot::neverclaim_parse_error_list& error_list}
 %parse-param {spot::ltl::environment& parse_environment}
-%parse-param {spot::tgba_explicit_string*& result}
+%parse-param {spot::tgba_digraph*& result}
+%parse-param {named_tgba_t*& namer}
+%parse-param {formula_cache& fcache}
 %union
 {
   std::string* str;
   pair* p;
   std::list<pair>* list;
+  const bdd* b;
 }
 
 %code
@@ -74,24 +85,24 @@ static bool accept_all_seen = false;
 %token ASSERT "assert"
 %token <str> FORMULA "boolean formula"
 %token <str> IDENT "identifier"
-%type <str> formula opt_dest
+%type <b> formula
+%type <str> opt_dest
 %type <p> transition src_dest
 %type <list> transitions transition_block
 %type <str> ident_list
 
 
 %destructor { delete $$; } <str>
-%destructor { $$->first->destroy(); delete $$->second; delete $$; } <p>
+%destructor { delete $$->second; delete $$; } <p>
 %destructor {
   for (std::list<pair>::iterator i = $$->begin();
        i != $$->end(); ++i)
   {
-    i->first->destroy();
     delete i->second;
   }
   delete $$;
   } <list>
-  %printer {
+%printer {
     if ($$)
       debug_stream() << *$$;
     else
@@ -111,11 +122,12 @@ states:
 ident_list:
     IDENT ':'
     {
+      namer->new_state(*$1);
       $$ = $1;
     }
   | ident_list IDENT ':'
     {
-      result->add_state_alias(*$2, *$1);
+      namer->alias_state(namer->get_state(*$1), *$2);
       // Keep any identifier that starts with accept.
       if (strncmp("accept", $1->c_str(), 6))
         {
@@ -146,11 +158,10 @@ state:
       if (*$1 == "accept_all")
 	accept_all_seen = true;
 
-      spot::state_explicit_string::transition* t = result->create_transition(*$1, *$1);
+      namer->new_transition(*$1, *$1, bddtrue,
-      bool acc = !strncmp("accept", $1->c_str(), 6);
+			    !strncmp("accept", $1->c_str(), 6) ?
-      if (acc)
+			    result->all_acceptance_conditions() :
-	result->add_acceptance_condition(t,
+			    static_cast<const bdd>(bddfalse));
-					 spot::ltl::constant::true_instance());
       delete $1;
     }
   | ident_list { delete $1; }
@@ -158,22 +169,15 @@ state:
   | ident_list transition_block
     {
       std::list<pair>::iterator it;
-      bool acc = !strncmp("accept", $1->c_str(), 6);
+      bdd acc = !strncmp("accept", $1->c_str(), 6) ?
-      for (it = $2->begin(); it != $2->end(); ++it)
+	result->all_acceptance_conditions() :
-      {
+	static_cast<const bdd>(bddfalse);
-	spot::state_explicit_string::transition* t =
+      for (auto& p: *$2)
-	  result->create_transition(*$1, *it->second);
+	namer->new_transition(*$1, *p.second, *p.first, acc);
-
-	result->add_condition(t, it->first);
-	if (acc)
-	  result
-	    ->add_acceptance_condition(t, spot::ltl::constant::true_instance());
-      }
       // Free the list
       delete $1;
-      for (std::list<pair>::iterator it = $2->begin();
+      for (auto& p: *$2)
-	   it != $2->end(); ++it)
+	delete p.second;
-	delete it->second;
       delete $2;
     }
 
@@ -191,7 +195,43 @@ transitions:
     }
 
 
-formula: FORMULA | "false" { $$ = new std::string("0"); }
+formula: FORMULA
+     {
+       formula_cache::const_iterator i = fcache.find(*$1);
+       if (i == fcache.end())
+	 {
+	   parse_error_list pel;
+	   const formula* f =
+	     spot::ltl::parse_boolean(*$1, pel, parse_environment,
+				      debug_level(), true);
+	   for (auto& j: pel)
+	     {
+	       // Adjust the diagnostic to the current position.
+	       spot::location here = @1;
+	       here.end.line = here.begin.line + j.first.end.line - 1;
+	       here.end.column = here.begin.column + j.first.end.column;
+	       here.begin.line += j.first.begin.line - 1;
+	       here.begin.column += j.first.begin.column;
+	       error_list.emplace_back(here, j.second);
+	     }
+           bdd cond = bddfalse;
+	   if (f)
+	     {
+	       cond = formula_to_bdd(f, result->get_dict(), result);
+	       f->destroy();
+	     }
+	   $$ = &(fcache[*$1] = cond);
+	 }
+       else
+	 {
+	   $$ = &i->second;
+	 }
+       delete $1;
+     }
+   | "false"
+     {
+       $$ = &bddfalse;
+     }
 
 opt_dest:
   /* empty */
@@ -218,28 +258,12 @@ src_dest: formula opt_dest
       //   fi
       if (!$2)
 	{
-	  delete $1;
 	  $$ = 0;
 	}
       else
 	{
-	  spot::ltl::parse_error_list pel;
+	  $$ = new pair($1, $2);
-	  const spot::ltl::formula* f =
+	  namer->new_state(*$2);
-	    spot::ltl::parse_boolean(*$1, pel, parse_environment,
-				     debug_level(), true);
-	  delete $1;
-	  for(spot::ltl::parse_error_list::const_iterator i = pel.begin();
-	  i != pel.end(); ++i)
-	    {
-	      // Adjust the diagnostic to the current position.
-	      spot::location here = @1;
-	      here.end.line = here.begin.line + i->first.end.line - 1;
-	      here.end.column = here.begin.column + i->first.end.column -1;
-	      here.begin.line += i->first.begin.line - 1;
-	      here.begin.column += i->first.begin.column - 1;
-	      error(here, i->second);
-	    }
-	  $$ = new pair(f, $2);
 	}
     }
 
@@ -264,7 +288,7 @@ neverclaimyy::parser::error(const location_type& location,
 
 namespace spot
 {
-  tgba_explicit_string*
+  tgba_digraph*
   neverclaim_parse(const std::string& name,
 		   neverclaim_parse_error_list& error_list,
 		   bdd_dict* dict,
@@ -277,23 +301,28 @@ namespace spot
 				std::string("Cannot open file ") + name);
 	return 0;
       }
-    tgba_explicit_string* result = new tgba_explicit_string(dict);
+    formula_cache fcache;
-    result->declare_acceptance_condition(spot::ltl::constant::true_instance());
+    tgba_digraph* result = new tgba_digraph(dict);
-    neverclaimyy::parser parser(error_list, env, result);
+    auto namer = result->create_namer<std::string>();
+
+    const ltl::formula* t = ltl::constant::true_instance();
+    bdd acc = bdd_ithvar(dict->register_acceptance_variable(t, result));
+    result->set_acceptance_conditions(acc);
+
+    neverclaimyy::parser parser(error_list, env, result, namer, fcache);
     parser.set_debug_level(debug);
     parser.parse();
     neverclaimyyclose();
 
     if (accept_all_needed && !accept_all_seen)
       {
-	spot::state_explicit_string::transition* t =
+	unsigned n = namer->new_state("accept_all");
-	  result->create_transition("accept_all", "accept_all");
+	result->new_transition(n, n, bddtrue, acc);
-	result->add_acceptance_condition
-	  (t, spot::ltl::constant::true_instance());
       }
     accept_all_needed = false;
     accept_all_seen = false;
 
+    delete namer;
     return result;
   }
 }

src/neverparse/public.hh

@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2010, 2013 Laboratoire de Recherche et Développement
+// Copyright (C) 2010, 2013, 2014 Laboratoire de Recherche et
-// de l'Epita (LRDE).
+// Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -20,7 +20,7 @@
 #ifndef SPOT_NEVERPARSE_PUBLIC_HH
 # define SPOT_NEVERPARSE_PUBLIC_HH
 
-# include "tgba/tgbaexplicit.hh"
+# include "tgba/tgbagraph.hh"
 # include "misc/location.hh"
 # include "ltlenv/defaultenv.hh"
 # include <string>
@@ -55,7 +55,7 @@ namespace spot
   /// was parsed succesfully, check \a error_list for emptiness.
   ///
   /// \warning This function is not reentrant.
-  SPOT_API tgba_explicit_string*
+  SPOT_API tgba_digraph*
   neverclaim_parse(const std::string& filename,
 		   neverclaim_parse_error_list&
 		   error_list,

src/tgbatest/ltl2tgba.cc

@@ -1025,6 +1025,7 @@ main(int argc, char** argv)
 	      break;
 	    case ReadNeverclaim:
 	      {
+		spot::tgba_digraph* e;
 		spot::neverclaim_parse_error_list pel;
 		tm.start("parsing neverclaim");
 		to_free = a = e = spot::neverclaim_parse(input, pel, dict,
@@ -1037,6 +1038,7 @@ main(int argc, char** argv)
 		    return 2;
 		  }
 		assume_sba = true;
+		e->merge_transitions();
 	      }
 	      break;
 	    case ReadLbtt:

src/tgbatest/neverclaimread.test

@@ -1,6 +1,6 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2010, 2011, 2012, 2013 Laboratoire de Recherche et
+# Copyright (C) 2010, 2011, 2012, 2013, 2014 Laboratoire de Recherche et
 # Développement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -47,14 +47,14 @@ cat >expected <<EOF
 digraph G {
   0 [label="", style=invis, height=0]
   0 -> 1
-  1 [label="T2_init"]
+  1 [label="0"]
   1 -> 1 [label="1\n"]
   1 -> 2 [label="p0 & p1\n"]
-  2 [label="T1"]
+  2 [label="1"]
   2 -> 3 [label="p1 & !p0\n"]
   2 -> 2 [label="!p1\n"]
   2 -> 1 [label="!p1\n"]
-  3 [label="accept_all", peripheries=2]
+  3 [label="2", peripheries=2]
   3 -> 3 [label="1\n{Acc[1]}"]
 }
 EOF
@@ -91,14 +91,14 @@ cat >expected <<EOF
 digraph G {
   0 [label="", style=invis, height=0]
   0 -> 1
-  1 [label="T2_init"]
+  1 [label="0"]
   1 -> 1 [label="1\n"]
   1 -> 2 [label="p0 & p1\n"]
-  2 [label="T1"]
+  2 [label="1"]
   2 -> 3 [label="p1 & !p0\n"]
   2 -> 2 [label="!p1\n"]
   2 -> 1 [label="!p1\n"]
-  3 [label="accept_all", peripheries=2]
+  3 [label="2", peripheries=2]
   3 -> 3 [label="1\n{Acc[1]}"]
 }
 EOF
@@ -130,9 +130,9 @@ cat >expected <<EOF
 digraph G {
   0 [label="", style=invis, height=0]
   0 -> 1
-  1 [label="accept_init", peripheries=2]
+  1 [label="0", peripheries=2]
   1 -> 2 [label="p1\n{Acc[1]}"]
-  2 [label="accept_all", peripheries=2]
+  2 [label="1", peripheries=2]
   2 -> 2 [label="1\n{Acc[1]}"]
 }
 EOF