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 TransitionMap &operator=(const TransitionMap &tm) = default;
85
86 mutable std::unordered_map<World, unsigned int> entries;
87 };
88
90 Automaton(unsigned int numProps, unsigned int numStates = 0);
91
92#if OMPL_HAVE_SPOT
97 Automaton(unsigned numProps, std::string formula, bool isCosafe = true);
98#endif
99
101 unsigned int addState(bool accepting = false);
102
104 void setAccepting(unsigned int s, bool a);
105
107 bool isAccepting(unsigned int s) const;
108
110 void setStartState(unsigned int s);
111
114 int getStartState() const;
115
117 void addTransition(unsigned int src, const World &w, unsigned int dest);
118
124 bool run(const std::vector<World> &trace) const;
125
129 int step(int state, const World &w) const;
130
132 TransitionMap &getTransitions(unsigned int src);
133
135 unsigned int numStates() const;
136
138 unsigned int numTransitions() const;
139
141 unsigned int numProps() const;
142
144 void print(std::ostream &out) const;
145
148 unsigned int distFromAccepting(unsigned int s) const;
149
151 static AutomatonPtr AcceptingAutomaton(unsigned int numProps);
152
155 static AutomatonPtr CoverageAutomaton(unsigned int numProps, const std::vector<unsigned int> &covProps);
156
159 static AutomatonPtr SequenceAutomaton(unsigned int numProps, const std::vector<unsigned int> &seqProps);
160
163 static AutomatonPtr DisjunctionAutomaton(unsigned int numProps, const std::vector<unsigned int> &disjProps);
164
167 static AutomatonPtr AvoidanceAutomaton(unsigned int numProps, const std::vector<unsigned int> &avoidProps);
168
172 static AutomatonPtr CoverageAutomaton(unsigned int numProps);
173
177 static AutomatonPtr SequenceAutomaton(unsigned int numProps);
178
181 static AutomatonPtr DisjunctionAutomaton(unsigned int numProps);
182
183 protected:
184 unsigned int numProps_;
185 unsigned int numStates_;
186 int startState_{-1};
187 std::vector<bool> accepting_;
188 std::vector<TransitionMap> transitions_;
189 mutable std::vector<unsigned int> distances_;
190 };
191 }
192}
193#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
Automaton(unsigned int numProps, unsigned int numStates=0)
Creates an automaton with a given number of propositions and states.
Definition: Automaton.cpp:75
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 ...
Definition: Automaton.cpp:382
unsigned int numTransitions() const
Returns the number of transitions in this automaton.
Definition: Automaton.cpp:227
unsigned int addState(bool accepting=false)
Adds a new state to the automaton and returns an ID for it.
Definition: Automaton.cpp:162
bool isAccepting(unsigned int s) const
Returns whether a given state of the automaton is accepting.
Definition: Automaton.cpp:177
void print(std::ostream &out) const
Prints the automaton to a given output stream, in Graphviz dot format.
Definition: Automaton.cpp:240
void setStartState(unsigned int s)
Sets the start state of the automaton.
Definition: Automaton.cpp:182
unsigned int numProps() const
Returns the number of propositions used by this automaton.
Definition: Automaton.cpp:235
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.
Definition: Automaton.cpp:306
static AutomatonPtr AcceptingAutomaton(unsigned int numProps)
Returns a single-state automaton that accepts on all inputs.
Definition: Automaton.cpp:296
TransitionMap & getTransitions(unsigned int src)
Returns the outgoing transition map for a given automaton state.
Definition: Automaton.cpp:217
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...
Definition: Automaton.cpp:210
int getStartState() const
Returns the start state of the automaton. Returns -1 if no start state has been set.
Definition: Automaton.cpp:187
void addTransition(unsigned int src, const World &w, unsigned int dest)
Adds a given transition to the automaton.
Definition: Automaton.cpp:192
unsigned int distFromAccepting(unsigned int s) const
Returns the shortest number of transitions from a given state to an accepting state.
Definition: Automaton.cpp:260
unsigned int numStates() const
Returns the number of states in this automaton.
Definition: Automaton.cpp:222
void setAccepting(unsigned int s, bool a)
Sets the accepting status of a given state.
Definition: Automaton.cpp:172
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.
Definition: Automaton.cpp:340
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...
Definition: Automaton.cpp:198
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...
Definition: Automaton.cpp:363
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