Question: Semantics

[nmanginas]

Hi many thanks for the tool.
I am trying to convert the formula (WX(a) <-> b) for which the automaton is this:

Shouldn't the string "~b", i.e. not b be accepted here? Am I missing something?

Thanks

[francescofuggitti]

Hi @nmanginas,

thanks for reaching out! Yes, you're right. The string "~b" should be accepted. This is a bug (a nice viz is here). Now, I don't have much time to look into it, but I'll try to do so asap.

Thank you!

[nickmagginas]

I am not sure this is wrong after all:
The formula WX(a) <-> b is equivelant to (WX(a) & b) | !(WX a) & ~b) which in NNF would correspond to
(WX(a) & b) | (X ~a) & ~b) per the rules in slide 32 here. In that case, I am thinking about this bottom up instead of top down as the compilation done here, it does make sense. Which begs the question what is the formula used to encode the desired behavior which is (WX a & b) | (WX ~a) & ~b). Which per the rules is not equivalent to WX(a) <-> b. Don't know if this makes sense?

[nickmagginas]

Sorry different account :') I am the same person.

[francescofuggitti]

The transformation to NNF is correct but also in that case the string "~b" should be accepted. See the comparison here

[JaviMuller]

I don't think this is a bug. WX(a) is satisfied if there are no more transitions (we have reached the end of the input), or if the next state satisfies a. In the case of the input {~b}, we have that WX(a) is satisfied, as after reading ~b, we have no more input. However, WX(a) is satisfied, in order for the current state to be accepting, b also needs to be satisfied, which is not the case.