Class Automaton

Defined in File Automaton.h

Nested Relationships

Nested Types

Struct Automaton::TransitionMap

Class Documentation

class Automaton

A class to represent a deterministic finite automaton, each edge of which corresponds to a World. A system trajectory, by way of project() and worldAtRegion() in PropositionalDecomposition, determines a sequence of Worlds, which are read by an Automaton to determine whether a trajectory satisfies a given specification.

An automaton is meant to be run in a read-only fashion, i.e., it does not keep track of an internal state and can be thought of as a lookup table.

Public Functions

Automaton(unsigned int numProps, unsigned int numStates = 0): Creates an automaton with a given number of propositions and states.

unsigned int addState(bool accepting = false): Adds a new state to the automaton and returns an ID for it.

void setAccepting(unsigned int s, bool a): Sets the accepting status of a given state.

bool isAccepting(unsigned int s) const: Returns whether a given state of the automaton is accepting.

void setStartState(unsigned int s): Sets the start state of the automaton.

int getStartState() const: Returns the start state of the automaton. Returns -1 if no start state has been set.

void addTransition(unsigned int src, const World &w, unsigned int dest): Adds a given transition to the automaton.

bool run(const std::vector<World> &trace) const: Runs the automaton from its start state, using the values of propositions from a given sequence of Worlds. Returns false if and only if the result is a nonexistent state (i.e., if and only if there does not exist an extension to trace that will lead it to an accepting state).

int step(int state, const World &w) const: Runs the automaton for one step from the given state, using the values of propositions from a given World. Returns the resulting state, or -1 if the result is a nonexistent state.

TransitionMap &getTransitions(unsigned int src): Returns the outgoing transition map for a given automaton state.

unsigned int numStates() const: Returns the number of states in this automaton.

unsigned int numTransitions() const: Returns the number of transitions in this automaton.

unsigned int numProps() const: Returns the number of propositions used by this automaton.

void print(std::ostream &out) const: Prints the automaton to a given output stream, in Graphviz dot format.

unsigned int distFromAccepting(unsigned int s) const: Returns the shortest number of transitions from a given state to an accepting state.

Public Static Functions

static AutomatonPtr AcceptingAutomaton(unsigned int numProps): Returns a single-state automaton that accepts on all inputs.

static AutomatonPtr CoverageAutomaton(unsigned int numProps, const std::vector<unsigned int> &covProps): Helper function to return a coverage automaton. Assumes all propositions are mutually exclusive.

static AutomatonPtr SequenceAutomaton(unsigned int numProps, const std::vector<unsigned int> &seqProps): Helper function to return a sequence automaton. Assumes all propositions are mutually exclusive.

static AutomatonPtr DisjunctionAutomaton(unsigned int numProps, const std::vector<unsigned int> &disjProps): Helper function to return a disjunction automaton, which accepts when one of the given propositions becomes true.

static AutomatonPtr AvoidanceAutomaton(unsigned int numProps, const std::vector<unsigned int> &avoidProps): Returns an avoidance automaton, which rejects when any one of the given list of propositions becomes true. Accepts otherwise.

static AutomatonPtr CoverageAutomaton(unsigned int numProps): Helper function to return a coverage automaton over propositions from 0 to numProps-1. Assumes all propositions are mutually exclusive.

static AutomatonPtr SequenceAutomaton(unsigned int numProps): Helper function to return a sequence automaton over propositions from 0 to numProps-1, in that order. Assumes all propositions are mutually exclusive.

static AutomatonPtr DisjunctionAutomaton(unsigned int numProps): Helper function to return a disjunction automaton, which accepts when one of the given propositions in [0,numProps-1] becomes true.

Protected Attributes

unsigned int numProps_

unsigned int numStates_

int startState_ = {-1}

std::vector<bool> accepting_

std::vector<TransitionMap> transitions_

mutable std::vector<unsigned int> distances_

struct TransitionMap

Each automaton state has a transition map, which maps from a World to another automaton state. A set \(P\) of true propositions correponds to the formula \(\bigwedge_{p\in P} p\).

Public Functions

int eval(const World &w) const: Returns the automaton state corresponding to a given World in this transition map. Returns -1 if no such transition exists.

Public Members

mutable std::unordered_map<World, unsigned int> entries