Class: Lernen::Equiv::VPASimulatorOracle

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

Overview

VPASimulatorOracle provides an implementation of equivalence query that finds a counterexample by simulating the VPA.

Instance Attribute Summary

Attributes inherited from Oracle

#sul

Instance Method Summary collapse

Methods inherited from Oracle

#+, #stats

Constructor Details

#initialize(alphabet, call_alphabet, return_alphabet, vpa, sul) ⇒ VPASimulatorOracle

: (

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



25
26
27
28
29
30
31
32
 
# File 'lib/lernen/equiv/vpa_simulator_oracle.rb', line 25

def initialize(alphabet, call_alphabet, return_alphabet, vpa, sul)
  super(sul)

  @alphabet = alphabet
  @call_alphabet = call_alphabet
  @return_alphabet = return_alphabet
  @vpa = vpa
end

Instance Method Details

#find_cex(hypothesis) ⇒ Object 



35
36
37
38
39
40
41
42
43
44
45
 
# File 'lib/lernen/equiv/vpa_simulator_oracle.rb', line 35

def find_cex(hypothesis)
  super

  Automaton::VPA.find_separating_word(
    @alphabet,
    @call_alphabet,
    @return_alphabet,
    @vpa,
    hypothesis # steep:ignore
  )
end