Class ProductGraph::State

Defined in File ProductGraph.h

Nested Relationships

This class is a nested type of Class ProductGraph.

Class Documentation

class State

A State of a ProductGraph represents a vertex in the graph-based Cartesian product represented by the ProductGraph. A State is simply a tuple consisting of a PropositionalDecomposition region, a co-safe Automaton state, and a safe Automaton state.

Public Functions

State() = default: Creates a State without any assigned PropositionalDecomposition region or Automaton states. All of these values are initialized to -1.

State(const State &s) = default: Basic copy constructor for State.

bool operator==(const State &s) const: Returns whether this State is equivalent to a given State, by comparing their PropositionalDecomposition regions and Automaton states.

bool isValid() const: Returns whether this State is valid. A State is valid if and only if none of its Automaton states are dead states (a dead state has value -1).

int getDecompRegion() const: Returns this State’s PropositionalDecomposition region component.

int getCosafeState() const: Returns this State’s co-safe Automaton state component.

int getSafeState() const: Returns this State’s safe Automaton state component.

Friends

friend struct HashState

friend std::ostream &operator<<(std::ostream &out, const State &s): Helper function to print this State to a given output stream.