Документация Engee

Операторы темпоральной логики

Смотрите также:

Первые шаги в конечных автоматах
Логика работы конечных автоматов
Иерархия машины состояний

Операторы темпоральной логики — это механизмы, которые задают момент, когда конечный автомат должен выполнять определенные операторы языка Julia и задаются на переходах до/внутри условий и в состояниях:

condition action stateflow

Где используются

Пример

На переходах, внутри условий, а также внутри действий, указанных в квадратных скобках

сondition action 1

[
  if at(10, tick)
    y = 10
  end
]

Внутри состояний вместе с группой операторов on или внутри кода Julia

сondition action 2

Например, с помощью операторов темпоральной логики и группы операторов on можно изменять значения переменных во времени:

stateflow on after 1

Здесь:

  • 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, tick) будет истинно на шаге, когда у ассоциированного состояния группа операторов during будет выполняться в десятый раз (начиная счет с единицы);

  • before — остается истинным до достижения определенного момента времени или количества тактов машины состояний. Например, before(3, sec) срабатывает, пока не прошло 3 секунды с момента активации ассоциированного состояния;

  • count — подсчитывает, сколько раз блок состояния выполнялся с момента, когда логическое выражение в параметре стало истинным. Например, команда on at(10, tick): y = count(true) присвоит переменной y значение 10, если состояние будет активно в течение 10 шагов машины состояний.;

  • duration — является аналогом оператора count, но вместо количества шагов возвращает время, в течение которого указанное логическое выражение остается истинным. Например, команда on after(10, sec): y = duration(true, sec) будет присваивать переменной y значения, которые становятся больше 10, если состояние останется активным спустя 10 секунд после активации;

  • elapsed, et — возвращает время, прошедшее с момента входа в текущее состояние. Например, et >= 2 будет истинным, если состояние активно в течение двух или более секунд;

  • every — срабатывает через заданное количество шагов машины состояний, пока ассоциированное состояние остается активным. Например, если ассоциированное состояние будет активно 10 шагов, то on every(3, tick): y += 1 трижды последовательно увеличит переменную y на единицу.

  • t, getSimulationTime — возвращает текущее время симуляции. Например, t >= 10 будет истинным, если время симуляции достигло 10 секунд;

  • temporalCount — это счетчик, который помогает отслеживать, сколько шагов выполнила машина состояний или сколько времени прошло, пока состояние оставалось активным. Например, вызов temporalCount(tick) покажет, сколько шагов машина состояний находилась в этом состоянии. А использование temporalCount(sec) вернет, сколько секунд прошло с момента активации этого состояния.

after

after — оператор, который реализует темпоральную логику на переходах. Он имеет два варианта вызова:

Синтаксис Описание Пример

after(n,tick)
n — целое положительное число или выражение.
tick — такт работы конечного автомата.

Возвращает true, если ассоциированное состояние остается активным не менее n тактов с момента своей активации. В противном случае возвращает false.

 
after(3,tick)[x>3]

Выход из текущего состояния, когда блок активируется не менее трех раз с тех пор, как состояние стало активным, при условии, что x > 3.

after(n,sec) after(n,msec) after(n,usec)
n — положительное вещественное число или результат вычисления выражения.
sec — секунда.
msec — миллисекунда.
usec — микросекунда.

Возвращает true, если с момента, когда текущее состояние стало активным, прошло не менее n единиц времени. В противном случае возвращает false.

 
[after(1,tick) || x > 5]

after(10,tick)[x > 5]

after(n, tick){y = 20;}

after(2, sec)[x < 3]{y = 0;}

Для лучшего понимания приводимых примеров рассмотрим:

after(4,sec)[x > 10]

Eсли значение переменной x больше 10 и прошло 4 секунды после начала перехода, то значение переменной y увеличивается на единицу.

at

at — оператор, который проверяет, произошло ли действие в определенный момент времени. Он имеет следующий синтаксис:

Синтаксис Описание Пример

at(n, tick)
n — целое положительное число или выражение.
tick — такт работы конечного автомата.

Возвращает true, если ассоциированное состояние остается активным ровно n тактов с момента своей активации. В противном случае возвращает false.

 
at(5, tick)[y < 3]

Для лучшего понимания приводимых примеров рассмотрим:

at(4, tick) [x < 7] {y = 8}

Если во время выполнения 4-го такта с момента активации ассоциированного состояния значение переменной x оказалось меньше 7, то переменной y будет присвоено значение 8.

before

before — оператор, который проверяет, произошло ли действие до указанного момента времени. Он имеет следующий синтаксис:

Синтаксис Описание Пример

before(n, sec) before(n, msec) before(n, usec)
n — положительное вещественное число или результат вычисления выражения.
sec — секунда.
msec — миллисекунда.
usec — микросекунда.

Возвращает true, если прошло менее n единиц времени с момента, когда текущее состояние стало активным. В противном случае возвращает false.

 
before(3, sec)[x < 5]

Переход происходит, если прошло меньше 3 секунд с момента активации состояния, при условии, что x < 5.

before(n, tick)
n — целое положительное число или выражение.
tick — такт работы конечного автомата.

Возвращает true, если ассоциированное состояние остается активным менее n тактов с момента своей активации. В противном случае возвращает false.

 
before(4, tick)[y > 2]

before(n, sec){z = 0;}

before(1, msec)[x != 10]{y = 2;}

Для лучшего понимания приводимых примеров рассмотрим:

before(5, sec)[x >= 8]

Переход происходит, если прошло меньше 5 секунд с момента активации состояния и значение переменной x больше или равно 8.

count

count — оператор, которая подсчитывает количество выполнений ассоциированного блока состояния с момента, когда переданное логическое выражение стало истинным. Оператор сount имеет следующий синтаксис:

Синтаксис Описание Пример

count(condition)
condition — логическое выражение.

Возвращает количество тактов машины состояний, прошедших с тех пор, как выражение n стало истинным, в то время, как ассоциированное состояние оставалось активным.

 
[count(x > 2) = 3]

Переход происходит, если значение переменной x оставалась больше двух ровно 3 такта с момента активации ассоциированного состояния.

duration

duration — оператор, который проверяет, сколько времени остается истинным определенное условие. Оператор duration имеет следующий синтаксис:

Синтаксис Описание Пример

duration(condition)
condition — логическое выражение, которое отслеживается во времени.

Возвращает количество единиц времени, прошедшего с момента, когда condition стало истинным. Если условие ложно, то возвращает 0.

 
duration(x > 5) > 3

Переход происходит, если прошло более 3 секунд с момента, когда x стало больше 5.

elapsed, et

elapsed (et) — оператор, который отслеживает, сколько времени прошло с момента активации состояния. Оператор elapsed имеет следующий синтаксис:

Синтаксис Описание Пример

et(sec) et(msec) et(usec)

или

elapsed(sec) elapsed(msec) elapsed(usec)

Возвращает количество единиц времени, прошедших с момента, когда ассоциированное состояние стало активным.

 
elapsed(sec) >= 3

Переход происходит, если прошло 3 или более секунды с момента активации состояния.

every

every — оператор, который помогает выполнять действия с заданной периодичностью. Он имеет следующий синтаксис:

Синтаксис Описание Пример

every(n, tick)
n — целое положительное число или выражение.
tick — такт работы конечного автомата.

Возвращает true, если число тактов, прошедших с момента активации ассоциированного состояния, кратно n.

 
every(3, tick)

Для лучшего понимания приводимых примеров рассмотрим:

every(4, tick)[a < 5]{b = 10}

Если каждый четвертый такт с момента активации ассоциированного состояния значение переменной a оказывается меньше 5, то происходит присваивание переменной b значения 10.

t, getSimulationTime

t (getSimulationTime) — оператор, который отслеживает текущее время симуляции. Он имеет следующий синтаксис:

Синтаксис Описание Пример

t

или

getSimulationTime

Возвращает время в секундах, прошедшее с начала симуляции.

 
t >= 5

Переход происходит, если текущее время симуляции достигло 5 секунд или больше.

temporalCount

temporalCount — оператор, который подсчитывает количество тактов или время, прошедшее с момента активации ассоциированного состояния. Оператор temporalCount имеет следующий синтаксис:

Синтаксис Описание Пример

temporalCount(tick)

Возвращает количество тактов машины состояний, прошедших с момента активации ассоциированного состояния.

 
temporalCount(tick)

temporalCount(sec) temporalCount(msec) temporalCount(usec)

Возвращает количество заданных единиц времени, прошедших с момента активации ассоциированного состояния.

 
temporalCount(msec)

Возвращает время, прошедшее с момента активации ассоциированного состояния, в миллисекундах.

Полезные ссылки

  1. Chart

  2. Машины состояний

  3. Состояния

  4. Узлы

  5. Переходы