BUG: Trouble with universal (forall) constraints

[andreas-zeller]

If I enter

$ fandango fuzz -f persons.fan -n 10 -c 'forall <lowercase_letter> in <first_name>: <lowercase_letter> == "a"'

I get a population of zero – Fandango cannot solve this.

The equivalent

$ fandango fuzz -f persons.fan -n 10 -c '<first_name>..<lowercase_letter> == "a"'

works, though.

[joszamama]

Hi Andreas!

This is a problem I really wanted to cover for a while. Let's take a look at your example:

forall <lowercase_letter> in <first_name>: <lowercase_letter> == "a"

The first nonterminal in the forall is a "tag" representation of the second nonterminal. In this case, <lowercase_letter> is not referring to a <lowercase_letter> child of <first_name>, but to <first_name> itself. So when you write <lowercase_letter> == "a", what you are really saying is that <first_name> == "a", and this cannot be parsed with the grammar persons.fan (<first_name> ::= <uppercase_letter><lowercase_letter>+;). That's why Fandango cannot find a solution.

The 'equivalent' way that you express in this issue, is not equivalent, since that is pointing to the actual children of <first_name>. The equivalent forall representation would be:

forall <foo> in <first_name>.<name>.<lowercase_letter>: <foo> == "a"

Now, I know what you are thinking, and yes, I do agree with you. I think the current way to represent foralls in Fandango is not intuitive, since, assuming a novice user perspective, I would expect that the first nonterminal of the forall refers to a child (direct/indirect) of the second nonterminal, as forall <child> in <parent>: ....

I will check this issue with Marius and come back to this issue.

[joszamama]

There also are all() and exists() functions in Python; maybe we can build on these? -- Andreas

[andreas-zeller]

With #175 done, we'll get rid of quantification keywords anyway