<p>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.</p>

<p>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.<br>
Only after the user selects a beverage, a can is dispensed, and the variable evaluation changes (the effect of $\textit{[sb]get}$).</p>

<p>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.</p>

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

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

<p>but the example given does not do so.</p>

CC BY-SA 3.0
2017-12-06T21:21:39.500Z
2017-12-06T21:21:39.500Z
tjanson
<p>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)</p>
<p><a href="https://i.sstatic.net/hKlT5.jpg" rel="nofollow noreferrer"><img src="https://i.sstatic.net/hKlT5.jpg" alt="enter image description here" /></a></p>
<p>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?</p>
<p>In the book, it states that η is the evaluation, but can somebody please elaborate it me with respect to the below example?</p>
<blockquote>
<p>Example 2.14. Beverage Vending Machine</p>
<p>The graph described in Example 2.12 (page 29) is a program graph. The set of variables is</p>
<p>Var = { nsoda, nbeer }</p>
<p>where both variables have the domain { 0, 1, . . . , max }. The set Loc of locations equals {start, select} with Loc0 = {start}, and</p>
<p>Act = { bget , sget, coin, ret coin, refill }.</p>
<p>The effect of the actions is defined by:</p>
<p>Effect(coin, η) = η</p>
<p>Effect(ret_coin, η) = η</p>
<p>Effect(sget, η) = η[nsoda := nsoda−1]</p>
<p>Effect(bget, η) = η[nbeer := nbeer−1]</p>
<p>Effect(refill, η) = [nsoda := max, nbeer := max]</p>
</blockquote>
<p>Why is the Effect(coin, η) = η and Effect(ret_coin, η) = η?</p>
<p>Thank you very much.</p>

<model-checking>
What is "Effects" in Program Graph?
Rao208
# What is "Effects" in Program Graph?

(Asked by: username_0 on 2017-11-08)

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)

[![enter image description here](https://i.sstatic.net/hKlT5.jpg)](https://i.sstatic.net/hKlT5.jpg)

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.

**Tags:** model-checking


---

## 1 answers

### Answer by username_1 on 2017-12-06. Score: 1

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.


---

