Investigating the non-terminating test cases

[jvoigtlaender]

@nimec01, can you figure out via experimentation what are specific values of LegalCNFConfig that cause the non-termination here? https://github.com/fmidue/logic-tasks/blob/6bfca636af83c1fb22fe0dc4ee9a44bcd5aedb17/test/LegalCNFSpec.hs#L131-L139

Once we see some collection of culpable settings there, we can probably revise checkLegalCNFConfig so that this non-termination never happens.

(Or is it that the generator validBoundsLegalCNF itself sometimes fails to terminate somehow?)

[nimec01]

The validBoundsLegalCNF generator works (there are some test cases for it, that do not fail).

Here are a few instances of LegalCNFConfig that lead to problems during generateLegalCNFInst:

LegalCNFConfig {
  cnfConfig = CnfConfig {
    baseConf = BaseConfig {
      minClauseLength = 16,
      maxClauseLength = 16,
      usedLiterals = "BCDEFGHIJLMNPQTVY"
    },
    minClauseAmount = 49,
    maxClauseAmount = 49
  },
  formulas = 1,
  externalGenFormulas = 1,
  illegals = 0,
  includeFormWithJustOneClause = False,
  includeFormWithJustOneLiteralPerClause = False,
  maxStringSize = 4949,
  minStringSize = 3724,
  allowArrowOperators = False,
  extraText = Nothing
}

LegalCNFConfig {
  cnfConfig = CnfConfig {
    baseConf = BaseConfig {
      minClauseLength = 16,
      maxClauseLength = 16,
      usedLiterals = "ACHIJKLOQRTUVWXZ"
    },
    minClauseAmount = 18,
    maxClauseAmount = 18
  },
  formulas = 1,
  externalGenFormulas = 0,
  illegals = 0,
  includeFormWithJustOneClause = False,
  includeFormWithJustOneLiteralPerClause = False,
  maxStringSize = 1818,
  minStringSize = 1368,
  allowArrowOperators = True,
  extraText = Nothing
}

LegalCNFConfig {
  cnfConfig = CnfConfig {
    baseConf = BaseConfig {
      minClauseLength = 18,
      maxClauseLength = 18,
      usedLiterals = "ADEGHIKLMNOPQRSTVZ"
    },
    minClauseAmount = 38,
    maxClauseAmount = 38
  },
  formulas = 1,
  externalGenFormulas = 0,
  illegals = 0,
  includeFormWithJustOneClause = False,
  includeFormWithJustOneLiteralPerClause = False,
  maxStringSize = 4294,
  minStringSize = 3268,
  allowArrowOperators = True,
  extraText = Nothing
}

LegalCNFConfig {
  cnfConfig = CnfConfig {
    baseConf = BaseConfig {
      minClauseLength = 14,
      maxClauseLength = 14,
      usedLiterals = "DEGHIJLMQRUWYZ"
    },
    minClauseAmount = 46,
    maxClauseAmount = 46
  },
  formulas = 1,
  externalGenFormulas = 0,
  illegals = 1,
  includeFormWithJustOneClause = False,
  includeFormWithJustOneLiteralPerClause = False,
  maxStringSize = 4094,
  minStringSize = 3036,
  allowArrowOperators = False,
  extraText = Nothing
}

LegalCNFConfig {
  cnfConfig = CnfConfig {
    baseConf = BaseConfig {
      minClauseLength = 14,
      maxClauseLength = 14,
      usedLiterals = "ACDFHIJKQRSVWXY"
    },
    minClauseAmount = 24,
    maxClauseAmount = 24
  },
  formulas = 1,
  externalGenFormulas = 0,
  illegals = 1,
  includeFormWithJustOneClause = False,
  includeFormWithJustOneLiteralPerClause = False,
  maxStringSize = 2136,
  minStringSize = 1584,
  allowArrowOperators = False,
  extraText = Nothing
}

I have not tried to figure out what exactly causes the problem with these instances yet. I will do so later. If you wish to find more instances with the same behaviour, you can go ahead and check out this branch. There you can go ahead and run

stack repl
ghci> loop

The loop function will eventually get stuck. The last print in the console then shows the config that is being used.

[nimec01]

I have done some more investigation and found out that (probably) the generated treeList (especially turning it into a String) seems to be the problem. Neither show nor simplestDisplay seem to work on the problematic instances.

[jvoigtlaender]

Hmm, the Show function being used on SynTrees is the standard derived one: https://github.com/fmidue/logic-tasks/blob/57981621e477ee5400bc19821e634149d5547b12/src/Trees/Types.hs#L37-L41 I don't see any chance how this show could be non-terminating on a finite tree.

So, it must be that some tree being fed to it is infinite or, probably more likely, the computation of said tree gets stuck in an infinite loop without producing further output constructore.

I would suggest that you try to get your hands on one such tree, but of course you won't be able to look at it by printing it out ...

[jvoigtlaender]

My immediate next hunch now would be that one of the suchThats in the code is the culprit, since suchThat is really "dumb" in that it cannot notice if it is asked to find something impossible. It will simply try forever.

It could be one of the suchThats in https://github.com/fmidue/logic-tasks/blob/57981621e477ee5400bc19821e634149d5547b12/src/Trees/Generate.hs#L24-L42 itself, but it is somewhat unlikely, since that generator is also used in other task types.

So, which other suchThats in the code are in play when the offending test case is run?

One possibility to find that out would be to follow the code "by hand".

Another would be to use stack test --coverage; stack hpc report --all --open while also passing some additional option to the first stack call that makes it so that only the sometimes endless-looping test is run. You probably must try to get a test run that happens to actually finish without hitting the problematic infiniteness. But then you can go through the generated report and find all the suchThats in the code that were executed.

Then, you can experiment with one after another replacing each suchThat by a trivial condition (thus making it terminate more often). Once you have thus turned the "offending" suchThat "off", you won't anymore get nontermination, no matter how often you repeat the tests.

Then, we would know where the offending suchThat (if indeed that is where the problem sits) is, and can try to analyze further why and in which situations it makes an impossible demand.

[nimec01]

I found the culprit: it actually was validBoundsLegalCNF. It turned out that minStringSize was the problem there. The demanded value was simply too high. Changing its calculation to (minClauseLength + 1) * (minClauseAmount - 1) (in validBoundsLegalCNF) does the job. Then we just need to also update checkLegalCNFConfig in order to accept this config.

I will go ahead and open a pull request for this.

[jvoigtlaender]

Being worked on there.