News
Project 1 Patch
Written on 29.12.2024 17:43 by Andrea Lattuada
Dear Students, apologies for a second email in one day.
The first few submissions for project 01 have made me notice that, while the project file is correct, it allows for certain kinds of unfortunate typos that may make your proof meaningless. I cannot guard against the majority of them, obviously (you are in charge of being careful in writing your specification and safety property, as we discussed at length), but in an attempt to better evaluate your skills in the project I have added a pseudo_liveness proof obligation (akin to the ones you have seen before in exercises) for exercise01.rs that will hopefully help you catch certain careless mistakes.
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/contents/view/6 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, and hope this helps.