Create the cosimulation.

* src/tgbaalgos/simulation.cc: Add the cosimulation:
(acc_compl_automaton) Add a template parameter.
(acc_compl_automaton::process_link) Add a swap source destination.
(direct_simulation) Add a template parameter.
(direct_simulation::compute_sig) Add a flag in the signature to
know if the state is initial.
(direct_simulation::build_result) Remove the flag before reading
the signature.
Swap source and destination when building the new automaton.
* src/tgbaalgos/simulation.hh: Declare and document the
Cosimulation.
* src/tgbatest/ltl2tgba.cc: Associate the cosimulation with the -RRS
option.
* src/tgbatest/spotlbtt.test: Add a test on the cosimulation.

src/tgbaalgos/simulation.cc

@@ -78,6 +78,13 @@
 // bdd_support(sig(X)) - allacc - allclassvar
 
 
+// We have had the Cosimulation by changing the acc_compl_automaton by
+// adding a template parameter. If this parameter is set to true, we
+// record the transition in the opposite direction (we just swap
+// sources and destination). In the build result we are making the
+// same thing to rebuild the automaton.
+// In the signature,
+
 namespace spot
 {
   namespace
@@ -93,7 +100,6 @@ namespace spot
                           state_ptr_hash,
                           state_ptr_equal> map_state_unsigned;
 
-
     // Get the list of state for each class.
     typedef std::map<bdd, std::list<const state*>,
                      bdd_less_than> map_bdd_lstate;
@@ -101,6 +107,7 @@ namespace spot
 
     // This class takes an automaton and creates a copy with all
     // acceptance conditions complemented.
+    template <bool Cosimulation>
     class acc_compl_automaton:
       public tgba_reachable_iterator_depth_first
     {
@@ -139,6 +146,15 @@ namespace spot
         int src = get_state(in_s);
         int dst = get_state(out_s);
 
+
+        // In the case of the cosimulation, we want to have all the
+        // ingoing transition, and to keep the rest of the code
+        // similar, we just create equivalent transition in the other
+        // direction. Since we do not have to run through the
+        // automaton to get the signature, this is correct.
+        if (Cosimulation)
+          std::swap(src, dst);
+
         bdd acc = ac_.complement(si->current_acceptance_conditions());
 
         tgba_explicit_number::transition* t
@@ -170,7 +186,7 @@ namespace spot
       state* init_;
     };
 
-
+    template <bool Cosimulation>
     class direct_simulation
     {
       // Shortcut used in update_po and go_to_next_it.
@@ -181,7 +197,7 @@ namespace spot
 	po_size_(0),
 	all_class_var_(bddtrue)
       {
-	acc_compl_automaton
+	acc_compl_automaton<Cosimulation>
 	  acc_compl(t);
 
 	// We'll start our work by replacing all the acceptance
@@ -190,6 +206,8 @@ namespace spot
 
 	a_ = acc_compl.out_;
 
+        initial_state = a_->get_init_state();
+
 	// We use the previous run to know the size of the
 	// automaton, and to class all the reachable states in the
 	// map previous_class_.
@@ -199,11 +217,10 @@ namespace spot
 	// class. We register one bdd by state, because in the worst
 	// case, |Class| == |State|.
 	unsigned set_num = a_->get_dict()
-	  ->register_anonymous_variables(size_a_, a_);
+	  ->register_anonymous_variables(size_a_ + 1, a_);
-	bdd init = bdd_ithvar(set_num);
 
-	// Because we have already take the first element which is init.
+        bdd_initial = bdd_ithvar(set_num++);
-	++set_num;
+	bdd init = bdd_ithvar(set_num++);
 
 	used_var_.push_back(init);
 	all_class_var_ = init;
@@ -258,12 +275,12 @@ namespace spot
                  it_s != it->second.end();
                  ++it_s)
 	      {
-		// If the signature of a state is bddfalse (which is
+		// If the signature of a state is bddfalse (no
-		// roughly equivalent to no transition) the class of
+		// transitions) the class of this state is bddfalse
-		// this state is bddfalse instead of an anonymous
+		// instead of an anonymous variable. It allows
-		// variable. It allows simplifications in the signature
+		// simplifications in the signature by removing a
-		// by removing a transition which has as a destination a
+		// transition which has as a destination a state with
-		// state with no outgoing transition.
+		// no outgoing transition.
 		if (it->first == bddfalse)
 		  previous_class_[*it_s] = bddfalse;
 		else
@@ -297,10 +314,10 @@ namespace spot
       // Take a state and compute its signature.
       bdd compute_sig(const state* src)
       {
-	tgba_succ_iterator* sit = a_->succ_iter(src);
+        tgba_succ_iterator* sit = a_->succ_iter(src);
-	bdd res = bddfalse;
+        bdd res = bddfalse;
 
-	for (sit->first(); !sit->done(); sit->next())
+        for (sit->first(); !sit->done(); sit->next())
           {
             const state* dst = sit->current_state();
             bdd acc = sit->current_acceptance_conditions();
@@ -315,10 +332,16 @@ namespace spot
             dst->destroy();
           }
 
-	delete sit;
+        // When we Cosimulate, we add a special flag to differentiate
-	return res;
+        // initial state.
+        if (Cosimulation && initial_state == src)
+          res |= bdd_initial;
+
+        delete sit;
+        return res;
       }
 
+
       void update_sig()
       {
 	// At this time, current_class_ must be empty.  It implies
@@ -402,21 +425,20 @@ namespace spot
 	     ++it1)
           {
             bdd accu = it1->second;
-
             for (map_bdd_bdd::const_iterator it2 = now_to_next.begin();
                  it2 != now_to_next.end();
                  ++it2)
-	      {
+              {
-		// Skip the case managed by the initialization of accu.
+                // Skip the case managed by the initialization of accu.
-		if (it1 == it2)
+                if (it1 == it2)
-		  continue;
+                  continue;
 
-		if (bdd_implies(it1->first, it2->first))
+                if (bdd_implies(it1->first, it2->first))
-		  {
+                  {
-		    accu &= it2->second;
+                    accu &= it2->second;
-		    ++po_size_;
+                    ++po_size_;
-		  }
+                  }
-	      }
+              }
             relation_[it1->second] = accu;
           }
       }
@@ -476,6 +498,9 @@ namespace spot
             // Get the signature.
             bdd sig = compute_sig(*(it->second.begin()));
 
+            if (Cosimulation)
+              sig = bdd_compose(sig, bddfalse, bdd_var(bdd_initial));
+
             // Get all the variable in the signature.
             bdd sup_sig = bdd_support(sig);
 
@@ -495,7 +520,6 @@ namespace spot
 					bddtrue);
 		all_atomic_prop -= one;
 
-
 		// For each possible valuation, iterator over all possible
 		// destination classes.   We use minato_isop here, because
 		// if the same valuation of atomic properties can go
@@ -533,6 +557,9 @@ namespace spot
 		    int src = bdd2state[previous_class_[*it->second.begin()]];
 		    int dst = bdd2state[dest];
 
+                    if (Cosimulation)
+                      std::swap(src, dst);
+
 		    // src or dst == 0 means "dest" or "prev..." isn't
 		    // in the map.  so it is a bug.
 		    assert(src != 0);
@@ -550,7 +577,9 @@ namespace spot
 
 	res->set_init_state(bdd2state[previous_class_
 				      [a_->get_init_state()]]);
+
 	res->merge_transitions();
+
 	return res;
       }
 
@@ -629,13 +658,29 @@ namespace spot
 
       // All the class variable:
       bdd all_class_var_;
+
+      // The flag to say if the outgoing state is initial or not
+      bdd bdd_initial;
+
+      // Initial state of the automaton we are working on
+      state* initial_state;
+
     };
+
   } // End namespace anonymous.
 
   tgba*
   simulation(const tgba* t)
   {
-    direct_simulation simul(t);
+    direct_simulation<false> simul(t);
+
+    return simul.run();
+  }
+
+  tgba*
+  cosimulation(const tgba* t)
+  {
+    direct_simulation<true> simul(t);
 
     return simul.run();
   }

src/tgbaalgos/simulation.hh

@@ -30,12 +30,11 @@ namespace spot
   /// \addtogroup tgba_reduction
   /// @{
 
-  /// \brief Attempt to reduce the automaton by direct simulation
+  /// \brief Attempt to reduce the automaton by direct simulation When
-  ///
+  /// the suffixes (letter and acceptance conditions) seen by one
-  /// When the language recognized by one state is included in the
+  /// state is included in the suffixes seen by another one, the first
-  /// language recognized by an another one, the first one is merged
+  /// one is merged with the second.  The algorithm is based on the
-  /// with the second.  The algorithm is based on the following
+  /// following paper, but generalized to handle TGBA directly.
-  /// paper, but generalized to handle TGBA directly.
   ///
   /// \verbatim
   /// @InProceedings{ etessami.00.concur,
@@ -58,6 +57,34 @@ namespace spot
   /// one
   tgba* simulation(const tgba* automaton);
 
+
+  /// \brief Attempt to reduce the automaton by direct cosimulation.
+  /// When the prefixes (letter and acceptance conditions) seen by one
+  /// state is included in the prefixes seen by another one, the first
+  /// one is merged with the second.  The algorithm is based on the
+  /// following paper, but generalized to handle TGBA directly.
+  /// \verbatim
+  /// @InProceedings{Somenzi:2000:EBA:647769.734097,
+  ///    author = {Somenzi, Fabio and Bloem, Roderick},
+  ///    title = {Efficient {B\"u}chi Automata from LTL Formulae},
+  ///    booktitle = {Proceedings of the 12th International
+  ///                 Conference on Computer Aided Verification},
+  ///    series = {CAV '00},
+  ///    year = {2000},
+  ///    isbn = {3-540-67770-4},
+  ///    pages = {248--263},
+  ///    numpages = {16},
+  ///    url = {http://dl.acm.org/citation.cfm?id=647769.734097},
+  ///    acmid = {734097},
+  ///    publisher = {Springer-Verlag},
+  ///    address = {London, UK, UK},
+  /// }
+  /// \endverbatim
+  /// \param automaton the automaton to simulate.
+  /// \return a new automaton which is at worst a copy of the received
+  /// one
+  tgba* cosimulation(const tgba* automaton);
+
   /// @}
 } // End namespace spot.
 

src/tgbatest/ltl2tgba.cc

@@ -204,6 +204,8 @@ syntax(char* prog)
 	    << std::endl
 	    << "  -RDS  minimize the automaton with direct simulation"
 	    << std::endl
+	    << "  -RRS  minimize the automaton with reverse simulation"
+	    << std::endl
             << "  -Rm   attempt to WDBA-minimize the automata" << std::endl
 	    << std::endl
 
@@ -352,13 +354,14 @@ main(int argc, char** argv)
   bool use_timer = false;
   bool assume_sba = false;
   bool reduction_dir_sim = false;
+  bool reduction_rev_sim = false;
   spot::tgba* temp_dir_sim = 0;
   bool ta_opt = false;
   bool tgta_opt = false;
   bool opt_with_artificial_initial_state = true;
   bool opt_single_pass_emptiness_check = false;
   bool opt_with_artificial_livelock = false;
-
+  spot::tgba* temp_rev_sim = 0;
 
   for (;;)
     {
@@ -631,6 +634,10 @@ main(int argc, char** argv)
 	  // equal to -RDS.
 	  reduction_dir_sim = true;
 	}
+      else if (!strcmp(argv[formula_index], "-RRS"))
+        {
+          reduction_rev_sim = true;
+        }
       else if (!strcmp(argv[formula_index], "-R3"))
 	{
 	  scc_filter = true;
@@ -1031,11 +1038,21 @@ main(int argc, char** argv)
 	      a = minimized;
               // When the minimization succeed, simulation is useless.
               reduction_dir_sim = false;
+              reduction_rev_sim = false;
 	      assume_sba = true;
 	    }
 	}
 
 
+      if (reduction_rev_sim)
+        {
+          tm.start("Reduction w/ reverse simulation");
+          temp_rev_sim = spot::cosimulation(a);
+          a = temp_rev_sim;
+          tm.stop("Reduction w/ reverse simulation");
+	  assume_sba = false;
+        }
+
       if (reduction_dir_sim)
         {
           tm.start("Reduction w/ direct simulation");
@@ -1505,6 +1522,7 @@ main(int argc, char** argv)
       delete to_free;
       delete echeck_inst;
       delete temp_dir_sim;
+      delete temp_rev_sim;
     }
   else
     {

src/tgbatest/spotlbtt.test

@@ -199,6 +199,15 @@ Algorithm
    Enabled = yes
 }
 
+Algorithm
+{
+   Name = "Spot (Couvreur -- FM), cosimulated"
+   Path = "${LBTT_TRANSLATE}"
+   Parameters = "--spot '../ltl2tgba -F -f -t -RRS  -r4 -R3'"
+   Enabled = yes
+}
+
+
 Algorithm
 {
    Name = "Spot (Couvreur -- LaCim), simulated"