Hi Alexandre, Following checking more operators in SPOT, just want to inform that the operand overflow problem also applies to the unary operators: Kleene star, goto, nonconseq. rep. (all seem to be stored in uint8_t variable). Thanks, Roei -----Original Message----- From: Roei Nahum Sent: Wednesday, November 17, 2021 4:44 PM To: Alexandre Duret-Lutz <adl(a)lrde.epita.fr> Cc: spot(a)lrde.epita.fr; Yael Meller <yael(a)nvidia.com> Subject: RE: Assistance with Spot Great, thanks -----Original Message----- From: Alexandre Duret-Lutz <adl(a)lrde.epita.fr> Sent: Wednesday, November 17, 2021 3:45 PM To: Roei Nahum <roeina(a)nvidia.com> Cc: spot(a)lrde.epita.fr; Yael Meller <yael(a)nvidia.com> Subject: Re: Assistance with Spot External email: Use caution opening links or attachments Roei Nahum <roeina(a)nvidia.com> writes: Implication-based simplifications of LTL formulas are described in section 5.4.3 of https://nam11.safelinks.protection.outlook.com/?url=https%3A%2F%2Fspot.lrde… tls-impl=1 corresponds to tl_simplifier_options::synt_impl tls-impl=2 corresponds to tl_simplifier_options::synt_impl + tl_simplifier_options::containment_checks tls-impl=3 corresponds to tl_simplifier_options::synt_impl + tl_simplifier_options::containment_checks + tl_simplifier_options::containment_checks_stronger One question is whether your formulas require such simplification at all.

Alexandre Duret-Lutz <adl(a)lrde.epita.fr> writes: We should have a release of 2.10.1 later today with those overflow tests and a few additional minor fixes. I have some idea to modify the way those "ranged" operators are stored in order to support larger values, but that will be for a later version. Note that while using ##[400] fails | % ltl2tgba '{a ##[400] b}' --stats="%s states" | >>> {a ##[400] b} | ^^^ | 400 exceeds maximum supported repetition (254) a workaround is to do | % ltl2tgba '{a ##[200] ##[200] b}' --stats="%s states" | 402 states That workaround did not work in previous version because ##[200] ##[200] would be fused into ##[400]. The 2.10.1 will only fuse those operators if they do not overflow.