Hi, all. I have updated the course web page with entries for the last session (slides, model, recording). As usual, I'll let you know of the URL for the next session (Wed, March 25th). In the meantime, some outstanding issues:
- Hermenegildo: you are not alone with the 32-bit issue in Mac OS Catalina:
https://sourceforge.net/p/rodin-b-sharp/mailman/message/36868847/
A possible workaround is using SMT solvers instead of the PP theorem prover (assuming they are 64-bit binaries). Go to Help -> Install new software, deinstall the Atelier B provers, in the "Work with" pull-down menu select
Rodin - http://rodin-b-sharp.sourceforge.net/updates
Scroll down to "Prover extensions", expand the entry, select "SMT Solvers" (latest version), install it, restart. In the Proving Perspective, a new "SMT" button should appear. I do not have a lot of experience with it, but I assume it also works with the hypotheses that appear in the "Selected Hypotheses" subwindow. In my limited experience, it works quite well. I have seen cases where PP does not straightforwardly solve issues that SMT does, and the other way around. I was not planning to use them in the course because I did not want to introduce additional ingredients, but having one possibility is better than none.
- Shuting: were the POs of m1 (with the variant-related proofs) finally discharged? They should have... I looked again at the goals that were pending and they were definitely provable. If you did not manage to discharge the POs, please try again clicking in the prover:
- pp (and wait until it fails) - p1 (and wait as well) - ml (it is better than pp in a few cases, but pp should be more than enough for this problem)
- Lucy: I redid the relative deadlock freedom from scratch and I also had to go to the theorem prover. I am convinced I did not have to do at some time. It may have to do with Rodin saving previous proof strategies and reusing them.
- Adrian: could you follow the lecture? IIRC you were using connecting using your cell phone. If it was troublesome, we can try to find a workaround.
- Someone else had troubles / issues, but I do not remember who that was...
- Last: I am still expecting HW#2 from some of you. If you are facing difficulties, please let me know.
Best,