This repository contains the code used to realize the project of Formal Method in Software Development a.y. 2019/2020 held at Sapienza University of Rome.
Given a grid (stated differently a matrix) which each cell have one of the following shape:
- Start cell (S);
- Obstacle cell (#);
- Legal cell (o);
- Goal cell (G).
The system returns, if exists the best path from S leading to G.
Everything is done, using the definition of controller implemented in Python 3.6. (see paragraph 4.1).
The developed controller is realised interacting with NuSMV symbolic model checker.
Before run , ENSURE that the NuSMV bin (download here http://nusmv.fbk.eu/) is inside numsmv_exactubles/linux or numsmv_exactubles/mac-os folder (it depends on your o.s.)
In order to proof the existence of a path that doesn't have any obstacles # from S to G, we state the following Temporal Logic formulae:
- LTL : ¬♢ (G*)
- CTL : ¬E♢ (G*)
G* means the coordinate of the Goal cell
python3 goal_game.py