7.3 Согласование акторов процесса
Согласованием акторов процесса G называются действия,
осуществляемые для обеспечения согласованности акторов процесса.
Согласование акторов процесса необходимо для того,
чтобы обеспечить существование производных значений общих переменных этого процесса.
Согласование акторов включает:
1. сопоставление локальных значений общих переменных акторов процесса;
2. повторное доказательство акторов, нейтрализованных в ходе проведённого сопоставления локальных значений.
7.3.1 Сопоставление локальных значений
На первом этапе согласования акторов сопоставляются локальные значения общих переменных, соответствующие различным акторам процесса G.
Сопоставление локальных значений общих переменных осуществляется следующим образом:
1. Вычисляются фиксированные актуальные значения общих переменных процесса G.
2. Нейтрализуются все акторы процесса G, находящиеся в состоянии «доказанный», локальные значения которых не могут быть унифицированы с фиксированными актуальными значениями процесса.
Порядок нейтрализации акторов в языке не определён.
7.3.2 Исполнение повторных доказательств
После сопоставления локальных значений общих переменных
автоматически вызывается повторное доказательство всех нейтральных акторов процесса G,
за исключением акторов-представителей портов процесса.
Порядок исполнения повторных доказательств акторов в языке не определён.
Согласование акторов считается успешным в том и только в том случае, если завершаются успехом все повторные доказательства.
Примечание. В результате повторного доказательства недетерминированного актора, могут возникать новые точки выбора.
Содержание