orig.da

import sys
import time

config(channel is fifo, clock is lamport)

class P(process):
    def setup(s:set, nrequests:int,  logps:Log):  # s is set of all other processes
        self.q = set()

    def mutex(task):
        -- request
        c = logical_clock()
        send(('request', c, self), to= s)
        q.add(('request', c, self))
        await(each(('request', c2, p) in q,
                   has= (c2, p)==(c, self) or (c, self) < (c2, p)) and
              each(p in s, has= some(received(('ack', c2, _p)), has= c2 > c)))
        -- critical_section
        send(('incs', logical_clock(), self), to=logps)
        task()
        send(('outcs', logical_clock(), self), to=logps)
        -- release
        q.remove(('request', c, self))
        send(('release', logical_clock(), self), to= s)

    def receive(msg= ('request', c2, p)):
        q.add(('request', c2, p))
        send(('ack', logical_clock(), self), to= p)

    def receive(msg= ('release', _, p)):
#        q.remove(('request', _, p))  # pattern matching needed for _
#        q.remove(anyof(setof(('request', c, p), ('request', c, _p) in q)))
        for x in setof(('request', c, p), ('request', c, _p) in q):
            q.remove(x)
            break
#        for ('request', c, _p) in q: q.remove('request', c, p); break
#        for (tag, c, p2) in q:
#            if tag == 'request' and p2 == p:
#                q.remove((tag, c, p2)); break

    def run():
        start_cpu_time = time.time()
        def task():
            pass
        for i in range(nrequests):
            mutex(task)

        send(('done', self), to= parent())
        end_cpu_time = time.time()
        total_cpu_time = end_cpu_time - start_cpu_time
        send (('cputime', total_cpu_time, self), to= logps)
        await(received(('done',), from_=parent()))
        #output('terminating')