diff --git a/NEWS b/NEWS index 24cc076de..6db3b49f0 100644 --- a/NEWS +++ b/NEWS @@ -34,6 +34,12 @@ New in spot 2.0a (not yet released) 'b U (a & b)' instead. The operators that can be listed between brackets are the same as those of ltlfilt --unabbreviate option. + * genltl has three new options: --dac-patterns=1..45, + --eh-patterns=1..12, and --sb-patterns=1..27. Unlike other options + these do not output scalable patterns, but simply a list of formulas + appearing in these three papers: Dwyer et al (FMSP'98), Etessami & + Holzmann (Concur'00) Somenzi & Bloem (CAV'00). + Library: * The print_hoa() function will now output version 1.1 of the HOA diff --git a/bench/ltl2tgba/Makefile.am b/bench/ltl2tgba/Makefile.am index 9bccb4c63..7be974138 100644 --- a/bench/ltl2tgba/Makefile.am +++ b/bench/ltl2tgba/Makefile.am @@ -19,7 +19,6 @@ EXTRA_DIST = \ big \ - formulae.ltl \ known \ small \ tools \ diff --git a/bench/ltl2tgba/README b/bench/ltl2tgba/README index 008e9e3f3..2c78407a1 100644 --- a/bench/ltl2tgba/README +++ b/bench/ltl2tgba/README @@ -46,7 +46,7 @@ this benchmark. Three scripts that run ltlcross on, respectively: 100 small formulae (size 10, 4 propositions) and their negations 100 big formulae (size 12..15, 8 propositions) and their negations - 92 known formulae (from formulae.ltl) and their negations + 92 known formulae (produced by genltl, see below) and their negations Each script generates 3 files: xxxx.log: the log of ltlcross' execution, updated as the script goes @@ -57,10 +57,9 @@ this benchmark. you kill a script before it terminates only the xxxx.log file will have been overwritten. -* formulae.ltl - A list of LTL formulae used by the `known' check. They come - from three sources: +The known LTL formulas are generated by genltl, and come from the following +three papers: @InProceedings{ dwyer.98.fmsp, author = {Matthew B. Dwyer and George S. Avrunin and James C. @@ -105,7 +104,7 @@ this benchmark. } In the known benchmark, we use both positive and negated versions - of these formulae. + of these formulae, yielding 178 unique formulas. * sym.py diff --git a/bench/ltl2tgba/formulae.ltl b/bench/ltl2tgba/formulae.ltl deleted file mode 100644 index bbd761c3b..000000000 --- a/bench/ltl2tgba/formulae.ltl +++ /dev/null @@ -1,92 +0,0 @@ -[](!p0) -<>p1 -> (!p0 U p1) -[](p2 -> [](!p0)) -[]((p2 & !p1 & <>p1) -> (!p0 U p1)) -[](p2 & !p1 -> (!p0 U (p1 | []!p0))) -<>(p0) -!p1 U ((p0 & !p1) | []!p1) -[](!p2) | <>(p2 & <>p0) -[](p2 & !p1 -> (!p1 U ((p0 & !p1) | []!p1))) -[](p2 & !p1 -> (!p1 U (p0 & !p1))) -<>p1 -> ((!p0 & !p1) U (p1 | ((p0 & !p1) U (p1 | ((!p0 & !p1) U (p1 | ((p0 & !p1) U (p1 | (!p0 U p1))))))))) -[]((p2 & <>p1) -> ((!p0 & !p1) U (p1 | ((p0 & !p1) U (p1 | ((!p0 & !p1) U (p1 | ((p0 & !p1) U (p1 | (!p0 U p1)))))))))) -[](p2 -> ((!p0 & !p1) U (p1 | ((p0 & !p1) U (p1 | ((!p0 & !p1) U (p1 | ((p0 & !p1) U (p1 | (!p0 U (p1 | []!p0)) | []p0))))))))) -[](p0) -<>p1 -> (p0 U p1) -[](p2 -> [](p0)) -[]((p2 & !p1 & <>p1) -> (p0 U p1)) -[](p2 & !p1 -> (p0 U (p1 | [] p0))) -!p0 U (p3 | []!p0) -<>p1 -> (!p0 U (p3 | p1)) -[]!p2 | <>(p2 & (!p0 U (p3 | []!p0))) -[]((p2 & !p1 & <>p1) -> (!p0 U (p3 | p1))) -[](p2 & !p1 -> (!p0 U ((p3 | p1) | []!p0))) -[](p0 -> <>p3) -<>p1 -> (p0 -> (!p1 U (p3 & !p1))) U p1 -[](p2 -> [](p0 -> <>p3)) -[]((p2 & !p1 & <>p1) -> (p0 -> (!p1 U (p3 & !p1))) U p1) -[](p2 & !p1 -> ((p0 -> (!p1 U (p3 & !p1))) U (p1 | [](p0 -> (!p1 U (p3 & !p1)))))) -<>p0 -> (!p0 U (p3 & !p0 & X(!p0 U p4))) -<>p1 -> (!p0 U (p1 | (p3 & !p0 & X(!p0 U p4)))) -([]!p2) | (!p2 U (p2 & <>p0 -> (!p0 U (p3 & !p0 & X(!p0 U p4))))) -[]((p2 & <>p1) -> (!p0 U (p1 | (p3 & !p0 & X(!p0 U p4))))) -[](p2 -> (<>p0 -> (!p0 U (p1 | (p3 & !p0 & X(!p0 U p4)))))) -(<>(p3 & X<>p4)) -> ((!p3) U p0) -<>p1 -> ((!(p3 & (!p1) & X(!p1 U (p4 & !p1)))) U (p1 | p0)) -([]!p2) | ((!p2) U (p2 & ((<>(p3 & X<>p4)) -> ((!p3) U p0)))) -[]((p2 & <>p1) -> ((!(p3 & (!p1) & X(!p1 U (p4 & !p1)))) U (p1 | p0))) -[](p2 -> (!(p3 & (!p1) & X(!p1 U (p4 & !p1))) U (p1 | p0) | [](!(p3 & X<>p4)))) -[] (p3 & X<> p4 -> X(<>(p4 & <> p0))) -<>p1 -> (p3 & X(!p1 U p4) -> X(!p1 U (p4 & <> p0))) U p1 -[] (p2 -> [] (p3 & X<> p4 -> X(!p4 U (p4 & <> p0)))) -[] ((p2 & <>p1) -> (p3 & X(!p1 U p4) -> X(!p1 U (p4 & <> p0))) U p1) -[] (p2 -> (p3 & X(!p1 U p4) -> X(!p1 U (p4 & <> p0))) U (p1 | [] (p3 & X(!p1 U p4) -> X(!p1 U (p4 & <> p0))))) -[] (p0 -> <>(p3 & X<>p4)) -<>p1 -> (p0 -> (!p1 U (p3 & !p1 & X(!p1 U p4)))) U p1 -[] (p2 -> [] (p0 -> (p3 & X<> p4))) -[] ((p2 & <>p1) -> (p0 -> (!p1 U (p3 & !p1 & X(!p1 U p4)))) U p1) -[] (p2 -> (p0 -> (!p1 U (p3 & !p1 & X(!p1 U p4)))) U (p1 | [] (p0 -> (p3 & X<> p4)))) -[] (p0 -> <>(p3 & !p5 & X(!p5 U p4))) -<>p1 -> (p0 -> (!p1 U (p3 & !p1 & !p5 & X((!p1 & !p5) U p4)))) U p1 -[] (p2 -> [] (p0 -> (p3 & !p5 & X(!p5 U p4)))) -[] ((p2 & <>p1) -> (p0 -> (!p1 U (p3 & !p1 & !p5 & X((!p1 & !p5) U p4)))) U p1) -[] (p2 -> (p0 -> (!p1 U (p3 & !p1 & !p5 & X((!p1 & !p5) U p4)))) U (p1 | [] (p0 -> (p3 & !p5 & X(!p5 U p4))))) -!p0 U ((p0 U ((!p0 U ((p0 U ([]!p0 | []p0)) | []!p0)) | []!p0)) | []!p0) -<>p2 -> (!p2 U (p2 & (!p0 U ((p0 U ((!p0 U ((p0 U ([]!p0 | []p0)) | []!p0)) | []!p0)) | []!p0)))) -p0 U p1 -p0 U (p1 U p2) -!p0 R (!p1 R !p2) -(1 U (0 R !p0)) | (0 R (1 U p1)) -(1 U p0) U (0 R p1) -(0 R p0) U p1 -(1 U p0) & (1 U (1 U p0)) & (0 R !p0) & (0 R (0 R !p0)) -(0 R (1 U p0)) & (1 U (0 R !p1)) -((0 R (1 U p0)) & (1 U (0 R !p1))) | ((0 R (1 U p1)) & (1 U (0 R !p0))) -p0 R (p0 | p1) -(Xp0 U Xp1) | X(!p0 R !p1) -(Xp0 U p1) | X(!p0 R (!p0 | !p1)) -(0 R (!p0 | (1 U p1))) & ((Xp0 U p1) | X(!p0 R (!p0 | !p1))) -(0 R (!p0 | (1 U p1))) & ((Xp0 U Xp1) | X(!p0 R !p1)) -0 R (!p0 | (1 U p1)) -1 U (p0 & X(!p1 U !p2)) -(1 U (0 R !p0)) & (0 R (1 U !p1)) -0 R ((1 U p0) & (1 U p1)) -(1 U p0) & (1 U !p0) -(Xp1 & p2) R X(((p3 U p0) R p2) U (p3 R p2)) -((0 R (p1 | (0 R (1 U p0)))) & (0 R (p2 | (0 R (1 U !p0))))) | (0 R p1) | (0 R p2) -((0 R (p1 | (1 U (0 R p0)))) & (0 R (p2 | (1 U (0 R !p0))))) | (0 R p1) | (0 R p2) -(0 R (p1 | X(0 R p0))) & (0 R (p2 | X(0 R !p0))) -0 R (p1 | (Xp0 & X!p0)) -p0 | (p1 U p0) -p0 U (p1 & (0 R p2)) -p0 U (p1 & X(p2 U p3)) -p0 U (p1 & X(p2 & (1 U (p3 & X(1 U (p4 & X(1 U (p5 & X(1 U p6))))))))) -1 U (p0 & X(0 R p1)) -1 U (p0 & X(p1 & X(1 U p2))) -1 U (p0 & X(p1 U p2)) -(1 U (0 R p0)) | (1 U (0 R p1)) -0 R (!p0 | (p1 U p2)) -1 U (p0 & X(1 U (p1 & X(1 U (p2 & X(1 U p3)))))) -(0 R (1 U p0)) & (0 R (1 U p1)) & (0 R (1 U p2)) & (0 R (1 U p3)) & (0 R (1 U p4)) -(p0 U (p1 U p2)) | (p1 U (p2 U p0)) | (p2 U (p0 U p1)) -0 R (!p0 | (p1 U ((0 R p2) | (0 R p3)))) diff --git a/bench/ltl2tgba/known b/bench/ltl2tgba/known index 8688afc1e..3350b3992 100755 --- a/bench/ltl2tgba/known +++ b/bench/ltl2tgba/known @@ -1,7 +1,7 @@ #!/bin/sh # -*- shell-script -*- -# Copyright (C) 2012, 2013 Laboratoire de Recherche et Developpement de -# l'Epita (LRDE) +# Copyright (C) 2012, 2013, 2016 Laboratoire de Recherche et +# Developpement de l'Epita (LRDE) # # This file is part of Spot, a model checking library. # @@ -20,6 +20,6 @@ . ./defs -$LTLCROSS "$@" --csv=known.csv --json=known.json \ - < "$srcdir/formulae.ltl" 2>&1 | +$GENLTL --dac-patterns --eh-patterns --sb-patterns | +$LTLCROSS "$@" --csv=known.csv --json=known.json 2>&1 | tee known.log diff --git a/bin/genltl.cc b/bin/genltl.cc index 39a5a269c..7cf135ef9 100644 --- a/bin/genltl.cc +++ b/bin/genltl.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2015 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2012, 2013, 2015, 2016 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -65,6 +65,47 @@ // series = {Lecture Notes in Computer Science}, // publisher = {Springer-Verlag} // } +// +// @InProceedings{dwyer.98.fmsp, +// author = {Matthew B. Dwyer and George S. Avrunin and James C. Corbett}, +// title = {Property Specification Patterns for Finite-state +// Verification}, +// booktitle = {Proceedings of the 2nd Workshop on Formal Methods in +// Software Practice (FMSP'98)}, +// publisher = {ACM Press}, +// address = {New York}, +// editor = {Mark Ardis}, +// month = mar, +// year = {1998}, +// pages = {7--15} +// } +// +// @InProceedings{etessami.00.concur, +// author = {Kousha Etessami and Gerard J. Holzmann}, +// title = {Optimizing {B\"u}chi Automata}, +// booktitle = {Proceedings of the 11th International Conference on +// Concurrency Theory (Concur'00)}, +// pages = {153--167}, +// year = {2000}, +// editor = {C. Palamidessi}, +// volume = {1877}, +// series = {Lecture Notes in Computer Science}, +// address = {Pennsylvania, USA}, +// publisher = {Springer-Verlag} +// } +// +// @InProceedings{somenzi.00.cav, +// author = {Fabio Somenzi and Roderick Bloem}, +// title = {Efficient {B\"u}chi Automata for {LTL} Formul{\ae}}, +// booktitle = {Proceedings of the 12th International Conference on +// Computer Aided Verification (CAV'00)}, +// pages = {247--263}, +// year = {2000}, +// volume = {1855}, +// series = {Lecture Notes in Computer Science}, +// address = {Chicago, Illinois, USA}, +// publisher = {Springer-Verlag} +// } #include "common_sys.hh" @@ -88,11 +129,12 @@ #include #include #include +#include using namespace spot; const char argp_program_doc[] ="\ -Generate temporal logic formulas from predefined scalable patterns."; +Generate temporal logic formulas from predefined patterns."; enum { OPT_AND_F = 1, @@ -101,6 +143,8 @@ enum { OPT_CCJ_ALPHA, OPT_CCJ_BETA, OPT_CCJ_BETA_PRIME, + OPT_DAC_PATTERNS, + OPT_EH_PATTERNS, OPT_GH_Q, OPT_GH_R, OPT_GO_THETA, @@ -113,6 +157,7 @@ enum { OPT_RV_COUNTER_CARRY, OPT_RV_COUNTER_CARRY_LINEAR, OPT_RV_COUNTER_LINEAR, + OPT_SB_PATTERNS, OPT_U_LEFT, OPT_U_RIGHT, LAST_CLASS, @@ -126,6 +171,8 @@ const char* const class_name[LAST_CLASS] = "ccj-alpha", "ccj-beta", "ccj-beta-prime", + "dac-patterns", + "eh-patterns", "gh-q", "gh-r", "go-theta", @@ -138,6 +185,7 @@ const char* const class_name[LAST_CLASS] = "rv-counter-carry", "rv-counter-carry-linear", "rv-counter-linear", + "sb-patterns", "u-left", "u-right", }; @@ -164,8 +212,14 @@ static const argp_option options[] = "F(p&X(p&X(p&...X(p)))) & F(q&X(q&X(q&...X(q))))", 0 }, { "ccj-beta-prime", OPT_CCJ_BETA_PRIME, "RANGE", 0, "F(p&(Xp)&(XXp)&...(X...X(p))) & F(q&(Xq)&(XXq)&...(X...X(q)))", 0 }, + { "dac-patterns", OPT_DAC_PATTERNS, "RANGE", OPTION_ARG_OPTIONAL, + "Dwyer et al. [FMSP'98] Spec. Patterns for LTL " + "(range should be included in 1..45)", 0 }, + { "eh-patterns", OPT_EH_PATTERNS, "RANGE", OPTION_ARG_OPTIONAL, + "Etessami and Holzmann [Concur'00] patterns " + "(range should be included in 1..12)", 0 }, { "gh-q", OPT_GH_Q, "RANGE", 0, - "(F(p1)|G(p2))&(F(p2)|G(p3))&... &(F(pn)|G(p{n+1}))", 0 }, + "(F(p1)|G(p2))&(F(p2)|G(p3))&...&(F(pn)|G(p{n+1}))", 0 }, { "gh-r", OPT_GH_R, "RANGE", 0, "(GF(p1)|FG(p2))&(GF(p2)|FG(p3))&... &(GF(pn)|FG(p{n+1}))", 0}, { "go-theta", OPT_GO_THETA, "RANGE", 0, @@ -186,6 +240,9 @@ static const argp_option options[] = "n-bit counter w/ carry (linear size)", 0 }, { "rv-counter-linear", OPT_RV_COUNTER_LINEAR, "RANGE", 0, "n-bit counter (linear size)", 0 }, + { "sb-patterns", OPT_SB_PATTERNS, "RANGE", OPTION_ARG_OPTIONAL, + "Somenzi and Bloem [CAV'00] patterns " + "(range should be included in 1..27)", 0 }, { "u-left", OPT_U_LEFT, "RANGE", 0, "(((p1 U p2) U p3) ... U pn)", 0 }, OPT_ALIAS(gh-u), { "u-right", OPT_U_RIGHT, "RANGE", 0, "(p1 U (p2 U (... U pn)))", 0 }, @@ -234,6 +291,15 @@ enqueue_job(int pattern, const char* range_str) jobs.push_back(j); } +static void +enqueue_job(int pattern, int min, int max) +{ + job j; + j.pattern = pattern; + j.range = {min, max}; + jobs.push_back(j); +} + static int parse_opt(int key, char* arg, struct argp_state*) { @@ -262,6 +328,24 @@ parse_opt(int key, char* arg, struct argp_state*) case OPT_U_RIGHT: enqueue_job(key, arg); break; + case OPT_DAC_PATTERNS: + if (arg) + enqueue_job(key, arg); + else + enqueue_job(key, 1, 55); + break; + case OPT_EH_PATTERNS: + if (arg) + enqueue_job(key, arg); + else + enqueue_job(key, 1, 12); + break; + case OPT_SB_PATTERNS: + if (arg) + enqueue_job(key, arg); + else + enqueue_job(key, 1, 27); + break; default: return ARGP_ERR_UNKNOWN; } @@ -716,6 +800,162 @@ ltl_counter_carry(std::string bit, std::string marker, return formula::And(std::move(res)); } +static void bad_number(const char* pattern, int n, int max) +{ + std::ostringstream err; + err << "no pattern " << n << " for " << pattern + << ", supported range is 1.." << max; + throw std::runtime_error(err.str()); +} + +static formula +dac_pattern(int n) +{ + static const char* formulas[] = { + "[](!p0)", + "<>p2 -> (!p0 U p2)", + "[](p1 -> [](!p0))", + "[]((p1 & !p2 & <>p2) -> (!p0 U p2))", + "[](p1 & !p2 -> (!p0 W p2))", + + "<>(p0)", + "!p2 W (p0 & !p2)", + "[](!p1) | <>(p1 & <>p0)", + "[](p1 & !p2 -> (!p2 W (p0 & !p2)))", + "[](p1 & !p2 -> (!p2 U (p0 & !p2)))", + + "(!p0 W (p0 W (!p0 W (p0 W []!p0))))", + "<>p2 -> ((!p0 & !p2) U (p2 | ((p0 & !p2) U (p2 |" + " ((!p0 & !p2) U (p2 | ((p0 & !p2) U (p2 | (!p0 U p2)))))))))", + "<>p1 -> (!p1 U (p1 & (!p0 W (p0 W (!p0 W (p0 W []!p0))))))", + "[]((p1 & <>p2) -> ((!p0 & !p2) U (p2 | ((p0 & !p2) U (p2 |" + "((!p0 & !p2) U (p2 | ((p0 & !p2) U (p2 | (!p0 U p2))))))))))", + "[](p1 -> ((!p0 & !p2) U (p2 | ((p0 & !p2) U (p2 | ((!p0 & !p2) U" + "(p2 | ((p0 & !p2) U (p2 | (!p0 W p2) | []p0)))))))))", + + "[](p0)", + "<>p2 -> (p0 U p2)", + "[](p1 -> [](p0))", + "[]((p1 & !p2 & <>p2) -> (p0 U p2))", + "[](p1 & !p2 -> (p0 W p2))", + + "!p0 W p3", + "<>p2 -> (!p0 U (p3 | p2))", + "[]!p1 | <>(p1 & (!p0 W p3))", + "[]((p1 & !p2 & <>p2) -> (!p0 U (p3 | p2)))", + "[](p1 & !p2 -> (!p0 W (p3 | p2)))", + + "[](p0 -> <>p3)", + "<>p2 -> (p0 -> (!p2 U (p3 & !p2))) U p2", + "[](p1 -> [](p0 -> <>p3))", + "[]((p1 & !p2 & <>p2) -> ((p0 -> (!p2 U (p3 & !p2))) U p2))", + "[](p1 & !p2 -> ((p0 -> (!p2 U (p3 & !p2))) W p2))", + + "<>p0 -> (!p0 U (p3 & !p0 & X(!p0 U p4)))", + "<>p2 -> (!p0 U (p2 | (p3 & !p0 & X(!p0 U p4))))", + "([]!p1) | (!p1 U (p1 & <>p0 -> (!p0 U (p3 & !p0 & X(!p0 U p4)))))", + "[]((p1 & <>p2) -> (!p0 U (p2 | (p3 & !p0 & X(!p0 U p4)))))", + "[](p1 -> (<>p0 -> (!p0 U (p2 | (p3 & !p0 & X(!p0 U p4))))))", + + "(<>(p3 & X<>p4)) -> ((!p3) U p0)", + "<>p2 -> ((!(p3 & (!p2) & X(!p2 U (p4 & !p2)))) U (p2 | p0))", + "([]!p1) | ((!p1) U (p1 & ((<>(p3 & X<>p4)) -> ((!p3) U p0))))", + "[]((p1 & <>p2) -> ((!(p3 & (!p2) & X(!p2 U (p4 & !p2)))) U (p2 | p0)))", + "[](p1 -> (!(p3 & (!p2) & X(!p2 U (p4 & !p2))) U (p2 | p0) |" + " [](!(p3 & X<>p4))))", + + "[] (p3 & X<> p4 -> X(<>(p4 & <> p0)))", + "<>p2 -> (p3 & X(!p2 U p4) -> X(!p2 U (p4 & <> p0))) U p2", + "[] (p1 -> [] (p3 & X<> p4 -> X(!p4 U (p4 & <> p0))))", + "[] ((p1 & <>p2) -> (p3 & X(!p2 U p4) -> X(!p2 U (p4 & <> p0))) U p2)", + "[] (p1 -> (p3 & X(!p2 U p4) -> X(!p2 U (p4 & <> p0))) U (p2 |" + "[] (p3 & X(!p2 U p4) -> X(!p2 U (p4 & <> p0)))))", + + "[] (p0 -> <>(p3 & X<>p4))", + "<>p2 -> (p0 -> (!p2 U (p3 & !p2 & X(!p2 U p4)))) U p2", + "[] (p1 -> [] (p0 -> (p3 & X<> p4)))", + "[] ((p1 & <>p2) -> (p0 -> (!p2 U (p3 & !p2 & X(!p2 U p4)))) U p2)", + "[] (p1 -> (p0 -> (!p2 U (p3 & !p2 & X(!p2 U p4)))) U (p2 | []" + "(p0 -> (p3 & X<> p4))))", + + "[] (p0 -> <>(p3 & !p5 & X(!p5 U p4)))", + "<>p2 -> (p0 -> (!p2 U (p3 & !p2 & !p5 & X((!p2 & !p5) U p4)))) U p2", + "[] (p1 -> [] (p0 -> (p3 & !p5 & X(!p5 U p4))))", + "[] ((p1 & <>p2) -> (p0 -> (!p2 U (p3 & !p2 & !p5 & X((!p2 & !p5) U" + " p4)))) U p2)", + "[] (p1 -> (p0 -> (!p2 U (p3 & !p2 & !p5 & X((!p2 & !p5) U p4)))) U (p2 |" + "[] (p0 -> (p3 & !p5 & X(!p5 U p4)))))", + }; + + constexpr unsigned max = (sizeof formulas)/(sizeof *formulas); + if (n < 1 || (unsigned) n > max) + bad_number("--dac-patterns", n, max); + return spot::relabel(parse_formula(formulas[n - 1]), Pnn); +} + +static formula +eh_pattern(int n) +{ + static const char* formulas[] = { + "p0 U (p1 & G(p2))", + "p0 U (p1 & X(p2 U p3))", + "p0 U (p1 & X(p2 & (F(p3 & X(F(p4 & X(F(p5 & X(F(p6))))))))))", + "F(p0 & X(G(p1)))", + "F(p0 & X(p1 & X(F(p2))))", + "F(p0 & X(p1 U p2))", + "(F(G(p0))) | (G(F(p1)))", + "G(p0 -> (p1 U p2))", + "G(p0 & X(F(p1 & X(F(p2 & X(F(p3)))))))", + "(G(F(p0))) & (G(F(p1))) & (G(F(p2))) & (G(F(p3))) & (G(F(p4)))", + "(p0 U (p1 U p2)) | (p1 U (p2 U p0)) | (p2 U (p0 U p1))", + "G(p0 -> (p1 U ((G(p2)) | (G(p3)))))", + }; + + constexpr unsigned max = (sizeof formulas)/(sizeof *formulas); + if (n < 1 || (unsigned) n > max) + bad_number("--eh-patterns", n, max); + return spot::relabel(parse_formula(formulas[n - 1]), Pnn); +} + +static formula +sb_pattern(int n) +{ + static const char* formulas[] = { + "p0 U p1", + "p0 U (p1 U p2)", + "!(p0 U (p1 U p2))", + "G(F(p0)) -> G(F(p1))", + "(F(p0)) U (G(p1))", + "(G(p0)) U p1", + "!((F(F(p0))) <-> (F(p)))", + "!((G(F(p0))) -> (G(F(p))))", + "!((G(F(p0))) <-> (G(F(p))))", + "p0 R (p0 | p1)", + "(Xp0 U Xp1) | !X(p0 U p1)", + "(Xp0 U p1) | !X(p0 U (p0 & p1))", + "G(p0 -> F(p1)) & (((X(p0)) U p1) | !X(p0 U (p0 & p1)))", + "G(p0 -> F(p1)) & (((X(p0)) U X(p1)) | !X(p0 U p1))", + "G(p0 -> F(p1))", + "!G(p0 -> X(p1 R p2))", + "!(F(G(p0)) | F(G(p1)))", + "G(F(p0) & F(p1))", + "F(p0) & F(!p0)", + "(X(p1) & p2) R X(((p3 U p0) R p2) U (p3 R p2))", + "(G(p1 | G(F(p0))) & G(p2 | G(F(!p0)))) | G(p1) | G(p2)", + "(G(p1 | F(G(p0))) & G(p2 | F(G(!p0)))) | G(p1) | G(p2)", + "!((G(p1 | G(F(p0))) & G(p2 | G(F(!p0)))) | G(p1) | G(p2))", + "!((G(p1 | F(G(p0))) & G(p2 | F(G(!p0)))) | G(p1) | G(p2))", + "(G(p1 | X(G p0))) & (G (p2 | X(G !p0)))", + "G(p1 | (Xp0 & X!p0))", + // p0 U p0 can't be represented other than as p0 in Spot + "(p0 U p0) | (p1 U p0)", + }; + + constexpr unsigned max = (sizeof formulas)/(sizeof *formulas); + if (n < 1 || (unsigned) n > max) + bad_number("--sb-patterns", n, max); + return spot::relabel(parse_formula(formulas[n - 1]), Pnn); +} static void output_pattern(int pattern, int n) @@ -742,6 +982,12 @@ output_pattern(int pattern, int n) case OPT_CCJ_BETA_PRIME: f = formula::And({N_prime_n("p", n), N_prime_n("q", n)}); break; + case OPT_DAC_PATTERNS: + f = dac_pattern(n); + break; + case OPT_EH_PATTERNS: + f = eh_pattern(n); + break; case OPT_GH_Q: f = Q_n("p", n); break; @@ -778,6 +1024,9 @@ output_pattern(int pattern, int n) case OPT_RV_COUNTER_LINEAR: f = ltl_counter("b", "m", n, true); break; + case OPT_SB_PATTERNS: + f = sb_pattern(n); + break; case OPT_U_LEFT: f = bin_n("p", n, op::U, false); break; @@ -829,6 +1078,14 @@ main(int argc, char** argv) error(1, 0, "Nothing to do. Try '%s --help' for more information.", program_name); - run_jobs(); + try + { + run_jobs(); + } + catch (const std::runtime_error& e) + { + error(2, 0, "%s", e.what()); + } + return 0; } diff --git a/bin/man/genltl.x b/bin/man/genltl.x index 64e4d9d61..fa6ca6119 100644 --- a/bin/man/genltl.x +++ b/bin/man/genltl.x @@ -27,5 +27,19 @@ Proceedings of CAV'01. LNCS 2102. rv K. Rozier and M. Vardi: LTL Satisfiability Checking. Proceedings of Spin'07. LNCS 4595. +.TP +dac +M. B. Dwyer and G. S. Avrunin and J. C. Corbett: Property +Specification Patterns for Finite-state Verification. +Proceedings of FMSP'98. +.TP +eh +K. Etessami and G. J. Holzmann: Optimizing Büchi Automata. +Proceedings of Concur'00. LNCS 1877. +.TP +sb +F. Somenzi and R. Bloem: Efficient Büchi Automata for LTL Formulae. +Proceedings of CAV'00. LNCS 1855. + [SEE ALSO] .BR randltl (1) diff --git a/doc/org/genltl.org b/doc/org/genltl.org index 026872a9f..60f849942 100644 --- a/doc/org/genltl.org +++ b/doc/org/genltl.org @@ -3,11 +3,13 @@ #+SETUPFILE: setup.org #+HTML_LINK_UP: tools.html -This tool generates LTL formulas according to scalable patterns. -These pattern are usually taken from the literature (see the man page -for references). Sometimes the same pattern is given different names -in different papers, so we alias different option names to the same -pattern. +This tool outputs LTL formulas that either comes from named lists of +formulas, or from scalable patterns. + +These patterns are usually taken from the literature (see the +[[./man/genltl.1.html][=genltl=]](1) man page for references). Sometimes the same pattern is +given different names in different papers, so we alias different +option names to the same pattern. #+BEGIN_SRC sh :results verbatim :exports results genltl --help | sed -n '/Pattern selection:/,/^$/p' | sed '1d;$d' @@ -24,8 +26,11 @@ genltl --help | sed -n '/Pattern selection:/,/^$/p' | sed '1d;$d' --ccj-beta=RANGE F(p&X(p&X(p&...X(p)))) & F(q&X(q&X(q&...X(q)))) --ccj-beta-prime=RANGE F(p&(Xp)&(XXp)&...(X...X(p))) & F(q&(Xq)&(XXq)&...(X...X(q))) - --gh-q=RANGE (F(p1)|G(p2))&(F(p2)|G(p3))&... &(F(pn)|G(p{n+1})) - + --dac-patterns[=RANGE] Dwyer et al. [FMSP'98] Spec. Patterns for LTL + (range should be included in 1..45) + --eh-patterns[=RANGE] Etessami and Holzmann [Concur'00] patterns (range + should be included in 1..12) + --gh-q=RANGE (F(p1)|G(p2))&(F(p2)|G(p3))&...&(F(pn)|G(p{n+1})) --gh-r=RANGE (GF(p1)|FG(p2))&(GF(p2)|FG(p3))&... &(GF(pn)|FG(p{n+1})) --go-theta=RANGE !((GF(p1)&GF(p2)&...&GF(pn)) -> G(q->F(r))) @@ -41,6 +46,8 @@ genltl --help | sed -n '/Pattern selection:/,/^$/p' | sed '1d;$d' --rv-counter-carry-linear=RANGE n-bit counter w/ carry (linear size) --rv-counter-linear=RANGE n-bit counter (linear size) + --sb-patterns[=RANGE] Somenzi and Bloem [CAV'00] patterns (range should + be included in 1..27) --u-left=RANGE, --gh-u=RANGE (((p1 U p2) U p3) ... U pn) --u-right=RANGE, --gh-u2=RANGE, --go-phi=RANGE @@ -111,5 +118,130 @@ genltl --ccj-alpha=3 --lbt This is because most tools using =lbt='s syntax require atomic propositions to have the form =pNN=. + +Three 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=, 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 --sb --format=%F,%L,%f +#+END_SRC + +#+RESULTS: +#+begin_example +dac-patterns,1,G!p0 +dac-patterns,2,Fp0 -> (!p1 U p0) +dac-patterns,3,G(p0 -> G!p1) +dac-patterns,4,G((p0 & !p1 & Fp1) -> (!p2 U p1)) +dac-patterns,5,G((p0 & !p1) -> (!p2 W p1)) +dac-patterns,6,Fp0 +dac-patterns,7,!p0 W (!p0 & p1) +dac-patterns,8,G!p0 | F(p0 & Fp1) +dac-patterns,9,G((p0 & !p1) -> (!p1 W (!p1 & p2))) +dac-patterns,10,G((p0 & !p1) -> (!p1 U (!p1 & p2))) +dac-patterns,11,!p0 W (p0 W (!p0 W (p0 W G!p0))) +dac-patterns,12,Fp0 -> ((!p0 & !p1) U (p0 | ((!p0 & p1) U (p0 | ((!p0 & !p1) U (p0 | ((!p0 & p1) U (p0 | (!p1 U p0))))))))) +dac-patterns,13,Fp0 -> (!p0 U (p0 & (!p1 W (p1 W (!p1 W (p1 W G!p1)))))) +dac-patterns,14,G((p0 & Fp1) -> ((!p1 & !p2) U (p1 | ((!p1 & p2) U (p1 | ((!p1 & !p2) U (p1 | ((!p1 & p2) U (p1 | (!p2 U p1)))))))))) +dac-patterns,15,G(p0 -> ((!p1 & !p2) U (p2 | ((p1 & !p2) U (p2 | ((!p1 & !p2) U (p2 | ((p1 & !p2) U (p2 | (!p1 W p2) | Gp1))))))))) +dac-patterns,16,Gp0 +dac-patterns,17,Fp0 -> (p1 U p0) +dac-patterns,18,G(p0 -> Gp1) +dac-patterns,19,G((p0 & !p1 & Fp1) -> (p2 U p1)) +dac-patterns,20,G((p0 & !p1) -> (p2 W p1)) +dac-patterns,21,!p0 W p1 +dac-patterns,22,Fp0 -> (!p1 U (p0 | p2)) +dac-patterns,23,G!p0 | F(p0 & (!p1 W p2)) +dac-patterns,24,G((p0 & !p1 & Fp1) -> (!p2 U (p1 | p3))) +dac-patterns,25,G((p0 & !p1) -> (!p2 W (p1 | p3))) +dac-patterns,26,G(p0 -> Fp1) +dac-patterns,27,Fp0 -> ((p1 -> (!p0 U (!p0 & p2))) U p0) +dac-patterns,28,G(p0 -> G(p1 -> Fp2)) +dac-patterns,29,G((p0 & !p1 & Fp1) -> ((p2 -> (!p1 U (!p1 & p3))) U p1)) +dac-patterns,30,G((p0 & !p1) -> ((p2 -> (!p1 U (!p1 & p3))) W p1)) +dac-patterns,31,Fp0 -> (!p0 U (!p0 & p1 & X(!p0 U p2))) +dac-patterns,32,Fp0 -> (!p1 U (p0 | (!p1 & p2 & X(!p1 U p3)))) +dac-patterns,33,G!p0 | (!p0 U ((p0 & Fp1) -> (!p1 U (!p1 & p2 & X(!p1 U p3))))) +dac-patterns,34,G((p0 & Fp1) -> (!p2 U (p1 | (!p2 & p3 & X(!p2 U p4))))) +dac-patterns,35,G(p0 -> (Fp1 -> (!p1 U (p2 | (!p1 & p3 & X(!p1 U p4)))))) +dac-patterns,36,F(p0 & XFp1) -> (!p0 U p2) +dac-patterns,37,Fp0 -> (!(!p0 & p1 & X(!p0 U (!p0 & p2))) U (p0 | p3)) +dac-patterns,38,G!p0 | (!p0 U (p0 & (F(p1 & XFp2) -> (!p1 U p3)))) +dac-patterns,39,G((p0 & Fp1) -> (!(!p1 & p2 & X(!p1 U (!p1 & p3))) U (p1 | p4))) +dac-patterns,40,G(p0 -> ((!(!p1 & p2 & X(!p1 U (!p1 & p3))) U (p1 | p4)) | G!(p2 & XFp3))) +dac-patterns,41,G((p0 & XFp1) -> XF(p1 & Fp2)) +dac-patterns,42,Fp0 -> (((p1 & X(!p0 U p2)) -> X(!p0 U (p2 & Fp3))) U p0) +dac-patterns,43,G(p0 -> G((p1 & XFp2) -> X(!p2 U (p2 & Fp3)))) +dac-patterns,44,G((p0 & Fp1) -> (((p2 & X(!p1 U p3)) -> X(!p1 U (p3 & Fp4))) U p1)) +dac-patterns,45,G(p0 -> (((p1 & X(!p2 U p3)) -> X(!p2 U (p3 & Fp4))) U (p2 | G((p1 & X(!p2 U p3)) -> X(!p2 U (p3 & Fp4)))))) +dac-patterns,46,G(p0 -> F(p1 & XFp2)) +dac-patterns,47,Fp0 -> ((p1 -> (!p0 U (!p0 & p2 & X(!p0 U p3)))) U p0) +dac-patterns,48,G(p0 -> G(p1 -> (p2 & XFp3))) +dac-patterns,49,G((p0 & Fp1) -> ((p2 -> (!p1 U (!p1 & p3 & X(!p1 U p4)))) U p1)) +dac-patterns,50,G(p0 -> ((p1 -> (!p2 U (!p2 & p3 & X(!p2 U p4)))) U (p2 | G(p1 -> (p3 & XFp4))))) +dac-patterns,51,G(p0 -> F(p1 & !p2 & X(!p2 U p3))) +dac-patterns,52,Fp0 -> ((p1 -> (!p0 U (!p0 & p2 & !p3 & X((!p0 & !p3) U p4)))) U p0) +dac-patterns,53,G(p0 -> G(p1 -> (p2 & !p3 & X(!p3 U p4)))) +dac-patterns,54,G((p0 & Fp1) -> ((p2 -> (!p1 U (!p1 & p3 & !p4 & X((!p1 & !p4) U p5)))) U p1)) +dac-patterns,55,G(p0 -> ((p1 -> (!p2 U (!p2 & p3 & !p4 & X((!p2 & !p4) U p5)))) U (p2 | G(p1 -> (p3 & !p4 & X(!p4 U p5)))))) +eh-patterns,1,p0 U (p1 & Gp2) +eh-patterns,2,p0 U (p1 & X(p2 U p3)) +eh-patterns,3,p0 U (p1 & X(p2 & F(p3 & XF(p4 & XF(p5 & XFp6))))) +eh-patterns,4,F(p0 & XGp1) +eh-patterns,5,F(p0 & X(p1 & XFp2)) +eh-patterns,6,F(p0 & X(p1 U p2)) +eh-patterns,7,FGp0 | GFp1 +eh-patterns,8,G(p0 -> (p1 U p2)) +eh-patterns,9,G(p0 & XF(p1 & XF(p2 & XFp3))) +eh-patterns,10,GFp0 & GFp1 & GFp2 & GFp3 & GFp4 +eh-patterns,11,(p0 U (p1 U p2)) | (p1 U (p2 U p0)) | (p2 U (p0 U p1)) +eh-patterns,12,G(p0 -> (p1 U (Gp2 | Gp3))) +sb-patterns,1,p0 U p1 +sb-patterns,2,p0 U (p1 U p2) +sb-patterns,3,!(p0 U (p1 U p2)) +sb-patterns,4,GFp0 -> GFp1 +sb-patterns,5,Fp0 U Gp1 +sb-patterns,6,Gp0 U p1 +sb-patterns,7,!(Fp0 <-> Fp1) +sb-patterns,8,!(GFp0 -> GFp1) +sb-patterns,9,!(GFp0 <-> GFp1) +sb-patterns,10,p0 R (p0 | p1) +sb-patterns,11,(Xp0 U Xp1) | !X(p0 U p1) +sb-patterns,12,(Xp0 U p1) | !X(p0 U (p0 & p1)) +sb-patterns,13,G(p0 -> Fp1) & ((Xp0 U p1) | !X(p0 U (p0 & p1))) +sb-patterns,14,G(p0 -> Fp1) & ((Xp0 U Xp1) | !X(p0 U p1)) +sb-patterns,15,G(p0 -> Fp1) +sb-patterns,16,!G(p0 -> X(p1 R p2)) +sb-patterns,17,!(FGp0 | FGp1) +sb-patterns,18,G(Fp0 & Fp1) +sb-patterns,19,Fp0 & F!p0 +sb-patterns,20,(p0 & Xp1) R X(((p2 U p3) R p0) U (p2 R p0)) +sb-patterns,21,Gp2 | (G(p0 | GFp1) & G(p2 | GF!p1)) | Gp0 +sb-patterns,22,Gp0 | Gp2 | (G(p0 | FGp1) & G(p2 | FG!p1)) +sb-patterns,23,!(Gp2 | (G(p0 | GFp1) & G(p2 | GF!p1)) | Gp0) +sb-patterns,24,!(Gp0 | Gp2 | (G(p0 | FGp1) & G(p2 | FG!p1))) +sb-patterns,25,G(p0 | XGp1) & G(p2 | XG!p1) +sb-patterns,26,G(p0 | (Xp1 & X!p1)) +sb-patterns,27,p0 | (p1 U p0) +#+end_example + +Note that ~--sb-patterns=2 --sb-patterns=4 --sb-patterns=21..22~ also +have their complement formula listed as ~--sb-patterns=3 +--sb-patterns=8 --sb-patterns=23..24~. So if you build the set of +formula output by =genltl --sb-patterns= plus its negation, it will +contain only 46 formulas, not 54. + +#+BEGIN_SRC sh :results verbatim :exports both +genltl --sb | ltlfilt --uniq --count +(genltl --sb; genltl --sb | ltlfilt --negate) | ltlfilt --uniq --count +#+END_SRC +#+RESULTS: +: 27 +: 46 + # LocalWords: genltl num toc LTL scalable SRC sed gh pn fg FG gf qn -# LocalWords: ccj Xp XXp Xq XXq rv GFp lbt +# LocalWords: ccj Xp XXp Xq XXq rv GFp lbt utf SETUPFILE html dac +# LocalWords: Dwyer et al FMSP Etessami Holzmann sb Somenzi Bloem +# LocalWords: CAV LaTeX Fq Fp pNN Gp XFp XF XGp FGp XG ltlfilt uniq diff --git a/tests/Makefile.am b/tests/Makefile.am index 5e90ddbf4..28b6078ec 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -216,6 +216,7 @@ TESTS_twa = \ core/sim2.test \ core/sim3.test \ core/ltl2tgba.test \ + core/ltl2tgba2.test \ core/ltl2neverclaim.test \ core/ltl2neverclaim-lbtt.test \ core/ltlprod.test \ diff --git a/tests/core/ltl2tgba2.test b/tests/core/ltl2tgba2.test new file mode 100755 index 000000000..d823080c7 --- /dev/null +++ b/tests/core/ltl2tgba2.test @@ -0,0 +1,219 @@ +#!/bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016 +# Laboratoire de Recherche et Développement de l'Epita (LRDE). +# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +# département Systèmes Répartis Coopératifs (SRC), Université Pierre +# et Marie Curie. +# +# 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 . + +. ./defs + +# If the size of automata produced by ltl2tgba on the formulas we +# commonly use as benchmark, we want to notice it. + +set -e +genltl --dac-patterns --eh-patterns --sb-patterns --format=%F,%L,%f >pos +(cat pos; ltlfilt --negate pos/3 --format='!%<,%f') | ltlfilt -u -F-/3 >formulas + +ltl2tgba -Fformulas/3 --stats='%<,%f, %s,%t' | + ltl2tgba -D -F-/3 --stats='%<,%f,%>, %s,%t' | + ltl2tgba -B -F-/3 --stats='%<,%f,%>, %s,%t' | + ltl2tgba -BD -F-/3 --stats='%<,%>, %s,%t' > output + +cat >expected <