Hi Philipp, On Sun, Nov 8, 2020 at 9:36 AM Philipp schwartz <pschwartz090(a)gmail.com> wrote: accepts or rejects a word? formula is accepting "cycle(b)"? % ltlfilt -f 'a U b' --accept-word 'cycle{b}' -c 1 % ltlfilt -f 'a U b' --accept-word 'cycle{!b}' -c 0 Beware that since AP={a,b} are atomic propositions, cycle{b} is not a word, but the set of words where b is always true. The --accept-word option matches any formula that *intersect* the given set, so it just has to accept one word. (The --reject-word match formulas that do not intersect the given set, so they have to reject all words.) As a consequence, the following should not be a surprise: % ltlfilt -f 'a U b' --accept-word 'cycle{!a}' -c 1 This is because the word cycle{!a & b} which is one of the words represented by cycle{!a} is accepted by 'a U b'. Best regards -- Alexandre Duret-Lutz

On Sun, Nov 8, 2020 at 10:20 PM Philip Schwartz &lt;pschwartz090(a)gmail.com&gt; wrote: Concatenation is only valid in Semi-Extended Regular Expressions (SERE), and those recognize finite words. As Spot deals with LTL or PSL formulas over infinite words, you need to select how to interpret your SERE over finite words by including it into one of {...} or {...}! In your simple example there is no difference between "{p2;p1&!p2}" or "{p2;p1&!p2}!", they are both equivalent to the LTL formula "p2 & X(p1 & !p2)". See https://spot.lrde.epita.fr/tl.pdf section 2.6 for the specification of {r} and {r}! (the latter being syntactic sugar for {r}<>->1). -- Alexandre Duret-Lutz

On Tue, Nov 10, 2020 at 9:28 PM Philip Schwartz &lt;pschwartz090(a)gmail.com&gt; wrote: There is no support for "actions", "events", or arbitrary "letters" in Spot's automata. The only kind of "letters" we support are assignments of a set of predeclared atomic propositions. If you have a set of predefined actions like "eat", "walk", "sleep", you could use some atomic propositions to binary encode them. For instance: "eat" = !p0 & !p1 "walk" = !p0 & p1 "sleep" = p0 & !p1 Then work with that. Spot will only want to hear about those p0, p1 propositions, so the mapping (and naming of the propositions) is up to you. An alternative encoding, that is more expensive in number of atomic propositions, but easier to work with for us humans is "eat" = eat & !walk & !sleep "walk" = !eat & walk & !sleep "sleep" = !eat & !walk & sleep (See also http://lists.lrde.epita.fr/pipermail/spot/2020q3/000293.html for an answer to a related question.) -- Alexandre Duret-Lutz

I read my previous email and I thought maybe I was not clear enough: My problem is transferring the "until" operator to an action recognized by spot (such as ! ).

My point is that I want to copy the behavior of the tool presented in the attached picture (just typed p1Up2&p2 here - https://spot.lrde.epita.fr/app/ and got automata with 2 states and the label of the edge form "1" to "0" is 'p1Up2&p2')

I'm trying to do the same using "Creating an automaton by adding states and transitions" as described in this guideline - https://spot.lrde.epita.fr/tut22.html.