Module: Lernen::Algorithm::CexProcessor

Defined in:
lib/lernen/algorithm/cex_processor.rb,
lib/lernen/algorithm/cex_processor/acex.rb,
lib/lernen/algorithm/cex_processor/prefix_transformer_acex.rb

Overview

CexProcessor contains implementations of counterexample processing functions.

A counterexample is a word that leads to the different result between a hypothesis automaton and a SUL (i.e., hypothesis.run(cex)[0].last != sul.query_last(cex)). Where h[n] = conf_to_prefix[hypothesis.run(cex[0...n])[1]], there are some n (where 0 <= n < cex.size) such that sul.query_last(h[n] + cex[n...]) != sul.query_last(h[n + 1] + cex[n + 1...]) because sul.query_last(cex) == sul.query_last(h[0] + cex[n...]) and sul.query_last(h[cex.size] + cex[cex.size...]) == hypothesis.run(cex)[0].last. Finding such a position n from cex is called "counterexample processing".

The result n of counterexample processing has a good property for automata learning. Because sul.query_last(h[n] + cex[n...]) != sul.query_last(h[n + 1] + cex[n + 1...]), a prefix h[n] + cex[n] leads a different state than a state of h[n + 1] with a suffix cex[n + 1...].

For counterexample processing, we can use some searching approach such like linear or binrary search. Using binary search for counterexample processing, it is known as the Rivest-Schapire (RS) optimization typically. For the more detailed information, please refer Isberner and Steffen (2014) "An Abstract Framework for Counterexample Analysis in Active Automata Learning".

Defined Under Namespace

Classes: Acex, PrefixTransformerAcex

Class Method Summary collapse

Class Method Details

.process(acex, cex_processing: :binary) ⇒ Object

Processes a given counterexample in the cex_processing way.

It returns n such that acex.effect(n) != acex.effect(n + 1).

: ( Acex acex, ?cex_processing: cex_processing_method ) -> Integer



42
43
44
45
46
47
48
49
50
51
52
53
 
# File 'lib/lernen/algorithm/cex_processor.rb', line 42

def self.process(acex, cex_processing: :binary)
  low = 0
  high = acex.size - 1
  case cex_processing
  in :linear
    process_linear(acex, low:, high:)
  in :binary
    process_binary(acex, low:, high:)
  in :exponential
    process_exponential(acex, low:, high:)
  end
end