* src/ltlvisit/tostring.hh (to_spin_string): New function.

Convert a formula into a string parsable by Spin.
* src/tgbaalgos/neverclaim.hh, src/tgbaalgos/neverclaim.cc: New files.
Print the never claim in Spin format of a degeneralized TGBA.
* src/tgbaalgos/Makefile.am: Add them.
* src/tgbatest/ltl2tgba.cc: Add the option -N which outputs the
never claim in Spin format of a degeneralized TGBA.
* src/tgbatest/ltl2neverclaim.test: New file.
* src/tgbatest/Makefile.am: Add it.

ChangeLog

@@ -1,3 +1,15 @@
+2004-04-21  Denis Poitrenaud  <dp@src.lip6.fr>
+
+	* src/ltlvisit/tostring.hh (to_spin_string): New function.
+	Convert a formula into a string parsable by Spin.
+	* src/tgbaalgos/neverclaim.hh, src/tgbaalgos/neverclaim.cc: New files.
+	Print the never claim in Spin format of a degeneralized TGBA.
+	* src/tgbaalgos/Makefile.am: Add them.
+	* src/tgbatest/ltl2tgba.cc: Add the option -N which outputs the
+	never claim in Spin format of a degeneralized TGBA.
+	* src/tgbatest/ltl2neverclaim.test: New file.
+	* src/tgbatest/Makefile.am: Add it.
+
 2004-04-20  Alexandre Duret-Lutz  <adl@src.lip6.fr>
 
 	* src/ltltest/defs.in, src/tgbatest/defs.in: Correctly set exitcode

lbtt/src/ExternalTranslator.cc

@@ -108,6 +108,8 @@ void ExternalTranslator::translate
   string translated_formula;
   translateFormula(formula, translated_formula);
 
+  std::cout << translated_formula << std::endl;
+
   ofstream input_file;
   input_file.open(external_program_input_file.getName().c_str(),
 		  ios::out | ios::trunc);

src/ltlvisit/tostring.cc

@@ -147,7 +147,7 @@ namespace spot
 	  }
 	os_ << ")";
       }
-    private:
+    protected:
       std::ostream& os_;
     };
 
@@ -166,5 +166,139 @@ namespace spot
       to_string(f, os);
       return os.str();
     }
+
+    class to_spin_string_visitor : public to_string_visitor
+    {
+    public:
+    to_spin_string_visitor(std::ostream& os = std::cout)
+      : to_string_visitor(os)
+      {
+      }
+
+      virtual
+      ~to_spin_string_visitor()
+      {
+      }
+
+      void
+      visit(const binop* bo)
+      {
+	os_ << "(";
+
+	switch(bo->op())
+	  {
+	  case binop::Xor:
+	    os_ << "(!";
+	    bo->first()->accept(*this);
+	    os_ << " && ";
+	    bo->second()->accept(*this);
+	    os_ << ") || (";
+	    bo->first()->accept(*this);
+	    os_ << " && !";
+	    bo->second()->accept(*this);
+	    os_ << ")";
+	    break;
+	  case binop::Implies:
+	    os_ << "!";
+	    bo->first()->accept(*this);
+	    os_ << " || ";
+	    bo->second()->accept(*this);
+	    break;
+	  case binop::Equiv:
+	    os_ << "(";
+	    bo->first()->accept(*this);
+	    os_ << " && ";
+	    bo->second()->accept(*this);
+	    os_ << ") || (!";
+	    bo->first()->accept(*this);
+	    os_ << " && !";
+	    bo->second()->accept(*this);
+	    os_ << ")";
+	  case binop::U:
+	    bo->first()->accept(*this);
+	    os_ << " U ";
+	    bo->second()->accept(*this);
+	    break;
+	  case binop::R:
+	    bo->first()->accept(*this);
+	   os_ << " V ";
+	    bo->second()->accept(*this);
+	    break;
+	  }
+
+	os_ << ")";
+      }
+
+      void
+      visit(const unop* uo)
+      {
+	// The parser treats X0, and X1 as atomic propositions.	 So
+	// make sure we output X(0) and X(1).
+	bool need_parent = false;
+	switch(uo->op())
+	  {
+	  case unop::Not:
+	    os_ << "!";
+	    break;
+	  case unop::X:
+	    need_parent = !! dynamic_cast<const constant*>(uo->child());
+	    os_ << "X";
+	    break;
+	  case unop::F:
+	    os_ << "<>";
+	    break;
+	  case unop::G:
+	    os_ << "[]";
+	    break;
+	  }
+
+	if (need_parent)
+	  os_ << "(";
+	uo->child()->accept(*this);
+	if (need_parent)
+	  os_ << ")";
+      }
+
+      void
+      visit(const multop* mo)
+      {
+	os_ << "(";
+	unsigned max = mo->size();
+	mo->nth(0)->accept(*this);
+	const char* ch = " ";
+	switch (mo->op())
+	  {
+	  case multop::Or:
+	    ch = " || ";
+	    break;
+	  case multop::And:
+	    ch = " && ";
+	    break;
+	  }
+
+	for (unsigned n = 1; n < max; ++n)
+	  {
+	    os_ << ch;
+	    mo->nth(n)->accept(*this);
+	  }
+	os_ << ")";
+      }
+    };
+
+    std::ostream&
+    to_spin_string(const formula* f, std::ostream& os)
+    {
+      to_spin_string_visitor v(os);
+      f->accept(v);
+      return os;
+    }
+
+    std::string
+    to_spin_string(const formula* f)
+    {
+      std::ostringstream os;
+      to_spin_string(f, os);
+      return os.str();
+    }
   }
 }

src/ltlvisit/tostring.hh

@@ -37,6 +37,15 @@ namespace spot
     /// \brief Convert a formula into a (parsable) string.
     /// \param f The formula to translate.
     std::string to_string(const formula* f);
+
+    /// \brief Output a formula as a (parsable by Spin) string.
+    /// \param f The formula to translate.
+    /// \param os The stream where it should be output.
+    std::ostream& to_spin_string(const formula* f, std::ostream& os);
+
+    /// \brief Convert a formula into a (parsable by Spin) string.
+    /// \param f The formula to translate.
+    std::string to_spin_string(const formula* f);
   }
 }
 

src/tgbaalgos/Makefile.am

@@ -33,6 +33,7 @@ tgbaalgos_HEADERS = \
   ltl2tgba_fm.hh \
   ltl2tgba_lacim.hh \
   magic.hh \
+  neverclaim.hh \
   powerset.hh \
   reachiter.hh \
   save.hh \
@@ -46,6 +47,7 @@ libtgbaalgos_la_SOURCES = \
   ltl2tgba_fm.cc \
   ltl2tgba_lacim.cc \
   magic.cc \
+  neverclaim.cc \
   powerset.cc \
   reachiter.cc \
   save.cc \

src/tgbaalgos/neverclaim.cc

@@ -0,0 +1,177 @@
+// Copyright (C) 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+// département Systèmes Répartis Coopératifs (SRC), Université Pierre
+// et Marie Curie.
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 2 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+#include <sstream>
+#include "bdd.h"
+#include "tgba/tgbatba.hh"
+#include "neverclaim.hh"
+#include "tgba/bddprint.hh"
+#include "reachiter.hh"
+#include "ltlvisit/tostring.hh"
+#include "tgba/formula2bdd.hh"
+#include "ltlvisit/destroy.hh"
+
+namespace spot
+{
+
+  class never_claim_bfs : public tgba_reachable_iterator_breadth_first
+  {
+  public:
+    never_claim_bfs(const tgba_tba_proxy* a, std::ostream& os, const ltl::formula* f)
+      : tgba_reachable_iterator_breadth_first(a), os_(os), f_(f), accept_all_(-1), fi_needed_(false)
+    {
+    }
+
+    void
+    start()
+    {
+      os_ << "never {";
+      if (f_)
+        {
+          os_ << " /* ";
+          to_spin_string(f_, os_);
+          os_ << " */";
+        }
+      os_ << std::endl;
+      init_ = automata_->get_init_state();
+    }
+
+    void
+    end()
+    {
+      if (fi_needed_)
+        os_ << "  fi;" << std::endl;
+      if (accept_all_ != -1)
+        {
+          os_ << "accept_all :" << std::endl;
+          os_ << "  skip" << std::endl;
+        }
+      os_ << "}" << std::endl;
+      delete init_;
+    }
+
+    std::string
+    get_state_label(const state* s, int n)
+    {
+      std::string label;
+      if (s->compare(init_) == 0)
+        if (dynamic_cast<const tgba_tba_proxy*>(automata_)->state_is_accepting(s))
+          label = "accept_init";
+        else
+          label = "T0_init";
+      else
+        {
+          std::ostringstream ost;
+          ost << n;
+          std::string ns(ost.str());
+
+          if (dynamic_cast<const tgba_tba_proxy*>(automata_)->state_is_accepting(s))
+            {
+              tgba_succ_iterator* it = automata_->succ_iter(s);
+              it->first();
+              if (it->done())
+                label = "accept_S" + ns;
+              else
+                {
+                  state* current = it->current_state();
+                  if (it->current_condition() != bddtrue || s->compare(current) != 0)
+                    label = "accept_S" + ns;
+                  else
+                    label = "accept_all";
+                  delete current;
+                }
+              delete it;
+            }
+          else
+            label = "T0_S" + ns;
+        }
+        return label;
+    }
+
+    void
+    process_state(const state* s, int n, tgba_succ_iterator*)
+    {
+      tgba_succ_iterator* it = automata_->succ_iter(s);
+      it->first();
+      if (it->done())
+        {
+          if (fi_needed_ != 0)
+            os_ << "  fi;" << std::endl;
+          os_ << get_state_label(s, n) << " : ";
+          os_ << "/* " << automata_->format_state(s) << " */" ;
+          os_ << std::endl;
+          os_ << "  if" << std::endl;
+          os_ << "  :: (0) -> goto " << get_state_label(s, n) << std::endl;
+          fi_needed_ = true;
+        }
+      else
+        {
+          state* current =it->current_state();
+          if (dynamic_cast<const tgba_tba_proxy*>(automata_)->state_is_accepting(s) &&
+              (it->current_condition() == bddtrue) && s->compare(init_) != 0 &&
+              s->compare(current) == 0)
+            accept_all_ = n;
+          else
+            {
+              if (fi_needed_)
+                os_ << "  fi;" << std::endl;
+              os_ << get_state_label(s, n) << " : ";
+              os_ << "/* " << automata_->format_state(s) << " */";
+              os_ << std::endl;
+              os_ << "  if" << std::endl;
+              fi_needed_ = true;
+            }
+          delete current;
+        }
+        delete it;
+     }
+
+    void
+    process_link(int in, int out, const tgba_succ_iterator* si)
+    {
+      if (in != accept_all_)
+        {
+          os_ << "  :: (" ;
+          const ltl::formula* f = bdd_to_formula(si->current_condition(), automata_->get_dict());
+          to_spin_string(f, os_);
+          destroy(f);
+          state* current = si->current_state();
+          os_ << ") -> goto " << get_state_label(current, out) << std::endl;
+          delete current;
+        }
+    }
+
+  private:
+    std::ostream& os_;
+    const ltl::formula* f_;
+    int accept_all_;
+    bool fi_needed_;
+    state* init_;
+  };
+
+  std::ostream&
+  never_claim_reachable(std::ostream& os, const tgba_tba_proxy* g, const ltl::formula* f)
+  {
+    never_claim_bfs n(g, os, f);
+    n.run();
+    return os;
+  }
+}

src/tgbaalgos/neverclaim.hh

@@ -0,0 +1,35 @@
+// Copyright (C) 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+// département Systèmes Répartis Coopératifs (SRC), Université Pierre
+// et Marie Curie.
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 2 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+#ifndef SPOT_TGBAALGOS_NEVERCLAIM_HH
+# define SPOT_TGBAALGOS_NEVERCLAIM_HH
+
+#include <iostream>
+#include "ltlast/formula.hh"
+#include "tgba/tgbatba.hh"
+
+namespace spot
+{
+  /// \brief Print reachable states in Spin never claim format.
+  std::ostream& never_claim_reachable(std::ostream& os, const tgba_tba_proxy* g, const ltl::formula* f=0);
+}
+
+#endif // SPOT_TGBAALGOS_NEVERCLAIM_HH

src/tgbatest/Makefile.am

@@ -60,6 +60,7 @@ TESTS = \
   tgbaread.test \
   readsave.test \
   ltl2tgba.test \
+  ltl2neverclaim.test \
   ltlprod.test \
   bddprod.test \
   explprod.test \

src/tgbatest/ltl2neverclaim.test

@@ -0,0 +1,41 @@
+#!/bin/sh
+# Copyright (C) 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+# département Systèmes Répartis Coopératifs (SRC), Université Pierre
+# et Marie Curie.
+#
+# This file is part of Spot, a model checking library.
+#
+# Spot is free software; you can redistribute it and/or modify it
+# under the terms of the GNU General Public License as published by
+# the Free Software Foundation; either version 2 of the License, or
+# (at your option) any later version.
+#
+# Spot is distributed in the hope that it will be useful, but WITHOUT
+# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+# or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+# License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with Spot; see the file COPYING.  If not, write to the Free
+# Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+# 02111-1307, USA.
+
+
+. ./defs
+
+set -e
+
+# We don't check the output, but just running these might be enough to
+# trigger assertions.
+
+run 0 ./ltl2tgba -N -x a
+run 0 ./ltl2tgba -N -x  'a U b'
+run 0 ./ltl2tgba -N -x 'X a'
+run 0 ./ltl2tgba -N -x 'a & b & c'
+run 0 ./ltl2tgba -N -x 'a | b | (c U (d & (g U (h ^ i))))'
+run 0 ./ltl2tgba -N -x 'Xa & (b U !a) & (b U !a)'
+run 0 ./ltl2tgba -N -x 'Fa & Xb & GFc & Gd'
+run 0 ./ltl2tgba -N -x 'Fa & Xa & GFc & Gc'
+run 0 ./ltl2tgba -N -x 'Fc & X(a | Xb) & GF(a | Xb) & Gc'
+run 0 ./ltl2tgba -N -x 'a R (b R c)'
+run 0 ./ltl2tgba -N -x '(a U b) U (c U d)'

src/tgbatest/ltl2tgba.cc

@@ -37,6 +37,7 @@
 #include "tgbaalgos/gtec/ce.hh"
 #include "tgbaparse/public.hh"
 #include "tgbaalgos/dupexp.hh"
+#include "tgbaalgos/neverclaim.hh"
 
 void
 syntax(char* prog)
@@ -69,6 +70,8 @@ syntax(char* prog)
 	    << std::endl
 	    << "  -n   same as -m, but display more counter-examples"
 	    << std::endl
+	    << "  -N   display the never clain for Spin "
+	    << "(implies -D)" << std::endl
 	    << "  -r   display the relation BDD, not the reachability graph"
 	    << std::endl
 	    << "  -R   same as -r, but as a set" << std::endl
@@ -186,6 +189,11 @@ main(int argc, char** argv)
 	  output = -1;
 	  magic_many = true;
 	}
+      else if (!strcmp(argv[formula_index], "-N"))
+	{
+	  degeneralize_opt = true;
+	  output = 8;
+	}
       else if (!strcmp(argv[formula_index], "-r"))
 	{
 	  output = 1;
@@ -295,7 +303,6 @@ main(int argc, char** argv)
 					       fm_symb_merge_opt);
 	  else
 	    to_free = a = concrete = spot::ltl_to_tgba_lacim(f, dict);
-	  spot::ltl::destroy(f);
 	}
 
       spot::tgba_tba_proxy* degeneralized = 0;
@@ -354,6 +361,9 @@ main(int argc, char** argv)
 	case 7:
 	  spot::nonacceptant_lbtt_reachable(std::cout, a);
 	  break;
+	case 8:
+	  spot::never_claim_reachable(std::cout, degeneralized, f);
+	  break;
 	default:
 	  assert(!"unknown output option");
 	}
@@ -414,6 +424,8 @@ main(int argc, char** argv)
 	  break;
 	}
 
+      if (f)
+        spot::ltl::destroy(f);
       if (expl)
 	delete expl;
       if (degeneralize_opt)

src/tgbatest/spotlbtt.test

@@ -70,6 +70,13 @@ Algorithm
    Enabled = yes
 }
 
+Algorithm
+{
+   Name = "Spot (Couvreur -- FM), degeneralized, via never claim"
+   Path = "${LBTT_TRANSLATE} --spin './ltl2tgba -F -f -N'"
+   Enabled = yes
+}
+
 Algorithm
 {
    Name = "Spot (Couvreur -- FM), fake"
@@ -257,7 +264,7 @@ FormulaOptions
 
   AndPriority = 10
   OrPriority = 10
-  # XorPriority = 0
+  XorPriority = 0
   # EquivalencePriority = 0
 
   BeforePriority = 0