Re: [Spot] 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.