* src/tgbaalgos/ltl2tgba_fm.hh (ltl_to_tgba_fm): New unobs argument.

* src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Handle unobs.
* src/tgbatest/ltl2tgba.cc (syntax, main): New -U option.

ChangeLog

@@ -1,3 +1,9 @@
+2004-09-23  Alexandre Duret-Lutz  <adl@src.lip6.fr>
+
+	* src/tgbaalgos/ltl2tgba_fm.hh (ltl_to_tgba_fm): New unobs argument.
+	* src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Handle unobs.
+	* src/tgbatest/ltl2tgba.cc (syntax, main): New -U option.
+
 2004-09-21  Alexandre Duret-Lutz  <adl@src.lip6.fr>
 
 	* src/tgbaalgos/colordfs.hh, src/tgbaalgos/minimalce.cc,

src/tgbaalgos/ltl2tgba_fm.cc

@@ -30,8 +30,9 @@
 #include "ltlvisit/destroy.hh"
 #include "ltlvisit/tostring.hh"
 #include "ltlvisit/postfix.hh"
+#include "ltlvisit/apcollect.hh"
 #include <cassert>
-
+#include <memory>
 #include "tgba/tgbabddconcretefactory.hh"
 #include "ltl2tgba_fm.hh"
 
@@ -639,7 +640,7 @@ namespace spot
   tgba_explicit*
   ltl_to_tgba_fm(const formula* f, bdd_dict* dict,
 		 bool exprop, bool symb_merge, bool branching_postponement,
-		 bool fair_loop_approx)
+		 bool fair_loop_approx, const ltl::atomic_prop_set* unobs)
   {
     possible_fair_loop_checker pflc;
 
@@ -659,13 +660,47 @@ namespace spot
 
     // Compute the set of all promises occurring inside the formula.
     bdd all_promises = bddtrue;
-    if (fair_loop_approx)
+    if (fair_loop_approx || unobs)
       {
 	ltl_promise_visitor pv(d);
 	f2->accept(pv);
 	all_promises = pv.result();
       }
 
+    // These are used when atomic propositions are interpreted as
+    // events.  There are two kinds of events: observable events are
+    // those used in the formula, and unobservable events or other
+    // events that can occur at anytime.  All events exclude each
+    // other.
+    bdd observable_events = bddfalse;
+    bdd unobservable_events = bddfalse;
+    if (unobs)
+      {
+	bdd neg_events = bddtrue;
+	std::auto_ptr<ltl::atomic_prop_set> aps(ltl::atomic_prop_collect(f));
+	for (ltl::atomic_prop_set::const_iterator i = aps->begin();
+	     i != aps->end(); ++i)
+	  {
+	    int p = d.register_proposition(*i);
+	    bdd pos = bdd_ithvar(p);
+	    bdd neg = bdd_nithvar(p);
+	    observable_events = (observable_events & neg) | (neg_events & pos);
+	    neg_events &= neg;
+	  }
+	for (ltl::atomic_prop_set::const_iterator i = unobs->begin();
+	     i != unobs->end(); ++i)
+	  {
+	    int p = d.register_proposition(*i);
+	    bdd pos = bdd_ithvar(p);
+	    bdd neg = bdd_nithvar(p);
+	    unobservable_events = ((unobservable_events & neg)
+				   | (neg_events & pos));
+	    observable_events &= neg;
+	    neg_events &= neg;
+	  }
+      }
+    bdd all_events = observable_events | unobservable_events;
+
     formulae_seen.insert(f2);
     formulae_to_translate.insert(f2);
 
@@ -682,6 +717,14 @@ namespace spot
 	// Translate it into a BDD to simplify it.
 	bdd res = fc.translate(f);
 
+	// Handle exclusive events.
+	if (unobs)
+	  {
+	    res &= observable_events;
+	    int n = d.register_next_variable(f);
+	    res |= unobservable_events & bdd_ithvar(n) & all_promises;
+	  }
+
 	std::string now = to_string(f);
 
 	// When branching_postponement is used, we must assume that
@@ -818,6 +861,11 @@ namespace spot
 	    assert(j->first == bddtrue);
 
 	    cond_for_true = j->second;
+	    // When translating LTL for an event-based logic with
+	    // unobservable events, the 1 state should accept even
+	    // unobservable events.
+	    if (unobs && f == constant::true_instance())
+	      cond_for_true = all_events;
 	    tgba_explicit::transition* t =
 	      a->create_transition(now, constant::true_instance()->val_name());
 	    a->add_condition(t, d.bdd_to_formula(cond_for_true));

src/tgbaalgos/ltl2tgba_fm.hh

@@ -24,6 +24,7 @@
 
 #include "ltlast/formula.hh"
 #include "tgba/tgbaexplicit.hh"
+#include "ltlvisit/apcollect.hh"
 
 namespace spot
 {
@@ -89,11 +90,16 @@ namespace spot
   /// unstable state is used to suppress all acceptance conditions from
   /// incoming transitions.
   ///
+  /// \param unobs When non-zero, the atomic propositions in the LTL formula
+  /// are interpreted as events that exclude each other.  The events in the
+  /// formula are observable events, and \c unobs can be filled with
+  /// additional unobservable events.
   /// \return A spot::tgba_explicit that recognizes the language of \a f.
   tgba_explicit* ltl_to_tgba_fm(const ltl::formula* f, bdd_dict* dict,
 				bool exprop = false, bool symb_merge = true,
 				bool branching_postponement = false,
-				bool fair_loop_approx = false);
+				bool fair_loop_approx = false,
+				const ltl::atomic_prop_set* unobs = 0);
 }
 
 #endif // SPOT_TGBA_LTL2TGBA_HH

src/tgbatest/ltl2tgba.cc

@@ -26,6 +26,7 @@
 #include "ltlvisit/destroy.hh"
 #include "ltlvisit/reduce.hh"
 #include "ltlvisit/tostring.hh"
+#include "ltlvisit/apcollect.hh"
 #include "ltlast/allnodes.hh"
 #include "ltlparse/public.hh"
 #include "tgbaalgos/ltl2tgba_lacim.hh"
@@ -45,7 +46,6 @@
 #include "tgbaparse/public.hh"
 #include "tgbaalgos/dupexp.hh"
 #include "tgbaalgos/neverclaim.hh"
-
 #include "tgbaalgos/reductgba_sim.hh"
 
 void
@@ -152,6 +152,8 @@ syntax(char* prog)
 	    << std::endl
 	    << "  -TJ   tarjan-on-fly (implies -D), expect no counter-example"
 	    << std::endl
+            << "  -U[PROPS]  consider atomic properties PROPS as exclusive "
+	    << "events (implies -f)" << std::endl
 	    << "  -v    display the BDD variables used by the automaton"
 	    << std::endl
             << "  -x    try to produce a more deterministic automata "
@@ -193,6 +195,8 @@ main(int argc, char** argv)
   bool display_parity_game = false;
   bool post_branching = false;
   bool fair_loop_approx = false;
+  spot::ltl::environment& env(spot::ltl::default_environment::instance());
+  spot::ltl::atomic_prop_set* unobservables = 0;
 
   for (;;)
     {
@@ -470,6 +474,19 @@ main(int argc, char** argv)
 	  expect_counter_example = false;
 	  output = -1;
 	}
+      else if (!strncmp(argv[formula_index], "-U", 2))
+	{
+	  unobservables = new spot::ltl::atomic_prop_set;
+	  fm_opt = true;
+	  // Parse -U's argument.
+	  const char* tok = strtok(argv[formula_index] + 2, ",; \t");
+	  while (tok)
+	    {
+	      unobservables->insert
+		(static_cast<spot::ltl::atomic_prop*>(env.require(tok)));
+	      tok = strtok(0, ",; \t");
+	    }
+	}
       else if (!strcmp(argv[formula_index], "-v"))
 	{
 	  output = 5;
@@ -523,7 +540,6 @@ main(int argc, char** argv)
       input = argv[formula_index];
     }
 
-  spot::ltl::environment& env(spot::ltl::default_environment::instance());
   spot::bdd_dict* dict = new spot::bdd_dict();
 
   spot::ltl::formula* f = 0;
@@ -563,7 +579,7 @@ main(int argc, char** argv)
 	    to_free = a = spot::ltl_to_tgba_fm(f, dict, fm_exprop_opt,
 					       fm_symb_merge_opt,
 					       post_branching,
-					       fair_loop_approx);
+					       fair_loop_approx, unobservables);
 	  else
 	    to_free = a = concrete = spot::ltl_to_tgba_lacim(f, dict);
 	}