What is "Effects" in Program Graph? I have a doubt regarding the &quot;effects&quot; in Program Graph. Below is the image from the book Principle of Model Checking from Christel Baier and Joost-Pieter Katoen
(The MIT Press Cambridge, Massachusetts London, England)

I know what interleaving means and also I know what Effects are. As per my knowledge, effects are nothing but the result of the action on your variable (correct me if I am wrong). What does the Greek letter &quot;η&quot; mean?
In the book, it states that η is the evaluation, but can somebody please elaborate it me with respect to the below example?

Example 2.14. Beverage Vending Machine
The graph described in Example 2.12 (page 29) is a program graph. The set of variables is
Var = { nsoda, nbeer }
where both variables have the domain { 0, 1, . . . , max }. The set Loc of locations equals {start, select} with Loc0 = {start}, and
Act = { bget , sget, coin, ret coin, refill }.
The effect of the actions is defined by:
Effect(coin, η) = η
Effect(ret_coin, η) = η
Effect(sget, η) = η[nsoda := nsoda−1]
Effect(bget, η) = η[nbeer := nbeer−1]
Effect(refill, η) = [nsoda := max, nbeer := max]

Why is the Effect(coin, η) = η and Effect(ret_coin, η) = η?
Thank you very much.
What you wrote is correct. The actions $\textit{coin}$ and $\textit{ret_coin}$ do not change the values of the variables $\textit{Var} = \{\textit{nsoda}, \textit{nbeer}\}$, i.e., the number of soda and beer cans in the machine.

Inserting a coin is only possible in the $\textit{start}$ location, and with this action the location changes to $\textit{select}$. If you’re wondering how the machine keeps track of payment at all, this is it: By the PG's two locations.
Only after the user selects a beverage, a can is dispensed, and the variable evaluation changes (the effect of $\textit{[sb]get}$).

Similarly, returning the coins (which can only happen in the case the vending machine has neither beer nor soda cans) does not change the number of cans.

You could propose a different model that does track the exact amount of coins inserted as a variable, and define


$\textit{Effect}(\textit{coin},η) = η[\textit{coins_inserted} := \textit{coins_inserted} + 1]$ as well as
$\textit{Effect}(\textit{ret_coin},η) = η[\textit{coins_inserted} := 0]$


but the example given does not do so.