Skip to content

Commit 873f641

Browse files
authored
Updated excercise requirements (#834)
Excercise was not considering safety and liveness specifications updates into account. Updated the excercise.
1 parent 7d910aa commit 873f641

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

Docs/docs/tutorial/clientserver.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -194,7 +194,7 @@ p check -tc tcAbstractServer -s 1000
194194
### Exercise Problem
195195

196196
- [Problem 1] Fix the bug in AbstractBankServer state machine and run the P Checker again on the test case to ensure that there are no more bugs in the models.
197-
- [Problem 2] Extend the ClientServer example with support for depositing money into the bank. This would require implementing events `eDepositReq` and `eDepositResp` which are used to interact between the client and server machine. The Client machine should be updated to deposit money into the account when the balance is low and the BankServer machine implementation would have to be updated to support depositing money into the bank account. After implementing the deposit feature, run the test-cases again to check if the system still satisfies the desired specifications.
197+
- [Problem 2] Extend the ClientServer example with support for depositing money into the bank. This would require implementing events `eDepositReq` and `eDepositResp` which are used to interact between the client and server machine. The Client machine should be updated to deposit money into the account when the balance is low, the BankServer machine implementation would have to be updated to support depositing money into the bank account and finally safety and liveness specifications needs to be updated take disposit events into account. After implementing the deposit feature, run the test-cases again to check if the system still satisfies the desired specifications.
198198

199199
!!! success "What did we learn through this example?"
200200
We explored writing P state machines, safety and liveness specifications as P monitors, writing multiple model checking scenarios to check the correctness of a P program, and finally, replacing complex components in P with their abstractions using P's module system.

0 commit comments

Comments
 (0)