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://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.
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.
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.
Roei Nahum roeina@nvidia.com writes:
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).
Yes, I've added an overflow test to all of those already; they all use the same parsing rule and data structure.
Alexandre Duret-Lutz adl@lrde.epita.fr writes:
Yes, I've added an overflow test to all of those already; they all use the same parsing rule and data structure.
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.
-
Alexandre Duret-Lutz -
Roei Nahum