Add support for W (weak until) and M (strong release) operators.

* src/ltlast/binop.cc, src/ltlast/binop.cc: Add support for
these new operators.
* src/ltlparse/ltlparse.yy, src/ltlparse/ltlscan.ll: Parse them.
* src/ltltest/reduccmp.test: Add new tests for W and M.
* src/ltlvisit/basicreduce.cc, src/ltlvisit/contain.cc,
src/ltlvisit/lunabbrev.cc, src/ltlvisit/nenoform.cc,
src/ltlvisit/randomltl.cc, src/ltlvisit/randomltl.hh,
src/ltlvisit/reduce.cc, src/ltlvisite/simpfg.cc,
src/ltlvisit/simpfg.hh, src/ltlvisit/syntimpl.cc,
src/ltlvisit/tostring.cc, src/tgba/formula2bdd.cc,
src/tgbaalgos/eltl2tgba_lacim.cc, src/tgbaalgos/ltl2taa.cc,
src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/ltl2tgba_lacim.cc:
Add support for W and M.
* src/tgbatest/ltl2neverclaim.test: Test never claim output
using LBTT, this is more thorough.  Also we cannot use -N
any more in the spotlbtt.test.
* src/tgbatests/ltl2tgba.cc: Define M and W for ELTL.
* src/tgbatest/ltl2neverclaim.test: Test W and M, and use
-DS instead of -N, because lbtt-translate does not want
to translate these operators for tools that masquerade as Spin.

ChangeLog

@@ -1,3 +1,28 @@
+2010-04-07  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	Add support for W (weak until) and M (strong release) operators.
+
+	* src/ltlast/binop.cc, src/ltlast/binop.cc: Add support for
+	these new operators.
+	* src/ltlparse/ltlparse.yy, src/ltlparse/ltlscan.ll: Parse them.
+	* src/ltltest/reduccmp.test: Add new tests for W and M.
+	* src/ltlvisit/basicreduce.cc, src/ltlvisit/contain.cc,
+	src/ltlvisit/lunabbrev.cc, src/ltlvisit/nenoform.cc,
+	src/ltlvisit/randomltl.cc, src/ltlvisit/randomltl.hh,
+	src/ltlvisit/reduce.cc, src/ltlvisite/simpfg.cc,
+	src/ltlvisit/simpfg.hh, src/ltlvisit/syntimpl.cc,
+	src/ltlvisit/tostring.cc, src/tgba/formula2bdd.cc,
+	src/tgbaalgos/eltl2tgba_lacim.cc, src/tgbaalgos/ltl2taa.cc,
+	src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/ltl2tgba_lacim.cc:
+	Add support for W and M.
+	* src/tgbatest/ltl2neverclaim.test: Test never claim output
+	using LBTT, this is more thorough.  Also we cannot use -N
+	any more in the spotlbtt.test.
+	* src/tgbatests/ltl2tgba.cc: Define M and W for ELTL.
+	* src/tgbatest/ltl2neverclaim.test: Test W and M, and use
+	-DS instead of -N, because lbtt-translate does not want
+	to translate these operators for tools that masquerade as Spin.
+
 2010-04-12  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
 
 	Adjust ltl2tgba.py to call scc_filter() with the "full" option as

src/ltlast/binop.cc

@@ -1,4 +1,4 @@
-// Copyright (C) 2009 Laboratoire de Recherche et Développement
+// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 // Copyright (C) 2003, 2005 Laboratoire d'Informatique de Paris
 // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
@@ -115,6 +115,10 @@ namespace spot
 	  return "U";
 	case R:
 	  return "R";
+	case W:
+	  return "W";
+	case M:
+	  return "M";
 	}
       // Unreachable code.
       assert(0);
@@ -126,7 +130,7 @@ namespace spot
     binop*
     binop::instance(type op, formula* first, formula* second)
     {
-      // Sort the operands of associative operators, so that for
+      // Sort the operands of commutative operators, so that for
       // example the formula instance for 'a xor b' is the same as
       // that for 'b xor a'.
       switch (op)
@@ -139,7 +143,9 @@ namespace spot
 	case Implies:
 	case U:
 	case R:
-	  // Non associative operators.
+	case W:
+	case M:
+	  // Non commutative operators.
 	  break;
 	}
 

src/ltlast/binop.hh

@@ -1,4 +1,4 @@
-// Copyright (C) 2009 Laboratoire de Recherche et Développement
+// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris
 // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
@@ -47,7 +47,14 @@ namespace spot
       ///
       /// And and Or are not here.  Because they
       /// are often nested we represent them as multops.
-      enum type { Xor, Implies, Equiv, U, R };
+      enum type { Xor,
+		  Implies,
+		  Equiv,
+		  U, //< until
+		  R, //< release (dual of until)
+		  W, //< weak until
+		  M  //< strong release (dual of weak until)
+      };
 
       /// Build an unary operator with operation \a op and
       /// children \a first and \a second.

src/ltlparse/ltlparse.yy

@@ -79,6 +79,7 @@ using namespace spot::ltl;
 %token OP_OR "or operator" OP_XOR "xor operator" OP_AND "and operator"
 %token OP_IMPLIES "implication operator" OP_EQUIV "equivalent operator"
 %token OP_U "until operator" OP_R "release operator"
+%token OP_W "weak until operator" OP_M "strong release operator"
 %token OP_F "sometimes operator" OP_G "always operator"
 %token OP_X "next operator" OP_NOT "not operator"
 %token <str> ATOMIC_PROP "atomic proposition"
@@ -95,7 +96,7 @@ using namespace spot::ltl;
 %left OP_AND
 
 /* LTL operators.  */
-%left OP_U OP_R
+%left OP_U OP_R OP_M OP_W
 %nonassoc OP_F OP_G
 %nonassoc OP_X
 
@@ -239,6 +240,14 @@ subformula: ATOMIC_PROP
 	      { $$ = binop::instance(binop::R, $1, $3); }
 	    | subformula OP_R error
 	      { missing_right_binop($$, $1, @2, "release operator"); }
+	    | subformula OP_W subformula
+	      { $$ = binop::instance(binop::W, $1, $3); }
+	    | subformula OP_W error
+	      { missing_right_binop($$, $1, @2, "weak until operator"); }
+	    | subformula OP_M subformula
+	      { $$ = binop::instance(binop::M, $1, $3); }
+	    | subformula OP_M error
+	      { missing_right_binop($$, $1, @2, "strong release operator"); }
 	    | OP_F subformula
 	      { $$ = unop::instance(unop::F, $2); }
 	    | OP_F error

src/ltlparse/ltlscan.ll

@@ -90,6 +90,8 @@ flex_set_buffer(const char* buf)
 "U"				BEGIN(0); return token::OP_U;
 "R"|"V"				BEGIN(0); return token::OP_R;
 "X"|"()"			BEGIN(0); return token::OP_X;
+"W"				BEGIN(0); return token::OP_W;
+"M"				BEGIN(0); return token::OP_M;
 
 "=0"				return token::OP_POST_NEG;
 "=1"				return token::OP_POST_POS;

src/ltltest/reduccmp.test

@@ -40,16 +40,26 @@ for x in ../reduccmp ../reductaustr; do
   # Syntactic reduction
   run 0 $x 'a & (!b R !a)' 'false'
   run 0 $x '(!b R !a) & a' 'false'
-
   run 0 $x 'a & (!b R !a) & c' 'false'
   run 0 $x 'c & (!b R !a) & a' 'false'
 
+  run 0 $x 'a & (!b M !a)' 'false'
+  run 0 $x '(!b M !a) & a' 'false'
+  run 0 $x 'a & (!b M !a) & c' 'false'
+  run 0 $x 'c & (!b M !a) & a' 'false'
+
   run 0 $x 'a & (b U a)' 'a'
   run 0 $x '(b U a) & a' 'a'
   run 0 $x 'a | (b U a)' '(b U a)'
   run 0 $x '(b U a) | a' '(b U a)'
   run 0 $x 'a U (b U a)' '(b U a)'
 
+  run 0 $x 'a & (b W a)' 'a'
+  run 0 $x '(b W a) & a' 'a'
+  run 0 $x 'a | (b W a)' '(b W a)'
+  run 0 $x '(b W a) | a' '(b W a)'
+  run 0 $x 'a W (b W a)' '(b W a)'
+
   run 0 $x 'a & (b U a) & a' 'a'
   run 0 $x 'a & (b U a) & a' 'a'
   run 0 $x 'a | (b U a) | a' '(b U a)'
@@ -101,6 +111,9 @@ for x in ../reduccmp ../reductaustr; do
      # reason as above.
      run 0 $x 'F(a & GFb & c)' 'F(a & GFb & c)'
      run 0 $x 'G(a | GFb | c)' 'G(a | c) | GFb'
+
+     run 0 $x 'Gb W a' 'Gb|a'
+     run 0 $x 'Fb M Fa' 'Fa & Fb'
      ;;
   esac
 
@@ -113,5 +126,4 @@ for x in ../reduccmp ../reductaustr; do
   run 0 $x 'GFGa' 'FGa'
   run 0 $x 'b R Ga' 'Ga'
   run 0 $x 'b R FGa' 'FGa'
-
 done

src/ltlvisit/basicreduce.cc

@@ -253,7 +253,8 @@ namespace spot
 	  formula* f2 = bo->second();
 	  unop* fu1;
 	  unop* fu2;
-	  switch (bo->op())
+	  binop::type op = bo->op();
+	  switch (op)
 	    {
 	    case binop::Xor:
 	    case binop::Equiv:
@@ -262,31 +263,49 @@ namespace spot
 					basic_reduce(f1),
 					basic_reduce(f2));
 	      return;
+	    case binop::W:
+	    case binop::M:
 	    case binop::U:
 	    case binop::R:
+	      f1 = basic_reduce(f1);
 	      f2 = basic_reduce(f2);
 
+	      // a W false = Ga
+	      if (op == binop::W && f2 == constant::false_instance())
+		{
+		  result_ = unop::instance(unop::G, f1);
+		  return;
+		}
+	      // a M true = Fa
+	      if (op == binop::M && f2 == constant::true_instance())
+		{
+		  result_ = unop::instance(unop::F, f1);
+		  return;
+		}
 	      // a U false = false
 	      // a U true = true
 	      // a R false = false
 	      // a R true = true
+	      // a W true = true
+	      // a M false = false
 	      if (dynamic_cast<constant*>(f2))
 		{
 		  result_ = f2;
+		  f1->destroy();
 		  return;
 		}
 
-	      f1 = basic_reduce(f1);
-
 	      // X(a) U X(b) = X(a U b)
 	      // X(a) R X(b) = X(a R b)
+	      // X(a) W X(b) = X(a W b)
+	      // X(a) M X(b) = X(a M b)
 	      fu1 = dynamic_cast<unop*>(f1);
 	      fu2 = dynamic_cast<unop*>(f2);
 	      if (fu1 && fu2
 		  && fu1->op() == unop::X
 		  && fu2->op() == unop::X)
 		{
-		  formula* ftmp = binop::instance(bo->op(),
+		  formula* ftmp = binop::instance(op,
 						  basic_reduce(fu1->child()),
 						  basic_reduce(fu2->child()));
 		  result_ = unop::instance(unop::X, basic_reduce(ftmp));
@@ -296,7 +315,7 @@ namespace spot
 		  return;
 	      }
 
-	      result_ = binop::instance(bo->op(), f1, f2);
+	      result_ = binop::instance(op, f1, f2);
 	      return;
 	    }
 	  /* Unreachable code.  */

src/ltlvisit/contain.cc

@@ -1,4 +1,4 @@
-// Copyright (C) 2009 Laboratoire de Recherche et Développement
+// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 // Copyright (C) 2006, 2007 Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -202,6 +202,31 @@ namespace spot
 		  result_ = binop::instance(binop::U, a, b);
 		}
 	      break;
+	    case binop::W:
+	      // if (a W b) => b, then keep b !
+	      if (stronger && lcc->contained(bo, b))
+		{
+		  a->destroy();
+		  result_ = b;
+		}
+	      // if a => b,  then a W b = b.
+	      else if ((!stronger) && lcc->contained(a, b))
+		{
+		  a->destroy();
+		  result_ = b;
+		}
+	      // if !a => b, then  a W b = 1
+	      else if (lcc->neg_contained(a, b))
+		{
+		  a->destroy();
+		  b->destroy();
+		  result_ = constant::true_instance();
+		}
+	      else
+		{
+		  result_ = binop::instance(binop::W, a, b);
+		}
+	      break;
 	    case binop::R:
 	      // if (a R b) => b, then keep b !
 	      if (stronger && lcc->contained(b, bo))
@@ -226,6 +251,31 @@ namespace spot
 		  result_ = binop::instance(binop::R, a, b);
 		}
 	      break;
+	    case binop::M:
+	      // if (a M b) => b, then keep b !
+	      if (stronger && lcc->contained(b, bo))
+		{
+		  a->destroy();
+		  result_ = b;
+		}
+	      // if b => a,  then a M b = b.
+	      else if ((!stronger) && lcc->contained(b, a))
+		{
+		  a->destroy();
+		  result_ = b;
+		}
+	      // if a => !b, then  a M b = 0
+	      else if (lcc->contained_neg(a, b))
+		{
+		  a->destroy();
+		  b->destroy();
+		  result_ = constant::false_instance();
+		}
+	      else
+		{
+		  result_ = binop::instance(binop::M, a, b);
+		}
+	      break;
 	    default:
 	      result_ = binop::instance(bo->op(), a, b);
 	    }

src/ltlvisit/lunabbrev.cc

@@ -1,4 +1,4 @@
-// Copyright (C) 2009 Laboratoire de Recherche et Développement
+// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -44,7 +44,8 @@ namespace spot
       formula* f1 = recurse(bo->first());
       formula* f2 = recurse(bo->second());
 
-      switch (bo->op())
+      binop::type op = bo->op();
+      switch (op)
 	{
 	  /* f1 ^ f2  ==  (f1 & !f2) | (f2 & !f1) */
 	case binop::Xor:
@@ -74,9 +75,13 @@ namespace spot
 	  return;
           /* f1 U f2 == f1 U f2 */
 	  /* f1 R f2 == f1 R f2 */
+          /* f1 W f2 == f1 W f2 */
+	  /* f1 M f2 == f1 M f2 */
    	case binop::U:
 	case binop::R:
-	  result_ = binop::instance(bo->op(), f1, f2);
+	case binop::W:
+	case binop::M:
+	  result_ = binop::instance(op, f1, f2);
 	  return;
 	}
       /* Unreachable code. */

src/ltlvisit/nenoform.cc

@@ -1,4 +1,4 @@
-// Copyright (C) 2009 Laboratoire de Recherche et Développement
+// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -154,6 +154,16 @@ namespace spot
 	      result_ = binop::instance(negated_ ? binop::U : binop::R,
 					recurse(f1), recurse(f2));
 	      return;
+	    case binop::W:
+	      /* !(a W b) == !a M !b */
+	      result_ = binop::instance(negated_ ? binop::M : binop::W,
+					recurse(f1), recurse(f2));
+	      return;
+	    case binop::M:
+	      /* !(a M b) == !a W !b */
+	      result_ = binop::instance(negated_ ? binop::W : binop::M,
+					recurse(f1), recurse(f2));
+	      return;
 	    }
 	  /* Unreachable code.  */
 	  assert(0);

src/ltlvisit/randomltl.cc

@@ -1,4 +1,4 @@
-// Copyright (C) 2008, 2009 Laboratoire de Recherche et Développement
+// Copyright (C) 2008, 2009, 2010 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 // Copyright (C) 2005 Laboratoire d'Informatique de Paris 6
 // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
@@ -102,7 +102,7 @@ namespace spot
 
     namespace
     {
-      const int proba_size = 14;
+      const int proba_size = 16;
     }
 
     random_ltl::random_ltl(const atomic_prop_set* ap)
@@ -122,8 +122,10 @@ namespace spot
       proba_[9].setup("xor",     3, binop_builder<binop::Xor>);
       proba_[10].setup("R",      3, binop_builder<binop::R>);
       proba_[11].setup("U",      3, binop_builder<binop::U>);
-      proba_[12].setup("and",    3, multop_builder<multop::And>);
+      proba_[12].setup("W",      3, binop_builder<binop::W>);
-      proba_[13].setup("or",     3, multop_builder<multop::Or>);
+      proba_[13].setup("M",      3, binop_builder<binop::M>);
+      proba_[14].setup("and",    3, multop_builder<multop::And>);
+      proba_[15].setup("or",     3, multop_builder<multop::Or>);
 
       proba_[0].proba = ap_->size();
 

src/ltlvisit/randomltl.hh

@@ -1,3 +1,5 @@
+// Copyright (C) 2010 Laboratoire de Recherche et Développement de
+// l'Epita (LRDE).
 // Copyright (C) 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
@@ -82,6 +84,8 @@ namespace spot
       /// xor     1
       /// R       1
       /// U       1
+      /// W       1
+      /// M       1
       /// and     1
       /// or      1
       /// \endverbatim

src/ltlvisit/reduce.cc

@@ -1,5 +1,5 @@
-// Copyright (C) 2008, 2009 Laboratoire de Recherche et Développement
+// Copyright (C) 2008, 2009, 2010 Laboratoire de Recherche et
-// de l'Epita (LRDE).
+// Développement de l'Epita (LRDE).
 // Copyright (C) 2004, 2006, 2007 Laboratoire d'Informatique de
 // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
 // Université Pierre et Marie Curie.
@@ -110,23 +110,46 @@ namespace spot
 	void
 	visit(binop* bo)
 	{
+	  binop::type op = bo->op();
+
 	  formula* f2 = recurse(bo->second());
+	  bool f2_eventual = false;
 
-	  /* If b is a pure eventuality formula then a U b = b.
+	  if (opt_ & Reduce_Eventuality_And_Universality)
-	     If b is a pure universality formula a R b = b. */
-	  if ((opt_ & Reduce_Eventuality_And_Universality)
-	      && ((is_eventual(f2) && ((bo->op()) == binop::U))
-		  || (is_universal(f2) && ((bo->op()) == binop::R))))
 	    {
-	      result_ = f2;
+	      f2_eventual = is_eventual(f2);
-	      return;
+	      /* If b is a pure eventuality formula then a U b = b.
+		 If b is a pure universality formula a R b = b. */
+	      if ((f2_eventual && (op == binop::U))
+		  || (is_universal(f2) && (op == binop::R)))
+		{
+		  result_ = f2;
+		  return;
+		}
 	    }
-	  /* case of implies */
-	  formula* f1 = recurse(bo->first());
 
+	  formula* f1 = recurse(bo->first());
+	  if (opt_ & Reduce_Eventuality_And_Universality)
+	    {
+	      /* If a&b is a pure eventuality formula then a M b = a & b.
+		 If a is a pure universality formula a W b = a|b. */
+	      if (is_eventual(f1) && f2_eventual && (op == binop::M))
+		{
+		  result_ = multop::instance(multop::And, f1, f2);
+		  return;
+		}
+	      if (is_universal(f1) && (op == binop::W))
+		{
+		  result_ = multop::instance(multop::Or, f1, f2);
+		  return;
+		}
+	    }
+
+
+	  /* case of implies */
 	  if (opt_ & Reduce_Syntactic_Implications)
 	    {
-	      switch (bo->op())
+	      switch (op)
 		{
 		case binop::Xor:
 		case binop::Equiv:
@@ -149,9 +172,10 @@ namespace spot
 		      return;
 		    }
 		  /* a < b => a U (b U c) = (b U c) */
+		  /* a < b => a U (b W c) = (b W c) */
 		  {
 		    binop* bo = dynamic_cast<binop*>(f2);
-		    if (bo && bo->op() == binop::U
+		    if (bo && (bo->op() == binop::U || bo->op() == binop::W)
 			&& syntactic_implication(f1, bo->first()))
 		      {
 			result_ = f2;
@@ -188,9 +212,68 @@ namespace spot
 		      }
 		  }
 		  break;
+
+		case binop::W:
+		  /* a < b => a W b = b */
+		  if (syntactic_implication(f1, f2))
+		    {
+		      result_ = f2;
+		      f1->destroy();
+		      return;
+		    }
+		  /* !b < a => a W b = 1 */
+		  if (syntactic_implication_neg(f2, f1, false))
+		    {
+		      result_ = constant::true_instance();
+		      f1->destroy();
+		      f2->destroy();
+		      return;
+		    }
+		  /* a < b => a W (b U c) = (b U c) */
+		  /* a < b => a W (b W c) = (b W c) */
+		  {
+		    binop* bo = dynamic_cast<binop*>(f2);
+		    if (bo && (bo->op() == binop::U || bo->op() == binop::W)
+			&& syntactic_implication(f1, bo->first()))
+		      {
+			result_ = f2;
+			f1->destroy();
+			return;
+		      }
+		  }
+		  break;
+
+		case binop::M:
+		  /* b < a => a M b = b */
+		  if (syntactic_implication(f2, f1))
+		    {
+		      result_ = f2;
+		      f1->destroy();
+		      return;
+		    }
+		  /* b < !a => a M b = 0 */
+		  if (syntactic_implication_neg(f2, f1, true))
+		    {
+		      result_ = constant::false_instance();
+		      f1->destroy();
+		      f2->destroy();
+		      return;
+		    }
+		  /* b < a => a R (b R c) = b R c */
+		  {
+		    binop* bo = dynamic_cast<binop*>(f2);
+		    if (bo && bo->op() == binop::R
+			&& syntactic_implication(bo->first(), f1))
+		      {
+			result_ = f2;
+			f1->destroy();
+			return;
+		      }
+		  }
+		  break;
 		}
 	    }
-	  result_ = binop::instance(bo->op(), f1, f2);
+	  result_ = binop::instance(op, f1, f2);
 	}
 
 	void

src/ltlvisit/simpfg.cc

@@ -1,3 +1,7 @@
+// Copyright (C) 2010 Laboratoire de Recherche et Développement de
+// l'Epita (LRDE).
+// département Systèmes Répartis Coopératifs (SRC), Université Pierre
+// et Marie Curie.
 // Copyright (C) 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
@@ -42,13 +46,14 @@ namespace spot
     {
       formula* f1 = recurse(bo->first());
       formula* f2 = recurse(bo->second());
+      binop::type op = bo->op();
 
-      switch (bo->op())
+      switch (op)
 	{
 	case binop::Xor:
 	case binop::Implies:
 	case binop::Equiv:
-	  result_ = binop::instance(bo->op(), f1, f2);
+	  result_ = binop::instance(op, f1, f2);
 	  return;
 	  /* true U f2 == F(f2) */
 	case binop::U:
@@ -64,6 +69,20 @@ namespace spot
 	  else
 	    result_ = binop::instance(binop::R, f1, f2);
 	  return;
+	  /* f1 W false == G(f1) */
+	case binop::W:
+	  if (f2 == constant::false_instance())
+	    result_ = unop::instance(unop::G, f1);
+	  else
+	    result_ = binop::instance(binop::W, f1, f2);
+	  return;
+	  /* f1 M true == F(f1) */
+	case binop::M:
+	  if (f1 == constant::true_instance())
+	    result_ = unop::instance(unop::F, f2);
+	  else
+	    result_ = binop::instance(binop::M, f1, f2);
+	  return;
 	}
       /* Unreachable code. */
       assert(0);

src/ltlvisit/simpfg.hh

@@ -1,3 +1,5 @@
+// Copyright (C) 2010 Laboratoire de Recherche et Développement de
+// l'Epita (LRDE).
 // Copyright (C) 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
@@ -30,6 +32,14 @@ namespace spot
   {
     /// \brief Replace <code>true U f</code> and <code>false R g</code> by
     /// <code>F f</code> and <code>G g</code>.
+    ///
+    /// Perform the following rewriting (from left to right):
+    ///
+    /// - true U a = F a
+    /// - a M true = F a
+    /// - false R a = G a
+    /// - a W false = G a
+    ///
     /// \ingroup ltl_visitor
     class simplify_f_g_visitor : public clone_visitor
     {
@@ -46,6 +56,14 @@ namespace spot
 
     /// \brief Replace <code>true U f</code> and <code>false R g</code> by
     /// <code>F f</code> and <code>G g</code>.
+    ///
+    /// Perform the following rewriting (from left to right):
+    ///
+    /// - true U a = F a
+    /// - a M true = F a
+    /// - false R a = G a
+    /// - a W false = G a
+    ///
     /// \ingroup ltl_rewriting
     formula* simplify_f_g(const formula* f);
   }

src/ltlvisit/syntimpl.cc

@@ -1,4 +1,4 @@
-// Copyright (C) 2009 Laboratoire de Recherche et Développement
+// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -108,7 +108,13 @@ namespace spot
 		  // Both operand must be purely eventual, unlike in
 		  // the proceedings of Concur'00.  (The revision of
 		  // the paper available at
-		  // http://www1.bell-labs.com/project/TMP/ is fixed.)
+		  // http://www.bell-labs.com/project/TMP/ is fixed.)
+		  || (recurse_ev(f1) && recurse_ev(f2)))
+		eventual = true;
+	      return;
+	    case binop::W:
+	      universal = recurse_un(f1) && recurse_un(f2);
+	      if ((f2 == constant::true_instance())
 		  || (recurse_ev(f1) && recurse_ev(f2)))
 		eventual = true;
 	      return;
@@ -118,6 +124,12 @@ namespace spot
 		  || (recurse_un(f1) && recurse_un(f2)))
 		universal = true;
 	      return;
+	    case binop::M:
+	      eventual = recurse_ev(f1) && recurse_ev(f2);
+	      if ((f2 == constant::false_instance())
+		  || (recurse_un(f1) && recurse_un(f2)))
+		universal = true;
+	      return;
 	    }
 	  /* Unreachable code.  */
 	  assert(0);
@@ -263,6 +275,7 @@ namespace spot
 	    case binop::Implies:
 	      return;
 	    case binop::U:
+	    case binop::W:
 	      if (syntactic_implication(f, f2))
 		result_ = true;
 	      return;
@@ -285,6 +298,25 @@ namespace spot
 		  && syntactic_implication(f, f2))
 		result_ = true;
 	      return;
+	    case binop::M:
+	      if (fb && fb->op() == binop::M)
+		if (syntactic_implication(fb->first(), f1) &&
+		    syntactic_implication(fb->second(), f2))
+		  {
+		    result_ = true;
+		    return;
+		  }
+	      if (fu && fu->op() == unop::F)
+		if (f2 == constant::true_instance() &&
+		    syntactic_implication(fu->child(), f1))
+		  {
+		    result_ = true;
+		    return;
+		  }
+	      if (syntactic_implication(f, f1)
+		  && syntactic_implication(f, f2))
+		result_ = true;
+	      return;
 	    }
 	  /* Unreachable code.  */
 	  assert(0);
@@ -480,6 +512,26 @@ namespace spot
 		  && syntactic_implication(f2, f))
 		result_ = true;
 	      return;
+	    case binop::W:
+	      /* (a < c) && (c < d) => a W b < c W d */
+	      if (fb && fb->op() == binop::W)
+		if (syntactic_implication(f1, fb->first()) &&
+		    syntactic_implication(f2, fb->second()))
+		  {
+		    result_ = true;
+		    return;
+		  }
+	      if (fu && fu->op() == unop::G)
+		if (f2 == constant::false_instance() &&
+		    syntactic_implication(f1, fu->child()))
+		  {
+		    result_ = true;
+		    return;
+		  }
+	      if (syntactic_implication(f1, f)
+		  && syntactic_implication(f2, f))
+		result_ = true;
+	      return;
 	    case binop::R:
 	      if (fu && fu->op() == unop::G)
 		if (f1 == constant::false_instance() &&
@@ -491,6 +543,17 @@ namespace spot
 	      if (syntactic_implication(f2, f))
 		result_ = true;
 	      return;
+	    case binop::M:
+	      if (fu && fu->op() == unop::F)
+		if (f2 == constant::true_instance() &&
+		    syntactic_implication(f1, fu->child()))
+		  {
+		    result_ = true;
+		    return;
+		  }
+	      if (syntactic_implication(f2, f))
+		result_ = true;
+	      return;
 	    }
 	  /* Unreachable code.  */
 	  assert(0);

src/ltlvisit/tostring.cc

@@ -1,4 +1,4 @@
-// Copyright (C) 2008 Laboratoire de Recherche et Développement
+// Copyright (C) 2008, 2010 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -118,6 +118,12 @@ namespace spot
 	    case binop::R:
 	      os_ << " R ";
 	      break;
+	    case binop::W:
+	      os_ << " W ";
+	      break;
+	    case binop::M:
+	      os_ << " M ";
+	      break;
 	    }
 
 	  bo->second()->accept(*this);
@@ -276,6 +282,17 @@ namespace spot
 	     os_ << " V ";
 	      bo->second()->accept(*this);
 	      break;
+	      /* W and M are not supported by Spin */
+	    case binop::W:
+	      bo->first()->accept(*this);
+	      os_ << " W ";
+	      bo->second()->accept(*this);
+	      break;
+	    case binop::M:
+	      bo->first()->accept(*this);
+	     os_ << " M ";
+	      bo->second()->accept(*this);
+	      break;
 	    }
 
 	  if (!top_level)

src/tgba/formula2bdd.cc

@@ -1,4 +1,4 @@
-// Copyright (C) 2009 Laboratoire de Recherche et Développement
+// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris
 // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
@@ -107,6 +107,8 @@ namespace spot
 	    return;
 	  case binop::U:
 	  case binop::R:
+	  case binop::W:
+	  case binop::M:
 	    assert(!"unsupported operator");
 	  }
 	/* Unreachable code.  */

src/tgbaalgos/eltl2tgba_lacim.cc

@@ -1,5 +1,5 @@
-// Copyright (C) 2008, 2009 Laboratoire de Recherche et Développement
+// Copyright (C) 2008, 2009, 2010 Laboratoire de Recherche et
-// de l'Epita (LRDE).
+// Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -124,6 +124,8 @@ namespace spot
 	    return;
 	  case binop::U:
 	  case binop::R:
+	  case binop::W:
+	  case binop::M:
 	    assert(!"unsupported operator");
 	  }
 	/* Unreachable code.  */

src/tgbaalgos/ltl2taa.cc

@@ -1,4 +1,4 @@
-// Copyright (C) 2009 Laboratoire de Recherche et Développement
+// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -155,12 +155,17 @@ namespace spot
 	std::vector<succ_state>::iterator i2;
 	taa_tgba::transition* t = 0;
 	bool contained = false;
+	bool strong = false;
+
 	switch (node->op())
 	{
-	  case binop::U: // Strong
+	case binop::U:
-	    if (refined_)
+	  strong = true;
-	      contained = lcc_->contained(node->second(), node->first());
+	  // fall thru
-	    for (i1 = v1.succ_.begin(); i1 != v1.succ_.end(); ++i1)
+	case binop::W:
+	  if (refined_)
+	    contained = lcc_->contained(node->second(), node->first());
+	  for (i1 = v1.succ_.begin(); i1 != v1.succ_.end(); ++i1)
 	    {
 	      // Refined rule
 	      if (refined_ && contained)
@@ -168,60 +173,75 @@ namespace spot
 		  (remove(i1->Q.begin(), i1->Q.end(), v1.init_), i1->Q.end());
 
 	      i1->Q.push_back(init_); // Add the initial state
-	      i1->acc.push_back(node->second());
+	      if (strong)
+		i1->acc.push_back(node->second());
 	      t = res_->create_transition(init_, i1->Q);
 	      res_->add_condition(t, i1->condition->clone());
-	      res_->add_acceptance_condition(t, node->second()->clone());
+	      if (strong)
+		res_->add_acceptance_condition(t, node->second()->clone());
+	      else
+		for (unsigned i = 0; i < i1->acc.size(); ++i)
+		  res_->add_acceptance_condition(t, i1->acc[i]->clone());
 	      succ_.push_back(*i1);
 	    }
-	    for (i2 = v2.succ_.begin(); i2 != v2.succ_.end(); ++i2)
+	  for (i2 = v2.succ_.begin(); i2 != v2.succ_.end(); ++i2)
 	    {
 	      t = res_->create_transition(init_, i2->Q);
 	      res_->add_condition(t, i2->condition->clone());
 	      succ_.push_back(*i2);
 	    }
-	    return;
+	  return;
-	  case binop::R: // Weak
+	case binop::M: // Strong Release
-	    if (refined_)
+	  strong = true;
-	      contained = lcc_->contained(node->first(), node->second());
+	case binop::R: // Weak Release
-	    for (i2 = v2.succ_.begin(); i2 != v2.succ_.end(); ++i2)
+	  if (refined_)
+	    contained = lcc_->contained(node->first(), node->second());
+
+	  for (i2 = v2.succ_.begin(); i2 != v2.succ_.end(); ++i2)
 	    {
 	      for (i1 = v1.succ_.begin(); i1 != v1.succ_.end(); ++i1)
-	      {
-		std::vector<const formula*> u; // Union
-		std::vector<const formula*> a; // Acceptance conditions
-		std::copy(i1->Q.begin(), i1->Q.end(), ii(u, u.end()));
-		formula* f = i1->condition->clone(); // Refined rule
-		if (!refined_ || !contained)
 		{
-		  std::copy(i2->Q.begin(), i2->Q.end(), ii(u, u.end()));
+		  std::vector<const formula*> u; // Union
-		  f = multop::instance(multop::And, f, i2->condition->clone());
+		  std::vector<const formula*> a; // Acceptance conditions
+		  std::copy(i1->Q.begin(), i1->Q.end(), ii(u, u.end()));
+		  formula* f = i1->condition->clone(); // Refined rule
+		  if (!refined_ || !contained)
+		    {
+		      std::copy(i2->Q.begin(), i2->Q.end(), ii(u, u.end()));
+		      f = multop::instance(multop::And, f,
+					   i2->condition->clone());
+		    }
+		  to_free_.push_back(f);
+		  t = res_->create_transition(init_, u);
+		  res_->add_condition(t, f->clone());
+		  succ_state ss = { u, f, a };
+		  succ_.push_back(ss);
 		}
-		to_free_.push_back(f);
-
-		t = res_->create_transition(init_, u);
-		res_->add_condition(t, f->clone());
-		succ_state ss = { u, f, a };
-		succ_.push_back(ss);
-	      }
 
 	      if (refined_) // Refined rule
 		i2->Q.erase
 		  (remove(i2->Q.begin(), i2->Q.end(), v2.init_), i2->Q.end());
 
+
 	      i2->Q.push_back(init_); // Add the initial state
 	      t = res_->create_transition(init_, i2->Q);
 	      res_->add_condition(t, i2->condition->clone());
-	      if (refined_)
+
+	      if (strong)
+		{
+		  i2->acc.push_back(node->first());
+		  res_->add_acceptance_condition(t, node->first()->clone());
+		}
+	      else if (refined_)
 		for (unsigned i = 0; i < i2->acc.size(); ++i)
 		  res_->add_acceptance_condition(t, i2->acc[i]->clone());
 	      succ_.push_back(*i2);
 	    }
-	    return;
+	  return;
-	  case binop::Xor:
+	case binop::Xor:
-	  case binop::Implies:
+	case binop::Implies:
-	  case binop::Equiv:
+	case binop::Equiv:
-	    assert(0); // TBD
+	  assert(0); // TBD
 	}
 	/* Unreachable code.  */
 	assert(0);

src/tgbaalgos/ltl2tgba_fm.cc

@@ -393,6 +393,13 @@ namespace spot
 	      res_ = f2 | (bdd_ithvar(a) & f1 & bdd_ithvar(x));
 	      return;
 	    }
+	  case binop::W:
+	    {
+	      // r(f1 W f2) = r(f2) + r(f1)r(X(f1 U f2))
+	      int x = dict_.register_next_variable(node);
+	      res_ = f2 | (f1 & bdd_ithvar(x));
+	      return;
+	    }
 	  case binop::R:
 	    {
 	      // r(f1 R f2) = r(f1)r(f2) + r(f2)r(X(f1 U f2))
@@ -400,6 +407,14 @@ namespace spot
 	      res_ = (f1 & f2) | (f2 & bdd_ithvar(x));
 	      return;
 	    }
+	  case binop::M:
+	    {
+	      // r(f1 M f2) = r(f1)r(f2) + a(f1)r(f2)r(X(f1 M f2))
+	      int a = dict_.register_a_variable(node->first());
+	      int x = dict_.register_next_variable(node);
+	      res_ = (f1 & f2) | (bdd_ithvar(a) & f2 & bdd_ithvar(x));
+	      return;
+	    }
 	  }
 	/* Unreachable code.  */
 	assert(0);
@@ -449,8 +464,8 @@ namespace spot
     };
 
 
-    // Check whether a formula has a R or G operator at its top-level
+    // Check whether a formula has a R, W, or G operator at its
-    // (preceding logical operators do not count).
+    // top-level (preceding logical operators do not count).
     class ltl_possible_fair_loop_visitor: public const_visitor
     {
     public:
@@ -501,8 +516,10 @@ namespace spot
 	      node->second()->accept(*this);
 	    return;
 	  case binop::U:
+	  case binop::M:
 	    return;
 	  case binop::R:
+	  case binop::W:
 	    res_ = true;
 	    return;
 	  }

src/tgbaalgos/ltl2tgba_lacim.cc

@@ -1,4 +1,4 @@
-// Copyright (C) 2009 Laboratoire de Recherche et Développement
+// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -160,7 +160,8 @@ namespace spot
 	bdd f1 = recurse(node->first());
 	bdd f2 = recurse(node->second());
 
-	switch (node->op())
+	binop::type op = node->op();
+	switch (op)
 	  {
 	  case binop::Xor:
 	    res_ = bdd_apply(f1, f2, bddop_xor);
@@ -172,39 +173,47 @@ namespace spot
 	    res_ = bdd_apply(f1, f2, bddop_biimp);
 	    return;
 	  case binop::U:
+	  case binop::W:
 	    {
-	      /*
+	      // f1 U f2 <=> f2 | (f1 & X(f1 U f2))
-		 f1 U f2 <=> f2 | (f1 & X(f1 U f2))
+	      //   In other words:
-		 In other words:
+	      // now <=> f2 | (f1 & next)
-		     now <=> f2 | (f1 & next)
-	      */
 	      int v = fact_.create_state(node);
 	      bdd now = bdd_ithvar(v);
 	      bdd next = bdd_ithvar(v + 1);
 	      fact_.constrain_relation(bdd_apply(now, f2 | (f1 & next),
 						 bddop_biimp));
-	      /*
+	      if (op == binop::U)
-		The rightmost conjunction, f1 & next, doesn't actually
+		{
-		encode the fact that f2 should be fulfilled eventually.
+		  // The rightmost conjunction, f1 & next, doesn't
-		We declare an acceptance condition for this purpose (see
+		  // actually encode the fact that f2 should be
-		the comment in the unop::F case).
+		  // fulfilled eventually.  We declare an acceptance
-	      */
+		  // condition for this purpose (see the comment in
-	      fact_.declare_acceptance_condition(f2 | !now, node->second());
+		  // the unop::F case).
+		  fact_.declare_acceptance_condition(f2 | !now, node->second());
+		}
 	      res_ = now;
 	      return;
 	    }
 	  case binop::R:
+	  case binop::M:
 	    {
-	      /*
+	      // f1 R f2 <=> f2 & (f1 | X(f1 R f2))
-		 f1 R f2 <=> f2 & (f1 | X(f1 R f2))
+	      //   In other words:
-		 In other words:
+	      // now <=> f2 & (f1 | next)
-		     now <=> f2 & (f1 | next)
-	      */
 	      int v = fact_.create_state(node);
 	      bdd now = bdd_ithvar(v);
 	      bdd next = bdd_ithvar(v + 1);
 	      fact_.constrain_relation(bdd_apply(now, f2 & (f1 | next),
 						 bddop_biimp));
+	      if (op == binop::M)
+		{
+		  // f2 & next, doesn't actually encode the fact that
+		  // f1 should be fulfilled eventually.  We declare an
+		  // acceptance condition for this purpose (see the
+		  // comment in the unop::F case).
+		  fact_.declare_acceptance_condition(f1 | !now, node->second());
+		}
 	      res_ = now;
 	      return;
 	    }

src/tgbatest/ltl2neverclaim.test

@@ -1,9 +1,6 @@
 #!/bin/sh
-# Copyright (C) 2009 Laboratoire de Recherche et Développement
+# Copyright (C) 2010 Laboratoire de Recherche et Développement
 # de l'Epita (LRDE).
-# 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.
 #
@@ -22,22 +19,85 @@
 # Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
 # 02111-1307, USA.
 
+# Do some quick translations to make sure the neverclaim produced by
+# spot actually look correct!
+
+# This test is separate from spotlbtt.test, because lbtt-translate
+# will refuse to passe M and W to a tool (spot) that masquerades as
+# Spin.
 
 . ./defs
 
 set -e
 
-# We don't check the output, but just running these might be enough to
+cat > config <<EOF
-# trigger assertions.
+Algorithm
+{
+   Name = "Spot (Couvreur -- FM)"
+   Path = "${LBTT_TRANSLATE}"
+   Parameters = "--spot '../ltl2tgba -F -f -t'"
+   Enabled = yes
+}
 
-run 0 ../ltl2tgba -N -x a
+Algorithm
-run 0 ../ltl2tgba -N -x  'a U b'
+{
-run 0 ../ltl2tgba -N -x 'X a'
+   Name = "Spot (Couvreur -- FM), with reductions"
-run 0 ../ltl2tgba -N -x 'a & b & c'
+   Path = "${LBTT_TRANSLATE}"
-run 0 ../ltl2tgba -N -x 'a | b | (c U (d & (g U (h ^ i))))'
+   Parameters = "--spot '../ltl2tgba -r4 -R3f -F -f -t'"
-run 0 ../ltl2tgba -N -x 'Xa & (b U !a) & (b U !a)'
+   Enabled = no
-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'
+Algorithm
-run 0 ../ltl2tgba -N -x 'a R (b R c)'
+{
-run 0 ../ltl2tgba -N -x '(a U b) U (c U d)'
+   Name = "Spot (Couvreur -- FM), degeneralized via never claim"
+   Path = "${LBTT_TRANSLATE}"
+   Parameters = "--spin '../ltl2tgba -F -f -N'"
+   Enabled = yes
+}
+
+Algorithm
+{
+   Name = "Spot (Couvreur -- FM), reductions, degeneralized via never claim"
+   Path = "${LBTT_TRANSLATE}"
+   Parameters = "--spin '../ltl2tgba -F -f -r4 -R3 -N'"
+   Enabled = yes
+}
+
+GlobalOptions
+{
+   Rounds = 100
+   Interactive = Never
+#   Verbosity = 5
+#   ComparisonCheck = no
+#   ConsistencyCheck = no
+#   IntersectionCheck = no
+}
+
+FormulaOptions
+{
+  Size = 1...13
+  Propositions = 6
+
+  AbbreviatedOperators = Yes
+  GenerateMode = Normal
+  OutputMode = Normal
+  PropositionPriority = 50
+
+  TruePriority = 1
+  FalsePriority = 1
+
+  AndPriority = 10
+  OrPriority = 10
+  XorPriority = 0
+  # EquivalencePriority = 0
+
+  BeforePriority = 0
+  StrongReleasePriority = 0
+  WeakUntilPriority = 0
+
+  DefaultOperatorPriority = 5
+}
+EOF
+
+${LBTT}
+rm config

src/tgbatest/ltl2tgba.cc

@@ -71,7 +71,9 @@ U=(0 0 $0	   \
    accept 1)	   \
 G=(0 0 $0)	   \
 F=U(true, $0)	   \
-R=!U(!$0, !$1)";
+W=G($0)|U($0, $1)  \
+R=!U(!$0, !$1)     \
+M=F($0)&R($0, $1)";
   return s;
 }
 

src/tgbatest/spotlbtt.test

@@ -208,9 +208,9 @@ Algorithm
 
 Algorithm
 {
-   Name = "Spot (Couvreur -- FM), degeneralized, via never claim"
+   Name = "Spot (Couvreur -- FM), degeneralized on states"
    Path = "${LBTT_TRANSLATE}"
-   Parameters = "--spin '../ltl2tgba -F -f -N'"
+   Parameters = "--spot '../ltl2tgba -F -f -t -DS'"
    Enabled = yes
 }
 
@@ -272,9 +272,9 @@ Algorithm
 
 Algorithm
 {
-   Name = "Spot (Couvreur -- FM), pre + post reduction, via never claim"
+   Name = "Spot (Couvreur -- FM), pre + post reduction, degeneralized on states"
    Path = "${LBTT_TRANSLATE}"
-   Parameters = "--spin '../ltl2tgba -F -f -N -R3 -r7'"
+   Parameters = "--spot '../ltl2tgba -F -f -DS -R3 -r7 -t'"
    Enabled = yes
 }
 
@@ -339,8 +339,6 @@ FormulaOptions
   # EquivalencePriority = 0
 
   BeforePriority = 0
-  StrongReleasePriority = 0
-  WeakUntilPriority = 0
 
   DefaultOperatorPriority = 5
 }