diff --git a/ReversalModel/reversal.pml b/ReversalModel/reversal.pml index c75a667..a45a107 100644 --- a/ReversalModel/reversal.pml +++ b/ReversalModel/reversal.pml @@ -5,15 +5,26 @@ int to_reverse[LENGTH]; // array to reverse int reversed[LENGTH]; // array where the reverse is stored +mtype = { END }; + // ThreadedReverser implementation -proctype ThreadedReverser(int from; int to) { +proctype ThreadedReverser(int from; int to; chan out) { + printf("proc[%d]: started\n", _pid); + int k; for (k: from .. to) { reversed[LENGTH - k - 1] = to_reverse[k]; - } + } + + printf("proc[%d]: ended\n", _pid); + +end: + out!_pid; } init { + chan in = [N] of { mtype }; + // array initialization { int i; @@ -27,6 +38,10 @@ init { // ParallelReverser implementation int n; int s = LENGTH / N; + + pid pids[N]; + + // fork section for (n: 0 .. N) { int from = n * s; int to; @@ -34,7 +49,14 @@ init { :: (n == N - 1) -> to = LENGTH; :: else -> to = n * s + s; fi - run ThreadedReverser(from, to); + pids[n] = run ThreadedReverser(from, to, in); + } + + // join section + for (n: 0 .. N) { + in??eval(pids[n]); + + printf("init: joined process %d\n", pids[n]); } }