| progr. | the source and target locations of these transitions will be obtained from the source and target locations of the original transition and the location from the other automaton | Исходные и целевые позиции таких переходов будут получены из исходных и целевых позиций рассматриваемого перехода и позиции второго автомата (см. Model Checking / Edmund M. Clarke, Jr., Orna Grumberg, and Doron A. Peled 1999) |