(b2);

(6.north west) ++(-0.1,0.1) node\[name=c1\] (7.south east) ++(0.1,-0.1) node\[name=c2\]; (c1) rectangle (c2);

(8.north west) ++(-0.1,0.1) node\[name=d1\] (9.south east) ++(0.1,-0.1) node\[name=d2\]; (d1) rectangle (d2);

Let us illustrate how EGAS works through a simple example. Let us consider the abstract transition system ${\mathcal{A}}$ in Figure \[figure-1\], where concrete states are numbers which are abstracted by blocks of the state partition $\{[1],[2,3],[4,5],[6],[7],[8,9]\}$. The abstract state space of ${\mathcal{A}}$ is simplified by merging the abstract states $[2,3]$ and $[4,5]$: EGAS guarantees that this can be safely done because $\operatorname{pre}^\sharp ([2,3]) = \{[1]\}=
\operatorname{pre}^\sharp([4,5])$ and $\operatorname{post}^\sharp ([2,3]) = \{[6],[7]\}=
\operatorname{post}^\sharp([4,5])$, where $\operatorname{pre}^\sharp$ and $\operatorname{post}^\sharp$ denote, respectively, the abstract predecessor and successor functions in ${\mathcal{A}}$. This abstraction simplification leads to the abstract system ${\mathcal{A}}'$ in Figure \[figure-1\]. Let us observe that the abstract path $\pi = \langle [1], [2,3,4,5], [7], [8,9]\rangle$ in ${\mathcal{A}}'$ is spurious because there is no concrete path whose abstraction in ${\mathcal{A}}'$ is $\pi$, while $\pi$ is instead the abstraction of the spurious path $\langle [1],$ $[4,5],$ $[7], [8,9]\rangle$ in ${\mathcal{A}}$. On the other hand, consider the path $\sigma = \langle [1], [2,3,4,5], [6], [8,9]\rangle$ in ${\mathcal{A}}'$ and observe that all the paths in ${\mathcal{A}}$ that are abstracted to $\pi'$, i.e.$\langle [1],[2,3],[6],[8,9]\rangle$ and 