diff --git a/NEWS b/NEWS index b2fc91052..6a5796969 100644 --- a/NEWS +++ b/NEWS @@ -30,10 +30,13 @@ New in spot 2.7.5.dev (not yet released) among "Inf(0)", "t", or "f", and persistance properties have an acceptance condition among "Fin(0)", "t", or "f". + - ltldo and ltlcross learned shorthands to call the tools ltl2na, + ltl2nba, and ltl2ngba from Owl 19.06. + Documentation: - https://spot.lrde.epita.fr/tut90.html is a new file that explains - the purpose of the =spot::bdd_dict= object. + the purpose of the spot::bdd_dict object. Library: @@ -102,7 +105,7 @@ New in spot 2.7.5.dev (not yet released) operators from SVA. So {##2 a ##0 b[+] ##1 c ##2 e} is another way to write {[*2];a:b[+];c;1;e}. The syntax {a ##[i:j] b} is replaced in different ways depending on the values of i, a, and b. - The formula::sugar_delay() function implement this SVA operator in + The formula::sugar_delay() function implements this SVA operator in terms of the existing PSL operators. ##[+] and ##[*] are sugar for ##[1:$] and ##[0:$]. diff --git a/bin/common_trans.cc b/bin/common_trans.cc index 73b6d8f8d..ec2b84542 100644 --- a/bin/common_trans.cc +++ b/bin/common_trans.cc @@ -54,14 +54,16 @@ static shorthands_t shorthands_ltl[] = { { "ltl2dgra", " %f>%O" }, { "ltl2dpa", " %f>%O" }, { "ltl2dra", " %f>%O" }, - { "ltl2ldba", " %f>%O" }, { "ltl2dstar", " --output-format=hoa %[MW]L %O"}, + { "ltl2ldba", " %f>%O" }, + { "ltl2na", " %f>%O" }, + { "ltl2nba", " %f>%O" }, + { "ltl2ngba", " %f>%O" }, { "ltl2tgba", " -H %f>%O" }, { "ltl3ba", " -f %s>%O" }, { "ltl3dra", " -f %s>%O" }, { "ltl3hoa", " -f %f>%O" }, - // ltl3tela is the new name of ltl3hoa - { "ltl3tela", " -f %f>%O" }, + { "ltl3tela", " -f %f>%O" }, // ltl3tela is the new name of ltl3hoa { "modella", " %[MWei^]L %O" }, { "spin", " -f %s>%O" }, };