l'algoritmo solutore e' un algoritmo di labelling che simula a tempo discreto la diffusione di due gas di cui l'uno (fantasmi) sovrascrive l'altro (pacman).
Resta da individuare un corretto criterio di arresto a questa simulazione.(Ad esempio, il criterio "finche' il pacman vive" darebbe non-terminazione su quelle istanze in cui il pacman si trova in una componente connessa senza fantasmini ne' pillolazzi).
Riesci ad individuare un corretto e conveniente criterio di terminazione?
Riesci a convincerti della sua correttezza sempre ragionando per rimappature del problema in analogia a quanto esemplificato?
(Quando i dettagli ultimi si dipanano in analogia ai passi importanti abbiamo conferma di essere entrati nella musica e nel ritmo del problema).