module SBCDES_Total_Observation[StateSpace, EventSet]

-- State-based control of discrete event systems.
--   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.

-- Operations on ternary relations
   open util/ternary as UTIL

-- Automaton

abstract sig Automaton
{
 states             : set StateSpace,
 events             : set EventSet,
 controllableEvents : set EventSet,
 transition         : set StateSpace -> EventSet -> StateSpace,
 initialState       : one StateSpace,
 markedStates       : set StateSpace
}
{
 controllableEvents in events
 transition.dom + transition.ran in states
 transition.mid in events
 initialState in states
 markedStates in states
}


-- Weakest precondition and weakest liberal precondition

pred wp[G: one Automaton,
        sigma: one EventSet, Q: set StateSpace, x: one StateSpace]
{
 (some x' : G.states | x->sigma->x' in G.transition and x' in Q)
}

pred wlp[G: one Automaton,
         sigma: one EventSet, Q: set StateSpace, x: one StateSpace]
{
 not (some x' : G.states | x->sigma->x' in G.transition)
  or (some x' : G.states | x->sigma->x' in G.transition and x' in Q)
}

fun GetTransition[G: one Automaton, E: set EventSet] : StateSpace -> StateSpace
{ -- return the unlabelled (binary) transition relation of G
  --   w.r.t. the event set E
  -- { x, x' : G.states | (some sigma : G.events |
  --                            sigma in E
  --                        and x->sigma->x' in G.transition ) }
 E.(UTIL/flip12[G.transition])
}

fun ControllableField[G: one Automaton, Q: set StateSpace] : set StateSpace
{
 let badStates = G.states - Q |           -- { x : G.states | not x in Q }
 G.states - (*(GetTransition[G, G.events-G.controllableEvents]).badStates)
}

pred Idempotent[G: one Automaton, Q: set StateSpace]
{
 ControllableField[G, Q] = ControllableField[G, ControllableField[G, Q]]
}

pred WeaklyCtrl[G: one Automaton, Q: set StateSpace]
{
 Q in ControllableField[G, Q]
}

-- Bad event set

fun A[G: one Automaton,
      Q: set StateSpace, x: one StateSpace] : set EventSet
{
 { sigma : G.controllableEvents | not wlp[G, sigma, Q, x] }
}

-- Reachability predicates

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

fun R[G: one Automaton, Q: set StateSpace] : set StateSpace
{
 (G.initialState & Q).*(GetRTransition[G, Q])
}

-- Controllability properties

pred WeaklyControllable[G: one Automaton, Q: set StateSpace]
{ -- "weak controllability" is equivalent to "Sigma_u invariant"
 Q in { x : G.states | all sigma : G.events - G.controllableEvents |
                           wlp[G, sigma, Q, x] }
}

pred Controllable[G: one Automaton, Q: set StateSpace]
{
 WeaklyControllable[G, Q] and Q in R[G, Q]
}

pred Property[G: one Automaton, Q: set StateSpace]
{ -- if Q is weakly controllable, then R(G, Q) is controllable
 WeaklyControllable[G, Q] and Controllable[G, R[G, Q]]
}

-- Nonblocking predicate

fun Nonblocking[G: one Automaton, Q: set StateSpace] : set StateSpace
{
 let goodTransitions = Q <: GetTransition[G, G.events] :> Q |
     { x : G.states |     x in Q
                      and (some x <: *goodTransitions :> G.markedStates) }
}

-- Template used to derive the supremal controllable predicate

fun NBC[G: one Automaton, Q: set StateSpace] : set StateSpace
{
 ControllableField[G, Q] & R[G, Q] & Nonblocking[G, Q]
}

pred IsNBC[NBCQ: set StateSpace, G: one Automaton, Q: set StateSpace]
{
 let goodTransitions = NBCQ <: GetTransition[G, G.events] :> NBCQ,
     unctrlTransitions = GetTransition[G, G.events-G.controllableEvents] |
     {
          -- good states are reachable from the initial state
          NBCQ in (G.initialState).*goodTransitions
          -- good states are coreachable to the set of marked states
      and (all x : NBCQ | some (x.*goodTransitions & G.markedStates))
          -- good states are closed under uncontrollable transitions
      and NBCQ.unctrlTransitions in NBCQ
          -- no sequence of uncontrollable transitions leads to a state
          -- that violates the control specification
      and no (*unctrlTransitions.(G.states-Q) & NBCQ)
     }
}

pred IsWeakerNBC[Q'', Q': set StateSpace, G: one Automaton, Q: set StateSpace]
{
     IsNBC[Q', G, Q]
 and IsNBC[Q'', G, Q]
 and Q' in Q'' and not (Q'= Q'')
}

-- State feedback control functions

pred f_sigma[G: one Automaton, Q: set StateSpace,
             sigma: one EventSet, x: one StateSpace]
{ -- Family of predicates used to define f
 Controllable[G, Q] and (not sigma in A[G, Q, x])
}

fun SFBC[G: one Automaton, Q: set StateSpace] : StateSpace -> EventSet
{ -- return the SFBC function that corresponds to a weak controllable Q,
  --    but for the set of disabled events at state x
  -- normal call: { x : G.states, sigma : G.events | 
  --                         (x->sigma in SFBC[G, ControllableField[G, Q]])
  --                     and (x in R[G, ControllableField[G, Q]]) } 
 { x : G.states, sigma : G.events | -- x in Q and  -- to avoid irrelevant pairs
                                    sigma in A[G, Q, x] }
}

fun SFBCEnabled[G: one Automaton, Q: set StateSpace] : StateSpace -> EventSet
{ -- return the SFBC function that corresponds to a weak 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' in Q and x->sigma->x' in G.transition) }
 - SFBC[G, Q]
}