Class: Lernen::Equiv::SPASimulatorOracle

Inherits:
Oracle
  • Object
show all
Defined in:
lib/lernen/equiv/spa_simulator_oracle.rb

Overview

SPASimulatorOracle provides an implementation of equivalence query that finds a counterexample by simulating the SPA.

Instance Attribute Summary

Attributes inherited from Oracle

#sul

Instance Method Summary collapse

Methods inherited from Oracle

#+, #stats

Constructor Details

#initialize(alphabet, call_alphabet, spa, sul) ⇒ SPASimulatorOracle

: (

  Array[In] alphabet,
  Array[Call] call_alphabet,
  Automaton::SPA[In, Call, Return] spa,
  System::SUL[In | Call | Return, bool] sul
) -> void



23
24
25
26
27
28
29
 
# File 'lib/lernen/equiv/spa_simulator_oracle.rb', line 23

def initialize(alphabet, call_alphabet, spa, sul)
  super(sul)

  @alphabet = alphabet
  @call_alphabet = call_alphabet
  @spa = spa
end

Instance Method Details

#find_cex(hypothesis) ⇒ Object 



32
33
34
35
36
 
# File 'lib/lernen/equiv/spa_simulator_oracle.rb', line 32

def find_cex(hypothesis)
  super

  Automaton::SPA.find_separating_word(@alphabet, @call_alphabet, @spa, hypothesis) # steep:ignore
end