TA Product optimization and WFair Formulas generation

* src/ta/taproduct.cc: TA Product optimization
* src/ltltest/randltl.cc: WFair Formulas generation

src/ltltest/randltl.cc

@@ -28,6 +28,7 @@
 #include <string>
 #include <cstdlib>
 #include <cstring>
+#include <sstream>
 #include "ltlast/atomic_prop.hh"
 #include "ltlvisit/randomltl.hh"
 #include "ltlvisit/tostring.hh"
@@ -36,6 +37,14 @@
 #include "ltlenv/defaultenv.hh"
 #include "misc/random.hh"
 
+#include "ltlast/allnodes.hh"
+
+
+using namespace spot;
+using namespace spot::ltl;
+
+environment& env(default_environment::instance());
+
 void
 syntax(char* prog)
 {
@@ -86,6 +95,35 @@ to_int(const char* s)
   return res;
 }
 
+
+// GF(p_1) & GF(p_2) & ... & GF(p_n)
+formula* GF_n(spot::ltl::atomic_prop_set* ap, int n)
+{
+
+  formula* result = 0;
+
+  multop::type op =  multop::And;
+
+  spot::ltl::atomic_prop_set::const_iterator i = ap->begin();
+    while (i != ap->end())
+      {
+
+      std::ostringstream p;
+      p <<  (*i)->name();
+      ++i;
+      formula* f = unop::instance(unop::G,
+                                  unop::instance(unop::F,
+                                                 env.require(p.str())));
+
+      if (result)
+        result = multop::instance(op, f, result);
+      else
+        result = f;
+    }
+  return result;
+}
+
+
 int
 main(int argc, char** argv)
 {
@@ -102,6 +140,7 @@ main(int argc, char** argv)
   bool opt_u = false;
   spot::ltl::ltl_simplifier_options simpopt(true, true, true, true, true);
   spot::ltl::ltl_simplifier simp(simpopt);
+  bool opt_wFair = false;
 
   spot::ltl::environment& env(spot::ltl::default_environment::instance());
   spot::ltl::atomic_prop_set* ap = new spot::ltl::atomic_prop_set;
@@ -183,6 +222,10 @@ main(int argc, char** argv)
 	{
 	  opt_u = true;
 	}
+      else if (!strcmp(argv[argn], "-wf"))
+        {
+          opt_wFair = true;
+        }
       else
 	{
 	  ap->insert(static_cast<const spot::ltl::atomic_prop*>
@@ -315,6 +358,10 @@ main(int argc, char** argv)
 	      while (max_tries_r--)
 		{
 		  f = rf->generate(opt_f);
+                  if (opt_wFair)
+                    {
+                      f = GF_n(atomic_prop_collect(f, 0), f->hash());
+                    }
 		  if (opt_r)
 		    {
 		      const spot::ltl::formula* g = simp.simplify(f);

src/ta/taproduct.cc

@@ -31,7 +31,7 @@ namespace spot
 
   state_ta_product::state_ta_product(const state_ta_product& o) :
     state(), ta_state_(o.get_ta_state()), kripke_state_(
-	o.get_kripke_state()->clone())
+        o.get_kripke_state()->clone())
   {
   }
 
@@ -91,9 +91,9 @@ namespace spot
       ta_succ_it_->next();
     if (ta_succ_it_->done())
       {
-	delete ta_succ_it_;
+        delete ta_succ_it_;
-	ta_succ_it_ = 0;
+        ta_succ_it_ = 0;
-	kripke_succ_it_->next();
+        kripke_succ_it_->next();
       }
   }
 
@@ -111,9 +111,9 @@ namespace spot
     // done().)
     if (kripke_succ_it_->done())
       {
-	delete kripke_succ_it_;
+        delete kripke_succ_it_;
-	kripke_succ_it_ = 0;
+        kripke_succ_it_ = 0;
-	return;
+        return;
       }
 
     next_non_stuttering_();
@@ -126,8 +126,8 @@ namespace spot
     current_state_ = 0;
     if (is_stuttering_transition())
       {
-	ta_succ_it_ = 0;
+        ta_succ_it_ = 0;
-	kripke_succ_it_->next();
+        kripke_succ_it_->next();
       }
     else
       step_();
@@ -144,34 +144,36 @@ namespace spot
 
     while (!done())
       {
-	state * kripke_succ_it_current_state = kripke_succ_it_->current_state();
+        state * kripke_succ_it_current_state = kripke_succ_it_->current_state();
-	bdd dc = kripke_->state_condition(kripke_succ_it_current_state);
+        bdd dc = kripke_->state_condition(kripke_succ_it_current_state);
 
-	is_stuttering_transition_ = (sc == dc);
+        is_stuttering_transition_ = (sc == dc);
-	if (is_stuttering_transition_)
+        if (is_stuttering_transition_)
-	  {
+          {
-	    //if stuttering transition, the TA automata stays in the same state
+            //if stuttering transition, the TA automata stays in the same state
-	    current_state_ = new state_ta_product(source_->get_ta_state(),
+            current_state_ = new state_ta_product(source_->get_ta_state(),
-		kripke_succ_it_current_state);
+                kripke_succ_it_current_state);
-	    current_condition_ = bddtrue;
+            current_condition_ = bddtrue;
-	    return;
+            return;
-	  }
+          }
 
-	if (ta_succ_it_ == 0){
+        if (ta_succ_it_ == 0)
-	    current_condition_ = bdd_setxor(sc, dc);
+          {
-	    ta_succ_it_ = ta_->succ_iter(source_->get_ta_state(), current_condition_);
+            current_condition_ = bdd_setxor(sc, dc);
-	    ta_succ_it_->first();
+            ta_succ_it_ = ta_->succ_iter(source_->get_ta_state(),
-	}
+                current_condition_);
+            ta_succ_it_->first();
+          }
 
-	if (!ta_succ_it_->done())
+        if (!ta_succ_it_->done())
-	  {
+          {
-	    current_state_ = new state_ta_product(ta_succ_it_->current_state(),
+            current_state_ = new state_ta_product(ta_succ_it_->current_state(),
-		kripke_succ_it_current_state);
+                kripke_succ_it_current_state);
-	    return;
+            return;
-	  }
+          }
 
-	kripke_succ_it_current_state->destroy();
+        kripke_succ_it_current_state->destroy();
-	step_();
+        step_();
       }
   }
 
@@ -227,7 +229,7 @@ namespace spot
   ta_product::ta_product(const ta* testing_automata,
       const kripke* kripke_structure) :
     dict_(testing_automata->get_dict()), ta_(testing_automata), kripke_(
-	kripke_structure)
+        kripke_structure)
   {
     assert(dict_ == kripke_structure->get_dict());
     dict_->register_all_variables_of(&ta_, this);
@@ -249,25 +251,24 @@ namespace spot
     ta::states_set_t::const_iterator it;
 
     ta::states_set_t initial_states_set;
+    state* kripke_init_state = kripke_->get_init_state();
+    bdd kripke_init_state_condition = kripke_->state_condition(
+        kripke_init_state);
 
     for (it = ta_init_states_set.begin(); it != ta_init_states_set.end(); it++)
       {
-	state* kripke_init_state = kripke_->get_init_state();
-	if ((kripke_->state_condition(kripke_init_state))
-	    == (ta_->get_state_condition(*it)))
-	  {
-	    state_ta_product* stp = new state_ta_product((*it),
-		kripke_init_state);
 
-	    initial_states_set.insert(stp);
+        if (kripke_init_state_condition == (ta_->get_state_condition(*it)))
-	  }
+          {
-	else
+            state_ta_product* stp = new state_ta_product((*it),
-	  {
+                kripke_init_state->clone());
-	    kripke_init_state->destroy();
+
-	  }
+            initial_states_set.insert(stp);
+          }
 
       }
 
+    kripke_init_state->destroy();
     return initial_states_set;
   }
 
@@ -292,7 +293,7 @@ namespace spot
     const state_ta_product* s = down_cast<const state_ta_product*> (state);
     assert(s);
     return kripke_->format_state(s->get_kripke_state()) + " * \n"
-	+ ta_->format_state(s->get_ta_state());
+        + ta_->format_state(s->get_ta_state());
   }
 
   bool
@@ -323,9 +324,9 @@ namespace spot
     state* kr_s = stp->get_kripke_state();
 
     return (ta_->is_initial_state(ta_s))
-	&& ((kripke_->get_init_state())->compare(kr_s) == 0)
+        && ((kripke_->get_init_state())->compare(kr_s) == 0)
-	&& ((kripke_->state_condition(kr_s))
+        && ((kripke_->state_condition(kr_s))
-	    == (ta_->get_state_condition(ta_s)));
+            == (ta_->get_state_condition(ta_s)));
   }
 
   bdd