16.12.2021, 9:00 - 11:00: Due to updates GitLab may be unavailable for some minutes between 09:00 and 11:00.

Commit d7ebe133 authored by Philipp Meyer's avatar Philipp Meyer
Browse files

Added scalable versions of mutual exclusion algorithms

parent 9426cfb0
#!/usr/bin/python3
import sys
#c[i] := 1
#b[i] := 1
#turn := 0
# s1: b[i] := 0;
# s2: if turn /= i then
# s3: c[i] := 1
# s4: if turn = 0 or b[turn] = 1 then
# s5: turn := i
# fi
# s6: goto s2
# fi
# s7: c[i] := 0
# s8: for j:= 1 to N do
# s9_j: if j != i and c[j] = 0 then
#s10: goto s2
# fi
# done
#s11: critical section
#s12: turn := 0
#s13: c[i] := 1
#s14: b[i] := 1
#s15: goto s1
def make_net(n, prop, p):
print('petri net "Dijstra\'s version for n processes of Dekker\'s mutual exclusion algorithm for n=%i" {' % n)
print(' places {', end='')
for i in range(1,n+1):
print()
print(' p%is1' % i)
print(' p%is2' % i)
print(' p%is3' % i)
print(' p%is4' % i)
print(' p%is4turn0' % i, end='')
for j in range(1,n+1):
print(' p%is4turn%i' % (i,j), end='')
print()
print(' p%is5' % i)
print(' p%is6' % i)
print(' p%is7' % i)
print(' p%is8' % i)
print(' ', end='')
for j in range(1,n+1):
print(' p%is9j%i' % (i,j), end='')
print()
print(' p%is10' % i)
print(' p%is11' % i)
print(' p%is12' % i)
print(' p%is13' % i)
print(' p%is14' % i)
print(' p%is15' % i)
print(' c%iv0 c%iv1 b%iv0 b%iv1' % (i,i,i,i))
print()
print(' turn0', end='')
for i in range(1,n+1):
print(' turn%i' % i, end='')
print()
print(' }')
print(' transitions {', end='')
for i in range(1,n+1):
print()
print(' t%is1b%iv0 t%is1b%iv1' % (i,i,i,i))
print(' t%is2turn0' % i, end='')
for j in range(1,n+1):
print(' t%is2turn%i' % (i,j), end='')
print()
print(' t%is3c%iv0 t%is3c%iv1' % (i,i,i,i))
print(' t%is4turn0' % i, end='')
for j in range(1,n+1):
print(' t%is4turn%i' % (i,j), end='')
print()
print(' ', end='')
for j in range(1,n+1):
print(' t%is4turn%ib%iv0 t%is4turn%ib%iv1' % (i,j,j,i,j,j), end='')
print()
print(' t%is5turn0' % i, end='')
for j in range(1,n+1):
print(' t%is5turn%i' % (i,j), end='')
print()
print(' t%is6' % i)
print(' t%is7c%iv0 t%is7c%iv1' % (i,i,i,i))
print(' t%is8' % i)
print(' ', end='')
for j in range(1,n+1):
if i == j:
print(' t%is9j%i' % (i,j), end='')
else:
print(' t%is9j%ic%iv0 t%is9j%ic%iv1' % (i,j,j,i,j,j), end='')
print()
print(' t%is10' % i)
print(' t%is11' % i)
print(' t%is12turn0' % i, end='')
for j in range(1,n+1):
print(' t%is12turn%i' % (i,j), end='')
print()
print(' t%is13c%iv0 t%is13c%iv1' % (i,i,i,i))
print(' t%is14b%iv0 t%is14b%iv1' % (i,i,i,i))
print(' t%is15' % i)
print(' }')
print(' arcs {', end='')
for i in range(1,n+1):
print()
print()
print(' { p%is1 b%iv0 } -> t%is1b%iv0 -> { p%is2 b%iv0 }' % (i,i,i,i,i,i))
print(' { p%is1 b%iv1 } -> t%is1b%iv1 -> { p%is2 b%iv0 }' % (i,i,i,i,i,i))
print(' { p%is2 turn0 } -> t%is2turn0 -> { p%is3 turn0 }' % (i,i,i))
for j in range(1,n+1):
if i == j:
print(' { p%is2 turn%i } -> t%is2turn%i -> { p%is7 turn%i }' % (i,j,i,j,i,j))
else:
print(' { p%is2 turn%i } -> t%is2turn%i -> { p%is3 turn%i }' % (i,j,i,j,i,j))
print(' { p%is3 c%iv0 } -> t%is3c%iv0 -> { p%is4 c%iv1 }' % (i,i,i,i,i,i))
print(' { p%is3 c%iv1 } -> t%is3c%iv1 -> { p%is4 c%iv1 }' % (i,i,i,i,i,i))
print(' { p%is4 turn0 } -> t%is4turn0 -> { p%is5 turn0 }' % (i,i,i))
for j in range(1,n+1):
print(' { p%is4 turn%i } -> t%is4turn%i -> { p%is4turn%i turn%i }' % (i,j,i,j,i,j,j))
for j in range(1,n+1):
print(' { p%is4turn%i b%iv0 } -> t%is4turn%ib%iv0 -> { p%is6 b%iv0 }' % (i,j,j,i,j,j,i,j))
print(' { p%is4turn%i b%iv1 } -> t%is4turn%ib%iv1 -> { p%is5 b%iv1 }' % (i,j,j,i,j,j,i,j))
for j in range(0,n+1):
print(' { p%is5 turn%i } -> t%is5turn%i -> { p%is6 turn%i }' % (i,j,i,j,i,i))
print(' { p%is6 } -> t%is6 -> { p%is2 }' % (i,i,i))
print(' { p%is7 c%iv0 } -> t%is7c%iv0 -> { p%is8 c%iv0 }' % (i,i,i,i,i,i))
print(' { p%is7 c%iv1 } -> t%is7c%iv1 -> { p%is8 c%iv0 }' % (i,i,i,i,i,i))
print(' { p%is8 } -> t%is8 -> { p%is9j1 }' % (i,i,i))
for j in range(1,n+1):
if i == j:
if j == n:
print(' { p%is9j%i } -> t%is9j%i -> { p%is11 }' % (i,j,i,j,i))
else:
print(' { p%is9j%i } -> t%is9j%i -> { p%is9j%i }' % (i,j,i,j,i,j+1))
else:
print(' { p%is9j%i c%iv0 } -> t%is9j%ic%iv0 -> { p%is10 c%iv0 }' % (i,j,j,i,j,j,i,j))
if j == n:
print(' { p%is9j%i c%iv1 } -> t%is9j%ic%iv1 -> { p%is11 c%iv1 }' % (i,j,j,i,j,j,i,j))
else:
print(' { p%is9j%i c%iv1 } -> t%is9j%ic%iv1 -> { p%is9j%i c%iv1 }' % (i,j,j,i,j,j,i,j+1,j))
print(' { p%is10 } -> t%is10 -> { p%is2 }' % (i,i,i))
print(' { p%is11 } -> t%is11 -> { p%is12 }' % (i,i,i))
for j in range(0,n+1):
print(' { p%is12 turn%i } -> t%is12turn%i -> { p%is13 turn0 }' % (i,j,i,j,i))
print(' { p%is13 c%iv0 } -> t%is13c%iv0 -> { p%is14 c%iv1 }' % (i,i,i,i,i,i))
print(' { p%is13 c%iv1 } -> t%is13c%iv1 -> { p%is14 c%iv1 }' % (i,i,i,i,i,i))
print(' { p%is14 b%iv0 } -> t%is14b%iv0 -> { p%is15 b%iv1 }' % (i,i,i,i,i,i))
print(' { p%is14 b%iv1 } -> t%is14b%iv1 -> { p%is15 b%iv1 }' % (i,i,i,i,i,i))
print(' { p%is15 } -> t%is15 -> { p%is1 }' % (i,i,i))
print()
print(' }')
print(' initial {')
for i in range(1,n+1):
print(' p%is1 b%iv1 c%iv1' % (i,i,i))
print(' turn0')
print(' }')
print('}')
if prop == 'fairness':
print('liveness property "starvation freedom for process %i" {' % p)
for i in range(1,n+1):
print(' t%is1b%iv0 + t%is1b%iv1 + ' % (i,i,i,i), end='')
print('t%is2turn0 + ' % i, end='')
for j in range(1,n+1):
print('t%is2turn%i + ' % (i,j), end='')
print('t%is3c%iv0 + t%is3c%iv1 + ' % (i,i,i,i), end='')
print('t%is4turn0 + ' % i, end='')
for j in range(1,n+1):
print('t%is4turn%i + ' % (i,j), end='')
for j in range(1,n+1):
print('t%is4turn%ib%iv0 + t%is4turn%ib%iv1 + ' % (i,j,j,i,j,j), end='')
print('t%is5turn0 + ' % i, end='')
for j in range(1,n+1):
print('t%is5turn%i + ' % (i,j), end='')
print('t%is6 + ' % i, end='')
print('t%is7c%iv0 + t%is7c%iv1 + ' % (i,i,i,i), end='')
print('t%is8 + ' % i, end='')
for j in range(1,n+1):
if i == j:
print('t%is9j%i + ' % (i,j), end='')
else:
print('t%is9j%ic%iv0 + t%is9j%ic%iv1 + ' % (i,j,j,i,j,j), end='')
print('t%is10 + ' % i, end='')
print('t%is11 + ' % i, end='')
print('t%is12turn0 + ' % i, end='')
for j in range(1,n+1):
print('t%is12turn%i + ' % (i,j), end='')
print('t%is13c%iv0 + t%is13c%iv1 + ' % (i,i,i,i), end='')
print('t%is14b%iv0 + t%is14b%iv1 + ' % (i,i,i,i), end='')
print('t%is15 > 0 &&' % i)
print(' t%is11 = 0' % p)
print('}')
elif prop == 'safety':
print('safety property "mutual exclusion" {')
print(' p1s11', end='')
for i in range(2,n+1):
print(' + p%is11' % i, end='')
print(' >= 2')
print('}')
n = int(sys.argv[1])
prop = 'fairness'
process = 1
make_net(n, prop, process)
#!/usr/bin/bash
n=$1
for i in $(seq 1 $n); do
echo "Creating net for n = $i"
./make_net.py $i > "n$i.pnet"
done
#!/usr/bin/python3
import sys
# x_i := false;
#s1: x_i = true;
#s2: for j := 1 until i - 1 do
#s2_j_1: if x_j then
#s2_j_2: x_i := false;
#s2_j_3: while x_j do od;
#s2_j_4: goto s1;
# fi
# od
#s3: for j := i + 1 until N do
#s3_j: while x_j do od;
# od
#s4: critical section
#s5: x_i := false
def make_net(n, prop, p):
print('petri net "Lamport\'s 1-bit mutual exclusion algorithm for n=%i" {' % n)
print(' places {', end='')
for i in range(1,n+1):
print()
print(' p%is1' % i)
print(' p%is2' % i, end='')
for j in range(1,i):
print(' p%is2j%is1' % (i,j), end='')
print(' p%is2j%is2' % (i,j), end='')
print(' p%is2j%is3' % (i,j), end='')
print(' p%is2j%is4' % (i,j), end='')
print()
print(' p%is3' % i, end='')
for j in range(i+1,n+1):
print(' p%is3j%i' % (i,j), end='')
print()
print(' p%is4' % i)
print(' p%is5' % i)
print(' b%it b%if' % (i,i))
print(' }')
print(' transitions {', end='')
for i in range(1,n+1):
print()
print(' t%is1' % i)
print(' t%is2' % i, end='')
for j in range(1,i):
print(' t%is2j%is1b%it' % (i,j,j), end='')
print(' t%is2j%is1b%if' % (i,j,j), end='')
print(' t%is2j%is2' % (i,j), end='')
print(' t%is2j%is3b%it' % (i,j,j), end='')
print(' t%is2j%is3b%if' % (i,j,j), end='')
print(' t%is2j%is4' % (i,j), end='')
print()
print(' t%is3' % i, end='')
for j in range(i+1,n+1):
print(' t%is3j%ib%it' % (i,j,j), end='')
print(' t%is3j%ib%if' % (i,j,j), end='')
print()
print(' t%is4' % i)
print(' t%is5' % i)
print(' }')
print(' arcs {', end='')
for i in range(1,n+1):
print()
print()
print(' { p%is1 b%if } -> t%is1 -> { p%is2 b%it }' % (i,i,i,i,i))
print()
if i == 1:
print(' { p%is2 } -> t%is2 -> { p%is3 }' % (i,i,i))
else:
print(' { p%is2 } -> t%is2 -> { p%is2j1s1 }' % (i,i,i))
for j in range(1,i):
print(' { p%is2j%is1 b%it } -> t%is2j%is1b%it -> { p%is2j%is2 b%it }'
% (i,j,j,i,j,j,i,j,j))
if j == i - 1:
print(' { p%is2j%is1 b%if } -> t%is2j%is1b%if -> { p%is3 b%if }'
% (i,j,j,i,j,j,i,j))
else:
print(' { p%is2j%is1 b%if } -> t%is2j%is1b%if -> { p%is2j%is1 b%if }'
% (i,j,j,i,j,j,i,j+1,j))
print(' { p%is2j%is2 b%it } -> t%is2j%is2 -> { p%is2j%is3 b%if }'
% (i,j,i,i,j,i,j,i))
print(' { p%is2j%is3 b%it } -> t%is2j%is3b%it -> { p%is2j%is3 b%it }'
% (i,j,j,i,j,j,i,j,j))
print(' { p%is2j%is3 b%if } -> t%is2j%is3b%if -> { p%is2j%is4 b%if }'
% (i,j,j,i,j,j,i,j,j))
print(' { p%is2j%is4 } -> t%is2j%is4 -> { p%is1 }'
% (i,j,i,j,i))
print()
if i == n:
print(' { p%is3 } -> t%is3 -> { p%is4 }' % (i,i,i))
else:
print(' { p%is3 } -> t%is3 -> { p%is3j%i }' % (i,i,i,i+1))
for j in range(i+1,n+1):
print(' { p%is3j%i b%it } -> t%is3j%ib%it -> { p%is3j%i b%it }'
% (i,j,j,i,j,j,i,j,j))
if j == n:
print(' { p%is3j%i b%if } -> t%is3j%ib%if -> { p%is4 b%if }'
% (i,j,j,i,j,j,i,j))
else:
print(' { p%is3j%i b%if } -> t%is3j%ib%if -> { p%is3j%i b%if }'
% (i,j,j,i,j,j,i,j+1,j))
print()
print(' { p%is4 } -> t%is4 -> { p%is5 }' % (i,i,i))
print()
print(' { p%is5 b%it } -> t%is5 -> { p%is1 b%if }' % (i,i,i,i,i))
print()
print(' }')
print(' initial {')
for i in range(1,n+1):
print(' p%is1 b%if' % (i,i))
print(' }')
print('}')
if prop == 'fairness':
print('liveness property "starvation freedom for process %i" {' % p)
for i in range(1,n+1):
print(' t%is1 + ' % i, end='')
print('t%is2 + ' % i, end='')
for j in range(1,i):
print('t%is2j%is1b%it + ' % (i,j,j), end='')
print('t%is2j%is1b%if + ' % (i,j,j), end='')
print('t%is2j%is2 + ' % (i,j), end='')
print('t%is2j%is3b%it + ' % (i,j,j), end='')
print('t%is2j%is3b%if + ' % (i,j,j), end='')
print('t%is2j%is4 + ' % (i,j), end='')
print('t%is3 + ' % i, end='')
for j in range(i+1,n+1):
print('t%is3j%ib%it + ' % (i,j,j), end='')
print('t%is3j%ib%if + ' % (i,j,j), end='')
print('t%is4 + ' % i, end='')
print('t%is5 > 0 &&' % i)
print(' t%is4 = 0' % p)
print('}')
elif prop == 'safety':
print('safety property "mutual exclusion" {')
print(' p1s4', end='')
for i in range(2,n+1):
print(' + p%is4' % i, end='')
print(' >= 2')
print('}')
n = int(sys.argv[1])
prop = 'fairness'
process = 1
make_net(n, prop, process)
#!/usr/bin/bash
n=$1
for i in $(seq 1 $n); do
echo "Creating net for n = $i"
./make_net.py $i > "n$i.pnet"
done
#!/usr/bin/python3
import sys
from itertools import chain
#q[i] := 0 for 1 ≤ i ≤ n
#turn[i] := 0 for 1 ≤ i ≤ n - 1
# s1: for j = 1 to n - 1 do
# s2_j: q[i] = j
# s3_j: turn[j] = i
# s4_j for k=1 to i-1, i+1 to n do
# s5_j_k: if ( q[k] >= j and
# s6_j_k turn[j] = i ) then
# s7_j_k: goto s4_j
# fi
# s8_j_k: next
# done
# s9_j: next
# done
#s10: q[i] = n
#s11: critical section
#s12: q[i] = 0
#s13: goto s1
def make_net(n, prop, p):
print('petri net "Peterson\'s mutual exclusion algorithm with levels for n=%i" {' % n)
print(' places {', end='')
for i in range(1,n+1):
print()
print(' p%is1' % i)
print(' ', end='')
for j in range(1,n):
print(' p%is2j%i' % (i,j), end='')
print()
print(' ', end='')
for j in range(1,n):
print(' p%is3j%i' % (i,j), end='')
print()
print(' ', end='')
for j in range(1,n):
print(' p%is4j%i' % (i,j), end='')
print()
print(' ', end='')
for j in range(1,n):
for k in chain(range(1,i), range(i+1,n+1)):
print(' p%is5j%ik%i' % (i,j,k), end='')
print()
print(' ', end='')
for j in range(1,n):
for k in chain(range(1,i), range(i+1,n+1)):
print(' p%is6j%ik%i' % (i,j,k), end='')
print()
print(' ', end='')
for j in range(1,n):
for k in chain(range(1,i), range(i+1,n+1)):
print(' p%is7j%ik%i' % (i,j,k), end='')
print()
print(' ', end='')
for j in range(1,n):
for k in chain(range(1,i), range(i+1,n+1)):
print(' p%is8j%ik%i' % (i,j,k), end='')
print()
print(' ', end='')
for j in range(1,n):
print(' p%is9j%i' % (i,j), end='')
print()
print(' p%is10' % i)
print(' p%is11' % i)
print(' p%is12' % i)
print(' p%is13' % i)
print(' q%iv0' % i, end='')
for j in range(1,n+1):
print(' q%iv%i' % (i,j), end='')
print()
print()
for j in range(1,n):
print(' ', end='')
for v in range(0,n+1):
print(' turn%iv%i' % (j,v), end='')
print()
print(' }')
print(' transitions {', end='')
for i in range(1,n+1):
print()
print(' t%is1' % i)
print(' ', end='')
for j in range(1,n):
print(' t%is2j%i' % (i,j), end='')
print()
print(' ', end='')
for j in range(1,n):
for k in range(0,n+1):
print(' t%is3j%iturn%iv%i' % (i,j,j,k), end='')
print()
print(' ', end='')
for j in range(1,n):
print(' t%is4j%i' % (i,j), end='')
print()
print(' ', end='')
for j in range(1,n):
for k in chain(range(1,i), range(i+1,n+1)):
for v in range(0,n+1):
print(' t%is5j%ik%iq%iv%i' % (i,j,k,k,v), end='')
print()
print(' ', end='')
for j in range(1,n):
for k in chain(range(1,i), range(i+1,n+1)):
for v in range(0,n+1):
print(' t%is6j%ik%iturn%iv%i' % (i,j,k,j,v), end='')
print()
print(' ', end='')
for j in range(1,n):
for k in chain(range(1,i), range(i+1,n+1)):
print(' t%is7j%ik%i' % (i,j,k), end='')
print()
print(' ', end='')
for j in range(1,n):
for k in chain(range(1,i), range(i+1,n+1)):
print(' t%is8j%ik%i' % (i,j,k), end='')
print()
print(' ', end='')
for j in range(1,n):
print(' t%is9j%i' % (i,j), end='')
print()
print(' t%is10' % i)
print(' t%is11' % i)
print(' t%is12' % i)
print(' t%is13' % i)
print(' }')
print(' arcs {', end='')
for i in range(1,n+1):
print()
print()
print(' { p%is1 } -> t%is1 -> { p%is2j1 }' % (i,i,i))
print()
for j in range(1,n):
print(' { p%is2j%i q%iv%i } -> t%is2j%i -> { p%is3j%i q%iv%i }'
% (i,j,i,j-1,i,j,i,j,i,j))
print()
for j in range(1,n):
for v in range(0,n+1):
print(' { p%is3j%i turn%iv%i } -> t%is3j%iturn%iv%i -> { p%is4j%i turn%iv%i }'
% (i,j,j,v,i,j,j,v,i,j,j,i))
print()
for j in range(1,n):
if i == 1:
print(' { p%is4j%i } -> t%is4j%i -> { p%is5j%ik2 }' % (i,j,i,j,i,j))
else:
print(' { p%is4j%i } -> t%is4j%i -> { p%is5j%ik1 }' % (i,j,i,j,i,j))
print()
for j in range(1,n):
for k in chain(range(1,i), range(i+1,n+1)):
for v in range(0,n+1):
if v >= j:
print(' { p%is5j%ik%i q%iv%i } -> t%is5j%ik%iq%iv%i -> { p%is6j%ik%i q%iv%i }'
% (i,j,k,k,v,i,j,k,k,v,i,j,k,k,v))
else:
print(' { p%is5j%ik%i q%iv%i } -> t%is5j%ik%iq%iv%i -> { p%is8j%ik%i q%iv%i }'
% (i,j,k,k,v,i,j,k,k,v,i,j,k,k,v))
print()
for j in range(1,n):
for k in chain(range(1,i), range(i+1,n+1)):
for v in range(0,n+1):
if v == i:
print(' { p%is6j%ik%i turn%iv%i } -> t%is6j%ik%iturn%iv%i -> { p%is7j%ik%i turn%iv%i }'
% (i,j,k,j,v,i,j,k,j,v,i,j,k,j,v))
else:
print(' { p%is6j%ik%i turn%iv%i } -> t%is6j%ik%iturn%iv%i -> { p%is8j%ik%i turn%iv%i }'
% (i,j,k,j,v,i,j,k,j,v,i,j,k,j,v))
print()
for j in range(1,n):
for k in chain(range(1,i), range(i+1,n+1)):
print(' { p%is7j%ik%i } -> t%is7j%ik%i -> { p%is4j%i }' % (i,j,k,i,j,k,i,j))
print()
for j in range(1,n):
for k in chain(range(1,i), range(i+1,n+1)):
if k == i - 1 and i == n or k == n:
print(' { p%is8j%ik%i } -> t%is8j%ik%i -> { p%is9j%i }'
% (i,j,k,i,j,k,i,j))
elif k == i - 1:
print(' { p%is8j%ik%i } -> t%is8j%ik%i -> { p%is5j%ik%i }'
% (i,j,k,i,j,k,i,j,i+1))
else:
print(' { p%is8j%ik%i } -> t%is8j%ik%i -> { p%is5j%ik%i }'
% (i,j,k,i,j,k,i,j,k+1))
print()
for j in range(1,n):
if j == n - 1:
print(' { p%is9j%i } -> t%is9j%i -> { p%is10 }' % (i,j,i,j,i))
else:
print(' { p%is9j%i } -> t%is9j%i -> { p%is2j%i }' % (i,j,i,j,i,j+1))
print()
print(' { p%is10 q%iv%i } -> t%is10 -> { p%is11 q%iv%i }' % (i,i,n-1,i,i,i,n))
print()
print(' { p%is11 } -> t%is11 -> { p%is12 }' % (i,i,i))
print()
print(' { p%is12 q%iv%i } -> t%is12 -> { p%is13 q%iv0 }' % (i,i,n,i,i,i))
print()
print(' { p%is13 } -> t%is13 -> { p%is1 }' % (i,i,i))
print()
print(' }')
print(' initial {')
for i in range(1,n+1):
print(' p%is1 q%iv0' % (i,i))
for j in range(1,n):
print(' turn%iv0' % j)
prin