# What is “Effects” in Program Graph?

I have a doubt regarding the "effects" 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 "η" 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.