module ADSL::Verification::FormulaGenerators

Public Instance Methods

[](formula) click to toggle source
# File lib/adsl/verification/formula_generators.rb, line 96
def [](formula)
  in_formula_builder do |fb|
    formula = formula.adsl_ast if formula.respond_to? :adsl_ast
    fb.adsl_stack << formula
  end
end
and(*params) click to toggle source
# File lib/adsl/verification/formula_generators.rb, line 130
def and(*params)
  binary_op_with_any_number_of_params :and, ASTAnd, params
end
binary_op(op, klass, params) click to toggle source
# File lib/adsl/verification/formula_generators.rb, line 116
def binary_op(op, klass, params)
  raise "`#{op}' takes two parameters or none at all" unless params.empty? or params.length == 2
  in_formula_builder do |fb|
    if params.empty?
      fb.adsl_stack << op
    else
      params.each do |param|
        raise "Invalid formula `#{param}' in `#{op}' parameter list" unless param.respond_to? :adsl_ast
      end
      fb.adsl_stack << klass.new(:subformula1 => params.first.adsl_ast, :subformula2 => params.last.adsl_ast)
    end
  end
end
binary_op_with_any_number_of_params(op, klass, params) click to toggle source
# File lib/adsl/verification/formula_generators.rb, line 103
def binary_op_with_any_number_of_params(op, klass, params)
  in_formula_builder do |fb|
    if params.empty?
      fb.adsl_stack << op
    else
      params.each do |param|
        raise "Invalid formula `#{param}' in `#{op}' parameter list" unless param.respond_to? :adsl_ast
      end
      fb.adsl_stack << klass.new(:subformulae => params.map(&:adsl_ast))
    end
  end
end
equiv(*params) click to toggle source
# File lib/adsl/verification/formula_generators.rb, line 138
def equiv(*params)
  binary_op_with_any_number_of_params :equiv, ASTEquiv, params
end
exists(arg_types = {}, &block) click to toggle source
# File lib/adsl/verification/formula_generators.rb, line 69
def exists(arg_types = {}, &block)
  handle_quantifier :exists, ASTExists, arg_types, block
end
false() click to toggle source
# File lib/adsl/verification/formula_generators.rb, line 90
def false
  in_formula_builder do |fb|
    fb.adsl_stack << false.adsl_ast
  end
end
forall(arg_types = {}, &block) click to toggle source
# File lib/adsl/verification/formula_generators.rb, line 65
def forall(arg_types = {}, &block)
  handle_quantifier :forall, ASTForAll, arg_types, block
end
handle_quantifier(quantifier, adsl_ast_node_klass, arg_types, block) click to toggle source
# File lib/adsl/verification/formula_generators.rb, line 27
def handle_quantifier(quantifier, adsl_ast_node_klass, arg_types, block)
  raise "A block needs to be passed to quantifiers" if block.nil?
  raise "At least some variables need to be given to the block" if block.parameters.empty?
  in_formula_builder do |fb|
    
    param_types = {}
    block.parameters.each do |param|
      classname = infer_classname_from_varname param[1]
      klass = Object.lookup_const classname
      param_types[param[1].to_sym] = klass
    end
    arg_types.each do |explicit_name, explicit_type|
      classname = classname_for_classname explicit_type
      klass = Object.lookup_const classname
      raise "Unknown class #{explicit_type} for parameter #{explicit_name}" if klass.nil?
      param_types[explicit_name.to_sym] = klass
    end

    param_types.each do |name, klass|
      raise "Unknown klass for variable `#{name}' in #{quantifier} quantifier" if klass.nil?
      raise "Class #{klass.name} is not instrumented" unless klass.respond_to? :adsl_ast
    end

    vars_and_objsets = block.parameters.map{ |param|
      [
        t(param[1].to_s),
        param_types[param[1].to_sym].all.adsl_ast
      ]
    }
    subformula = block.(*block.parameters.map do |param|
      param_types[param[1].to_sym].new :adsl_ast => ASTVariable.new(:var_name => t(param[1]))
    end)
    subformula = true if subformula.nil?
    raise "Invalid formula returned by block in `#{quantifier}'" unless subformula.respond_to? :adsl_ast 
    fb.adsl_stack << adsl_ast_node_klass.new(:vars => vars_and_objsets, :subformula => subformula.adsl_ast)
  end
end
implies(*params) click to toggle source
# File lib/adsl/verification/formula_generators.rb, line 142
def implies(*params)
  binary_op :implies, ASTImplies, params
end
in_formula_builder() { |formula_builder| ... } click to toggle source
# File lib/adsl/verification/formula_generators.rb, line 15
def in_formula_builder
  formula_builder = nil
  if self.is_a? ::ADSL::Verification::FormulaBuilder
    formula_builder = self
  else
    formula_builder = ::ADSL::Verification::FormulaBuilder.new
    formula_builder.adsl_stack << self.adsl_ast if self.respond_to? :adsl_ast
  end
  yield formula_builder
  formula_builder
end
neg(param = nil)
Alias for: not
not(param = nil) click to toggle source
# File lib/adsl/verification/formula_generators.rb, line 73
def not(param = nil)
  in_formula_builder do |fb|
    if param.nil?
      fb.adsl_stack << :not
    else
      fb.adsl_stack << ASTNot.new(:subformula => param.adsl_ast)
    end
  end
end
Also aliased as: neg
or(*params) click to toggle source
# File lib/adsl/verification/formula_generators.rb, line 134
def or(*params)
  binary_op_with_any_number_of_params :or, ASTOr, params
end
true() click to toggle source
# File lib/adsl/verification/formula_generators.rb, line 84
def true
  in_formula_builder do |fb|
    fb.adsl_stack << true.adsl_ast
  end
end