#include <mpi.h>

#include "../common.h"                                                        //

#include "divine.h"                                                           //
enum APs { rank_0_finished, rank_1_finished };                                //
LTL(finished_ok, F(rank_0_finished) && F(rank_1_finished));                   //

int main(void) {
    MPI_Init(NULL, NULL);

    int rank; MPI_Comm_rank(MPI_COMM_WORLD, &rank);

    MPI_Finalize();

    switch (rank) {
        case 0: AP(rank_0_finished); break;
        case 1: AP(rank_1_finished); break;
    }

    return 0;
}