You need a promela (SPIN) program that will start with an integer stack of 100 tokens.
It will then create two child processes that will remove 1 token at a time from the stack when they reach the critical section, and keep a local count of tokens that are removed.
The child processes will also randomly determine if a token is one of three categories: Sunny, Cloudy, and Rainy.
If they pop a token off the global stack and it is determined to be a Raniy token, it will not be counted in the local count of the process that popped it off.
In the end the processes will print to the screen a count of tokens they popped off. All of this must be done using Peterson's Mutex Algorithm.