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

pub struct HardPolicy {
    pub prop_vars: Vec<Condition>,
    pub expr: LTLModal,
    // some fields omitted
}
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.

Applies a next step to the LTL model

Undoes the last call to step

Reset the strucutre, such that no state exists.

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

Returns a copy of the value. Read more

Performs copy-assignment from source. Read more

Formats the value using the given formatter. Read more

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.