module SBCDES_Partial_Observation[StateSpace, EventSet, ObservationSpace]

-- State-based control of discrete event systems under partial observation.
--   H. Bherer, J. Desharnais and R. St-Denis,
--   Control of parameterized discrete event systems,
--   Discrete Event Dynamic Systems: Theory and Applications,
--   19 (2), 2009, 213-265.
-- copyright Richard St-Denis, Universite de Sherbrooke, 2013.

open SBCDES_Total_Observation[StateSpace, EventSet]

-- Predicate transformers

fun M0[G: one Automaton, M: StateSpace->ObservationSpace,
       Q: set StateSpace] : set ObservationSpace
{
 { y : ObservationSpace | some x : G.states | M[x] = y and x in Q }
}

fun M1M[G: one Automaton, M: StateSpace->ObservationSpace,
        Q: set StateSpace] : set StateSpace
{
 { x : G.states | some x' : G.states | M[x] = M[x'] and x' in Q }
}

-- Bad event sets

fun A_hat[G: one Automaton, M: StateSpace->ObservationSpace,
          Q: set StateSpace, y: one ObservationSpace] : set EventSet
{
 { sigma : G.controllableEvents | some x : G.states |
                                      M[x] = y and
                                  not wlp[G, sigma, Q, x] }
}

fun A_breve[G: one Automaton, M: StateSpace->ObservationSpace,
            Q: set StateSpace, y: one ObservationSpace] : set EventSet
{
 { sigma : G.controllableEvents | some x : G.states |
                                      M[x] = y and x in Q
                                  and not wlp[G, sigma, Q, x] }
}

-- Reachability predicates

fun GetR_hatTransition[M: StateSpace->ObservationSpace,
                       G: one Automaton, Q: set StateSpace] : StateSpace -> StateSpace
{ -- return the unlabelled transition relation w.r.t. the rechability
  -- predicate definition R hat
 { x, x' : G.states | (some sigma : G.events |
                            x->sigma->x' in G.transition
                        and (not sigma in A_hat[G, M, Q, M[x]])
                        and wp[G, sigma, Q, x]) }
}

fun GetR_breveTransition[M: StateSpace->ObservationSpace,
                         G: one Automaton, Q: set StateSpace] : StateSpace -> StateSpace
{ -- return the unlabelled transition relation w.r.t. the rechability
  -- predicate definition R breve
 { x, x' : G.states | (some sigma : G.events |
                            x->sigma->x' in G.transition
                        and (not sigma in A_breve[G, M, Q, M[x]])
                        and wp[G, sigma, Q, x]) }
}

fun R_hat[M: StateSpace->ObservationSpace,
          G: one Automaton, Q: set StateSpace] : set StateSpace
{
 (G.initialState & Q).*(GetR_hatTransition[M, G, Q])
}

fun R_breve[M: StateSpace->ObservationSpace,
            G: one Automaton, Q: set StateSpace] : set StateSpace
{
 (G.initialState & Q).*(GetR_breveTransition[M, G, Q])
}

-- Controllability properties

pred StrongM_controllable[M: StateSpace->ObservationSpace,
                          G: one Automaton, Q: set StateSpace]
{
     Q in { x : G.states | all sigma : G.events - G.controllableEvents |
                               wlp[G, sigma, Q, x] }
 and Q in R_hat[M, G, Q]
}

pred M_controllable[M: StateSpace->ObservationSpace,
                    G: one Automaton, Q: set StateSpace]
{
     Q in { x : G.states | all sigma : G.events - G.controllableEvents |
                               wlp[G, sigma, Q, x] }
 and Q in R_breve[M, G, Q] 
}

pred Property[M: StateSpace->ObservationSpace,
               G: one Automaton, Q: set StateSpace]
{ -- if Q is weakly controllable, then R_breve(G, Q) is M-controllable
 WeaklyControllable[G, Q] and M_controllable[M, G, R_breve[M, G, Q]]
}

-- Normality property

pred Normal[M: StateSpace->ObservationSpace,
            G: one Automaton, Q: set StateSpace]
{
 M1M[G, M, Q] in Q
}

-- Template used to derive the supremal controllable and normal predicate

fun CN[M: StateSpace->ObservationSpace,
       G: one Automaton, Q: set StateSpace] : set StateSpace
{
   ControllableField[G, Q] & R[G, Q]
 & { x : StateSpace | x in Q and M1M[G, M, Q] in Q }
}

-- Template used to derive the supremal nonblocking
-- controllable and normal predicate

fun NBCN[M: StateSpace->ObservationSpace,
       G: one Automaton, Q: set StateSpace] : set StateSpace
{
   ControllableField[G, Q]
 & R[G, Q] & { x : StateSpace | x in Q and M1M[G, M, Q] in Q }
 & Nonblocking[G, Q]
}

-- Template used to derive the supremal strongly M-controllable predicate

fun SC[M: StateSpace->ObservationSpace,
       G: one Automaton, Q: set StateSpace] : set StateSpace
{
 ControllableField[G, Q] & R_hat[M, G, Q]
}

-- Template used to derive the supremal nonblocking
-- strongly M-controllable predicate

fun NBSC[M: StateSpace->ObservationSpace,
         G: one Automaton, Q: set StateSpace] : set StateSpace
{
 ControllableField[G, Q] & R_hat[M, G, Q] & Nonblocking[G, Q]
}


-- State feedback control functions

pred f_sigma_hat[M: StateSpace->ObservationSpace, G: one Automaton, Q: set StateSpace,
                 sigma: one EventSet, x: one StateSpace]
{
 StrongM_controllable[M, G, Q] and (not sigma in A_hat[G, M, Q, x.M])
}

pred f_sigma_breve[M: StateSpace->ObservationSpace, G: one Automaton, Q: set StateSpace,
                   sigma: one EventSet, x: one StateSpace]
{
 M_controllable[M, G, Q] and (not sigma in A_breve[G, M, Q, x.M])
}

fun SFBC_hat[M: StateSpace->ObservationSpace,
             G: one Automaton, Q: set StateSpace] : StateSpace -> EventSet
{ -- return the SFBC function that corresponds to a strongly M-controllable Q,
  --    but for the set of disabled events at state x
 { x : G.states, sigma : G.events | sigma in A_hat[G, M, Q, M[x]] }
}

fun SFBC_hatEnabled[M: StateSpace->ObservationSpace,
                    G: one Automaton, Q: set StateSpace] : StateSpace -> EventSet
{ -- return the SFBC function that corresponds to a strongly M-controllable Q, 
  --    but for the set of enabled events at state x
   { x : G.states, sigma : G.events |
            x in Q
         and
            (some x' : G.states | x->sigma->x' in G.transition) } 
 - SFBC_hat[M, G, Q]
}

fun SFBC_breve[M: StateSpace->ObservationSpace,
               G: one Automaton, Q: set StateSpace] : StateSpace -> EventSet
{ -- normal call: SFBC_breve[M, G, R_breve[M, G, ControllableField[G, Q]]]
 { x : G.states, sigma : G.events |     x in Q  -- to avoid irrelevant pairs
                                    and sigma in A_breve[G, M, Q, M[x]] }
}

fun SFBC_breveEnabled[M: StateSpace->ObservationSpace,
                      G: one Automaton, Q: set StateSpace] : StateSpace -> EventSet
{
   { x : G.states, sigma : G.events |
             x in Q
         and
            (some x' : G.states | x->sigma->x' in G.transition) }
 - SFBC_breve[M, G, Q]
}

fun SFBC_hatF[M: StateSpace->ObservationSpace,
                G: one Automaton, Q: set StateSpace] : StateSpace -> EventSet
{ -- from the SFBC under total observation
  -- normal call : { x : G.states, sigma : G.events |
  --                         (x->sigma in SFBC_breveF[M, G, Q])
  --                     and (x in R_hat[M, G, ControllableField[G, Q]]) }
 let fc = SFBC[G, ControllableField[G, Q]] |
     { x : G.states, sigma : G.events |
           (some x' : G.states |
                         x in ControllableField[G, Q]  -- to avoid irrelevant pairs
                     and M[x] = M[x']
                     and x'->sigma in fc) }
}

fun SFBC_breveF[M: StateSpace->ObservationSpace,
                G: one Automaton, Q: set StateSpace] : StateSpace -> EventSet
{ -- from the SFBC under total observation
  -- normal call : { x : G.states, sigma : G.events |
  --                         (x->sigma in SFBC_breveF[M, G, Q])
  --                     and (x in R_breve[M, G, ControllableField[G, Q]]) }
 let fc = SFBC[G, ControllableField[G, Q]] |
     { x : G.states, sigma : G.events |
           (some x' : G.states |
                         x in ControllableField[G, Q]  -- to avoid irrelevant pairs
                     and M[x] = M[x']
                     and x' in ControllableField[G, Q] and x'->sigma in fc) }
}