7.1 Акторы



Актором называется подцель доказательства, соответствующая акторному вызову предиката.

Актор Q называется «вложенным» по отношению к актору Р, если эти акторы принадлежат одному процессу, и доказательство актора Q, результаты которого в данный момент не отменены, происходит (произошло) в ходе доказательства актора Р.

Нейтрализацией актора называется отмена всех результатов его доказательства, за исключением результатов доказательства вложенных по отношению к нему акторов.

Повторным доказательством актора называется повторение доказательства актора с самого начала.

Актор может находиться в одном из трёх состояний:

1. «активный» актор;

2. «доказанный» актор;

3. «нейтральный» актор.

Актор Р, доказательство которого происходит (произошло) в ходе некоторой фазы F исполнения процесса G, считается (называется) «активным» с момента начала его доказательства до завершения рассматриваемой фазы F. В случае успешного завершения доказательства актора Р, а также успешного завершения фазы F, актор Р считается «доказанным» с момента завершения фазы F до его (возможной) нейтрализации на одной из последующих фаз исполнения процесса G.

Актор, предыдущее доказательство которого отменено, а повторное доказательство ещё не началось, называется «нейтральным». Перевод актора в активное состояние называется «активизацией» актора.



Содержание