From bdae5563c638094cca9b441bfcab26e885dd9b38 Mon Sep 17 00:00:00 2001 From: Antoine Martin Date: Wed, 8 Dec 2021 11:31:54 +0100 Subject: [PATCH] ltlfilt: add --sonf and --sonf-aps flags * bin/ltlfilt.cc: Here. * NEWS: Mention new ltlfilt flags. * tests/Makefile.am, tests/core/sonf.test: Test these flags. --- NEWS | 5 +++ bin/ltlfilt.cc | 35 ++++++++++++++++++ tests/Makefile.am | 3 +- tests/core/sonf.test | 85 ++++++++++++++++++++++++++++++++++++++++++++ 4 files changed, 127 insertions(+), 1 deletion(-) create mode 100644 tests/core/sonf.test diff --git a/NEWS b/NEWS index cc0fe35a6..5e7816b7b 100644 --- a/NEWS +++ b/NEWS @@ -9,6 +9,11 @@ New in spot 2.10.4.dev (net yet released) - autfilt has a new --to-finite option, illustrated on https://spot.lrde.epita.fr/tut12.html + - ltlfilt has a new --sonf option to produce a formula's Suffix + Operator Normal Form, described in [cimatti.06.fmcad]. The + associated option --sonf-aps allows listing the newly introduced + atomic propositions. + Library: - The new function suffix_operator_normal_form() implements diff --git a/bin/ltlfilt.cc b/bin/ltlfilt.cc index cc9e0f02b..af9316192 100644 --- a/bin/ltlfilt.cc +++ b/bin/ltlfilt.cc @@ -38,6 +38,7 @@ #include #include #include +#include #include #include #include @@ -100,6 +101,8 @@ enum { OPT_SIZE_MAX, OPT_SIZE_MIN, OPT_SKIP_ERRORS, + OPT_SONF, + OPT_SONF_APS, OPT_STUTTER_INSENSITIVE, OPT_SUSPENDABLE, OPT_SYNTACTIC_GUARANTEE, @@ -127,6 +130,11 @@ static const argp_option options[] = { "negate", OPT_NEGATE, nullptr, 0, "negate each formula", 0 }, { "nnf", OPT_NNF, nullptr, 0, "rewrite formulas in negative normal form", 0 }, + { "sonf", OPT_SONF, "PREFIX", OPTION_ARG_OPTIONAL, + "rewrite formulas in suffix operator normal form", 0 }, + { "sonf-aps", OPT_SONF_APS, "FILENAME", OPTION_ARG_OPTIONAL, + "when used with --sonf, output the newly introduced atomic " + "propositions", 0 }, { "relabel", OPT_RELABEL, "abc|pnn", OPTION_ARG_OPTIONAL, "relabel all atomic propositions, alphabetically unless " \ "specified otherwise", 0 }, @@ -316,6 +324,7 @@ static range opt_nth = { 0, std::numeric_limits::max() }; static int opt_max_count = -1; static long int match_count = 0; static const char* from_ltlf = nullptr; +static const char* sonf = nullptr; // We want all these variables to be destroyed when we exit main, to @@ -327,6 +336,7 @@ static struct opt_t spot::bdd_dict_ptr dict = spot::make_bdd_dict(); spot::exclusive_ap excl_ap; std::unique_ptr output_define = nullptr; + std::unique_ptr output_sonf = nullptr; spot::formula implied_by = nullptr; spot::formula imply = nullptr; spot::formula equivalent_to = nullptr; @@ -460,6 +470,12 @@ parse_opt(int key, char* arg, struct argp_state*) case OPT_NNF: nnf = true; break; + case OPT_SONF: + sonf = arg ? arg : "sonf_"; + break; + case OPT_SONF_APS: + opt->output_sonf.reset(new output_file(arg ? arg : "-")); + break; case OPT_OBLIGATION: obligation = true; break; @@ -650,6 +666,25 @@ namespace if (nnf) f = simpl.negative_normal_form(f); + if (sonf != nullptr) + { + std::vector new_aps; + std::tie(f, new_aps) = suffix_operator_normal_form(f, sonf); + + if (opt->output_sonf + && output_format != count_output + && output_format != quiet_output) + { + for (size_t i = 0; i < new_aps.size(); ++i) + { + if (i > 0) + opt->output_sonf->ostream() << ' '; + opt->output_sonf->ostream() << new_aps[i]; + } + opt->output_sonf->ostream() << '\n'; + } + } + switch (relabeling) { case ApRelabeling: diff --git a/tests/Makefile.am b/tests/Makefile.am index a6f4ab56c..afcd0c8d2 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -198,7 +198,8 @@ TESTS_tl = \ core/stutter-ltl.test \ core/hierarchy.test \ core/mempool.test \ - core/format.test + core/format.test \ + core/sonf.test TESTS_graph = \ core/graph.test \ diff --git a/tests/core/sonf.test b/tests/core/sonf.test new file mode 100644 index 000000000..0febfc342 --- /dev/null +++ b/tests/core/sonf.test @@ -0,0 +1,85 @@ +#!/bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) 2021 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 + +cat >input < Fa) & G(b -> ({x[*]}[]-> c)) +{x[*]}[]-> F({y[*]}<>-> GFz) +<>(({{p12}[*0..3]}[]-> ((p9) || (!(p17)))) V ((true) U (p17))) +{{true} || {[*0]}}[]-> (false) +{{p14} & {{p0}[*]}}[]-> (p11) +{{{!{p6}} -> {!{p3}}}[*]}[]-> ((p3)V((p3) || ((X((false))) && ((p2)V(p18))))) +X({{true} || {[*0]}}[]-> ((p17) U ((p8) && (p17)))) +({{{p4} || {p5} || {{p16} <-> {{p15} -> {p11}}}}[*]}[]-> (false)) -> (p8) +{[*1..6]}[]-> ((p9) V ((p9) || (!((p4) && (p19))))) +X({{{[*0]} || {{{p10};{p14}}[:*2..3]}}[:*]}<>-> (p8)) +{{true} && {{p8}[*]}}<>-> (!(p10)) +<>(!(({{p7}[*1..2]}<>-> (p11)) V ((!(p9)) && ([]((p11) || (X(p10))))))) +<>({{!{{p5} || {{!{p2}} <-> {p7}}}} & {[*]}}<>-> (p17)) +{{p0} || {{{[*0..2]}[:*2]}[*]}}<>-> ((p1) && (p6)) +EOF + +cat >expected < c)) +s1&G(!s2|GFz)&G(!s0|({y[*]}<>-> s2))&G(!s3|Fs0)&G(!s1|({x[*]}[]-> s3)) +F(s0 R (1 U p17))&G(p9|!p17|!s1)&G(!s0|({p12[*0..3]}[]-> s1)) +s0&G!s1&G(!s0|({1|[*0]}[]-> s1)) +s0&G(!s0|({p14&p0[*]}[]-> p11)) +s0&G(!s1|(p3 R (p3|(X(0)&(p2 R p18)))))&G(!s0|({{!p3|p6}[*]}[]-> s1)) +Xs0&G(!s1|(p17 U (p8&p17)))&G(!s0|({1|[*0]}[]-> s1)) +(p8|s0)&G(!s0|({{p4|p5|{p16 && {p11|!p15}}|{!p11 && p15 && !p16}}[*]}<>-> s1)) +s0&G(!s1|(p9 R (!p4|p9|!p19)))&G(!s0|({[*1..6]}[]-> s1)) +G(!s0|({{[*0]|{p10;p14}[:*2..3]}[:*]}<>-> p8))&Xs0 +s0&G(!p10|!s1)&G(!s0|({1 && p8[*]}<>-> s1)) +F(s0 U (p9|F(!p11&X!p10)))&G(!p11|!s1)&G(!s0|({p7[*1..2]}[]-> s1)) +G(!s0|({{!p5 && {{!p2 && !p7}|{p2 && p7}}}&[*]}<>-> p17))&Fs0 +s0&G(!s1|(p1&p6))&G(!s0|({p0|[*0..2][:*2][*]}<>-> s1)) +EOF + +cat >expected-aps < stdout +diff expected stdout +diff expected-aps stdout-aps + +# check idempotence +ltlfilt -F expected --sonf=s --sonf-aps=stdout-aps \ + | sed 's/ \([|&]\) /\1/g' > stdout +diff expected stdout +# should be 14 empty lines, no new aps introduced this time +test "$(wc -l -m stdout-aps | awk '{print $1 " " $2}')" = "14 14"