Enum snowcap::hard_policies::LTLModal

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>),
}

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

impl Clone for LTLModal

fn clone(&self) -> LTLModal

Returns a copy of the value.

pub fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for LTLModal

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl LTLOperator for LTLModal

fn check(&self, history: &[Vec<bool>]) -> bool

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

fn partial(&self, history: &[Vec<bool>]) -> LTLResult

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

fn watch(&self, history: &[Vec<bool>]) -> Vec<usize>

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.

fn watch_partial(&self, history: &[Vec<bool>]) -> Vec<usize>

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

fn repr(&self) -> String

represent the operator as a string