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. More...

#include <ompl/control/planners/ltl/Automaton.h>

Classes
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\). More...

Public Member 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.

Static Public Member 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_

std::vector< unsigned int >	distances_

Detailed Description

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.

Definition at line 134 of file Automaton.h.

The documentation for this class was generated from the following files:

ompl/control/planners/ltl/Automaton.h
ompl/control/planners/ltl/src/Automaton.cpp

Classes

Public Member Functions

Static Public Member Functions

Protected Attributes

Detailed Description