Synthetic (modal) dataset generation

@Perro2110 and I are working towards enhancing the expressivity of the `models.jl` script.
In particular, we have at least two approaches for generating synthetic modal datasets (the exact type being `AbstractVector{K} where {K <: AbstractKripkeStructure`, for example, with a `Vector` or - better - a `SVector{...}`).

Let us consider the case where we have fixed a set of formulas, `F_1={f_1,f_2}`, `F_2={f_3,f_4}`, `...`, `F_N={f_{N-1}, f_N}`, encoding different classes.
We want the user to be able to generate a modal dataset where the first `N` instances satisfy only and exactly all the formulas in `F1`, the next `M` instances satisfy only and exactly all the formulas in `F2`, and so on.

---

# First approach (random-based)

We can randomly generate a `KripkeStructure` (both the frame and the valuation function, or only the former) and check whether all the formulas in the ith group are satisfied, while all the other formulas are not. This might be quite time-consuming, but it is for sure the most naive approach.

# Second approach (constraint-based)

A more structured approach is to iteratively build a model from a frame having only the initial world `w_0`.
To do so, we only need to parse the logical formula.

For example, let us say that `F_1` includes the formula `box ( diamond p and q) and r`, which can be translated to `w_0` with `v(w_0, r)=T` (note how box is trivially true), or, better, to:

`w_0` -- any number of neighbors --> `w_i` -- at least one neighbor --> `w_j`

where `v(w_0,r)=T`, `v(w_i,q)=T forall i`, `v(w_j,p)=T forall j`.

At this point, we continue enriching the model with all the other formulas in `F_1`, obtaining a final model, embodying the only class associated with `F_1` (which encodes the conjunction of all the formulas in `F_1`). We call such a model `M_1`.

Now, we do the same for all the formulas in `F_2`, but starting from the frame of `M_1`. In particular, we keep track of a list of constraints that must be respected while iterating the formulas in `F_2`. The idea is that violating one of such constraints automatically ensures that one formula of `F_1` surely holds on the current model.

After obtaining `M_2`, we repeat for the set of formulas we fixed at the start of the algorithm (all the classes).