diff --git a/NEWS b/NEWS index c00a8f195..a2450b955 100644 --- a/NEWS +++ b/NEWS @@ -42,16 +42,20 @@ New in spot 2.0.3a (not yet released) 'b U (a & b)' instead. The operators that can be listed between brackets are the same as those of ltlfilt --unabbreviate option. - * genltl has three new options: --dac-patterns=1..45, + * genltl has learned three new families: --dac-patterns=1..45, --eh-patterns=1..12, and --sb-patterns=1..27. Unlike other options these do not output scalable patterns, but simply a list of formulas appearing in these three papers: Dwyer et al (FMSP'98), Etessami & Holzmann (Concur'00), Somenzi & Bloem (CAV'00). + * genltl has two additional options, --positive and --negative, to + control wether formulas should be output after negation or not (or + both). + * Arguments passed to -x (in ltl2tgba, ltl2tgta, autfilt, dstar2tgba) that are not used are now reported as they might be typos. This ocurred a couple of times in our test-suite. A similar - check is done the the arguments of autfilt --sat-minimize=... + check is done for the arguments of autfilt --sat-minimize=... Library: diff --git a/bin/genltl.cc b/bin/genltl.cc index 7cf135ef9..4448787d5 100644 --- a/bin/genltl.cc +++ b/bin/genltl.cc @@ -161,6 +161,8 @@ enum { OPT_U_LEFT, OPT_U_RIGHT, LAST_CLASS, + OPT_POSITIVE, + OPT_NEGATIVE, }; const char* const class_name[LAST_CLASS] = @@ -251,6 +253,12 @@ static const argp_option options[] = RANGE_DOC, /**************************************************/ { nullptr, 0, nullptr, 0, "Output options:", -20 }, + { "negative", OPT_NEGATIVE, nullptr, 0, + "output the negated versions of all formulas", 0 }, + OPT_ALIAS(negated), + { "positive", OPT_POSITIVE, nullptr, 0, + "output the positive versions of all formulas (done by default, unless" + " --negative is specified without --positive)", 0 }, { nullptr, 0, nullptr, 0, "The FORMAT string passed to --format may use " "the following interpreted sequences:", -19 }, { "%f", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, @@ -273,7 +281,8 @@ struct job typedef std::vector jobs_t; static jobs_t jobs; - +bool opt_positive = false; +bool opt_negative = false; const struct argp_child children[] = { @@ -346,6 +355,12 @@ parse_opt(int key, char* arg, struct argp_state*) else enqueue_job(key, 1, 27); break; + case OPT_POSITIVE: + opt_positive = true; + break; + case OPT_NEGATIVE: + opt_negative = true; + break; default: return ARGP_ERR_UNKNOWN; } @@ -1042,7 +1057,16 @@ output_pattern(int pattern, int n) if (output_format == lbt_output && !f.has_lbt_atomic_props()) f = relabel(f, Pnn); - output_formula_checked(f, class_name[pattern - 1], n); + if (opt_positive || !opt_negative) + { + output_formula_checked(f, class_name[pattern - 1], n); + } + if (opt_negative) + { + std::string tmp = "!"; + tmp += class_name[pattern - 1]; + output_formula_checked(spot::formula::Not(f), tmp.c_str(), n); + } } static void diff --git a/tests/Makefile.am b/tests/Makefile.am index be1649ff5..84f541387 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -151,6 +151,7 @@ TESTS_tl = \ core/length.test \ core/equals.test \ core/tostring.test \ + core/genltl.test \ core/lunabbrev.test \ core/tunabbrev.test \ core/nenoform.test \ diff --git a/tests/core/genltl.test b/tests/core/genltl.test new file mode 100755 index 000000000..4e0eb2c99 --- /dev/null +++ b/tests/core/genltl.test @@ -0,0 +1,80 @@ +#!/bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) 2016 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 +set -e + +run 0 genltl --dac=1..5 --eh=1..5 --pos --neg --format="%F:%L %f" >output +cat >expected < (!p1 U p0) +!dac-patterns:2 !(Fp0 -> (!p1 U p0)) +dac-patterns:3 G(p0 -> G!p1) +!dac-patterns:3 !G(p0 -> G!p1) +dac-patterns:4 G((p0 & !p1 & Fp1) -> (!p2 U p1)) +!dac-patterns:4 !G((p0 & !p1 & Fp1) -> (!p2 U p1)) +dac-patterns:5 G((p0 & !p1) -> (!p2 W p1)) +!dac-patterns:5 !G((p0 & !p1) -> (!p2 W p1)) +eh-patterns:1 p0 U (p1 & Gp2) +!eh-patterns:1 !(p0 U (p1 & Gp2)) +eh-patterns:2 p0 U (p1 & X(p2 U p3)) +!eh-patterns:2 !(p0 U (p1 & X(p2 U p3))) +eh-patterns:3 p0 U (p1 & X(p2 & F(p3 & XF(p4 & XF(p5 & XFp6))))) +!eh-patterns:3 !(p0 U (p1 & X(p2 & F(p3 & XF(p4 & XF(p5 & XFp6)))))) +eh-patterns:4 F(p0 & XGp1) +!eh-patterns:4 !F(p0 & XGp1) +eh-patterns:5 F(p0 & X(p1 & XFp2)) +!eh-patterns:5 !F(p0 & X(p1 & XFp2)) +EOF +diff expected output + +genltl --dac=1..5 --eh=1..5 --neg --format="%L %f" >output +cat >expected < (!p1 U p0)) +3 !G(p0 -> G!p1) +4 !G((p0 & !p1 & Fp1) -> (!p2 U p1)) +5 !G((p0 & !p1) -> (!p2 W p1)) +1 !(p0 U (p1 & Gp2)) +2 !(p0 U (p1 & X(p2 U p3))) +3 !(p0 U (p1 & X(p2 & F(p3 & XF(p4 & XF(p5 & XFp6)))))) +4 !F(p0 & XGp1) +5 !F(p0 & X(p1 & XFp2)) +EOF +diff expected output + +genltl --dac=1..5 --eh=1..5 --pos --format="%f" >output +cat >expected < (!p1 U p0) +G(p0 -> G!p1) +G((p0 & !p1 & Fp1) -> (!p2 U p1)) +G((p0 & !p1) -> (!p2 W p1)) +p0 U (p1 & Gp2) +p0 U (p1 & X(p2 U p3)) +p0 U (p1 & X(p2 & F(p3 & XF(p4 & XF(p5 & XFp6))))) +F(p0 & XGp1) +F(p0 & X(p1 & XFp2)) +EOF +diff expected output + +genltl --dac=1..5 --eh=1..5 >output2 +diff output output2