17 Nov
2021
17 Nov
'21
2:45 p.m.
Roei Nahum <roeina(a)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://spot.lrde.epita.fr/tl.pdf
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.