Temporal logic operators

Temporal logic operators are mechanisms that specify the moment when a finite automaton must execute certain Julia language operators and are set at transitions before/inside conditions and in states:

condition action stateflow en

Where they are used

Example

On transitions, inside conditions, as well as inside actions specified in square brackets

condition action 1

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

Inside states together with a group of operators on or inside the Julia code

condition action 2

For example, using temporal logic operators and the on group of operators, you can change the values of variables over time.:

stateflow on after 1

Here:

en, du: y = x — when entering state A and while it is active, the variable y is assigned the value `x'. This action is performed immediately and repeated while the state is active.
on after(2.5, sec): y = 0 — if state A is active 2.5 or more seconds, then y becomes '0`.
on after(5, sec): y = -1 — if state A is active 5 or more seconds, then y becomes equal to -1.

The following temporal logic operators are available in Engee:

after — it is triggered after a set number of actions or time. For example, after(5, sec) activates the transition 5 seconds after the start of the current state;
at — it is triggered at a specific step. For example, at(10, tick) will be true in the step when the associated state has a group of during statements executed for the tenth time (starting counting from one);
before — remains true until a certain point in time or the number of clock cycles of the state machine is reached. For example, before(3, sec) is triggered until 3 seconds have passed since the activation of the associated state;
count — counts the number of times the status block has been executed since the boolean expression in the parameter became true. For example, the command on at(10, tick): y = count(true) will assign the value 10 to the variable y if the state is active during the 10 steps of the state machine.;
duration is an analog of the count operator, but instead of the number of steps, it returns the time during which the specified boolean expression remains true. For example, the command on after(10, sec): y = duration(true, sec)`will assign values to the variable `y that become greater than 10 if the state remains active after 10 seconds after activation;
elapsed, et — returns the time elapsed since entering the current state. For example, et >= 2 will be true if the state has been active for two or more seconds.;
every — is triggered after a set number of steps of the state machine, while the associated state remains active. For example, if the associated state is active for 10 steps, then on every(3, tick): y += 1 will increment the variable y by one three times consecutively.
t, getSimulationTime — returns the current simulation time. For example, t >= 10 will be true if the simulation time has reached 10 seconds.;
temporalCount is a counter that helps you keep track of how many steps the state machine has completed or how much time has passed while the state remained active. For example, calling temporalCount(tick) will show how many steps the state machine has been in this state. And using temporalCount(sec) will return how many seconds have passed since this state was activated.

`after`

after is an operator that implements temporal logic on transitions. It has two call options:

Syntax Description Example

Syntax	Description	Example
`after(n,tick)` `n` is a positive integer or expression. `tick' — the clock cycle of the state machine.	Returns `true` if the associated state remains active for at least `n` clock cycles since its activation. Otherwise, it returns `false'.	`after(3,tick)[x>3]` Exit from the current state when the block has been activated at least three times since the state became active, provided that `x > 3'.
`after(n,sec)` `after(n,msec)` `after(n,usec)` `n` is a positive real number or the result of calculating an expression. `sec' is a second. `msec' — millisecond. `usec' — microsecond.	Returns `true` if at least `n` time units have passed since the current state became active. Otherwise, it returns `false'.	`[after(1,tick) \|\| x > 5] after(10,tick)[x > 5] after(n, tick){y = 20;} after(2, sec)[x < 3]{y = 0;}` For a better understanding of the examples given, consider: `after(4,sec)[x > 10]` If the value of the variable `x` is greater than `10` and it has been `4` seconds since the transition began, then the value of the variable `y` increases by one.

after(n,tick)
n is a positive integer or expression.
`tick' — the clock cycle of the state machine.

Returns true if the associated state remains active for at least n clock cycles since its activation. Otherwise, it returns `false'.

after(3,tick)[x>3]

Exit from the current state when the block has been activated at least three times since the state became active, provided that `x > 3'.

after(n,sec) after(n,msec) after(n,usec)
n is a positive real number or the result of calculating an expression.
`sec' is a second.
`msec' — millisecond.
`usec' — microsecond.

Returns true if at least n time units have passed since the current state became active. Otherwise, it returns `false'.

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

after(10,tick)[x > 5]

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

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

For a better understanding of the examples given, consider:

after(4,sec)[x > 10]

If the value of the variable x is greater than 10 and it has been 4 seconds since the transition began, then the value of the variable y increases by one.

`at`

at is an operator that checks whether an action has occurred at a certain point in time. It has the following syntax:

Syntax Description Example

Syntax	Description	Example
`at(n, tick)` `n` is a positive integer or expression. `tick' — the clock cycle of the state machine.	Returns `true` if the associated state remains active for exactly `n` clock cycles from the moment of its activation. Otherwise, it returns `false'.	`at(5, tick)[y < 3]` For a better understanding of the examples given, consider: `at(4, tick) [x < 7] {y = 8}` If, during the execution of the 4th clock cycle from the moment of activation of the associated state, the value of the variable `x` turned out to be less than `7`, then the variable `y` will be assigned the value `8`.

at(n, tick)
n is a positive integer or expression.
`tick' — the clock cycle of the state machine.

Returns true if the associated state remains active for exactly n clock cycles from the moment of its activation. Otherwise, it returns `false'.

at(5, tick)[y < 3]

For a better understanding of the examples given, consider:

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

If, during the execution of the 4th clock cycle from the moment of activation of the associated state, the value of the variable x turned out to be less than 7, then the variable y will be assigned the value 8.

`before`

before is an operator that checks whether the action occurred before the specified time. It has the following syntax:

Syntax Description Example

Syntax	Description	Example
`before(n, sec)` `before(n, msec)` `before(n, usec)` `n` is a positive real number or the result of calculating an expression. `sec' is a second. `msec' — millisecond. `usec' — microsecond.	Returns `true` if less than `n` time units have passed since the current state became active. Otherwise, it returns `false'.	`before(3, sec)[x < 5]` The transition occurs if less than 3 seconds have passed since the activation of the state, provided that `x < 5`.
`before(n, tick)` `n` is a positive integer or expression. `tick' — the clock cycle of the state machine.	Returns `true` if the associated state remains active for less than `n` clock cycles from the moment of its activation. Otherwise, it returns `false'.	`before(4, tick)[y > 2] before(n, sec){z = 0;} before(1, msec)[x != 10]{y = 2;}` For a better understanding of the examples given, consider: `before(5, sec)[x >= 8]` The transition occurs if less than `5` seconds have passed since the activation of the state and the value of the variable `x` is greater than or equal to `8`.

before(n, sec) before(n, msec) before(n, usec)
n is a positive real number or the result of calculating an expression.
`sec' is a second.
`msec' — millisecond.
`usec' — microsecond.

Returns true if less than n time units have passed since the current state became active. Otherwise, it returns `false'.

before(3, sec)[x < 5]

The transition occurs if less than 3 seconds have passed since the activation of the state, provided that x < 5.

before(n, tick)
n is a positive integer or expression.
`tick' — the clock cycle of the state machine.

Returns true if the associated state remains active for less than n clock cycles from the moment of its activation. Otherwise, it returns `false'.

before(4, tick)[y > 2]

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

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

For a better understanding of the examples given, consider:

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

The transition occurs if less than 5 seconds have passed since the activation of the state and the value of the variable x is greater than or equal to 8.

`count`

count is an operator that counts the number of executions of the associated status block from the moment when the passed boolean expression became true. The count operator has the following syntax:

Syntax Description Example

Syntax	Description	Example
`count(condition)` `condition' is a boolean expression.	Returns the number of state machine clock cycles that have elapsed since the expression `n` became true, while the associated state remained active.	`[count(x > 2) = 3]` The transition occurs if the value of the variable `x` has remained more than two exactly `3` clock cycles since the activation of the associated state.

count(condition)
`condition' is a boolean expression.

Returns the number of state machine clock cycles that have elapsed since the expression n became true, while the associated state remained active.

[count(x > 2) = 3]

The transition occurs if the value of the variable x has remained more than two exactly 3 clock cycles since the activation of the associated state.

`duration`

duration is an operator that checks how long a certain condition remains true. The duration operator has the following syntax:

Syntax Description Example

Syntax	Description	Example
`duration(condition)` `condition' is a boolean expression that is tracked over time.	Returns the number of units of time that have elapsed since the `condition` became true. If the condition is false, it returns `0'.	`duration(x > 5) > 3` The transition occurs if more than `3` seconds have passed since `x` became more than `5`.

duration(condition)
`condition' is a boolean expression that is tracked over time.

Returns the number of units of time that have elapsed since the condition became true. If the condition is false, it returns `0'.

duration(x > 5) > 3

The transition occurs if more than 3 seconds have passed since x became more than 5.

`elapsed, et`

elapsed (et) is an operator that keeps track of how much time has passed since the state was activated. The elapsed operator has the following syntax:

Syntax Description Example

Syntax	Description	Example
`et(sec)` `et(msec)` `et(usec)` or `elapsed(sec)` `elapsed(msec)` `elapsed(usec)`	Returns the number of time units that have elapsed since the associated state became active.	`elapsed(sec) >= 3` The transition occurs if 3 or more seconds have passed since the activation of the state.

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

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

Returns the number of time units that have elapsed since the associated state became active.

elapsed(sec) >= 3

The transition occurs if 3 or more seconds have passed since the activation of the state.

`every`

every is an operator that helps you perform actions with a specified frequency. It has the following syntax:

Syntax Description Example

Syntax	Description	Example
`every(n, tick)` `n` is a positive integer or expression. `tick' — the clock cycle of the state machine.	Returns `true` if the number of clock cycles elapsed since the activation of the associated state is a multiple of `n'.	`every(3, tick)` For a better understanding of the examples given, consider: `every(4, tick)[a < 5]{b = 10}` If every fourth clock cycle since the activation of the associated state, the value of the variable `a` is less than `5`, then the value `10` is assigned to the variable `b`.

every(n, tick)
n is a positive integer or expression.
`tick' — the clock cycle of the state machine.

Returns true if the number of clock cycles elapsed since the activation of the associated state is a multiple of `n'.

every(3, tick)

For a better understanding of the examples given, consider:

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

If every fourth clock cycle since the activation of the associated state, the value of the variable a is less than 5, then the value 10 is assigned to the variable b.

`t, getSimulationTime`

t (getSimulationTime) is an operator that keeps track of the current simulation time. It has the following syntax:

Syntax Description Example

Syntax	Description	Example
`t` or `getSimulationTime`	Returns the time in seconds that has passed since the start of the simulation.	`t >= 5` The transition occurs if the current simulation time has reached 5 seconds or more.

t

getSimulationTime

Returns the time in seconds that has passed since the start of the simulation.

t >= 5

The transition occurs if the current simulation time has reached 5 seconds or more.

`temporalCount`

temporalCount is an operator that counts the number of clock cycles or the time elapsed since the activation of the associated state. The temporalCount operator has the following syntax:

Syntax Description Example

Syntax	Description	Example
`temporalCount(tick)`	Returns the number of state machine clock cycles that have elapsed since the associated state was activated.	`temporalCount(tick)`
`temporalCount(sec)` `temporalCount(msec)` `temporalCount(usec)`	Returns the number of specified time units that have elapsed since the associated state was activated.	`temporalCount(msec)` Returns the time elapsed since the associated state was activated, in milliseconds.

temporalCount(tick)

Returns the number of state machine clock cycles that have elapsed since the associated state was activated.

temporalCount(tick)

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

Returns the number of specified time units that have elapsed since the associated state was activated.

temporalCount(msec)

Returns the time elapsed since the associated state was activated, in milliseconds.

Temporal logic operators

after

at

before

count

duration

elapsed, et

every

t, getSimulationTime

temporalCount

Useful links

`after`

`at`

`before`

`count`

`duration`

`elapsed, et`

`every`

`t, getSimulationTime`

`temporalCount`