Testen mit zufälligen Konfigurationen bei Prolog

[nimec01]

Bezieht sich auf #264.

Die Tests für Prolog wurden so weit für das Testen mit zufälligen Konfigurationen angepasst. Allerdings ist die aktuelle Implementierung von verifyQuiz für PrologConfig anscheinen nicht ausreichend.

Dies führt dazu, dass die generierten Konfigurationen als gültig abgestempelt werden, obwohl die Generation von Aufgabeninstanzen damit nicht zwingend möglich ist.

Das ganze lässt sich wahrscheinlich auch auf die Nutzung von tryGen zurückführen.

Demnach müsste #106 zuerst umgesetzt werden, bevor hier weitere Anpassungen getroffen werden können.

[jvoigtlaender]

#106 ist jetzt gelöst (wobei der entsprechende Commit 24f946a allerdings zumindest nicht offensichtlich den Prolog-Code berührt)

[patritzenfeld]

Ich habe beim Löschen von tryGen zunächst auch die Testfälle angepasst, das dann aber nicht mit gepusht, da es hier auch schon Änderungen daran gab. Dabei ist mir folgendes aufgefallen, wodurch das bestehende Problem ausgelöst wird:

1. Kann man ClauseShape HornClause Fact auswählen, aber gleichzeitig die minClauseLength auf > 1 stellen, wodurch niemals ein Fakt generiert werden kann.
2. Kann man ClauseShape HornClause Procedure auswählen, aber gleichzeitig die maxClauseLength auf < 2 stellen, wodurch niemals eine Regel generiert werden kann.

Beides wird nicht in der Config geprüft und führt zu endloser Rekursion in suchThat (oder vorher abbrechen von tryGen)

Das kann aus meinem jetzt verworfenen commit kopiert werden. (den Teil unter der Markierung bitte ignorieren, das war ein Fehler)

[nimec01]

Ich habe beim Löschen von tryGen zunächst auch die Testfälle angepasst, das dann aber nicht mit gepusht, da es hier auch schon Änderungen daran gab. Dabei ist mir folgendes aufgefallen, wodurch das bestehende Problem ausgelöst wird:

1. Kann man ClauseShape HornClause Fact auswählen, aber gleichzeitig die minClauseLength auf > 1 stellen, wodurch niemals ein Fakt generiert werden kann.
2. Kann man ClauseShape HornClause Procedure auswählen, aber gleichzeitig die maxClauseLength auf < 2 stellen, wodurch niemals eine Regel generiert werden kann.

Beides wird nicht in der Config geprüft und führt zu endloser Rekursion in suchThat (oder vorher abbrechen von tryGen)

Das kann aus meinem jetzt verworfenen commit kopiert werden. (den Teil unter der Markierung bitte ignorieren, das war ein Fehler)

Ich habe die von dir angemerkten Checks jetzt in verifyQuiz aufgenommen, allerdings ändert das bei mir nichts.

[patritzenfeld]

Habe nochmal nachgesehen. Bei meinen Tests war usedPredicates immer genauso lang wie maxClauseLength, hier ist das aber zufällig gewürfelt. Vielleicht gibt es da noch einen Zusammenhang, der das Problem auslöst.

[patritzenfeld]

Es wird nicht getestet, ob maxClauseLength > length usedPredicates gilt. Wenn man das tatsächlich so einstellt, entstehen manchmal seltsame Instanzen, die minClauseLength ignorieren.

[patritzenfeld]

Ich habe das Problem gefunden:

Beim Generieren der Klauseln wird aktiv verhindert, dass es mehrere gegensätzliche Literale gibt, wohl damit es eine eindeutige Lösung gibt. Das ist erstmal auch kein Problem, aber kann speziell bei zweimal HornClause Procedure dazu führen, dass keine mögliche Instanz existiert. Denn dann muss es zwingend mehrere resolvierbare Literale geben, um die Struktur einzuhalten.

Das passiert dann, wenn usedPredicates kürzer oder gleich dem Maximum von 2 und minClauseLength ist.