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).last != sul.query_last(cex)`). Where `h = conf_to_prefix[hypothesis.run(cex)[1]]`, there are some `n` (where `0 <= n < cex.size`) such that `sul.query_last(h + cex) != sul.query_last(h[n + 1] + cex[n + 1…])` because `sul.query_last(cex) == sul.query_last(h + cex)` and `sul.query_last(h + cex) == hypothesis.run(cex).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 + cex) != sul.query_last(h[n + 1] + cex[n + 1…])`, a prefix `h + cex` 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”](proceedings.mlr.press/v34/isberner14a).

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