From 939f63eec987bd5bee62abb43b86bf00df4b2c9d Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 3 Jun 2018 18:17:48 +0200 Subject: [PATCH] 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. --- NEWS | 4 +- bin/common_output.cc | 33 +++++-- bin/common_output.hh | 11 ++- bin/genltl.cc | 47 +++++++-- bin/ltlfilt.cc | 3 +- python/spot/gen.i | 58 ++++++++--- spot/gen/formulas.cc | 86 +++++++++++++++- spot/gen/formulas.hh | 8 +- tests/core/genltl.test | 48 +++++---- tests/python/gen.ipynb | 217 ++++++++++++++++++++++++++++++++++++++++- 10 files changed, 462 insertions(+), 53 deletions(-) diff --git a/NEWS b/NEWS index 990d6e614..3d6803e13 100644 --- a/NEWS +++ b/NEWS @@ -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] diff --git a/bin/common_output.cc b/bin/common_output.cc index 55448b079..a264c3332 100644 --- a/bin/common_output.cc +++ b/bin/common_output.cc @@ -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 filename_; - spot::printable_value line_; + spot::printable_value line_; spot::printable_value prefix_; spot::printable_value suffix_; spot::printable_value 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); +} diff --git a/bin/common_output.hh b/bin/common_output.hh index 6850eeda6..1cff67229 100644 --- a/bin/common_output.hh +++ b/bin/common_output.hh @@ -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); diff --git a/bin/genltl.cc b/bin/genltl.cc index e0e3dd865..b3fd1ae9c 100644 --- a/bin/genltl.cc +++ b/bin/genltl.cc @@ -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 jobs_t; @@ -211,9 +214,28 @@ enqueue_job(int pattern, const char* range_str = nullptr) { job j; j.pattern = static_cast(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; diff --git a/bin/ltlfilt.cc b/bin/ltlfilt.cc index dc507ff83..f44dfe82d 100644 --- a/bin/ltlfilt.cc +++ b/bin/ltlfilt.cc @@ -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); diff --git a/python/spot/gen.i b/python/spot/gen.i index b2fa5057f..b3cc29769 100644 --- a/python/spot/gen.i +++ b/python/spot/gen.i @@ -1,5 +1,5 @@ // -*- 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 - else: - ls = len(spec) - if ls == 2: - pat, min, max = spec[0], spec[1], spec[1] - elif ls == 3: - pat, min, max = spec + argc = ltl_pattern_argc(spec) + if argc == 1: + max = ltl_pattern_max(spec) or 10 else: - raise RuntimeError("invalid pattern specification") + min2 = 1 + max = max2 = 3 + else: + argc = ltl_pattern_argc(spec[0]) + ls = len(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: + 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 diff --git a/spot/gen/formulas.cc b/spot/gen/formulas.cc index 8d1cfea27..6033112de 100644 --- a/spot/gen/formulas.cc +++ b/spot/gen/formulas.cc @@ -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"); + } } } diff --git a/spot/gen/formulas.hh b/spot/gen/formulas.hh index b56bee195..8c6996ab1 100644 --- a/spot/gen/formulas.hh +++ b/spot/gen/formulas.hh @@ -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); } } diff --git a/tests/core/genltl.test b/tests/core/genltl.test index 3615e0ebc..706ac92b4 100755 --- a/tests/core/genltl.test +++ b/tests/core/genltl.test @@ -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 < 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 diff --git a/tests/python/gen.ipynb b/tests/python/gen.ipynb index 7d95c9d53..a6c655a52 100644 --- a/tests/python/gen.ipynb +++ b/tests/python/gen.ipynb @@ -295,6 +295,219 @@ " display(f)" ] }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Some LTL patterns take two arguments. In this case, the arguments passed to `ltl_pattern()` should be one of:\n", + "- `(id, n, m)` giving the value of both arguments,\n", + "- `(id, min1, max1, min2, max2)` specifying a range for both arguments,\n", + "- `(id, n)` equivalent to `(id, n, n)`,\n", + "- `id` equivalent to `(id, 1, 3, 1, 3)`." + ] + }, + { + "cell_type": "code", + "execution_count": 5, + "metadata": {}, + "outputs": [ + { + "data": { + "text/latex": [ + "$\\mathsf{G} \\mathsf{F} a_{1} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{0} \\mathbin{\\mathsf{U}} \\mathsf{X} b)$" + ], + "text/plain": [ + "GFa1 U G(GFa0 U Xb)" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$\\mathsf{G} \\mathsf{F} a_{1} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{0} \\mathbin{\\mathsf{U}} \\mathsf{X} \\mathsf{X} b)$" + ], + "text/plain": [ + "GFa1 U G(GFa0 U XXb)" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$\\mathsf{G} \\mathsf{F} a_{1} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{0} \\mathbin{\\mathsf{U}} \\mathsf{X} \\mathsf{X} \\mathsf{X} b)$" + ], + "text/plain": [ + "GFa1 U G(GFa0 U XXXb)" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$\\mathsf{G} \\mathsf{F} a_{2} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{1} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{0} \\mathbin{\\mathsf{U}} \\mathsf{X} b))$" + ], + "text/plain": [ + "GFa2 U G(GFa1 U G(GFa0 U Xb))" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$\\mathsf{G} \\mathsf{F} a_{2} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{1} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{0} \\mathbin{\\mathsf{U}} \\mathsf{X} \\mathsf{X} b))$" + ], + "text/plain": [ + "GFa2 U G(GFa1 U G(GFa0 U XXb))" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$\\mathsf{G} \\mathsf{F} a_{2} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{1} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{0} \\mathbin{\\mathsf{U}} \\mathsf{X} \\mathsf{X} \\mathsf{X} b))$" + ], + "text/plain": [ + "GFa2 U G(GFa1 U G(GFa0 U XXXb))" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$\\mathsf{G} \\mathsf{F} a_{3} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{2} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{1} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{0} \\mathbin{\\mathsf{U}} \\mathsf{X} b)))$" + ], + "text/plain": [ + "GFa3 U G(GFa2 U G(GFa1 U G(GFa0 U Xb)))" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$\\mathsf{G} \\mathsf{F} a_{3} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{2} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{1} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{0} \\mathbin{\\mathsf{U}} \\mathsf{X} \\mathsf{X} b)))$" + ], + "text/plain": [ + "GFa3 U G(GFa2 U G(GFa1 U G(GFa0 U XXb)))" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$\\mathsf{G} \\mathsf{F} a_{3} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{2} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{1} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{0} \\mathbin{\\mathsf{U}} \\mathsf{X} \\mathsf{X} \\mathsf{X} b)))$" + ], + "text/plain": [ + "GFa3 U G(GFa2 U G(GFa1 U G(GFa0 U XXXb)))" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "for f in sg.ltl_patterns(sg.LTL_SEJK_F):\n", + " display(f)" + ] + }, + { + "cell_type": "code", + "execution_count": 6, + "metadata": {}, + "outputs": [ + { + "data": { + "text/latex": [ + "$\\mathsf{G} \\mathsf{F} a_{2} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{1} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{0} \\mathbin{\\mathsf{U}} \\mathsf{X} \\mathsf{X} \\mathsf{X} b))$" + ], + "text/plain": [ + "GFa2 U G(GFa1 U G(GFa0 U XXXb))" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$\\mathsf{G} \\mathsf{F} a_{2} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{1} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{0} \\mathbin{\\mathsf{U}} \\mathsf{X} \\mathsf{X} b))$" + ], + "text/plain": [ + "GFa2 U G(GFa1 U G(GFa0 U XXb))" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$\\mathsf{G} \\mathsf{F} a_{1} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{0} \\mathbin{\\mathsf{U}} \\mathsf{X} b)$" + ], + "text/plain": [ + "GFa1 U G(GFa0 U Xb)" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$\\mathsf{G} \\mathsf{F} a_{1} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{0} \\mathbin{\\mathsf{U}} \\mathsf{X} \\mathsf{X} b)$" + ], + "text/plain": [ + "GFa1 U G(GFa0 U XXb)" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$\\mathsf{G} \\mathsf{F} a_{2} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{1} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{0} \\mathbin{\\mathsf{U}} \\mathsf{X} b))$" + ], + "text/plain": [ + "GFa2 U G(GFa1 U G(GFa0 U Xb))" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$\\mathsf{G} \\mathsf{F} a_{2} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{1} \\mathbin{\\mathsf{U}} \\mathsf{G} (\\mathsf{G} \\mathsf{F} a_{0} \\mathbin{\\mathsf{U}} \\mathsf{X} \\mathsf{X} b))$" + ], + "text/plain": [ + "GFa2 U G(GFa1 U G(GFa0 U XXb))" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "for f in sg.ltl_patterns((sg.LTL_SEJK_F, 2, 3), (sg.LTL_SEJK_F, 2), (sg.LTL_SEJK_F, 1, 2, 1, 2)):\n", + " display(f)" + ] + }, { "cell_type": "markdown", "metadata": {}, @@ -306,7 +519,7 @@ }, { "cell_type": "code", - "execution_count": 5, + "execution_count": 7, "metadata": {}, "outputs": [ { @@ -977,7 +1190,7 @@ }, { "cell_type": "code", - "execution_count": 6, + "execution_count": 8, "metadata": {}, "outputs": [ {