Add initial ProductIMDP framework

src/models/DFA.jl

@@ -0,0 +1,149 @@
+"""
+    DFA{
+        T <: TransitionFunction,  
+        VT <: AbstractVector{Int32},
+        DA <: AbstractDict{String, Int32}
+    }
+
+A type representing Deterministic Finite Automata (DFA) which are finite automata with deterministic transitions.
+
+Formally, let ``(Z, 2^{AP}, \\tau, z_0, Z_{ac})`` be an DFA, where 
+- ``Z`` is the set of states,
+- ``Z_{ac} \\subseteq Z`` is the set of accepting states,
+- ``z_0`` is the initial state,
+- ``2^{AP}`` is the power set of automic propositions, and
+- ``\\tau : |Z| \\times |2^{AP}| => |Z|`` is the deterministic transition function, for each state-input pair.
+
+Then the ```DFA``` type is defined as follows: indices `1:num_states` are the states in ``Z``, 
+`transition` represents ``\\tau``, inputs are implicitly defined by indices enumerating the alphabet, and `initial_states` is the set of initial states ``z_0``. 
+See [TransitionFunction](@ref) for more information on the structure of the transition function.
+
+### Fields
+- `transition::T`: transition function where columns represent inputs and rows source states.
+- `initial_state::Int32`: initial states.
+- `accepting_states::VT`: vector of accepting states
+- `alphabetptr::DA`: mapping from input to index.
+
+"""
+
+struct DFA{
+    T <: TransitionFunction,  
+    VT <: AbstractVector{Int32},
+    DA <: AbstractDict{String, Int32}
+} <: DeterministicAutomata
+    transition::T # : |Z| x |2^{AP}| => |Z|   
+    initial_state::Int32 #z0
+    accepting_states::VT #Z_ac
+    alphabetptr::DA
+    num_states::Int32
+    num_alphabet::Int32
+end
+
+
+
+function DFA(
+    transition::TransitionFunction,
+    initial_state::Int32,
+    accepting_states::AbstractVector{Int32}
+    alphabet::AbstractVector{String},
+)
+    checkdfa!(transition, initial_state, accepting_state, alphabet) 
+
+    alphabetptr, num_alphabet = alphabet2index(alphabet)
+
+    num_states = getsize_dfa!(transition)
+
+    return DFA(
+        transition,
+        initial_states,
+        accepting_state,
+        alphabetptr,
+        num_states,
+        num_alphabet,
+    )
+end
+
+
+"""
+    Given vector of letters L, compute power set 2^L 
+    Returns the alphabet (powerset) and corresponding index as Dictionary
+"""
+function letters2alphabet(
+    letters::AbstractVector{String},
+)   
+
+    alphabet = [""]; #already add empty set
+
+    for letter in letters
+        append!(alphabet, string.(alphabet, letter))
+    end 
+
+    return alphabet2index(alphabet)
+end
+
+"""
+    Given vector of alphabet 2^L, maps its index for lookup
+    Returns dictionary, assume same indices used in Transition function.
+"""
+function alphabet2index(alphabet::AbstractVector{String})
+    N = length(alphabet);
+    idxs = collect(1:N);
+
+    alphabet_idx = Dict{String, Int32}(zip(alphabet, idxs)); 
+    return alphabet_idx, N
+end
+
+
+"""
+Check given dfa valid
+"""
+function checkdfa!(transition::TransitionFunction,
+                    initial_state::Int32,
+                    accepting_state::AbstractVector{Int32}
+                    alphabet::AbstractVector{String},
+                    )
+    # check z0 and Z_ac in Z, check size(alphabet) == size(transition dim)
+    # @assert size(transition.transition, 1) == length(alphabet) "size of alphabet match"
+    # @assert all(accepting_state .>= 1) "all accepting states exists"
+    # @assert all(accepting_state .<= size(transition.transition, 2)) "all accepting states exists"
+    # @assert initial_state .>= 1 "initial state exists"
+    # @assert initial_state .<= size(transition.transition, 2) "initial state exists"
+
+
+    if size(transition.transition, 1) != length(alphabet)
+        throw(
+            throw(DimensionMismatch("The size of alphabet ($(length(alphabet))) is not equal to the size of the transition column $(size(transition.transition, 1))",))
+        )
+    end
+
+    if !all(accepting_state .>= 1)
+        throw(
+            throw(ArgumentError("Next state index cannot be zero or negative"))
+        )
+    end
+
+    if !all(accepting_state .<= size(transition.transition, 2))
+        throw(
+            throw(ArgumentError("Next state index cannot be larger than total number of states"))
+        )
+    end
+
+    if initial_state < 1
+        throw(
+            throw(ArgumentError("Initial state index cannot be zero or negative"))
+        )
+    end
+
+    if initial_state > size(transition.transition, 2)
+        throw(
+            throw(ArgumentError("Initial state index cannot be larger than total number of states"))
+        )
+    end
+
+
+end
+
+function getsize_dfa!(transition)
+    return size(transition.transition, 2)
+
+#TODO add accessor methods 

src/models/DeterministicAutomata.jl

@@ -0,0 +1,8 @@
+"""
+    DeterministicAutomata
+
+An abstract type for deterministic automata.
+"""
+abstract type DeterministicAutomata end
+
+

src/models/ProductIntervalMarkovDecisionProcess.jl

@@ -0,0 +1,84 @@
+"""
+    struct ProductIntervalMarkovDecisionProcessDFA{
+        D <: DFA,
+        M <: IntervalMarkovDecisionProcess,
+        L <: AbstractLabelling,
+    }
+
+A type representing the product between Interval Markov Decision Processes (IMDP) and Deterministic Finite Automata (DFA). 
+
+Formally, let ``(S^{\\prime}, A, \\Gamma^{\\prime}, S^{\\prime}_{ac}, S^{\\prime}_{0}, L)`` be an product interval Markov decision process DFA, where 
+- ``S^{\\prime} = S \\times Z`` is the set of product states q = (s, z)``,
+- ``S^{\\prime}_{0} = S_0 \\times z_0 \\subset S^{\\prime}`` is the set of initial product states ``q = (s, z_0)``,
+- ``S^{\\prime}_{ac} = S \\times Z_{ac} \\subseteq S^{\\prime}`` is the set of accepting product states,
+- ``A`` is the set of actions,
+- ``\\Gamma^{\\prime} = \\{\\Gamma^{\\prime}_{q,a}\\}_{q \\in S^{\\prime}, a \\in A}`` is a set of interval ambiguity sets on the transition probabilities, for each product source-action pair, and
+- ``L : S => 2^{AP}`` is the labelling function that maps a state in the IMDP to an input to the DFA.
+
+Then the ```ProductIntervalMarkovDecisionProcessDFA``` type is defined as follows: DFA part of the product as a DFA object, IMDP part of the product as a IMDP object and a Labelling function to specify the relationshup between the DFA and IMDP.
+
+See [IntervalMarkovDecisionProcess](@ref) and [DFA](@ref) for more information on the structure, definition, and usage of the DFA and IMDP.
+
+### Fields
+- `imdp::M`: contains details for the IMDP
+- `dfa::D`: contains details for the DFA
+- `labelling_func::L`: the labelling function from IMDP states to DFA actions
+"""
+
+struct ProductIntervalMarkovDecisionProcessDFA{
+    D <: DFA,
+    M <: IntervalMarkovDecisionProcess,
+    L <: AbstractLabelling,
+} <: ProductIntervalMarkovProcess
+    imdp::M
+    dfa::D
+    labelling_func::L
+end
+
+function ProductIntervalMarkovDecisionProcessDFA(
+    imdp::IntervalMarkovDecisionProcess,
+    dfa::DFA,
+    labelling_func::AbstractLabelling
+)
+    checklabelling!(transition, initial_state, accepting_state, alphabet) 
+
+    return ProductIntervalMarkovDecisionProcessDFA(
+        imdp,
+        dfa,
+        labelling_func
+    )
+end
+
+
+
+"""
+Check given imdp, dfa, labelling combination is valid
+"""
+function checklabelling!(imdp::IntervalMarkovDecisionProcess,
+                         dfa::DFA,
+                         labelling_func::AbstractLabelling
+                        )
+
+    # check labelling states (input) match IMDP states
+    if labelling_func.num_inputs == imdp.num_states
+        throw(
+            DimensionMismatch(
+                "The number of IMDP states ($(imdp.num_states)) is not equal to number of mapped states  $(labelling_func.num_inputs) in the labelling function.",
+            ),
+        )
+    end
+
+    # check state labels (output) match DFA alphabet
+    if labelling_func.num_outputs <= dfa.num_alphabet # not all actions needed to be mapped so can be less but certainly not more
+        throw(
+            DimensionMismatch(
+                "The number of DFA inputs ($(dfa.num_alphabet)) is not equal to number of mapped states  $(labelling_func.num_outputs) in the labelling function.",
+            ),
+        )
+    end
+
+    # check all S in Labelfunc
+    # check all 2^{AP} in Label func
+
+
+end

src/models/ProductIntervalMarkovProcess.jl

@@ -0,0 +1,6 @@
+"""
+    ProductIntervalMarkovProcess
+
+An abstract type for product interval Markov processes including [`ProductIntervalMarkovDecisionProcessDFA`](@ref).
+"""
+abstract type ProductIntervalMarkovProcess <: IntervalMarkovProcess end

src/probabilities/Labelling.jl

@@ -0,0 +1,46 @@
+abstract type AbstractLabelling end
+
+"""
+    struct LabellingFunction{
+        T  <:Unsigned, 
+        VT <: AbstractVector{T}
+    }
+
+A type representing the labelling of IMDP states into DFA inputs.
+
+Formally, let ``L : S => 2^{AP}`` be a labelling function, where 
+- ``S`` is the set of IMDP states, and
+- ``2^{AP}`` is the power set of atomic propositions
+
+Then the ```LabellingFunction``` type is defined as vector which stores the mapping. 
+
+### Fields
+- `map::VT`: mapping function where indices are IMDP states and stored values are DFA inputs.
+- `num_inputs::Int32`: number of IMDP states accounted for in mapping.
+- `num_outputs::Int32`: number of DFA inputs accounted for in mapping.
+
+"""
+
+struct LabellingFunction{T<:Unsigned, VT <: AbstractVector{T}
+} <: AbstractLabelling
+    map::VT,
+    num_inputs::Int32,
+    num_outputs::Int32,
+end
+
+function LabellingFunction(map::VT) where {T<:Unsigned, VT <: AbstractVector{T}}
+
+    num_inputs, num_outputs = count_mapping!(map) 
+
+    return LabellingFunction(map, num_inputs, num_outputs)
+end
+
+"""
+Find size of input and output space of function
+"""
+function count_mapping!(map::AbstractVector)
+    num_inputs = length(map)
+    num_outputs = maximum(map)
+
+    return num_inputs, num_outputs
+end

src/probabilities/TransitionFunction.jl

@@ -0,0 +1,50 @@
+"""
+    struct TransitionFunction{
+        T<:Unsigned, 
+        MT <: AbstractMatrix{T}
+    }
+
+A type representing the determininistic transition function of a DFA.
+
+Formally, let ``T : |2^{AP}| \\times |Z| => |Z|`` be a transition function, where 
+- ``Z`` is the set of DFA states, and
+- ``2^{AP}`` is the power set of atomic propositions
+
+Then the ```TransitionFunction``` type is defined as matrix which stores the mapping. The column indices are the alphabet indices and the row indices represent the states.  
+
+### Fields
+- `transition::MT`: transition function.
+
+"""
+
+struct TransitionFunction{T<:Unsigned, MT <: AbstractMatrix{T}}
+    transition::MT
+end
+
+function TransitionFunction(transition::MT) where {T<:Unsigned, MT <: AbstractMatrix{T}}
+
+    checktransition!(transition) 
+
+    return TransitionFunction(transition)
+end
+
+"""
+Check given transition func valid
+"""
+function checktransition!(transition::AbstractMatrix)
+    # check only transition to valid states
+    # @assert all(transition .>= 1) "all transitioned states exists"
+    # @assert all(transition .<= size(transition, 2)) "all transitioned states exists"
+
+    if !all(transition .>= 1)
+        throw(
+            throw(ArgumentError("Transitioned state index cannot be zero or negative"))
+        )
+    end
+
+    if !all(transition .<= size(transition, 2))
+        throw(
+            throw(ArgumentError("Transitioned state index cannot be larger than total number of states"))
+        )
+    end
+end