ltlfilt: add a --exclusive-ap option

* src/ltlvisit/exclusive.cc, src/ltlvisit/exclusive.hh: New files.
* src/ltlvisit/Makefile.am: Add them.
* src/bin/ltlfilt.cc: Implement the --exclusive-ap option.
* NEWS: Mention it.
* src/ltltest/exclusive.test: New file.
* src/ltltest/Makefile.am: Add it.

NEWS

@@ -44,6 +44,9 @@ New in spot 1.99b (not yet released)
     - ltlfilt has a new --count option to count the number of matching
       automata.
 
+    - ltlfilt has a new --exclusive-ap option to constrain formulas
+      based on a list of mutually exclusive atomic propositions.
+
     - all tools that produce formulas or automata now have an --output
       (a.k.a. -o) option to redirect that output to a file instead of
       standard output.  The name of this file can be constructed using

src/bin/ltlfilt.cc

@@ -41,6 +41,7 @@
 #include "ltlvisit/wmunabbrev.hh"
 #include "ltlvisit/remove_x.hh"
 #include "ltlvisit/apcollect.hh"
+#include "ltlvisit/exclusive.hh"
 #include "ltlast/unop.hh"
 #include "ltlast/multop.hh"
 #include "tgbaalgos/ltl2tgba_fm.hh"
@@ -56,13 +57,14 @@ Exit status:\n\
   2  if any error has been reported";
 
 enum {
-  OPT_AP_N = 1,
+  OPT_AP_N = 256,
   OPT_BOOLEAN,
   OPT_BOOLEAN_TO_ISOP,
   OPT_BSIZE_MAX,
   OPT_BSIZE_MIN,
   OPT_DROP_ERRORS,
   OPT_EQUIVALENT_TO,
+  OPT_EXCLUSIVE_AP,
   OPT_EVENTUAL,
   OPT_GUARANTEE,
   OPT_IGNORE_ERRORS,
@@ -118,6 +120,11 @@ static const argp_option options[] =
     { "remove-x", OPT_REMOVE_X, 0, 0,
       "remove X operators (valid only for stutter-insensitive properties)",
       0 },
+    { "exclusive-ap", OPT_EXCLUSIVE_AP, "AP,AP,...", 0,
+      "if any of those APs occur in the formula, add a term ensuring "
+      "two of them may not be true at the same time.  Use this option "
+      "multiple times to declare independent groups of exclusive "
+      "propositions.", 0 },
     DECLARE_OPT_R,
     LEVEL_DOC(4),
     /**************************************************/
@@ -239,6 +246,7 @@ static bool ap = false;
 static unsigned ap_n = 0;
 static int opt_max_count = -1;
 static long int match_count = 0;
+static spot::exclusive_ap excl_ap;
 
 static const spot::ltl::formula* implied_by = 0;
 static const spot::ltl::formula* imply = 0;
@@ -254,8 +262,6 @@ parse_formula_arg(const std::string& input)
   return f;
 }
 
-
-
 static int
 parse_opt(int key, char* arg, struct argp_state*)
 {
@@ -299,6 +305,9 @@ parse_opt(int key, char* arg, struct argp_state*)
     case OPT_DROP_ERRORS:
       error_style = drop_errors;
       break;
+    case OPT_EVENTUAL:
+      eventual = true;
+      break;
     case OPT_EQUIVALENT_TO:
       {
 	if (equivalent_to)
@@ -306,8 +315,8 @@ parse_opt(int key, char* arg, struct argp_state*)
 	equivalent_to = parse_formula_arg(arg);
 	break;
       }
-    case OPT_EVENTUAL:
+    case OPT_EXCLUSIVE_AP:
-      eventual = true;
+      excl_ap.add_group(arg);
       break;
     case OPT_GUARANTEE:
       guarantee = obligation = true;
@@ -545,6 +554,13 @@ namespace
 	  f = res;
 	}
 
+      if (!excl_ap.empty())
+	{
+	  auto res = excl_ap.constrain(f);
+	  f->destroy();
+	  f = res;
+	}
+
       bool matched = true;
 
       matched &= !ltl || f->is_ltl_formula();
@@ -630,6 +646,8 @@ main(int argc, char** argv)
   const argp ap = { options, parse_opt, "[FILENAME[/COL]...]",
 		    argp_program_doc, children, 0, 0 };
 
+  try
+    {
       if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, 0, 0))
 	exit(err);
 
@@ -641,8 +659,7 @@ main(int argc, char** argv)
       spot::ltl::ltl_simplifier_options opt(simplification_level);
       opt.boolean_to_isop = boolean_to_isop;
       spot::ltl::ltl_simplifier simpl(opt);
-  try
+
-    {
       ltl_processor processor(simpl);
       if (processor.run())
 	return 2;
@@ -651,6 +668,10 @@ main(int argc, char** argv)
     {
       error(2, 0, "%s", e.what());
     }
+  catch (const std::invalid_argument& e)
+    {
+      error(2, 0, "%s", e.what());
+    }
 
   if (output_format == count_output)
     std::cout << match_count << std::endl;

src/ltltest/Makefile.am

@@ -98,6 +98,7 @@ TESTS = \
   ltlgrind.test \
   ltlcrossgrind.test \
   ltlfilt.test \
+  exclusive.test \
   latex.test \
   lbt.test \
   lenient.test \

src/ltltest/exclusive.test

@@ -0,0 +1,56 @@
+#! /bin/sh
+# -*- coding: utf-8 -*-
+# Copyright (C) 2015 Laboratoire de Recherche et Développement de
+# l'Epita (LRDE).
+#
+# 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 3 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 this program.  If not, see <http://www.gnu.org/licenses/>.
+
+
+. ./defs || exit 1
+
+set -e
+
+cat >formulas <<EOF
+GFa
+a U b
+a U b U c
+a U b U d U e
+a U b U c U d U e
+EOF
+
+cat >expected <<EOF
+GFa
+(a U b) & G!(a & b)
+(a U (b U c)) & G(!(a & b) & !(a & c) & !(b & c))
+(a U (b U (d U e))) & G(!(a & b) & !(d & e))
+(a U (b U (c U (d U e)))) & G(!(a & b) & !(a & c) & !(b & c) & !(d & e))
+EOF
+
+run 0 ../../bin/ltlfilt --exclusive-ap=a,b,c --exclusive-ap=d,e formulas >out
+cat out
+diff out expected
+
+run 0 ../../bin/ltlfilt --exclusive-ap='"a" ,b, "c" ' --exclusive-ap=' d , e' \
+    formulas >out
+cat out
+diff out expected
+
+../../bin/ltlfilt --exclusive-ap='"a","b' 2>stderr && exit 1
+grep 'missing closing ."' stderr
+../../bin/ltlfilt --exclusive-ap='a,,b' 2>stderr && exit 1
+grep "unexpected ',' in a,,b" stderr
+../../bin/ltlfilt --exclusive-ap='"a"b' 2>stderr && exit 1
+grep "unexpected character 'b' in \"a\"b" stderr

src/ltlvisit/Makefile.am

@@ -1,6 +1,6 @@
 ## -*- coding: utf-8 -*-
-## Copyright (C) 2010, 2011, 2012, 2013, 2014 Laboratoire de Recherche
+## Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire de
-## et Developpement de l'Epita (LRDE).
+## Recherche et Developpement de l'Epita (LRDE).
 ## Copyright (C) 2004, 2005, 2006 Laboratoire d'Informatique de Paris
 ## 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
 ## Université Pierre et Marie Curie.
@@ -31,6 +31,7 @@ ltlvisit_HEADERS = \
   clone.hh \
   dotty.hh \
   dump.hh \
+  exclusive.hh \
   lbt.hh \
   length.hh \
   lunabbrev.hh \
@@ -54,6 +55,7 @@ libltlvisit_la_SOURCES = \
   clone.cc \
   dotty.cc \
   dump.cc \
+  exclusive.cc \
   lbt.cc \
   length.cc \
   lunabbrev.cc \

src/ltlvisit/exclusive.cc

@@ -0,0 +1,161 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2015 Laboratoire de Recherche et Développement de
+// l'Epita (LRDE).
+//
+// 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 3 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 this program.  If not, see <http://www.gnu.org/licenses/>.
+
+#include "exclusive.hh"
+#include "ltlenv/defaultenv.hh"
+#include "ltlast/multop.hh"
+#include "ltlast/unop.hh"
+#include "ltlast/constant.hh"
+#include "misc/casts.hh"
+#include "apcollect.hh"
+
+namespace spot
+{
+  exclusive_ap::~exclusive_ap()
+  {
+    for (auto& g: groups)
+      for (auto ap: g)
+	ap->destroy();
+  }
+
+  namespace
+  {
+    static const std::vector<const spot::ltl::atomic_prop*>
+    split_aps(const char* arg)
+    {
+      auto& env = spot::ltl::default_environment::instance();
+      std::vector<const spot::ltl::atomic_prop*> group;
+      auto start = arg;
+      while (*start)
+	{
+	  while (*start == ' ' || *start == '\t')
+	    ++start;
+	  if (!*start)
+	    break;
+	  if (*start == ',')
+	    {
+	      std::string s = "unexpected ',' in ";
+	      s += arg;
+	      throw std::invalid_argument(s);
+	    }
+	  if (*start == '"')
+	    {
+	      ++start;
+	      auto end = start;
+	      while (*end && *end != '"')
+		{
+		  if (*end == '\\')
+		    ++end;
+		  ++end;
+		}
+	      if (!*end)
+		{
+		  std::string s = "missing closing '\"' in ";
+		  s += arg;
+		  throw std::invalid_argument(s);
+		}
+	      std::string ap(start, end - start);
+	      auto* t = env.require(ap);
+	      group.push_back(down_cast<const spot::ltl::atomic_prop*>(t));
+	      do
+		++end;
+	      while (*end == ' ' || *end == '\t');
+	      if (*end && *end != ',')
+		{
+		  std::string s = "unexpected character '";
+		  s += *end;
+		  s += "' in ";
+		  s += arg;
+		  throw std::invalid_argument(s);
+		}
+	      if (*end == ',')
+		++end;
+	      start = end;
+	    }
+	  else
+	    {
+	      auto end = start;
+	      while (*end && *end != ',')
+		++end;
+	      auto rend = end;
+	      while (rend > start && (rend[-1] == ' ' || rend[-1] == '\t'))
+		--rend;
+	      std::string ap(start, rend - start);
+	      auto* t = env.require(ap);
+	      group.push_back(down_cast<const spot::ltl::atomic_prop*>(t));
+	      if (*end == ',')
+		start = end + 1;
+	      else
+		break;
+	    }
+	}
+      return group;
+    }
+  }
+
+  void exclusive_ap::add_group(const char* ap_csv)
+  {
+    add_group(split_aps(ap_csv));
+  }
+
+  void exclusive_ap::add_group(std::vector<const ltl::atomic_prop*> ap)
+  {
+    groups.push_back(ap);
+  }
+
+  namespace
+  {
+    const ltl::formula*
+    nand(const ltl::formula* lhs, const ltl::formula* rhs)
+    {
+      auto f = ltl::multop::instance(ltl::multop::And,
+				     lhs->clone(), rhs->clone());
+      return ltl::unop::instance(ltl::unop::Not, f);
+    }
+  }
+
+  const ltl::formula*
+  exclusive_ap::constrain(const ltl::formula* f) const
+  {
+    spot::ltl::atomic_prop_set* s = atomic_prop_collect(f);
+
+    std::vector<const ltl::atomic_prop*> group;
+    ltl::multop::vec* v = new ltl::multop::vec;
+
+    for (auto& g: groups)
+      {
+	group.clear();
+
+	for (auto ap: g)
+	  if (s->find(ap) != s->end())
+	    group.push_back(ap);
+
+	unsigned s = group.size();
+	for (unsigned j = 0; j < s; ++j)
+	  for (unsigned k = j + 1; k < s; ++k)
+	    v->push_back(nand(group[j], group[k]));
+      };
+
+    delete s;
+
+    auto* c = ltl::unop::instance(ltl::unop::G,
+				  ltl::multop::instance(ltl::multop::And, v));
+    return ltl::multop::instance(ltl::multop::And, f->clone(), c);
+  }
+}

src/ltlvisit/exclusive.hh

@@ -0,0 +1,45 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2015 Laboratoire de Recherche et Développement de
+// l'Epita (LRDE).
+//
+// 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 3 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 this program.  If not, see <http://www.gnu.org/licenses/>.
+
+#pragma once
+
+#include <vector>
+#include "ltlast/atomic_prop.hh"
+#include "ltlast/formula.hh"
+
+namespace spot
+{
+  class SPOT_API exclusive_ap
+  {
+    std::vector<std::vector<const ltl::atomic_prop*>> groups;
+  public:
+    ~exclusive_ap();
+#ifndef SWIG
+    void add_group(std::vector<const ltl::atomic_prop*> ap);
+#endif
+    void add_group(const char* ap_csv);
+
+    bool empty() const
+    {
+      return groups.empty();
+    }
+
+    const ltl::formula* constrain(const ltl::formula* f) const;
+  };
+}