whitemech/LTLf2DFA

Same syntax for multiple backends

Closed this issue · 2 comments

ivanDonadello commented

Dear developers,

during the Whitemech project several backend engines for translating an LTLf formula into DFAs have been developed (e.g., ltlf2dfa or Lydia). It could be really useful to have a common syntax for the input formulas so users can use/switch to different backends without the need of rewriting the formulas.

Best

Ivan

francescofuggitti commented

Hi @ivanDonadello, thank you for submitting the issue. As you can see, here at LTLf2DFA we have planned in #51 to integrate pylogics with the package, which will give LTLf2DFA a common syntax with other tools.

However, this issue seems more related to the logaut package (I guess you refer to logaut as you talk about backends) rather than directly to LTLf2DFA. In fact, in general, if a tool wants to keep its own syntax (not the case for LTLf2DFA), it is an issue of logaut to make things work with multiple backends.

ivanDonadello commented

Thanks a lot @francescofuggitti! Yes, this issue is more related to logaut. In addition, I saw in #51 a "pay attention to the symbol naming convention", indeed, for the Lydia backend the symbols in the DFA transitions are lowercase, whereas in LTLF2DFA are in uppercase, so a normalization would be helpful. I think that maybe also this is for logaut. Do you want me to open an issue there?