-- SMV model of first attempt in notes.
-- Asynchronous, fair model assuming finite non-critical section.
-- Satisfies mutual exclusion and eventual entry.
-- Works fine, but is based on assumption that non-critical section 
-- is always terminating. Could just use round robin in that case.
-- Parameter id used by value, parameter turn used by reference
MODULE C(id, turn)
VAR
  st : {nc, cr};
ASSIGN
  init(st) := nc;
  next(st) := 
    case
      st=nc & turn=id : cr;
      st=cr : nc;
      TRUE : st;
    esac;
  next(turn) := 
    case
      st=cr : !turn;
      TRUE : turn;
    esac;
FAIRNESS
  running

MODULE main
VAR
  C0 : process C(0, turn);
  C1 : process C(1, turn);
  turn : boolean;

-- mutual exclusion
-- true
SPEC AG !(C0.st=cr & C1.st=cr)

-- eventual entry for C0
-- true
SPEC AG (C0.st=nc -> AF C0.st=cr)

-- eventual entry for C1
-- true
SPEC AG (C1.st=nc -> AF C1.st=cr)

-- C0 in critical section infintely often
-- true
SPEC AG AF C0.st=cr

-- C1 in critical section infintely often
-- true
SPEC AG AF C1.st=cr

--------------------------------------------------------

-- SMV model of first attempt in notes.
-- Asynchronous, fair model allowing non-termininating non-critical section
-- Satisfies mutex
-- Does not satisfy eventual entry, because process pointed to by turn may 
-- not be interested in entering 
MODULE P(id, turn)
VAR
  st : {nc, en, cr, ex};
ASSIGN
  init(st) := nc;
  next(st) := 
    case
      st=nc : {nc, en};
      st=en & turn=id : cr;
      st=cr : ex;
      st=ex : nc;
      TRUE : st;
    esac;
  next(turn) := 
    case
      st=ex : !turn;
      TRUE : turn;
    esac;
FAIRNESS
  running

MODULE main
VAR
  p0 : process P(0, turn);
  p1 : process P(1, turn);
  turn : boolean;
ASSIGN
  init(turn) := FALSE;
SPEC 
-- true
  AG !(p0.st=cr & p1.st=cr)
SPEC
-- false (why?)
  AG (p0.st=en -> AF p0.st=cr)
SPEC
-- false (why?)
  AG (p1.st=en -> AF p1.st=cr)

--------------------------------------------------------

-- SMV model of 2nd attempt given in notes 
-- Asynchronous, fair model allowing non-termininating non-critical section
-- Satisfies mutex
-- Does not satisfy eventual entry, because turn may not be set to interested 
-- process
MODULE P(id, myReq, otherReq, turn)
VAR
  st : {nc, en1, en2, cr, ex1, ex2};
ASSIGN
  init(st) := nc;
  next(st) := 
    case
      st=nc : {nc, en1};
      st=en1 : en2;
      st=en2 & turn=id : cr;
      st=cr : ex1;
      st=ex1 : ex2;
      st=ex2 : nc;
      TRUE : st;
    esac;
  next(myReq) :=
    case
      st=en1 : TRUE;
      st=ex1 : FALSE;
      TRUE : myReq;
    esac;
  next(turn) := 
    case
      st=ex2 & otherReq : !id;
      TRUE : turn;
    esac;
FAIRNESS
  running

MODULE main
VAR
  p0 : process P(0, req0, req1, turn);
  p1 : process P(1, req1, req0, turn);
  turn : boolean;
  req0 : boolean;
  req1 : boolean;
ASSIGN
  init(turn) := FALSE;
  init(req0) := FALSE;
  init(req1) := FALSE;
SPEC 
-- true
  AG !(p0.st=cr & p1.st=cr)
SPEC
-- false (why?)
  AG (p0.st=en1 -> AF p0.st=cr)
SPEC
-- false (why?)
  AG (p1.st=en1 -> AF p1.st=cr)

--------------------------------------------------------

-- SMV model of 3rd attempt given in notes 
-- Asynchronous, fair model allowing non-termininating non-critical section 
-- Satisfies mutex
-- Does not satisfy eventual entry, because both processes may get stuck in 
-- entry protocol
MODULE P(id, myReq, otherReq)
VAR
  st : {nc, en1, en2, cr, ex};
ASSIGN
  init(st) := nc;
  next(st) := 
    case
      st=nc : {nc, en1};
      st=en1 : en2;
      st=en2 & !otherReq : cr;
      st=cr : ex;
      st=ex : nc;
      TRUE : st;
    esac;
  next(myReq) :=
    case
      st=en1 : TRUE;
      st=ex : FALSE;
      TRUE : myReq;
    esac;
FAIRNESS
  running

MODULE main
VAR
  p0 : process P(0, req0, req1);
  p1 : process P(1, req1, req0);
  req0 : boolean;
  req1 : boolean;
ASSIGN
  init(req0) := FALSE;
  init(req1) := FALSE;
SPEC 
-- true
  AG !(p0.st=cr & p1.st=cr)
SPEC
-- false (why?)
  AG (p0.st=en1 -> AF p0.st=cr)
SPEC
-- false (why?)
  AG (p1.st=en1 -> AF p1.st=cr)

-------------------------------------------------------------

-- SMV model of 4th attempt given in notes 
-- Version 1: req and last get set simultaneously
-- Asynchronous, fair model allowing non-termininating non-critical section 
-- Satisfies mutex and eventual entry
MODULE P(id, myReq, otherReq, last)
VAR
  st : {nc, en1, en2, cr, ex};
ASSIGN
  init(st) := nc;
  next(st) := 
    case
      st=nc : {nc, en1};
      st=en1 : en2;
      st=en2 & myReq & (!otherReq | !last=id) : cr;
      st=cr : ex;
      st=ex : nc;
      TRUE : st;
    esac;
  next(myReq) :=
    case
      st=en1 : TRUE;
      st=ex : FALSE;
      TRUE : myReq;
    esac;
  next(last) :=
    case
      st=en1 : id;
      TRUE : last;
    esac;
FAIRNESS
  running

MODULE main
VAR
  p0 : process P(0, req0, req1, last);
  p1 : process P(1, req1, req0, last);
  req0 : boolean;
  req1 : boolean;
  last : boolean;
ASSIGN
  init(req0) := FALSE;
  init(req1) := FALSE;
SPEC 
-- true
  AG !(p0.st=cr & p1.st=cr)
SPEC
-- false (why?)
  AG (p0.st=en1 -> AF p0.st=cr)
SPEC
-- false (why?)
  AG (p1.st=en1 -> AF p1.st=cr)

-------------------------------------------------------------

-- SMV model of 4th attempt given in notes 
-- Version 2: req set first and then last 
-- Asynchronous, fair model allowing non-termininating non-critical section 
-- Satisfies mutex and eventual entry
MODULE P(id, myReq, otherReq, last)
VAR
  st : {nc, en1, en2, en3, cr, ex};
ASSIGN
  init(st) := nc;
  next(st) := 
    case
      st=nc : {nc, en1};
      st=en1 : en2;
      st=en2 : en3;
      st=en3 & myReq & (!otherReq | !last=id) : cr;
      st=cr : ex;
      st=ex : nc;
      TRUE : st;
    esac;
  next(myReq) :=
    case
      st=en1 : TRUE;
      st=ex : FALSE;
      TRUE : myReq;
    esac;
  next(last) :=
    case
      st=en2 : id;
      TRUE : last;
    esac;
FAIRNESS running

MODULE main
VAR
  p0 : process P(0, req0, req1, last);
  p1 : process P(1, req1, req0, last);
  req0 : boolean;
  req1 : boolean;
  last : boolean;
ASSIGN
  init(req0) := FALSE;
  init(req1) := FALSE;
SPEC 
-- true
  AG !(p0.st=cr & p1.st=cr)
SPEC
-- true 
  AG (p0.st=en1 -> AF p0.st=cr)
SPEC
-- true
  AG (p1.st=en1 -> AF p1.st=cr)

-------------------------------------------------------------

-- SMV model of 4th attempt given in notes 
-- Version 3: last set first and then req
-- Asynchronous, fair model allowing non-termininating non-critical section 
-- Satisfies eventual entry
-- Does not satisfy mutex!
MODULE P(id, myReq, otherReq, last)
VAR
  st : {nc, en1, en2, en3, cr, ex};
ASSIGN
  init(st) := nc;
  next(st) := 
    case
      st=nc : {nc, en1};
      st=en1 : en2;
      st=en2 : en3;
      st=en3 & myReq & (!otherReq | !last=id) : cr;
      st=cr : ex;
      st=ex : nc;
      TRUE : st;
    esac;
  next(myReq) :=
    case
      st=en2 : TRUE;
      st=ex : FALSE;
      TRUE : myReq;
    esac;
  next(last) :=
    case
      st=en1 : id;
      TRUE : last;
    esac;
FAIRNESS
  running

MODULE main
VAR
  p0 : process P(0, req0, req1, last);
  p1 : process P(1, req1, req0, last);
  req0 : boolean;
  req1 : boolean;
  last : boolean;
ASSIGN
  init(req0) := FALSE;
  init(req1) := FALSE;
SPEC 
-- false (why?)
  AG !(p0.st=cr & p1.st=cr)
SPEC
-- true
  AG (p0.st=en1 -> AF p0.st=cr)
SPEC
-- true
  AG (p1.st=en1 -> AF p1.st=cr)