Class: Lernen::Automaton::SPA

Inherits:
MooreLike show all
Defined in:
lib/lernen/automaton/spa.rb

Overview

SPA represents a system of procedural automata.

Note that this class takes ‘return_input` as the return symbol because this value is necessary to run this kind of automata correctly.

Constant Summary collapse

Conf =

Conf is a configuration of SPA run.

Data.define(:prev, :proc, :state)

Instance Attribute Summary collapse

Class Method Summary collapse

Instance Method Summary collapse

Methods inherited from MooreLike

#run_empty, #step

Methods inherited from TransitionSystem

random_transition_function, #run, #step, #to_dot, #to_mermaid

Constructor Details

#initialize(initial_proc, return_input, proc_to_dfa) ⇒ SPA

: (

  Call initial_proc,
  Return return_input,
  Hash[Call, DFA[In | Call]] proc_to_dfa
) -> void



42
43
44
45
46
47
48
 
# File 'lib/lernen/automaton/spa.rb', line 42

def initialize(initial_proc, return_input, proc_to_dfa)
  super()

  @initial_proc = initial_proc
  @return_input = return_input
  @proc_to_dfa = proc_to_dfa
end

Instance Attribute Details

#initial_proc ⇒ Object (readonly)

: Call



50
51
52
 
# File 'lib/lernen/automaton/spa.rb', line 50

def initial_proc
  @initial_proc
end

#proc_to_dfa ⇒ Object (readonly)

: Hash[Call, DFA[In | Call]]



52
53
54
 
# File 'lib/lernen/automaton/spa.rb', line 52

def proc_to_dfa
  @proc_to_dfa
end

#return_input ⇒ Object (readonly)

: Return



51
52
53
 
# File 'lib/lernen/automaton/spa.rb', line 51

def return_input
  @return_input
end

Class Method Details

.find_separating_word(alphabet, call_alphabet, spa1, spa2) ⇒ Object

Finds a separating word between ‘spa1` and `spa2`.

This method assume return symbols for two SPAs are the same. If they are not, this raises ‘ArgumentError`.

: [In, Call, Return] (

  Array[In] alphabet,
  Array[Call] call_alphabet,
  SPA[In, Call, Return] spa1,
  SPA[In, Call, Return] spa2
) -> (Array[In | Call | Return] | nil)

Raises:

  • (ArgumentError) 


139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
 
# File 'lib/lernen/automaton/spa.rb', line 139

def self.find_separating_word(alphabet, call_alphabet, spa1, spa2)
  raise ArgumentError, "Cannot find a separating word for different type automata" unless spa2.is_a?(spa1.class)
  unless spa1.return_input == spa2.return_input # steep:ignore
    raise ArgumentError, "Return symbols for two SPAs are different"
  end

  as1, ts1, rs1 = spa1.proc_to_atr_sequence(alphabet, call_alphabet)
  as2, ts2, rs2 = spa2.proc_to_atr_sequence(alphabet, call_alphabet)

  local_alphabet = alphabet.dup
  local_alphabet.concat((ts1.keys.to_set & ts2.keys.to_set).to_a) # steep:ignore

  call_alphabet.each do |proc|
    dfa1 = spa1.proc_to_dfa[proc]
    dfa2 = spa2.proc_to_dfa[proc]
    next if !dfa1 && !dfa2

    a1 = as1[proc]
    t1 = ts1[proc]
    r1 = rs1[proc]

    a2 = as2[proc]
    t2 = ts2[proc]
    r2 = rs2[proc]

    case
    when dfa1 && !dfa2
      return a1 + t1 + r1 if a1 && t1 && r1
      next
    when !dfa1 && dfa2
      return a2 + t2 + r2 if a2 && t2 && r2
      next
    end

    # Then, `dfa1 && dfa2` holds.
    next unless a1 && t1 && r1 && a2 && t2 && r2

    sep_word = DFA.find_separating_word(local_alphabet, dfa1, dfa2)
    next unless sep_word

    as, ts, rs = dfa1.output(dfa1.run(sep_word)[1]) ? [as1, ts1, rs1] : [as2, ts2, rs2]
    sep_word = ProcUtil.expand(spa1.return_input, sep_word, ts)
    return as[proc] + sep_word + rs[proc]
  end

  nil
end

.random(alphabet:, call_alphabet:, return_input:, min_proc_size: 1, max_proc_size: call_alphabet.size, dfa_min_state_size: 5, dfa_max_state_size: 10, dfa_accept_state_size: 2, random: Random) ⇒ Object

Generates a SPA randomly.

: [In, Call, Return] (

  alphabet: Array[In],
  call_alphabet: Array[Call],
  return_input: Return,
  ?min_proc_size: Integer,
  ?max_proc_size: Integer,
  ?dfa_min_state_size: Integer,
  ?dfa_max_state_size: Integer,
  ?dfa_accept_state_size: Integer,
  ?random: Random,
) -> SPA[In, Call, Return]



200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
 
# File 'lib/lernen/automaton/spa.rb', line 200

def self.random(
  alphabet:,
  call_alphabet:,
  return_input:,
  min_proc_size: 1,
  max_proc_size: call_alphabet.size,
  dfa_min_state_size: 5,
  dfa_max_state_size: 10,
  dfa_accept_state_size: 2,
  random: Random
)
  proc_size = random.rand(min_proc_size..max_proc_size)
  procs = call_alphabet.dup.shuffle!(random:)[0...proc_size]

  initial_proc = procs[0] # steep:ignore
  proc_to_dfa = {}
  procs.each do |proc| # steep:ignore
    proc_to_dfa[proc] = DFA.random(
      alphabet: alphabet + procs, # steep:ignore
      random:,
      min_state_size: dfa_min_state_size,
      max_state_size: dfa_max_state_size,
      accept_state_size: dfa_accept_state_size
    )
  end

  new(initial_proc, return_input, proc_to_dfa)
end

Instance Method Details

#==(other) ⇒ Object

Checks the structural equality between ‘self` and `other`.

: (untyped other) -> bool



96
97
98
99
 
# File 'lib/lernen/automaton/spa.rb', line 96

def ==(other)
  other.is_a?(SPA) && initial_proc == other.initial_proc && return_input == other.return_input && # steep:ignore
    proc_to_dfa == other.proc_to_dfa
end

#initial_conf ⇒ Object 



58
 
# File 'lib/lernen/automaton/spa.rb', line 58

def initial_conf = :init

#output(conf) ⇒ Object 



91
 
# File 'lib/lernen/automaton/spa.rb', line 91

def output(conf) = conf == :term

#proc_to_atr_sequence(alphabet, call_alphabet) ⇒ Object

Returns the mapping from procedure names to access/terminating/return sequences.

: (

  Array[In] alphabet,
  Array[Call] call_alphabet
) -> [
  Hash[Call, Array[In | Call | Return]],
  Hash[Call, Array[In | Call | Return]],
  Hash[Call, Array[In | Call | Return]]
]



121
122
123
124
125
126
 
# File 'lib/lernen/automaton/spa.rb', line 121

def proc_to_atr_sequence(alphabet, call_alphabet)
  proc_to_terminating_sequence = compute_proc_to_terminating_sequence(alphabet, call_alphabet)
  proc_to_access_sequence, proc_to_return_sequence =
    compute_proc_to_access_and_return_sequences(alphabet, call_alphabet, proc_to_terminating_sequence)
  [proc_to_access_sequence, proc_to_terminating_sequence, proc_to_return_sequence]
end

#step_conf(conf, input) ⇒ Object 



61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
 
# File 'lib/lernen/automaton/spa.rb', line 61

def step_conf(conf, input)
  case conf
  in :init
    if input == initial_proc
      dfa = proc_to_dfa[initial_proc]
      Conf[:term, initial_proc, dfa.initial_state]
    else
      :sink
    end
  in :term | :sink
    :sink
  in Conf[prev, proc, state]
    dfa = proc_to_dfa[proc]

    next_state = dfa.transition_function[[state, input]]
    if next_state
      next_dfa = proc_to_dfa[input]
      if next_dfa
        return_conf = Conf[prev, proc, next_state]
        return Conf[return_conf, input, next_dfa.initial_state]
      end

      return Conf[prev, proc, next_state]
    end

    input == return_input && dfa.accept_state_set.include?(state) ? prev : :sink
  end
end

#to_graph ⇒ Object 



102
103
104
105
106
107
108
109
 
# File 'lib/lernen/automaton/spa.rb', line 102

def to_graph
  subgraphs =
    proc_to_dfa.map do |proc, dfa|
      Graph::SubGraph[proc.inspect, dfa.to_graph] # steep:ignore
    end

  Graph.new({}, [], subgraphs)
end

#type ⇒ Object

: () -> :spa



55
 
# File 'lib/lernen/automaton/spa.rb', line 55

def type = :spa