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....
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.