* src/tgba/tgbatba.hh, src/tgba/tgbatba.cc

(tgba_tba_proxy::state_is_accepting): New method.
* src/tgbaalgos/magic.hh, src/tgbaalgos/magic.cc: New files.
* src/tgbaalgos/Makefile.am (libtgbaalgos_la_SOURCES,
tgbaalgos_HEADERS): Add them.
* src/tgbatest/ltlmagic.cc, src/tgbatest/ltlmagic.test: New files.
* src/tgbatest/Makefile.am (TESTS, ltlmagic_SOURCES,
check_PROGRAMS): Add them.

ChangeLog

@@ -1,3 +1,14 @@
+2003-07-28  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
+
+	* src/tgba/tgbatba.hh, src/tgba/tgbatba.cc
+	(tgba_tba_proxy::state_is_accepting): New method.
+	* src/tgbaalgos/magic.hh, src/tgbaalgos/magic.cc: New files.
+	* src/tgbaalgos/Makefile.am (libtgbaalgos_la_SOURCES,
+	tgbaalgos_HEADERS): Add them.
+	* src/tgbatest/ltlmagic.cc, src/tgbatest/ltlmagic.test: New files.
+	* src/tgbatest/Makefile.am (TESTS, ltlmagic_SOURCES,
+	check_PROGRAMS): Add them.
+
 2003-07-25  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
 
 	* src/tgba/tgba.hh (tgba::~tgba): Make it public.

src/tgba/tgbatba.cc

@@ -27,7 +27,7 @@ namespace spot
     {
     }
 
-    virtual 
+    virtual
     ~state_tba_proxy()
     {
       delete s_;
@@ -45,7 +45,7 @@ namespace spot
       return acc_;
     }
 
-    virtual int 
+    virtual int
     compare(const state* other) const
     {
       const state_tba_proxy* o = dynamic_cast<const state_tba_proxy*>(other);
@@ -55,8 +55,8 @@ namespace spot
 	return res;
       return acc_.id() - o->accepting_cond().id();
     }
-    
-    virtual 
+
+    virtual
     state_tba_proxy* clone() const
     {
       return new state_tba_proxy(*this);
@@ -75,7 +75,7 @@ namespace spot
     tgba_tba_proxy_succ_iterator(tgba_succ_iterator* it,
 				 bdd acc, bdd next_acc,
 				 bdd the_accepting_cond)
-      : it_(it), acc_(acc), next_acc_(next_acc), 
+      : it_(it), acc_(acc), next_acc_(next_acc),
 	the_accepting_cond_(the_accepting_cond)
     {
     }
@@ -87,19 +87,19 @@ namespace spot
 
     // iteration
 
-    void 
+    void
     first()
     {
       it_->first();
     }
 
-    void 
+    void
     next()
     {
       it_->next();
     }
 
-    bool 
+    bool
     done() const
     {
       return it_->done();
@@ -107,14 +107,14 @@ namespace spot
 
     // inspection
 
-    state_tba_proxy* 
+    state_tba_proxy*
     current_state() const
     {
       state* s = it_->current_state();
       bdd acc;
       // Transition in the ACC_ accepting set should be directed
       // to the NEXT_ACC_ accepting set.
-      if (acc_ == bddtrue 
+      if (acc_ == bddtrue
 	  || (acc_ & it_->current_accepting_conditions()) == acc_)
 	acc = next_acc_;
       else
@@ -122,13 +122,13 @@ namespace spot
       return new state_tba_proxy(s, acc);
     }
 
-    bdd 
+    bdd
     current_condition() const
     {
       return it_->current_condition();
     }
 
-    bdd 
+    bdd
     current_accepting_conditions() const
     {
       return the_accepting_cond_;
@@ -176,7 +176,7 @@ namespace spot
     get_dict()->unregister_all_my_variables(this);
   }
 
-  state* 
+  state*
   tgba_tba_proxy::get_init_state() const
   {
     cycle_map::const_iterator i = acc_cycle_.find(bddtrue);
@@ -189,62 +189,71 @@ namespace spot
 			    const state* global_state,
 			    const tgba* global_automaton) const
   {
-    const state_tba_proxy* s = 
+    const state_tba_proxy* s =
       dynamic_cast<const state_tba_proxy*>(local_state);
     assert(s);
 
-    tgba_succ_iterator* it = a_->succ_iter(s->real_state(), 
+    tgba_succ_iterator* it = a_->succ_iter(s->real_state(),
 					   global_state, global_automaton);
     bdd acc = s->accepting_cond();
     cycle_map::const_iterator i = acc_cycle_.find(acc);
     assert(i != acc_cycle_.end());
-    return 
+    return
       new tgba_tba_proxy_succ_iterator(it, acc, i->second,
-				       (acc == bddtrue) 
+				       (acc == bddtrue)
 				       ? the_accepting_cond_ : bddfalse);
   }
-  
-  bdd_dict* 
+
+  bdd_dict*
   tgba_tba_proxy::get_dict() const
   {
     return a_->get_dict();
   }
-  
-  std::string 
+
+  std::string
   tgba_tba_proxy::format_state(const state* state) const
   {
-    const state_tba_proxy* s = 
+    const state_tba_proxy* s =
       dynamic_cast<const state_tba_proxy*>(state);
     assert(s);
-    return a_->format_state(s->real_state()) + "(" 
+    return a_->format_state(s->real_state()) + "("
       + bdd_format_set(get_dict(), s->accepting_cond()) + ")";
   }
-  
-  bdd 
+
+  bdd
   tgba_tba_proxy::all_accepting_conditions() const
   {
     return the_accepting_cond_;
   }
-  
-  bdd 
+
+  bdd
   tgba_tba_proxy::neg_accepting_conditions() const
   {
     return !the_accepting_cond_;
   }
-  
-  bdd 
+
+  bool
+  tgba_tba_proxy::state_is_accepting(const state* state) const
+  {
+    const state_tba_proxy* s =
+      dynamic_cast<const state_tba_proxy*>(state);
+    assert(s);
+    return bddtrue == s->accepting_cond();
+  }
+
+  bdd
   tgba_tba_proxy::compute_support_conditions(const state* state) const
   {
-    const state_tba_proxy* s = 
+    const state_tba_proxy* s =
       dynamic_cast<const state_tba_proxy*>(state);
     assert(s);
     return a_->support_conditions(s->real_state());
   }
-  
-  bdd 
+
+  bdd
   tgba_tba_proxy::compute_support_variables(const state* state) const
   {
-    const state_tba_proxy* s = 
+    const state_tba_proxy* s =
       dynamic_cast<const state_tba_proxy*>(state);
     assert(s);
     return a_->support_variables(s->real_state());

src/tgba/tgbatba.hh

@@ -44,6 +44,8 @@ namespace spot
     virtual bdd all_accepting_conditions() const;
     virtual bdd neg_accepting_conditions() const;
 
+    bool state_is_accepting(const state* state) const;
+
   protected:
     virtual bdd compute_support_conditions(const state* state) const;
     virtual bdd compute_support_variables(const state* state) const;

src/tgbaalgos/Makefile.am

@@ -8,6 +8,7 @@ tgbaalgos_HEADERS = \
   dotty.hh \
   lbtt.hh \
   ltl2tgba.hh \
+  magic.hh \
   save.hh
 
 noinst_LTLIBRARIES = libtgbaalgos.la
@@ -16,4 +17,5 @@ libtgbaalgos_la_SOURCES = \
   dotty.cc \
   lbtt.cc \
   ltl2tgba.cc \
+  magic.cc \
   save.cc

src/tgbaalgos/magic.cc

@@ -0,0 +1,143 @@
+#include <iterator>
+#include "magic.hh"
+#include "tgba/bddprint.hh"
+
+namespace spot
+{
+
+  const unsigned char seen_without_magic = 1;
+  const unsigned char seen_with_magic = 2;
+
+  magic_search::magic_search(const tgba_tba_proxy* a)
+    : a(a), x(0)
+  {
+  }
+
+  magic_search::~magic_search()
+  {
+    for (hash_type::iterator i = h.begin(); i != h.end(); ++i)
+      delete i->first;
+    if (x)
+      delete x;
+  }
+
+  void
+  magic_search::push(const state* s, bool m)
+  {
+    tgba_succ_iterator* i = a->succ_iter(s);
+    i->first();
+
+    hash_type::iterator hi = h.find(s);
+    if (hi == h.end())
+      {
+	magic d = { !m, m };
+	h[s] = d;
+      }
+    else
+      {
+	hi->second.seen_without |= !m;
+	hi->second.seen_with |= m;
+	if (hi->first != s)
+	  delete s;
+	s = hi->first;
+      }
+
+    magic_state ms = { s, m };
+    stack.push_front(state_iter_pair(ms, i));
+  }
+
+  bool
+  magic_search::has(const state* s, bool m) const
+  {
+    hash_type::const_iterator i = h.find(s);
+    if (i == h.end())
+      return false;
+    if (!m && i->second.seen_without)
+      return true;
+    if (m && i->second.seen_with)
+      return true;
+    return false;
+  }
+
+  bool
+  magic_search::check()
+  {
+    if (stack.empty())
+      // It's a new search.
+      push(a->get_init_state(), false);
+    else
+      // Remove the transition to the cycle root.
+      tstack.pop_front();
+
+    assert(stack.size() == 1 + tstack.size());
+
+    while (! stack.empty())
+      {
+      recurse:
+	magic_search::state_iter_pair& p = stack.front();
+	tgba_succ_iterator* i = p.second;
+	const bool magic = p.first.m;
+
+	while (! i->done())
+	  {
+	    const state* s_prime = i->current_state();
+	    bdd c = i->current_condition();
+	    i->next();
+	    if (magic && 0 == s_prime->compare(x))
+	      {
+		delete s_prime;
+		tstack.push_front(c);
+		assert(stack.size() == tstack.size());
+		return true;
+	      }
+	    if (! has(s_prime, magic))
+	      {
+		push(s_prime, magic);
+		tstack.push_front(c);
+		goto recurse;
+	      }
+	    delete s_prime;
+	  }
+
+	const state* s = p.first.s;
+	stack.pop_front();
+
+	if (! magic && a->state_is_accepting(s))
+	  {
+	    if (! has(s, true))
+	      {
+		if (x)
+		  delete x;
+		x = s->clone();
+		push(s, true);
+		continue;
+	      }
+	  }
+	if (! stack.empty())
+	  tstack.pop_front();
+      }
+
+    assert(tstack.empty());
+    return false;
+  }
+
+  std::ostream&
+  magic_search::print_result(std::ostream& os) const
+  {
+    stack_type::const_reverse_iterator i;
+    tstack_type::const_reverse_iterator ti;
+    os << "Prefix:" << std::endl;
+    const bdd_dict* d = a->get_dict();
+    for (i = stack.rbegin(), ti = tstack.rbegin(); 
+	 i != stack.rend(); ++i, ++ti)
+      {
+	if (i->first.s->compare(x) == 0)
+	  os <<"Cycle:" <<std::endl;
+	os << "  " << a->format_state(i->first.s) << std::endl;
+	os << "    | " << bdd_format_set(d, *ti) << std::endl;
+      }
+    os << "  " << a->format_state(x) << std::endl;
+    return os;
+  }
+
+}

src/tgbaalgos/magic.hh

@@ -0,0 +1,98 @@
+#ifndef SPOT_TGBAALGOS_MAGIC_HH
+# define SPOT_TGBAALGOS_MAGIC_HH
+
+#include <list>
+#include <utility>
+#include <ostream>
+#include "tgba/tgbatba.hh"
+
+namespace spot
+{
+  /// \brief Emptiness check on spot::tgba_tba_proxy automata using
+  /// the Magic Search algorithm. 
+  ///
+  /// This algorithm comes from
+  /// \verbatim
+  /// @InProceedings{   godefroid.93.pstv,
+  ///   author        = {Patrice Godefroid and Gerard .J. Holzmann},
+  ///   title         = {On the verification of temporal properties},
+  ///   booktitle     = {Proceedings of the 13th IFIP TC6/WG6.1 International
+  ///                   Symposium on Protocol Specification, Testing, and
+  ///                   Verification (PSTV'93)},
+  ///   month         = {May},
+  ///   editor        = {Andr{\'e} A. S. Danthine and Guy Leduc
+  ///                    and Pierre Wolper},
+  ///   address       = {Liege, Belgium},
+  ///   pages         = {109--124},
+  ///   publisher     = {North-Holland},
+  ///   year          = {1993},
+  ///   series        = {IFIP Transactions},
+  ///   volume        = {C-16},
+  ///   isbn          = {0-444-81648-8}
+  /// }
+  /// \endverbatim
+  struct magic_search
+  {
+    /// Initialize the Magic Search algorithm on the automaton \a a.
+    magic_search(const tgba_tba_proxy *a);
+    ~magic_search();
+
+    /// \brief Perform a Magic Search.
+    /// 
+    /// \return true iff the algorithm has found a new accepting
+    ///    path.
+    ///
+    /// check() can be called several times until it return false,
+    /// to enumerate all accepting paths.
+    bool check();
+
+    /// Print the last accepting path found.
+    std::ostream& print_result(std::ostream& os) const;
+
+  private:
+
+    // The names "stack", "h", and "x", are those used in the paper.
+
+    /// \brief  Records whether a state has be seen with the magic bit
+    /// on or off.
+    struct magic
+    {
+      bool seen_without : 1;
+      bool seen_with    : 1;
+    };
+    
+    /// \brief A state for the spot::magic_search algorithm.
+    struct magic_state
+    {
+      const state* s;
+      bool m;			///< The state of the magic demon.
+    };
+
+    typedef std::pair<magic_state, tgba_succ_iterator*> state_iter_pair;
+    typedef std::list<state_iter_pair> stack_type;
+    stack_type stack;		///< Stack of visited states on the path.
+
+    typedef std::list<bdd> tstack_type;
+    /// \brief Stack of transitions.  
+    ///
+    /// This is an addition to the data from the paper.
+    tstack_type tstack;
+
+    // FIXME: use a hash_map.
+    typedef std::map<const state*, magic, state_ptr_less_than> hash_type;
+    hash_type h;		///< Map of visited states.
+
+    /// Append a new state to the current path.
+    void push(const state* s, bool m);
+    /// Check whether we already visited \a s with the Magic bit set to \a m.
+    bool has(const state* s, bool m) const;
+
+    const tgba_tba_proxy* a;	///< The automata to check.
+    /// The state for which we are currently seeking an SCC.
+    const state* x;		
+  };
+
+
+}
+
+#endif // SPOT_TGBAALGOS_MAGIC_HH

src/tgbatest/.cvsignore

@@ -15,3 +15,4 @@ explprod
 tripprod
 mixprod
 spotlbtt
+ltlmagic

src/tgbatest/Makefile.am

@@ -4,16 +4,17 @@ LDADD = ../libspot.la
 check_SCRIPTS = defs
 # Keep this sorted alphabetically.
 check_PROGRAMS = \
-  explicit \
-  readsave \
-  tgbaread \
-  ltl2tgba \
-  ltlprod \
   bddprod \
+  explicit \
   explprod \
-  tripprod \
+  ltl2tgba \
+  ltlmagic \
+  ltlprod \
   mixprod \
-  spotlbtt
+  readsave \
+  spotlbtt \
+  tgbaread \
+  tripprod
 
 # Keep this sorted alphabetically.
 bddprod_SOURCES  = ltlprod.cc
@@ -21,6 +22,7 @@ bddprod_CXXFLAGS = -DBDD_CONCRETE_PRODUCT
 explicit_SOURCES = explicit.cc
 explprod_SOURCES = explprod.cc
 ltl2tgba_SOURCES = ltl2tgba.cc
+ltlmagic_SOURCES = ltlmagic.cc
 ltlprod_SOURCES  = ltlprod.cc
 mixprod_SOURCES  = mixprod.cc
 readsave_SOURCES = readsave.cc
@@ -40,7 +42,8 @@ TESTS = \
   explprod.test \
   tripprod.test \
   mixprod.test \
-  spotlbtt.test
+  spotlbtt.test \
+  ltlmagic.test
 
 EXTRA_DIST = $(TESTS)
 

src/tgbatest/ltlmagic.cc

@@ -0,0 +1,77 @@
+#include <iostream>
+#include <cassert>
+#include "ltlvisit/destroy.hh"
+#include "ltlast/allnodes.hh"
+#include "ltlparse/public.hh"
+#include "tgbaalgos/ltl2tgba.hh"
+#include "tgbaalgos/magic.hh"
+
+void
+syntax(char* prog)
+{
+  std::cerr << prog << " formula" << std::endl;
+  exit(2);
+}
+
+int
+main(int argc, char** argv)
+{
+  int exit_code = 0;
+  int formula_index = 0;
+  bool all_opt = false;
+
+  for (;;)
+    {
+      if (argc < formula_index + 1)
+	syntax(argv[0]);
+
+      ++formula_index;
+
+      if (!strcmp(argv[formula_index], "-a"))
+	{
+	  all_opt = true;
+	}
+      else
+	{
+	  break;
+	}
+    }
+
+  spot::ltl::environment& env(spot::ltl::default_environment::instance());
+
+  spot::ltl::parse_error_list pel1;
+  spot::ltl::formula* f1 = spot::ltl::parse(argv[formula_index], pel1, env);
+
+  if (spot::ltl::format_parse_errors(std::cerr, argv[formula_index], pel1))
+    return 2;
+
+  spot::bdd_dict* dict = new spot::bdd_dict();
+  {
+    spot::tgba_bdd_concrete* a1 = spot::ltl_to_tgba(f1, dict);
+    spot::tgba_tba_proxy* a2 = new spot::tgba_tba_proxy(a1);
+    spot::ltl::destroy(f1);
+
+    spot::magic_search ms(a2);
+    
+    if (ms.check())
+      {
+	do 
+	  ms.print_result (std::cout);
+	while (all_opt && ms.check());
+      }
+    else
+      {
+	exit_code = 1;
+      }
+
+    delete a2;
+    delete a1;
+  }
+
+  assert(spot::ltl::atomic_prop::instance_count() == 0);
+  assert(spot::ltl::unop::instance_count() == 0);
+  assert(spot::ltl::binop::instance_count() == 0);
+  assert(spot::ltl::multop::instance_count() == 0);
+  delete dict;
+  return exit_code;
+}

src/tgbatest/ltlmagic.test

@@ -0,0 +1,15 @@
+#!/bin/sh
+
+. ./defs
+
+set -e
+
+./ltlmagic a
+./ltlmagic 0 || test $? = 1
+./ltlmagic 'a & !a' || test $? = 1
+./ltlmagic 'a U b'
+./ltlmagic '!(a U b)'
+./ltlmagic '!(a U b) & !(!a R !b)' || test $? = 1
+# Expect four satisfactions
+test `./ltlmagic -a 'FFx <=> Fx' | grep Prefix: | wc -l` = 4
+./ltlmagic '!(FFx <=> Fx)'  || test $? = 1