irafhy
Interval arithmetic based Reachability Analysis Framework for Hybrid Automaton
system.h
Go to the documentation of this file.
1 #ifndef REPRESENTATION_FORMAL_BASIC_SYSTEM_H
2 #define REPRESENTATION_FORMAL_BASIC_SYSTEM_H
3 
5 #include <capd/capdlib.h>
6 #include <vector>
7 #include <functional>
8 
9 namespace irafhy
10 {
11  class System
12  {
13  private:
17  std::vector<Formula> formulas_;
18 
19  private:
26  static std::function<void(capd::autodiff::Node,
27  capd::autodiff::Node[],
28  int,
29  capd::autodiff::Node[],
30  int,
31  capd::autodiff::Node[],
32  int)>
33  assign(const std::function<capd::autodiff::Node(
34  capd::autodiff::Node, capd::autodiff::Node[], int, capd::autodiff::Node[], int)>& f,
35  int index);
42  static std::function<void(capd::autodiff::Node,
43  capd::autodiff::Node[],
44  int,
45  capd::autodiff::Node[],
46  int,
47  capd::autodiff::Node[],
48  int)>
49  group(const std::function<void(capd::autodiff::Node,
50  capd::autodiff::Node[],
51  int,
52  capd::autodiff::Node[],
53  int,
54  capd::autodiff::Node[],
55  int)>& lhs,
56  const std::function<void(capd::autodiff::Node,
57  capd::autodiff::Node[],
58  int,
59  capd::autodiff::Node[],
60  int,
61  capd::autodiff::Node[],
62  int)>& rhs);
63 
64  public:
68  System() = default;
73  explicit System(const std::vector<Formula>& formulas);
77  ~System() = default;
82  [[nodiscard]] std::function<void(capd::autodiff::Node,
83  capd::autodiff::Node[],
84  int,
85  capd::autodiff::Node[],
86  int,
87  capd::autodiff::Node[],
88  int)>
89  odeSystem() const;
94  [[nodiscard]] bool empty() const;
98  void reverse() const;
105  friend std::ostream& operator<<(std::ostream& out, const System& rhs);
106  };
107 } // namespace irafhy
108 #endif //REPRESENTATION_FORMAL_BASIC_SYSTEM_H
std::vector< Formula > formulas_
formulas of the system whihc indicate the vector field
Definition: system.h:17
void reverse() const
reverse the direction of the vector field
Definition: system.cpp:72
std::function< void(capd::autodiff::Node, capd::autodiff::Node[], int, capd::autodiff::Node[], int, capd::autodiff::Node[], int)> odeSystem() const
get the arithmetic function of the current vector field
Definition: system.cpp:56
bool empty() const
check if the system is empty or not
Definition: system.cpp:70
static std::function< void(capd::autodiff::Node, capd::autodiff::Node[], int, capd::autodiff::Node[], int, capd::autodiff::Node[], int)> group(const std::function< void(capd::autodiff::Node, capd::autodiff::Node[], int, capd::autodiff::Node[], int, capd::autodiff::Node[], int)> &lhs, const std::function< void(capd::autodiff::Node, capd::autodiff::Node[], int, capd::autodiff::Node[], int, capd::autodiff::Node[], int)> &rhs)
group two functions
Definition: system.cpp:27
static std::function< void(capd::autodiff::Node, capd::autodiff::Node[], int, capd::autodiff::Node[], int, capd::autodiff::Node[], int)> assign(const std::function< capd::autodiff::Node(capd::autodiff::Node, capd::autodiff::Node[], int, capd::autodiff::Node[], int)> &f, int index)
construct an assign formula
Definition: system.cpp:9
Definition: condition.cpp:3
Definition: system.h:11
~System()=default
destructor
friend std::ostream & operator<<(std::ostream &out, const System &rhs)
out the given system to standard out stream
Definition: system.cpp:78
System()=default
constructor