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.
Hi,
When invoking `autfilt sub.aut --included-in=sup.aut` on the two enclosed
Buchi automata
with Spot 2.10 I am getting:
```
Too many acceptance sets used. The limit is 32.
```
With Spot 2.9.7 I was getting a non-terminating execution.
Is it the expected result? If so, what is the explanation behind the too
many acceptance sets?
Is it the complementation procedure for `sup.aut` that fails?
Thank you and keep up with the excellent work,
Pierre.
Hi,
I was wondering if someone could point me to resources in spot that show
how to evaluate an LTL word or trace on an automaton.
Or anyway to check whether a trace or word satisfies a particular LTL
formula.
I'm new to Spot. So far I've been able to use the python notebook - word,
(and other examples) to iterate over an automaton generated from an LTL
formula.
Thank you so much,
--
Regards,
Fatma
HI,
My name is Roei Nahum. Your wonderful platform helps me to translate temporal formulas into Buchi automata. I downloaded Spot (version 2.9.4), and wrote a C++ program based on Spot API.
As the following code snippet shows, I configured Spot so it will produce small state-based Buchi automata. I also skip the wdba minimalization.
spot::option_map extra_options;
spot::bdd_dict_ptr dict = spot::make_bdd_dict();
spot::translator* trans;
extra_options.set("wdba-minimize", 0);
trans = new spot::translator(dict, &extra_options);
trans->set_type(spot::postprocessor::BA);
trans->set_pref(spot::postprocessor::Small);
twa_graph_ptr aut = trans->run(pf.f);
Spot works very well on few examples I checked, but having a hard time with the following formula, in which it runs for a very long time without finishing:
(!G(!({{a ##[1:500] b} ##[1:500] c})))
Can you please help me understand why? Is there anything I can configure differently in order to help it to be converged?
Thanks in advance,
Roei
