News
Chapter 4 Patch
Written on 18.12.2024 10:09 by Andrea Lattuada
Dear Students, there is a small issue in exercise01.rs in the handout I distributed for Chapter 4 (and Chapter 5). For an accurate model of the system, we need to state that the network's sent_msgs Set is finite as a well_formed condition. This will not have prevented you from proving safety and is a weaker network property (so it's not incorrect, just models a network where the messages could be infinite); but the update is still a valid, and more accurate, network model and makes the proof for Chapter 5 simpler.
If you have already submitted, I have applied the patch to your code and re-submitted for you: you can download the updated code from your personal status page. If you have not submitted you have two options:
(a) recommended, especially if you've only done a little bit of work: re-download the handout and copy over your solution within the grading markers,
(b) use the write up at https://cms.sic.saarland/sysverification2425/5/Chapter_4_Patch to apply the change to exercise01.rs (note that you will need to do this carefully, to make sure that your code will pass the auto-grader check for changes outside the grading markers)
Sorry for the inconvenience.
I will also soon update the incremental.rs example from the last lecture demos to match the same network model.