m_prod_cons_cv_non_atomic_wait.c

#include "ddsv.h"

#define NUM_PROCESSES 2

#define MAX_COUNT 1

typedef unsigned prop_t;     /* process id bit */

typedef struct shared_vars {
    int mutex;
    unsigned cond;
    int count;
} sv_t;

void print_sv(FILE *fp, const sv_t *p)
{
    fprintf(fp, "m=%d cv=%d c=%d", p->mutex, p->cond, p->count);
}

unsigned hash_sv(const sv_t *p)
{
    return (((p->mutex << 2) ^ p->cond) << 2) ^ p->count;
}

bool equal_sv(const sv_t *p, const sv_t *q)
{
    return p->mutex == q->mutex && p->cond == q->cond
        && p->count == q->count;
}

#include "ddsv.c"

bool guard_lock(prop_t prop, const sv_t *p)
{
    return p->mutex == 0;
}

void action_lock(prop_t prop, sv_t *q, const sv_t *p)
{
    q->mutex = 1;
}

void action_unlock(prop_t prop, sv_t *q, const sv_t *p)
{
    q->mutex = 0;
}

bool guard_not_empty(prop_t prop, const sv_t *p)
{
    return p->count > 0;
}

bool guard_not_full(prop_t prop, const sv_t *p)
{
    return p->count < MAX_COUNT;
}

bool guard_empty(prop_t prop, const sv_t *p)
{
    return p->count == 0;
}

bool guard_full(prop_t prop, const sv_t *p)
{
    return p->count == MAX_COUNT;
}

bool guard_ready(prop_t process_id_bit, const sv_t *p)
{
    return (p->cond & process_id_bit) == 0;
}

void action_wait(prop_t process_id_bit, sv_t *q, const sv_t *p)
{
    q->mutex = 0;
    q->cond = p->cond | process_id_bit;
}

void action_signal(prop_t process_id_bit, sv_t *q, const sv_t *p)
{
    /* turn off the right-most bit */
    q->cond = p->cond & (p->cond - 1);
}

void action_inc(prop_t i, sv_t *q, const sv_t *p)
{
    q->count = p->count + 1;
}

void action_dec(prop_t i, sv_t *q, const sv_t *p)
{
    q->count = p->count - 1;
}

process_trans_t P0[] = {
    { "lock", 1, &guard_lock, &action_lock },
    { NULL, -1, NULL, NULL },
};

process_trans_t P1[] = {
    { "unlock", 5, &guard_full, &action_unlock },
    { "produce", 3, &guard_not_full, &action_inc },
    { NULL, -1, NULL, NULL },
};

process_trans_t P2[] = {
    { "wakeup", 0, &guard_ready, &action_nop },
    { NULL, -1, NULL, NULL },
};

process_trans_t P3[] = {
    { "signal", 4, &guard_true, &action_signal },
    { NULL, -1, NULL, NULL },
};

process_trans_t P4[] = {
    { "unlock", 0, &guard_true, &action_unlock },
    { NULL, -1, NULL, NULL },
};

process_trans_t P5[] = {
    { "wait", 2, &guard_true, &action_wait },
    { NULL, -1, NULL, NULL },
};

process_trans_t *P_trans[] = { P0, P1, P2, P3, P4, P5, NULL };


process_trans_t Q0[] = {
    { "lock", 1, &guard_lock, &action_lock },
    { NULL, -1, NULL, NULL },
};

process_trans_t Q1[] = {
    { "unlock", 5, &guard_empty, &action_unlock },
    { "consume", 3, &guard_not_empty, &action_dec },
    { NULL, -1, NULL, NULL },
};

process_trans_t Q2[] = {
    { "wakeup", 0, &guard_ready, &action_nop },
    { NULL, -1, NULL, NULL },
};

process_trans_t Q3[] = {
    { "signal", 4, &guard_true, &action_signal },
    { NULL, -1, NULL, NULL },
};

process_trans_t Q4[] = {
    { "unlock", 0, &guard_true, &action_unlock },
    { NULL, -1, NULL, NULL },
};

process_trans_t Q5[] = {
    { "wait", 2, &guard_true, &action_wait },
    { NULL, -1, NULL, NULL },
};

process_trans_t *Q_trans[] = { Q0, Q1, Q2, Q3, Q4, Q5, NULL };

process_t P = { "P", 1, P_trans };    /* name, prop, trans */
process_t Q = { "Q", 2, Q_trans };

process_t *process_def[] = { &P, &Q };

int main()
{
    vis_process("m_prod_cons5_P", &P);
    vis_process("m_prod_cons5_Q", &Q);

    sv_t r = { 0, 0, 0 };
    state_t *s0 = make_initial_state(&r);
    lts_t *lts = concurrent_composition(process_def, s0);
    vis_lts("m_prod_cons5", lts);
    return 0;
}