Операторы темпоральной логики
Операторы темпоральной логики — это механизмы, которые задают момент, когда конечный автомат должен выполнять определенные операторы языка Julia и задаются на переходах до/внутри условий и в состояниях:
Где используются |
Пример |
На переходах, внутри условий, а также внутри действий, указанных в квадратных скобках |
|
Внутри состояний вместе с группой операторов on или внутри кода Julia |
Например, с помощью операторов темпоральной логики и группы операторов on
можно изменять значения переменных во времени:
Здесь:
-
en, du: y = x
— при входе в состояние A и пока оно активно, переменнойy
присваивается значениеx
. Это действие выполняется сразу и повторяется, пока состояние активно. -
on after(2.5, sec): y = 0
— если состояние A активно2.5
или более секунд, тоy
становится равным0
. -
on after(5, sec): y = -1
— если состояние A активно5
или более секунд, тоy
становится равным-1
.
В Engee доступны следующие операторы темпоральной логики:
-
after — срабатывает после заданного количества действий или времени. Например,
after(5, sec)
активирует переход через5
секунд после начала текущего состояния; -
at — срабатывает в конкретный момент времени или при достижении определенного условия. Например,
at(10, sec)
активируется, когда прошли10
секунд с момента начала симуляции; -
before — используется для выполнения действия до достижения определенного момента времени или количества действий. Например,
before(3, sec)
срабатывает, пока не прошло3
секунды; -
count — подсчитывает, сколько раз ассоциированный блок состояния выполнялся с тех пор, как логическое выражение, переданное в качестве параметра, стало истинным. Например,
count(10)
активируется после десяти срабатываний; -
duration — проверяет, как долго система находится в определенном состоянии. Триггер срабатывает, если это время превышает заданное значение. Например,
duration > 5
активируется, если состояние сохраняется более5
секунд; -
elapsed, et — возвращает время, прошедшее с момента входа в текущее состояние. Например,
et >= 2
будет истинным, если состояние активно в течение двух или более секунд; -
every — срабатывает через регулярные промежутки времени. Например,
every(1, sec)
активируется каждую секунду. -
t, getSimulationTime — возвращает текущее время симуляции. Например,
t >= 10
будет истинным, если время симуляции достигло10
секунд; -
temporalCount — счетчик, который отслеживает количество раз, когда состояние было активным в течение заданного интервала времени. Например,
temporalCount(1, sec) > 3
активируется, если состояние было активным более3
раз за одну секунду;
after
after — функция, которая реализует темпоральную логику на переходах. Логика after имеет два варианта вызова:
Синтаксис | Описание | Пример |
---|---|---|
|
Возвращает true, если блок Chart включался не менее |
Выход из текущего состояния, когда блок активируется не менее трех раз с тех пор, как состояние стало активным, при условии, что |
|
Возвращает true, если с момента, когда текущее состояние стало активным, прошло не менее |
Для лучшего понимания приводимых примеров рассмотрим:
Eсли значение переменной |
at
at — функция, которая проверяет, произошло ли действие в определенный момент времени. Логика at имеет следующий синтаксис:
Синтаксис | Описание | Пример |
---|---|---|
|
Возвращает true, если прошло ровно |
Переход происходит, если прошло ровно 3 секунды с момента, когда состояние стало активным, при условии, что |
|
Возвращает true, если блок Chart активировался ровно |
Для лучшего понимания приводимых примеров рассмотрим:
Если прошло ровно 4 секунды после активации состояния и значение переменной |
before
before — функция, которая проверяет, произошло ли действие до указанного момента времени. Логика before имеет следующий синтаксис:
Синтаксис | Описание | Пример |
---|---|---|
|
Возвращает true, если прошло менее |
Переход происходит, если прошло меньше 3 секунд с момента активации состояния, при условии, что |
|
Возвращает true, если блок Chart активировался менее |
Для лучшего понимания приводимых примеров рассмотрим:
Если прошло меньше 5 секунд с момента активации состояния и значение переменной |
count
count — функция, которая подсчитывает количество выполнений ассоциированного блока состояния с момента, когда переданное логическое выражение стало истинным. Логика Count имеет следующий синтаксис:
Синтаксис | Описание | Пример |
---|---|---|
|
Возвращает true, если блок Chart активировался ровно |
Переход происходит, если блок Chart активировался ровно 3 раза с момента активации состояния, при условии, что |
|
Возвращает true, если количество активаций блока Chart с момента активации состояния равно |
Для лучшего понимания приводимых примеров рассмотрим:
Если блок Chart активировался ровно 4 раза с момента активации состояния и значение переменной |
duration
duration — функция, которая проверяет, сколько времени прошло с момента выполнения определенного условия. Логика duration имеет следующий синтаксис:
Синтаксис | Описание | Пример |
---|---|---|
|
Возвращает количество времени, прошедшего с момента, когда |
Переход происходит, если прошло более 3 секунд с момента, когда |
|
Возвращает true, если условие |
Для лучшего понимания приводимых примеров рассмотрим:
Если прошло более 4 секунд с момента, когда значение переменной |
elapsed, et
elapsed (et) — функция, которая отслеживает, сколько времени прошло с момента активации состояния. Логика elapsed имеет следующий синтаксис:
Синтаксис | Описание | Пример |
---|---|---|
|
Возвращает true, если прошло не менее |
Переход происходит, если прошло 3 или более секунды с момента активации состояния. |
|
Возвращает true, если прошло менее |
Для лучшего понимания приводимых примеров рассмотрим:
Если прошло 4 или более секунды с момента активации состояния и значение переменной |
every
every — функция, которая проверяет, выполняется ли действие с заданной периодичностью. Логика Every имеет следующий синтаксис:
Синтаксис | Описание | Пример |
---|---|---|
|
Возвращает true, если прошло ровно |
Переход происходит каждые 2 секунды, пока состояние активно. |
|
Возвращает true, если блок Chart активируется каждые |
Для лучшего понимания приводимых примеров рассмотрим:
Если каждые 4 секунды значение переменной |
t, getSimulationTime
t (getSimulationTime) — функция, которая отслеживает текущее время симуляции. Логика t имеет следующий синтаксис:
Синтаксис | Описание | Пример |
---|---|---|
|
Возвращает true, если текущее время симуляции больше или равно |
Переход происходит, если текущее время симуляции достигло 5 секунд или больше. |
|
Возвращает true, если текущее время симуляции меньше |
Для лучшего понимания приводимых примеров рассмотрим:
Если текущее время симуляции больше или равно 4 секундам и значение переменной |
temporalCount
temporalCount — функция, которая отслеживает количество раз, когда состояние было активировано за определенный период времени. Логика temporalCount имеет следующий синтаксис:
Синтаксис | Описание | Пример |
---|---|---|
|
Возвращает количество активаций состояния, когда условие |
Возвращает количество раз, когда состояние было активировано при условии, что |
|
Возвращает true, если состояние активировалось не менее |
Для лучшего понимания приводимых примеров рассмотрим:
Если состояние активировалось не менее 4 раз, когда значение переменной |