## 2 System Model
### Baseline Scheduling Algorithm with Sub-Flow Division
#### 2.4.2 Iterative Constraint Boundary Determination and GCL Generation via SMT Solver  
Once the streams are prepared, the algorithm proceeds to determine the precise schedule start times \(\varphi_{i,j,\mu}\) (or \(\phi_{i,\mu}\) for undivided streams) that satisfy all constraints from Section 2.3. This is achieved using an iterative approach coupled with the Z3 SMT solver.  
The core challenge lies in finding appropriate, yet tight, boundaries for operational constraints such as end-to-end latency, jitter, and inter-cycle start time deviations, as these directly impact schedulability and performance. The iterative process is as follows:  
1. Initial Strict Constraint Setting: The process begins by establishing the most stringent (i.e., performance-optimal) target values for latency and jitter. For each stream \(F_{i}\), LatencyRequirements\({}_{i}\) is initialized to its minimum possible value (sum of its total transmission time over the path, all propagation delays, and minimal switch processing times, effectively aiming for zero queuing delay). JitterRequirements\({}_{i}\) is set to a near-zero value (e.g., 1 \(\upmu\)s). The deadlines \(D_{i}\) are taken as hard upper bounds from user input, and inter-cycle start time deviations \(\delta_{i}\) are initially set to tight values.
2. SMT Solver Invocation: With the current set of constraint boundaries, the Z3 SMT solver is invoked. The solver attempts to find a satisfying assignment for all \(\varphi_{i,j,\mu}\) variables that meets all mathematical constraints defined in Section 2.3.
3. Adaptive Constraint Relaxation: If the SMT solver reports that the problem is unsatisfiable with the current constraint boundaries, the algorithm systematically relaxes the LatencyRequirements\({}_{i}\) and JitterRequirements\({}_{i}\). This relaxation is typically performed iteratively:  
* Relaxation prioritizes lower-priority streams first.
* The values are increased by small increments.  
Figure 1: Illustration of the sub-flow division mechanism. (**a**) A scheduling attempt fails as the long transmission block of the stream in Queue 2 prevents the stream in Queue 1 from meeting its deadline. (**b**) After the algorithm automatically applies sub-flow division, the high-bandwidth stream is segmented, resolving the conflict and enabling a successful schedule for both streams.  
After each relaxation step, the SMT solver is invoked again (Step 2).  
User-defined deadlines \(D_{i}\) are generally treated as hard constraints and are not relaxed unless all other avenues fail and the application permits.
4. Convergence and GCL Finalization: This iterative loop of solving and relaxing constraints continues until the SMT solver finds a feasible solution. The objective is to converge to the \"tightest\" possible set of latency and jitter values for which the entire stream set \(\mathcal{S}_{\textit{scd}}\) is schedulable. Once a feasible set of start times \(\varphi_{i,j,\mu}\) is determined, the GCL is constructed. For each sub-stream \(f_{i,j}\), its transmission window in each cycle instance \(\mu\) is \([\varphi_{i,j,\mu},\varphi_{i,j,\mu}+a_{ij}]\). These time windows, along with the \(PCP_{i}\) of the corresponding original stream \(F_{i}\), define the GCL entries. Each entry specifies the opening and closing times of the transmission gate for the queue associated with \(PCP_{i}\) on the relevant TSN switch output ports along path \(P_{i}\).  
This SMT-based iterative approach allows for a robust search for a feasible GCL that adheres to complex timing constraints while attempting to optimize for low latency and jitter. If sub-flows were created during preprocessing, they are treated as individual scheduling entities during this GCL computation phase; their reassembly into the original data stream is assumed to occur at the receiving end-station.