SumNotTarget.prot

// The Sum-Not-(l-1) protocol defined in
// Title: Automated Design of Self-Stabilization
// Author: Aly Farahat
// Year: 2012

// The constants' names differ from Aly's dissertation.

constant N := 3;
constant M := 3;
constant Target := M-1;

variable x[N] < M;

process P[i < N]
{
  read:  x[i-1];
  write: x[i];

  (future & silent)
    (x[i-1] + x[i] != Target);

  puppet action:
    ( x[i-1] + x[i] == Target --> x[i] := Target + 1 - x[i-1]; );
}