Skip to content

Instantly share code, notes, and snippets.

@hatsugai
Created August 9, 2020 07:23
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save hatsugai/698675754d7af5b09940f606d3014144 to your computer and use it in GitHub Desktop.
Save hatsugai/698675754d7af5b09940f606d3014144 to your computer and use it in GitHub Desktop.
#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;
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment