Für Programm-Spezifikation (und -Verifikation) muß der Zustand sowieso benannt werden,
und verschiedene Zustände brauchen verschiedene Namen (wenigstens: vorher/nachher)
also kann man sie gleich durch verschiedene Objekte repräsentieren.