Loading...
Searching...
No Matches

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. More...
 
unsigned int addState (bool accepting=false)
 Adds a new state to the automaton and returns an ID for it. More...
 
void setAccepting (unsigned int s, bool a)
 Sets the accepting status of a given state. More...
 
bool isAccepting (unsigned int s) const
 Returns whether a given state of the automaton is accepting. More...
 
void setStartState (unsigned int s)
 Sets the start state of the automaton. More...
 
int getStartState () const
 Returns the start state of the automaton. Returns -1 if no start state has been set. More...
 
void addTransition (unsigned int src, const World &w, unsigned int dest)
 Adds a given transition to the automaton. More...
 
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). More...
 
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. More...
 
TransitionMapgetTransitions (unsigned int src)
 Returns the outgoing transition map for a given automaton state. More...
 
unsigned int numStates () const
 Returns the number of states in this automaton. More...
 
unsigned int numTransitions () const
 Returns the number of transitions in this automaton. More...
 
unsigned int numProps () const
 Returns the number of propositions used by this automaton. More...
 
void print (std::ostream &out) const
 Prints the automaton to a given output stream, in Graphviz dot format. More...
 
unsigned int distFromAccepting (unsigned int s) const
 Returns the shortest number of transitions from a given state to an accepting state. More...
 

Static Public Member Functions

static AutomatonPtr AcceptingAutomaton (unsigned int numProps)
 Returns a single-state automaton that accepts on all inputs. More...
 
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. More...
 
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. More...
 
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. More...
 
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. More...
 
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. More...
 
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. More...
 
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. More...
 

Protected Attributes

unsigned int numProps_
 
unsigned int numStates_
 
int startState_ {-1}
 
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 70 of file Automaton.h.

Constructor & Destructor Documentation

◆ Automaton()

ompl::control::Automaton::Automaton ( unsigned int  numProps,
unsigned int  numStates = 0 
)

Creates an automaton with a given number of propositions and states.

Definition at line 75 of file Automaton.cpp.

Member Function Documentation

◆ AcceptingAutomaton()

ompl::control::AutomatonPtr ompl::control::Automaton::AcceptingAutomaton ( unsigned int  numProps)
static

Returns a single-state automaton that accepts on all inputs.

Definition at line 296 of file Automaton.cpp.

◆ addState()

unsigned int ompl::control::Automaton::addState ( bool  accepting = false)

Adds a new state to the automaton and returns an ID for it.

Definition at line 162 of file Automaton.cpp.

◆ addTransition()

void ompl::control::Automaton::addTransition ( unsigned int  src,
const World w,
unsigned int  dest 
)

Adds a given transition to the automaton.

Definition at line 192 of file Automaton.cpp.

◆ AvoidanceAutomaton()

ompl::control::AutomatonPtr ompl::control::Automaton::AvoidanceAutomaton ( unsigned int  numProps,
const std::vector< unsigned int > &  avoidProps 
)
static

Returns an avoidance automaton, which rejects when any one of the given list of propositions becomes true. Accepts otherwise.

Definition at line 382 of file Automaton.cpp.

◆ CoverageAutomaton() [1/2]

ompl::control::AutomatonPtr ompl::control::Automaton::CoverageAutomaton ( unsigned int  numProps)
static

Helper function to return a coverage automaton over propositions from 0 to numProps-1. Assumes all propositions are mutually exclusive.

Definition at line 392 of file Automaton.cpp.

◆ CoverageAutomaton() [2/2]

ompl::control::AutomatonPtr ompl::control::Automaton::CoverageAutomaton ( unsigned int  numProps,
const std::vector< unsigned int > &  covProps 
)
static

Helper function to return a coverage automaton. Assumes all propositions are mutually exclusive.

Definition at line 306 of file Automaton.cpp.

◆ DisjunctionAutomaton() [1/2]

ompl::control::AutomatonPtr ompl::control::Automaton::DisjunctionAutomaton ( unsigned int  numProps)
static

Helper function to return a disjunction automaton, which accepts when one of the given propositions in [0,numProps-1] becomes true.

Definition at line 405 of file Automaton.cpp.

◆ DisjunctionAutomaton() [2/2]

ompl::control::AutomatonPtr ompl::control::Automaton::DisjunctionAutomaton ( unsigned int  numProps,
const std::vector< unsigned int > &  disjProps 
)
static

Helper function to return a disjunction automaton, which accepts when one of the given propositions becomes true.

Definition at line 363 of file Automaton.cpp.

◆ distFromAccepting()

unsigned int ompl::control::Automaton::distFromAccepting ( unsigned int  s) const

Returns the shortest number of transitions from a given state to an accepting state.

Definition at line 260 of file Automaton.cpp.

◆ getStartState()

int ompl::control::Automaton::getStartState ( ) const

Returns the start state of the automaton. Returns -1 if no start state has been set.

Definition at line 187 of file Automaton.cpp.

◆ getTransitions()

ompl::control::Automaton::TransitionMap & ompl::control::Automaton::getTransitions ( unsigned int  src)

Returns the outgoing transition map for a given automaton state.

Definition at line 217 of file Automaton.cpp.

◆ isAccepting()

bool ompl::control::Automaton::isAccepting ( unsigned int  s) const

Returns whether a given state of the automaton is accepting.

Definition at line 177 of file Automaton.cpp.

◆ numProps()

unsigned int ompl::control::Automaton::numProps ( ) const

Returns the number of propositions used by this automaton.

Definition at line 235 of file Automaton.cpp.

◆ numStates()

unsigned int ompl::control::Automaton::numStates ( ) const

Returns the number of states in this automaton.

Definition at line 222 of file Automaton.cpp.

◆ numTransitions()

unsigned int ompl::control::Automaton::numTransitions ( ) const

Returns the number of transitions in this automaton.

Definition at line 227 of file Automaton.cpp.

◆ print()

void ompl::control::Automaton::print ( std::ostream &  out) const

Prints the automaton to a given output stream, in Graphviz dot format.

Definition at line 240 of file Automaton.cpp.

◆ run()

bool ompl::control::Automaton::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).

Definition at line 198 of file Automaton.cpp.

◆ SequenceAutomaton() [1/2]

ompl::control::AutomatonPtr ompl::control::Automaton::SequenceAutomaton ( unsigned int  numProps)
static

Helper function to return a sequence automaton over propositions from 0 to numProps-1, in that order. Assumes all propositions are mutually exclusive.

Definition at line 399 of file Automaton.cpp.

◆ SequenceAutomaton() [2/2]

ompl::control::AutomatonPtr ompl::control::Automaton::SequenceAutomaton ( unsigned int  numProps,
const std::vector< unsigned int > &  seqProps 
)
static

Helper function to return a sequence automaton. Assumes all propositions are mutually exclusive.

Definition at line 340 of file Automaton.cpp.

◆ setAccepting()

void ompl::control::Automaton::setAccepting ( unsigned int  s,
bool  a 
)

Sets the accepting status of a given state.

Definition at line 172 of file Automaton.cpp.

◆ setStartState()

void ompl::control::Automaton::setStartState ( unsigned int  s)

Sets the start state of the automaton.

Definition at line 182 of file Automaton.cpp.

◆ step()

int ompl::control::Automaton::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.

Definition at line 210 of file Automaton.cpp.

Member Data Documentation

◆ accepting_

std::vector<bool> ompl::control::Automaton::accepting_
protected

Definition at line 187 of file Automaton.h.

◆ distances_

std::vector<unsigned int> ompl::control::Automaton::distances_
mutableprotected

Definition at line 189 of file Automaton.h.

◆ numProps_

unsigned int ompl::control::Automaton::numProps_
protected

Definition at line 184 of file Automaton.h.

◆ numStates_

unsigned int ompl::control::Automaton::numStates_
protected

Definition at line 185 of file Automaton.h.

◆ startState_

int ompl::control::Automaton::startState_ {-1}
protected

Definition at line 186 of file Automaton.h.

◆ transitions_

std::vector<TransitionMap> ompl::control::Automaton::transitions_
protected

Definition at line 188 of file Automaton.h.


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