Hi, all. During today's lecture I intend to use an additional Rodin plugin. It would be great if you install it ahead of time. If you cannot, we'll do it during the lecture.

It's the ProB model checker. Please install it by selecting the menu entry Help -> Install new Software . In the "work with" input box type "prob" and a url will appear. Select it, and the select the "ProB for Rodin" plugin that should appear listed below (if you expand the plugin, four components should show up; select all of them). Click "Next" at the bottom of the window, wait, restart and you should be good to go.

You may want to install as well the SMT solvers package:

- Go to "Install new software". - In the "Work with" input, click on the right downwards arrow to open a pull-down menu, select "All available sites". - In the list, scroll down to locate "Prover extensions". - Expand "Prover extensions" clicking on the ">" sign on the right. - Select "SMT Solvers" - Click "Next", wait for it to install, restart. - You will then have a new "SMT" button in the Theorem Prover perspective.

Best,