Введение
В теоретической информатике, язык временных процессов (TPL) - это процесс расчета, который расширяет CCS Робина Милнера с понятием многосторонней синхронизации, что позволяет нескольким процессам синхронизироваться на глобальных "часах". Эти часы измеряют время, хотя и не конкретно, а скорее как абстрактный сигнал, который определяет, когда весь процесс может перейти к следующему шагу.
Неофициальное определение
TPL - это консервативное расширение CCS, с добавлением специального действия, называемого σ, представляющего прохождение времени процессом тикания абстрактных часов. Как и в CCS, TPL имеет префикс действия и может быть описан как терпеливый, то есть процесс будет бездейственно принимать тиканье часов, написанный как Ключ к использованию абстрактного времени - оператор тайм-аут, который представляет два процесса, один, чтобы вести себя так, как будто часы тикают, другой, чтобы вести себя так, как будто он не может, то есть при условии, что процесс E не препятствует тиканию часов. при условии, что E может выполнить действие a, чтобы стать E'. В TPL есть два способа предотвратить тиканье часов. Первый - через присутствие оператора ω, например, в процессе часов предотвращается тиканье. Можно сказать, что действие a является настойчивым, т.е. оно настаивает на действиях до того, как часы снова могут тикать. Второй способ, которым можно предотвратить тикинг, - это концепция максимального прогресса, которая гласит, что тихие действия (т.е. действия τ) всегда имеют приоритет над действиями σ и, таким образом, подавляют их. Таким образом, если два параллельных процесса способны синхронизироваться в данный момент, то часы не могут тикать. Таким образом, простой способ рассмотрения многосторонней синхронизации заключается в том, что группа составных процессов позволит времени пройти, если ни один из них не препятствует этому, т.е. система соглашается, что пришло время двигаться дальше.
Key to the use of abstract time is the timeout operator, which presents two processes, one to behave as if the clock ticks, one to behave as if it can't, i. e.
provided process E does not prevent the clock from ticking. provided E can perform action a to become E'. In TPL, there are two ways to prevent the clock from ticking. First is via the presence of the ω operator, for example in process the clock is prevented from ticking. It can be said that the action a is insistent, i. e. it insists on acting before the clock can tick again. The second way in which ticking can be prevented is via the concept of maximal progress, which states that silent actions (i. e. τ actions) always take precedence over and thus suppress σ actions. Thus is two parallel processes are capable of synchronizing at a given instant, it is not possible for the clock to tick. Thus a simple way of viewing multi party synchronization is that a group of composed processes will allow time to pass provided none of them prevent it, i. e. the system agrees that it is time to move on.
Синтаксис
Пусть a - это имя действия, не являющееся тихим, α - любое имя действия (включая τ, тихое действие) и является этикетка процесса, используемая для рекурсии.