Closed nimec01 closed 4 months ago
There also seems to be problems with generateLegalPropositionInst
.
Might be a good option to revert #111 as I'm revealing more and more problems. But I'm still confused how these problems did not show up on my machine until now.
I wouldn't be so pessimistic. Let's look at one problem after the other (though from my side that will mean next week).
I guess a lot of the things were simply not really exhaustively tested before, since the "config generators" were a bit naive/narrow and thus not really exploring the full space of what could be input to the task generators. I find it valuable to find these problems now.
The new https://github.com/fmidue/logic-tasks/blob/1cfc4bdd43b7eeccaae4403ae8af6d0b544f82e5/test/SynTreeSpec.hs#L44 looks good to me.
The "new" problems are maybe not really about generateLegalPropositionInst
per se. At least, the latest commit on master (f13357fb43759650bacc9d81bc7553527d9724a9) seems to have led to a timeout somewhere in: https://github.com/fmidue/logic-tasks/blob/f13357fb43759650bacc9d81bc7553527d9724a9/test/LegalPropositionSpec.hs#L43-L72
So, it might well be that validBoundsSynTree
itself is looping in some freak corner cases. My suggestion is to first test this generator more extensively. Possibly by amending https://github.com/fmidue/logic-tasks/blob/f13357fb43759650bacc9d81bc7553527d9724a9/test/SynTreeSpec.hs#L62-L64 locally by using modifyMaxSuccess
like this:
it "validBoundsSynTree should generate a valid config" $
modifyMaxSuccess (const 1000) $
forAll validBoundsSynTree $ \synTreeConfig ->
isJust $ runIdentity $ evalLangM (checkSynTreeConfig synTreeConfig :: LangM Maybe)
or similarly.
Using modifyMaxSuccess (const 10000)
did not change anything for me. Tests are still passing for me.
I was able to grab some SynTreeConfigs that led into non-termination (at "at least creates actual formula symbols"):
SynTreeConfig {
minNodes = 4,
maxNodes = 6,
minDepth = 3,
maxDepth = 4,
usedLiterals = "BDHIKMOQSWXZ",
atLeastOccurring = 2,
allowArrowOperators = True,
maxConsecutiveNegations = 1,
minUniqueBinOperators = 2
}
SynTreeConfig {
minNodes = 4,
maxNodes = 10,
minDepth = 3,
maxDepth = 4,
usedLiterals = "AEFJKMORUVWYZ",
atLeastOccurring = 1,
allowArrowOperators = True,
maxConsecutiveNegations = 1,
minUniqueBinOperators = 2
}
SynTreeConfig {
minNodes = 4,
maxNodes = 4,
minDepth = 3,
maxDepth = 3,
usedLiterals = "ABCDEFGHIJKLMOQRTUVWYZ",
atLeastOccurring = 2,
allowArrowOperators = True,
maxConsecutiveNegations = 2,
minUniqueBinOperators = 2
}
And some LegalPropositionConfigs:
LegalPropositionConfig {
syntaxTreeConfig = SynTreeConfig {
minNodes = 4,
maxNodes = 9,
minDepth = 3,
maxDepth = 6,
usedLiterals = "FHJKLNOPSUXZ",
atLeastOccurring = 1,
allowArrowOperators = False,
maxConsecutiveNegations = 2,
minUniqueBinOperators = 2},
formulas = 9,
illegals = 4,
bracketFormulas = 5,
extraText = Nothing,
printSolution = False
}
LegalPropositionConfig {
syntaxTreeConfig = SynTreeConfig {
minNodes = 4,
maxNodes = 23,
minDepth = 3,
maxDepth = 7,
usedLiterals = "BCEGIKMNOPQRTUWXY",
atLeastOccurring = 2,
allowArrowOperators = False,
maxConsecutiveNegations = 1,
minUniqueBinOperators = 2},
formulas = 14,
illegals = 12,
bracketFormulas = 0,
extraText = Nothing,
printSolution = False
}
LegalPropositionConfig {
syntaxTreeConfig = SynTreeConfig {
minNodes = 4,
maxNodes = 24,
minDepth = 3,
maxDepth = 5,
usedLiterals = "ABCEFHJMTUVYZ",
atLeastOccurring = 1,
allowArrowOperators = False,
maxConsecutiveNegations = 2,
minUniqueBinOperators = 2},
formulas = 10,
illegals = 6,
bracketFormulas = 0,
extraText = Nothing,
printSolution = False}
LegalPropositionConfig {
syntaxTreeConfig = SynTreeConfig {
minNodes = 4,
maxNodes = 6,
minDepth = 3,
maxDepth = 4,
usedLiterals = "CGHJNOPQRTVWYZ",
atLeastOccurring = 1,
allowArrowOperators = False,
maxConsecutiveNegations = 1,
minUniqueBinOperators = 2},
formulas = 4,
illegals = 2,
bracketFormulas = 0,
extraText = Nothing,
printSolution = False
}
LegalPropositionConfig {
syntaxTreeConfig = SynTreeConfig {
minNodes = 6,
maxNodes = 6,
minDepth = 3,
maxDepth = 3,
usedLiterals = "ABCHIJKLMNRUY",
atLeastOccurring = 1,
allowArrowOperators = False,
maxConsecutiveNegations = 1,
minUniqueBinOperators = 2},
formulas = 7,
illegals = 1,
bracketFormulas = 5,
extraText = Nothing,
printSolution = False
}
LegalPropositionConfig {
syntaxTreeConfig = SynTreeConfig {
minNodes = 4,
maxNodes = 13,
minDepth = 3,
maxDepth = 8,
usedLiterals = "BDGJKMOQRSTWZ",
atLeastOccurring = 1,
allowArrowOperators = True,
maxConsecutiveNegations = 1,
minUniqueBinOperators = 2},
formulas = 1,
illegals = 1,
bracketFormulas = 0,
extraText = Nothing,
printSolution = False}
For the three SynTreeConfig
s you give above, does genSynTree
fail to terminate (sometimes)?
For the three
SynTreeConfig
s you give above, doesgenSynTree
fail to terminate (sometimes)?
I think so. At least display synTree
does not terminate.
Can you check whether the following code produces output?
let nodes = 4 -- then test with 5, and with 6
in syntaxShape nodes 4 True True
`suchThat` \synTree ->
checkAtLeastOccurring synTree &&
checkMinUniqueOps synTree &&
consecutiveNegations synTree <= 1)
where checkAtLeastOccurring synTree = fromIntegral (length (collectLeaves synTree)) >= 2
checkMinUniqueOps synTree = numOfUniqueBinOpsInSynTree synTree >= 2
Oh, I guess I see that it won't produce output for nodes = 4
, because there is no tree with just 4
nodes but at least 2
binary operators.
So, another check is needed to prevent such a configuration in the first place.
A partial fix (helping with the first of the configs you reported) should be to move
https://github.com/fmidue/logic-tasks/blob/f13357fb43759650bacc9d81bc7553527d9724a9/src/Trees/Generate.hs#L54C15-L54C43
to the "next outer suchThat
level".
That should definitely be done.
But it won't help with the case
SynTreeConfig {
minNodes = 4,
maxNodes = 4,
minDepth = 3,
maxDepth = 3,
usedLiterals = "ABCDEFGHIJKLMOQRTUVWYZ",
atLeastOccurring = 2,
allowArrowOperators = True,
maxConsecutiveNegations = 2,
minUniqueBinOperators = 2
}
because there the nodes
will always end up being 4
, even with "retrying".
To address the latter, I think an additional config check is needed that makes sure maxNodes
is large enough to really admit minUniqueBinOperators
binary nodes.
The only case yet unaccounted for by my above explanation would be this one from above:
SynTreeConfig {
minNodes = 6,
maxNodes = 6,
minDepth = 3,
maxDepth = 3,
usedLiterals = "ABCHIJKLMNRUY",
atLeastOccurring = 1,
allowArrowOperators = False,
maxConsecutiveNegations = 1,
minUniqueBinOperators = 2}
In that case, the problem could be the formulas = 7
setting in the "surrounding" LegalPropositionConfig
being too big to satisfy this: https://github.com/fmidue/logic-tasks/blob/f13357fb43759650bacc9d81bc7553527d9724a9/src/Tasks/LegalProposition/Quiz.hs#L25-L38
That is, there possibly aren't 7 "different enough" trees with exactly 6
nodes and depth 3
.
Again, identifying this cause should allow to strengthen the config checker to weed out such cases.
About this:
To address the latter, I think an additional config check is needed that makes sure
maxNodes
is large enough to really admitminUniqueBinOperators
binary nodes.
I now think the relevant check should actually prevent minNodes <= 2 * minUniqueBinOperators
.
And the "moving out" of checkMinUniqueOps synTree
to the outer suchThat
level is then probably not even needed.
That is, there possibly aren't 7 "different enough" trees with exactly
6
nodes and depth3
.Again, identifying this cause should allow to strengthen the config checker to weed out such cases.
How does it determine whether two SynTree
s are similar? Or more specifically: How can I interpret the following code?
similarTree :: Eq o => SynTree o c -> SynTree o c -> Bool
similarTree t1 t2 = void t1 == void t2
What would be a fitting guard for the config?
How can I interpret the following code?
That code takes t1 :: SynTree o c
and t2 :: SynTree o c
, turns both into a SynTree o ()
each, by replacing each leaf label by ()
, then compares the resulting structures.
So what it is really doing is compare whether the two trees have exactly the same "shape" (also taking into account which operators are labelled at the inner nodes).
With
SynTreeConfig {
minNodes = 6,
maxNodes = 6,
minDepth = 3,
maxDepth = 3,
usedLiterals = "ABCHIJKLMNRUY",
atLeastOccurring = 1,
allowArrowOperators = False,
maxConsecutiveNegations = 1,
minUniqueBinOperators = 2}
there are only four possible shapes in that sense:
And (Or () ()) (Not ())
And (Not ()) (Or () ())
Or (And () ()) (Not ())
Or (Not ()) (And () ())
Hence, formulas = 7
is too much.
A very rough sketch might be: ensure that (if allowArrowOperators then 4 else 2) ^ ((maxNodes - 1) `div` 2 - minUniqueBinOperators + 1) >= formulas
holds.
It is quite pessimistic, but in practice it will probably be fulfilled in all relevant cases. (For example, it rejects the above case but accepts when maxNodes
is increased from 6
to 9
.)
Most of the mentioned changes should be implemented now. There is a problem with SuperfluousBrackets which I'm investigating now.
SuperfluousBracketsSpec had some test cases being stuck sometimes. I would guess that this is happening due to the combination of
`suchThat` sameAssociativeOperatorAdjacent
used in generateSuperfluousBracketsInst
and a low maxNodes
/ maxDepth
setting.
There might be a better way, but I changed it to only use configs with at least 8 nodes.
Such repairs by letting certain counts have a minimal value (in the config generators in the test suite) should then probably also make their way into the config checkers (on lecturer-provided configs).
After all, it doesn't really make sense to systematically test fewer cases than may appear in actual usage. Or, put differently, the validity checkers (being used and tested) should be as strong as what constraints are added to the test case generators for making tests go through. Otherwise, we are deliberately saying "let's not test this case, because the test sometimes fails, but let's still allow the lecturer to make a configuration with this known-to-be-causing-failures characteristics". At least if the additional constraint is not too far-fetched for teaching use cases.
The current implementation of
validBoundsSynTree
can still generate invalidSynTreeConfig
s. The test cases did not reveal that at my end. I fixed this now.