Skip to content

Commit

Permalink
Clean and add IA3 and IA7 for the bidimensional case
Browse files Browse the repository at this point in the history
  • Loading branch information
giopaglia committed Jul 5, 2023
1 parent 313e73f commit 82758a8
Show file tree
Hide file tree
Showing 6 changed files with 34 additions and 27 deletions.
24 changes: 0 additions & 24 deletions NOTE
Original file line number Diff line number Diff line change
@@ -1,27 +1,3 @@
# 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

Expand Down
2 changes: 1 addition & 1 deletion src/algebras/frames/full-dimensional-frame/main.jl
Original file line number Diff line number Diff line change
Expand Up @@ -131,7 +131,7 @@ nworlds(fr::FullDimensionalFrame{3}) = div(X(fr)*(X(fr)+1),2) * div(Y(fr)*(Y(fr)

emptyworld(fr::FullDimensionalFrame{0}) = OneWorld()
emptyworld(fr::FullDimensionalFrame{1}) = Interval{Int}(-1,0)
emptyworld(fr::FullDimensionalFrame{2}) = Interval2D{Int}(Interval{Int}(w),Interval{Int}(w))
emptyworld(fr::FullDimensionalFrame{2}) = Interval2D{Int}(Interval{Int}(-1,0),Interval{Int}(-1,0))

# Smallest centered hyperrectangle
_centeredworld(X::Integer) = Interval{Int}(div(X,2)+1,(div(X,2)+1)+1+(isodd(X) ? 0 : 1))
Expand Down
1 change: 1 addition & 0 deletions src/algebras/relations/IA.jl
Original file line number Diff line number Diff line change
Expand Up @@ -226,6 +226,7 @@ IARelation = Union{typeof.(IARelations)...}

"""
const IA7Relations = [IA_AorO, IA_L, IA_DorBorE,
IA_AiorOi, IA_Li, IA_DiorBiorEi]
Vector of 7 interval relations from a coarser version of Allen's interval algebra.
Expand Down
29 changes: 29 additions & 0 deletions src/algebras/relations/IA2D.jl
Original file line number Diff line number Diff line change
Expand Up @@ -113,3 +113,32 @@ IA2DRelations...,
IA2D_URelations...
]
IA2DRelation_extended = Union{typeof.(IA2DRelations_extended)...}

############################################################################################

# IA7 2D
const IA7_IdAorO = RectangleRelation(identityrel , IA_AorO); const IA7_IdL = RectangleRelation(identityrel , IA_L); const IA7_IdDorBorE = RectangleRelation(identityrel , IA_DorBorE); const IA7_IdAiorOi = RectangleRelation(identityrel , IA_AiorOi); const IA7_IdLi = RectangleRelation(identityrel , IA_Li); const IA7_IdDiorBiorEi = RectangleRelation(identityrel , IA_DiorBiorEi);
const IA7_AorOId = RectangleRelation(IA_AorO , identityrel); const IA7_AorOAorO = RectangleRelation(IA_AorO , IA_AorO); const IA7_AorOL = RectangleRelation(IA_AorO , IA_L); const IA7_AorODorBorE = RectangleRelation(IA_AorO , IA_DorBorE); const IA7_AorOAi = RectangleRelation(IA_AorO , IA_AiorOi); const IA7_AorOLi = RectangleRelation(IA_AorO , IA_Li); const IA7_AorODiorBiorEi = RectangleRelation(IA_AorO , IA_DiorBiorEi);
const IA7_LId = RectangleRelation(IA_L , identityrel); const IA7_LAorO = RectangleRelation(IA_L , IA_AorO); const IA7_LL = RectangleRelation(IA_L , IA_L); const IA7_LDorBorE = RectangleRelation(IA_L , IA_DorBorE); const IA7_LAiorOi = RectangleRelation(IA_L , IA_AiorOi); const IA7_LLi = RectangleRelation(IA_L , IA_Li); const IA7_LDiorBiorEi = RectangleRelation(IA_L , IA_DiorBiorEi);
const IA7_DorBorEId = RectangleRelation(IA_DorBorE , identityrel); const IA7_DorBorEAorO = RectangleRelation(IA_DorBorE , IA_AorO); const IA7_DorBorEL = RectangleRelation(IA_DorBorE , IA_L); const IA7_DorBorEDorBorE = RectangleRelation(IA_DorBorE , IA_DorBorE); const IA7_DorBorEAiorOi = RectangleRelation(IA_DorBorE , IA_AiorOi); const IA7_DorBorELi = RectangleRelation(IA_DorBorE , IA_Li); const IA7_DorBorEDiorBiorEi = RectangleRelation(IA_DorBorE , IA_DiorBiorEi);
const IA7_AiorOiId = RectangleRelation(IA_AiorOi , identityrel); const IA7_AiorOiAorO = RectangleRelation(IA_AiorOi , IA_AorO); const IA7_AiorOiL = RectangleRelation(IA_AiorOi , IA_L); const IA7_AiorOiDorBorE = RectangleRelation(IA_AiorOi , IA_DorBorE); const IA7_AiorOiAiorOi = RectangleRelation(IA_AiorOi , IA_AiorOi); const IA7_AiorOiLi = RectangleRelation(IA_AiorOi , IA_Li); const IA7_AiorOiDiorBiorEi = RectangleRelation(IA_AiorOi , IA_DiorBiorEi);
const IA7_LiId = RectangleRelation(IA_Li , identityrel); const IA7_LiAorO = RectangleRelation(IA_Li , IA_AorO); const IA7_LiL = RectangleRelation(IA_Li , IA_L); const IA7_LiDorBorE = RectangleRelation(IA_Li , IA_DorBorE); const IA7_LiAiorOi = RectangleRelation(IA_Li , IA_AiorOi); const IA7_LiLi = RectangleRelation(IA_Li , IA_Li); const IA7_LiDiorBiorEi = RectangleRelation(IA_Li , IA_DiorBiorEi);
const IA7_DiorBiorEiId = RectangleRelation(IA_DiorBiorEi , identityrel); const IA7_DiorBiorEiAorO = RectangleRelation(IA_DiorBiorEi , IA_AorO); const IA7_DiorBiorEiL = RectangleRelation(IA_DiorBiorEi , IA_L); const IA7_DiorBiorEiDorBorE = RectangleRelation(IA_DiorBiorEi , IA_DorBorE); const IA7_DiorBiorEiAiorOi = RectangleRelation(IA_DiorBiorEi , IA_AiorOi); const IA7_DiorBiorEiLi = RectangleRelation(IA_DiorBiorEi , IA_Li); const IA7_DiorBiorEiDiorBiorEi = RectangleRelation(IA_DiorBiorEi , IA_DiorBiorEi);


const IA72DRelations = [IA7_IdAorO, IA7_IdL, IA7_IdDorBorE, IA7_IdAiorOi, IA7_IdLi, IA7_IdDiorBiorEi, IA7_AorOId, IA7_AorOAorO, IA7_AorOL, IA7_AorODorBorE, IA7_AorOAi, IA7_AorOLi, IA7_AorODiorBiorEi, IA7_LId, IA7_LAorO, IA7_LL, IA7_LDorBorE, IA7_LAiorOi, IA7_LLi, IA7_LDiorBiorEi, IA7_DorBorEId, IA7_DorBorEAorO, IA7_DorBorEL, IA7_DorBorEDorBorE, IA7_DorBorEAiorOi, IA7_DorBorELi, IA7_DorBorEDiorBiorEi, IA7_AiorOiId, IA7_AiorOiAorO, IA7_AiorOiL, IA7_AiorOiDorBorE, IA7_AiorOiAiorOi, IA7_AiorOiLi, IA7_AiorOiDiorBiorEi, IA7_LiId, IA7_LiAorO, IA7_LiL, IA7_LiDorBorE, IA7_LiAiorOi, IA7_LiLi, IA7_LiDiorBiorEi, IA7_DiorBiorEiId, IA7_DiorBiorEiAorO, IA7_DiorBiorEiL, IA7_DiorBiorEiDorBorE, IA7_DiorBiorEiAiorOi, IA7_DiorBiorEiLi, IA7_DiorBiorEiDiorBiorEi]

IA72DRelation = Union{typeof.(IA72DRelations)...}

############################################################################################

# IA3 2D
const IA3_IdI = RectangleRelation(identityrel , IA_I); const IA3_IdL = RectangleRelation(identityrel , IA_L); const IA3_IdLi = RectangleRelation(identityrel , IA_Li);
const IA3_IId = RectangleRelation(IA_I , identityrel); const IA3_II = RectangleRelation(IA_I , IA_I); const IA3_IL = RectangleRelation(IA_I , IA_L); const IA3_ILi = RectangleRelation(IA_I , IA_Li);
const IA3_LId = RectangleRelation(IA_L , identityrel); const IA3_LI = RectangleRelation(IA_L , IA_I); const IA3_LL = RectangleRelation(IA_L , IA_L); const IA3_LLi = RectangleRelation(IA_L , IA_Li);
const IA3_LiId = RectangleRelation(IA_Li , identityrel); const IA3_LiI = RectangleRelation(IA_Li , IA_I); const IA3_LiL = RectangleRelation(IA_Li , IA_L); const IA3_LiLi = RectangleRelation(IA_Li , IA_Li);


const IA32DRelations = [IA3_IdI, IA3_IdL, IA3_IdLi, IA3_IId, IA3_II, IA3_IL, IA3_ILi, IA3_LId, IA3_LI, IA3_LL, IA3_LLi, IA3_LiId, IA3_LiI, IA3_LiL, IA3_LiLi]

IA32DRelation = Union{typeof.(IA32DRelations)...}
4 changes: 2 additions & 2 deletions src/general.jl
Original file line number Diff line number Diff line change
Expand Up @@ -41,7 +41,7 @@ isbinary(a) = arity(a) == 2
Produces the string representation of a formula or syntax token by performing
a tree traversal of the syntax tree representation of the formula.
Note that this representation may introduce redundant parenthesis.
Note that this representation may introduce redundant brackets.
`kwargs` can be used to specify how to display syntax tokens/trees under
some specific conditions.
Expand Down Expand Up @@ -84,7 +84,7 @@ the function can simply be:
!!! warning
The `syntaxstring` for syntax tokens (e.g., propositions, operators) should not be
prefixed/suffixed by whitespaces, as this may cause ambiguities upon *parsing*.
For similar reasons, `syntaxstring`s should not contain parenthesis (`'('`, `')'`),
For similar reasons, `syntaxstring`s should not contain brackets (`'('`, `')'`),
and, when parsing in function notation, commas (`','`).
See also [`parsebaseformula`](@ref).
Expand Down
1 change: 1 addition & 0 deletions src/propositional-logic.jl
Original file line number Diff line number Diff line change
Expand Up @@ -195,6 +195,7 @@ Dict{Proposition{Int64}, Bool} with 4 entries:
julia> t1 = TruthDict(1:4, false); t1[5] = true; t1
TruthDict wrapping:
Dict{Proposition{Int64}, Bool} with 4 entries:
Proposition{Int64}(5) => 1
Proposition{Int64}(4) => 0
Proposition{Int64}(2) => 0
Proposition{Int64}(3) => 0
Expand Down

0 comments on commit 82758a8

Please sign in to comment.