Commit 08c153d3 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

genltl: add support for --p-patterns

Fixes #246.

* bin/genltl.cc: Implement it.
* bin/man/genltl.x, doc/org/genltl.org, NEWS: Document it.
* tests/core/ltl2tgba2.test: Test it.
parent 4b7a6238
......@@ -6,8 +6,9 @@ New in spot 2.3.2.dev (not yet released)
and ltl2ldba (from Owl) without needing to specify %f>%O.
- genltl learned --spec-patterns as an alias for --dac-patterns; it
also learned a new set of LTL formulas under --hkrss-patterns
(a.k.a. --liberouter-patterns).
also learned two new sets of LTL formulas under --hkrss-patterns
(a.k.a. --liberouter-patterns) and --p-patterns
(a.k.a. --beem-patterns).
Bug fixes:
......
......@@ -142,6 +142,19 @@
// number = 03,
// institution = {CESNET}
// }
//
// @InProceedings{pelanek.07.spin,
// author = {Radek Pel\'{a}nek},
// title = {{BEEM}: benchmarks for explicit model checkers},
// booktitle = {Proceedings of the 14th international SPIN conference on
// Model checking software},
// year = 2007,
// pages = {263--267},
// numpages = {5},
// volume = {4595},
// series = {Lecture Notes in Computer Science},
// publisher = {Springer-Verlag}
// }
#include "common_sys.hh"
......@@ -196,6 +209,7 @@ enum {
OPT_OR_FG,
OPT_OR_G,
OPT_OR_GF,
OPT_P_PATTERNS,
OPT_R_LEFT,
OPT_R_RIGHT,
OPT_RV_COUNTER,
......@@ -235,6 +249,7 @@ const char* const class_name[LAST_CLASS - FIRST_CLASS] =
"or-fg",
"or-g",
"or-gf",
"p-patterns",
"r-left",
"r-right",
"rv-counter",
......@@ -303,6 +318,11 @@ static const argp_option options[] =
OPT_ALIAS(gh-s),
{ "or-gf", OPT_OR_GF, "RANGE", 0, "GF(p1)|GF(p2)|...|GF(pn)", 0 },
OPT_ALIAS(gh-c1),
{ "p-patterns", OPT_P_PATTERNS, "RANGE", OPTION_ARG_OPTIONAL,
"Pelánek [Spin'07] patterns from BEEM "
"(range should be included in 1..20)", 0 },
OPT_ALIAS(beem-patterns),
OPT_ALIAS(p),
{ "r-left", OPT_R_LEFT, "RANGE", 0, "(((p1 R p2) R p3) ... R pn)", 0 },
{ "r-right", OPT_R_RIGHT, "RANGE", 0, "(p1 R (p2 R (... R pn)))", 0 },
{ "rv-counter", OPT_RV_COUNTER, "RANGE", 0,
......@@ -436,6 +456,12 @@ parse_opt(int key, char* arg, struct argp_state*)
else
enqueue_job(key, 1, 12);
break;
case OPT_P_PATTERNS:
if (arg)
enqueue_job(key, arg);
else
enqueue_job(key, 1, 20);
break;
case OPT_SB_PATTERNS:
if (arg)
enqueue_job(key, arg);
......@@ -1142,6 +1168,38 @@ eh_pattern(int n)
return spot::relabel(parse_formula(formulas[n - 1]), Pnn);
}
static formula
p_pattern(int n)
{
static const char* formulas[] = {
"G(p0 -> Fp1)",
"(GFp1 & GFp0) -> GFp2",
"G(p0 -> (p1 & (p2 U p3)))",
"F(p0 | p1)",
"GF(p0 | p1)",
"(p0 U p1) -> ((p2 U p3) | Gp2)",
"G(p0 -> (!p1 U (p1 U (!p1 & (p2 R !p1)))))",
"G(p0 -> (p1 R !p2))",
"G(!p0 -> Fp0)",
"G(p0 -> F(p1 | p2))",
"!(!(p0 | p1) U p2) & G(p3 -> !(!(p0 | p1) U p2))",
"G!p0 -> G!p1",
"G(p0 -> (G!p1 | (!p2 U p1)))",
"G(p0 -> (p1 R (p1 | !p2)))",
"G((p0 & p1) -> (!p1 R (p0 | !p1)))",
"G(p0 -> F(p1 & p2))",
"G(p0 -> (!p1 U (p1 U (p1 & p2))))",
"G(p0 -> (!p1 U (p1 U (!p1 U (p1 U (p1 & p2))))))",
"GFp0 -> GFp1",
"GF(p0 | p1) & GF(p1 | p2)",
};
constexpr unsigned max = (sizeof formulas)/(sizeof *formulas);
if (n < 1 || (unsigned) n > max)
bad_number("--p-patterns", n, max);
return spot::relabel(parse_formula(formulas[n - 1]), Pnn);
}
static formula
sb_pattern(int n)
{
......@@ -1488,6 +1546,9 @@ output_pattern(int pattern, int n)
case OPT_OR_GF:
f = GF_n("p", n, false);
break;
case OPT_P_PATTERNS:
f = p_pattern(n);
break;
case OPT_R_LEFT:
f = bin_n("p", n, op::R, false);
break;
......
......@@ -46,6 +46,10 @@ kv
O. Kupferman and M. Y. Vardi: From Linear Time to Branching Time.
ACM Transactions on Computational Logic, 6(2):273-294, 2005.
.TP
p
R. Pelánek: BEEM: benchmarks for explicit model checkers
Proceedings of Spin'07. LNCS 4595.
.TP
rv
K. Rozier and M. Vardi: LTL Satisfiability Checking.
Proceedings of Spin'07. LNCS 4595.
......
......@@ -133,15 +133,15 @@ This is because most tools using =lbt='s syntax require atomic
propositions to have the form =pNN=.
Four options provide lists of unrelated LTL formulas, taken from the
Five options provide lists of unrelated LTL formulas, taken from the
literature (see the [[./man/genltl.1.html][=genltl=]](1) man page for references):
=--dac-patterns=, =--eh-patterns=, =--hkrss-patterns=, and
=--sb-patterns=. With these options, the range is used to select a
subset of the list of formulas. Without range, all formulas are used.
Here is the complete list:
=--dac-patterns=, =--eh-patterns=, =--hkrss-patterns=, =--p-patterns=,
and =--sb-patterns=. With these options, the range is used to select
a subset of the list of formulas. Without range, all formulas are
used. Here is the complete list:
#+BEGIN_SRC sh :results verbatim :exports both
genltl --dac --eh --hkrss --sb --format=%F:%L,%f
genltl --dac --eh --hkrss --p --sb --format=%F:%L,%f
#+END_SRC
#+RESULTS:
......@@ -268,6 +268,26 @@ hkrss-patterns:52,XG(p0 -> (G!p1 | (!Xp1 U p2)))
hkrss-patterns:53,XG((p0 & !p1) -> (G!p1 | (!p1 U p2)))
hkrss-patterns:54,XG((p0 & p1) -> ((p1 U p2) | Gp1))
hkrss-patterns:55,Xp0 & G((!p0 & Xp0) -> XXp0)
p-patterns:1,G(p0 -> Fp1)
p-patterns:2,(GFp1 & GFp0) -> GFp2
p-patterns:3,G(p0 -> (p1 & (p2 U p3)))
p-patterns:4,F(p0 | p1)
p-patterns:5,GF(p0 | p1)
p-patterns:6,(p0 U p1) -> ((p2 U p3) | Gp2)
p-patterns:7,G(p0 -> (!p1 U (p1 U (!p1 & (p2 R !p1)))))
p-patterns:8,G(p0 -> (p1 R !p2))
p-patterns:9,G(!p0 -> Fp0)
p-patterns:10,G(p0 -> F(p1 | p2))
p-patterns:11,!(!(p0 | p1) U p2) & G(p3 -> !(!(p0 | p1) U p2))
p-patterns:12,G!p0 -> G!p1
p-patterns:13,G(p0 -> (G!p1 | (!p2 U p1)))
p-patterns:14,G(p0 -> (p1 R (p1 | !p2)))
p-patterns:15,G((p0 & p1) -> (!p1 R (p0 | !p1)))
p-patterns:16,G(p0 -> F(p1 & p2))
p-patterns:17,G(p0 -> (!p1 U (p1 U (p1 & p2))))
p-patterns:18,G(p0 -> (!p1 U (p1 U (!p1 U (p1 U (p1 & p2))))))
p-patterns:19,GFp0 -> GFp1
p-patterns:20,GF(p0 | p1) & GF(p1 | p2)
sb-patterns:1,p0 U p1
sb-patterns:2,p0 U (p1 U p2)
sb-patterns:3,!(p0 U (p1 U p2))
......
......@@ -27,7 +27,7 @@
# commonly use as benchmark change, we want to notice it.
set -e
genltl --dac --eh --sb --hkrss --format=%F,%L,%f >pos
genltl --dac --eh --sb --hkrss --p --format=%F,%L,%f >pos
(cat pos; ltlfilt --negate pos/3 --format='!%<,%f') |
ltlfilt -u -F-/3 >formulas
......@@ -183,6 +183,24 @@ hkrss-patterns,52, 4,25, 4,25, 5,29, 5,29
hkrss-patterns,53, 3,22, 3,22, 3,22, 3,22
hkrss-patterns,54, 3,22, 3,22, 3,22, 3,22
hkrss-patterns,55, 5,8, 5,8, 5,8, 5,8
p-patterns,2, 4,36, 4,36, 5,44, 5,44
p-patterns,3, 2,20, 2,20, 2,20, 2,20
p-patterns,4, 2,8, 2,8, 2,8, 2,8
p-patterns,5, 1,4, 1,4, 2,8, 2,8
p-patterns,6, 4,50, 4,50, 4,50, 4,50
p-patterns,7, 4,27, 4,27, 4,27, 4,27
p-patterns,8, 2,10, 2,10, 2,10, 2,10
p-patterns,9, 1,2, 1,2, 2,4, 2,4
p-patterns,10, 2,16, 2,16, 2,16, 2,16
p-patterns,11, 2,20, 2,20, 2,20, 2,20
p-patterns,12, 3,12, 3,12, 3,12, 3,12
p-patterns,13, 3,20, 3,20, 3,20, 3,20
p-patterns,14, 2,13, 2,13, 2,13, 2,13
p-patterns,15, 2,7, 2,7, 2,7, 2,7
p-patterns,16, 2,16, 2,16, 2,16, 2,16
p-patterns,17, 3,20, 3,20, 3,20, 3,20
p-patterns,18, 5,36, 5,36, 5,36, 5,36
p-patterns,20, 1,8, 1,8, 3,24, 3,24
!dac-patterns,1, 2,4, 2,4, 2,4, 2,4
!dac-patterns,2, 3,10, 3,10, 3,10, 3,10
!dac-patterns,3, 3,12, 3,12, 3,12, 3,12
......@@ -321,6 +339,24 @@ hkrss-patterns,55, 5,8, 5,8, 5,8, 5,8
!hkrss-patterns,53, 4,32, 4,32, 4,32, 4,32
!hkrss-patterns,54, 4,32, 4,32, 4,32, 4,32
!hkrss-patterns,55, 5,12, 6,12, 5,12, 6,12
!p-patterns,2, 2,15, 2,15, 4,23, 4,23
!p-patterns,3, 3,41, 3,41, 3,41, 3,41
!p-patterns,4, 1,1, 1,1, 1,1, 1,1
!p-patterns,5, 2,6, 2,6, 2,6, 2,6
!p-patterns,6, 4,42, 4,42, 4,42, 4,42
!p-patterns,7, 5,34, 5,34, 5,34, 5,34
!p-patterns,8, 3,24, 3,24, 3,24, 3,24
!p-patterns,9, 2,4, 2,4, 2,4, 2,4
!p-patterns,10, 2,11, 2,11, 2,11, 2,11
!p-patterns,11, 3,48, 3,48, 3,48, 3,48
!p-patterns,12, 2,4, 2,4, 2,4, 2,4
!p-patterns,13, 4,32, 4,32, 4,32, 4,32
!p-patterns,14, 3,24, 3,24, 3,24, 3,24
!p-patterns,15, 3,12, 3,12, 3,12, 3,12
!p-patterns,16, 2,17, 2,17, 2,17, 2,17
!p-patterns,17, 4,31, 4,31, 4,31, 4,31
!p-patterns,18, 6,43, 6,43, 6,43, 6,43
!p-patterns,20, 3,16, 3,16, 3,16, 3,16
EOF
diff output expected
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