One confusion about the output

[guest-oo]

May I ask that LTL formula is not directly output in the output result? May I ask how to directly output LTL formula?

[francescofuggitti]

Hi @guest-oo,

thanks for reaching out!

Can you elaborate more on your requests? Perhaps with some examples of what is output now, and what would you like it to be?

[guest-oo]

The output is now Declare Template: (ExistenceTwo Slack)

English meaning: Slack will happen at least twice.

Confidence: 1.0441302578101386e-07, what should I do if I want to output it as A standard LTL statement such as G(A)&G(B)?

[francescofuggitti]

So, I guess you're currently using the pretty print in the engine utils module.

In the case you want to output only the LTL standard statement, you should replace the pretty print with something like

[...]
ltlf_formulas = translate(utterance, engine, filter)

for k, v in ltlf_formulas.items():
    print(f"LTL formula:  {k.to_ltlf()}", end="\n")

In general, you can call all methods available in the declare.py module for a Formula in the output, namely:

• to_english()
• to_ltlf()
• to_ppltl()

Let me know if this helps. Cheers!