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

genltl: add support for --sejk-f=n,m

Together with the previous patch, this Fixes #353.

Implementing this required to extend our interface two support
two-parameter patterns.

* spot/gen/formulas.cc, spot/gen/formulas.hh: Implement it.
* bin/genltl.cc: Add --sejk-f.
* bin/common_output.cc, bin/common_output.hh: Adjust to handle
"line numbers" that are not integers (e.g., "3,2"), since those
are used to display pattern parameters.
* bin/ltlfilt.cc: Adjust.
* python/spot/gen.i: Add support for two-parameters patterns.
* tests/core/genltl.test, tests/python/gen.ipynb: Augment.
* NEWS: Mention it.
parent c76df95c
......@@ -22,7 +22,9 @@ New in spot 2.5.3.dev (not yet released)
product to avoid exceeding the number of supported
acceptance sets.
- genltl learned to generate three new families of formulas:
- genltl learned to generate four new families of formulas:
--sejk-f=RANGE[,RANGE] f(0,j)=(GFa0 U X^j(b)), f(i,j)=(GFai U
G(f(i-1,j)))
--sejk-j=RANGE (GFa1&...&GFan) -> (GFb1&...&GFbn)
--sejk-k=RANGE (GFa1|FGb1)&...&(GFan|FGbn)
--sejk-patterns[=RANGE] φ₁,φ₂,φ₃ from Sikert et al's [CAV'16]
......
......@@ -78,20 +78,21 @@ const struct argp output_argp = { options, parse_opt_output,
static
void
report_not_ltl(spot::formula f,
const char* filename, int linenum, const char* syn)
const char* filename, const char* linenum, const char* syn)
{
std::string s = spot::str_psl(f);
static const char msg[] =
"formula '%s' cannot be written %s's syntax because it is not LTL";
if (filename)
error_at_line(2, 0, filename, linenum, msg, s.c_str(), syn);
error_at_line(2, 0, filename, atoi(linenum), msg, s.c_str(), syn);
else
error(2, 0, msg, s.c_str(), syn);
}
std::ostream&
stream_formula(std::ostream& out,
spot::formula f, const char* filename, int linenum)
spot::formula f, const char* filename,
const char* linenum)
{
switch (output_format)
{
......@@ -132,7 +133,8 @@ stream_formula(std::ostream& out,
static void
stream_escapable_formula(std::ostream& os,
spot::formula f,
const char* filename, int linenum)
const char* filename,
const char* linenum)
{
if (escape_csv)
{
......@@ -155,7 +157,7 @@ namespace
{
spot::formula f;
const char* filename;
int line;
const char* line;
const char* prefix;
const char* suffix;
};
......@@ -283,7 +285,7 @@ namespace
printable_formula_with_location fl_;
printable_timer timer_;
spot::printable_value<const char*> filename_;
spot::printable_value<int> line_;
spot::printable_value<const char*> line_;
spot::printable_value<const char*> prefix_;
spot::printable_value<const char*> suffix_;
spot::printable_value<int> size_;
......@@ -348,9 +350,9 @@ parse_opt_output(int key, char* arg, struct argp_state*)
static void
output_formula(std::ostream& out,
spot::formula f, spot::process_timer* ptimer = nullptr,
const char* filename = nullptr, int linenum = 0,
const char* prefix = nullptr, const char* suffix = nullptr)
spot::formula f, spot::process_timer* ptimer,
const char* filename, const char* linenum,
const char* prefix, const char* suffix)
{
if (!format)
{
......@@ -392,7 +394,7 @@ output_formula(std::ostream& out,
void
output_formula_checked(spot::formula f, spot::process_timer* ptimer,
const char* filename, int linenum,
const char* filename, const char* linenum,
const char* prefix, const char* suffix)
{
if (output_format == count_output)
......@@ -422,3 +424,14 @@ output_formula_checked(spot::formula f, spot::process_timer* ptimer,
// (like disk full or broken pipe with SIGPIPE ignored).
check_cout();
}
void output_formula_checked(spot::formula f,
spot::process_timer* ptimer,
const char* filename, int linenum,
const char* prefix,
const char* suffix)
{
output_formula_checked(f, ptimer, filename,
std::to_string(linenum).c_str(),
prefix, suffix);
}
......@@ -75,10 +75,17 @@ int parse_opt_output(int key, char* arg, struct argp_state* state);
// Low-level output
std::ostream&
stream_formula(std::ostream& out,
spot::formula f, const char* filename, int linenum);
spot::formula f, const char* filename, const char* linenum);
void output_formula_checked(spot::formula f,
spot::process_timer* ptimer = nullptr,
const char* filename = nullptr, int linenum = 0,
const char* filename = nullptr,
const char* linenum = nullptr,
const char* prefix = nullptr,
const char* suffix = nullptr);
void output_formula_checked(spot::formula f,
spot::process_timer* ptimer,
const char* filename, int linenum,
const char* prefix = nullptr,
const char* suffix = nullptr);
......@@ -141,6 +141,8 @@ static const argp_option options[] =
{ "sb-patterns", gen::LTL_SB_PATTERNS, "RANGE", OPTION_ARG_OPTIONAL,
"Somenzi and Bloem [CAV'00] patterns "
"(range should be included in 1..27)", 0 },
{ "sejk-f", gen::LTL_SEJK_F, "RANGE[,RANGE]", 0,
"f(0,j)=(GFa0 U X^j(b)), f(i,j)=(GFai U G(f(i-1,j)))", 0 },
{ "sejk-j", gen::LTL_SEJK_J, "RANGE", 0,
"(GFa1&...&GFan) -> (GFb1&...&GFbn)", 0 },
{ "sejk-k", gen::LTL_SEJK_K, "RANGE", 0,
......@@ -192,6 +194,7 @@ struct job
{
gen::ltl_pattern_id pattern;
struct range range;
struct range range2;
};
typedef std::vector<job> jobs_t;
......@@ -211,9 +214,28 @@ enqueue_job(int pattern, const char* range_str = nullptr)
{
job j;
j.pattern = static_cast<gen::ltl_pattern_id>(pattern);
j.range2.min = -1;
j.range2.max = -1;
if (range_str)
{
j.range = parse_range(range_str);
if (gen::ltl_pattern_argc(j.pattern) == 2)
{
const char* comma = strchr(range_str, ',');
if (!comma)
{
j.range2 = j.range = parse_range(range_str);
}
else
{
std::string range1(range_str, comma);
j.range = parse_range(range1.c_str());
j.range2 = parse_range(comma + 1);
}
}
else
{
j.range = parse_range(range_str);
}
}
else
{
......@@ -251,24 +273,29 @@ parse_opt(int key, char* arg, struct argp_state*)
static void
output_pattern(gen::ltl_pattern_id pattern, int n)
output_pattern(gen::ltl_pattern_id pattern, int n, int n2)
{
formula f = gen::ltl_pattern(pattern, n);
formula f = gen::ltl_pattern(pattern, n, n2);
// Make sure we use only "p42"-style of atomic propositions
// in lbt's output.
if (output_format == lbt_output && !f.has_lbt_atomic_props())
f = relabel(f, Pnn);
std::string args = std::to_string(n);
if (n2 >= 0)
args = args + ',' + std::to_string(n2);
if (opt_positive || !opt_negative)
{
output_formula_checked(f, nullptr, gen::ltl_pattern_name(pattern), n);
output_formula_checked(f, nullptr, gen::ltl_pattern_name(pattern),
args.c_str());
}
if (opt_negative)
{
std::string tmp = "!";
tmp += gen::ltl_pattern_name(pattern);
output_formula_checked(formula::Not(f), nullptr, tmp.c_str(), n);
output_formula_checked(formula::Not(f), nullptr, tmp.c_str(),
args.c_str());
}
}
......@@ -281,7 +308,15 @@ run_jobs()
int n = j.range.min;
for (;;)
{
output_pattern(j.pattern, n);
int inc2 = (j.range2.max < j.range2.min) ? -1 : 1;
int n2 = j.range2.min;
for (;;)
{
output_pattern(j.pattern, n, n2);
if (n2 == j.range2.max)
break;
n2 += inc2;
}
if (n == j.range.max)
break;
n += inc;
......
......@@ -781,7 +781,8 @@ namespace
for (auto& p: m)
stream_formula(opt->output_define->ostream()
<< "#define " << p.first << " (",
p.second, filename, linenum) << ")\n";
p.second, filename,
std::to_string(linenum).c_str()) << ")\n";
}
one_match = true;
output_formula_checked(f, &timer, filename, linenum, prefix, suffix);
......
// -*- coding: utf-8 -*-
// Copyright (C) 2017 Laboratoire de Recherche et Développement de
// Copyright (C) 2017, 2018 Laboratoire de Recherche et Développement de
// l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
......@@ -61,7 +61,11 @@ def ltl_patterns(*args):
"""
Generate LTL patterns.
The arguments should be have one of these three forms:
Each argument should specify a pattern with a
range for its parameter(s).
For single-parameter patterns, arguments of
ltl_patterns() should be have one of these three forms:
- (id, n)
- (id, min, max)
- id
......@@ -71,22 +75,54 @@ def ltl_patterns(*args):
id denotes one of the hard-coded list of LTL formulas (like,
DAC_PATTERNS, EH_PATTERNS, etc.) where all formulas from that
list are output.
For two-parameter patterns, arguments of
ltl_patterns() should be have one of these four forms:
- (id, n1)
- (id, n1, n2)
- (id, min1, max1, min2, max2)
- id
In the first case, n2 is assumed to be equal to n1. In
the third case, all combination of n1 and n2 such that
min1<=n1<=max1 and min2<=n2<=max2 are generated. The
last case is a shorthand for (id, 1, 3, 1, 3).
"""
for spec in args:
min2 = -1
max2 = -1
if type(spec) is int:
pat = spec
min = 1
max = ltl_pattern_max(spec) or 10
argc = ltl_pattern_argc(spec)
if argc == 1:
max = ltl_pattern_max(spec) or 10
else:
min2 = 1
max = max2 = 3
else:
argc = ltl_pattern_argc(spec[0])
ls = len(spec)
if ls == 2:
pat, min, max = spec[0], spec[1], spec[1]
elif ls == 3:
pat, min, max = spec
if argc == 1:
if ls == 2:
pat, min, max = spec[0], spec[1], spec[1]
elif ls == 3:
pat, min, max = spec
else:
raise RuntimeError("invalid pattern specification " + str(spec))
else:
raise RuntimeError("invalid pattern specification")
if ls == 2:
pat, min, max, min2, max2 = \
spec[0], spec[1], spec[1], spec[1], spec[1]
elif ls == 3:
pat, min, max, min2, max2 = \
spec[0], spec[1], spec[1], spec[2], spec[2]
elif ls == 5:
pat, min, max, min2, max2 = spec
else:
raise RuntimeError("invalid pattern specification " + str(spec))
for n in range(min, max + 1):
yield ltl_pattern(pat, n)
for m in range(min2, max2 + 1):
yield ltl_pattern(pat, n, m)
# Override aut_pattern now(), because %feature("shadow") does not
......
......@@ -1140,6 +1140,20 @@ namespace spot
return res;
}
static formula
sejk_f(std::string a, std::string b, int n, int m)
{
formula left = G_(F_(formula::ap(a + std::to_string(0))));
formula right = X_n(formula::ap(b), m);
formula f0 = U_(left, right);
for (int i = 1; i <= n; ++i)
{
formula left = G_(F_(formula::ap(a + std::to_string(i))));
f0 = U_(left, G_(f0));
}
return f0;
}
static formula
sejk_j(std::string a, std::string b, int n)
{
......@@ -1176,7 +1190,7 @@ namespace spot
}
}
formula ltl_pattern(ltl_pattern_id pattern, int n)
formula ltl_pattern(ltl_pattern_id pattern, int n, int m)
{
if (n < 0)
{
......@@ -1185,6 +1199,13 @@ namespace spot
<< " should be positive";
throw std::runtime_error(err.str());
}
if ((m >= 0) ^ (ltl_pattern_argc(pattern) == 2))
{
std::ostringstream err;
err << "unexpected number of arguments for "
<< ltl_pattern_name(pattern);
throw std::runtime_error(err.str());
}
switch (pattern)
{
......@@ -1257,6 +1278,8 @@ namespace spot
return ltl_counter("b", "m", n, true);
case LTL_SB_PATTERNS:
return sb_pattern(n);
case LTL_SEJK_F:
return sejk_f("a", "b", n, m);
case LTL_SEJK_J:
return sejk_j("a", "b", n);
case LTL_SEJK_K:
......@@ -1322,6 +1345,7 @@ namespace spot
"rv-counter-carry-linear",
"rv-counter-linear",
"sb-patterns",
"sejk-f",
"sejk-j",
"sejk-k",
"sejk-patterns",
......@@ -1390,6 +1414,7 @@ namespace spot
return 0;
case LTL_SB_PATTERNS:
return 27;
case LTL_SEJK_F:
case LTL_SEJK_J:
case LTL_SEJK_K:
return 0;
......@@ -1408,5 +1433,64 @@ namespace spot
}
throw std::runtime_error("unsupported pattern");
}
int ltl_pattern_argc(ltl_pattern_id pattern)
{
switch (pattern)
{
// Keep this alphabetically-ordered!
case LTL_AND_F:
case LTL_AND_FG:
case LTL_AND_GF:
case LTL_CCJ_ALPHA:
case LTL_CCJ_BETA:
case LTL_CCJ_BETA_PRIME:
case LTL_DAC_PATTERNS:
case LTL_EH_PATTERNS:
case LTL_FXG_OR:
case LTL_GF_EQUIV:
case LTL_GF_IMPLIES:
case LTL_GH_Q:
case LTL_GH_R:
case LTL_GO_THETA:
case LTL_GXF_AND:
case LTL_HKRSS_PATTERNS:
case LTL_KR_N:
case LTL_KR_NLOGN:
case LTL_KV_PSI:
case LTL_MS_EXAMPLE:
case LTL_MS_PHI_H:
case LTL_MS_PHI_R:
case LTL_MS_PHI_S:
case LTL_OR_FG:
case LTL_OR_G:
case LTL_OR_GF:
case LTL_P_PATTERNS:
case LTL_R_LEFT:
case LTL_R_RIGHT:
case LTL_RV_COUNTER_CARRY:
case LTL_RV_COUNTER_CARRY_LINEAR:
case LTL_RV_COUNTER:
case LTL_RV_COUNTER_LINEAR:
case LTL_SB_PATTERNS:
return 1;
case LTL_SEJK_F:
return 2;
case LTL_SEJK_J:
case LTL_SEJK_K:
case LTL_SEJK_PATTERNS:
case LTL_TV_F1:
case LTL_TV_F2:
case LTL_TV_G1:
case LTL_TV_G2:
case LTL_TV_UU:
case LTL_U_LEFT:
case LTL_U_RIGHT:
return 1;
case LTL_END:
break;
}
throw std::runtime_error("unsupported pattern");
}
}
}
......@@ -244,6 +244,7 @@ namespace spot
LTL_RV_COUNTER_CARRY_LINEAR,
LTL_RV_COUNTER_LINEAR,
LTL_SB_PATTERNS,
LTL_SEJK_F,
LTL_SEJK_J,
LTL_SEJK_K,
LTL_SEJK_PATTERNS,
......@@ -262,7 +263,7 @@ namespace spot
/// The pattern is specified using one value from the ltl_pattern_id
/// enum. See the man page of the `genltl` binary for a
/// description of those patterns, and bibliographic references.
SPOT_API formula ltl_pattern(ltl_pattern_id pattern, int n);
SPOT_API formula ltl_pattern(ltl_pattern_id pattern, int n, int m = -1);
/// \brief convert an ltl_pattern_id value into a name
///
......@@ -275,5 +276,10 @@ namespace spot
/// If an LTL pattern has an upper bound, this returns it.
/// Otherwise, this returns 0.
SPOT_API int ltl_pattern_max(ltl_pattern_id pattern);
/// \brief argument count for LTL patterns
///
/// Return the number of arguments expected by an LTL pattern.
SPOT_API int ltl_pattern_argc(ltl_pattern_id pattern);
}
}
......@@ -24,7 +24,8 @@ set -e
# Make sure the name of each pattern is correctly output by %F.
opts=`genltl --help | sed -n '/=RANGE/{
s/^ *//
s/[=[].*/=1/p
s/=RANGE\[\?,RANGE.*/=1,1/p
s/\[\?=RANGE.*/=1/p
}'`
res=`genltl $opts --format="--%F=%L"`
test "$opts" = "$res"
......@@ -95,27 +96,38 @@ genltl --dac=1..5 --eh=1..5 >output2
diff output output2
genltl --tv-f1=1:3 --tv-f2=1:3 --tv-g1=1:3 --tv-g2=1:3 --tv-uu=1:3 \
--format=%F,%L,%f >output
--sejk-f='0:2,0:3' --format='%F,"%L",%f' >output
cat >expected <<EOF
tv-f1,1,G(p -> q)
tv-f1,2,G(p -> (q | Xq))
tv-f1,3,G(p -> (q | Xq | XXq))
tv-f2,1,G(p -> q)
tv-f2,2,G(p -> (q | Xq))
tv-f2,3,G(p -> (q | X(q | Xq)))
tv-g1,1,G(p -> q)
tv-g1,2,G(p -> (q & Xq))
tv-g1,3,G(p -> (q & Xq & XXq))
tv-g2,1,G(p -> q)
tv-g2,2,G(p -> (q & Xq))
tv-g2,3,G(p -> (q & X(q & Xq)))
tv-uu,1,G(p1 -> (p1 U p2))
tv-uu,2,G(p1 -> (p1 U (p2 & (p2 U p3))))
tv-uu,3,G(p1 -> (p1 U (p2 & (p2 U (p3 & (p3 U p4))))))
tv-f1,"1",G(p -> q)
tv-f1,"2",G(p -> (q | Xq))
tv-f1,"3",G(p -> (q | Xq | XXq))
tv-f2,"1",G(p -> q)
tv-f2,"2",G(p -> (q | Xq))
tv-f2,"3",G(p -> (q | X(q | Xq)))
tv-g1,"1",G(p -> q)
tv-g1,"2",G(p -> (q & Xq))
tv-g1,"3",G(p -> (q & Xq & XXq))
tv-g2,"1",G(p -> q)
tv-g2,"2",G(p -> (q & Xq))
tv-g2,"3",G(p -> (q & X(q & Xq)))
tv-uu,"1",G(p1 -> (p1 U p2))
tv-uu,"2",G(p1 -> (p1 U (p2 & (p2 U p3))))
tv-uu,"3",G(p1 -> (p1 U (p2 & (p2 U (p3 & (p3 U p4))))))
sejk-f,"0,0",GFa0 U b
sejk-f,"0,1",GFa0 U Xb
sejk-f,"0,2",GFa0 U XXb
sejk-f,"0,3",GFa0 U XXXb
sejk-f,"1,0",GFa1 U G(GFa0 U b)
sejk-f,"1,1",GFa1 U G(GFa0 U Xb)
sejk-f,"1,2",GFa1 U G(GFa0 U XXb)
sejk-f,"1,3",GFa1 U G(GFa0 U XXXb)
sejk-f,"2,0",GFa2 U G(GFa1 U G(GFa0 U b))
sejk-f,"2,1",GFa2 U G(GFa1 U G(GFa0 U Xb))
sejk-f,"2,2",GFa2 U G(GFa1 U G(GFa0 U XXb))
sejk-f,"2,3",GFa2 U G(GFa1 U G(GFa0 U XXXb))
EOF
diff output expected
genltl --kr-n2=1..2 --kr-nlogn=1..2 --kr-n=1..2 --gxf-and=0..3 --fxg-or=0..3 \
--format=%F=%L,%f |
ltl2tgba --low --det -F-/2 --stats='%<,%s' > out
......