应对状态爆炸

抽象掉无关细节、用对称性归约、用符号表示状态集合而非逐个枚举。