using Pkg; Pkg.add("SoleLogics")
using SoleLogics

julia> φ1 = parseformula("¬p∧q∧(¬s∧¬z)");

julia> φ1 isa SyntaxTree
true

julia> syntaxstring(φ1)
"¬p ∧ q ∧ ¬s ∧ ¬z"

julia> φ2 = ⊥ ∨ Atom("t") → φ1;

julia> φ2 isa SyntaxTree
true

julia> syntaxstring(φ2)
"(⊥ ∨ t) → (¬p ∧ q ∧ ¬s ∧ ¬z)"

julia> using Random

julia> height = 2

julia> alphabet = Atom.(["p", "q"])

# Propositional case 
julia> SoleLogics.BASE_PROPOSITIONAL_CONNECTIVES
6-element Vector{SoleLogics.Connective}:
 ¬
 ∧
 ∨
 →

julia> randformula(Random.MersenneTwister(507), height, alphabet, SoleLogics.BASE_PROPOSITIONAL_CONNECTIVES)
SyntaxBranch: ¬(q → p)

# Modal case
julia> SoleLogics.BASE_MODAL_CONNECTIVES
8-element Vector{SoleLogics.Connective}:
 ¬
 ∧
 ∨
 →
 ◊
 □

julia> randformula(Random.MersenneTwister(14), height, alphabet, SoleLogics.BASE_MODAL_CONNECTIVES)
SyntaxBranch: ¬□p

julia> phi = parseformula("¬(p ∧ q)")
SyntaxBranch: ¬(p ∧ q)

julia> I = TruthDict(["p" => true, "q" => false])
┌────────┬────────┐
│      q │      p │
│ String │ String │
├────────┼────────┤
│  false │   true │
└────────┴────────┘

julia> check(phi, I)
true

julia> using Graphs

# Instantiate a Kripke frame with 5 worlds and 5 edges
julia> worlds = SoleLogics.World.(1:5);

julia> edges = Edge.([(1,2), (1,3), (2,4), (3,4), (3,5)]);

julia> fr = SoleLogics.ExplicitCrispUniModalFrame(worlds, Graphs.SimpleDiGraph(edges))
SoleLogics.ExplicitCrispUniModalFrame{SoleLogics.World{Int64}, SimpleDiGraph{Int64}} with
- worlds = ["1", "2", "3", "4", "5"]
- accessibles = 
        1 -> [2, 3]
        2 -> [4]
        3 -> [4, 5]
        4 -> []
        5 -> []

# Enumerate the world that are accessible from the first world
julia> accessibles(fr, first(worlds))
2-element Vector{SoleLogics.World{Int64}}:
 SoleLogics.World{Int64}(2)
 SoleLogics.World{Int64}(3)

julia> p,q = Atom.(["p", "q"])

 # Assign each world a propositional interpretation
julia> valuation = Dict([
	        worlds[1] => TruthDict([p => true, q => false]),
	        worlds[2] => TruthDict([p => true, q => true]),
	        worlds[3] => TruthDict([p => true, q => false]),
	        worlds[4] => TruthDict([p => false, q => false]),
	        worlds[5] => TruthDict([p => false, q => true]),
	     ])

# Instantiate a Kripke structure by combining a Kripke frame and the propositional interpretations over each world
julia> K = KripkeStructure(fr, valuation)

# Generate a modal formula
julia> modphi = parseformula("◊(p ∧ q)")

# Check the just generated formula on each world of the Kripke structure
julia> [w => check(modphi, K, w) for w in worlds]
5-element Vector{Pair{SoleLogics.World{Int64}, Bool}}:
 SoleLogics.World{Int64}(1) => 1
 SoleLogics.World{Int64}(2) => 0
 SoleLogics.World{Int64}(3) => 0
 SoleLogics.World{Int64}(4) => 0
 SoleLogics.World{Int64}(5) => 0

# A temporal frame of 10 (equidistant) points
julia> fr = SoleLogics.FullDimensionalFrame((10,), SoleLogics.Point{1,Int});

# Linear Temporal Logic (LTL) `successor` relation
julia> accessibles(fr, SoleLogics.Point(3), SoleLogics.SuccessorRel) |> collect
1-element Vector{SoleLogics.Point{1, Int64}}:
 ❮4❯

# Linear Temporal Logic (LTL) `greater than` relation
julia> accessibles(fr, SoleLogics.Point(3), SoleLogics.GreaterRel) |> collect
7-element Vector{SoleLogics.Point{1, Int64}}:
 ❮4❯
 ❮5❯
 ❮6❯
 ❮7❯
 ❮8❯
 ❮9❯
 ❮10❯

# An interval temporal frame on 10 (equidistant) points
julia> fr = SoleLogics.FullDimensionalFrame(10);

# Interval Algebra (IA) relation `L` (later, see [Halpern & Shoham, 1991](https://dl.acm.org/doi/abs/10.1145/115234.115351))
julia> accessibles(fr, Interval(3,5), IA_L) |> collect
15-element Vector{Interval{Int64}}:
 Interval{Int64}(6, 7)
 Interval{Int64}(6, 8)
 Interval{Int64}(7, 8)
 Interval{Int64}(6, 9)
 Interval{Int64}(7, 9)
 Interval{Int64}(8, 9)
 Interval{Int64}(6, 10)
 Interval{Int64}(7, 10)
 Interval{Int64}(8, 10)
 Interval{Int64}(9, 10)
 Interval{Int64}(6, 11)
 Interval{Int64}(7, 11)
 Interval{Int64}(8, 11)
 Interval{Int64}(9, 11)
 Interval{Int64}(10, 11)

# Region Connection Calculus relation `DC` (disconnected, see [Cohn et al., 1997](https://link.springer.com/article/10.1023/A:1009712514511))
julia> accessibles(fr, Interval(3,5), Topo_DC) |> collect
 16-element Vector{Interval{Int64}}:
 Interval{Int64}(6, 7)
 Interval{Int64}(6, 8)
 Interval{Int64}(7, 8)
 Interval{Int64}(6, 9)
 Interval{Int64}(7, 9)
 Interval{Int64}(8, 9)
 Interval{Int64}(6, 10)
 Interval{Int64}(7, 10)
 Interval{Int64}(8, 10)
 Interval{Int64}(9, 10)
 Interval{Int64}(6, 11)
 Interval{Int64}(7, 11)
 Interval{Int64}(8, 11)
 Interval{Int64}(9, 11)
 Interval{Int64}(10, 11)
 Interval{Int64}(1, 2)