nametype Index = {1,2}

channel non_crit, enter_crit, leave_crit: Index


----------------------------------------------------------------------------
--   Version 1
----------------------------------------------------------------------------

{-
    Each process P_i executes the following basic code:

        while true do
	   do_non_critical_stuff;
           while pnum = (3-i) do skip;
           enter_critical_section_i;
           leave_critical_section_i;
           pnum := 3-i;

    Moreover, pnum is initially set to 1.
 -}

-- Note that each P_i must be able to synchronize with the PNUM counter, 
-- but we don't want a 3-way synchronization.  In fact, for all intents 
-- and purposes, we'll allow P_1 and P_2 to operate indepedently of one
-- another  (ie, we'll use the interleaving operator |||).  Their only
-- constraints are those imposed by their interactions with the shared
-- variable pnum (represented by process PNUM).

-- Assignments to, and value-checking of, the variable is simulated via 
-- two distinct channels.

channel val_pnum, set_pnum: Index

X1 = {| val_pnum, set_pnum |}  -- all events involving val_pnum, set_pnum

-- PNUM(v) has current value v, so that's the only possible value it can 
-- report.  However, it will happily accept any and all requests to change
-- its current value 

PNUM(v) = val_pnum.v -> PNUM(v) [] set_pnum?w -> PNUM(w)

-- The encoding of each process P_i, version 1

PV1(i) = non_crit.i -> PV1_enter(i)

PV1_enter(i) =  val_pnum.(3-i) -> PV1_enter(i)
             [] val_pnum.i -> enter_crit.i -> leave_crit.i 
                                           -> set_pnum.(3-i) -> PV1(i) 


-- The initial configuration; note that PNUM originally has value 1
-- Processes PV1(1) and PV2(2) interact only through the shared
--   variable; they do not synchronize at all

SYSTEM_V1 = (PV1(1) ||| PV1(2) ) [Events || X1] PNUM(1)