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 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 ...
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