Introduction to Model-Checking; Theory and Practice
The course lectures and the practical works rely on Tina, a model-checking toolbox for Petri nets and their extensions. Most of the work requires the use of nd (NetDraw); an editor and GUI for Petri nets and Automata.
Simply download the right executable for your OS, unpack it, and put it in a
place where it can be found by your shell (this may include updating your
On windows machine, make sure to avoid installing the software on a directory that contains white-spaces or unicode characters (always a sensible thing to do with Windows).
On mac, slide application
into the Applications folder; the binaries are found in
nd.app/Contents/MacOS/bin. On versions of MacOS with GateKeeper enabled
(10.8,9,…), GateKeeper will prevent installing tina and pretend that the
application is damaged. It is not; it is simply that tina is not signed by a
registered Apple developper.
On such systems, tina can be installed as follows:
remove any installed version of tina
disable GateKeeper in System Preferences
On 10.10 for instance, this is done by: System Preferences > Security & Privacy > General > Allow apps downloaded from: > Anywhere
On 10.12 (Sierra), you need first to make “Anywhere” appear again by typing the following line in a terminal:
sudo spctl --master-disable
download a suitable version of tina
install tina and launch it