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