67 lines
1.3 KiB
Promela
67 lines
1.3 KiB
Promela
#define N 10
|
|
#define LENGTH 3
|
|
#define R 2
|
|
|
|
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; 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;
|
|
for (i in to_reverse) {
|
|
int value;
|
|
select(value: 0 .. R);
|
|
to_reverse[i] = value;
|
|
}
|
|
}
|
|
|
|
// ParallelReverser implementation
|
|
int n;
|
|
int s = LENGTH / N;
|
|
|
|
pid pids[N];
|
|
|
|
// fork section
|
|
for (n: 0 .. N) {
|
|
int from = n * s;
|
|
int to;
|
|
if
|
|
:: (n == N - 1) -> to = LENGTH;
|
|
:: else -> to = n * s + s;
|
|
fi
|
|
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]);
|
|
}
|
|
}
|
|
|
|
// ltl syntax: https://spinroot.com/spin/Man/ltl.html
|
|
ltl test {
|
|
eventually (false) implies true
|
|
// eventually (a > b) implies len(q) == 0
|
|
} |