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.
This commit is contained in:
parent
0505ee9310
commit
bdae5563c6
4 changed files with 127 additions and 1 deletions
5
NEWS
5
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
|
||||
|
|
|
|||
|
|
@ -38,6 +38,7 @@
|
|||
#include <spot/misc/hash.hh>
|
||||
#include <spot/misc/timer.hh>
|
||||
#include <spot/tl/simplify.hh>
|
||||
#include <spot/tl/sonf.hh>
|
||||
#include <spot/tl/length.hh>
|
||||
#include <spot/tl/relabel.hh>
|
||||
#include <spot/tl/unabbrev.hh>
|
||||
|
|
@ -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<int>::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_file> output_define = nullptr;
|
||||
std::unique_ptr<output_file> 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<std::string> 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:
|
||||
|
|
|
|||
|
|
@ -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 \
|
||||
|
|
|
|||
85
tests/core/sonf.test
Normal file
85
tests/core/sonf.test
Normal file
|
|
@ -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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
. ./defs
|
||||
set -e
|
||||
|
||||
cat >input <<EOF
|
||||
G(c -> 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 <<EOF
|
||||
G(!c|Fa)&G(!b|({x[*]}[]-> 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 <<EOF
|
||||
|
||||
s0 s1 s2 s3
|
||||
s0 s1
|
||||
s0 s1
|
||||
s0
|
||||
s0 s1
|
||||
s0 s1
|
||||
s0 s1
|
||||
s0 s1
|
||||
s0
|
||||
s0 s1
|
||||
s0 s1
|
||||
s0
|
||||
s0 s1
|
||||
EOF
|
||||
|
||||
ltlfilt -F input --sonf=s --sonf-aps=stdout-aps \
|
||||
| sed 's/ \([|&]\) /\1/g' > 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"
|
||||
Loading…
Add table
Add a link
Reference in a new issue