问题描述
我正在模拟 Solution of a Problem in Concurrent Programming Control 中的 Dijkstra 算法。
虽然是 Promela 的新手（但熟悉 C），但我能够重新创建上面文章中的伪代码：
Page临界区应该只能由一个进程访问。但是，我的 /* Dijkstra's solution - promela model */
int k,b[2],c[2],critical_section;
active [2] proctype Dijkstra()
{
int j;
Li0: b[_pid] = 0;
Li1: if :: (k != _pid) ->
Li2: c[_pid] = 1;
Li3: if :: (b[k] == 1) ->
k = _pid;
goto Li1;
fi;
:: else ->
Li4: c[_pid] = 0;
for(j : 0 .. 1) {
if :: (j != _pid && !c[j]) ->
goto Li1;
fi;
}
fi;
critical_section = critical_section + 1;
assert(critical_section == 1);
printf("critial section: %u\n",critical_section)
critical_section = critical_section - 1;
c[_pid] = 1
b[_pid] = 1;
goto Li0;
}
从未到达。谁能发现我的错误？
解决方法
暂无找到可以解决该程序问题的有效方法，小编努力寻找整理中！
如果你已经找到好的解决方法，欢迎将解决方案带上本链接一起发送给小编。
小编邮箱:dio#foxmail.com (将#修改为@）