# State-based control of discrete event systems under total observation.
# copyright Richard St-Denis, Universite de Sherbrooke, 2016.
#
# References:
#   [1] Supervisory control theory with Alloy,
#       B. Fraikin, M. Frappier and R. St-Denis,
#       Science of Computer Programming,
#       94 (2), 2014, 217-237.
#
#   [2] Control of parameterized discrete event systems,
#       H. Bherer, J. Desharnais and R. St-Denis,
#       Discrete Event Dynamic Systems: Theory and Applications,
#       19 (2), 2009, 213-265.

alloy :SBCDES do
  abstract sig StateSpace [ ] { }
  abstract sig EventSet [ ] { }

  abstract sig Automaton [
      states: (set StateSpace),
      initialState: (one StateSpace),
      markedStates: (set StateSpace),
      events: (set EventSet),
      ctrlEvents: (set EventSet),
      transition: (set StateSpace ** EventSet ** StateSpace),
    ] {
       initialState.in? states and
       markedStates.in? states and
       ctrlEvents.in? events and
       transition.(this.states).(this.events).in? states and
       events.(states.(this.transition)).in? states and
       states.(this.transition).(this.states).in? events
      }

# ----------
#
# Notation: g denotes a generator (automaton);
#           q, q1, q2 denote a predicate viewed as a set of states;
#           sigma denotes an event;
#           x, src, dst denote states;
#           x, y, z denote bound variables.

# ----------  Elementary functions for debugging test only.

  fun getInitialState[g: (one Automaton)] [(one StateSpace)] {
    g.initialState
  }

  fun getMarkedStates[g: (one Automaton)] [(set StateSpace)] {
    g.markedStates
  }

  fun findMarkedStates[g: (one Automaton)] [(set StateSpace)] {
    (StateSpace).select { |x| x.in? g.markedStates }
  }

  fun getInitialMarkedState[g: (one Automaton)] [(lone StateSpace)] {
    g.initialState & g.markedStates
  }

  fun getSrc[g: (one Automaton)] [(set StateSpace)] {
    g.transition.(g.states).(g.events)
  }

  fun getDst[g: (one Automaton)] [(set StateSpace)] {
    g.events.(g.states.(g.transition))
  }

  fun getEvt[g: (one Automaton)] [(set EventSet)] {
    g.states.(g.transition).(g.states)
  }

  fun getSrcEvt[g: (one Automaton)] [(set StateSpace ** EventSet)] {
    g.transition.(g.states)
  }

  fun getEvtDst[g: (one Automaton)] [(set EventSet ** StateSpace)] {
    g.states.(g.transition)
  }

  fun getEvtSrcDst[g: (one Automaton)] [
                   (set EventSet ** StateSpace ** StateSpace)] {
    (EventSet ** StateSpace ** StateSpace).select { |x, y, z|
      x.in? g.events and
      y.in? g.states and
      z.in? g.states and
      (y ** x ** z).in? g.transition }
  }

# ---------- Basic predicate transformers.

  pred wp[g: (one Automaton),
          sigma: (one EventSet), q: (set StateSpace), x: (one StateSpace)] {
  # Weakest precondition.
    some(dst: g.states) { (x ** sigma ** dst).in? g.transition and
                          dst.in? q }
  }

  pred wlp[g: (one Automaton),
           sigma: (one EventSet), q: (set StateSpace), x: (one StateSpace)] {
  # Weakest liberal precondition.
    not (some(dst: g.states) { (x ** sigma ** dst).in? g.transition }) or
    some(dst: g.states) { (x ** sigma ** dst).in? g.transition and
                          dst.in? q }
  }

# ---------- Controllable field and its properties.

  fun getTrs[g: (one Automaton),
             e: (set EventSet)] [(set StateSpace ** StateSpace)] {
  # Return the unlabelled (binary) transition relation of g
  # w.r.t. a set of events.
    (StateSpace ** StateSpace).select { |src, dst|
       some(sigma: e) { (src ** sigma ** dst).in? g.transition } }
  }

  fun ctrlField[g: (one Automaton), q: (set StateSpace)] [(set StateSpace)] {
  # Return the weakly controllable field of a predicate.
    let(bad: g.states - q) {
      g.states - (getTrs(g, g.events-g.ctrlEvents).rclosure.(bad)) }
  }

  pred idempotent[g: (one Automaton), q: (set StateSpace)] {
  # The controllable field is idempotent.
    ctrlField(g, q) == ctrlField(g, ctrlField(g, q))
  }

  pred weaklyCtrl[g: (one Automaton), q: (set StateSpace)] {
  # Check if a predicate is weakly controllable.
    q.in? ctrlField(g, q)
  }

# ---------- Bas event set (A).

  fun badEventSetA[g: (one Automaton),
                   q: (set StateSpace), x: (one StateSpace)] [(set EventSet)] {
  # Return the bad event set (A, see reference [2]).
    (g.ctrlEvents).select { |sigma| not wlp(g, sigma, q, x) }
  }

# ---------- Reachability (R) and coreachability properties (nonblocking).

  fun getRTrs[g: (one Automaton),
              q: (set StateSpace)] [(set StateSpace ** StateSpace)] {
  #  Return the unlabelled (binary) transition relation of g
  #  w.r.t. the reachability predicate definition (R, see reference [2]).
    (StateSpace ** StateSpace).select { |src, dst|
      some(sigma: g.events) { (src ** sigma ** dst).in? g.transition and
                              # not sigma.in? badEventSetA(g, q, src) and
                              wp(g, sigma, q, src) } }
  }

  fun reachField[g: (one Automaton), q: (set StateSpace)] [(set StateSpace)] {
  # Return the reachability predicate R (R, the set of reachable good states,
  # see reference [2]).
    (g.initialState & q).*getRTrs(g, q)
  }

  fun coreachField[g: (one Automaton), q: (set StateSpace)] [(set StateSpace)] {
  # Return the set of coreachable good states.
    let(good: q.<(getTrs(g, g.events)).>(q)) {
          (good.rclosure).>(g.markedStates).(g.states) }
  }

# ---------- Controllability properties.

  pred weaklyControllable[g: (one Automaton), q: (set StateSpace)] {
  # weak controllability is equivalent to Sigma_u invariant.
    q.in? ((g.states).select { |x|
           all(sigma: g.events - g.ctrlEvents) {
                      wlp(g, sigma, q, x) } })
  }

  pred controllable[g: (one Automaton), q: (set StateSpace)] {
  # The controllability property.
    weaklyControllable(g, q) and q.in? reachField(g, q)
  }

  pred propertyCtrl[g: (one Automaton), q: (set StateSpace)] {
  # If q is weakly controllable, then reachable(g, q) is controllable.
    weaklyControllable(g, q) and controllable(g, reachField(g, q))
  }

# ---------- Template for the 1st first strategy.

  fun nbcField[g: (one Automaton), q: (set StateSpace)] [(set StateSpace)] {
  # Template used to derive the supremal controllable predicate.
    ctrlField(g, q) & reachField(g, q) & coreachField(g, q)
  }

# ---------- Templates for the 2nd strategy.

  pred isNBC[nbcq: (set StateSpace), g: (one Automaton), q: (set StateSpace)] {
  # Check if nbcq is a nonblocking controllable subpredicate of q.
    let(goodTrs: nbcq.<(getTrs(g, g.events)).>(nbcq),
        unctrlTrs: getTrs(g, g.events-g.ctrlEvents)) {
      # good states are reachable from the initial state
      nbcq.in? ((g.initialState).*goodTrs) and
      # good states are coreachable to the set of marked states
      all(x: nbcq) {
        some(y: nbcq) { y.in? ((x.*goodTrs) & g.markedStates) } } and
      # good states are closed under uncontrollable transitions
      nbcq.(unctrlTrs).in? nbcq and
      # no sequence of uncontrollable transitions leads to a state
      # that violates the control specification
      no() { ((unctrlTrs.rclosure).(g.states-q) & nbcq) } and
      # not the trivial predicate False
      not nbcq == none }
  }

  pred isWeakerNBC[q1, q2: (set StateSpace), g: (one Automaton),
                   q: (set StateSpace)] {
  # Check if q1 is a weaker predicate than q2,
  # which are both nonblocking and controllable.
    isNBC(q1, g, q) and
    isNBC(q2, g, q) and
    q2.in? q1 and not (q1 == q2)
  }

# ---------- State feedback functions.

  pred f_Sigma[g: (one Automaton), q: (set StateSpace),
               sigma: (one EventSet), x: (one StateSpace)] {
  # Family of predicates used to define f.
    q == nbcField(g, q) and (not sigma.in? badEventSetA(g, q, x))
  }

  fun sfbc[g: (one Automaton),
           q: (set StateSpace)] [(set StateSpace ** EventSet)] {
  # Return the SFBC function that corresponds to a weak controllable q,
  # but for the set of disabled events at state x.
    (StateSpace ** EventSet).select { |x, sigma|
       x.in? g.states and sigma.in? g.events and
       x.in? q and sigma.in? badEventSetA(g, q, x) }
  }

  fun sfbcEnabled[g: (one Automaton),
                  q: (set StateSpace)] [(set StateSpace ** EventSet)] {
  # Return the SFBC function that corresponds to a weak controllable q,
  # but for the set of enabled events at state x.
    ((StateSpace ** EventSet).select { |src, sigma|
        src.in? g.states and sigma.in? g.events and
        src.in? q and
        some(dst: g.states) { dst.in? q and
                              (src ** sigma ** dst).in? g.transition } }) -
    sfbc(g, q)
  }
end