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@lrde.epita.fr> Cc: spot@lrde.epita.fr; Yael Meller <yael@nvidia.com> Subject: RE: Assistance with Spot Great, thanks -----Original Message----- From: Alexandre Duret-Lutz <adl@lrde.epita.fr> Sent: Wednesday, November 17, 2021 3:45 PM To: Roei Nahum <roeina@nvidia.com> Cc: spot@lrde.epita.fr; Yael Meller <yael@nvidia.com> Subject: Re: Assistance with Spot External email: Use caution opening links or attachments Roei Nahum <roeina@nvidia.com> writes:
I didn't fully understand what utility I miss by lowering tls-impl to 2 (or to lower values) - are there additional materials I can use?
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.epita.fr%2Ftl.pdf&data=04%7C01%7Croeina%40nvidia.com%7C133a8e829b2f4612dc1a08d9a9d077d7%7C43083d15727340c1b7db39efd9ccc17a%7C0%7C0%7C637727535773155654%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=cj4fEwQ%2FtjSnZJyDsL1swDyjmfJGBcy%2BUCmKSoSC4a4%3D&reserved=0 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.