Темпоральная логика
Темпоральная логика — это механизмы, которые задают момент, когда конечный автомат должен реагировать на определенные действия и задаются на переходах до/внутри условий и в состояниях:
На переходах до и внутри условий |
|
Внутри состояний вместе с оператором on |
Внутри состояний вместе с оператором 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
раз за одну секунду; -
ceil — округляет значение вверх до ближайшего целого числа. Например,
ceil(3.2)
вернет4
; -
floor — округляет значение вниз до ближайшего целого числа. Например,
floor(3.8)
вернет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 — функция, которая проверяет количество срабатываний блока Chart с момента активации состояния. Логика 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 раз, когда значение переменной |
ceil
ceil — функция для округления числовых значений вверх. Она возвращает ближайшее целое число, которое больше или равно заданному значению.
Синтаксис | Описание | Пример |
---|---|---|
|
Возвращает наименьшее целое число, большее или равное значению |
Возвращает |
|
Возвращает true, если округлённое вверх значение |
Переход будет активирован, когда округленное вверх значение |
floor
floor — функция для округления числовых значений вниз. Она возвращает ближайшее целое число, которое меньше или равно заданному значению.
Синтаксис | Описание | Пример |
---|---|---|
|
Возвращает наибольшее целое число, меньшее или равное значению |
Возвращает |
|
Возвращает true, если округлённое вниз значение |
Действие |