Искусственный интеллект

202 9.7. Свойства живости (осуществимости) Пример. Условие отсутствия дедлока для программы вычисления биноминальных коэффициентов является следующим: N (0 < к <я) =>0{[(в месте (/,)л в_месте (тг) => (у4 > 0)1 л [(в_месте (/,)л л вместе (тс) з (у4 > 0)] л [(вместе (/с) л в_месте (/я3) => (у4 > 0)]}. Это условие учитывает тот факт, что при нахождении в (/,, /яэ) имеет место уч > 0 и один из процессов должен выполняться. Если один из процессов оказывается в терминальном месте, то другой не должен попасть в дедлок при выполнении команды занять. 9.7. Свойства живости (осуществимости) Эта категория свойств выражается общей формулой: Эта формула означает, что для каждого допустимого вычисления, если и», является изначально истинной, w2 должна в конце концов также стать истинной. В отличие от свойств инвариантности, которые описывают только сохранение желаемых свойств при переходах от одного места к другому, свойства живости говорят о том, что некоторые события в конце концов должны осуществиться. Эта формула в определенном смысле формулирует цель, которая обязательно должна быть достигнута после некоторого, в общем случае неизвестного, числа тактов.