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... | |
TransitionMap & | getTransitions (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< 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 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()
|
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()
|
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]
|
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]
|
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]
|
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]
|
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]
|
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]
|
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_
|
protected |
Definition at line 187 of file Automaton.h.
◆ distances_
|
mutableprotected |
Definition at line 189 of file Automaton.h.
◆ numProps_
|
protected |
Definition at line 184 of file Automaton.h.
◆ numStates_
|
protected |
Definition at line 185 of file Automaton.h.
◆ startState_
|
protected |
Definition at line 186 of file Automaton.h.
◆ transitions_
|
protected |
Definition at line 188 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