Spinroot
A forum for Spin users
You are not logged in.
- Topics: Active | Unanswered
#1 2011-11-06 20:56:04
- awesan
- Member
- Registered: 2011-04-30
- Posts: 45
allowing constant expression for number of processes in proctype
*****************
#define MAX_SEM_VAL 2
int sem = MAX_SEM_VAL;
active [MAX_SEM_VAL+1] proctype P()
{
end:
do
:: acq_sem(sem);
//progress:
rel_sem(sem);
od;
}
*****************
It would be nice, if SPIN allows constant expression that evaluates to an integer for the number of processes in proctype as above as a syntactic sugar. This would just make the model more expressive that the author thinks "maximum of counting semaphore + 1" number of processes is sufficient to verify the model. It is a different issue whether the author's thinking is correct or not, though it looks like it is true in this case to verify a counting semaphore model.
Offline
