# The Abstract Model

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.

# How to read the diagrams

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,

1. the process makes an internal transition

2. it extracts and reads a message $$msg$$ from its mailbox

3. it sends a message $$msg$$ to a process of pid class $$\pid'$$

4. it spawns a process of pid class $$\pid'$$.

The various kinds of control states and transitions are represented pictorially as follows.

Explanation of elements of an ACS diagram [open]