* src/ltlvisit/nenoform.hh, src/ltlvisit/nenoform.cc: New files.

* src/ltlvisit/Makefile.am (libltlvisit_a_SOURCES): Add them.
* src/ltltest/equals.cc (main) [NENOFORM]: Call negative_normal_form.
* src/ltltest/nenoform.test, src/ltltest/tunenoform.test: New files.
* src/ltltest/Makefile.am (check_PROGRAMS): Add nenoform and
tunenoform.
(nenoform_SOURCES, nenoform_CPPFLAGS, tunenoform_SOURCES,
tunenoform_CPPFLAGS): New variables.
(TESTS): Add nenoform.test and tunenoform.test.

ChangeLog

@@ -1,5 +1,15 @@
 2003-04-17  Alexandre DURET-LUTZ  <aduret@src.lip6.fr>
 
+	* src/ltlvisit/nenoform.hh, src/ltlvisit/nenoform.cc: New files.
+	* src/ltlvisit/Makefile.am (libltlvisit_a_SOURCES): Add them.
+	* src/ltltest/equals.cc (main) [NENOFORM]: Call negative_normal_form.
+	* src/ltltest/nenoform.test, src/ltltest/tunenoform.test: New files.
+	* src/ltltest/Makefile.am (check_PROGRAMS): Add nenoform and
+	tunenoform.
+	(nenoform_SOURCES, nenoform_CPPFLAGS, tunenoform_SOURCES, 
+	tunenoform_CPPFLAGS): New variables.
+	(TESTS): Add nenoform.test and tunenoform.test.
+
 	* src/ltlvisit/lunabbrev.hh: Fix include guard.
 
 2003-04-16  Alexandre DURET-LUTZ  <aduret@src.lip6.fr>

src/ltltest/.cvsignore

@@ -10,3 +10,5 @@ defs
 equals
 lunabbrev
 tunabbrev
+nenoform
+tunenoform

src/ltltest/Makefile.am

@@ -4,7 +4,17 @@ LDADD = ../ltlparse/libltlparse.a \
         ../ltlast/libltlast.a 
 
 check_SCRIPTS = defs
-check_PROGRAMS = ltl2dot ltl2text equals lunabbrev tunabbrev
+
+# Keep this sorted alphabetically.
+check_PROGRAMS = \
+  equals \
+  ltl2dot \
+  ltl2text \
+  lunabbrev \
+  nenoform \
+  tunabbrev \
+  tunenoform
+
 ltl2dot_SOURCES = readltl.cc
 ltl2dot_CPPFLAGS = $(AM_CPPFLAGS) -DDOTTY
 ltl2text_SOURCES = readltl.cc
@@ -13,8 +23,21 @@ lunabbrev_SOURCES = equals.cc
 lunabbrev_CPPFLAGS = $(AM_CPPFLAGS) -DLUNABBREV
 tunabbrev_SOURCES = equals.cc
 tunabbrev_CPPFLAGS = $(AM_CPPFLAGS) -DTUNABBREV
+nenoform_SOURCES = equals.cc
+nenoform_CPPFLAGS = $(AM_CPPFLAGS) -DNENOFORM
+tunenoform_SOURCES = equals.cc
+tunenoform_CPPFLAGS = $(AM_CPPFLAGS) -DNENOFORM -DTUNABBREV
 
 EXTRA_DIST = $(TESTS)
-TESTS = parse.test parseerr.test equals.test lunabbrev.test tunabbrev.test
+
+# Ordered by strength of the test.  Test basic features first.
+TESTS = \
+  parse.test \
+  parseerr.test \
+  equals.test \
+  lunabbrev.test \
+  tunabbrev.test \
+  nenoform.test \
+  tunenoform.test
 
 CLEANFILES = stdout expect parse.dot

src/ltltest/equals.cc

@@ -4,6 +4,7 @@
 #include "ltlvisit/lunabbrev.hh"
 #include "ltlvisit/tunabbrev.hh"
 #include "ltlvisit/dump.hh"
+#include "ltlvisit/nenoform.hh"
 
 void
 syntax(char *prog)
@@ -34,10 +35,17 @@ main(int argc, char **argv)
 #ifdef LUNABBREV
   f1 = spot::ltl::unabbreviate_logic(f1);
   spot::ltl::dump(*f1, std::cout);
+  std::cout << std::endl;
 #endif
 #ifdef TUNABBREV
   f1 = spot::ltl::unabbreviate_ltl(f1);
   spot::ltl::dump(*f1, std::cout);
+  std::cout << std::endl;
+#endif
+#ifdef NENOFORM
+  f1 = spot::ltl::negative_normal_form(f1);
+  spot::ltl::dump(*f1, std::cout);
+  std::cout << std::endl;
 #endif
 
   if (equals(f1, f2))

src/ltltest/nenoform.test

@@ -0,0 +1,49 @@
+#! /bin/sh
+
+# Check for the negative_normal_form visitor
+
+. ./defs || exit 1
+
+check()
+{
+  ./nenoform "$1" "$2" || exit 1
+}
+
+# A few things that do not change
+check 'a' 'a'
+check '1' '1'
+check '0' '0'
+check '!a' '!a'
+check 'a U b' 'a U b'
+check 'a & b' 'a & b'
+check 'a & b' 'b & a'
+check 'a & !b & c' 'c & a & !b'
+check 'a & b & c' 'b & c & a'
+check 'Xa & b & Xa' 'b & Xa & b'
+check 'a & b' 'b & a & b'
+check 'a & !b' '!b & a & a'
+check 'a & b & (Xc |(f U !g)| e)' 'b & a & a & (Xc | e |(f U !g)| e | Xc) & b'
+check 'GFa => FGb' 'GFa => FGb'
+
+# Basic rewritings
+check '!!a' 'a'
+check '!!!!!a' '!a'
+check '!Xa' 'X!a'
+check '!Fa' 'G!a'
+check '!Ga' 'F!a'
+check '!(a ^ b)' 'a <=> b'
+check '!(a <=> b)' '(((a) ^ (b)))'
+check '!(a => b)' 'a&!b'
+check '!(!a => !b)' '!a&b'
+check '!(a U b)' '!a R !b'
+check '!(a R b)' '!a U !b'
+check '!(!a R !b)' 'a U b'
+check '!(a & b & c & d & b)' '!a | !b | !c | !d'
+check '!(a | b | c | d)' '!a & !b & !c & !d'
+
+# Nested rewritings
+check '!(a U (!b U ((a & b & c) R d)))' '!a R (b R ((!a | !b | !c) U !d))'
+check '!(GF a => FG b)' 'GFa & GF!b'
+
+# Success.
+:

src/ltltest/tunenoform.test

@@ -0,0 +1,21 @@
+#! /bin/sh
+
+# Check for unabbreviate_ltl + negative_normal_form visitors
+
+. ./defs || exit 1
+
+check()
+{
+  ./tunenoform "$1" "$2" || exit 1
+}
+
+check '!(a ^ b)' '(a|!b) & (!a|b)'
+check '!(a <=> b)' '(a|b) & (!a|!b)'
+check '!(a => b)' 'a&!b'
+check '!(!a => !b)' '!a&b'
+check '!Fa' 'false R !a'
+check '!G!a' 'true U a'
+check '!(GF a => FG b)' '(0 R (1 U a)) & (0 R (1 U !b))'
+
+# Success.
+:

src/ltlvisit/Makefile.am

@@ -11,5 +11,7 @@ libltlvisit_a_SOURCES = \
   equals.hh \
   lunabbrev.hh \
   lunabbrev.cc \
+  nenoform.hh \
+  nenoform.cc \
   tunabbrev.hh \
   tunabbrev.cc

src/ltlvisit/nenoform.cc

@@ -0,0 +1,173 @@
+#include "nenoform.hh"
+#include "ltlast/allnodes.hh"
+
+namespace spot
+{
+  namespace ltl
+  {
+
+    class negative_normal_form_visitor : public const_visitor
+    {
+    public:
+      negative_normal_form_visitor(bool negated)
+	: negated_(negated)
+      {
+      }
+
+      virtual 
+      ~negative_normal_form_visitor()
+      {
+      }
+
+      formula* result() const
+      {
+	return result_;
+      }
+      
+      void 
+      visit(const atomic_prop* ap)
+      {
+	formula* f = new atomic_prop(ap->name());
+	if (negated_)
+	  result_ = new unop(unop::Not, f);
+	else
+	  result_ = f;
+      }
+
+      void 
+      visit(const constant* c)
+      {
+	if (! negated_)
+	  {
+	    result_ = new constant(c->val());
+	    return;
+	  }
+
+	switch (c->val())
+	  {
+	  case constant::True:
+	    result_ = new constant(constant::False);
+	    return;
+	  case constant::False:
+	    result_ = new constant(constant::True);
+	    return;
+	  }
+	/* Unreachable code.  */
+	assert(0);
+      }
+
+      void 
+      visit(const unop* uo)
+      {
+	const formula* f = uo->child();
+	switch (uo->op())
+	  {
+	  case unop::Not:
+	    result_ = recurse_(f, negated_ ^ true);
+	    return;
+	  case unop::X:
+	    /* !Xa == X!a */
+	    result_ = new unop(unop::X, recurse(f));
+	    return;
+	  case unop::F:
+	    /* !Fa == G!a */
+	    result_ = new unop(negated_ ? unop::G : unop::F, recurse(f));
+	    return;
+	  case unop::G:
+	    /* !Ga == F!a */
+	    result_ = new unop(negated_ ? unop::F : unop::G, recurse(f));
+	    return;
+	  }
+	/* Unreachable code.  */
+	assert(0);
+      }
+
+      void 
+      visit(const binop* bo)
+      {
+	const formula* f1 = bo->first();
+	const formula* f2 = bo->second();
+	switch (bo->op())
+	  {
+	  case binop::Xor:
+	    /* !(a ^ b) == a <=> b */
+	    result_ = new binop(negated_ ? binop::Equiv : binop::Xor,
+				recurse_(f1, false), recurse_(f2, false));
+	    return;
+	  case binop::Equiv:
+	    /* !(a <=> b) == a ^ b */
+	    result_ = new binop(negated_ ? binop::Xor : binop::Equiv,
+				recurse_(f1, false), recurse_(f2, false));
+	    return;
+	  case binop::Implies:
+	    if (negated_)
+	      /* !(a => b) == a & !b */
+	      result_ = new multop(multop::And,
+				   recurse_(f1, false), recurse_(f2, true));
+	    else
+	      result_ = new binop(binop::Implies, recurse(f1), recurse(f2));
+	    return;
+	  case binop::U:
+	    /* !(a U b) == !a R !b */
+	    result_ = new binop(negated_ ? binop::R : binop::U,
+				recurse(f1), recurse(f2));
+	    return;
+	  case binop::R:
+	    /* !(a R b) == !a U !b */
+	    result_ = new binop(negated_ ? binop::U : binop::R,
+				recurse(f1), recurse(f2));
+	    return;
+	  }
+	/* Unreachable code.  */
+	assert(0);
+      }
+
+      void 
+      visit(const multop* mo)
+      {
+	/* !(a & b & c) == !a | !b | !c  */
+	/* !(a | b | c) == !a & !b & !c  */
+	multop::type op = mo->op();
+	if (negated_)
+	  switch (op)
+	    {
+	    case multop::And:
+	      op = multop::Or;
+	      break;
+	    case multop::Or:
+	      op = multop::And;
+	      break;
+	    }
+	multop* res = new multop(op);
+	unsigned mos = mo->size();
+	for (unsigned i = 0; i < mos; ++i)
+	  res->add(recurse(mo->nth(i)));
+	result_ = res;
+      }
+	
+      formula* 
+      recurse_(const formula* f, bool negated)
+      {
+	return negative_normal_form(f, negated);
+      }
+
+      formula* 
+      recurse(const formula* f)
+      {
+	return recurse_(f, negated_);
+      }
+      
+    protected:
+      formula* result_;
+      bool negated_;
+    };
+
+    formula* 
+    negative_normal_form(const formula* f, bool negated)
+    {
+      negative_normal_form_visitor v(negated);
+      f->accept(v);
+      return v.result();
+    }
+  }
+}

src/ltlvisit/nenoform.hh

@@ -0,0 +1,18 @@
+#ifndef SPOT_LTLVISIT_NENOFORM_HH
+# define SPOT_LTLVISIT_NENOFORM_HH
+
+#include "ltlast/formula.hh"
+#include "ltlast/visitor.hh"
+
+namespace spot 
+{
+  namespace ltl
+  {
+    /* Return the negative normal form of F, i.e., all negations
+       of the formula are pushed in front of the atomic propositions.
+       If NEGATED is true, return the normal form of !F instead.  */
+    formula* negative_normal_form(const formula* f, bool negated = false);
+  }
+}
+
+#endif //  SPOT_LTLVISIT_NENOFORM_HH