November 2021 - Spot

[BUG] Tests fail to build on FreeBSD: error: use of undeclared identifier 'sched_getcpu'
by Yuri 23 Nov '21

23 Nov '21

On FreeBSD 13 version 2.10 fails to build tests: c++ -DHAVE_CONFIG_H -I. -I.. -I.. -I.. -I../buddy/src \-I../lib -I../lib -fno-omit-frame-pointer -D_THREAD_SAFE -DNDEBUG -O2 -pipe -fno-omit-frame-pointer -fstack-protector-strong -fno-strict-aliasing -fno-omit-frame-pointer -fvisibility=hidden -fvisibility-inlines-hidden -DSPOT_BUILD -std=c++17 -g -O3 -ffast-math -fstrict-aliasing -fomit-frame-pointer -pthread -O2 -pipe -fno-omit-frame-pointer -fstack-protector-strong -fno-strict-aliasing -fno-omit-frame-pointer -fvisibility=hidden -fvisibility-inlines-hidden -DSPOT_BUILD -std=c++17 -g -O3 -ffast-math -fstrict-aliasing -fomit-frame-pointer -MT ltsmin/modelcheck-modelcheck.o -MD -MP -MF ltsmin/.deps/modelcheck-modelcheck.Tpo -c -o ltsmin/modelcheck-modelcheck.o `test -f 'ltsmin/modelcheck.cc' || echo './'`ltsmin/modelcheck.cc In file included from ltsmin/modelcheck.cc:27: ../spot/mc/mc_instanciator.hh:122:43: error: use of undeclared identifier 'sched_getcpu' << ": on CPU " << sched_getcpu() << '\n'; ^ ../spot/mc/mc_instanciator.hh:134:9: error: unknown type name 'cpu_set_t'; did you mean 'cpusetid_t'? cpu_set_t cpuset; ^~~~~~~~~ cpusetid_t /usr/include/sys/types.h:86:22: note: 'cpusetid_t' declared here typedef __cpusetid_t cpusetid_t; ^ In file included from ltsmin/modelcheck.cc:27: ../spot/mc/mc_instanciator.hh:135:9: error: use of undeclared identifier 'CPU_ZERO' CPU_ZERO(&cpuset); ^ ../spot/mc/mc_instanciator.hh:136:9: error: use of undeclared identifier 'CPU_SET' CPU_SET(i, &cpuset); ^ ../spot/mc/mc_instanciator.hh:137:18: error: use of undeclared identifier 'pthread_setaffinity_np' int rc = pthread_setaffinity_np(threads[i].native_handle(), ^ ../spot/mc/mc_instanciator.hh:138:48: error: use of undeclared identifier 'cpu_set_t' sizeof(cpu_set_t), &cpuset); ^ 6 errors generated. Thanks, Yuri

2 1

Re: [Spot] Assistance with Spot
by Alexandre Duret-Lutz 19 Nov '21

19 Nov '21

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.

2 4

Behavior change in autfilt from 2.9.7 to 2.10
by Pierre Ganty 17 Nov '21

17 Nov '21

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.

2 1

Evaluating a word on an automaton/formula
by Fatma Faruq 17 Nov '21

17 Nov '21

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

2 1

Assistance with Spot
by Roei Nahum 16 Nov '21

16 Nov '21

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

2 3