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 
48 namespace ompl
49 {
50  namespace control
51  {
53 
54  OMPL_CLASS_FORWARD(Automaton);
56 
70  class Automaton
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
93 
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,
149  unsigned int maxDist = std::numeric_limits<unsigned int>::max()) const;
150 
152  static AutomatonPtr AcceptingAutomaton(unsigned int numProps);
153 
156  static AutomatonPtr CoverageAutomaton(unsigned int numProps, const std::vector<unsigned int> &covProps);
157 
160  static AutomatonPtr SequenceAutomaton(unsigned int numProps, const std::vector<unsigned int> &seqProps);
161 
164  static AutomatonPtr DisjunctionAutomaton(unsigned int numProps, const std::vector<unsigned int> &disjProps);
165 
168  static AutomatonPtr AvoidanceAutomaton(unsigned int numProps, const std::vector<unsigned int> &avoidProps);
169 
173  static AutomatonPtr CoverageAutomaton(unsigned int numProps);
174 
178  static AutomatonPtr SequenceAutomaton(unsigned int numProps);
179 
182  static AutomatonPtr DisjunctionAutomaton(unsigned int numProps);
183 
184  protected:
185  unsigned int numProps_;
186  unsigned int numStates_;
187  int startState_{-1};
188  std::vector<bool> accepting_;
189  std::vector<TransitionMap> transitions_;
190  mutable std::vector<unsigned int> distances_;
191  };
192  }
193 }
194 #endif
void print(std::ostream &out) const
Prints the automaton to a given output stream, in Graphviz dot format.
Definition: Automaton.cpp:241
unsigned int numTransitions() const
Returns the number of transitions in this automaton.
Definition: Automaton.cpp:228
void setAccepting(unsigned int s, bool a)
Sets the accepting status of a given state.
Definition: Automaton.cpp:173
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:211
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:261
unsigned int numProps() const
Returns the number of propositions used by this automaton.
Definition: Automaton.cpp:236
int getStartState() const
Returns the start state of the automaton. Returns -1 if no start state has been set.
Definition: Automaton.cpp:188
Automaton(unsigned int numProps, unsigned int numStates=0)
Creates an automaton with a given number of propositions and states.
Definition: Automaton.cpp:76
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:341
void setStartState(unsigned int s)
Sets the start state of the automaton.
Definition: Automaton.cpp:183
Main namespace. Contains everything in this library.
Definition: AppBase.h:21
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:364
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:58
Each automaton state has a transition map, which maps from a World to another automaton state...
Definition: Automaton.h:77
unsigned int addState(bool accepting=false)
Adds a new state to the automaton and returns an ID for it.
Definition: Automaton.cpp:163
void addTransition(unsigned int src, const World &w, unsigned int dest)
Adds a given transition to the automaton.
Definition: Automaton.cpp:193
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:297
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:307
bool isAccepting(unsigned int s) const
Returns whether a given state of the automaton is accepting.
Definition: Automaton.cpp:178
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:383
A class to represent a deterministic finite automaton, each edge of which corresponds to a World...
Definition: Automaton.h:70
unsigned int numStates() const
Returns the number of states in this automaton.
Definition: Automaton.cpp:223
TransitionMap & getTransitions(unsigned int src)
Returns the outgoing transition map for a given automaton state.
Definition: Automaton.cpp:218
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:199