Commit 82480720 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

ltlfilt: add a --define option

* src/bin/ltlfilt.cc: Implement it.
* src/bin/common_output.cc, src/bin/common_output.hh: export the
stream_formula function.
* src/ltltest/ltlfilt.test: Test it.
* src/ltlvisit/relabel.hh: Make it possible to clear the
relabeling map.
* NEWS, doc/org/ltlfilt.org: Mention --define.
parent 65a729ab
......@@ -47,6 +47,10 @@ New in spot 1.99b (not yet released)
- ltlfilt has a new --exclusive-ap option to constrain formulas
based on a list of mutually exclusive atomic propositions.
- ltlfilt has a new option --define to be used in conjunction with
--relabel or --relabel-bool to print the mapping between old and
new labels.
- 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
......
......@@ -184,6 +184,66 @@ Here 29 formulas were reduced into 9 formulas after relabeling of
Boolean subexpression and removing of duplicate formulas. In other
words the original set of formulas contains 9 different patterns.
An option that can be used in combination with =--relabel= or
=--relabel-bool= is =--define=. This causes the correspondence of old
a new names to be printed as a set of =#define= statements.
#+BEGIN_SRC sh :results verbatim :exports both
ltlfilt -f '(a & !b) & GF(a & !b) & FG(!c)' --relabel-bool=pnn --define --spin
#+END_SRC
#+RESULTS:
: #define p0 (a && !b)
: #define p1 (!c)
: p0 && []<>p0 && <>[]p1
This can be used for instance if you want to use some complex atomic
propositions with third-party translators that do not understand them.
For instance the following sequence show how to use =ltl3ba= to create
a neverclaim for an LTL formula containing atomic propositions that
=ltl3ba= cannot parse:
#+BEGIN_SRC sh :results verbatim :exports both
ltlfilt -f '"proc@loc1" U "proc@loc2"' --relabel=pnn --define=ltlex.def --spin |
ltl3ba -F - >ltlex.never
cat ltlex.def ltlex.never
#+END_SRC
#+RESULTS:
#+begin_example
#define p0 ((proc@loc1))
#define p1 ((proc@loc2))
never { /* p0 U p1 */
T0_init:
if
:: (!p1 && p0) -> goto T0_init
:: (p1) -> goto accept_all
fi;
accept_all:
skip
}
#+end_example
As a side note, the tool [[file:ltldo.org][=ltldo=]] might be a simpler answer to this syntactic problem:
#+BEGIN_SRC sh :results verbatim :exports both
ltldo ltl3ba -f '"proc@loc1" U "proc@loc2"' --spin
#+END_SRC
#+RESULTS:
: never {
: T0_init:
: if
: :: ((proc@loc1) && (!(proc@loc2))) -> goto T0_init
: :: ((proc@loc2)) -> goto accept_all
: fi;
: accept_all:
: skip
: }
This case also relabels the formula before calling =ltl3ba=, and it
then rename all the atomic propositions in the output.
* Filtering
=ltlfilt= supports many ways to filter formulas:
......
......@@ -77,7 +77,7 @@ report_not_ltl(const spot::ltl::formula* f,
error(2, 0, msg, s.c_str(), syn);
}
static void
std::ostream&
stream_formula(std::ostream& out,
const spot::ltl::formula* f, const char* filename, int linenum)
{
......@@ -114,6 +114,7 @@ stream_formula(std::ostream& out,
case quiet_output:
break;
}
return out;
}
static void
......
......@@ -40,6 +40,11 @@ extern const struct argp output_argp;
int parse_opt_output(int key, char* arg, struct argp_state* state);
// Low-level output
std::ostream&
stream_formula(std::ostream& out,
const spot::ltl::formula* f, const char* filename, int linenum);
void output_formula_checked(const spot::ltl::formula* f,
const char* filename = 0, int linenum = 0,
const char* prefix = 0, const char* suffix = 0);
......
......@@ -42,6 +42,7 @@
#include "ltlvisit/remove_x.hh"
#include "ltlvisit/apcollect.hh"
#include "ltlvisit/exclusive.hh"
#include "ltlvisit/tostring.hh"
#include "ltlast/unop.hh"
#include "ltlast/multop.hh"
#include "tgbaalgos/ltl2tgba_fm.hh"
......@@ -62,6 +63,7 @@ enum {
OPT_BOOLEAN_TO_ISOP,
OPT_BSIZE_MAX,
OPT_BSIZE_MIN,
OPT_DEFINE,
OPT_DROP_ERRORS,
OPT_EQUIVALENT_TO,
OPT_EXCLUSIVE_AP,
......@@ -112,6 +114,9 @@ static const argp_option options[] =
{ "relabel-bool", OPT_RELABEL_BOOL, "abc|pnn", OPTION_ARG_OPTIONAL,
"relabel Boolean subexpressions, alphabetically unless " \
"specified otherwise", 0 },
{ "define", OPT_DEFINE, "[FILENAME]", OPTION_ARG_OPTIONAL,
"when used with --relabel or --relabel-bool, output the relabeling map "
"using #define statements", 0 },
{ "remove-wm", OPT_REMOVE_WM, 0, 0,
"rewrite operators W and M using U and R", 0 },
{ "boolean-to-isop", OPT_BOOLEAN_TO_ISOP, 0, 0,
......@@ -247,6 +252,8 @@ static unsigned ap_n = 0;
static int opt_max_count = -1;
static long int match_count = 0;
static spot::exclusive_ap excl_ap;
static std::unique_ptr<output_file> output_define = nullptr;
static const spot::ltl::formula* implied_by = 0;
static const spot::ltl::formula* imply = 0;
......@@ -302,6 +309,9 @@ parse_opt(int key, char* arg, struct argp_state*)
case OPT_BSIZE_MAX:
bsize_max = to_int(arg);
break;
case OPT_DEFINE:
output_define.reset(new output_file(arg ? arg : "-"));
break;
case OPT_DROP_ERRORS:
error_style = drop_errors;
break;
......@@ -427,6 +437,7 @@ namespace
public:
spot::ltl::ltl_simplifier& simpl;
fset_t unique_set;
spot::ltl::relabeling_map relmap;
~ltl_processor()
{
......@@ -531,14 +542,16 @@ namespace
{
case ApRelabeling:
{
const spot::ltl::formula* res = spot::ltl::relabel(f, style);
relmap.clear();
auto res = spot::ltl::relabel(f, style, &relmap);
f->destroy();
f = res;
break;
}
case BseRelabeling:
{
const spot::ltl::formula* res = spot::ltl::relabel_bse(f, style);
relmap.clear();
auto res = spot::ltl::relabel_bse(f, style, &relmap);
f->destroy();
f = res;
break;
......@@ -628,6 +641,19 @@ namespace
if (matched)
{
if (output_define
&& output_format != count_output
&& output_format != quiet_output)
{
// Sort the formulas alphabetically.
std::map<std::string, const spot::ltl::formula*> m;
for (auto& p: relmap)
m.emplace(to_string(p.first), p.second);
for (auto& p: m)
stream_formula(output_define->ostream()
<< "#define " << p.first << " (",
p.second, filename, linenum) << ")\n";
}
one_match = true;
output_formula_checked(f, filename, linenum, prefix, suffix);
++match_count;
......
......@@ -171,6 +171,57 @@ EOF
run 0 ../../bin/ltlfilt -u --nnf --relabel-bool=pnn in >out
diff exp out
cat >exp <<EOF
#define p0 (a && c)
#define p1 (b)
p0 && Xp1
#define p0 (a)
#define p1 (b)
#define p2 (c)
p0 && p1 && []<>(p0 || p2) && <>[](p0 || p2)
#define p0 (b)
#define p1 (a || c)
p0 && []<>p1 && <>[]p1
#define p0 (h || i)
#define p1 (d && e)
#define p2 (!c)
#define p3 (f)
p0 || []p1 || <>[](p2 || Xp3)
EOF
run 0 ../../bin/ltlfilt -s -u --nnf --relabel-bool=pnn --define in >out
diff exp out
cat >exp <<EOF
#define p0 ((a=1))
#define p1 ((c=1))
#define p2 ((b=1))
(p0=1) * (p1=1) * (X(p2=1))
#define p0 ((a=1))
#define p1 ((b=1))
#define p2 ((c=1))
(p0=1) * (p1=1) * (G(F((p0=1) + (p2=1)))) * (F(G((p0=1) + (p2=1))))
#define p0 ((b=1))
#define p1 ((a=1))
#define p2 ((c=1))
(p0=1) * (G(F((p1=1) + (p2=1)))) * (F(G((p1=1) + (p2=1))))
#define p0 ((h=1))
#define p1 ((i=1))
#define p2 ((d=1))
#define p3 ((e=1))
#define p4 ((c=1))
#define p5 ((f=1))
(p0=1) + (p1=1) + (G((p2=1) * (p3=1))) + (F(G((p4=0) + (X(p5=1)))))
#define p0 ((b=1))
#define p1 ((e=1))
#define p2 ((f=1))
#define p3 ((g=1))
#define p4 ((c=1))
(p0=1) * (p1=1) * ((p2=1) + (p3=1)) * (X(p4=0))
EOF
run 0 ../../bin/ltlfilt -p --wring -u --nnf --relabel=pnn --define in >out
diff exp out
SPOT_STUTTER_CHECK=0 \
../../bin/ltlfilt --stutter-invariant -f '!{a:b*:c}' 2> stderr && exit 1
test $? = 2
......
// -*- coding: utf-8 -*-
// Copyright (C) 2012, 2013 Laboratoire de Recherche et
// Copyright (C) 2012, 2013, 2015 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
......@@ -33,10 +33,17 @@ namespace spot
const formula*,
ptr_hash<formula>>
{
~relabeling_map()
void clear()
{
for (iterator i = begin(); i != end(); ++i)
i->second->destroy();
this->std::unordered_map<const formula*,
const formula*, ptr_hash<formula>>::clear();
}
~relabeling_map()
{
clear();
}
};
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment