alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

ltldo, ltlcross: add support from ltl2ba, ltl2nba, ltl2dgba

Browse source 
* bin/common_trans.cc: Here.
* NEWS: Document this.
This commit is contained in:
Alexandre Duret-Lutz 2019-07-08 15:36:13 +02:00
parent 0d9cc29b46
commit 9f616e0451
2 changed files with 10 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

7
NEWS
View file

@ -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 among "Inf(0)", "t", or "f", and persistance properties have an
acceptance condition among "Fin(0)", "t", or "f". 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: Documentation:
- https://spot.lrde.epita.fr/tut90.html is a new file that explains - 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: 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 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 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. 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 terms of the existing PSL operators. ##[+] and ##[*] are sugar
for ##[1:$] and ##[0:$]. for ##[1:$] and ##[0:$].

8
bin/common_trans.cc
View file

@ -54,14 +54,16 @@ static shorthands_t shorthands_ltl[] = {
{ "ltl2dgra", " %f>%O" }, { "ltl2dgra", " %f>%O" },
{ "ltl2dpa", " %f>%O" }, { "ltl2dpa", " %f>%O" },
{ "ltl2dra", " %f>%O" }, { "ltl2dra", " %f>%O" },
{ "ltl2ldba", " %f>%O" },
{ "ltl2dstar", " --output-format=hoa %[MW]L %O"}, { "ltl2dstar", " --output-format=hoa %[MW]L %O"},
{ "ltl2ldba", " %f>%O" },
{ "ltl2na", " %f>%O" },
{ "ltl2nba", " %f>%O" },
{ "ltl2ngba", " %f>%O" },
{ "ltl2tgba", " -H %f>%O" }, { "ltl2tgba", " -H %f>%O" },
{ "ltl3ba", " -f %s>%O" }, { "ltl3ba", " -f %s>%O" },
{ "ltl3dra", " -f %s>%O" }, { "ltl3dra", " -f %s>%O" },
{ "ltl3hoa", " -f %f>%O" }, { "ltl3hoa", " -f %f>%O" },
// ltl3tela is the new name of ltl3hoa { "ltl3tela", " -f %f>%O" }, // ltl3tela is the new name of ltl3hoa
{ "ltl3tela", " -f %f>%O" },
{ "modella", " %[MWei^]L %O" }, { "modella", " %[MWei^]L %O" },
{ "spin", " -f %s>%O" }, { "spin", " -f %s>%O" },
}; };