Liian hyvää ollakseen totta.

Ensin toisella :

Refine checked 393,216 states
With 2080768 transitions
Allocated a total of 219 pages of size 128K
Compaction produced 0 chunks of 16K.
Took 31(24+0) seconds

Sitten toisella, "-Full":

Begin Header
State_cnt = 393216
Action_cnt = 56
Transition_cnt = 2080768
Initial_states = 1;
End Header

Sitten reduktion kanssa:

Begin Header
State_cnt = 20
Action_cnt = 56
Transition_cnt = 22
Initial_states = 1;
End Header

Vastaus on oikein, tietysti, mutta kyse on tietysti tästä:

This pathological situation is commonly referred to as the ignoring problem. The prevention of this phenomenon is not mandatory if one wants to verify if the system halts but it must be resolved for more elaborate properties like, for example, safety or liveness properties.

Joskus, kun lukee alan papereita, ja joku väittää välttäneensä eksponentiaalisen räjähdyksen, tulee mieleen, että jaaha, tässä on pakko olla kyse huijauksesta. Niinkuin onkin, mutta vain siinä mielessä että kysymykseen saadaan oikea vastaus, koska kysymys on triviaali.