Class: Lernen::Algorithm::LStar::ObservationTable

Inherits:
Object
  • Object
show all
Defined in:
lib/lernen/algorithm/lstar/observation_table.rb

Overview

ObservationTable is an implementation of observation tabel data structure.

This data structure is used for Angluin’s L* algorithm.

Instance Method Summary collapse

Constructor Details

#initialize(alphabet, sul, automaton_type:, cex_processing:) ⇒ ObservationTable

: (

  Array[In] alphabet,
  System::SUL[In, Out] sul,
  automaton_type: :dfa | :moore | :mealy,
  cex_processing: cex_processing_method | nil
) -> void



28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
 
# File 'lib/lernen/algorithm/lstar/observation_table.rb', line 28

def initialize(alphabet, sul, automaton_type:, cex_processing:)
  @alphabet = alphabet
  @sul = sul
  @automaton_type = automaton_type
  @cex_processing = cex_processing

  @prefixes = [[]]
  @suffixes = []
  @table = {}

  case @automaton_type
  in :dfa | :moore
    @suffixes << []
  in :mealy
    @alphabet.each { |a| @suffixes << [a] }
  end
end

Instance Method Details

#build_hypothesis ⇒ Object

Constructs a hypothesis automaton from this observation table.

: () -> [Automaton::TransitionSystem[Integer, In, Out], Hash[Integer, Array]]



49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
 
# File 'lib/lernen/algorithm/lstar/observation_table.rb', line 49

def build_hypothesis
  make_consistent_and_closed

  state_to_prefix = @prefixes.each_with_index.to_h { |prefix, state| [state, prefix] }
  row_to_state = @prefixes.each_with_index.to_h { |prefix, state| [@table[prefix], state] }

  transition_function = {}
  @prefixes.each_with_index do |prefix, state|
    @alphabet.each_with_index do |input, index|
      case @automaton_type
      in :moore | :dfa
        transition_function[[state, input]] = row_to_state[@table[prefix + [input]]]
      in :mealy
        transition_function[[state, input]] = [@table[prefix][index], row_to_state[@table[prefix + [input]]]]
      end
    end
  end

  automaton =
    case @automaton_type
    in :dfa
      accept_state_set =
        state_to_prefix.to_a.filter { |(_, prefix)| @table[prefix][0] }.to_set { |(state, _)| state }
      Automaton::DFA.new(0, accept_state_set, transition_function)
    in :moore
      outputs = state_to_prefix.transform_values { |prefix| @table[prefix][0] }
      Automaton::Moore.new(0, outputs, transition_function)
    in :mealy
      Automaton::Mealy.new(0, transition_function)
    end

  [automaton, state_to_prefix]
end

#refine_hypothesis(cex, hypothesis, state_to_prefix) ⇒ Object

Updates this observation table by the given ‘cex`.

: (

  Array[In] cex,
  Automaton::TransitionSystem[Integer, In, Out] hypothesis,
  Hash[Integer, Array[In]] state_to_prefix
) -> void



90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
 
# File 'lib/lernen/algorithm/lstar/observation_table.rb', line 90

def refine_hypothesis(cex, hypothesis, state_to_prefix)
  cex_processing = @cex_processing
  if cex_processing
    state_to_prefix_lambda = ->(state) { state_to_prefix[state] }

    acex = CexProcessor::PrefixTransformerAcex.new(cex, @sul, hypothesis, state_to_prefix_lambda)
    n = CexProcessor.process(acex, cex_processing:)
    old_prefix = cex[0...n]
    new_input = cex[n]
    new_suffix = cex[n + 1...]

    _, old_state = hypothesis.run(old_prefix) # steep:ignore
    new_prefix = state_to_prefix[old_state] + [new_input]
    @prefixes << new_prefix unless @prefixes.include?(new_prefix)
    @suffixes << new_suffix unless @suffixes.include?(new_suffix) # steep:ignore
  else
    cex_prefixes = (0..cex.size).map { |n| cex[0...n] }
    cex_prefixes.each do |prefix|
      @prefixes << prefix unless @prefixes.include?(prefix) # steep:ignore
    end
  end
end