ompl::control::Automaton Class Reference

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.
 
TransitionMapgetTransitions (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, unsigned int maxDist=std::numeric_limits< unsigned int >::max()) 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_
 
std::vector< bool > accepting_
 
std::vector< TransitionMaptransitions_
 
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 69 of file Automaton.h.


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