diff --git a/NEWS b/NEWS
index 54b2d5922..7be115c7c 100644
--- a/NEWS
+++ b/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
diff --git a/src/bin/ltlfilt.cc b/src/bin/ltlfilt.cc
index 7d0b039f1..ace159e00 100644
--- a/src/bin/ltlfilt.cc
+++ b/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:
- eventual = true;
+ case OPT_EXCLUSIVE_AP:
+ 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,19 +646,20 @@ main(int argc, char** argv)
const argp ap = { options, parse_opt, "[FILENAME[/COL]...]",
argp_program_doc, children, 0, 0 };
- if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, 0, 0))
- exit(err);
-
- if (jobs.empty())
- jobs.emplace_back("-", 1);
-
- if (boolean_to_isop && simplification_level == 0)
- simplification_level = 1;
- spot::ltl::ltl_simplifier_options opt(simplification_level);
- opt.boolean_to_isop = boolean_to_isop;
- spot::ltl::ltl_simplifier simpl(opt);
try
{
+ if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, 0, 0))
+ exit(err);
+
+ if (jobs.empty())
+ jobs.emplace_back("-", 1);
+
+ if (boolean_to_isop && simplification_level == 0)
+ simplification_level = 1;
+ spot::ltl::ltl_simplifier_options opt(simplification_level);
+ opt.boolean_to_isop = boolean_to_isop;
+ spot::ltl::ltl_simplifier simpl(opt);
+
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;
diff --git a/src/ltltest/Makefile.am b/src/ltltest/Makefile.am
index 06e4ea9f3..9850d3d00 100644
--- a/src/ltltest/Makefile.am
+++ b/src/ltltest/Makefile.am
@@ -98,6 +98,7 @@ TESTS = \
ltlgrind.test \
ltlcrossgrind.test \
ltlfilt.test \
+ exclusive.test \
latex.test \
lbt.test \
lenient.test \
diff --git a/src/ltltest/exclusive.test b/src/ltltest/exclusive.test
new file mode 100755
index 000000000..82b8c02eb
--- /dev/null
+++ b/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 .
+
+
+. ./defs || exit 1
+
+set -e
+
+cat >formulas <expected <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
diff --git a/src/ltlvisit/Makefile.am b/src/ltlvisit/Makefile.am
index e1417b284..cae72d8e2 100644
--- a/src/ltlvisit/Makefile.am
+++ b/src/ltlvisit/Makefile.am
@@ -1,6 +1,6 @@
## -*- coding: utf-8 -*-
-## Copyright (C) 2010, 2011, 2012, 2013, 2014 Laboratoire de Recherche
-## et Developpement de l'Epita (LRDE).
+## Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire de
+## 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 \
diff --git a/src/ltlvisit/exclusive.cc b/src/ltlvisit/exclusive.cc
new file mode 100644
index 000000000..857480863
--- /dev/null
+++ b/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 .
+
+#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
+ split_aps(const char* arg)
+ {
+ auto& env = spot::ltl::default_environment::instance();
+ std::vector 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(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(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 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 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);
+ }
+}
diff --git a/src/ltlvisit/exclusive.hh b/src/ltlvisit/exclusive.hh
new file mode 100644
index 000000000..cd9d20ff6
--- /dev/null
+++ b/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 .
+
+#pragma once
+
+#include
+#include "ltlast/atomic_prop.hh"
+#include "ltlast/formula.hh"
+
+namespace spot
+{
+ class SPOT_API exclusive_ap
+ {
+ std::vector> groups;
+ public:
+ ~exclusive_ap();
+#ifndef SWIG
+ void add_group(std::vector ap);
+#endif
+ void add_group(const char* ap_csv);
+
+ bool empty() const
+ {
+ return groups.empty();
+ }
+
+ const ltl::formula* constrain(const ltl::formula* f) const;
+ };
+}