alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

genltl: add --lily-patterns

Browse source 
* spot/gen/formulas.cc, spot/gen/formulas.hh, bin/genltl.cc: Implement
support for --lily-pattern.
* doc/spot.bib, bin/man/genltl.x: Add references.
* NEWS: Mention it.
* tests/core/ltlsynt.test: Use these formulas.
* tests/core/genltl.test: Adjust.
This commit is contained in:
Alexandre Duret-Lutz 2024-08-26 15:27:23 +02:00
parent 844fb887d9
commit c6f4b18655
8 changed files with 131 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

7
NEWS
View file

@ -15,6 +15,13 @@ New in spot 2.12.0.dev (not yet released)
specify which atomic propositions are input or output, as this can
be inferred from their name.
- genltl learned --lily-patterns to generate the example LTL
synthesis specifications from Lily 1.0.2. Those come with input
and output atomic proposition rewriten in the form "iNN" or "oNN",
so they can be fed to ltlsynt directly, as in
% genltl --lily-patterns | ltlsynt -q
- autfilt learned --restrict-dead-end-edges, to restricts labels of
edges leading to dead-ends. See the description of
restrict_dead_end_edges_here() below.

5
bin/genltl.cc
View file

@ -115,6 +115,11 @@ static const argp_option options[] =
{ "kv-psi", gen::LTL_KV_PSI, "RANGE", 0,
"quadratic formula with doubly exponential DBA", 0 },
OPT_ALIAS(kr-n2),
{ "lily-patterns", gen::LTL_LILY_PATTERNS, "RANGE", OPTION_ARG_OPTIONAL,
"LTL synthesis specification examples from Lily 1.0.2 "
"[Jobstmann & Bloem, FMCAD'06] "
"(range should be included in 1..23)", 0 },
OPT_ALIAS(jb-patterns),
{ "ms-example", gen::LTL_MS_EXAMPLE, "RANGE[,RANGE]", 0,
"GF(a1&X(a2&X(a3&...Xan)))&F(b1&F(b2&F(b3&...&Xbm)))", 0 },
{ "ms-phi-h", gen::LTL_MS_PHI_H, "RANGE", 0,

10
bin/man/genltl.x
View file

@ -29,13 +29,17 @@ gh
J. Geldenhuys and H. Hansen: Larger automata and less
work for LTL model checking. Proceedings of Spin'06. LNCS 3925.
.TP
go
P. Gastin and D. Oddoux: Fast LTL to Büchi Automata Translation.
Proceedings of CAV'01. LNCS 2102.
.TP
hkrss
J. Holeček, T. Kratochvila, V. Řehák, D. Šafránek, and P. Šimeček:
Verification Results in Liberouter Project. Tech. Report 03, CESNET, 2004.
.TP
go
P. Gastin and D. Oddoux: Fast LTL to Büchi Automata Translation.
Proceedings of CAV'01. LNCS 2102.
jb, lily
B. Jobstmann, and R. Bloem:
Optimizations for LTL Synthesis. Proceedings of FMCAD'06. IEEE.
.TP
kr
O. Kupferman and A. Rosenberg: The Blow-Up in Translating LTL to Deterministic

11
doc/spot.bib
View file

@ -639,6 +639,17 @@
doi = {10.4204/EPTCS.229.10}
}
@InProceedings{ jobsmann.06.fmcad,
author = {Barbara Jobstmann and Roderick Bloem},
title = {Optimizations for {LTL} Systhesis},
booktitle = {Proceedings of the 6th International Conference on Formal
Methods in Computer-Aided Design (FMCAD'06)},
year = {2006},
month = nov,
publisher = {IEEE},
doi = {10.1109/FMCAD.2006.22}
}
@InCollection{ klein.07.ciaa,
year = {2007},
booktitle = {Proceedings of the 12th International Conference on the

69
spot/gen/formulas.cc
View file

@ -824,6 +824,56 @@ namespace spot
return spot::relabel(parse_formula(formulas[n - 1]), Pnn);
}
static formula
lily_pattern(int n)
{
static const char* formulas[] = {
"G(i2->(X(o0&X(o0&Xo0))&(o0->X!o0)&(i0->X(!o0 U i1))))",
"G(i2->(X(o0|X(o0|Xo0))&(o0->X!o0)&(i0->X(!o0 U i1))))",
"G(i0->Xi1)->G(i2->(X(o0|X(o0|Xo0))&(o0->X!o0)&(i0->X(!o0 U i1))))",
"G(i0->X(i1|Xi1))->"
"G(i2->(X(o0|X(o0|Xo0))&(o0->X!o0)&(i0->X(!o0 U i1))))",
"G(i0->X(i1|Xi1))->"
"G(i2->(X(i0|o0|X(i0|o0|X(i0|o0)))&(o0->X!o0)&(i0->X(!o0 U i1))))",
"G(i0->X(i1|X(i1|Xi1)))->"
"G(i2->(X(i0|o0|X(i0|o0|X(i0|o0)))&(o0->X!o0)&(i0->X(!o0 U i1))))",
"G(i0->X(i1|Xi1))->G(i0->(X(!o0 U i1)"
"&(o0->X!o0)&(i2->(i0|o0|X(i0|o0|X(i0|o0|X(i0|o0)))))))",
"GFi0->GFo0",
"GFi0->(!o0&G(!o0->((!o0 U i0)&(i0->Fo0)))&GFo0)",
"(GFi1|Fi0)->(GFo1|Go0)",
"!(G(i1->Fo0)&G(i0->Fo1))",
"G!o1|G(i1->Fo0)|G(i0->Fo1)",
"Gi0->(Fo0&(G!i0->F!o0))",
"G!(o0&o1)&(GFi0->GFo0)&(GFi1->GFo1)",
// lily=15 This matches the original formula from Lily, not
// the unrealizable version from Syfco. See
// https://github.com/reactive-systems/syfco/issues/55
"G(i0->(!(o0&o1)&Fo0&(i1->Fo1)))&((!o0 U i0)|G!o0)&((!o1 U i1)|G!o1)",
// lily=16 Same comment as above.
"G(i0->(!(o0&o1)&!(o0&o2)&!(o1&o2)&Fo0&(i1->Fo1)&(i2->Fo2)))&"
"((!o0 U i0)|G!o0)&((!o1 U i1)|G!o1)&((!o2 U i2)|G!o2)",
"G(!(o0&o1)&!(o1&o2)&!(o0&o2))&(GFi0->GFo0)&(GFi1->GFo1)&GFo2",
"G(!(o0&o1)&!(o0&o2)&!(o0&o3)&!(o1&o2)&!(o1&o3)&!(o2&o3))&"
"(GFi0->GFo0)&(GFi1->GFo1)&(GFi2->GFo2)&GFo3",
"GFi1->G(o1->(!(o0&o1)&(o1 U i1)&(o0->(o0 U i1))&(i0->Fo0)&Fo1))",
"(!i1&G((!i1&!o2)->X!i1)&G(i1->F!i1)&G(o2->Xi1))->"
"G((o1&X!o1)->(o2&(o0|o1)&((o0&X!o0)->o2)&((!o0&(!i0|!i1))->"
"Xo0)&((!o1&(i0|!i1))->Xo1)&(i0->F!o0)&F!o1))",
"(G(!i0|!i1)&G(!i0|!i2)&G(!i0|!i3)&G(!i1|!i2)&G(!i1|!i3)&"
"G(!i2|!i3))->G((!o0|!o1)&(!o0|!o2)&(!o0|!o3)&(!o1|!o2)&(!o1|!o3)&"
"(!o2|!o3)&G(i0->(Xo0|XXo0|XXXo0))&G(i1->(Xo1|XXo1|XXXo1))&"
"G(i2->(Xo2|XXo2|XXXo2))&G(i3->(Xo3|XXo3|XXXo3)))",
"(!i0&!i1&!i2&G!(i0&i1)&GF!i2&G((!i2&o0)->X!i2)&G(i2->X(!i2|"
"X(!i2|X(!i2 | X!i2)))))->G(!(i2&Xo0)&(i1->F!o0)&(i0->Fo0))",
"(G((i0&Xo0)->Xi0)&GF!i0)->GX(!i0&X!o0)",
};
constexpr unsigned max = (sizeof formulas)/(sizeof *formulas);
if (n < 1 || (unsigned) n > max)
bad_number("lily-patterns", n, max);
return parse_formula(formulas[n - 1]);
}
static formula
p_pattern(int n)
{
@ -1359,12 +1409,8 @@ namespace spot
return kr1_exp(n, "a", "b", "c", "d", "y", "z");
case LTL_KV_PSI:
return kv_exp(n, "a", "b", "c", "d");
case LTL_OR_FG:
return FG_n("p", n, false);
case LTL_OR_G:
return combunop_n("p", n, op::G, false);
case LTL_OR_GF:
return GF_n("p", n, false);
case LTL_LILY_PATTERNS:
return lily_pattern(n);
case LTL_MS_EXAMPLE:
return ms_example("a", "b", n, m);
case LTL_MS_PHI_H:
@ -1373,6 +1419,12 @@ namespace spot
return ms_phi_rs("a", "b", n, true);
case LTL_MS_PHI_S:
return ms_phi_rs("a", "b", n, false);
case LTL_OR_FG:
return FG_n("p", n, false);
case LTL_OR_G:
return combunop_n("p", n, op::G, false);
case LTL_OR_GF:
return GF_n("p", n, false);
case LTL_P_PATTERNS:
return p_pattern(n);
case LTL_PPS_ARBITER_STANDARD:
@ -1448,6 +1500,7 @@ namespace spot
"kr-n",
"kr-nlogn",
"kv-psi",
"lily-patterns",
"ms-example",
"ms-phi-h",
"ms-phi-r",
@ -1518,6 +1571,9 @@ namespace spot
case LTL_KR_N:
case LTL_KR_NLOGN:
case LTL_KV_PSI:
return 0;
case LTL_LILY_PATTERNS:
return 23;
case LTL_MS_EXAMPLE:
case LTL_MS_PHI_H:
case LTL_MS_PHI_R:
@ -1586,6 +1642,7 @@ namespace spot
case LTL_KR_N:
case LTL_KR_NLOGN:
case LTL_KV_PSI:
case LTL_LILY_PATTERNS:
return 1;
case LTL_MS_EXAMPLE:
return 2;

3
spot/gen/formulas.hh
View file

@ -91,6 +91,9 @@ namespace spot
/// \cite kupferman.10.mochart ,
/// \cite kupferman.05.tcl .
LTL_KV_PSI,
/// LTL synthesis examples specification from the Lily 1.0.2
/// distribution. \cite jobstmann.06.fmcad
LTL_LILY_PATTERNS,
/// `GF(a1&X(a2&X(a3&...Xan)))&F(b1&F(b2&F(b3&...&Xbm)))`
/// \cite muller.17.gandalf
LTL_MS_EXAMPLE,

6
tests/core/genltl.test
View file

@ -241,6 +241,12 @@ test $? = 2
test "`cat err`" = \
"genltl: no pattern hkrss-patterns=0, supported range is 1..55"
genltl --lily-patterns=0 2> err && exit 1
test $? = 2
test "`cat err`" = \
"genltl: no pattern lily-patterns=0, supported range is 1..23"
genltl --kr-n=0 2> err && exit 1
test $? = 2
test "`cat err`" = "genltl: no pattern kr-n=0, supported range is 1.."

29
tests/core/ltlsynt.test
View file

@ -1316,3 +1316,32 @@ f2='G(i1->(o1|!o2)) & G(!i1->(o3|!o4)) & G(i2->(!o1|o2)) & G(!i2->(!o3|o4))&Go5'
ltlsynt -f "$f2" --polarity=before-decom --verbose 2>out 1>&2
sed 's/ [0-9.e-]* seconds/ X seconds/g;s/ -> /->/g;' out > outx
diff outx exp
genltl --lily-patterns | ltlsynt -q > out && exit 2
cat >expected <<EOF
UNREALIZABLE
UNREALIZABLE
REALIZABLE
REALIZABLE
REALIZABLE
REALIZABLE
REALIZABLE
REALIZABLE
REALIZABLE
REALIZABLE
UNREALIZABLE
REALIZABLE
REALIZABLE
REALIZABLE
REALIZABLE
REALIZABLE
REALIZABLE
REALIZABLE
REALIZABLE
REALIZABLE
REALIZABLE
REALIZABLE
REALIZABLE
EOF
diff out expected