-
Add the following data constraint which expresses that when the return of money is requested, the delivered amount cannot be negative:
data constraints variables int val returnReg command ReturnMoney;reply(val) where val >= 0
-
Run the monitoring and inspect the results.