diff --git a/Project.toml b/Project.toml
index 8e62d523..47b5c852 100644
--- a/Project.toml
+++ b/Project.toml
@@ -1,7 +1,7 @@
 name = "SoleLogics"
 uuid = "b002da8f-3cb3-4d91-bbe3-2953433912b5"
-authors = ["Mauro MILELLA", "Giovanni PAGLIARINI", "Alberto PAPARELLA", "Eduard I. STAN"]
-version = "0.8.2"
+authors = ["Mauro MILELLA", "Giovanni PAGLIARINI", "Edoardo PONSANESI", "Alberto PAPARELLA", "Eduard I. STAN"]
+version = "0.9.0"
 
 [deps]
 AbstractTrees = "1520ce14-60c1-5f80-bbc7-55ef81b5835c"
diff --git a/docs/src/modal-logic.md b/docs/src/modal-logic.md
index b5fcf6fc..aee3130c 100644
--- a/docs/src/modal-logic.md
+++ b/docs/src/modal-logic.md
@@ -144,7 +144,7 @@ accessibles(fr::AbstractMultiModalFrame{W}, w::W, r::AbstractRelation) where {W<
 ```@docs
 AbstractKripkeStructure
 
-check(φ::SyntaxTree, i::AbstractKripkeStructure, w::Union{Nothing,<:AbstractWorld} = nothing; use_memo::Union{Nothing,AbstractDict{<:Formula,<:Vector{<:AbstractWorld}}} = nothing, perform_normalization::Bool = true, memo_max_height::Union{Nothing,Int} = nothing)
+check(φ::SyntaxTree, i::AbstractKripkeStructure, w; use_memo::Union{Nothing,AbstractDict{<:Formula,<:Vector{<:AbstractWorld}}} = nothing, perform_normalization::Bool = true, memo_max_height::Union{Nothing,Int} = nothing)
 
 KripkeStructure{FR<:AbstractFrame, MAS<:AbstractDict}
 ```
diff --git a/docs/src/more-on-formulas.md b/docs/src/more-on-formulas.md
index d982ab23..43cc2199 100644
--- a/docs/src/more-on-formulas.md
+++ b/docs/src/more-on-formulas.md
@@ -50,6 +50,7 @@ parsebaseformula(expr::String, additional_operators::Union{Nothing,Vector{<:Oper
 
 ```@docs
 Base.rand(alphabet::AbstractAlphabet, args...; kwargs...)
+SoleLogics.randatom
 StatsBase.sample(alphabet::AbstractAlphabet, weights::AbstractWeights, args...; kwargs...)
 
 randformula(height::Integer, alphabet, operators::AbstractVector; rng::Union{Integer,AbstractRNG} = Random.GLOBAL_RNG)
diff --git a/src/SoleLogics.jl b/src/SoleLogics.jl
index 8d7591c1..b081c191 100644
--- a/src/SoleLogics.jl
+++ b/src/SoleLogics.jl
@@ -27,7 +27,9 @@ export syntaxstring
 export arity, valuetype, tokentype, tokenstype,
         atomstype, operatorstype, truthtype,
         associativity, precedence
-export value, token, children, formulas
+
+# export value # TODO remove. The name is too generic, and it clashes, e.g., with JuMP.value.
+export token, children, formulas
 export tree
 
 export tokens, ntokens, atoms, natoms, truths, ntruths, leaves, nleaves,
diff --git a/src/core.jl b/src/core.jl
index 0c3bf412..dd790b06 100644
--- a/src/core.jl
+++ b/src/core.jl
@@ -717,8 +717,8 @@ end
 ############################################################################################
 
 """
-    struct SyntaxBranch{T<:Connective} <: SyntaxTree
-        token::T
+    struct SyntaxBranch <: SyntaxTree
+        token::Connective
         children::NTuple{N,SyntaxTree} where {N}
     end
 
@@ -737,7 +737,7 @@ julia> p,q = Atom.([p, q])
  Atom{String}: q
 
 julia> branch = SyntaxBranch(CONJUNCTION, p, q)
-SyntaxBranch{NamedConnective{:∧}}: p ∧ q
+SyntaxBranch: p ∧ q
 
 julia> token(branch)
 ∧
@@ -764,47 +764,30 @@ See also
 [`operators`](@ref), [`noperators`](@ref),
 [`tokens`](@ref), [`ntokens`](@ref),
 """
-struct SyntaxBranch{T<:Connective} <: SyntaxTree
+struct SyntaxBranch <: SyntaxTree
 
     # The syntax token at the current node
-    token::T
+    token::Connective
 
     # The child nodes of the current node
     children::NTuple{N,SyntaxTree} where {N}
 
-    function _aritycheck(N, T, token, children)
-        @assert arity(token) == N "Cannot instantiate SyntaxBranch{$(T)} with token " *
+    function _aritycheck(N, token, children)
+        @assert arity(token) == N "Cannot instantiate SyntaxBranch with token " *
                                   "$(token) of arity $(arity(token)) and $(N) children."
         return nothing
     end
 
-    function SyntaxBranch{T}(
-        token::T,
-        children::NTuple{N,SyntaxTree} = (),
-    ) where {T<:Connective,N}
-        _aritycheck(N, T, token, children)
-        return new{T}(token, children)
-    end
-
-    function SyntaxBranch{T}(
-        φ::SyntaxBranch{T},
-    ) where {T<:Connective}
-        return SyntaxBranch{T}(token(φ), children(φ))
-    end
-
     function SyntaxBranch(
-        token::T,
+        token::Connective,
         children::NTuple{N,SyntaxTree} = (),
-    ) where {T<:Connective,N}
-        _aritycheck(N, T, token, children)
-        return new{T}(token, children)
+    ) where {N}
+        _aritycheck(N, token, children)
+        return new(token, children)
     end
 
     # Helpers
-    function SyntaxBranch{T}(token::T, children...) where {T<:Connective}
-        return SyntaxBranch{T}(token, children)
-    end
-    function SyntaxBranch(token::T, children...) where {T<:Connective}
+    function SyntaxBranch(token::Connective, children...)
         return SyntaxBranch(token, children)
     end
 
diff --git a/src/interpretation-sets.jl b/src/interpretation-sets.jl
index ddb468f7..363ad19d 100644
--- a/src/interpretation-sets.jl
+++ b/src/interpretation-sets.jl
@@ -109,21 +109,41 @@ function check(
     i::LogicalInstance,
     args...;
     kwargs...
+)
+    return error("Please, provide method " *
+        "check(φ::SyntaxTree, i::$(typeof(i)), " *
+        "args...::$(typeof(args)); " *
+        "kwargs...::$(typeof(kwargs))).")
+end
+
+function check(
+    φ::SyntaxTree,
+    i::LogicalInstance,
+    args...;
+    kwargs...
 )
     return istop(interpret(φ, i, args...; kwargs...))
     # return check(tree(φ), i, args...; kwargs...)
 end
 
+# # General grounding
 # function check(
 #     φ::SyntaxTree,
-#     i::LogicalInstance,
-#     args...;
+#     i::LogicalInstance{AbstractInterpretationSet{<:AbstractKripkeStructure}};
 #     kwargs...
 # )
-#     return error("Please, provide method " *
-#         "check(φ::SyntaxTree, i::$(typeof(i)), " *
-#         "args...::$(typeof(args)); " *
-#         "kwargs...::$(typeof(kwargs))).")
+#     if token(φ) isa Union{DiamondRelationalConnective,BoxRelationalConnective}
+#         rel = SoleLogics.relation(SoleLogics.token(φ))
+#         if rel == tocenterrel
+#             check(first(children(φ)), i, centralworld(frame(i)); kwargs...)
+#         elseif rel == globalrel
+#             check(first(children(φ)), i, AnyWorld(); kwargs...)
+#         else
+#             check(first(children(φ)), i, accessibles(frame(i), rel); kwargs...)
+#         end
+#     else
+#         error("Unexpected formula: $φ!")
+#     end
 # end
 
 function interpret(
@@ -306,44 +326,3 @@ end
 accessibles(s::AbstractInterpretationSet, i_instance::Integer, args...) = accessibles(frame(s, i_instance), args...)
 allworlds(s::AbstractInterpretationSet, i_instance::Integer, args...) = allworlds(frame(s, i_instance), args...)
 nworlds(s::AbstractInterpretationSet, i_instance::Integer) = nworlds(frame(s, i_instance))
-
-function check(
-    φ::SyntaxBranch{
-        Union{
-            DiamondRelationalConnective{typeof(tocenterrel)},
-            BoxRelationalConnective{typeof(tocenterrel)},
-        }
-    },
-    i::AbstractInterpretation;
-    kwargs...
-)
-    check(first(children(φ)), i, centralworld(frame(i)); kwargs...)
-end
-
-function check(
-    φ::SyntaxBranch{
-        Union{
-            DiamondRelationalConnective{typeof(globalrel)},
-            BoxRelationalConnective{typeof(globalrel)},
-        }
-    },
-    i::AbstractInterpretation;
-    kwargs...
-)
-    check(first(children(φ)), i, nothing; kwargs...)
-end
-
-# # General grounding
-# function check(
-#     φ::SyntaxBranch{
-#         Union{
-#             DiamondRelationalConnective{R},
-#             BoxRelationalConnective{R},
-#         }
-#     },
-#     i::AbstractInterpretation;
-#     kwargs...
-# ) where {R<:AbstractRelation}
-#     rel = SoleLogics.relation(SoleLogics.token(φ))
-#     check(first(children(φ)), i, accessibles(frame(i), rel); kwargs...)
-# end
diff --git a/src/logics.jl b/src/logics.jl
index a6fe94fe..7d9c2d78 100644
--- a/src/logics.jl
+++ b/src/logics.jl
@@ -1,3 +1,5 @@
+import SoleBase: initrng
+
 import Base: convert, promote_rule, _promote
 import Base: eltype, in, getindex, isiterable, iterate, IteratorSize, length, isequal, hash
 
@@ -117,20 +119,49 @@ function Base.in(value::Union{AbstractString,Number,AbstractChar}, a::AbstractAl
 end
 
 """
-    Base.length(a::AbstractAlphabet)::Bool
+    natoms(a::AbstractAlphabet)::Integer
 
-Return the alphabet length, if it is finite.
+Return the number of atoms of a *finite* alphabet.
 
-See also [`AbstractAlphabet`](@ref), [`SyntaxBranch`](@ref).
+See also [`randatom`](@ref), [`AbstractAlphabet`](@ref).
 """
-function Base.length(a::AbstractAlphabet)
+function natoms(a::AbstractAlphabet)::Integer
+    if Base.isfinite(a)
+        return error("Please, provide method natoms(::$(typeof(a))).")
+    else
+        return error("Cannot compute natoms of (infinite) alphabet of type $(typeof(a)).")
+    end
+end
+
+"""
+    randatom(a::AbstractAlphabet)
+    randatom(rng, a::AbstractAlphabet)
+
+Return a random atom from a *finite* alphabet.
+
+See also [`natoms`](@ref), [`AbstractAlphabet`](@ref).
+"""
+function randatom(a::AbstractAlphabet, args...; kwargs...)
+    randatom(Random.GLOBAL_RNG, a, args...; kwargs...)
+end
+
+function randatom(rng::Union{Random.AbstractRNG, Integer}, a::AbstractAlphabet, args...; kwargs...)
     if isfinite(a)
-        return Base.length(atoms(a))
+        # TODO: note that `atoms(a)` can lead to brutal reduction in performance,
+        #  if one forgets to implement specific methods for `randatom` for custom alphabets!
+        return Base.rand(rng, atoms(a), args...; kwargs...)
     else
-        return error("Cannot compute length of (infinite) alphabet of type $(typeof(a)).")
+        error("Please provide method randatom(rng::$(typeof(rng)), " *
+            "alphabet::$(typeof(a)), args...; kwargs...)")
     end
 end
 
+# Helper
+function Base.length(a::AbstractAlphabet)
+    @warn "Please use `natoms` instead of `Base.length` with alphabets."
+    return natoms(a)
+end
+
 """
     Base.iterate(a::AbstractAlphabet)
     Base.iterate(a::AbstractAlphabet, state)
@@ -188,6 +219,7 @@ struct ExplicitAlphabet{V} <: AbstractAlphabet{V}
     end
 end
 atoms(a::ExplicitAlphabet) = a.atoms
+natoms(a::ExplicitAlphabet) = length(atoms(a))
 
 Base.convert(::Type{AbstractAlphabet}, alphabet::Vector{<:Atom}) =
     ExplicitAlphabet(alphabet)
@@ -213,7 +245,7 @@ Base.in(::Atom{PV}, ::AlphabetOfAny{VV}) where {PV,VV} = (PV <: VV)
 
 # Finite alphabet of conditions induced from a set of metaconditions
 """
-Alphabet given by the union of many alphabets.
+Alphabet given by the *union* of a number of (sub-)alphabets.
 
 See also
 [`UnboundedScalarAlphabet`](@ref),
@@ -222,24 +254,80 @@ See also
 """
 
 struct UnionAlphabet{C,A<:AbstractAlphabet{C}} <: AbstractAlphabet{C}
-    alphabets::Vector{A}
+    subalphabets::Vector{A}
 end
 
-alphabets(a::UnionAlphabet) = a.alphabets
+subalphabets(a::UnionAlphabet) = a.subalphabets
+nsubalphabets(a::UnionAlphabet) = length(subalphabets(a))
 
 function Base.show(io::IO, a::UnionAlphabet)
     println(io, "$(typeof(a)):")
-    for cha in alphabets(a)
-        Base.show(io, cha)
+    for sa in subalphabets(a)
+        Base.show(io, sa)
     end
 end
 
+
+
 function atoms(a::UnionAlphabet)
-    return Iterators.flatten(Iterators.map(atoms, alphabets(a)))
+    return Iterators.flatten(Iterators.map(atoms, subalphabets(a)))
 end
 
+natoms(a::UnionAlphabet) = sum(natoms, subalphabets(a))
+
 function Base.in(p::Atom, a::UnionAlphabet)
-    return any(cha -> Base.in(p, cha), alphabets(a))
+    return any(sa -> Base.in(p, sa), subalphabets(a))
+end
+
+"""
+    randatom(
+        rng::Union{Integer,AbstractRNG},
+        a::UnionAlphabet;
+        atompicking_mode::Symbol=:uniform,
+        subalphabets_weights::Union{AbstractWeights,AbstractVector{<:Real},Nothing} = nothing
+    )::Atom
+
+Sample an atom from a `UnionAlphabet`. By default, the sampling is uniform with respect to the atoms.
+However, by setting `atompicking_mode = :uniform_subalphabets` one can force
+a uniform sampling with respect to the sub-alphabets.
+Moreover, one can specify a `:weighted` `atompicking_mode`,
+together with a `subalphabets_weights` vector.
+
+See also [`UnionAlphabet`](@ref).
+"""
+function randatom(
+    rng::Union{Integer,AbstractRNG},
+    a::UnionAlphabet;
+    atompicking_mode::Symbol=:uniform,
+    subalphabets_weights::Union{AbstractWeights,AbstractVector{<:Real},Nothing} = nothing
+)::Atom
+
+    # @show a
+    @assert atompicking_mode in [:uniform, :uniform_subalphabets, :weighted] "Value for `atompicking_mode` not..."
+    rng = initrng(rng)
+    alphs = subalphabets(a)
+
+    if atompicking_mode == :weighted
+        if isnothing(subalphabets_weights)
+            error("`:weighted` picking_mode requires weights in `subalphabets_weights` ")
+        end
+        @assert length(subalphabets_weights) == length(alphs) "Mismatching numbers of alphabets " *
+            "($(length(alphs))) and weights ($(length(subalphabets_weights)))."
+        subalphabets_weights = StatsBase.weights(subalphabets_weights)
+        pickedalphabet = StatsBase.sample(rng, alphs, subalphabets_weights)
+    else
+        subalphabets_weights = begin
+            # This atomatically excludes subalphabets with empty threshold vector
+            if atompicking_mode == :uniform_subalphabets
+                Weights(ones(Int, length(alphs)))
+            elseif atompicking_mode == :uniform
+                Weights(natoms.(alphs))
+            end
+        end
+        pickedalphabet = sample(rng, alphs, subalphabets_weights)
+    end
+
+    return randatom(rng, pickedalphabet)
 end
 
 ############################################################################################
diff --git a/src/modal-logic.jl b/src/modal-logic.jl
index 3346c0f5..707aac74 100644
--- a/src/modal-logic.jl
+++ b/src/modal-logic.jl
@@ -666,11 +666,37 @@ accessibles(i::AbstractKripkeStructure, args...) = accessibles(frame(i), args...
 allworlds(i::AbstractKripkeStructure, args...) = allworlds(frame(i), args...)
 nworlds(i::AbstractKripkeStructure) = nworlds(frame(i))
 
+# TODO explain
+struct AnyWorld end
+
+# # General grounding
+# function check(
+#     φ::SyntaxTree,
+#     i::AbstractKripkeStructure;
+#     kwargs...
+# )
+#     if token(φ) isa Union{DiamondRelationalConnective,BoxRelationalConnective}
+#         rel = SoleLogics.relation(SoleLogics.token(φ))
+#         if rel == tocenterrel
+#             checkw(first(children(φ)), i, centralworld(frame(i)); kwargs...)
+#         elseif rel == globalrel
+#             checkw(first(children(φ)), i, AnyWorld(); kwargs...)
+#         elseif isgrounding(rel)
+#             checkw(first(children(φ)), i, accessibles(frame(i), rel); kwargs...)
+#         else
+#             error("Unexpected formula: $φ! Perhaps ")
+#         end
+#     else
+#         # checkw(φ, i, nothing; kwargs...)
+#         error("Unexpected formula: $φ! Perhaps ")
+#     end
+# end
+
 """
     function check(
         φ::SyntaxTree,
         i::AbstractKripkeStructure,
-        w::Union{Nothing,<:AbstractWorld} = nothing;
+        w::Union{Nothing,AnyWorld,<:AbstractWorld} = nothing;
         use_memo::Union{Nothing,AbstractDict{<:Formula,<:Vector{<:AbstractWorld}}} = nothing,
         perform_normalization::Bool = true,
         memo_max_height::Union{Nothing,Int} = nothing,
@@ -724,7 +750,7 @@ See also [`SyntaxTree`](@ref), [`AbstractWorld`](@ref), [`KripkeStructure`](@ref
 function check(
     φ::SyntaxTree,
     i::AbstractKripkeStructure,
-    w::Union{Nothing,<:AbstractWorld} = nothing; # TODO remove defaulting
+    w::Union{Nothing,AnyWorld,<:AbstractWorld} = nothing;
     use_memo::Union{Nothing,AbstractDict{<:Formula,<:Vector{<:AbstractWorld}}} = nothing,
     perform_normalization::Bool = true,
     memo_max_height::Union{Nothing,Int} = nothing
@@ -736,7 +762,7 @@ function check(
             w = first(allworlds(frame(i)))
         end
     end
-    @assert isgrounded(φ) || !isnothing(w) "Please, specify a world in order " *
+    @assert isgrounded(φ) || !(isnothing(w)) "Please, specify a world in order " *
         "to check non-grounded formula: $(syntaxstring(φ))."
 
     setformula(memo_structure::AbstractDict{<:Formula}, φ::Formula, val) = memo_structure[tree(φ)] = val
@@ -798,7 +824,7 @@ function check(
     end
 
     ret = begin
-        if isnothing(w)
+        if isnothing(w) || w isa AnyWorld
             length(readformula(memo_structure, φ)) > 0
         else
             w in readformula(memo_structure, φ)
diff --git a/src/random.jl b/src/random.jl
index 2322f96f..68f1aee5 100644
--- a/src/random.jl
+++ b/src/random.jl
@@ -55,22 +55,17 @@ See also
 """
 
 """$(doc_rand)"""
-function Base.rand(alphabet::AbstractAlphabet, args...; kwargs...)
-    Base.rand(Random.GLOBAL_RNG, alphabet, args...; kwargs...)
+function Base.rand(a::AbstractAlphabet, args...; kwargs...)
+    Base.rand(Random.GLOBAL_RNG, a, args...; kwargs...)
 end
 
 function Base.rand(
     rng::AbstractRNG,
-    alphabet::AbstractAlphabet,
+    a::AbstractAlphabet,
     args...;
     kwargs...
 )
-    if isfinite(alphabet)
-        Base.rand(rng, atoms(alphabet), args...; kwargs...)
-    else
-        error("Please, provide method Base.rand(rng::AbstractRNG, " *
-            "alphabet::$(typeof(alphabet)), args...; kwargs...).")
-    end
+    randatom(rng, a, args...; kwargs...)
 end
 
 function Base.rand(height::Integer, l::AbstractLogic, args...; kwargs...)
@@ -179,7 +174,6 @@ the others, then the first atom in the alphabet is selected more frequently.
 
 See also [`AbstractAlphabet`](@ref), [`AbstractWeights`](@ref), [`Atom`](@ref).
 """
-
 function StatsBase.sample(
     alphabet::AbstractAlphabet,
     weights::AbstractWeights,
@@ -306,12 +300,12 @@ function randformula(
     alphabet,
     operators::AbstractVector;
     modaldepth::Integer = height,
-    atompicker::Union{Function,AbstractWeights,AbstractVector{<:Real},Nothing} = sample,
-    opweights::Union{AbstractWeights,AbstractVector{<:Real},Nothing} = nothing,
+    atompicker::Union{Function,AbstractWeights,AbstractVector{<:Real},Nothing} = randatom,
+    opweights::Union{AbstractWeights,AbstractVector{<:Real},Nothing} = nothing
 )::SyntaxTree
+
     rng = initrng(rng)
     alphabet = convert(AbstractAlphabet, alphabet)
-
     @assert all(x->x isa Operator, operators) "Unexpected object(s) passed as" *
         " operator:" * " $(filter(x->!(x isa Operator), operators))"
 
@@ -324,10 +318,11 @@ function randformula(
     end
 
     if (isnothing(atompicker))
-        atompicker = StatsBase.uweights(length(alphabet))
+        atompicker = StatsBase.uweights(natoms(alphabet))
+
     elseif (atompicker isa AbstractVector)
-        @assert length(atompicker) == length(alphabet) "Mismatching numbers of atoms " *
-                "($(length(alphabet))) and atompicker ($(length(atompicker)))."
+        @assert length(atompicker) == natoms(alphabet) "Mismatching numbers of atoms " *
+                "($(natoms(alphabet))) and atompicker ($(length(atompicker)))."
         atompicker = StatsBase.weights(atompicker)
     end
 
@@ -338,14 +333,15 @@ function randformula(
 
     nonmodal_operators = findall(!ismodal, operators)
 
+    # recursive call
     function _randformula(
         rng::AbstractRNG,
         height::Integer,
-        modaldepth::Integer
+        modaldepth::Integer;
     )::SyntaxTree
+
         if height == 0
-            # Sample atom from alphabet
-            return atompicker(rng, atoms(alphabet))
+            return atompicker(rng, alphabet)
         else
             # Sample operator and generate children (modal connectives only if modaldepth > 0)
             ops, ops_w = begin
diff --git a/src/syntax-utils.jl b/src/syntax-utils.jl
index ad6b3e9f..cf7c7c48 100644
--- a/src/syntax-utils.jl
+++ b/src/syntax-utils.jl
@@ -40,17 +40,17 @@ LeftmostConjunctiveForm with 2 Atom{String} children:
         q
 
 julia> tree(conj)
-SyntaxBranch{NamedConnective{:∧}}: p ∧ q
+SyntaxBranch: p ∧ q
 
 julia> nconj = NEGATION(conj)
 LeftmostLinearForm with connective ¬ and 1 LeftmostConjunctiveForm{Atom{String}} children:
         (p) ∧ (q)
 
 julia> tree(nconj)
-SyntaxBranch{NamedConnective{:¬}}: ¬(p ∧ q)
+SyntaxBranch: ¬(p ∧ q)
 
 julia> tree(nconj ∧ nconj)
-SyntaxBranch{NamedConnective{:∧}}: ¬(p ∧ q) ∧ ¬(p ∧ q)
+SyntaxBranch: ¬(p ∧ q) ∧ ¬(p ∧ q)
 ```
 """
 
@@ -279,7 +279,7 @@ nleaves(φ::LeftmostLinearForm) = sum(nleaves, children(φ))
 #     # return TODO
 # end
 
-function atoms(φ::LeftmostLinearForm{C,<:Atom})::Bool where {C<:Connective}
+function atoms(φ::LeftmostLinearForm{C,<:Atom})::Vector{Atom} where {C<:Connective}
     return children(φ)
 end
 
@@ -291,7 +291,7 @@ end
 #     # return TODO
 # end
 
-function leaves(φ::LeftmostLinearForm{C,<:SyntaxLeaf})::Bool where {C<:Connective}
+function leaves(φ::LeftmostLinearForm{C,<:SyntaxLeaf})::SyntaxLeaf where {C<:Connective}
     return children(φ)
 end
 
@@ -299,7 +299,7 @@ end
 #     # return TODO
 # end
 
-function natoms(φ::LeftmostLinearForm{C,<:Atom})::Bool where {C<:Connective}
+function natoms(φ::LeftmostLinearForm{C,<:Atom})::Integer where {C<:Connective}
     return nchildren(φ)
 end
 
@@ -311,7 +311,7 @@ end
 #     # return TODO
 # end
 
-function nleaves(φ::LeftmostLinearForm{C,<:SyntaxLeaf})::Bool where {C<:Connective}
+function nleaves(φ::LeftmostLinearForm{C,<:SyntaxLeaf})::Integer where {C<:Connective}
     return nchildren(φ)
 end
 
@@ -522,10 +522,9 @@ struct Literal{T<:SyntaxLeaf} <: AbstractSyntaxStructure
     function Literal(φ::SyntaxLeaf, flag = true)
         return Literal(flag, φ)
     end
-    function Literal(φ::SyntaxBranch{typeof(¬)}, flag = true)
+    function Literal(φ::SyntaxBranch, flag = true)
         ch = first(children(φ))
-        @assert ch isa Union{SyntaxLeaf,SyntaxBranch{typeof(¬)}} "Cannot " *
-        # @assert ch isa SyntaxLeaf "Cannot " *
+        @assert (token(φ) == ¬) "Cannot " *
             "construct Literal with formula of type $(typeof(ch))): $(syntaxstring(ch))."
         return Literal(ch, !flag)
     end
@@ -579,25 +578,30 @@ function _cnf(φ::Formula, literaltype = Literal)
     return error("Cannot convert to CNF formula of type $(typeof(φ)): $(syntaxstring(φ))")
 end
 
-function _cnf(φ::Union{SyntaxLeaf,SyntaxBranch{typeof(¬)}}, literaltype = Literal)
+function _cnf(φ::SyntaxLeaf, literaltype = Literal)
     φ = φ isa literaltype ? φ : literaltype(φ)
     return LeftmostConjunctiveForm([LeftmostDisjunctiveForm{literaltype}([φ])])
 end
 
-function _cnf(φ::SyntaxBranch{typeof(∧)}, literaltype = Literal)
-    return _cnf(first(children(φ)), literaltype) ∧ _cnf(last(children(φ)), literaltype)
-end
-
-function _cnf(φ::SyntaxBranch{typeof(∨)}, literaltype = Literal)
-    conjs = vec([begin
-        # @show typeof(c1), typeof(c2)
-        # @show typeof(c1 ∨ c2)
-        # LeftmostDisjunctiveForm{literaltype}(c1 ∨ c2)
-        c1 ∨ c2
-    end for (c1,c2) in Iterators.product(conjuncts(_cnf(first(children(φ)), literaltype)),conjuncts(_cnf(last(children(φ)), literaltype)))])
-    # @show typeof.(conjs)
-    # conjs = Vector{LeftmostDisjunctiveForm{literaltype}}(conjs)
-    LeftmostConjunctiveForm(conjs)
+function _cnf(φ::SyntaxBranch, literaltype = Literal)
+    if token(φ) == ∧
+        return _cnf(first(children(φ)), literaltype) ∧ _cnf(last(children(φ)), literaltype)
+    elseif token(φ) == ∨
+        conjs = vec([begin
+            # @show typeof(c1), typeof(c2)
+            # @show typeof(c1 ∨ c2)
+            # LeftmostDisjunctiveForm{literaltype}(c1 ∨ c2)
+            c1 ∨ c2
+        end for (c1,c2) in Iterators.product(conjuncts(_cnf(first(children(φ)), literaltype)),conjuncts(_cnf(last(children(φ)), literaltype)))])
+        # @show typeof.(conjs)
+        # conjs = Vector{LeftmostDisjunctiveForm{literaltype}}(conjs)
+        return LeftmostConjunctiveForm(conjs)
+    elseif token(φ) == ¬
+        φ = φ isa literaltype ? φ : literaltype(φ)
+        return LeftmostConjunctiveForm([LeftmostDisjunctiveForm{literaltype}([φ])])
+    else
+        return error("Unexpected token $(token)!")
+    end
 end
 
 
diff --git a/src/ui.jl b/src/ui.jl
index 7f27ff6c..61467db6 100644
--- a/src/ui.jl
+++ b/src/ui.jl
@@ -65,8 +65,8 @@ Atom{String}("p")
 julia> @synexpr st = p ∧ q → r
 (p ∧ q) → r
 
-julia> typeof(st)
-SyntaxBranch{SoleLogics.NamedConnective{:→}}
+julia> token(st)
+→
 ```
 
 See also [`parseformula`](@ref), [`Atom`](@ref), [`Connective`](@ref),
diff --git a/test/kripke-image.jl b/test/kripke-image.jl
index 82d56947..83f402ac 100644
--- a/test/kripke-image.jl
+++ b/test/kripke-image.jl
@@ -8,7 +8,7 @@ struct BWImageKripkeStructure <: AbstractKripkeStructure
 end
 
 function interpret(a::Atom{Int}, i::BWImageKripkeStructure, w::Point{2,Int})
-	integervalue = value(a)
+	integervalue = SoleLogics.value(a)
 	valueatpoint = i.image[w[1], w[2]]
 	return (valueatpoint >= integervalue) ? TOP : BOT
 end
diff --git a/test/kripke-word.jl b/test/kripke-word.jl
index 89fe52b1..64d30e02 100644
--- a/test/kripke-word.jl
+++ b/test/kripke-word.jl
@@ -9,7 +9,7 @@ end
 frame(i::KripkeWord) = FullDimensionalFrame((length(i.word),), Point{1,Int})
 
 function interpret(a::Atom{Char}, i::KripkeWord, w::Point)
-    ch = value(a)
+    ch = SoleLogics.value(a)
     wordch = i.word[w[1]]
     return (wordch == ch) ? TOP : BOT
 end
diff --git a/test/misc.jl b/test/misc.jl
index ef76916d..573010fc 100644
--- a/test/misc.jl
+++ b/test/misc.jl
@@ -131,9 +131,9 @@ interp2             = TruthDict(1:4, BOT)
 @test trees_implication |> children |> first == pandq
 @test trees_implication |> children |> last  == porq
 
-@test norm |> children |> first                     == SyntaxTree(m)
-@test norm |> children |> first |> token            == m
-@test norm |> children |> first |> token |> value   == value(m)
+@test norm |> children |> first                              == SyntaxTree(m)
+@test norm |> children |> first |> token                     == m
+@test norm |> children |> first |> token |> SoleLogics.value == SoleLogics.value(m)
 
 @test_nowarn interp1[p] = BOT
 @test_nowarn interp1[p] = TOP
diff --git a/test/random.jl b/test/random.jl
index 3fc67f8b..685e63b6 100644
--- a/test/random.jl
+++ b/test/random.jl
@@ -78,7 +78,7 @@ g = SoleLogics.CompleteFlatGrammar(alph, ops)
 @test_nowarn randformula(Random.MersenneTwister(1), 4, alph, ops; atompicker = 1:5)
 @test_throws AssertionError randformula(Random.MersenneTwister(1), 4, alph, ops; atompicker = 1:6)
 
-@test_nowarn StatsBase.sample(4, g, Weights([1:length(alphabet(g))]...))
+@test_nowarn StatsBase.sample(4, g, Weights([1:natoms(alphabet(g))]...))
 @test_nowarn StatsBase.sample(4, g, Weights([1,1,1,1,100]))
 @test_throws MethodError StatsBase.sample(4, g, [1,1,1,1,100])
 @test_throws MethodError StatsBase.sample(Random.MersenneTwister(1), 4, g, 1:2)
diff --git a/test/runtests.jl b/test/runtests.jl
index 33fdb97a..c61d4f53 100644
--- a/test/runtests.jl
+++ b/test/runtests.jl
@@ -6,7 +6,7 @@ function run_tests(list)
     println("\n" * ("#"^50))
     for test in list
         println("TEST: $test")
-        include(test)
+        @time include(test)
     end
 end