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
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:
 Watch $psi$ at every state before (not including where) $phi$ first holds.
 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:
 Watch $phi$ at every state before (and including where) $psi$ first holds.
 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
Auto Trait Implementations
impl RefUnwindSafe for LTLModal
impl UnwindSafe for LTLModal
Blanket Implementations
Mutably borrows from an owned value. Read more