define(N, `2')
define(LENGTH, `3')
define(R, `2')

define(`for',`ifelse($#,0,``$0'',`ifelse(eval($2<=$3),1,
    `pushdef(`$1',$2)$4`'popdef(`$1')$0(`$1',incr($2),$3,`$4')')')')

int to_reverse[LENGTH]; // array to reverse
int reversed_seq[LENGTH]; // for SequentialReverser: where the reverse is stored 
int reversed_par[LENGTH]; // for ParallelReverser: where the reverse is stored

// stores termination of each reverser
// index 0 is for the sequential algorithm
// indices 1-N are for the ThreadedReverser instances
bool done[N + 1]; // initialized to false

bool seq_eq_to_parallel = true;

// ThreadedReverser implementation
proctype ThreadedReverser(int from; int to; int n) {
    printf("proc[%d]: started from=%d to=%d\n", n, from, to);

    int k;
    for (k: from .. to) {
        printf("reversed_par[%d] = to_reverse[%d]\n", LENGTH - k - 1, k);
        reversed_par[LENGTH - k - 1] = to_reverse[k];
    }

    printf("proc[%d]: ended\n", n);
    done[n] = true;
}

init {
    printf("program start\n");
    // array initialization
    {
        int i;
        for (i in to_reverse) {
            int value;
            select(value: 0 .. R);
            to_reverse[i] = value;
            printf("to_reverse[%d]: %d\n", i, value);
        }
    }

    printf("sequential start\n");
    // SequentialReverser implementation
    {
        int k;
        for (k: 0 .. (LENGTH - 1)) {
            reversed_par[LENGTH - k - 1] = to_reverse[k];
            printf("reversed_seq[%d] = to_reverse[%d]\n", LENGTH - k - 1, k);
        }
        done[0] = true; // mark sequential end
    }
    printf("sequential end\n");

    printf("parallel start\n");
    // ParallelReverser implementation
    {
        int n;
        int s = LENGTH / N;
        
        // fork section
        for (n: 1 .. N) {
            int from = n * s;
            int to;
            if
            :: (n == N) -> to = LENGTH - 1;
            :: else -> to = n * s + s - 1; 
            fi
            run ThreadedReverser(from, to, n); // run as "thread n"
        }

        // join section
        for (n: 1 .. N) {
            (done[n] == true); // wait "thread n"
            printf("[%d] joined\n", n);
        }
    }
    printf("parallel end\n");

    // test if seq and parallel are the same
    {
        int i;
        for (i: 0 .. (LENGTH - 1)) {
            if
            :: (reversed_seq[i] != reversed_par[i]) -> seq_eq_to_parallel = false;
            fi
        }
    }
}

// ltl syntax: https://spinroot.com/spin/Man/ltl.html

ltl seq_eq_parallel {
    // the variable seq_eq_to_parallel will never be false if all the elements
    // between the sequential and parallel reversed arrays are equal
    (done[0] == false || done[N] == false) U (seq_eq_to_parallel == true)
}

ltl termination {
    // <> (done[0] == true for(`x', 1, N, ` && done[x] == true'))
    <> (done[0] == true && done[N] == true)
}

ltl correctness_seq {
    done[0] == true -> (true for(`k', 0, LENGTH-1, ` &&
        reversed_seq[eval(LENGTH - k - 1)] == to_reverse[k]'))
}