Is TL Parsing Fully Implemented?

[junghye01]

NeuS-V/neus_v/veval/parse.py

Line 1 in 03db19a

def parse_tl_formula(tl_spec: str) -> str:

I’m trying to understand the intended semantics of the TL/LTL parsing utilities and noticed two transformations that seem to change the meaning of the specification.

1. parse_tl_formula: G → F

• G (ALWAYS) and F (EVENTUALLY) have different semantics, but the code appears to rewrite G into F
• Could you clarify the rationale for this conversion? Is it due to a Storm parser limitation, an intentional approximation for the evaluation pipeline, or something else?

2. parse_until_to_next_frame: U → & F

• The function replaces U globally via tl_spec.replace("U", "& F").
• What is the motivation behind rewriting U this way? Is it meant to approximate “until” under some assumptions (e.g., windowed evaluation), or to fit a restricted logic fragment supported by the checker?

Finally, given these semantic-changing rewrites, I’m wondering whether the TL specification handling is still incomplete / work-in-progress , or if this is the intended final behavior. Any clarification or documentation pointers would be greatly appreciated.

Thanks!