# Inference-based decentralized control framework.
# copyright Richard St-Denis, Universite de Sherbrooke, 2016.
#
# Reference:
#   [1] Inference-based ambiguity management in decentralized decision-making:
#       decentralized control of discrete event systems,
#       R. Kumar and S. Takai,
#       IEEE Transactions on Automatic Control,
#       52 (10), 2007, 1783-1794.

$E0D0 = "
fun %s[g: (one Automaton), e: (one EventSet)] [(set StateSpace)] {
  (g.states).select {|x1|
    some(x2: %s) {
      let(delta: x1 ** e ** x2) { delta.in? g.transition } } }
}
"

$EiDi = "
fun %s[g: (one Automaton), e: (one EventSet)] [(set StateSpace)] {
  (%s(g, e)).select { |x1|
    all(i: getIn(e)) {
      some(x2: %s(g, e), y: NFAStateSpace) {
        (i ** y).in? getSupervisorStates and
        (i ** y ** x2).in? getNFADFA and
        (i ** y ** x1).in? getNFADFA } } }
}
"

$AllEiDi = ''
(1..$N+1).each{|i|
  $AllEiDi += "#{$EiDi % ['e'+i.to_s, 'e'+(i-1).to_s, 'd'+(i-1).to_s]}\n  " +
              "#{$EiDi % ['d'+i.to_s, 'd'+(i-1).to_s, 'e'+(i-1).to_s]}\n  "}

$nInf = "
pred nInf[g: (one Automaton)] {
  all(e: g.ctrlEvents) {
    e%s(g, e) == none or d%s(g, e) == none }
}
"

def gen_ned(nm1,nm2)
$ne = "
fun n#{nm1}[g: (one Automaton), i: (one Int), e: (one EventSet)] [
       (set NFAStateSpace ** Int)] {
  let(statei: i.(getSupervisorStates)) {\n"
(0..$N+1).each{|i|
  $ne += "#{' '*2}(statei.select { |y| \n"
  (0..i-1).each{|j|
  $ne += "#{' '*4}(some(x#{j}: g.states) { ((i ** y ** x#{j}).in? getNFADFA) and\n" + 
           "#{' '*27}(x#{j}.in? #{nm2}#{j}(g, e)) }) and\n"}
  $ne += "#{' '*4}(all(x: g.states) { if (i ** y ** x).in? getNFADFA\n" +
         "#{' '*27}not x.in? #{nm2}#{i}(g, e) end }) } ** #{i})"
  $ne += "#{i == $N+1 ? " }\n}" : " +\n"}" }
return $ne
end

$theory = "
alloy :NInf do
  abstract sig NFAStateSpace [ ] { }
  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
      }

  # E and D functions.
  #{$E0D0 % ['e0', 'g.states - getBadStates']}
  #{$E0D0 % ['d0', 'getBadStates']}
  #{$AllEiDi}

  # N-inference observability property.
  #{$nInf % ([$N+1] * 2)}

  # Ambiguity level of an enablement and a disablement decision.
  # by a supervisor
  #{gen_ned('e', 'd')}
  #{gen_ned('d', 'e')}

  abstract sig Decision [ ] { }
  one sig Enabled extends Decision [ ] { }
  one sig Disabled extends Decision [ ] { }
  one sig Unsure extends Decision [ ] { }

  # Local control decision for a controllable event.
  fun lc[g: (one Automaton), i: Int, e: (one EventSet)] [
         NFAStateSpace ** Decision] {
    (NFAStateSpace).select { |y|
      some(j1, j2: Int) {
        ((y ** j1).in? nd(g, i, e)) and
        ((y ** j2).in? ne(g, i, e)) and (j1 < j2) } } ** Disabled +
    (NFAStateSpace).select { |y|
      some(j1, j2: Int) {
        ((y ** j1).in? nd(g, i, e)) and
        ((y ** j2).in? ne(g, i, e)) and (j1 > j2) } } ** Enabled +
    (NFAStateSpace).select { |y|
      some(j1, j2: Int) {
        ((y ** j1).in? nd(g, i, e)) and
        ((y ** j2).in? ne(g, i, e)) and (j1 == j2) } } ** Unsure
  }

  # Ambiguity level for a controllable event.
  fun lna[g: (one Automaton), i: Int, e: (one EventSet)] [
          NFAStateSpace ** Int] {
    (NFAStateSpace ** Int).select { |y, k| ((y ** k).in? nd(g, i, e)) and
      (some(j: Int) { ((y ** j).in? ne(g, i, e)) and (k < j) }) }
  }

  fun lnb[g: (one Automaton), i: Int, e: (one EventSet)] [
          NFAStateSpace ** Int] {
    (NFAStateSpace ** Int).select { |y, k| ((y ** k).in? ne(g, i, e)) and
      (some(j: Int) { ((y ** j).in? nd(g, i, e)) and (k <= j) }) }
  }
  # The function ln has been separated into two parts due a bug in ARby
  fun ln[g: (one Automaton), i: Int, e: (one EventSet)] [
         NFAStateSpace ** Int] {
    lna(g, i, e) + lnb(g, i, e)
  }

  fun allLn[g: (one Automaton), e: (one EventSet)] [
            NFAStateSpace ** Int] {
    (NFAStateSpace ** Int).select { |s, k|
      some(i: getIn(e)) { (s ** k).in? ln(g, i, e) } }
  }

  # Global control decision.
  fun getSi_States[g: (one Automaton), e: (one EventSet),
                   d: (one Decision)] [StateSpace] {
    (g.states).select { |x|
      some(k: Int) { ((x ** k).in? getAlln) and
        all(i: getIn(e)) {
          let(y: (i).(getNFADFA()).(x)) {
            if (y ** k).in? ln(g, i, e) then
               (y ** d).in? lc(g, i, e) end } } } }
  }

  fun si[g: (one Automaton), e: (one EventSet)] [StateSpace ** Decision] {
    let(enabled_states: getSi_States(g, e, Enabled),
        disabled_states: getSi_States(g, e, Disabled)) {
      let(unsure_states: g.states - (enabled_states + disabled_states)) {
        (enabled_states ** Enabled) +
        (disabled_states ** Disabled) +
        (unsure_states ** Unsure) } }
  }

  # Auxiliairy functions.
  fun getBadStates[] [(set StateSpace)] {
    none + Problem.bad_states
  }

  fun getinSigma[] [(set EventSet ** Int)] {
    (none ** none) + Problem.in_sigma
  }

  fun getSupervisorStates[] [(set Int ** NFAStateSpace)] {
    (none ** none) + Problem.supervisor_states
  }

  fun getNFADFA[] [(set Int ** NFAStateSpace ** StateSpace)] {
    (none ** none ** none) + Problem.nfa_dfa
  }

  fun getIn[e: (one EventSet)] [Int] {
    (Int).select {|i| (e ** i).in? getinSigma }
  }

  fun getAlln[] [(set StateSpace ** Int)] {
    (none ** none) + Problem.minAmbiguityLevel
  }
end
"