# Notes about SoleLogics structure.

	# This alphabet is not complete and its dispatches requires more arguments to work
	struct NonCompleteDimensionalAlphabet{A} <: AbstractAlphabet{A}
	    #
	end

	# AbstractAlphabet children types
	propositions(::NonCompleteDimensionalAlphabet, thresholds...) = for for for for

    #### Alphabet: new things (5 december) ####
    AbstractDimensionaAlphabet
        DimensionalAlphabet # Wraps a Vector{L}
        FullUnbounded       # 4 parameters are combined using product
                            #but A is infinite (thresholds are needed to enumerate things)

* formula normalization heuristic (can be done using precedence for letters, and precedence + hashing for operators)

* fan-in fan-out method to generate pseudorandom Kripke Frames

* `generate()` to generate pseudo random Kripke Frames



<!-- Draft README.md 
# Usage

## Parsing Formulas
Consider the string representation of a logical formula (in infix notation, e.g., "p∧q" or in function notation, e.g. "∧(p,q)". Such expressions can easily be parsed to a `SyntaxTree` representation using the method `parseformulatree`. As you can see from the documentation, it is highly customizable, allowing parsing custom-defined operators and changing how recognized propositions must be interpreted (e.g. in "true∧false" propositions are booleans, while in "1∧0" they are integers).

The `SyntaxTree` returned by `parseformulatree` can be paired with a logic (a grammar and an algebra) using `parseformula`, thus returning a Formula: the latter method disposes of the same flexibility of `parseformulatree`.

## Generating random formulas
Random formulas generation is provided by the following methods:
- randformula (which returns a SyntaxTree);
- randformulatree (which returns a SyntaxTree anchored to a Logic, thus, a Formula).

Both allow customizing the generation process by setting an alphabet (that is, which propositional letters are in play), an operators vector, the maximum height of the SyntaxTree and the maximum modal depth (that is, the maximum number of modal operators, if any, in each SyntaxTree path).

Notes for Giovanni; 
1) many important definitions are introduced here: is this the correct place to explain them or it's better to just link the documentation? 
2) I'm still working on putting a modal_depth parameter in both randformula and randformulatree 
3) As stated in AbstractSyntaxStructure docstring, classically a logical formula is implemented using a tree structure (an AST) but other representations may exist: I guess we could add a "randnormalform" method

## Generating random interpretations
Kripke models generation is provided by gen_kmodel interface. As you can see from the documentation, internally it builds up a random directed graph structure (using some, possibly custom algorithm). The adjacency list obtained is enriched with informations to obtain a so called Kripke frame; this is done by taking each vertex in the list and

- converting it into a World structure;
- defining which worlds are accessible from this following a specific relation (I'm trying to summarize both the concept of binary accessiblity relation R and the accessibles method...).

Finally, pairing each world in the Kripke frame with a list of propositional letters (this goes undeer the name of world valuation function), a Kripke model is returned by gen_kmodel.

## Model checking

## Interpretation sets

 -->
