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
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