## Constraint-Based Model
### Generation of a Workflow Log  
A workflow log \(W=\{\sigma_{1},\sigma_{2},...\sigma_{L}\}\) is a multiset of event traces [53]\(\sigma\), which can be defined as ordered sequences of activities in a process: \(\sigma=(\tau^{(1)},\tau^{(2)},...\tau^{(K)})\). Although the definition of a workflow log allows traces to appear multiple times, the aim of the presented approach is to generate a complete log artificially [54], which contains distinct workflow traces covering all the admissible execution sequences of the process. Therefore, \(W\) will be considered as an ordinary set in the further analysis. The synthetic workflow log is generated based on the data input/output specification in the process. Thus, its generation requires data structures that were presented in Section 5.1. For the purpose of finding a set of solutions, the notion of a process state is introduced. It is an \(m\)-element vector representing the presence of data entities at a particular stage of the process execution. Before specifying constraints needed to generate proper logs, it is necessary to define the satisfiability predicate [52], which determines if state vector \(s\) fulfills the requirement for a task to be executed (Formula (4)). \[sat(s,TC(\tau_{i}))\iff\forall j=1...m:s_{j}=TC(\tau_{i})_{j}\lor TC(\tau_{i}) _{j}=-1 \tag{4}\]  
where \(TC(\tau_{i})\) corresponds to the \(i\)-th row in the \(M_{TC}\) matrix. To generate a complete process log, the analyzed problem must be modeled using constraints over variables [55]. This concept is based on three main pillars: \begin{table}
\begin{tabular}{c c c c c} \hline \hline
**Value** & \(M_{TC}\) & \(M_{TE}\) & \(M_{ST}\) & \(s_{0}\) \\ \hline \(-1\) & not relevant & unchanged & not relevant & — \\
0 & forbidden & deleted & forbidden & forbidden \\
1 & required & created & required & required \\ \hline \hline \end{tabular}
\end{table} 
Table 6: Explanation of process data structure values in the constraint model. 1. Search space: finite sequences of tasks. 2. Decision variables: workflow trace, process state matrix. 3. Constraints over variables: determined by the input data, as well as a set of predefined formulae. The constraint-based model was created in the MiniZinc [56] modeling language. In this section, we present the description of applied predicates and constraints, along with their simplified code representations. Two custom predicates were defined in order to be reused in constraint definitions, namely:  
* State satisfies requirements (based on Formula (4)). predicate state_satisfies_requirements(state, requirements) = forall(s in 1..m)( state[s] == requirements[s] \/ requirements[s] == -1 );
* State satisfies set of requirements. predicate state_satisfies_requirements_set(state, requirements_set) = exists(i in 1..g)( state_satisfies_requirements(state, row(requirements_set,i)) );  
Then, the predefined constraints, which ensure the correctness of the process were formulated as follows:  
1. The global limit of executions for all tasks is a constant value and denoted as \(MAX_{EX}\). constraint max_execution_number = MAX_EX;
2. The number of executions for each task should be lower than or equal to the corresponding value in vector \(e_{t}\) or to the global limit. constraint forall(i in 1..n)( if (e_t[i] == 0 \/ e_t[i] > max_execution_number) then count_geq(workflow_trace, i, max_execution_number) else count_geq(workflow_trace, i, e_t[i]) endif );
3. The maximum length of the workflow trace is equal to \(n\times MAX_{EX}\). constraint last_task_index < n*max_execution_number+1;
4. The input state of the first executed task should be equal to \(s_{0}\). constraint forall(i in 1..m)( process_states[1, i] == s_0[i] );
5. Every non-empty task should change the current state.