代码之家 › 专栏 › 技术社区 › cwap

活跃性和进步性有什么区别?

lts

1

cwap · 技术社区 · 16 年前

我知道这是一个很学术的问题,但我希望这里有人能帮我找到答案。

我正在学习一个并发类,在这个类中我们使用LTS和FLTL。在我们的一个赋值中,有一个问题被给出:“举一个生动性属性的例子,用一个不能表示为进度属性的FLTL公式表示。” 只是澄清一下,我不想回答这个问题 .

我的问题是,我一直认为2是1),所以为了回答这个问题,我需要知道进展和活跃特性之间的区别。

如有任何帮助,我们将不胜感激:)

1 回复 | 直到 14 年前

1

thetrompf 16 年前

Liveness属性是指在定义该属性时,在将来的某个时候,程序将执行程序的给定部分。在FSP中,您可以将大多数Liveness属性定义为一个进度属性,但是在您的任务中,您必须想出一个示例,将Liveness属性表示为一个fltl,但不能将其作为一个进度属性。

您必须在fsp中查找fltl公式和progress属性的定义,以了解它们是如何不同的,然后想出一个示例,在其中导致fsp progress属性中的某些限制不能表示为一个限制。

更进一步,我只是读了一些关于它的内容,在fsp的progress属性中,您似乎无法描述“松散”的活跃性,例如,当动作“enter”发生时,可能会发生其他动作,但最终会发生“exit”动作。这不能描述为进度属性,因为您只能描述具体情况,例如“回车”和“退出”都会发生,并且在公平的假设下,它们都会无限频繁地发生,但在FLTL中可以说,[(回车-><>退出),这意味着当“回车”最终发生时,总会有发生“退出”。这是FSP和FLTL形式主义发展的巨大差异。