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

Темпоральная логика

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

На переходах до и внутри условий

condition action stateflow

сondition action 1

Внутри состояний вместе с оператором on

с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, 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 имеет два варианта вызова:

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

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

Возвращает true, если блок Chart включался не менее 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 секунды после начала перехода, то происходит переход в следующее состояние.

at

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

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

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

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

at(3, sec)[x > 5]

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

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

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

at(5, tick)[y < 3]

at(n, sec){z = 10;}

at(2, msec)[x == 0]{y = 1;}

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

at(4, sec)[x < 7]

Если прошло ровно 4 секунды после активации состояния и значение переменной x меньше 7, то происходит переход в следующее состояние.

before

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, если блок Chart активировался менее 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 — функция, которая проверяет количество срабатываний блока Chart с момента активации состояния. Логика Count имеет следующий синтаксис:

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

count(n)
n — целое положительное число или выражение.

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

count(3)[x > 2]

Переход происходит, если блок Chart активировался ровно 3 раза с момента активации состояния, при условии, что x > 2.

count(n) == m
n — целое положительное число или выражение.
m — число, с которым сравнивается результат вызова count.

Возвращает true, если количество активаций блока Chart с момента активации состояния равно m.

count(5) == 4

count(2){y = 10;}

count(6)[z < 7]{x = 0;}

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

count(4)[x <= 5]

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

duration

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

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

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

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

duration(x > 5) > 3

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

duration(condition) >= n
n — положительное вещественное число или результат вычисления выражения.

Возвращает true, если условие condition было истинным в течение не менее n единиц времени.

duration(y < 10) >= 2

duration(x == 0){z = 1;}

duration(z > 7)[x != 3]{y = 5;}

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

duration(x < 8) > 4

Если прошло более 4 секунд с момента, когда значение переменной x стало меньше 8, то происходит переход в следующее состояние.

elapsed, et

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

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

et >= n
n — положительное вещественное число или выражение.

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

et >= 3

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

et < n
n — положительное вещественное число или выражение.

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

et < 2

et >= 5[y > 3]

et < 4{x = 10;}

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

et >= 4[x < 6]

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

every

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

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

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

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

every(2, sec)

Переход происходит каждые 2 секунды, пока состояние активно.

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

Возвращает true, если блок Chart активируется каждые n раз с момента активации состояния.

every(3, tick)

every(5, sec)[x > 2]

every(10, msec){y = 0;}

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

every(4, sec)[y < 5]

Если каждые 4 секунды значение переменной y меньше 5, то происходит переход в следующее состояние.

t, getSimulationTime

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

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

t >= n
n — положительное вещественное число или выражение.

Возвращает true, если текущее время симуляции больше или равно n единицам времени.

t >= 5

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

t < n
n — положительное вещественное число или выражение.

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

t < 10

t >= 3[x > 2]

t < 8{y = 15;}

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

t >= 4[x < 7]

Если текущее время симуляции больше или равно 4 секундам и значение переменной x меньше 7, то происходит переход в следующее состояние.

temporalCount

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

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

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

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

temporalCount(x > 5)

Возвращает количество раз, когда состояние было активировано при условии, что x больше 5.

temporalCount(condition) >= n
n — целое положительное число.

Возвращает true, если состояние активировалось не менее n раз, когда условие condition было истинным.

temporalCount(y < 10) >= 3

temporalCount(x == 0){z = 1;}

temporalCount(z > 7)[x != 3]{y = 5;}

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

temporalCount(x > 10) >= 4

Если состояние активировалось не менее 4 раз, когда значение переменной x больше 10, то происходит переход в следующее состояние.

ceil

ceil — функция для округления числовых значений вверх. Она возвращает ближайшее целое число, которое больше или равно заданному значению.

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

ceil(x) + x — вещественное число или выражение.

Возвращает наименьшее целое число, большее или равное значению x. Если x — уже целое число, возвращается оно же.

ceil(5.3)

Возвращает 6.

ceil(x) > n + n — целое число.

Возвращает true, если округлённое вверх значение x больше n, что может использоваться для контроля условий переходов.

[ceil(x) > 10]

Переход будет активирован, когда округленное вверх значение x больше 10.

floor

floor — функция для округления числовых значений вниз. Она возвращает ближайшее целое число, которое меньше или равно заданному значению.

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

floor(x) + x — вещественное число или выражение.

Возвращает наибольшее целое число, меньшее или равное значению x. Если x — уже целое число, возвращается оно же.

floor(4.8)

Возвращает 4.

floor(x) < n + n — целое число.

Возвращает true, если округлённое вниз значение x меньше n, что может использоваться для контроля условий переходов.

[floor(y) <= 5] {действие(); }

Действие () будет выполняться, если округленное вниз значение y меньше или равно 5.