实验一 Modeling and analysis using Uppaal

Question1:

Use the verifier to check the properties. Try to improve the model until both properties are true. For the first property you have to change the bank. For the second property you have to change Eric. (What should Eric do if the ATM does not pay out cash but does return his bank card?) Uppaal tip: under the menu Options:Diagnostic Trace select the option Shortest to let the verifier generates a counterexample in the simulator.

1)性质1满足

2)性质2满足

通过增加信号not_cash实现性质2的满足

Question2:

Change the ATMso that initially it only has 30 euro in the till instead of 200.

There is still something in the model of the ATM that is not realistic: with this lower amount of money in the till something can happen in the model which would be impossible in reality. Try to figure out what this is. You can do that by simulating the model for a while, or by letting Uppaal do a random simulation. (Hint: Eric wants to do some shopping and needs a lot of cash.)

Change the model of the ATM to improve this.

Once you have done this, add a query to the verifier to check that the problem has been avoided. The query should express the obvious reality check for the ATM. Of course, the adapted model still should not deadlock!

答：修改模型中ATM中的钱为30，银行账户余额为80.

• 模型中会出现ATM机中的钱为负数；

改变后的ATM模型：

改变后的银行模型：

通过在银行发来OK信号时判断ATM机余额是否足够来改善此情况，同时atm余额足够时发信号给银行可以更新银行中的账户余额。

改变后2条性质任然满足，如下图。