considerations.tex

\chapter{Considerations}

In this chapter, we elaborate on different considerations regarding the specification and implementation of complex data types.

\section{Scope of unique object identifiers}
\label{sec:local_vs_global_idents}
As described in Algorithm \ref{code:gen_tuples} of Section \ref{sec:transform_temp_structure}, we assign unique identifiers to tuples generated from complex JSON object values. The current implementation uses a simple integer-based counter, which the monitor resets at the beginning of each time point -- therefore assigning only locally unique identifiers. The greatest advantage of this implementation is its simplicity, while it still allows unique referencing between tuples of the same time point. On the other hand, non-global uniqueness implies that unrelated objects of different time points share the same identifier. Therefore, we cannot use the value of an identifier in different temporal scopes (such as in \code{UNTIL} or \code{EVENTUALLY}) without risking an unintended change of semantics of the input formula. Furthermore, we cannot define the more efficient referential equality between objects observed at different time points. Instead, we must rely on structural equality by preprocessing complex-typed formulas before compilation. The example in Section \ref{sec:preprocessing} illuminates possible issues when dealing with locally unique identifiers.

An alternative implementation may depend on globally unique identifiers instead. Assigning every observed object a unique identifier may not be helpful: every referential equality between two objects would evaluate as false. Instead, objects with equal structure should be assigned the same identifier. Referring back to the example of Section \ref{sec:preprocessing}, every object instance related to the same user would share the same identifier, allowing to pass identifiers over temporal operators and enabling referential equality. This would significantly simplify the structure of compiled formulas by skipping the transformations during preprocessing explained in Section \ref{sec:preprocessing}. The downside of globally unique identifiers is the complexity of the implementation: Assigning shared identifiers to structurally equal objects at different time points requires the monitoring system to keep track of a mapping from object structures to their assigned identifiers. To limit the space complexity of this map, obsolete entries must be garbage collected regularly, based on the temporal reach of the formula under monitoring.

To keep the scope of this work limited, we have chosen an implementation with locally unique identifiers instead.

\section{Orderable custom sorts and boolean sorts}
As declared by the type derivation rules in Figure \ref{fig:formula_type_rules}, values of custom product and boolean sorts are not (totally) ordered. For both kinds of sorts, the ordering of values may be interpreted differently based on the application. Introducing an order in this work and changing it later would not guarantee backward compatibility with formulas written for older versions of \MonPolyN. Moreover, authors of formulas may always declare a particular order relation on custom sorts using let bindings. For these reasons, we do not introduce a fixed order for custom and boolean sorts.

\section{Reporting values of nested fields}
Whenever \MonPoly encounters a prefix of a trace satisfying a given MFODL formula, it prints the corresponding interpretation of the formula, i.e. the values assigned to all free variables at the evaluated time point. Whenever a free variable is of a complex sort, the variable's value points to the compound value's identifier, as described in Chapter \ref{chap:compilation}. While the compilation process does generate new variables for each projection in the original CMFODL formula, each of these variables is bound by an existential quantifier and is therefore not a free variable of the input formula. A possible solution is to avoid binding variables representing nested fields of free variables. This approach changes the set of free variables during compilation as a side effect. We instead delegate the decision on which values to report to the author of the formula, by allowing assignments of nested values to arbitrary free variables. Referring to Example \ref{ex:compile_custom_sorts} on page \pageref{ex:compile_custom_sorts}, if the URL of a violating request should be reported, one can extend the formula in conjunction with the assignment $\mathsf{url\ =\ r.url}$, introducing a new free variable $\mathsf{url}$.

%%% Local Variables:
%%% mode: latex
%%% TeX-master: "thesis"
%%% End: