Topology generation for UAV designs using Pacti¶
We demonstrate how pacti can be utilized to generate designs for Unmanned Aerial Vehicles (UAVs) under a set of predefined "design rules". Our primary objective is to produce a 3D grid, consisting of interconnected points that represent the abstract topology of the UAV. Each point within the grid represents a specific component of the UAV, such as fuselage, wing, rotor, etc., while each edge between two points depicts the connection among components. To achieve this, we employ a context-sensitive grammar (CSG) that formalizes the placement of UAV components on the grid based on their local context, i.e., the components around them.
Our grammar's primary goal is to generate all legal configurations of components and their connections within the 3D grid. A context-sensitive grammar (CSG) is a formal grammar that describes a formal language through a set of rules that define how strings of symbols within the language can be generated.
In the following, we introduce the main building blocks of our grammar: grid, context, symbols, and rules. By leveraging these components, our proposed method generates UAV designs that adhere to predefined design rules, resulting in functional and efficient UAV designs.
Grid¶
A 3D grid of points, or simply a grid, can be formally defined as a set of ordered triplets, where each triplet represents a point in 3D space. The triplet is composed of three integer coordinates \((x, y, z)\) that specify the position of the point in the 3D grid. Let \(n_{half} \in \mathbb{Z}\), and let \(G = \{(x, y, z) | x, y, z \in \mathbb{Z}, -n_{half} \leq x, y, z \leq n_{half}\}\) be the set of all points in a 3D grid. We define the size of a grid \(G\) as \(|G| = ((n_{half} * 2) + 1)^3\).
Below, we present an example of a grid of size 27, and we highlight the middle point of the grid, which has coordinates \((0,0,0)\):
Using the defined grid structure, we can easily specify the position of each component of the UAV in the form of a 3D point. This facilitates the use of a context-sensitive grammar to formalize the placement of components on the grid.
Context¶
Given a 3D grid of points, we define the context of a point \(p\) as a tuple of seven points, where six points are the coordinates of the adjacent points in the grid and one point is \(p\) itself. We define a set of seven directions \(\Delta = (\texttt{ego}, \texttt{front}, \texttt{rear}, \texttt{left}, \texttt{right}, \texttt{top}, \texttt{bottom})\). Given a point \(p = (x, y, z)\), we can construct its context \(Ctx(p) = (p_\texttt{ego}, p_\texttt{front}, p_\texttt{rear}, p_\texttt{left}, p_\texttt{right}, p_\texttt{top}, p_{bottom})\) as follows:
Below we show an example of a grid together with context of the point \((0,0,0)\)
Note that the points at the edge of the grid have contexts with some points having coordinates outside the grid, i.e., the points adjacent to them in the specified direction are not included in the grid. The context of a point is used to define the placement of components of an UAV in the grid according to their local context.
Symbols¶
In our grammar, each point \(p\) in the grid is associated with a symbol, denoted by \(Sym(p)\). The symbols are divided into two main categories: terminal symbols and nonterminal symbols. Terminal symbols represent actual characters or words in the language that the grammar defines, while nonterminal symbols are used to represent groups or structures in the language. These symbols can be expanded or rewritten by the production rules of the grammar to generate strings in the language.
We define the set of terminal symbols as \(\Lambda\), which contains five elements that mostly represent UAV components: \({\texttt{Fuselage}, \texttt{Rotor}, \texttt{Wing}, \texttt{Connector}, \texttt{Empty}}\). We define the set of nonterminal symbols as \(\Theta\), which contains one element: \({\texttt{Unoccupied}}\).
Note that although \(\texttt{Empty}\) and \(\texttt{Unoccupied}\) represent the same concept (i.e., the absence of a component), they are different symbols. \(\texttt{Empty}\) is terminal, meaning it cannot be expanded into a new symbol, while \(\texttt{Unoccupied}\) is nonterminal.
At initialization, all points in the grid are associated with the \(\texttt{Unoccupied}\) symbol.
We associate each symbol with a color, as shown in the figure below:
Local Context¶
A local context \(LC=(sym_1, sym_2, \dots, sym_7)\) is a tuple of seven symbols, i.e. \(l_c \in \Lambda \cup \Theta\), one for each direction in \(\Delta\). The figure below shows a local context \(LC_i\) = (\(\texttt{Unoccupied}\), \(\texttt{Unoccupied}\), \(\texttt{Unoccupied}\), \(\texttt{Fuselage}\), \(\texttt{Unoccupied}\), \(\texttt{Rotor}\), \(\texttt{Unoccupied}\)).
State¶
The state of a point \(p\) on a grid is the local context around that point, denoted by \(S(p)\).
For example, given the grid depicted below, let us consider the point \(p=(0,0,0)\). We have that \(S(p)=(\texttt{Fuselage}, \texttt{Unoccupied}, \texttt{Unoccupied}, \texttt{Wing}, \texttt{Wing}, \texttt{Rotor}, \texttt{Unoccupied})\). In the picture below, we have associated a color with each symbol.
Please see grid.py for the implementation of the grid and local context.
Rules¶
In our grammar a production rule, or rule, defines how a single nonterminal symbol can be substituted with a non-terminal symbol according to its context.
In our grammar, a production rule, or simply a rule, defines how a single nonterminal symbol can be substituted with another non-terminal symbol based on its context.
A rule \(R_i = (\Omega, \Pi)\) consists of a condition \(\Omega\) and a production \(\Pi\), where:
- \(\Omega=\{LC_0, LC_1, ..., LC_c\}\) is a set of \(c\) local contexts.
- \(\Pi = (sym, \texttt{dir})\) where \(sym \in \Lambda\) and \(\texttt{dir} \in \Delta\).
The condition \(\Omega\) determines all the local contexts where the rule can be applied. The production \(\Pi\) specifies the nonterminal symbol \(sym \in Tau\) to be produced and the direction of the edge that connects the newly generated symbol to one of the adjacent symbols in the grid. If no connection is required, then \(\texttt{dir}\) is simply \(\texttt{ego}\).
Matching¶
At each time step, we apply a rule to a point in the grid. A rule \(R_i\) matches with a point \(p\) if the local context of \(p\), i.e. \(S(p)\), is a subset of the conditions of \(R_i\), i.e. if \(S(p) \subseteq \Omega\). If a rule \(R_i = (\Omega, \Pi)\) matches with a point \(p\), then the production \(\Pi\) is applied to the point \(p\). That is, let \(\Pi=(sym, p_{dir})\), then the symbol \(sym\) is placed in \(p\), i.e. \(Sym(p)=sym\), and an edge is created from \(p\) to \(p_{dir}\). The figure below shows an example of a grid at a time step \(t\), where a point \(p\) matches a rule \(R_i\), and the production of \(R_i\) is applied to \(p\), modifying the state of the grid in the next time step \(t+1\).
Grammar and design generation process¶
Given \(n\) rules, a grammar \(Gr={R_0, R_1, \dots , R_n}\) is simply the set of all rules.
We start with a grid where all points are associated with the nonterminal symbol Unassigned. Then, at discrete time-steps, we choose a point in the grid and try to match it with one or more rules in the grammar. If a rule matches the local context of the chosen point, we apply the production of the rule to the point, which changes its nonterminal symbol and potentially creates edges between adjacent points. We repeat this process until all points contain nonterminal symbols or until we have no rules matching in the grammar.
Contract formalization with Pacti¶
We can use pacti as verification engine to match rules with points on the grid. We are going to use the composition and refinement operators to verify weather local contexts of points match rule's conditions. In the following we are going to formalize local contexts and rules with contracts of polyhedra constraints.
We can use pacti as a verification engine to match rules with points on the grid. We are going to use the composition and refinement operators to verify weather local contexts of points match rule's conditions. To do this, we will define contracts using polyhedral constraints to formalize local contexts and rules.
Local directions as linear constraint¶
We will define a variable for every terminal and nonterminal symbol of the grammar and an integer for every direction. For example, given the grammar with nonterminal symbols \(\Lambda={\texttt{Fuselage}, \texttt{Rotor}, \texttt{Wing}, \texttt{Connector}, \texttt{Empty}}\) and terminal symbol \(\Theta={\texttt{Unoccupied}}\), we generate a set of variables \(V = {f, r, w, c, e, u}\) where each element corresponds to the element in \(\Lambda \cup \Theta\) starting with the corresponding letter. We define a set of integers \(\Delta'={0,1,2,3,4,5,6}\) where every element corresponds to an element in \(\Delta={\texttt{ego}, \texttt{front}, \texttt{rear}, \texttt{left}, \texttt{right}, \texttt{top}, \texttt{bottom}}\). Our goal is to represent a local context with linear constraints such as \(U \le 6~~ \land~~ F = 7\), which prescribe a local context having \(\texttt{Unoccupied}\) in the direction corresponding to the integers \(i \in \Delta'\) where \(i \leq 6\) and a \(\texttt{Fuselage}\) in the direction corresponding to the integer \(7\). From this example we can see how the assignment of integers in \(\Delta'\) to directions in \(\Delta\) can greatly influence the number of constraints necessary to express a set of local contexts.
Direction assignment problem¶
We have seen how from a local context we can produe a set of local constraints that represents it.
Given a grammar with \(n\) rules \(Gr=\{R_0, R_1, \dots , R_n\}\) where every rule \(R_i \in Gr\) contains a set if local contexts, e.g. \(\Omega_i = \{LC_0, LC_1, \dots, LC_c\}\); given a set of seven directions \(\Delta=\{\texttt{ego}, \texttt{front}, \texttt{rear}, \texttt{left}, \texttt{right}, \texttt{top}, \texttt{bottom}\}\); Produce a function \(Dir: \Delta \rightarrow \Delta'\) that maps elements of \(\Delta\) to elements of \(\Delta'=\{0,1, 2,3,4,5,6\}\) such that it minimizes the number of constraints representing the local contexts for all the rules in the grammar.
Please see the method get_directions_assignment in grammar.py for the implementation of such function.
For the grammar in our case study the optimal assignment is the following:
Contracts for State¶
We can transform any state of a point \(p\) in the grid into a contract having true assumptions and the set of linear constraints representing the state as guarantees.
For example, let us consider the state in the figure below:
We have annotated all the edges with a tuple containing respectively the integer assignment of the direction and the variable representing the symbol. The contract representing the state in the figure is the following:
Notice that the guarantees of \(C_{s(t)}\) contain a disjunction. Since in pacti contracts can only have conjunctions of constraints, we distribute the disjunction and create new contracts that we group in a structure that we refer as ContractUnions
Contracts for Rules¶
Let us show how rules can be modeled as contracts. The figure below shows a pictorial representation of one rule having four local contexts as matching conditions and producing a symbol and a connection.
The conditions describe four different states where from the ego position we can have in front a fuselage (red), a propeller (green), a wing (blue), and a connector (grey). The production prescribes the ego symbol to be a connector and a connection to the symbol in front of it. We represent the rule with a ContractUnion formed by four contracts.
The assumptions of the contract represent all possible conditions that are accepted by the rule, while the guarantees specify the symbol to be placed in the ego position (\(c=6\)) and provide information about a possible connection. In this case, the value of \(edge=4\) indicates a connection from the ego position to direction 4, which represents the front direction.
Assuring matching conditions using contracts composition¶
We are using the composition operation offered by pacti to assure that a rule is a valid match for a given state. When composing two contracts pacti will check if the guarantees of a contract are compatible with the assumptions of the other contract being composed. Composing a state contract with a rule contract will automatically check if the state is compatible with the rule, as shown in the following picture.
We have seen how both rules and states can be expressed as ContractUnion objects. When pacti composes a rule ContractUnion with a state ContractUnion, it checks if every element of the state can be composed with at least one element of the rule. Furthermore before composing a rule with a state, we produce an abstraction of every contract in the rule ContractUnion, by removing constraints related to variables which are not present in the state. The figure below shows the abstraction produced by the rule \(r_{i}\) introduced before.
Running the code¶
We start with some imports
import random
from src.contracts_utils.union import ContractsUnions
from src.grammar.grammar import Grammar
from src.grammar.grid import GridBuilder
from src.shared.shared import DirectionsAssignment, SymbolType
from src.shared.paths import rules_path
from src.tools.refinement_checking import rule_matching
from src.tools.plotting import create_gif
import matplotlib.pyplot as plt
We define three constants defining the half size (\(n_{half}\)) of the grid, the max number of wings and rotors that we want the UAV to have.
We can generate a new grid with the GridBuilder class
We can build a Grammar object from a json file where we have defined all the rules.
Then we produce an optimal assignment of integers to the diretions based on the grammar
directions_assignment = DirectionsAssignment()
directions_assignment.set_direction_assignment(grammar.get_directions_assignment())
Creating the object
We convert all the rules of the grammar to contracts
We explore all the points of the grid until there are no more points to visit. At each iteration, we * Update the current point to visit * Get the local state wrt the point chosen * Create the list of "rule contracts" that are allowed at the current iteration based on the current number of wings and propellers * Convert the state to a contract * Find all the matching rules to the current state * Select one of the compatible rules randomly and apply it to the current state
step = 0
figures: list[plt.Figure] = []
while len(grid.points_to_visit) > 0:
# print(f"STEP {step}")
# print(f"{len(grid.points_to_visit)} POINTS LEFT:\t{grid.points_to_visit}")
grid.update_current_point()
current_state = grid.local_state()
if step > 0 and not current_state.has_non_empty_symbols():
continue
forbidden_symbols = set()
if grid.n_wings == max_num_wings and grid.n_rotors == max_num_rotors:
break
if grid.n_wings >= max_num_wings:
forbidden_symbols.add(SymbolType.WING)
if grid.n_rotors >= max_num_rotors:
forbidden_symbols.add(SymbolType.ROTOR)
rules_allowed_contracts = list({k: v for k, v in rule_contracts.items() if k not in forbidden_symbols}.values())
rules_allowed_contracts = [item for sublist in rules_allowed_contracts for item in sublist]
if step > 0:
rules_allowed_contracts = list(filter(lambda x: x.name != "r0", rules_allowed_contracts))
rule_names_allowed = [r.name for r in rules_allowed_contracts]
if step == 0:
rules_compatible_contracts = [grammar.rules["r0"]]
else:
rules_compatible_contracts = rule_matching(current_state.contract, rules_allowed_contracts)
r_id_from_contracts = [rc.name for rc in rules_compatible_contracts]
r_id_from_contracts_str = "-".join(sorted(r_id_from_contracts))
# print(f"R_C: {r_id_from_contracts_str}")
if len(list(rules_compatible_contracts)) > 0:
chosen_rule = random.choice(list(rules_compatible_contracts))
grid.apply_rule(grammar.rules[chosen_rule.name])
else:
grid.apply_rule(grammar.rules["r19"])
fig: plt.Figure = grid.figure_with_edges
figures.append(fig)
# Increase step counter
step += 1
grid.cleanup()
figures.append(grid.figure_with_edges)
print(f"Design generated in {step} steps")
gif_path = create_gif(figures=figures, filename="uav_design_process.gif")
Design generated in 41 steps
GIF generated at: uav_design_process.gif
We can visualize the different steps of the design process in the following GIF:
