Class: Lernen::Algorithm::LSharp::LSharpLearner

Inherits:
Lernen::Algorithm::Learner show all
Defined in:
lib/lernen/algorithm/lsharp/lsharp_learner.rb

Overview

LSharpLearner is an implementation of L# algorithm.

L# is introduced by [Vaandrager et al. (2022) “A New Approach for Active Automata Learning Based on Apartness”](link.springer.com/chapter/10.1007/978-3-030-99524-9_12).

Instance Method Summary collapse

Methods inherited from Lernen::Algorithm::Learner

#learn

Constructor Details

#initialize(alphabet, sul, automaton_type:) ⇒ LSharpLearner

: (

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


30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
# File 'lib/lernen/algorithm/lsharp/lsharp_learner.rb', line 30

def initialize(alphabet, sul, automaton_type:)
  super()

  @alphabet = alphabet.dup
  @sul = sul
  @automaton_type = automaton_type

  @tree = ObservationTree.new(sul, automaton_type:)
  @witness_cache = {}

  @basis = []
  @basis_set = Set.new
  @frontier = {}

  @incomplete_basis = []

  add_basis([])
end

Instance Method Details

#add_alphabet(input) ⇒ Object



92
93
94
95
# File 'lib/lernen/algorithm/lsharp/lsharp_learner.rb', line 92

def add_alphabet(input)
  @alphabet << input
  @incomplete_basis = @basis.dup
end

#build_hypothesisObject



50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
# File 'lib/lernen/algorithm/lsharp/lsharp_learner.rb', line 50

def build_hypothesis
  loop do
    next if promotion || completion || identification

    hypothesis, state_to_prefix = build_hypothesis_internal
    cex = check_consistency(hypothesis, state_to_prefix)
    if cex
      process_cex(cex, hypothesis, state_to_prefix)
      update_frontier
      next
    end

    return hypothesis, state_to_prefix
  end

  raise "BUG: unreachable"
end

#refine_hypothesis(cex, hypothesis, state_to_prefix) ⇒ Object



69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
# File 'lib/lernen/algorithm/lsharp/lsharp_learner.rb', line 69

def refine_hypothesis(cex, hypothesis, state_to_prefix)
  @tree.query(cex)

  node = @tree.root
  state = hypothesis.initial_conf
  cex.size.times do |n|
    input = cex[n]
    node = node.branch[input]

    _, state = hypothesis.step(state, input)
    state_node = @tree[state_to_prefix[state]]
    raise "BUG: A node for the basis prefix must exist" unless state_node

    if check_apartness(state_node, node)
      cex = cex[0..n]
      break
    end
  end

  process_cex(cex, hypothesis, state_to_prefix)
end