diff --git a/NEWS b/NEWS index 9a5c0a1c7..fe5355e49 100644 --- a/NEWS +++ b/NEWS @@ -10,7 +10,7 @@ New in spot 2.12.0.dev (not yet released) consistency) and augmented (with new statistics). The new CSV output should be more useful when the input specification is decomposed, in particular, there is a column giving the number of - sub-specifications obained, and other statistics columns have + sub-specifications obtained, and other statistics columns have names starting with "max_" or "sum_" indicating how said statistics are updated across sub-specifications. @@ -44,6 +44,12 @@ New in spot 2.12.0.dev (not yet released) % genltl --lily-patterns | ltlsynt -q + - genltl's --pps-arbiter-standard and --pps-arbiter-strict have been + changed to rename variables {r1,r2,...,g1,g2...} as + {i1,i1,...,o1,o2,...} so that these formula can be fed directly to + ltlsynt. + + - 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. diff --git a/bin/genltl.cc b/bin/genltl.cc index 5a3ab3539..80789fc9d 100644 --- a/bin/genltl.cc +++ b/bin/genltl.cc @@ -140,11 +140,11 @@ static const argp_option options[] = OPT_ALIAS(beem-patterns), OPT_ALIAS(p), { "pps-arbiter-standard", gen::LTL_PPS_ARBITER_STANDARD, "RANGE", 0, - "Arbiter with n clients that sent requests (ri) and " - "receive grants (gi). Standard semantics.", 0 }, + "Arbiter with n clients that sent requests (iN) and " + "receive grants (oN). Standard semantics.", 0 }, { "pps-arbiter-strict", gen::LTL_PPS_ARBITER_STRICT, "RANGE", 0, - "Arbiter with n clients that sent requests (ri) and " - "receive grants (gi). Strict semantics.", 0 }, + "Arbiter with n clients that sent requests (iN) and " + "receive grants (oN). Strict semantics.", 0 }, { "r-left", gen::LTL_R_LEFT, "RANGE", 0, "(((p1 R p2) R p3) ... R pn)", 0 }, { "r-right", gen::LTL_R_RIGHT, "RANGE", 0, "(p1 R (p2 R (... R pn)))", 0 }, { "rv-counter", gen::LTL_RV_COUNTER, "RANGE", 0, "n-bit counter", 0 }, diff --git a/spot/gen/formulas.cc b/spot/gen/formulas.cc index ad7f2e8d4..f8314151b 100644 --- a/spot/gen/formulas.cc +++ b/spot/gen/formulas.cc @@ -1428,9 +1428,9 @@ namespace spot case LTL_P_PATTERNS: return p_pattern(n); case LTL_PPS_ARBITER_STANDARD: - return pps_arbiter("r", "g", n, false); + return pps_arbiter("i", "o", n, false); case LTL_PPS_ARBITER_STRICT: - return pps_arbiter("r", "g", n, true); + return pps_arbiter("i", "o", n, true); case LTL_R_LEFT: return bin_n("p", n, op::R, false); case LTL_R_RIGHT: