Modelling a basic sequential circuit as a transition system?
How does the transition system (denoted by $\texttt{TS}$) relate to the sequential circuit (denoted by $\texttt{SC}$)?



The states of $\texttt{TS}$ are all possible combinations of values of variable $x$ and register $r$ (no output variable $y$) in $\texttt{SC}$.
The label of each state in $\texttt{TS}$ consists of all the variables (including the register) which are evaluated true given the valuations in $\texttt{SC}$.
For example, $\{x, r, y \}$ for state $(x = 1, r = 1)$ means that all variables are true according to $\lambda_y = \lnot (x \oplus r)$ and $\delta_r = x \lor r$ given $x = 1, r = 1$.
The transitions (arcs with arrow) between states in $\texttt{TS}$ result from the functions $\lambda_y$ and $\delta_r$.
For example, $(x = 0,r = 1) \to (x = 0,r = 1)$ if the next input bit equals 0.




For more details and a general recipe for modeling sequential hardware circuits as transition systems, please refer to the book "Principles of Model Checking" (Section 2.1.2) by Christel Baier and Joost-Pieter Katoen. The MIT Press.