这个 FSP 如何分隔两个 USER 路径？
How does this FSP seperate both USER paths?
RESOURCE = (acquire->continue->RESOURCE).
USER = (acquire->use->continue->USER).
||RESOURCE_SHARE = (a:USER || b:USER || {a,b}::RESOURCE).
a.USER和a.RESOURCE之间的共同行动continue如何确保a.USER路径不与b.USER路径交织在一起？例如，我的 LTSA 不允许以下跟踪，我不明白为什么不可以。
a.acquire->b.acquire->a.use->b.use->...
这种混淆是通过将其与以下 FSP/LTSA 进行比较而产生的。删除两个进程中的 continue 操作，我们剩下：
RESOURCE = (acquire->RESOURCE).
USER = (acquire->use->USER).
||RESOURCE_SHARE = (a:USER || b:USER || {a,b}::RESOURCE).
这个 FSP/LTSA 突然允许 USER 路径交织在一起，因为我们可以执行以下跟踪：
a.acquire->b.acquire->a.use->b.use->...
显然，添加 continue 会强制 USER 路径分开。为什么呢？
来源：
第一个 FSP 来自 Jeff Magee 和 Jeff Kramer 的书'Concurrency'。
我给老师发了一封邮件来帮助我。我会解释他：
There are three processes, two prefixes a and b of USER and
{a,b}::RESOURCE. The action 'acquire' from a.USER and b.USER merges
with {a,b}.acquire from {a,b}::RESOURCE. This also happens for
{a,b}.continue.
Therefore, in the first state there are two possible traces enabled: a.acquire OR b.acquire. Assume the action a.acquire is chosen. A transition occurs
and a.USER will only have the action a.use enabled, while
{a,b}::RESOURCE has two options enabled: {a,b}.continue.
Since a.continue is not yet enabled in a.USER, a.continue cannot occur
in {a,b}::RESOURCE. The only action left is for a.use to occur. In the
meantime, b.USER is still in the first state, and cannot run b.acquire
since {a,b}::RESOURCE only has {a,b}.continue enabled.
After the a.use transition, a.USER is now ready for the shared action
a.continue. Once this happens, all three processes are back to the
beginning state.
RESOURCE = (acquire->continue->RESOURCE).
USER = (acquire->use->continue->USER).
||RESOURCE_SHARE = (a:USER || b:USER || {a,b}::RESOURCE).
a.USER和a.RESOURCE之间的共同行动continue如何确保a.USER路径不与b.USER路径交织在一起？例如，我的 LTSA 不允许以下跟踪，我不明白为什么不可以。
a.acquire->b.acquire->a.use->b.use->...
这种混淆是通过将其与以下 FSP/LTSA 进行比较而产生的。删除两个进程中的 continue 操作，我们剩下：
RESOURCE = (acquire->RESOURCE).
USER = (acquire->use->USER).
||RESOURCE_SHARE = (a:USER || b:USER || {a,b}::RESOURCE).
这个 FSP/LTSA 突然允许 USER 路径交织在一起，因为我们可以执行以下跟踪：
a.acquire->b.acquire->a.use->b.use->...
显然，添加 continue 会强制 USER 路径分开。为什么呢？
来源： 第一个 FSP 来自 Jeff Magee 和 Jeff Kramer 的书'Concurrency'。
我给老师发了一封邮件来帮助我。我会解释他：
There are three processes, two prefixes a and b of USER and {a,b}::RESOURCE. The action 'acquire' from a.USER and b.USER merges with {a,b}.acquire from {a,b}::RESOURCE. This also happens for {a,b}.continue.
Therefore, in the first state there are two possible traces enabled: a.acquire OR b.acquire. Assume the action a.acquire is chosen. A transition occurs and a.USER will only have the action a.use enabled, while {a,b}::RESOURCE has two options enabled: {a,b}.continue.
Since a.continue is not yet enabled in a.USER, a.continue cannot occur in {a,b}::RESOURCE. The only action left is for a.use to occur. In the meantime, b.USER is still in the first state, and cannot run b.acquire since {a,b}::RESOURCE only has {a,b}.continue enabled.
After the a.use transition, a.USER is now ready for the shared action a.continue. Once this happens, all three processes are back to the beginning state.