Spot

spot@lrde.epita.fr

209 discussions

Start a nNew thread

Regarding LTL with past

by David Lidell

2 years, 8 months

Question regarding Spot operations on automata

by Edmond Irani Liu

Dear Spot team, greetings. This is Edmond Irani Liu, a Ph.D student at the Cyber-Physical Systems Group, Technical University of Munich. First of all, I would say thank you for your effort in developing such a great platform and tool! I have been using Spot lately, and have a few questions regarding automata manipulation in Spot. I attach a Jupyter notebook explaining my use case: we are using spot to compute the product automata of some LTLf formulas and our system described in Kripke structure. If I understand this (https://spot.lrde.epita.fr/tut12.html) page correctly, we need to append a new state at the end of the system that holds a proposition which becomes inactive at the end of our system. Could you give us a quick feedback if our formulation in the notebook is correct? There states z1-z8 are system states, and z9 is the extra state for Spot to correctly handle LTLf formulas. As we are trying to obtain the product automaton of a relatively large formula with our system, we assume that breaking down the formula and paralellizing the computation will observe a speed up in the computation. We would like to inquire if there exist operations like taking the union or intersection of the accepting runs of the automata? The concrete example is illustrated in the note book. Is there a documentation available somewhere explaining the functions of objects in the Python wrapper? I tried looking around but couldn't find one explaining those. An example is also attached. Thank you for your attention. Looking forward to hearing from you. Kind Regards, Edmond

2 years, 9 months

How to read disjunction output?

by Mark Santolucito

Hi there, Thanks so much for the great tool! I am having trouble understanding the disjunction on state transitions. For example, I have the following small spec: ASSUME { G (p1); } GUARANTEE { G ((x) && (! (y)) || ((y) && (! (x)))); G (F x); G (F y); } From this, ltlsynt gives me: AP: 3 "x" "y" "p1" acc-name: all Acceptance: 0 t properties: trans-labels explicit-labels state-acc deterministic --BODY-- State: 0 [!0&!1&!2 | 0&1&!2] 1 [!0&1&2] 1 State: 1 [!0&!1&!2 | 0&1&!2] 1 [0&!1&2] 0 --END-- Should I understand the "[!0&!1&!2 | 0&1&!2] 1" to mean that when !2 is true, the system is free to choose from !0&!1 or 0&1? On a related note, due to the ASSUME in the spec, !2 should never be true anyway. Is there a way to filter this out of the model? For context, I am really looking to get a Mealy Machine out of ltlsynt which I can then convert into program code that would run in an infinite loop. Maybe I am just going about this the wrong way? Mark

2 years, 11 months

How to free the memory of an automaton in spot's Python API?

by Yechuan Xia

Hi, I'm building some automatons using spot's python interface. Simply, codes like: for i in n: temp_aut = spot.automaton(aut.to_str()) # copy an automaton ...something del temp_aut But I found that whenever it enters a new loop, the memory of the automaton assigned to temp_aut is not freed. And it leads to a memory overflow. I thought this might be solved with 'delete temp_aut' in the C++ version spot, but in the python interface 'del temp' doesn't seem to work. Is there any interface in Python or other operations to make it possible?

3 years

Question regarding SPOT's accepting_run behaviour

by Clément TAMINES

Hello, I am contacting this list because I have a question regarding the behaviour of SPOT’s accepting_run function. I created an example (see attached) where, if I am not mistaken, the accepting run that is yielded does not satisfy the acceptance formula. Could you confirm that this is a problem and not a mistake in my understanding of the function and/or acceptance formula ? In addition, the acceptance formula is somehow detected as being a gen. Streett condition, can this be prevented and does it have an influence on how the emptiness check/accepting run generation is handled ? Thank you for your help, Clément

3 years

ltlsynt and hoa input

by Ayrat Khalimov

hello, Is there a way to feed HOA file (as a nondet Buchi) instead of a formula to ltlsynt? I tried smth (see below), but I am getting 'unrealisable' for nondet Buchi automaton spec that is supposed to be realisable (see attached). Maybe I missing something? (like ltlsynt dualising the automaton, etc.) Here is what I tried. Into file synthesis.cc, add: #include "spot/parseaut/public.hh" Then in line 822, comment out: // auto aut = trans.run(f); and instead add: spot::bdd_dict_ptr dict = spot::make_bdd_dict(); auto parsed_aut = parse_aut("/tmp/spec.hoa", dict); if (parsed_aut->aborted) abort(); auto aut = parsed_aut->aut; This forces ltlsynt to read file "/tmp/spec.hoa" and ignore the formula. Further, when calling ltlsynt, pass the argument --decompose=no ('just in case'): ./ltlsynt --formula="GF a" --ins=x,y --dot --outs=a,b,c --decompose=no and provide the correct --ins and --outs arguments, and any formula with one of those propositions. The tool outputs expected implementations on toy examples, but on a larger example attached it outputs "unrealizable" instead of "realizable". That is why the question. best wishes, Ayrat

3 years, 1 month

Spot Debian package not working due to expired certificate error for the LRDE website

by Young, David Clark

Hi, I am trying to install Spot using the Debian package at www.lrde.epita.fr/repo/debian/ but it looks as though the security certificate for www.lrde.epita.fr has expired. In fact, it looks like it expired yesterday (Dec. 29th). The reason I'm installing Spot is that it's a dependency of another project I would like to install, and that project's Dockerfile uses the Debian package. It is possible to compile Spot from the source, but it is more efficient to use a Debian package (and potentially eases reproducibility, which is nice when using Docker). Would it be possible for someone to update the certificate? Thanks! - David

3 years, 1 month

SPOT: formula:is_literal shall be marked const?

by Ayrat Khalimov

hi Alexandre, Seems like the function formula::is_literal() should be marked const: /// \brief Whether the formula is an atomic proposition or its /// negation. bool is_literal() { return (is(op::ap) || // If f is in nenoform, Not can only occur in front of // an atomic proposition. So this way we do not have // to check the type of the child. (is(op::Not) && is_boolean() && is_in_nenoform())); } kind wishes, Ayrat

3 years, 2 months

[BUG] Tests fail to build on FreeBSD: error: use of undeclared identifier 'sched_getcpu'

by Yuri

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

3 years, 2 months

Re: [Spot] Assistance with Spot

by Alexandre Duret-Lutz

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.

3 years, 2 months

← Newer
1
2
3
4
5
6
7
8
...
21
Older →

Jump to page:

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Spot