0
$\begingroup$

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

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.

$\endgroup$
1
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.