В чем разница между активностью и активностью прогресса?

Question

Я знаю, что это очень академический вопрос, но я надеялся, что кто-то может помочь мне получить ответ.

Я беру класс параллелизма, в котором мы используем LTS'ы и FLTL. В одном из наших заданий задается вопрос: «Приведите пример свойства liveness, выраженного как формула FLTL, который не может быть выражен как свойство прогресса». Просто уточнить, я не хочу отвечать на этот вопрос.

Моя проблема в том, что я всегда думал о 2 как 1 :) Поэтому, чтобы ответить на вопрос, мне нужно знать разницу между свойствами прогресса и жизнеспособности.

Любая помощь будет принята с благодарностью :)

Answer 1

живучести свойство, когда вы определяя, что, в какой-то момент в будущем программа будет выполнять данную часть программы. В FSP вы можете определить большинство свойств liveness как свойство progress, но в вашем задании вам нужно придумать пример, в котором вы выражаете свойство liveness как FLTL, но вы не можете сделать это как свойство прогресса.

Вы должны найти определение формулы FLTL и свойство progress в FSP, чтобы увидеть, как они отличаются, а затем придумать пример, где вызванное некоторым ограничением свойство прогресса FSP не может выражаться как единое целое.

Кроме того, я просто немного прочитал об этом, и, кажется, en свойство прогресса FSP, вы не можете описать «рывковую» прочность, например, когда действие «войти» происходит, а затем некоторые другие действия может произойти, но в конечном итоге происходит действие «выхода». Это невозможно описать как свойство прогресса, потому что вы можете описать специфику, например, «войти» и «выйти», и при условии справедливости они будут возникать бесконечно часто, но в FLTL можно скажем, что [] (введите -> <> выход), это означает, что всегда, когда происходит «вступление», произойдет «выход». это большая разница в прогрессе в формальности FSP и FLTL.