Class: Lernen::Automaton::VPA

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

Overview

VPA represents a visily pushdown automaton.

Especially, this definition represents 1-SEVPA (1-module single-entry visibly pushdown automaton).

Constant Summary collapse

Conf =

Conf is a configuration of VPA run.

Data.define(:state, :stack)

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_state, accept_state_set, transition_function, return_transition_function) ⇒ VPA

: ( Integer initial_state, Set accept_state_set, Hash[[Integer, In], Integer] transition_function. Hash[[Integer, Return], Hash[[Integer, Call], Integer]] return_transition_function ) -> void



37
38
39
40
41
42
43
44
 
# File 'lib/lernen/automaton/vpa.rb', line 37

def initialize(initial_state, accept_state_set, transition_function, return_transition_function)
  super()

  @initial_state = initial_state
  @accept_state_set = accept_state_set
  @transition_function = transition_function
  @return_transition_function = return_transition_function
end

Instance Attribute Details

#accept_state_set ⇒ Object (readonly)

: Set



47
48
49
 
# File 'lib/lernen/automaton/vpa.rb', line 47

def accept_state_set
  @accept_state_set
end

#initial_state ⇒ Object (readonly)

: Integer



46
47
48
 
# File 'lib/lernen/automaton/vpa.rb', line 46

def initial_state
  @initial_state
end

#return_transition_function ⇒ Object (readonly)

: Hash[[Integer, Return], Hash[[Integer, Call], Integer]]



49
50
51
 
# File 'lib/lernen/automaton/vpa.rb', line 49

def return_transition_function
  @return_transition_function
end

#transition_function ⇒ Object (readonly)

: Hash[[Integer, In], Integer]



48
49
50
 
# File 'lib/lernen/automaton/vpa.rb', line 48

def transition_function
  @transition_function
end

Class Method Details

.find_separating_word(alphabet, call_alphabet, return_alphabet, vpa1, vpa2) ⇒ Object

Finds a separating word between vpa1 and vpa2.

: [In, Call, Return] ( Array alphabet, Array call_alphabet, Array return_alphabet, VPA[In, Call, Return] vpa1, VPA[In, Call, Return] vpa2 ) -> (Array[In | Call | Return] | nil)

Raises:

  • (ArgumentError) 


191
192
193
194
195
196
197
198
199
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
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
 
# File 'lib/lernen/automaton/vpa.rb', line 191

def self.find_separating_word(alphabet, call_alphabet, return_alphabet, vpa1, vpa2)
  raise ArgumentError, "Cannot find a separating word for different type automata" unless vpa2.is_a?(vpa1.class)

  queue = []
  prefix_hash = {}

  initial_pair = [vpa1.initial_conf&.state, vpa2.initial_conf&.state]
  queue << initial_pair
  prefix_hash[initial_pair] = []

  until queue.empty?
    state1, state2 = queue.shift
    prefix = prefix_hash[[state1, state2]]

    alphabet.each do |input|
      output1, next_conf1 = vpa1.step(state1 && Conf[state1, []], input)
      output2, next_conf2 = vpa2.step(state2 && Conf[state2, []], input)

      word = prefix + [input]
      return word if output1 != output2

      next_pair = [next_conf1&.state, next_conf2&.state]
      unless prefix_hash.include?(next_pair)
        queue << next_pair
        prefix_hash[next_pair] = word
      end
    end

    found_state_pairs = prefix_hash.keys
    call_alphabet.each do |call_input|
      return_alphabet.each do |return_input|
        found_state_pairs.each do |(call_state1, call_state2)|
          return_conf1 = state1 && Conf[state1, [[call_state1, call_input]]] # steep:ignore
          return_conf2 = state2 && Conf[state2, [[call_state2, call_input]]] # steep:ignore

          output1, next_conf1 = vpa1.step(return_conf1, return_input)
          output2, next_conf2 = vpa2.step(return_conf2, return_input)

          word = prefix_hash[[call_state1, call_state2]] + [call_input] + prefix + [return_input]
          return word if output1 != output2

          next_pair = [next_conf1&.state, next_conf2&.state]
          unless prefix_hash.include?(next_pair)
            queue << next_pair
            prefix_hash[next_pair] = word
          end
        end
      end
    end
  end

  nil
end

.random(alphabet:, call_alphabet:, return_alphabet:, min_state_size: 5, max_state_size: 10, accept_state_size: 2, random: Random) ⇒ Object

Generates a VPA randomly.

: [In, Call, Return] ( alphabet: Array, call_alphabet: Array, return_alphabet: Array, ?min_state_size: Integer, ?max_state_size: Integer, ?accept_state_size: Integer, ?random: Random, ) -> VPA[In, Call, Return]



256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
 
# File 'lib/lernen/automaton/vpa.rb', line 256

def self.random(
  alphabet:,
  call_alphabet:,
  return_alphabet:,
  min_state_size: 5,
  max_state_size: 10,
  accept_state_size: 2,
  random: Random
)
  transition_function, reachable_paths =
    TransitionSystem.random_transition_function(
      alphabet:,
      min_state_size:,
      max_state_size:,
      num_reachable_paths: accept_state_size,
      random:
    )
  accept_state_set = reachable_paths.to_set(&:last) #: Set[Integer]

  state_set = Set.new
  transition_function.each do |(state, _), next_state|
    state_set << state
    state_set << next_state
  end
  states = state_set.to_a
  states.sort!

  return_transition_function = {}
  states.each do |return_state|
    return_alphabet.each do |return_input|
      return_transition_guard = return_transition_function[[return_state, return_input]] = {}
      states.each do |call_state|
        call_alphabet.each do |call_input|
          next_state = states.sample(random:)
          return_transition_guard[[call_state, call_input]] = next_state
        end
      end
    end
  end

  new(0, accept_state_set, transition_function, return_transition_function)
end

Instance Method Details

#==(other) ⇒ Object

Checks the structural equality between self and other.

: (untyped other) -> bool



85
86
87
88
89
 
# File 'lib/lernen/automaton/vpa.rb', line 85

def ==(other)
  other.is_a?(VPA) && initial_state == other.initial_state && accept_state_set == other.accept_state_set &&
    transition_function == other.transition_function &&
    return_transition_function == other.return_transition_function
end

#error_state ⇒ Object

Returns the error state of this VPA.

An error state is:

  • neither a initial state nor accepting states, and
  • only having self-loops for all input.

If an error state is not found, it returns nil.

: () -> (Integer | nil)



124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
 
# File 'lib/lernen/automaton/vpa.rb', line 124

def error_state
  transition_function
    .group_by { |(state, _), _| state }
    .transform_values { _1.to_h { |(_, input), next_state| [input, next_state] } }
    .each do |state, transition_hash|
      # The initial state and accepting states are not an error state.
      next if state == initial_state || accept_state_set.include?(state)

      # An error state should only have self-loops.
      next unless transition_hash.all? { |_, next_state| state == next_state }
      all_returns_are_self_loops =
        return_transition_function.all? do |_, return_transition_guard|
          return_transition_guard
            .filter { |(call_state, _), _| call_state == state }
            .all? { |_, next_state| state == next_state }
        end
      next unless all_returns_are_self_loops

      return state
    end

  nil
end

#initial_conf ⇒ Object 



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

def initial_conf = Conf[initial_state, []]

#output(conf) ⇒ Object 



78
79
80
 
# File 'lib/lernen/automaton/vpa.rb', line 78

def output(conf)
  !conf.nil? && accept_state_set.include?(conf.state) && conf.stack.empty?
end

#states ⇒ Object

Returns the array of states of this VPA.

The result array is sorted.

: () -> Array



96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
 
# File 'lib/lernen/automaton/vpa.rb', line 96

def states
  state_set = Set.new
  state_set << initial_state
  accept_state_set.each { |state| state_set << state }
  transition_function.each do |(state, _), next_state|
    state_set << state
    state_set << next_state
  end
  return_transition_function.each do |(state, _), return_transition_guard|
    state_set << state
    return_transition_guard.each do |(call_state, _), next_state|
      state_set << call_state
      state_set << next_state
    end
  end
  state_set.to_a.sort!
end

#step_conf(conf, input) ⇒ Object 



58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
 
# File 'lib/lernen/automaton/vpa.rb', line 58

def step_conf(conf, input)
  return nil if conf.nil?

  next_state = transition_function[[conf.state, input]] # steep:ignore
  return Conf[next_state, conf.stack] if next_state

  return_transition_guard = return_transition_function[[conf.state, input]] # steep:ignore
  if return_transition_guard
    *next_stack, last_call = conf.stack
    return nil unless last_call
    next_state = return_transition_guard[last_call]
    return Conf[next_state, next_stack]
  end

  # When there is no usual transition and no return tansition for `input`,
  # then we assume that `input` is a call alphabet.
  Conf[initial_state, conf.stack + [[conf.state, input]]] # steep:ignore
end

#to_graph(shows_error_state: false) ⇒ Object

Returns a graph of this VPA.

(?shows_error_state: bool) -> Graph



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
 
# File 'lib/lernen/automaton/vpa.rb', line 151

def to_graph(shows_error_state: false)
  error_state = error_state() unless shows_error_state

  nodes =
    states
      .filter_map do |state|
        next if state == error_state
        shape = accept_state_set.include?(state) ? :doublecircle : :circle #: Graph::node_shape
        [state, Graph::Node[state.to_s, shape]]
      end
      .to_h

  edges =
    transition_function.filter_map do |(state, input), next_state|
      next if state == error_state || next_state == error_state
      Graph::Edge[state, input.inspect, next_state] # steep:ignore
    end

  edges +=
    return_transition_function.flat_map do |(state, return_input), return_transition_guard|
      next [] if state == error_state
      return_transition_guard.filter_map do |(call_state, call_input), next_state|
        next if call_state == error_state || next_state == error_state
        label = "#{return_input.inspect} / (#{call_state}, #{call_input.inspect})" # steep:ignore
        Graph::Edge[state, label, next_state]
      end
    end

  Graph.new(nodes, edges)
end

#type ⇒ Object 



52
 
# File 'lib/lernen/automaton/vpa.rb', line 52

def type = :vpa