New handling of conjunction branch depth
The handling of conjunctions in the current game structure allows for situations where the game does not offer the simplest HML formula in certain situations.
One instance is comparing the processes, where the failure trace <a>(¬<a> ∧ <b>¬<b>) is not found:
a.b.0
a.0 + a.b.b.0 + a.(a.0+b.0)The problem is discussed in more detail in review_special_01_v3.pdf. The review suggests to extend the game by conjunction moves where the defender choses a set from a partitioning of the original states that can be offereded by the defender. (The current mechanics would be a special case of this with the attacker always offering the partition {{q} | q:Q}.)
The issue is about first implementing the suggested new game mechanics and preparing the ground to also explore other fixes.