Promela Timeout Question Hello, I am working with Promela (SPIN) and I am trying

Question

Promela Timeout Question

Hello, I am working with Promela (SPIN) and I am trying to get this code to decrement the token counter that starts at 100 all the way to 0. At 0 each process is supposed to print out how many times it decremented the counter less any tokens it decremented when (token count % 3 = 0). However, I am getting a timeout and it is not decrementing anything or counting the tokens it decrements. Could someone please read over my code and tell me what's going on?

//define 100 tokens
byte tres = 100;
bool flag[2] = false;
bool turn = 0;
byte count = 0;

/* flag is initialized to all false, */
/* and turn has the initial value 0 */
active [2] proctype peterson(){
pid i = _pid;
pid j = 1 - _pid;
byte num = 0;
/* Infinite loop */
again:
    /* [noncritical section] */
    if
    :: (tres == 0)->
    do
    :: printf("d", num);
    od
    goto end
    fi
    flag[i] = true;
    /* [trying section] */
    turn = i;
    (flag[j] == false || turn != i);
    count++;
    assert(count == 1);
    /* [critical section] */
    count--;
    /*Decrement tokens*/
    atomic{
       tres--;
    }
    /*Random enough for Rainy tokens*/
    /*if rainy, skip count*/
    if
    :: (tres % 3 == 0)-> goto skipp
    fi
    /*otherwise increment local count*/
    num++;
    skipp:
    flag[i] = false;
    goto again
    end:
}

Explanation / Answer

int rq_begin = 0, rq_end = 0;
int av_begin = 0, av_end = 0;

#define MAX_DUR 10
#define RQ_DUR 5

proctype Writer() {
do
:: (av_end < rq_end) -> av_end++;
if
:: (av_end - av_begin) > MAX_DUR -> av_begin = av_end - MAX_DUR;
:: else -> skip;
fi
printf("span: [%d,%d] ", av_begin, av_end);
od
}

proctype Reader()
{
do::d_step
{
rq_begin++;
rq_end = rq_begin + RQ_DUR;
}
printf("rqstd span: [%d,%d] ", rq_begin, rq_end);
(rq_begin >= av_begin && rq_end <= av_end);
printf("got rqstd span ");
od
}

init {
run Writer();
run Reader();
}

Related Questions

Navigate

• Browse (All)
• Browse P
• Subjects

Integrity-first tutoring: explanations and feedback only — we do not complete graded work. Learn more.