class ADSL::Verification::FormulaBuilder

forward declaration

Attributes

adsl_stack[R]

Public Class Methods

new(component = nil) click to toggle source
# File lib/adsl/verification/formula_generators.rb, line 152
def initialize(component = nil)
  @adsl_stack = []
  @adsl_stack << component unless component.nil?
end

Public Instance Methods

adsl_ast() click to toggle source
# File lib/adsl/verification/formula_generators.rb, line 202
def adsl_ast
  elements = gather_adsl_asts
  if elements.length != 1
    raise "Invalid formula/operator stack state [#{ elements.map{ |e| e.respond_to?(:to_adsl) ? e.to_adsl : e }.join(', ') }]"
  end
  elements.first
end
gather_adsl_asts() click to toggle source
# File lib/adsl/verification/formula_generators.rb, line 182
def gather_adsl_asts
  elements = @adsl_stack.clone
  handle_unary_operator elements, :not do |formula|
    ASTNot.new(:subformula => formula)
  end
  handle_binary_operator elements, :and do |formula1, formula2|
    ASTAnd.new(:subformulae => [formula1, formula2])
  end
  handle_binary_operator elements, :or do |formula1, formula2|
    ASTOr.new(:subformulae => [formula1, formula2])
  end
  handle_binary_operator elements, :implies do |formula1, formula2|
    ASTImplies.new(:subformula1 => formula1, :subformula2 => formula2)
  end
  handle_binary_operator elements, :equiv do |formula1, formula2|
    ASTEquiv.new(:subformula1 => formula1, :subformula2 => formula2)
  end
  elements 
end
handle_binary_operator(elements, operator) { |*args| ... } click to toggle source
# File lib/adsl/verification/formula_generators.rb, line 168
def handle_binary_operator(elements, operator)
  until (index = elements.find_index(operator)).nil?
    raise "Binary operator `#{operator}' not infix-called" if index == 0 or index == elements.length-1
    args = [elements[index-1], elements[index+1]]
    args.each do |arg|
      raise "`#{arg}', used by operator `#{operator}', is not a formula" unless arg.is_a? ASTNode
    end
    result = yield *args
    elements.delete_at index - 1
    elements.delete_at index - 1
    elements[index - 1] = result
  end
end
handle_unary_operator(elements, operator) { |arg| ... } click to toggle source
# File lib/adsl/verification/formula_generators.rb, line 157
def handle_unary_operator(elements, operator)
  until (index = elements.find_index(operator)).nil?
    raise "Unary operator `#{operator}' not prefix-called" if index == elements.length-1
    arg = elements[index+1]
    raise "`#{arg}', used by operator `#{operator}', is not a formula" unless arg.is_a? ASTNode
    result = yield arg
    elements.delete_at index
    elements[index] = result
  end
end