Hello,
My name is Phillip and I tried to use Spot tool to "play" with LTL formulas.
My question is, is it possible to get boolean result if LTL formula accepts or rejects a word? e.g. In case the LTL formula is "aUb" is it possible to check that the formula is accepting "cycle(b)"?
Best regards,
Phillip
Hi Philipp,
On Sun, Nov 8, 2020 at 9:36 AM Philipp schwartz pschwartz090@gmail.com wrote:
My question is, is it possible to get boolean result if LTL formula accepts or rejects a word? e.g. In case the LTL formula is "aUb" is it possible to check that the 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
Thank you very much,
In addition, when trying to translate a "concatenation" I get error message: "unexpected atomic proposition"
E.g. spot.formula("p2;p1&!p2").translate()
Best regards, Phillipp
On Sun, Nov 8, 2020, 11:59 Alexandre Duret-Lutz adl@lrde.epita.fr wrote:
Hi Philipp,
On Sun, Nov 8, 2020 at 9:36 AM Philipp schwartz pschwartz090@gmail.com wrote:
My question is, is it possible to get boolean result if LTL formula
accepts or rejects a word?
e.g. In case the LTL formula is "aUb" is it possible to check that the
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 pschwartz090@gmail.com wrote:
In addition, when trying to translate a "concatenation" I get error message: "unexpected atomic proposition"
E.g. spot.formula("p2;p1&!p2").translate()
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).
Thank you again for the detailed explanation.
When adding edges using "aut.new_edge" as in this example https://spot.lrde.epita.fr/tut22.html how can I transfer a string to bdd for the third parameter? e.g. in case the action is "p1Up2&p2" and I want to add it as edge
aut.new_edge(1, 2, "p1Up2&p2".to_bdd())
Best Regards,
Phillipp
On Mon, 9 Nov 2020 at 10:05, Alexandre Duret-Lutz adl@lrde.epita.fr wrote:
On Sun, Nov 8, 2020 at 10:20 PM Philip Schwartz pschwartz090@gmail.com wrote:
In addition, when trying to translate a "concatenation" I get error message: "unexpected atomic proposition"
E.g. spot.formula("p2;p1&!p2").translate()
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 pschwartz090@gmail.com wrote:
When adding edges using "aut.new_edge" as in this example https://spot.lrde.epita.fr/tut22.html how can I transfer a string to bdd for the third parameter? e.g. in case the action is "p1Up2&p2" and I want to add it as edge
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.)
Hello, Thank you for your answer, I still didn't understand, in case the action is "p1Up2&p2". How can I pass this as parameter to new edge function?
Regards Phillipp
On Tue, 10 Nov 2020 at 23:42, Alexandre Duret-Lutz adl@lrde.epita.fr wrote:
On Tue, Nov 10, 2020 at 9:28 PM Philip Schwartz pschwartz090@gmail.com wrote:
When adding edges using "aut.new_edge" as in this example https://spot.lrde.epita.fr/tut22.html how can I transfer a string to bdd for the third parameter? e.g. in case the action is "p1Up2&p2" and I want to add it as edge
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
Hello again,
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 ! ).
Regards, Phillipp
On Tue, Nov 10, 2020, 23:49 Philip Schwartz pschwartz090@gmail.com wrote:
Hello, Thank you for your answer, I still didn't understand, in case the action is "p1Up2&p2". How can I pass this as parameter to new edge function?
Regards Phillipp
On Tue, 10 Nov 2020 at 23:42, Alexandre Duret-Lutz adl@lrde.epita.fr wrote:
On Tue, Nov 10, 2020 at 9:28 PM Philip Schwartz pschwartz090@gmail.com
wrote:
When adding edges using "aut.new_edge" as in this example https://spot.lrde.epita.fr/tut22.html how can I transfer a string to bdd for the third parameter? e.g. in case the action is "p1Up2&p2" and I want to add it as edge
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
On Wed, Nov 11, 2020 at 2:38 PM Philip Schwartz pschwartz090@gmail.com wrote:
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 ! ).
That's making it even more confusing.
Spot only supports automa labelled by Boolean formulas over atomic propositions.
If you really expect to label an edge by an LTL formula, can you describe the semantic of such an edge ?
Hello Prof. Alexandre Duret-Lutz,
Thank you again for the detailed answers,
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.
Regards, Phillipp
On Wed, 11 Nov 2020 at 21:10, Alexandre Duret-Lutz adl@lrde.epita.fr wrote:
On Wed, Nov 11, 2020 at 2:38 PM Philip Schwartz pschwartz090@gmail.com wrote:
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 ! ).
That's making it even more confusing.
Spot only supports automa labelled by Boolean formulas over atomic propositions.
If you really expect to label an edge by an LTL formula, can you describe the semantic of such an edge ?
-- Alexandre Duret-Lutz
On Thu, Nov 12, 2020 at 9:00 AM Philip Schwartz pschwartz090@gmail.com wrote:
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')
Please check the output difference between typing "(p1 U p2) & p2" and "p1Up2 & p2". p1Up2 is just an arbitrary name that is assumed to be an atomic proposition.
The difference between "aUb", and "a U b" is also discussed in the help text (Help > LTL Infix Syntax > Atomic Propositions) for the online tool,
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.
This page uses two AP named "p1" and "p2". You can name them as you want by changing the argument of register_ap().
-
Alexandre Duret-Lutz -
Philip Schwartz -
Philipp schwartz