Soter derives a finitely representable over-approximation of the execution of the input Erlang module. This abstract model of the program is called an Actor Communicating System (ACS).
An ACS can be read as a "decorated" control-flow graph but in fact it is interpreted by Soter (and BFC) as an infinite-state system, equivalent to a Vector Addition System (VAS) or, equivalently, a Petri net.
An ACS transition rule has the shape
\[\pid : q \xrightarrow{\ell} q'\]
which means that a process of pid class \(\pid\) can transition from state \(q\) to state \(q'\) with (possible) communication side effect \(\ell\), of which there are four kinds, namely,
the process makes an internal transition
it extracts and reads a message \(msg\) from its mailbox
it sends a message \(msg\) to a process of pid class \(\pid'\)
it spawns a process of pid class \(\pid'\).
The various kinds of control states and transitions are represented pictorially as follows.
![[open]](../img/acslegend.svg){kind=link}