Loading...
Searching...
No Matches
Automaton.h
1/*********************************************************************
2* Software License Agreement (BSD License)
3*
4* Copyright (c) 2012, Rice University
5* All rights reserved.
6*
7* Redistribution and use in source and binary forms, with or without
8* modification, are permitted provided that the following conditions
9* are met:
10*
11* * Redistributions of source code must retain the above copyright
12* notice, this list of conditions and the following disclaimer.
13* * Redistributions in binary form must reproduce the above
14* copyright notice, this list of conditions and the following
15* disclaimer in the documentation and/or other materials provided
16* with the distribution.
17* * Neither the name of the Rice University nor the names of its
18* contributors may be used to endorse or promote products derived
19* from this software without specific prior written permission.
20*
21* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
22* "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
23* LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
24* FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
25* COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
26* INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
27* BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
28* LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
29* CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
30* LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
31* ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
32* POSSIBILITY OF SUCH DAMAGE.
33*********************************************************************/
34
35/* Author: Matt Maly, Keliang He */
36
37#ifndef OMPL_CONTROL_PLANNERS_LTL_AUTOMATON_
38#define OMPL_CONTROL_PLANNERS_LTL_AUTOMATON_
39
40#include "ompl/control/planners/ltl/World.h"
41#include "ompl/util/ClassForward.h"
42#include "ompl/config.h"
43#include <unordered_map>
44#include <limits>
45#include <ostream>
46#include <vector>
47
48namespace ompl
49{
50 namespace control
51 {
53
54 OMPL_CLASS_FORWARD(Automaton);
56
71 {
72 public:
78 {
82 int eval(const World &w) const;
83
84 mutable std::unordered_map<World, unsigned int> entries;
85 };
86
88 Automaton(unsigned int numProps, unsigned int numStates = 0);
89
90#if OMPL_HAVE_SPOT
95 Automaton(unsigned numProps, std::string formula, bool isCosafe = true);
96#endif
97
99 unsigned int addState(bool accepting = false);
100
102 void setAccepting(unsigned int s, bool a);
103
105 bool isAccepting(unsigned int s) const;
106
108 void setStartState(unsigned int s);
109
112 int getStartState() const;
113
115 void addTransition(unsigned int src, const World &w, unsigned int dest);
116
122 bool run(const std::vector<World> &trace) const;
123
127 int step(int state, const World &w) const;
128
130 TransitionMap &getTransitions(unsigned int src);
131
133 unsigned int numStates() const;
134
136 unsigned int numTransitions() const;
137
139 unsigned int numProps() const;
140
142 void print(std::ostream &out) const;
143
146 unsigned int distFromAccepting(unsigned int s) const;
147
149 static AutomatonPtr AcceptingAutomaton(unsigned int numProps);
150
153 static AutomatonPtr CoverageAutomaton(unsigned int numProps, const std::vector<unsigned int> &covProps);
154
157 static AutomatonPtr SequenceAutomaton(unsigned int numProps, const std::vector<unsigned int> &seqProps);
158
161 static AutomatonPtr DisjunctionAutomaton(unsigned int numProps, const std::vector<unsigned int> &disjProps);
162
165 static AutomatonPtr AvoidanceAutomaton(unsigned int numProps, const std::vector<unsigned int> &avoidProps);
166
170 static AutomatonPtr CoverageAutomaton(unsigned int numProps);
171
175 static AutomatonPtr SequenceAutomaton(unsigned int numProps);
176
179 static AutomatonPtr DisjunctionAutomaton(unsigned int numProps);
180
181 protected:
182 unsigned int numProps_;
183 unsigned int numStates_;
184 int startState_{-1};
185 std::vector<bool> accepting_;
186 std::vector<TransitionMap> transitions_;
187 mutable std::vector<unsigned int> distances_;
188 };
189 }
190}
191#endif
A shared pointer wrapper for ompl::control::Automaton.
A class to represent a deterministic finite automaton, each edge of which corresponds to a World....
Definition Automaton.h:71
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 ...
unsigned int numTransitions() const
Returns the number of transitions in this automaton.
unsigned int addState(bool accepting=false)
Adds a new state to the automaton and returns an ID for it.
bool isAccepting(unsigned int s) const
Returns whether a given state of the automaton is accepting.
void print(std::ostream &out) const
Prints the automaton to a given output stream, in Graphviz dot format.
void setStartState(unsigned int s)
Sets the start state of the automaton.
unsigned int numProps() const
Returns the number of propositions used by this automaton.
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 AcceptingAutomaton(unsigned int numProps)
Returns a single-state automaton that accepts on all inputs.
TransitionMap & getTransitions(unsigned int src)
Returns the outgoing transition map for a given automaton 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 W...
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.
unsigned int distFromAccepting(unsigned int s) const
Returns the shortest number of transitions from a given state to an accepting state.
unsigned int numStates() const
Returns the number of states in this automaton.
void setAccepting(unsigned int s, bool a)
Sets the accepting status of a given state.
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.
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 Wo...
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 b...
A class to represent an assignment of boolean values to propositions. A World can be partially restri...
Definition World.h:72
Main namespace. Contains everything in this library.
Each automaton state has a transition map, which maps from a World to another automaton state....
Definition Automaton.h:78
int eval(const World &w) const
Returns the automaton state corresponding to a given World in this transition map....
Definition Automaton.cpp:57