# Struct snowcap::hard_policies::HardPolicy [−][src]

## Expand description

# Linear Temporal Logic

This structure holds the entire LTL expression. It is stored as a vector of propositional a history of which constraints were satisfied, and an expression which can check the property based on the history.

## Fields

`prop_vars: Vec<Condition>`

Conditional variables of the hard poicy

`expr: LTLModal`

LTL Expression

## Implementations

Helper function to generate the reachability policy

Create a new Linear Temporal Logic Hard Policy, where all conditions supplied need to be satisfied all the time.

Create a new Linear Temporal Logic Hard Policy. The LTL expression will have the following form, where $\phi_i$ are all propositional variables in the second argument, and $\psi_i$ are all from the third argument.

$$ \Big( \bigwedge \phi_i \Big) \ \mathbf{U}\ \mathbf{G}\ \Big( \bigwedge \psi_i \Big) $$

Create a new Linear Temporal Logic Hard Policy

Sets the total number of modifiers, if it was not yet set before. If it is already set, then
nothing will change. This function returns `true`

if there was no previous value.

#### pub fn step(

&mut self,

net: &mut Network,

state: &mut ForwardingState

) -> Result<(), NetworkError>

#### pub fn step(

&mut self,

net: &mut Network,

state: &mut ForwardingState

) -> Result<(), NetworkError>

Applies a next step to the LTL model

Computes the condition using Linear Temporal Logic, and returns if the expression holds. The
finish flag will be determined automatically if the number of calls to `step`

subtracted by
the number of calls to `undo`

(i.e., the length of the history) is equal to the number of
modifiers plus one (since the initial state will also be part of the history.) Finish will
be set to `false`

if the number of modifiers was not set yet.

Computes the condition using Linear Temporal Logic, and returns if the expression holds. The
provided `finish`

flag will be used to determine the method (`check`

vs `partial`

).

Compute the set of propositional variables that need to be watched in order to change the outcome of the current state of the checker. This function should only be used when the result is either false or undefined.

Compute the watch and get the last errors of the respective watch. This is a helpful utility for getting the errors, and comparing it later.

Compute the set of propositional variables that need to be watched in order to change the
outcome of the current state of the checker. This function should only be used when the
result is either false or undefined. The `finish`

flagg will be used to determine the method
(`watch`

or `watch_partial`

).

Returns the set of all errors of all propositional variables. It might be the case that these errors don’t necessarily contribute to the result of the last call to check.

Get the error associated with the watch provided to this method. The watch is an array containing the indices of all propositional variables which need to be considered. The resulting vector contains the error of the propositional variable, in the same order as provided. If a propositional variable is true, the error corresponding to this variable is None.

This method compares the current state of the checker with a previous state, which was
extracted using the method `get_watch_errors`

. This funciton returns `true`

if the errors
are the same, and `false`

if the errors are different. Only the errors from the watch are
compared.

Represent the LTL condition by a multiline string

## Trait Implementations

## Auto Trait Implementations

### impl RefUnwindSafe for HardPolicy

### impl Send for HardPolicy

### impl !Sync for HardPolicy

### impl Unpin for HardPolicy

### impl UnwindSafe for HardPolicy

## Blanket Implementations

Mutably borrows from an owned value. Read more