########## MAIN TODOS ####################################################################################


Connectives:
  ☐ Change DiamondRelationalConnective and BoxRelationalConnective from singletons to structs wrapping a relation.

Interpretations:
  ☐ Create a SupportedInterpretation
  ☐ Algorithm to generate a truth table

Normalization:
  ☐ Add custom normalization rules to normalize
  ☐ Assuming boolean logic, "((¬q v p) ∧ ¬q)" could be simplified to "¬q"

Random:
  ☐ Generator for formulas with specific contraints:
    ✔ Fixed height formulas @done(23-12-06 12:04)
    ☐ CNF/DNF formulas
    ☐ UnSAT formulas
    ☐ Fuzzy formulas (algebra is an argument)
    ☐ Logger for offline formulas (in a log file, i can load and retrieve already generated formulas)
    ☐ Generator for complete collection of formulas generator (all possible combinations of formulas are considered)
  
  ☐ Add the following utility dispatches:
    ☐ rand(connectives, atom leaves array, algebra from which infer truth values)
    ☐ rand(connectives, atom leaves array, truth values with common supertype)
    ☐ rand(connectives, atom leaves array, true/false (use truth values as leaf or not. If true, default to boolean))
    ☐ sample(..., probability distribution)
    
  ✔ Write random models generation (see pluto-demo.jl and exploit Graphs.SimpleGraphs generation) @done(23-12-20 17:52)
  ☐ Expand the models generator, giving the possibility to use a generic SimpleGraphs method to shape a kripke frame 

Readability:
  ☐ Add parameters to syntaxstring:
    ☐ parenthesize_unary_modals = false (force <G>phi becomes <G>(phi))
    ☐ parenthesize_operators 
  ☐ meaningful names for relations: - IA_L -> After/Right - IA_A -> RightAfter

Tests:
  ☐ Increase code coverage

PAndQ:
  ☐ Recognize if a formula is satisfiable, is a contingency, a tautology or a contraddiction.

########## DONE ##########################################################################################

Documentation:
  ✔ In the documentation, show how to create a custom operator (maybe a Xor/⊻/⊕) starting from scratch. @done(23-12-06 12:05)

Normalization:
  ✔ Simplify code when possible, using dual/hasdual traits @done(23-12-06 12:05)
  
Random:
  ✔ Clean rand and sample dispatches

README:
  ✔ Check examples (see NOTE or pluto-demo.jl) @done(23-09-05 19:34)
  ✔ List of similar packages @done(23-09-05 19:30)
  ✔ Highlight SoleLogics use cases

Readability: 
  ✔ Write check's docstring @done(23-09-05 19:33)
  ✔ Rename things to increase readability, using @deprecate in a deprecate.jl file. @done(23-12-06 12:05)

Tests:
  ✔ Fix SatsBase.sample errors @done(23-09-05 19:36)
  ✔ Add the following tests: @done(23-12-20 18:07)
    ✔ syntaxstring tests: get "◊¬p ∧ ¬q" from "(◊¬p) ∧ (¬q)" @done(23-12-20 18:06)
    ✔ syntaxstring tests: get "(q) → ((p) → (¬(q)))" from "q → p → ¬q" @done(23-12-20 18:07)
    ✔ (parseformula("p ∧ q ∧ r ∨ s ∧ t")) == @synexpr p ∧ q ∧ r ∨ s ∧ t @done(23-12-19 10:29)

Utilities:
  ✔ Differentiate Base.rand and StatsBase.sample (randformula should have a picker::Function argument, which can be rand or sample) @done(23-12-06 12:05)
  ✔ @atoms defaulted to String @done(23-09-12 15:48)

PAndQ:
  ✔ Write the algorithm that produces truth tables of propositional formulae @done(23-09-05 19:36)
  ✔ Macro to easily create atoms and parse expressions related to syntax (See PAndQ.jl) @done(23-09-05 19:36)
