Enum snowcap::hard_policies::LTLModal[][src]

pub enum LTLModal {
    Now(Box<dyn LTLOperator>),
    Next(Box<dyn LTLOperator>),
    Finally(Box<dyn LTLOperator>),
    Globally(Box<dyn LTLOperator>),
    Until(Box<dyn LTLOperator>, Box<dyn LTLOperator>),
    Release(Box<dyn LTLOperator>, Box<dyn LTLOperator>),
    WeakUntil(Box<dyn LTLOperator>, Box<dyn LTLOperator>),
    StrongRelease(Box<dyn LTLOperator>, Box<dyn LTLOperator>),
}
Expand description

Temporal modal operators of LTL. For reconfiguration purpose, in the last state, we assume that nothing changes anymore, and every propositional variable does not change its state. See here

As an example, let $\phi_1$ be the policy that needs to be satisfied initially, and $\phi_2$ the policy that needs to be satisfied at the end. Additionally, we would like that we switch once from $\phi_1$ to $\phi_2$. This would be the following expression:

$$\phi_1\ \mathbf{U}\ \mathbf{G}\ \phi_2$$

Variants

Now(Box<dyn LTLOperator>)

$\phi$: $\phi$ holds at the current state.

Next(Box<dyn LTLOperator>)

$\mathbf{X}\ \phi$: $\phi$ holds at the next state. If the sequence is finished, then $\mathbf{X} \phi \iff \phi$ is identical to stating that $\phi$ holds now.

Finally(Box<dyn LTLOperator>)

$\mathbf{F}\ \phi$: $\phi$ needs to hold eventually (once)

Globally(Box<dyn LTLOperator>)

$\mathbf{G}\ \phi$: $\phi$ needs to hold in the current and every future state

Until(Box<dyn LTLOperator>, Box<dyn LTLOperator>)

$\psi\ \mathbf{U}\ \phi$: $\psi$ has to hold at least until (but not including the state where) $\phi$ becomes true. $\phi$ can hold at the current or a future position (once). Until then, $psi$ must be true. $\phi$ must hold eventually!

Release(Box<dyn LTLOperator>, Box<dyn LTLOperator>)

$\psi\ \mathbf{R}\ \phi$: $\phi$ has to hold until and including the point where $\psi$ first holds. If $\psi$ never holds, then $\phi$ must hold forever.

WeakUntil(Box<dyn LTLOperator>, Box<dyn LTLOperator>)

$\psi\ \mathbf{W}\ \phi$: $\psi$ has to hold at least at least util (but not including the state where) $\phi$ becomes true. If $\phi$ never holds, $\psi$ must hold forever.

StrongRelease(Box<dyn LTLOperator>, Box<dyn LTLOperator>)

$\psi\ \mathbf{M}\ \phi$: $\phi$ has to hold until and including the point where $\psi$ first holds. $\psi$ can hold now or at any future state, but $\psi$ must hold eventually!

Trait Implementations

Returns a copy of the value. Read more

Performs copy-assignment from source. Read more

Formats the value using the given formatter. Read more

Generate the watch of the operator at the current state. All operations and their behavior is explained:

  • Now: Simply generate the watch of the current history

  • Next: Generate the watch of the next step. if there exists no next step, then generate the watch of the current state.

  • Finally: Tis is anaolg to the Or boolean operation for computing the watch

  • Globally: This is analog to the And boolean operation for computing the watch.

  • Unitl($psi$, $phi$): If the expression is True, then create the union of all ways in which this expression can become false:

    1. Watch $psi$ at every state before (not including where) $phi$ first holds.
    2. Watch $phi$ at every point where $phi$ holds, while (but not including where) $psi$ is true

    If the expression is false, try all possible ways in which it can turn true. For this, we need to iterate over all possible cases how it might become true. This means, iterating over every position and trying to make it true. Since we build the union of this, this is the same as building the union over all watches of $psi$ and $phi$, where $psi$ or $phi$ are false.

  • Release($psi$, $phi$): If the expression is True, then create the union of all ways in which this expression can become false:

    1. Watch $phi$ at every state before (and including where) $psi$ first holds.
    2. If $phi$ does not hold forever, watch $psi$ at every point where $psi$ holds, while (and including where) $phi$ is true

    If the expression is false, try all possible ways in which it can turn true. For this, we need to iterate over all possible cases how it might become true. This means, iterating over every position and trying to make it true. Since we build the union of this, this is the same as building the union over all watches of $psi$ and $phi$, where $psi$ or $phi$ are false.

  • WeakUntil($psi$, $phi$): Here, we do exactly the same as for Until.

  • StrongRelease($psi$, $phi$): Here, we do exactly the same as for Release.

Here, we do the exact samething as for watch. However, if the result is undefined, then return an empty watch list.

Checks if the operator holds for the given history. For this, it is assumed that the sequence is finished! Read more

Checks if the operator holds for the given history, assuming that we have only a partial sequence. Read more

represent the operator as a string

Auto Trait Implementations

Blanket Implementations

Gets the TypeId of self. Read more

Immutably borrows from an owned value. Read more

Mutably borrows from an owned value. Read more

Performs the conversion.

Performs the conversion.

The resulting type after obtaining ownership.

Creates owned data from borrowed data, usually by cloning. Read more

🔬 This is a nightly-only experimental API. (toowned_clone_into)

recently added

Uses borrowed data to replace owned data, usually by cloning. Read more

The type returned in the event of a conversion error.

Performs the conversion.

The type returned in the event of a conversion error.

Performs the conversion.