Open Access
表2
部分函数节点到PROMELA模型的映射规则
| 编号 | 函数节点 | 映射到PROMELA的结果 |
| R20 | main | active proctype p_main() |
| R21 | 线程 | bool lck_p_线程名_ret; bool lck_p_线程名; chan ret_p_线程名=[1] of {pid}; chan req_cll_p_线程名=[1] of {pid}; chan exc_cll_p_线程名=[0] of {pid}; active proctype p_线程名() |
| R22 | pthread_ create | bool lck_p_函数名_ret; bool lck_p_函数名; chan ret_p_函数名=[1] of {pid}; chan req_cll_p_函数名=[1] of {pid}; chan exc_cll_p_函数名=[0] of {pid}; active proctype p_函数名() |
| thr_create | ||
| R23 | thr_suspend | bool suspended; suspended = 1; //挂起suspended = 0; //继续在进程声明后添加provided (!suspended) |
| thr_continue | ||
| R24 | pthread_ mutex_t |
int |
| R25 | mutex_lock | atomic {互斥变量名==0->互斥变量名=1} |
| mutex_unlock | 互斥变量名=0 | |
| pthread_ mutex_lock |
atomic{互斥变量名==0->互斥变量名=1} | |
| pthread_ mutex_unlock |
互斥变量名=0 |
Current usage metrics show cumulative count of Article Views (full-text article views including HTML views, PDF and ePub downloads, according to the available data) and Abstracts Views on Vision4Press platform.
Data correspond to usage on the plateform after 2015. The current usage metrics is available 48-96 hours after online publication and is updated daily on week days.
Initial download of the metrics may take a while.