soft-an04/ReversalModel/reversal_seq_eq_parallel_2_3_2.pml

/* 
m4 for loop definition


*/

int a[3]; // array to reverse
int r_s[3]; // for SequentialReverser: where the reverse is stored 
int r_p[3]; // for ParallelReverser: where the reverse is stored

// stores termination of each reverser
// index 0 is for the sequential algorithm
// indices 1-2 are for the ThreadedReverser instances
bool done[2 + 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 - 1)) {
        printf("r_p[%d] = a[%d]\n", 3 - k - 1, k);
        r_p[3 - k - 1] = a[k];
    }

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

// SequentialReverser implementation
proctype SequentialReverser() {
    int k;
    for (k: 0 .. (3 - 1)) {
        r_s[3 - k - 1] = a[k];
        printf("r_s[%d] = a[%d]\n", 3 - k - 1, k);
    }
    done[0] = true; // mark sequential end
}

// ParallelReverser implementation
proctype ParallelReverser() {
    int n;
    int s = 3 / 2;
    
    // fork section
    for (n: 0 .. (2 - 1)) {
        int from = n * s;
        int to;
        if
        :: (n == 2 - 1) -> to = 3;
        :: else -> to = n * s + s; 
        fi
        run ThreadedReverser(from, to, n + 1); // run as "thread n"
    }

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

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

    printf("sequential start\n");
    run SequentialReverser();

    printf("parallel start\n");
    run ParallelReverser();

    (done[0] == true && done[2] == true);

    // test if seq and parallel are the same
    {
        int i;
        for (i: 0 .. (3 - 1)) {
            if
            :: (r_s[i] != r_p[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
    [] (seq_eq_to_parallel == true)
}

ltl termination {
    // termination happens when the sequential reverser terminates
    // (done[0] is true) and the last process in the parallel reverser joins
    // (done[2] is true)
    <> (done[0] == true && done[2] == true)
}

// Due to avoid excessive parser complexity when checking the model
// with other ltl properties the correctness_seq is excluded by m4 from the 
// ProMeLa source when there is no need to check it
// 

// Similar exclusion logic is applied to correctness_par
//