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