Automaton.cpp
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 */
36 
37 #include "ompl/control/planners/ltl/Automaton.h"
38 #include "ompl/control/planners/ltl/World.h"
39 #include <boost/range/irange.hpp>
40 #include <unordered_map>
41 #include <unordered_set>
42 #include <boost/dynamic_bitset.hpp>
43 #include <ostream>
44 #include <limits>
45 #include <queue>
46 #include <vector>
47 
49 {
50  const auto d = entries.find(w);
51  if (d != entries.end())
52  return d->second;
53  for (const auto &entry : entries)
54  {
55  if (w.satisfies(entry.first))
56  {
57  // Since w satisfies another world that leads to d->second,
58  // we can add an edge directly from w to d->second.
59  entries[w] = entry.second;
60  return entry.second;
61  }
62  }
63  return -1;
64 }
65 
67  : numProps_(numProps)
68  , numStates_(numStates)
69  , accepting_(numStates_, false)
70  , transitions_(numStates_)
71  , distances_(numStates_, std::numeric_limits<unsigned int>::max())
72 {
73 }
74 
75 unsigned int ompl::control::Automaton::addState(bool accepting)
76 {
77  ++numStates_;
78  accepting_.resize(numStates_);
79  accepting_[numStates_ - 1] = accepting;
80  transitions_.resize(numStates_);
81  return numStates_ - 1;
82 }
83 
84 void ompl::control::Automaton::setAccepting(unsigned int s, bool a)
85 {
86  accepting_[s] = a;
87 }
88 
89 bool ompl::control::Automaton::isAccepting(unsigned int s) const
90 {
91  return accepting_[s];
92 }
93 
95 {
96  startState_ = s;
97 }
98 
100 {
101  return startState_;
102 }
103 
104 void ompl::control::Automaton::addTransition(unsigned int src, const World &w, unsigned int dest)
105 {
106  TransitionMap &map = transitions_[src];
107  map.entries[w] = dest;
108 }
109 
110 bool ompl::control::Automaton::run(const std::vector<World> &trace) const
111 {
112  int current = startState_;
113  for (const auto &w : trace)
114  {
115  current = step(current, w);
116  if (current == -1)
117  return false;
118  }
119  return true;
120 }
121 
122 int ompl::control::Automaton::step(int state, const World &w) const
123 {
124  if (state == -1)
125  return -1;
126  return transitions_[state].eval(w);
127 }
128 
130 {
131  return transitions_[src];
132 }
133 
135 {
136  return numStates_;
137 }
138 
140 {
141  unsigned int ntrans = 0;
142  for (const auto &transition : transitions_)
143  ntrans += transition.entries.size();
144  return ntrans;
145 }
146 
148 {
149  return numProps_;
150 }
151 
152 void ompl::control::Automaton::print(std::ostream &out) const
153 {
154  out << "digraph automaton {" << std::endl;
155  out << "rankdir=LR" << std::endl;
156  for (unsigned int i = 0; i < numStates_; ++i)
157  {
158  out << i << R"( [label=")" << i << R"(",shape=)";
159  out << (accepting_[i] ? "doublecircle" : "circle") << "]" << std::endl;
160 
161  for (const auto &e : transitions_[i].entries)
162  {
163  const World &w = e.first;
164  unsigned int dest = e.second;
165  const std::string formula = w.formula();
166  out << i << " -> " << dest << R"( [label=")" << formula << R"("])" << std::endl;
167  }
168  }
169  out << "}" << std::endl;
170 }
171 
172 unsigned int ompl::control::Automaton::distFromAccepting(unsigned int s, unsigned int maxDist) const
173 {
174  if (distances_[s] < std::numeric_limits<unsigned int>::max())
175  return distances_[s];
176  if (accepting_[s])
177  return 0;
178  std::queue<unsigned int> q;
179  std::unordered_set<unsigned int> processed;
180  std::unordered_map<unsigned int, unsigned int> distance;
181 
182  q.push(s);
183  distance[s] = 0;
184  processed.insert(s);
185 
186  while (!q.empty())
187  {
188  unsigned int current = q.front();
189  q.pop();
190  if (accepting_[current])
191  {
192  distances_[s] = distance[current];
193  return distance[current];
194  }
195  for (const auto &e : transitions_[current].entries)
196  {
197  unsigned int neighbor = e.second;
198  if (processed.count(neighbor) > 0)
199  continue;
200  q.push(neighbor);
201  processed.insert(neighbor);
202  distance[neighbor] = distance[current] + 1;
203  }
204  }
205  return std::numeric_limits<unsigned int>::max();
206 }
207 
209 {
210  auto phi(std::make_shared<Automaton>(numProps, 1));
211  World trivial(numProps);
212  phi->addTransition(0, trivial, 0);
213  phi->setStartState(0);
214  phi->setAccepting(0, true);
215  return phi;
216 }
217 
219  const std::vector<unsigned int> &covProps)
220 {
221  auto phi(std::make_shared<Automaton>(numProps, 1 << covProps.size()));
222  for (unsigned int src = 0; src < phi->numStates(); ++src)
223  {
224  const boost::dynamic_bitset<> state(covProps.size(), src);
225  World loop(numProps);
226  // each value of p is an index of a proposition in covProps
227  for (unsigned int p = 0; p < covProps.size(); ++p)
228  {
229  // if proposition covProps[p] has already been covered at state src, skip it
230  if (state[p])
231  continue;
232  // for each proposition covProps[p] that has not yet been
233  // covered at state src, construct a transition from src to (src|p)
234  // on formula (covProps[p]==true)
235  boost::dynamic_bitset<> target(state);
236  target[p] = true;
237  World nextProp(numProps);
238  nextProp[covProps[p]] = true;
239  phi->addTransition(src, nextProp, target.to_ulong());
240  // also build a loop from src to src on formula with conjunct (covProps[p]==false)
241  loop[covProps[p]] = false;
242  }
243  // now we add a loop from src to src on conjunction of (covProps[p]==false)
244  // for every p such that the pth bit of src is 1
245  phi->addTransition(src, loop, src);
246  }
247  phi->setAccepting(phi->numStates() - 1, true);
248  phi->setStartState(0);
249  return phi;
250 }
251 
253  const std::vector<unsigned int> &seqProps)
254 {
255  auto seq(std::make_shared<Automaton>(numProps, seqProps.size() + 1));
256  for (unsigned int state = 0; state < seqProps.size(); ++state)
257  {
258  // loop when next proposition in sequence is not satisfied
259  World loop(numProps);
260  loop[seqProps[state]] = false;
261  seq->addTransition(state, loop, state);
262 
263  // progress forward when next proposition in sequence is satisfied
264  World progress(numProps);
265  progress[seqProps[state]] = true;
266  seq->addTransition(state, progress, state + 1);
267  }
268  // loop on all input when in accepting state
269  seq->addTransition(seqProps.size(), World(numProps), seqProps.size());
270  seq->setAccepting(seqProps.size(), true);
271  seq->setStartState(0);
272  return seq;
273 }
274 
276  const std::vector<unsigned int> &disjProps)
277 {
278  auto disj(std::make_shared<Automaton>(numProps, 2));
279  World loop(numProps);
280  for (unsigned int disjProp : disjProps)
281  {
282  World satisfy(numProps);
283  satisfy[disjProp] = true;
284  loop[disjProp] = false;
285  disj->addTransition(0, satisfy, 1);
286  }
287  disj->addTransition(0, loop, 0);
288  disj->addTransition(1, World(numProps), 1);
289  disj->setAccepting(1, true);
290  disj->setStartState(0);
291  return disj;
292 }
293 
295  const std::vector<unsigned int> &avoidProps)
296 {
297  /* An avoidance automaton is simply a disjunction automaton with its acceptance condition flipped. */
298  AutomatonPtr avoid = DisjunctionAutomaton(numProps, avoidProps);
299  avoid->setAccepting(0, true);
300  avoid->setAccepting(1, false);
301  return avoid;
302 }
303 
305 {
306  const boost::integer_range<unsigned int> props = boost::irange(0u, numProps);
307  return CoverageAutomaton(numProps, std::vector<unsigned int>(props.begin(), props.end()));
308 }
309 
311 {
312  const boost::integer_range<unsigned int> props = boost::irange(0u, numProps);
313  return SequenceAutomaton(numProps, std::vector<unsigned int>(props.begin(), props.end()));
314 }
315 
317 {
318  const boost::integer_range<unsigned int> props = boost::irange(0u, numProps);
319  return DisjunctionAutomaton(numProps, std::vector<unsigned int>(props.begin(), props.end()));
320 }
void print(std::ostream &out) const
Prints the automaton to a given output stream, in Graphviz dot format.
Definition: Automaton.cpp:152
unsigned int numTransitions() const
Returns the number of transitions in this automaton.
Definition: Automaton.cpp:139
void setAccepting(unsigned int s, bool a)
Sets the accepting status of a given state.
Definition: Automaton.cpp:84
A class to represent an assignment of boolean values to propositions. A World can be partially restri...
Definition: World.h:71
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:122
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.
Definition: Automaton.cpp:172
STL namespace.
std::string formula() const
Returns a formatted string representation of this World, as a conjunction of literals.
Definition: World.cpp:77
unsigned int numProps() const
Returns the number of propositions used by this automaton.
Definition: Automaton.cpp:147
int getStartState() const
Returns the start state of the automaton. Returns -1 if no start state has been set.
Definition: Automaton.cpp:99
Automaton(unsigned int numProps, unsigned int numStates=0)
Creates an automaton with a given number of propositions and states.
Definition: Automaton.cpp:66
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:252
bool satisfies(const World &w) const
Returns whether this World propositionally satisfies a given World w. Specifically, returns true iff for every proposition p assigned in w, p is assigned in this World and this[p] == w[p].
Definition: World.cpp:65
void setStartState(unsigned int s)
Sets the start state of the automaton.
Definition: Automaton.cpp:94
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:275
int eval(const World &w) const
Returns the automaton state corresponding to a given World in this transition map. Returns -1 if no such transition exists.
Definition: Automaton.cpp:48
Each automaton state has a transition map, which maps from a World to another automaton state...
Definition: Automaton.h:76
unsigned int addState(bool accepting=false)
Adds a new state to the automaton and returns an ID for it.
Definition: Automaton.cpp:75
void addTransition(unsigned int src, const World &w, unsigned int dest)
Adds a given transition to the automaton.
Definition: Automaton.cpp:104
A shared pointer wrapper for ompl::control::Automaton.
static AutomatonPtr AcceptingAutomaton(unsigned int numProps)
Returns a single-state automaton that accepts on all inputs.
Definition: Automaton.cpp:208
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:218
bool isAccepting(unsigned int s) const
Returns whether a given state of the automaton is accepting.
Definition: Automaton.cpp:89
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:294
unsigned int numStates() const
Returns the number of states in this automaton.
Definition: Automaton.cpp:134
TransitionMap & getTransitions(unsigned int src)
Returns the outgoing transition map for a given automaton state.
Definition: Automaton.cpp:129
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:110