diff --git a/NEWS b/NEWS index 5734a7f33..4c5217c48 100644 --- a/NEWS +++ b/NEWS @@ -50,6 +50,12 @@ New in spot 2.2.2.dev (Not yet released) print the class of a formula in the temporal hierarchy of Manna & Pnueli using %h. See https://www.lrde.epita.fr/hierarchy.html + * ltldo and ltlcross learned a --relabel option to force the + relabeling of atomic propositions to p0, p1, etc. This is more + useful with ltldo, as it allows calling a tool that restricts the + atomic propositions it supports, and the output automaton will + then be fixed to use the original atomic propositions. + Library: * A twa is required to have at least one state, the initial state. diff --git a/bin/common_trans.cc b/bin/common_trans.cc index a446f0545..6b9363c0a 100644 --- a/bin/common_trans.cc +++ b/bin/common_trans.cc @@ -622,6 +622,7 @@ exec_with_timeout(const char* cmd) enum { OPT_LIST = 1, + OPT_RELABEL = 2, }; static const argp_option options[] = { @@ -632,6 +633,8 @@ static const argp_option options[] = { "timeout", 'T', "NUMBER", 0, "kill translators after NUMBER seconds", 0 }, { "list-shorthands", OPT_LIST, nullptr, 0, "list availabled shorthands to use in COMMANDFMT", 0}, + { "relabel", OPT_RELABEL, nullptr, 0, + "always relabel atomic propositions before calling any translator", 0 }, /**************************************************/ { nullptr, 0, nullptr, 0, "COMMANDFMT should specify input and output arguments using the " @@ -649,7 +652,8 @@ static const argp_option options[] = "If either %l, %L, or %T are used, any input formula that does " "not use LBT-style atomic propositions (i.e. p0, p1, ...) will be " "relabeled automatically. Likewise if %s or %S are used with " - "atomic proposition that compatible with Spin's syntax.\n" + "atomic proposition that compatible with Spin's syntax. You can " + "force this relabeling to always occur with option --relabel.\n" "The sequences %f,%s,%l,%w,%F,%S,%L,%W can optionally be \"infixed\"" " by a bracketed sequence of operators to unabbreviate before outputing" " the formula. For instance %[MW]f will rewrite operators M and W" @@ -660,6 +664,8 @@ static const argp_option options[] = { nullptr, 0, nullptr, 0, nullptr, 0 } }; +bool opt_relabel = false; + static int parse_opt_trans(int key, char* arg, struct argp_state*) { switch (key) @@ -677,6 +683,9 @@ static int parse_opt_trans(int key, char* arg, struct argp_state*) case OPT_LIST: show_shorthands(); exit(0); + case OPT_RELABEL: + opt_relabel = true; + break; default: return ARGP_ERR_UNKNOWN; } diff --git a/bin/common_trans.hh b/bin/common_trans.hh index 776ea2730..ac87498da 100644 --- a/bin/common_trans.hh +++ b/bin/common_trans.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement de -// l'Epita (LRDE). +// Copyright (C) 2015, 2016, 2017 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -29,6 +29,7 @@ extern const struct argp trans_argp; +extern bool opt_relabel; struct translator_spec { diff --git a/bin/ltlcross.cc b/bin/ltlcross.cc index 7e22feff2..4f067372b 100644 --- a/bin/ltlcross.cc +++ b/bin/ltlcross.cc @@ -992,10 +992,12 @@ namespace { static unsigned round = 0; - // If we need LBT atomic proposition in any of the input or - // output, relabel the formula. - if ((!f.has_lbt_atomic_props() && - (runner.has('l') || runner.has('L') || runner.has('T'))) + if (opt_relabel + // If we need LBT atomic proposition in any of the input or + // output, relabel the formula. + || (!f.has_lbt_atomic_props() && + (runner.has('l') || runner.has('L') || runner.has('T'))) + // Likewise for Spin || (!f.has_spin_atomic_props() && (runner.has('s') || runner.has('S')))) f = spot::relabel(f, spot::Pnn); diff --git a/bin/ltldo.cc b/bin/ltldo.cc index 1664704ae..14f10df47 100644 --- a/bin/ltldo.cc +++ b/bin/ltldo.cc @@ -299,8 +299,9 @@ namespace // If atomic propositions are incompatible with one of the // output, relabel the formula. - if ((!f.has_lbt_atomic_props() && - (runner.has('l') || runner.has('L') || runner.has('T'))) + if (opt_relabel + || (!f.has_lbt_atomic_props() && + (runner.has('l') || runner.has('L') || runner.has('T'))) || (!f.has_spin_atomic_props() && (runner.has('s') || runner.has('S')))) { diff --git a/doc/org/ltldo.org b/doc/org/ltldo.org index 37bd1efa3..ca50be734 100644 --- a/doc/org/ltldo.org +++ b/doc/org/ltldo.org @@ -359,7 +359,6 @@ ltldo ltl3ba 'ltl3ba -H2' -f GFa --stats='%T, %s states, %e edges' : ltl3ba, 2 states, 4 edges : ltl3ba -H2, 1 states, 2 edges - * Transparent renaming If you have ever tried to use =spin=, =ltl2ba=, or =ltl3ba=, to translate @@ -407,6 +406,10 @@ formula has atomic propositions incompatible with Spin's conventions; or when some command uses =%l= or =%L=, and the formula has atomic propositions incompatible with [[http://www.tcs.hut.fi/Software/maria/tools/lbt/][LBT's conventions]]. +For =%f=, =%w=, =%F=, and =%W=, no relabeling is automatically +performed, but you can pass option =--relabel= if you need to force it +for some reason (e.g., if you have a tool that uses almost Spot's +syntax, but cannot cope with double-quoted atomic propositions). There are some cases where the renaming is not completely transparent. For instance if a translator tool outputs some HOA file named after diff --git a/tests/core/ltl3ba.test b/tests/core/ltl3ba.test index 04c028bac..9692beaac 100755 --- a/tests/core/ltl3ba.test +++ b/tests/core/ltl3ba.test @@ -47,3 +47,19 @@ sed 's/[^,]//g'