I am looking for someone who could write a simple model using Promela language 'Leader election using ring'. I got a code and documentation for that and I have to consider two cases:
1) all nodes have different IDs
2) two nodes have the same ID
but still, I got problems with installing Spin.
I need an output model (screens).