problem

[zhang-cell]

Dear author: I use the substitute keyword to analyze the mutex in case 6 lock (&count The mapping rules are as follows: Substitute c code{mutex lock(&count lock);} atomic { count lock == 0 -> count lock = 1 } Substitute c code{mutex unlock(&count lock);} count lock = 0 However, I found that atomic {count} was not generated in the generated Promela model lock == 0 -> count Lock = 1} and count lock = 0 Instead: C code { mutex lock((&( now.count Lock));}; and c code { mutex unlock((&( now.count lock))); }; Do you know what the problem is?

[nimble-code]

is it a problem? does the code verify correctly?

[zhang-cell]

This should be mapped to atomic {count lock == 0 -> count Lock = 1} and count_ lock = 0，instead of using c_code the default mapping method

[zhang-cell]

And in the manual under the mdoex file abp.prx The file defines two mapping tables. But only 'abprcv 'realizes mapping relation, 'abp snd' does not use the mapping relationship in the. PRX file, but uses the default mapping relationship. Why

[nimble-code]

ok

[zhang-cell]

Hello,does Promela contain operations to stop threads?

[nimble-code]

no it doesn't