* src/tgbaparse/tgbaparse.yy (cond_list): Simplify into...

(condition): ... this.  We now accept only one condition, which
is a formula.
* src/tgba/tgbaexplicit.hh (tgba_explicit::add_neg_condition,
tgba_explicit::get_condition): Remove, unused.
* src/tgba/tgbaexplicit.cc: Likewise.

ChangeLog

@@ -1,5 +1,12 @@
 2003-11-28  Alexandre Duret-Lutz  <adl@src.lip6.fr>
 
+	* src/tgbaparse/tgbaparse.yy (cond_list): Simplify into...
+	(condition): ... this.  We now accept only one condition, which
+	is a formula.
+	* src/tgba/tgbaexplicit.hh (tgba_explicit::add_neg_condition,
+	tgba_explicit::get_condition): Remove, unused.
+	* src/tgba/tgbaexplicit.cc: Likewise.
+
 	* iface/gspn/eesrg.cc, iface/gspn/eesrg.hh, iface/gspn/gspn.cc,
 	iface/gspn/gspn.hh, src/tgba/bdddict.cc, src/tgba/bdddict.hh,
 	src/tgba/bddprint.hh, src/tgba/succiter.hh,

src/tgba/tgbaexplicit.cc

@@ -171,15 +171,6 @@ namespace spot
     return t;
   }
 
-  bdd
-  tgba_explicit::get_condition(const ltl::formula* f)
-  {
-    assert(dynamic_cast<const ltl::atomic_prop*>(f));
-    int v = dict_->register_proposition(f, this);
-    ltl::destroy(f);
-    return bdd_ithvar(v);
-  }
-
   void
   tgba_explicit::add_condition(transition* t, const ltl::formula* f)
   {
@@ -187,12 +178,6 @@ namespace spot
     ltl::destroy(f);
   }
 
-  void
-  tgba_explicit::add_neg_condition(transition* t, const ltl::formula* f)
-  {
-    t->condition -= get_condition(f);
-  }
-
   void
   tgba_explicit::add_conditions(transition* t, bdd f)
   {

src/tgba/tgbaexplicit.hh

@@ -56,7 +56,6 @@ namespace spot
     create_transition(const std::string& source, const std::string& dest);
 
     void add_condition(transition* t, const ltl::formula* f);
-    void add_neg_condition(transition* t, const ltl::formula* f);
     /// This assumes that all variables in \a f are known from dict.
     void add_conditions(transition* t, bdd f);
     void declare_acceptance_condition(const ltl::formula* f);
@@ -84,7 +83,6 @@ namespace spot
     virtual bdd compute_support_variables(const spot::state* state) const;
 
     state* add_state(const std::string& name);
-    bdd get_condition(const ltl::formula* f);
     bdd get_acceptance_condition(const ltl::formula* f);
 
     typedef Sgi::hash_map<const std::string, tgba_explicit::state*,

src/tgbaparse/tgbaparse.yy

@@ -33,7 +33,7 @@
 {
   int token;
   std::string* str;
-  std::list<std::pair<bool, spot::ltl::formula*> >* listp;
+  spot::ltl::formula* f;
   std::list<spot::ltl::formula*>* list;
 }
 
@@ -59,7 +59,7 @@ typedef std::pair<bool, spot::ltl::formula*> pair;
 %token <str> STRING UNTERMINATED_STRING
 %token <str> IDENT
 %type <str> strident string
-%type <listp> cond_list
+%type <f> condition
 %type <list> acc_list
 %token ACC_DEF
 
@@ -73,22 +73,16 @@ lines: line
        | lines line
        ;
 
-line: strident ',' strident ',' cond_list ',' acc_list ';'
+line: strident ',' strident ',' condition ',' acc_list ';'
        {
 	 spot::tgba_explicit::transition* t
 	   = result->create_transition(*$1, *$3);
-	 std::list<pair>::iterator i;
+	 result->add_condition(t, $5);
-	 for (i = $5->begin(); i != $5->end(); ++i)
+	 std::list<formula*>::iterator i;
-	   if (i->first)
+	 for (i = $7->begin(); i != $7->end(); ++i)
-	     result->add_neg_condition(t, i->second);
+	   result->add_acceptance_condition(t, *i);
-	   else
-	     result->add_condition(t, i->second);
-	 std::list<formula*>::iterator i2;
-	 for (i2 = $7->begin(); i2 != $7->end(); ++i2)
-	     result->add_acceptance_condition(t, *i2);
 	 delete $1;
 	 delete $3;
-	 delete $5;
 	 delete $7;
        }
        ;
@@ -102,40 +96,27 @@ string: STRING
 
 strident: string | IDENT
 
-cond_list:
+condition:
        {
-	 $$ = new std::list<pair>;
+	 $$ = constant::true_instance();
        }
-       | cond_list string
+       | string
        {
-	 if (*$2 != "")
+	 parse_error_list pel;
+	 formula* f = spot::ltl::parse(*$1, pel, parse_environment);
+	 for (parse_error_list::iterator i = pel.begin();
+	      i != pel.end(); ++i)
 	   {
-	     parse_error_list pel;
+	     // Adjust the diagnostic to the current position.
-	     formula* f = spot::ltl::parse(*$2, pel, parse_environment);
+	     Location here = @1;
-	     for (parse_error_list::iterator i = pel.begin();
+	     here.begin.line += i->first.begin.line;
-		  i != pel.end(); ++i)
+	     here.begin.column += i->first.begin.column;
-	       {
+	     here.end.line = here.begin.line + i->first.begin.line;
-		 // Adjust the diagnostic to the current position.
+	     here.end.column = here.begin.column + i->first.begin.column;
-		 Location here = @2;
+	     error_list.push_back(spot::tgba_parse_error(here, i->second));
-		 here.begin.line += i->first.begin.line;
-		 here.begin.column += i->first.begin.column;
-		 here.end.line = here.begin.line + i->first.begin.line;
-		 here.end.column = here.begin.column + i->first.begin.column;
-		 error_list.push_back(spot::tgba_parse_error(here, i->second));
-	       }
-	     $1->push_back(pair(false, f));
 	   }
-	 delete $2;
+	 delete $1;
-	 $$ = $1;
+	 $$ = f ? f : constant::false_instance();
-       }
-       | cond_list '!' strident
-       {
-	 if (*$3 != "")
-	   {
-	     $1->push_back(pair(true, parse_environment.require(*$3)));
-	   }
-	 delete $3;
-	 $$ = $1;
        }
        ;