/* Now, we think we are putting the right progress assertion
  and checking for absence of priority inversion.

  Nope - as expected, this is not good enough! */

/*
From ratan@facility Fri Feb 17 16:20:27 1995
Received: from sunset.cs.utah.edu by bliss.cs.utah.edu (8.6.9/utah-2.15sun-leaf)
	id JAA03737; Fri, 17 Feb 1995 09:20:26 -0700
From: ratan@facility
Received: from lal.cs.utah.edu by sunset.cs.utah.edu (8.6.9/utah-2.15sun-leaf)
	id JAA10122; Fri, 17 Feb 1995 09:20:25 -0700
Received: by lal.cs.utah.edu (8.6.9/utah-2.15sun-leaf)
	id JAA20451; Fri, 17 Feb 1995 09:20:24 -0700
Date: Fri, 17 Feb 1995 09:20:24 -0700
Message-Id: <199502171620.JAA20451@lal.cs.utah.edu>
To: ganesh@facility
Subject: locking protocol
Content-Length: 3256
Status: R
*/

/* Modified by Ganesh */

/* Three processes, and one lock */

#define NPROC 3
#define NPROC_1 2

#define PID byte

bit mutex[NPROC];
PID po[NPROC];
chan request[NPROC] = [NPROC_1] of {PID};
chan q_len_ch[NPROC] = [1] of {byte};
chan waiters[NPROC] = [NPROC_1] of {PID};
byte qlen[NPROC];   /* How many are waiting? */
bit locked[NPROC];

proctype acquire(PID me)
{
    PID thread;
    byte count;
    loop:
        /* Try to acquire the lock */
        atomic { mutex[me] == 0 ->
                 mutex[me] = 1
        };
        if
        :: po[me] == me -> locked[me] = 1;
                            mutex[me] = 0
        :: po[me] != me ->
                        request[po[me]]!me;
                        mutex[me] = 0;
			
                        /* Wait until reply comes back */
                       q_len_ch[me] ? [count];
 
                       atomic { mutex[me]==0 ;

		       /* This is the key step of getting a lock !! */
                                po[me] = me;
				
                                mutex[me] = 1;
                                q_len_ch[me] ? count;
                                qlen[me] = qlen[me]+count;
                                count = 0
                        };
                        ( len(waiters[me]) == qlen[me] );
                        locked[me] = 1;
                        mutex[me]=0
        fi;

                        /* Acquire continued */
    release:
        atomic {
            mutex[me] == 0 ->
            locked[me] = 0;
            mutex[me] = 1
        };
        if
        :: qlen[me] ->
            waiters[me] ? po[me];
            qlen[me] = qlen[me]-1;
            q_len_ch[po[me]] ! qlen[me];
            do
            :: qlen[me] -> atomic {
                waiters[me] ? thread;
                waiters[po[me]] ! thread;
                thread = 0;
                qlen[me] = qlen[me]-1
               }
            :: !qlen[me] -> break
            od
        :: !qlen[me] -> skip
        fi;
        mutex[me] = 0;
        assert (qlen[me] >= 0);
    goto loop
}


proctype handle(int me)
{   
    PID requester;

    do
    :: atomic {
            mutex[me] == 0 && request[me]?[requester] ->
            mutex[me] = 1;
            request[me] ? requester
        };
        if
        :: po[me] != me -> request[po[me]] ! requester
        :: po[me] == me && locked[me] ->
                    waiters[me] ! requester;
                    qlen[me] = qlen[me] + 1;
                    assert (qlen[me] < NPROC)
        :: po[me] == me && !locked[me] ->
                    q_len_ch[requester] ! 0;
                    assert (qlen[me] == 0);
                    po[me] = requester
        fi;
        mutex[me] = 0
    od
}


init {
    byte cnt = 0;

    atomic {
        do
        :: cnt == NPROC-> break
        :: cnt != NPROC-> run acquire(cnt);
                      run handle(cnt);
                      cnt = cnt+1
        od
    }
}

/*==*/

#define a	(len(q_len_ch[1])>0)
#define b	(po[1]==1)
#define c	(locked[0]==0)
#define d	(locked[0]==1)

	/*
	 * Formula As Typed: [](a -> <> b)  -> [](c -> <> d)
	 * The Never Claim Below Corresponds
	 * To The Negated Formula !([](a -> <> b)  -> [](c -> <> d))
	 * (formalizing violations of the original)
	 */

never {    /* !([](a -> <> b)  -> [](c -> <> d)) */
T0_init:
	if
	:: (! ((d)) && (b) && (c)) -> goto accept_S8
	:: (! ((d)) && (c)) -> goto T0_S135
	:: (! ((a)) && ! ((d)) && (c)) -> goto accept_S111
	:: (((! ((a))) || ((b)))) -> goto T0_init
	:: (1) -> goto T0_S203
	fi;
accept_S8:
	if
	:: (! ((d)) && (b)) -> goto T0_S8
	:: (! ((d))) -> goto T0_S135
	:: (! ((a)) && ! ((d))) -> goto T0_S111
	fi;
accept_S111:
	if
	:: (! ((d))) -> goto T0_S135
	:: (((! ((a)) && ! ((d))) || (! ((d)) && (b)))) -> goto T0_S111
	fi;
accept_S135:
	if
	:: (! ((d))) -> goto T0_S135
	:: (! ((d)) && (b)) -> goto T0_S111
	fi;
T0_S8:
	if
	:: (! ((d)) && (b)) -> goto accept_S8
	:: (! ((d))) -> goto T0_S135
	:: (! ((a)) && ! ((d))) -> goto accept_S111
	fi;
T0_S111:
	if
	:: (! ((d))) -> goto T0_S135
	:: (((! ((a)) && ! ((d))) || (! ((d)) && (b)))) -> goto accept_S111
	fi;
T0_S135:
	if
	:: (! ((d))) -> goto T0_S135
	:: (! ((d)) && (b)) -> goto accept_S111
	:: (! ((d)) && (b)) -> goto accept_S135
	fi;
T0_S203:
	if
	:: (! ((d)) && (c)) -> goto T0_S135
	:: ((b)) -> goto T0_init
	:: (1) -> goto T0_S203
	:: (! ((d)) && (b) && (c)) -> goto accept_S111
	:: (! ((d)) && (b) && (c)) -> goto accept_S135
	fi;
}

#ifdef NOTES
Use Load to open a file or a template.

#endif
#ifdef RESULT


#endif