diff --git a/NEWS b/NEWS index a4670f5d8..cb1129084 100644 --- a/NEWS +++ b/NEWS @@ -9,6 +9,8 @@ New in spot 2.12.0.dev (not yet released) - ltlfilt learned --pi1, --sigma1, --delta1, --pi2, --sigma2, and --delta2 to filter according to classes Π₁,Σ₁,Δ₁,Π₂,Σ₂, and Δ₂. + - ltlfilt learned --to-delta2 to transform an LTL formula into Δ₂. + Library: - restrict_dead_end_edges_here() can reduce non-determinism (but diff --git a/bin/ltlfilt.cc b/bin/ltlfilt.cc index f56074d78..2fd069dc2 100644 --- a/bin/ltlfilt.cc +++ b/bin/ltlfilt.cc @@ -38,6 +38,7 @@ #include #include #include +#include #include #include #include @@ -115,6 +116,7 @@ enum { OPT_SYNTACTIC_RECURRENCE, OPT_SYNTACTIC_SAFETY, OPT_SYNTACTIC_SI, + OPT_TO_DELTA2, OPT_UNABBREVIATE, OPT_UNIVERSAL, }; @@ -161,6 +163,8 @@ static const argp_option options[] = { "remove-x", OPT_REMOVE_X, nullptr, 0, "remove X operators (valid only for stutter-insensitive properties)", 0 }, + { "to-delta2", OPT_TO_DELTA2, nullptr, 0, + "rewrite LTL formula in Δ₂-form", 0 }, { "unabbreviate", OPT_UNABBREVIATE, "STR", OPTION_ARG_OPTIONAL, "remove all occurrences of the operators specified by STR, which " "must be a substring of \"eFGiMRW^\", where 'e', 'i', and '^' stand " @@ -349,7 +353,7 @@ static int opt_max_count = -1; static long int match_count = 0; static const char* from_ltlf = nullptr; static const char* sonf = nullptr; - +static bool to_delta2 = false; // We want all these variables to be destroyed when we exit main, to // make sure it happens before all other global variables (like the @@ -579,6 +583,9 @@ parse_opt(int key, char* arg, struct argp_state*) case OPT_STUTTER_INSENSITIVE: stutter_insensitive = true; break; + case OPT_TO_DELTA2: + to_delta2 = true; + break; case OPT_UNABBREVIATE: if (arg) unabbreviate += arg; @@ -734,6 +741,9 @@ namespace } } + if (to_delta2) + f = spot::to_delta2(f); + switch (relabeling) { case ApRelabeling: diff --git a/tests/Makefile.am b/tests/Makefile.am index 08dfbf377..bffb79ff1 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -236,6 +236,7 @@ TESTS_twa = \ core/renault.test \ core/nondet.test \ core/det.test \ + core/delta2.test \ core/semidet.test \ core/neverclaimread.test \ core/parseaut.test \ diff --git a/tests/core/delta2.test b/tests/core/delta2.test new file mode 100644 index 000000000..ee202cbd2 --- /dev/null +++ b/tests/core/delta2.test @@ -0,0 +1,30 @@ +#!/bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) by the Spot authors, see the AUTHORS file for details. +# +# 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 + +genltl --dac-p --eh-p --hkrss-p --sb-p --sejk-p \ + --stats='%F:%L,%f' > formulas.txt +ltlfilt --to-delta2 --delta2 -F formulas.txt/2 > res.txt +ltlfilt --to-delta2 -v --delta2 -F formulas.txt/2 --stats='%<' || : +test `wc -l < formulas.txt` -eq `wc -l < res.txt` + +ltlcross -F formulas.txt/2 \ + 'ltl2tgba' 'ltlfilt --to-delta2 -f %f | ltl2tgba -G >%O'