module Sfp::SasTranslator

include ‘Sas’ module to enable processing Sfp into Finite-Domain Representation (FDR)

TODO:

Constants

ActivateSimpleGlobalConstraint
GlobalConstraintMethod
GlobalOperator
GlobalVariable
GoalOperator
GoalVariable
ImplicationToDisjunction
SometimeOperatorPrefix
SometimeVariablePrefix

Attributes

axioms[R]
benchmarks[R]
goals[R]
operators[R]
root[RW]
types[R]
variables[R]

Public Class Methods

next_axiom_id() click to toggle source

return the next axiom’s id

# File lib/sfp/sas_translator.rb, line 798
def self.next_axiom_id
        return (@@axiom_id += 1) if defined?(@@axiom_id) != nil
        @@axiom_id = 0
        return @@axiom_id
end
next_constraint_id() click to toggle source

return the next constraint’s id

# File lib/sfp/sas_translator.rb, line 780
def self.next_constraint_id
        return (@@constraint_id += 1) if defined?(@@constraint_id) != nil
        @@constraint_id = 0
        return @@constraint_id
end
next_constraint_key() click to toggle source
# File lib/sfp/sas_translator.rb, line 786
def self.next_constraint_key
        return 'constraint_' + next_constraint_id.to_s
end
next_operator_id() click to toggle source

return the next operator’s id

# File lib/sfp/sas_translator.rb, line 773
def self.next_operator_id
        return (@@op_id += 1) if defined?(@@op_id) != nil
        @@op_id = 0
        return @@op_id
end
next_variable_id() click to toggle source

return the next variable’s id

# File lib/sfp/sas_translator.rb, line 791
def self.next_variable_id
        return (@@variable_id += 1) if defined?(@@variable_id) != nil
        @@variable_id = 0
        return @@variable_id
end
null_of(class_ref=nil) click to toggle source
# File lib/sfp/sas_translator.rb, line 1602
def self.null_of(class_ref=nil)
        return { '_context' => 'null', '_isa' => class_ref } if class_ref.is_a?(String) and
                class_ref != '' and class_ref.isref
        return nil
end
reset_operator_id() click to toggle source
# File lib/sfp/sas_translator.rb, line 768
def self.reset_operator_id
        @@op_id = -1
end

Public Instance Methods

add_unknown_undefined_value_to_variables() click to toggle source
# File lib/sfp/sas_translator.rb, line 1045
def add_unknown_undefined_value_to_variables
        @variables.each_value { |variable|
                #next if variable.is_final
                variable << @unknown_value
                variable << Sfp::Undefined.create(variable.type)
                variable.uniq!
        }
end
add_unknown_value_to_nonstatic_variables() click to toggle source
# File lib/sfp/sas_translator.rb, line 1038
def add_unknown_value_to_nonstatic_variables
        @variables.each_value { |variable|
                next if variable.is_final
                variable << @unknown_value
        }
end
and_equals_constraint_to_map(c) click to toggle source
# File lib/sfp/sas_translator.rb, line 818
def and_equals_constraint_to_map(c)
        return { c['_self'] => c['_value'] } if c['_type'] == 'equals'
        map = {}
        c.each { |k,v| map[k] = v['_value'] if k[0,1] != '_' and v['_type'] == 'equals' }
        return map
end
apply_global_constraint_method_1(operator) click to toggle source
# File lib/sfp/sas_translator.rb, line 1054
def apply_global_constraint_method_1(operator)
        return true if not @root.has_key?('global') or not @root['global'].isconstraint
        operator[@global_var.name] = Parameter.new(@global_var, true, false)
end
apply_global_constraint_method_2(operator) click to toggle source

return true if global constraint could be applied, otherwise false

# File lib/sfp/sas_translator.rb, line 1060
def apply_global_constraint_method_2(operator)
        return true if not @root.has_key?('global') or #@root['global'] == nil or
                not @root['global'].isconstraint

        # return true if operator's effect is consistent with "left := right"
        def consistent_with_equals(left, right, operator)
                return false if operator.has_key?(left) and operator[left].post != nil and
                        operator[left].post != right['_value']
                return true
        end

        # return true if operator's effect is consistent with given 'and' constraint
        def consistent_with_and(constraint, operator)
                constraint.each { |k,v|
                        next if k[0,1] == '_'
                        return false if not consistent_with_equals(k, v, operator)
                }
                return true
        end

        # global constraint is AND formula
        return consistent_with_and(@root['global'], operator) if
                        @root['global']['_type'] == 'and'
        
        # global constraint is OR formula
        total = 0
        satisfied = Array.new
        @root['global'].each { |k,v|
                next if k[0,1] == '_'
                total += 1
                satisfied << k if consistent_with_and(v, operator)
        }
        if satisfied.length < total
                # partial satisfaction or OR formula
                satisfied.each { |key|
                        # create an operator for each satisfied sub-formula
                        op = operator.clone
                        op.modifier_id = key
                        map_cond = and_equals_constraint_to_map(@root['global'][key])
                        map_cond.each { |k,v|
                                next if k[0,1] == '_'
                                raise VariableNotFoundException, 'Variable not found: ' + k if
                                        not @variables.has_key?(k)
                                if not op.has_key?(@variables[k].name)
                                        op[@variables[k].name] = Parameter.new(@variables[k], v, nil)
                                else
                                        #op[@variables[k].name].pre = v
                                end
                        }
                        @operators[op.name] = op
                        @g_operators << op
                }
                # the original operator is not required
                return false
        end

        return true
end
array_to_or_constraint(arr) click to toggle source
# File lib/sfp/sas_translator.rb, line 1144
def array_to_or_constraint(arr)
        c = {'_context'=>'constraint', '_type'=>'or'}
        arr.each { |v| c[Sfp::SasTranslator.next_constraint_key] = v }
        return c
end
break_nested_reference(ref) click to toggle source
# File lib/sfp/sas_translator.rb, line 1179
def break_nested_reference(ref)
        rest, last = ref.pop_ref
        names = [last]
        while rest != '$' and not @variables.has_key?(rest)
                rest, last = rest.pop_ref
                names.unshift(last)
        end
        rest, last = rest.pop_ref
        names.unshift(last)
        return [names, rest]
end
calculate_depth(formula, depth) click to toggle source

testing/debugging methods

# File lib/sfp/sas_translator.rb, line 1523
def calculate_depth(formula, depth)
        formula.each { |k,v|
                next if k[0,1] == '_'
                depth = calculate_depth(v, depth+1)
                break
        }
        depth
end
combinator(bucket, grounder, procedure, names, params, selected, index) click to toggle source

combinatorial method for all possible values of parameters using recursive method

# File lib/sfp/sas_translator.rb, line 966
def combinator(bucket, grounder, procedure, names, params, selected, index)
        if index >= names.length
                p = Sfp::Helper.deep_clone(procedure) # procedure.clone
                # grounding all references
                selected['$.this'] = procedure['_parent'].ref
                selected.each { |k,v| selected[k] = (v.is_a?(Hash) ? v.ref : v) }
                grounder.map = selected
                p['_condition'].accept(grounder)
                p['_effect'].accept(grounder)
                p['_context'] = 'operator'
                p['_parameters'] = selected.clone
                # remove parameters because it's already grounded
                p.each { |k,v| p.delete(k) if k[0,1] != '_' }
                bucket << p
        else
                params[ names[index] ].each { |val|
                        ref = '$.' + names[index]
                        selected[ref] = val
                        combinator(bucket, grounder, procedure, names, params, selected, index+1)
                        selected.delete(ref)
                }
        end
end
compile_step_1() click to toggle source
# File lib/sfp/sas_translator.rb, line 71
def compile_step_1
        begin
                @benchmarks = {}
                @unknown_value = ::Sfp::Unknown.new

                @arrays = Hash.new
                if @parser_arrays != nil
                        @parser_arrays.each do |k,v|
                                first, rest = k.explode[1].explode
                                next if rest == nil
                                @arrays['$.' + rest.to_s] = v
                        end
                end

                return nil if @root == nil
                return nil if not @root.has_key?('initial') or not @root.has_key?('goal')

                @variables = Hash.new
                @types = { '$.Boolean' => [true, false],
                        '$.Integer' => Array.new,
                        '$.String' => Array.new
                }
                @operators = Hash.new
                @axioms = Array.new

                @g_operators = []

                # collect classes
                #self.collect_classes
        
                # unlink 'initial', 'goal', 'global' with root
                @root['initial'].delete('_parent')
                @root['goal'].delete('_parent')
                if @root['goal'].has_key?('always')
                        @root['global'] = @root['goal']['always']
                        @root['goal'].delete('always')
                        @root['global']['_self'] = 'global'
                        @root['global']['_type'] = 'and'
                end
                @root['global'].delete('_parent') if @root.has_key?('global')

                if @root['goal'].has_key?('sometime')
                        @root['sometime'] = @root['goal']['sometime']
                        @root['goal'].delete('sometime')
                        @root['sometime']['_type'] = 'or'
                        @root['sometime'].delete('_parent')
                end

                if @root['goal'].has_key?('sometime-after')
                        @root['sometime-after'] = @root['goal']['sometime-after']
                        @root['goal'].delete('sometime')
                        @root['sometime-after'].delete('_parent')
                end

        @benchmarks['generating variables'] = Benchmark.measure do
                @root['initial'].accept(Sfp::Visitor::ReferenceModifier.new)
                @root['goal'].accept(Sfp::Visitor::ReferenceModifier.new) if @root.has_key?('goal')
                @root['global'].accept(Sfp::Visitor::ReferenceModifier.new) if @root.has_key?('global')
                #@root['sometime'].accept(ReferenceModifier.new)
                #@root['sometime-after'].accept(ReferenceModifier.new)

                ### collect variables ###
                @root['initial'].accept(VariableCollector.new(self))

                ### collect values ###
                # collect values from goal constraint
                value_collector = Sfp::SasTranslator::ValueCollector.new(self)
                @root['goal'].accept(value_collector) if @root.has_key?('goal') and
                                @root['goal'].isconstraint
                # collect values from global constraint
                @root['global'].accept(value_collector) if @root.has_key?('global') and
                                @root['global'].isconstraint
                # collect values from sometime constraint
                @root['sometime'].accept(value_collector) if @root.has_key?('sometime')

                # remove duplicates from type's set of value
                #@types.each_value { |values| values.uniq! }
                @types.keys.each { |type| @types[type] = to_set(@types[type]) }

                # set domain values for each variable
                self.set_variable_values

                # identify immutable variables
                #self.identify_immutable_variables

                # re-evaluate set variables and types
                self.evaluate_set_variables_and_types
        end

        @benchmarks['processing goal'] = Benchmark.measure do
                ### process goal constraint ###
                process_goal(@root['goal']) if @root.has_key?('goal') and
                                @root['goal'].isconstraint
        end

        @benchmarks['processing global constraint'] = Benchmark.measure do
                ### process global constrait
                self.process_global_constraint
        end

        @benchmarks['processing sometime constraint'] = Benchmark.measure do
                ### normalize sometime formulae ###
                if @root.has_key?('sometime')
                        raise TranslationException, 'Invalid sometime constraint' if
                                not normalize_formula(@root['sometime'])
                end
        end

        @variables.each_value do |var|
                if !var.index(var.init)
                        var << var.init
                        @types[var.type] << var.init
                end
                if !var.goal.nil? and !var.index(var.goal)
                        var << var.goal
                        @types[var.type] << var.goal
                end
        end
        @types.keys.each { |type| @types[type] = to_set(@types[type]) }

        # add Sfp::Unknown and Sfp::Undefined value to all non-final variables
        self.add_unknown_undefined_value_to_variables

        @benchmarks['processing procedures'] = Benchmark.measure do
                ### process all procedures
                @variables.each_value do |var|
                        if var.is_final
                                var.init.each { |k,v| process_procedure(v, var.init) if v.is_a?(Hash) and v.isprocedure }
                        end
                end
                self.reset_operators_name
        end

                ### process sometime modalities ###
                self.process_sometime if @root.has_key?('sometime')
                ### process sometime-after modalities ###
                self.process_sometime_after if @root.has_key?('sometime-after')

                # detect and merge mutually inclusive operators
                self.search_and_merge_mutually_inclusive_operators

                #self.add_unknown_value_to_nonstatic_variables

                #self.dump_types
                #self.dump_vars
                #self.dump_operators

                @vars = @variables.values

        rescue Exception => e
                raise e
        end
end
compile_step_2() click to toggle source
# File lib/sfp/sas_translator.rb, line 65
def compile_step_2
        @benchmarks['postprocessing simple global constraint'] = Benchmark.measure do
                self.postprocess_simple_global_constraint
        end
end
conjunction_only(id, f) click to toggle source
# File lib/sfp/sas_translator.rb, line 457
def conjunction_only(id, f)
        #return true if @variables.has_key?(id) and f['_type'] == 'equals'
        return true if f['_type'] == 'equals'
        if f['_type'] == 'and'
                f.each { |k,v| return false if k[0,1] != '_' and not conjunction_only(k, v) }
                return true
        end

        false
end
consistent_with_and(constraint, operator) click to toggle source

return true if operator’s effect is consistent with given ‘and’ constraint

# File lib/sfp/sas_translator.rb, line 1072
def consistent_with_and(constraint, operator)
        constraint.each { |k,v|
                next if k[0,1] == '_'
                return false if not consistent_with_equals(k, v, operator)
        }
        return true
end
consistent_with_equals(left, right, operator) click to toggle source

return true if operator’s effect is consistent with “left := right”

# File lib/sfp/sas_translator.rb, line 1065
def consistent_with_equals(left, right, operator)
        return false if operator.has_key?(left) and operator[left].post != nil and
                operator[left].post != right['_value']
        return true
end
create_and_constraint(key, parent) click to toggle source
# File lib/sfp/sas_translator.rb, line 1136
def create_and_constraint(key, parent)
        return {'_context'=>'constraint', '_type'=>'and', '_self'=>key, '_parent'=>parent}
end
create_equals_constraint(value) click to toggle source
# File lib/sfp/sas_translator.rb, line 1124
def create_equals_constraint(value)
        return {'_context'=>'constraint', '_type'=>'equals', '_value'=>value}
end
create_not_constraint(key, parent) click to toggle source
# File lib/sfp/sas_translator.rb, line 1132
def create_not_constraint(key, parent)
        return {'_context'=>'constraint', '_type'=>'not', '_self'=>key, '_parent'=>parent}
end
create_not_equals_constraint(value) click to toggle source
# File lib/sfp/sas_translator.rb, line 1128
def create_not_equals_constraint(value)
        return {'_context'=>'constraint', '_type'=>'not-equals', '_value'=>value}
end
create_or_constraint(key, parent) click to toggle source
# File lib/sfp/sas_translator.rb, line 1140
def create_or_constraint(key, parent)
        return {'_context'=>'constraint', '_type'=>'or', '_self'=>key, '_parent'=>parent}
end
create_output() click to toggle source
# File lib/sfp/sas_translator.rb, line 629
def create_output
        self.to_s
end
cross_product_and(bucket, names, formula, values=Hash.new, index=0) click to toggle source

dot-product the nodes

# File lib/sfp/sas_translator.rb, line 1326
def cross_product_and(bucket, names, formula, values=Hash.new, index=0)
        if index >= names.length
                key = Sfp::SasTranslator.next_constraint_key
                c = create_and_constraint(key, formula)
                values.each { |k,v| c[k] = v }
                if flatten_and_or_graph(c)
                        # add the constraint because it's consistent
                        formula[key] = c
                end
        else
                key = names[index]
                val = formula[ key ]
                if val.is_a?(Hash) and val.isconstraint and val['_type'] == 'or'
                        val.each { |k,v|
                                next if k[0,1] == '_'
                                values[k] = v
                                cross_product_and(bucket, names, formula, values, index+1)
                                values.delete(k)
                        }
                else
                        values[key] = val
                        cross_product_and(bucket, names, formula, values, index+1)
                end
        end
end
dump(stream) click to toggle source
# File lib/sfp/sas_translator.rb, line 633
def dump(stream)
        init = @root['initial']

        # version
        stream.write "begin_version\n3\nend_version\n"
        # metric
        stream.write "begin_metric\n1\nend_metric\n"

        ### use symbolic as key in map of variables
        vars = {}
        @variables.each { |k,v| vars[k.to_sym] = v }
        names = vars.keys

        # variables
        stream.write "#{names.length}\n"
        names.sort!
        names.each_index do |i|
                var = vars[ names[i] ]
                var.id = i
                var.dump(stream, init)
        end

        # mutex
        stream.write "0\n"

        # initial & goal state
        stream.write "begin_state\n"
        goal = ''
        goal_count = 0
        names.each do |name|
                var = vars[name]
                if var.init.is_a?(Hash) and var.init.isnull
                        stream.write "0\n"
                elsif var.init.is_a?(::Sfp::Unknown)
                        stream.write "#{var.length - 1}\n"
                else
                        val = var.index(var.init).to_s
                        raise TranslationException, "Unknown init: #{var.name}=#{var.init.inspect}" if val.length <= 0
                        stream.write "#{val}\n"
                end

                if var.goal != nil
                        goal << "#{var.id} #{var.index(var.goal)}\n"
                        goal_count += 1
                end
        end
        stream.write "end_state\nbegin_goal\n#{goal_count}\n#{goal}end_goal\n"

        # operators
        operators = @operators.values.select { |op| op.total_preposts > 0 }
        stream.write "#{operators.length}\n"
        operators.each { |operator| operator.dump(stream, init, vars) }

        # axioms
        stream.write "0"
end
dump_axioms() click to toggle source
# File lib/sfp/sas_translator.rb, line 1021
def dump_axioms
        puts '--- axioms'
        @axioms.each { |ax| puts ax.to_s }
end
dump_operators() click to toggle source
# File lib/sfp/sas_translator.rb, line 1016
def dump_operators
        puts '--- operators'
        @operators.each_value { |op| puts op.to_s + ' -- ' + op.params.inspect }
end
dump_types() click to toggle source
# File lib/sfp/sas_translator.rb, line 995
def dump_types
        puts '--- types'
        @types.each { |name,values|
                next if values == nil
                print name + ": "
                values.each { |val|
                        if val.is_a?(Hash)
                                print (val.isnull ? 'null ' : val.ref + " ")
                        else
                                print val.to_s + " "
                        end
                }
                puts '| ' + values.length.to_s
        }
end
dump_vars() click to toggle source
# File lib/sfp/sas_translator.rb, line 1011
def dump_vars
        puts '--- variables'
        @variables.each_value { |value| puts value.to_s }
end
enforce_equals_constraint(operator, var, val) click to toggle source
# File lib/sfp/sas_translator.rb, line 350
def enforce_equals_constraint(operator, var, val)
        if operator.has_key?(var)
                return nil if !operator[var].pre.nil? or operator[var].pre != val
                operator[var].pre = val
        else
                operator[var] = Parameter.new(@variables[var], val)
        end
        operator
end
evaluate_set_variables_and_types() click to toggle source
# File lib/sfp/sas_translator.rb, line 263
def evaluate_set_variables_and_types
        @variables.each_value do |var|
                next if not var.isset
                new_values = []
                var.each { |x| new_values << x['_values'] if x.is_a?(Hash) and x.isset }
                new_values.each { |x| var << x }
                #var.delete_if { |x| x.nil? or x == '' }
                var.delete_if { |x| x.nil? or x == '' or (x.is_a?(Hash) and x.isset) }
                var.each { |x| x.sort! }
                var.uniq!

                var.init = var.init['_values'] if var.init.is_a?(Hash) and var.init.isset
                var.goal = var.goal['_values'] if var.goal.is_a?(Hash) and var.goal.isset
        end

        @types.each do |name,values|
                next if name[0,1] != '('
                new_values = []
                values.each { |x| new_values << x['_values'] if x.is_a?(Hash) and x.isset }
                new_values.each { |x| values << x }
                values.delete_if { |x| x.nil? or x == '' or (x.is_a?(Hash) and x.isset) }
                #values.delete_if { |x| x == nil or x == '' }
                values.each { |x| x.sort! }
                values.uniq!
        end
end
flatten_and_or_graph(formula) click to toggle source

Recursively pull statements that has the same AND/OR operator. Only receive a formula with AND, OR, EQUALS constraints.

return false if there is any contradiction of facts, otherwise true

# File lib/sfp/sas_translator.rb, line 1291
def flatten_and_or_graph(formula)
        # transform formula into a format:
        #   (x1 and x2) or (y1 and y2 and y3) or z1
        is_and_or_tree = false
        formula.keys.each { |k|
                next if k[0,1] == '_'
                v = formula[k]
                if v.is_a?(Hash) and v.isconstraint
                        if v['_type'] == 'or' or v['_type'] == 'and'
                                if not flatten_and_or_graph(v)
                                        # remove it because it's not consistent
                                        formula.delete(k)
                                        v['_parent'] = nil
                                end

                                if formula['_type'] == v['_type']
                                        # pull-out all node's elements
                                        v.keys.each { |k1|
                                                next if k1[0,1] == '_'
                                                v1 = v[k1]
                                                # check contradiction facts
                                                if formula.has_key?(k1)
                                                        return false if formula[k1]['_type'] != v1['_type']
                                                        return false if formula[k1]['_value'] != v1['_value']
                                                else
                                                        formula[k1] = v1
                                                end
                                        }
                                        formula.delete(k)
                                end
                                is_and_or_tree = true if formula['_type'] == 'and' and v['_type'] == 'or'
                        end
                end
        }
        # dot-product the nodes
        def cross_product_and(bucket, names, formula, values=Hash.new, index=0)
                if index >= names.length
                        key = Sfp::SasTranslator.next_constraint_key
                        c = create_and_constraint(key, formula)
                        values.each { |k,v| c[k] = v }
                        if flatten_and_or_graph(c)
                                # add the constraint because it's consistent
                                formula[key] = c
                        end
                else
                        key = names[index]
                        val = formula[ key ]
                        if val.is_a?(Hash) and val.isconstraint and val['_type'] == 'or'
                                val.each { |k,v|
                                        next if k[0,1] == '_'
                                        values[k] = v
                                        cross_product_and(bucket, names, formula, values, index+1)
                                        values.delete(k)
                                }
                        else
                                values[key] = val
                                cross_product_and(bucket, names, formula, values, index+1)
                        end
                end
        end
        if is_and_or_tree
                # change it into OR->AND tree
                names = Array.new
                formula.keys.each { |k| names << k if k[0,1] != '_' }
                bucket = Array.new
                cross_product_and(bucket, names, formula)
                names.each { |k| formula.delete(k) }
                formula['_type'] = 'or'
        end

        return true
end
get_list_not_value_of(var_name, value) click to toggle source

‘var_name’ := x, value := p1 variable x := p1 | p2 | p3 return an array (p2, p3)

# File lib/sfp/sas_translator.rb, line 1367
def get_list_not_value_of(var_name, value)
        raise VariableNotFoundException, 'Variable not found: ' + var_name if
                not @variables.has_key?(var_name)
        if value.is_a?(String) and value.isref
                value = @root['initial'].at?(value)
        elsif value.is_a?(Hash) and value.isnull
                value = @variables[var_name][0]
        end
        return (@variables[var_name] - [value])
end
ground_procedure_parameters(procedure) click to toggle source

determine all possible sets of parameters’ value and create an operator for each set

# File lib/sfp/sas_translator.rb, line 913
                def ground_procedure_parameters(procedure)
                        params = Hash.new
                        procedure.each { |k,v|
                                next if k[0,1] == '_'
### debug
#puts procedure.ref
#p = Sfp::Helper.deep_clone(procedure)
#p.accept(Sfp::Visitor::ParentEliminator.new)
#p.delete('_parent')
#puts JSON.pretty_generate(p)
### end debug
                                type = case v
                                when Sfp::Undefined
                                        v.type
                                when Hash
                                        case v['_context']
                                        when 'null', 'any_value'
                                                v['_isa']
                                        when 'set'
                                                "(#{v['_isa']})"
                                        else
                                                nil
                                        end
                                else
                                        return nil
                                end

                                #if not @types.has_key?( v['_isa'] )
                                #   return nil
                                #end
                                #type = case v['_context']
                                #   when 'null', 'any_value'
                                #           v['_isa']
                                #   when 'set'
                                #           "(#{v['_isa']})"
                                #   else
                                #           nil
                                #   end

                                #next if type == nil
                                #raise TypeNotFoundException, type if not @types.has_key?(type)

                                # if the specified parameter does not have any value,
                                # then it's invalid procedure (should print a warning)
                                return nil if not @types.has_key?(type)

                                params[k] = Array.new
                                @types[ type ].each { |val| params[k] << val if
                                        not (val.is_a?(Hash) and val.isnull) and
                                        !val.is_a?(Sfp::Undefined) and !val.is_a?(Sfp::Unknown) }
                        }
                        # combinatorial method for all possible values of parameters
                        # using recursive method
                        def combinator(bucket, grounder, procedure, names, params, selected, index)
                                if index >= names.length
                                        p = Sfp::Helper.deep_clone(procedure) # procedure.clone
                                        # grounding all references
                                        selected['$.this'] = procedure['_parent'].ref
                                        selected.each { |k,v| selected[k] = (v.is_a?(Hash) ? v.ref : v) }
                                        grounder.map = selected
                                        p['_condition'].accept(grounder)
                                        p['_effect'].accept(grounder)
                                        p['_context'] = 'operator'
                                        p['_parameters'] = selected.clone
                                        # remove parameters because it's already grounded
                                        p.each { |k,v| p.delete(k) if k[0,1] != '_' }
                                        bucket << p
                                else
                                        params[ names[index] ].each { |val|
                                                ref = '$.' + names[index]
                                                selected[ref] = val
                                                combinator(bucket, grounder, procedure, names, params, selected, index+1)
                                                selected.delete(ref)
                                        }
                                end
                        end
                        bucket = Array.new
                        grounder = ParameterGrounder.new(@root['initial'])
                        combinator(bucket, grounder, procedure, params.keys, params, Hash.new, 0)
                        return bucket
                end
identify_immutable_variables() click to toggle source

Find immutable variables – variables that will never be affected with any actions. Then reduce the size of their domain by 1 only i.e. the possible value is only their initial value. BUGGY! – operator’s effects may contain other object’s variable

# File lib/sfp/sas_translator.rb, line 294
def identify_immutable_variables
        def is_this(ref)
                ref.length > 7 and (ref[0,7] == '$.this.' or ref[0,7] == '$.self.')
        end

        mutables = {}
        @variables.each_key { |k| mutables[k] = false }
        @variables.each_value do |var|
                next if not var.is_final
                var.init.each do |k1,v1|
                        next if k1[0,1] == '_' or
                                        not v1.is_a?(Hash) or
                                        not v1.isprocedure
                        v1['_effect'].each do |k2,v2|
                                next if k2[0,1] == '_' or not k2.isref
                                if is_this(k2)
                                        vname = var.name + k2[6..k2.length-1]
                                        mutables[vname] = true
                                else
                                        # TODO
                                end
                        end
                end
        end
        mutables.each do |vname, is_mutable|
                var = @variables[vname]
                if var != nil and not var.is_final and (not is_mutable)
                        var.clear
                        var << var.init
                        var.mutable = false
                end
        end
end
is_this(ref) click to toggle source
# File lib/sfp/sas_translator.rb, line 295
def is_this(ref)
        ref.length > 7 and (ref[0,7] == '$.this.' or ref[0,7] == '$.self.')
end
normalize_formula(formula, dump=false) click to toggle source

normalize the given first-order formula by transforming it to DNF

# File lib/sfp/sas_translator.rb, line 1121
def normalize_formula(formula, dump=false)
        {:formula => formula}.accept(ImplicationToDisjunction)

        def create_equals_constraint(value)
                return {'_context'=>'constraint', '_type'=>'equals', '_value'=>value}
        end

        def create_not_equals_constraint(value)
                return {'_context'=>'constraint', '_type'=>'not-equals', '_value'=>value}
        end

        def create_not_constraint(key, parent)
                return {'_context'=>'constraint', '_type'=>'not', '_self'=>key, '_parent'=>parent}
        end

        def create_and_constraint(key, parent)
                return {'_context'=>'constraint', '_type'=>'and', '_self'=>key, '_parent'=>parent}
        end

        def create_or_constraint(key, parent)
                return {'_context'=>'constraint', '_type'=>'or', '_self'=>key, '_parent'=>parent}
        end

        def array_to_or_constraint(arr)
                c = {'_context'=>'constraint', '_type'=>'or'}
                arr.each { |v| c[Sfp::SasTranslator.next_constraint_key] = v }
                return c
        end

        # combinatorial method for all possible values of nested reference
        # using recursive method
        def ref_combinator(bucket, parent, names, last_value, last_names=nil,
                        index=0, selected=Hash.new)

                return if names[index] == nil
                var_name = parent + '.' + names[index]
                if not @variables.has_key?(var_name)
                        raise VariableNotFoundException, 'Variable not found: ' + var_name
                end

                if index >= names.length or (index >= names.length-1 and last_value != nil)
                        selected[var_name] = last_value if last_value != nil
                        last_names << var_name if last_names != nil
                        result = selected.clone
                        result['_context'] = 'constraint'
                        result['_type'] = 'and'
                        bucket << result
                else
                        @variables[var_name].each { |v|
                                next if v.is_a?(Hash) and v.isnull
                                v = v.ref if v.is_a?(Hash) and v.isobject
                                selected[var_name] = create_equals_constraint(v)
                                ref_combinator(bucket, v, names, last_value, last_names, index+1, selected)
                        }
                end
                selected.delete(var_name)
        end

        def break_nested_reference(ref)
                rest, last = ref.pop_ref
                names = [last]
                while rest != '$' and not @variables.has_key?(rest)
                        rest, last = rest.pop_ref
                        names.unshift(last)
                end
                rest, last = rest.pop_ref
                names.unshift(last)
                return [names, rest]
        end

        def normalize_nested_right_only_multiple_values(left, right, formula)
                # TODO -- evaluate this method
                ref = right['_value']
                key1 = Sfp::SasTranslator.next_constraint_key
                c_or = create_or_constraint(key1, formula)
                @variables[ref].each do |v|
                        value = ( (v.is_a?(Hash) and v.isobject) ? v.ref : v)
                        key2 = Sfp::SasTranslator.next_constraint_key
                        c_and = create_and_constraint(key2, c_or)
                        #c_and[ref] = create_equals_constraint(value) ## HACK! -- this should be uncomment
                        c_and[left] = create_equals_constraint(value) if right['_type'] == 'equals'
                        c_and[left] = create_not_equals_constraint(value) if right['_type'] == 'not-equals'
                        c_or[key2] = c_and
                end
                formula.delete(left)
                formula[key1] = c_or
                return key1
        end

        def normalize_nested_right_values(left, right, formula)
                # TODO
                #puts 'nested right: ' + left + ' = ' + right['_value']

                raise TranslationException, "not implemented: normalized_nested_right => #{right}"
        end

        def normalize_nested_right_only(left, right, formula)
                value = right['_value']
                return if @variables.has_key?(value) and @variables[value].is_final

                if @variables.has_key?(value)
                        normalize_nested_right_only_multiple_values(left, right, formula)
                else
                        normalize_nested_right_values(left, right, formula)
                end
        end

        def normalize_nested_left_right(left, right, formula)
                # TODO
                #puts 'nested left-right'
                #names, rest = break_nested_reference(left)
                #bucket1 = Array.new
                #last_names1 = Array.new
                #ref_combinator(bucket1, rest, names, nil, last_names1)

                raise TranslationException, 'not implemented: normalized_nested_left_right'
        end

        def normalize_nested_left_only(left, right, formula)
                names, rest = break_nested_reference(left)
                bucket = Array.new
                ref_combinator(bucket, rest, names, right)
                formula.delete(left)
                if bucket.length > 0
                        key = Sfp::SasTranslator.next_constraint_key
                        formula[key] = array_to_or_constraint(bucket)
                        to_and_or_graph(formula[key])
                        return key
                end
        end

        # transform a first-order formula into AND/OR graph
        def to_and_or_graph(formula)
                keys = formula.keys
                keys.each { |k|
                        next if k[0,1] == '_'
                        v = formula[k]
                        if k.isref and not @variables.has_key?(k)
                                if v.is_a?(Hash) and v.isconstraint
                                        if (v['_type'] == 'equals' or v['_type'] == 'not-equals') and
                                                        v['_value'].is_a?(String) and v['_value'].isref and
                                                        not @variables.has_key?(v['_value'])
                                                # nested left & right
                                                normalize_nested_left_right(k, v, formula)
                                        elsif (v['_type'] == 'or' or v['_type'] == 'and')
                                                to_and_or_graph(v)
                                        else
                                                # nested left only
                                                normalize_nested_left_only(k, v, formula)
                                        end
                                end
                        else
                                if v.is_a?(Hash) and v.isconstraint
                                        if (v['_type'] == 'equals' or v['_type'] == 'not-equals') and
                                                        v['_value'].is_a?(String) and v['_value'].isref 
                                                # nested right only
                                                normalize_nested_right_only(k, v, formula)
                                        elsif (v['_type'] == 'or' or v['_type'] == 'and')
                                                to_and_or_graph(v)
                                        end
                                end
                        end
                }
        end


        # Recursively pull statements that has the same AND/OR operator.
        # Only receive a formula with AND, OR, EQUALS constraints.
        #
        # return false if there is any contradiction of facts, otherwise true
        def flatten_and_or_graph(formula)
                # transform formula into a format:
                #   (x1 and x2) or (y1 and y2 and y3) or z1
                is_and_or_tree = false
                formula.keys.each { |k|
                        next if k[0,1] == '_'
                        v = formula[k]
                        if v.is_a?(Hash) and v.isconstraint
                                if v['_type'] == 'or' or v['_type'] == 'and'
                                        if not flatten_and_or_graph(v)
                                                # remove it because it's not consistent
                                                formula.delete(k)
                                                v['_parent'] = nil
                                        end

                                        if formula['_type'] == v['_type']
                                                # pull-out all node's elements
                                                v.keys.each { |k1|
                                                        next if k1[0,1] == '_'
                                                        v1 = v[k1]
                                                        # check contradiction facts
                                                        if formula.has_key?(k1)
                                                                return false if formula[k1]['_type'] != v1['_type']
                                                                return false if formula[k1]['_value'] != v1['_value']
                                                        else
                                                                formula[k1] = v1
                                                        end
                                                }
                                                formula.delete(k)
                                        end
                                        is_and_or_tree = true if formula['_type'] == 'and' and v['_type'] == 'or'
                                end
                        end
                }
                # dot-product the nodes
                def cross_product_and(bucket, names, formula, values=Hash.new, index=0)
                        if index >= names.length
                                key = Sfp::SasTranslator.next_constraint_key
                                c = create_and_constraint(key, formula)
                                values.each { |k,v| c[k] = v }
                                if flatten_and_or_graph(c)
                                        # add the constraint because it's consistent
                                        formula[key] = c
                                end
                        else
                                key = names[index]
                                val = formula[ key ]
                                if val.is_a?(Hash) and val.isconstraint and val['_type'] == 'or'
                                        val.each { |k,v|
                                                next if k[0,1] == '_'
                                                values[k] = v
                                                cross_product_and(bucket, names, formula, values, index+1)
                                                values.delete(k)
                                        }
                                else
                                        values[key] = val
                                        cross_product_and(bucket, names, formula, values, index+1)
                                end
                        end
                end
                if is_and_or_tree
                        # change it into OR->AND tree
                        names = Array.new
                        formula.keys.each { |k| names << k if k[0,1] != '_' }
                        bucket = Array.new
                        cross_product_and(bucket, names, formula)
                        names.each { |k| formula.delete(k) }
                        formula['_type'] = 'or'
                end

                return true
        end

        # 'var_name' := x, value := p1
        # variable x := p1 | p2 | p3
        # return an array (p2, p3)
        def get_list_not_value_of(var_name, value)
                raise VariableNotFoundException, 'Variable not found: ' + var_name if
                        not @variables.has_key?(var_name)
                if value.is_a?(String) and value.isref
                        value = @root['initial'].at?(value)
                elsif value.is_a?(Hash) and value.isnull
                        value = @variables[var_name][0]
                end
                return (@variables[var_name] - [value])
        end

        # variable x := p1 | p2 | p3
        # then formula  (x not-equals p1) is transformed into
        # formula ( (x equals p2) or (x equals p3) )
        def not_equals_statement_to_or_constraint(formula)
                formula.keys.each do |k|
                        next if k[0,1] == '_'
                        v = formula[k]
                        if v.is_a?(Hash) and v.isconstraint
                                if v['_type'] == 'or' or v['_type'] == 'and'
                                        not_equals_statement_to_or_constraint(v)
                                elsif v['_type'] == 'not-equals'
                                        key1 = Sfp::SasTranslator.next_constraint_key
                                        c_or = create_or_constraint(key1, formula)
                                        get_list_not_value_of(k, v['_value']).each do |val1|
                                                val1 = val1.ref if val1.is_a?(Hash) and val1.isobject
                                                key2 = Sfp::SasTranslator.next_constraint_key
                                                c_and = create_and_constraint(key2, c_or)
                                                c_and[k] = create_equals_constraint(val1)
                                                c_or[key2] = c_and
                                        end
                                        formula.delete(k)
                                        formula[key1] = c_or
                                end
                        end
                end
        end

        def substitute_template(grounder, template, parent)
                id = Sfp::SasTranslator.next_constraint_key
                c_and = Sfp::Helper.deep_clone(template)
                c_and['_self'] = id
                c_and.accept(grounder)
                parent[id] = c_and
                remove_not_and_iterator_constraint(c_and)
                c_and
        end

        # Remove the following type of constraint in the given formula:
        # - NOT constraints by transforming them into EQUALS, NOT-EQUALS, AND, OR constraints
        # - ARRAY-Iterator constraint by extracting all possible values of given ARRAY
        #
        def remove_not_and_iterator_constraint(formula)
                # (not (equals) (not-equals) (and) (or))
                if formula.isconstraint and formula['_type'] == 'not'
                        formula['_type'] = 'and'
                        formula.each { |k,v|
                                next if k[0,1] == '_'
                                if v.is_a?(Hash) and v.isconstraint
                                        case v['_type']
                                        when 'equals'
                                                v['_type'] = 'not-equals'
                                        when 'not-equals'
                                                v['_type'] = 'equals'
                                        when 'and'
                                                v['_type'] = 'or'
                                                v.keys.each { |k1|
                                                        next if k1[0,1] == '_'
                                                        v1 = v[k1]
                                                        k2 = Sfp::SasTranslator.next_constraint_key
                                                        c_not = create_not_constraint(k2, v)
                                                        c_not[k1] = v1
                                                        v1['_parent'] = c_not
                                                        v.delete(k1)
                                                        remove_not_and_iterator_constraint(c_not)
                                                }
                                        when 'or'
                                                v['_type'] = 'and'
                                                v.keys.each { |k1|
                                                        next if k1[0,1] == '_'
                                                        v1 = v[k1]
                                                        k2 = Sfp::SasTranslator.next_constraint_key
                                                        c_not = create_not_constraint(k2, v)
                                                        c_not[k1] = v1
                                                        v1['_parent'] = c_not
                                                        v.delete(k1)
                                                        remove_not_and_iterator_constraint(c_not)
                                                }
                                        else
                                                raise TranslationException, 'unknown rules: ' + v['_type']
                                        end
                                end
                        }
                elsif formula.isconstraint and formula['_type'] == 'iterator'
                        ref = formula['_value']
                        var = '$.' + formula['_variable']
                        if @arrays.has_key?(ref)
                                # substitute ARRAY
                                total = @arrays[ref]
                                grounder = ParameterGrounder.new(@root['initial'], {})
                                for i in 0..(total-1)
                                        grounder.map.clear
                                        grounder.map[var] = ref + "[#{i}]"
                                        substitute_template(grounder, formula['_template'], formula)
                                end
                        else
                                setvalue = (ref.is_a?(Array) ? ref : @root['initial'].at?(ref))
                                if setvalue.is_a?(Hash) and setvalue.isset
                                        # substitute SET
                                        grounder = ParameterGrounder.new(@root['initial'], {})
                                        setvalue['_values'].each do |v|
                                                grounder.map.clear
                                                grounder.map[var] = v
                                                substitute_template(grounder, formula['_template'], formula)
                                        end
                                elsif setvalue.is_a?(Array)
                                        grounder = ParameterGrounder.new(@root['initial'], {})
                                        setvalue.each do |v|
                                                grounder.map.clear
                                                grounder.map[var] = v
                                                substitute_template(grounder, formula['_template'], formula)
                                        end
                                else
                                        #puts setvalue.inspect + ' -- ' + formula.ref + ' -- ' + var.to_s
                                        #raise UndefinedValueException, 'Undefined'
                                        raise UndefinedValueException.new(var)
                                end
                        end
                        formula['_type'] = 'and'
                        formula.delete('_value')
                        formula.delete('_variable')
                        formula.delete('_template')
                elsif formula.isconstraint and formula['_type'] == 'forall'
                        classref = '$.' + formula['_class']
                        raise TypeNotFoundException, classref if not @types.has_key?(classref)
                        var = '$.' + formula['_variable']
                        grounder = ParameterGrounder.new(@root['initial'], {})
                        @types[classref].each do |v|
                                next if v == nil or (v.is_a?(Hash) and v.isnull)
                                grounder.map.clear
                                grounder.map[var] = v.ref
                                substitute_template(grounder, formula['_template'], formula)
                        end
                        formula['_type'] = 'and'
                        formula.delete('_class')
                        formula.delete('_variable')
                        formula.delete('_template')
                else
                        formula.each { |k,v|
                                next if k[0,1] == '_'
                                remove_not_and_iterator_constraint(v) if v.is_a?(Hash) and v.isconstraint
                        }
                end
        end

        ### testing/debugging methods
        def calculate_depth(formula, depth)
                formula.each { |k,v|
                        next if k[0,1] == '_'
                        depth = calculate_depth(v, depth+1)
                        break
                }
                depth
        end

        def total_element(formula, total=0, total_or=0, total_and=0)
                formula.each { |k,v|
                        next if k[0,1] == '_'
                        if v['_type'] == 'or'
                                total_or += 1
                        elsif v['_type'] == 'and'
                                total_and += 1
                        else
                        end
                        total, total_or, total_and = total_element(v, total+1, total_or, total_and)
                }
                [total,total_or,total_and]
        end

        def visit_and_or_graph(formula, map={}, total=0)
                if formula['_type'] == 'and'
                        map = map.clone
                        is_end = true
                        formula.each do |k,v|
                                next if k[0,1] == '_'
                                if v['_type'] == 'equals'
                                        # bad branch
                                        if map.has_key?(k) and map[k] != v['_value']
                                                return
                                        end
                                        map[k] = v['_value']
                                elsif v['_type'] == 'and' or v['_type'] == 'or'
                                        is_end = false
                                end
                        end

                        if is_end
                                # map is valid conjunction
                        else
                                formula.each do |k,v|
                                        next if k[0,1] == '_'
                                        if v['_type'] == 'and' or v['_type'] == 'or'
                                                return visit_and_or_graph(v, map, total)
                                        end
                                end
                        end

                elsif formula['_type'] == 'or'
                        formula.each do |k,v|
                                next if k[0,1] == '_'
                                if v['_type'] == 'equals'
                                        # bad branch
                                        if map.has_key?(k) and map[k] != v['_value']
                                        end
                                        final_map = map.clone
                                        final_map[k] = v['_value']
                                        # map is valid conjunction
                                elsif v['_type'] == 'and' or v['_type'] == 'or'
                                        visit_and_or_graph(v, map, total)
                                end
                        end

                end
                total
        end
        ### end of testing/debugging methods

        remove_not_and_iterator_constraint(formula)
        to_and_or_graph(formula)
        not_equals_statement_to_or_constraint(formula)

        return flatten_and_or_graph(formula)
end
normalize_nested_left_only(left, right, formula) click to toggle source
# File lib/sfp/sas_translator.rb, line 1239
def normalize_nested_left_only(left, right, formula)
        names, rest = break_nested_reference(left)
        bucket = Array.new
        ref_combinator(bucket, rest, names, right)
        formula.delete(left)
        if bucket.length > 0
                key = Sfp::SasTranslator.next_constraint_key
                formula[key] = array_to_or_constraint(bucket)
                to_and_or_graph(formula[key])
                return key
        end
end
normalize_nested_left_right(left, right, formula) click to toggle source
# File lib/sfp/sas_translator.rb, line 1228
def normalize_nested_left_right(left, right, formula)
        # TODO
        #puts 'nested left-right'
        #names, rest = break_nested_reference(left)
        #bucket1 = Array.new
        #last_names1 = Array.new
        #ref_combinator(bucket1, rest, names, nil, last_names1)

        raise TranslationException, 'not implemented: normalized_nested_left_right'
end
normalize_nested_right_only(left, right, formula) click to toggle source
# File lib/sfp/sas_translator.rb, line 1217
def normalize_nested_right_only(left, right, formula)
        value = right['_value']
        return if @variables.has_key?(value) and @variables[value].is_final

        if @variables.has_key?(value)
                normalize_nested_right_only_multiple_values(left, right, formula)
        else
                normalize_nested_right_values(left, right, formula)
        end
end
normalize_nested_right_only_multiple_values(left, right, formula) click to toggle source
# File lib/sfp/sas_translator.rb, line 1191
def normalize_nested_right_only_multiple_values(left, right, formula)
        # TODO -- evaluate this method
        ref = right['_value']
        key1 = Sfp::SasTranslator.next_constraint_key
        c_or = create_or_constraint(key1, formula)
        @variables[ref].each do |v|
                value = ( (v.is_a?(Hash) and v.isobject) ? v.ref : v)
                key2 = Sfp::SasTranslator.next_constraint_key
                c_and = create_and_constraint(key2, c_or)
                #c_and[ref] = create_equals_constraint(value) ## HACK! -- this should be uncomment
                c_and[left] = create_equals_constraint(value) if right['_type'] == 'equals'
                c_and[left] = create_not_equals_constraint(value) if right['_type'] == 'not-equals'
                c_or[key2] = c_and
        end
        formula.delete(left)
        formula[key1] = c_or
        return key1
end
normalize_nested_right_values(left, right, formula) click to toggle source
# File lib/sfp/sas_translator.rb, line 1210
def normalize_nested_right_values(left, right, formula)
        # TODO
        #puts 'nested right: ' + left + ' = ' + right['_value']

        raise TranslationException, "not implemented: normalized_nested_right => #{right}"
end
not_equals_statement_to_or_constraint(formula) click to toggle source

variable x := p1 | p2 | p3 then formula (x not-equals p1) is transformed into formula ( (x equals p2) or (x equals p3) )

# File lib/sfp/sas_translator.rb, line 1381
def not_equals_statement_to_or_constraint(formula)
        formula.keys.each do |k|
                next if k[0,1] == '_'
                v = formula[k]
                if v.is_a?(Hash) and v.isconstraint
                        if v['_type'] == 'or' or v['_type'] == 'and'
                                not_equals_statement_to_or_constraint(v)
                        elsif v['_type'] == 'not-equals'
                                key1 = Sfp::SasTranslator.next_constraint_key
                                c_or = create_or_constraint(key1, formula)
                                get_list_not_value_of(k, v['_value']).each do |val1|
                                        val1 = val1.ref if val1.is_a?(Hash) and val1.isobject
                                        key2 = Sfp::SasTranslator.next_constraint_key
                                        c_and = create_and_constraint(key2, c_or)
                                        c_and[k] = create_equals_constraint(val1)
                                        c_or[key2] = c_and
                                end
                                formula.delete(k)
                                formula[key1] = c_or
                        end
                end
        end
end
post_support_premise(operator, premise) click to toggle source

return true if postcondition supports premise

# File lib/sfp/sas_translator.rb, line 381
def post_support_premise(operator, premise)
        premise.each { |var,c|
                return true if var[0,1] != '_' and operator.has_key?(var) and
                        !operator[var].post.nil? and operator[var].post == c['_value']
        }
        false
end
post_threat_conclusion(operator, conclusion) click to toggle source
# File lib/sfp/sas_translator.rb, line 389
def post_threat_conclusion(operator, conclusion)
        conclusion.each { |var,c|
                return true if var[0,1] == '_' and operator.has_key?(var) and
                        !operator[var].post.nil? and operator[var].post != c['_value']
        }
        false
end
postprocess_simple_global_constraint() click to toggle source

Method for postprocessing simple global constraints

# File lib/sfp/sas_translator.rb, line 331
def postprocess_simple_global_constraint
        @operators.keys.each do |name|
                # skip global, sometime, and goal verifier operators
                next if name =~ /\-globalop\-/
                next if name =~ /\-sometime\-/
                next if name =~ /\-goal\-/

                operator = @operators[name]
                @operators.delete(name)

                postprocess_simple_global_constraint_to_operator(operator).each { |op|
                        @operators[op.name] = op
                }
        end if @operators.is_a?(Hash)
end
postprocess_simple_global_constraint_to_operator(operator) click to toggle source
# File lib/sfp/sas_translator.rb, line 347
def postprocess_simple_global_constraint_to_operator(operator)
        return [operator] if GlobalConstraintMethod == 2

        def enforce_equals_constraint(operator, var, val)
                if operator.has_key?(var)
                        return nil if !operator[var].pre.nil? or operator[var].pre != val
                        operator[var].pre = val
                else
                        operator[var] = Parameter.new(@variables[var], val)
                end
                operator
        end

        if @global_simple_conjunctions.is_a?(Hash)
                # simple conjunction
                @global_simple_conjunctions.each do |var,c|
                        if c['_type'] == 'and'
                                c.each { |k,v| return [] if enforce_equals_constraint(operator, k, v['_value']).nil? }
                        else c['_type'] == 'equals'
                                return [] if enforce_equals_constraint(operator, var, c['_value']).nil?
                        end
                end
        end

        # return true if precondition supports premise
        def pre_support_premise(operator, premise)
                premise.each { |var,c|
                        next if var[0,1] == '_'
                        return false if !operator.has_key?(var) or (!operator[var].pre.nil? and operator[var].pre != c['_value'])
                }
                true
        end

        # return true if postcondition supports premise
        def post_support_premise(operator, premise)
                premise.each { |var,c|
                        return true if var[0,1] != '_' and operator.has_key?(var) and
                                !operator[var].post.nil? and operator[var].post == c['_value']
                }
                false
        end

        def post_threat_conclusion(operator, conclusion)
                conclusion.each { |var,c|
                        return true if var[0,1] == '_' and operator.has_key?(var) and
                                !operator[var].post.nil? and operator[var].post != c['_value']
                }
                false
        end

        def pre_threat_conclusion(operator, conclusion)
                conclusion.each { |var,c|
                        next if var[0,1] == '_'
                        return true if !operator.has_key?(var) or (!operator[var].pre.nil? and operator[var].pre != c['_value'])
                }
                false
        end

        return [operator] if not @global_simple_implications.is_a?(Hash)

        @global_simple_implications.each do |id,imply|
                # If the operator's precondition support the premise or
                # if the operator's postcondition support the premise, then
                # it should support the conclusion as well.
                if pre_support_premise(operator, imply['_premise']) or
                   post_support_premise(operator, imply['_premise'])
                        imply['_conclusion'].each do |var,c|
                                next if var[0,1] == '_'
                                if operator.has_key?(var)
                                        if operator[var].pre.nil? # enforce the operator to support the conclusion
                                                operator[var].pre = c['_value']
                                        end
                                        # this operator's does not support conclusion, then remove it from operators list
                                        return [] if operator[var].pre != c['_value']
                                else
                                        # enforce the operator to support the conclusion
                                        operator[var] = Parameter.new(@variables[var], c['_value'])
                                end
                        end
                end
        end
        
        results = []
        @global_simple_implications.each do |id,imply|
                if pre_threat_conclusion(operator, imply['_conclusion']) or
                   post_threat_conclusion(operator, imply['_conclusion'])
                        imply['_premise'].each do |var,c|
                                next if var[0,1] == '_'
                                @variables[var].not(c['_value']).each do |x|
                                        op = operator.clone
                                        if op.has_key?(var)
                                                if op[var].pre != x
                                                        op[var].pre == x
                                                        results << op
                                                end
                                        else
                                                op[var] = Parameter.new(@variables[var], x)
                                                results << op
                                        end
                                end
                        end
                end
        end
        return [operator] if results.length <= 0
        results
end
pre_support_premise(operator, premise) click to toggle source

return true if precondition supports premise

# File lib/sfp/sas_translator.rb, line 372
def pre_support_premise(operator, premise)
        premise.each { |var,c|
                next if var[0,1] == '_'
                return false if !operator.has_key?(var) or (!operator[var].pre.nil? and operator[var].pre != c['_value'])
        }
        true
end
pre_threat_conclusion(operator, conclusion) click to toggle source
# File lib/sfp/sas_translator.rb, line 397
def pre_threat_conclusion(operator, conclusion)
        conclusion.each { |var,c|
                next if var[0,1] == '_'
                return true if !operator.has_key?(var) or (!operator[var].pre.nil? and operator[var].pre != c['_value'])
        }
        false
end
preprocess_simple_global_constraint() click to toggle source
# File lib/sfp/sas_translator.rb, line 454
def preprocess_simple_global_constraint
        return if GlobalConstraintMethod == 2

        def conjunction_only(id, f)
                #return true if @variables.has_key?(id) and f['_type'] == 'equals'
                return true if f['_type'] == 'equals'
                if f['_type'] == 'and'
                        f.each { |k,v| return false if k[0,1] != '_' and not conjunction_only(k, v) }
                        return true
                end

                false
        end

        def simple_formulae(id, f)
                if f['_type'] == 'imply'
                        f.each { |k,v| return false if k[0,1] != '_' and not conjunction_only(k, v) }
                        return true
                end
                conjunction_only(id, f)
        end

        global = @root['global']
        simples = global.select { |k,v| k[0,1] != '_' and
                (!k.isref or @variables.has_key?(k)) and
                simple_formulae(k, v)
        }

        @global_simple_conjunctions = {}
        @global_simple_implications = {}
        simples.each do |id,constraint|
                case constraint['_type']
                when 'equals', 'and'
                        raise TranslationException, 'Invalid global constraint' if not normalize_formula(constraint)
                        @global_simple_conjunctions[id] = constraint
                when 'imply'
                        constraint.keys.each { |k|
                                next if k[0,1] == '_'
                                raise TranslationException, 'Invalid global constraint' if not normalize_formula(constraint[k])
                                constraint[k].select { |k,v| k[0,1] != '_' }
                                constraint['_premise'] = constraint[k] if constraint[k]['_subtype'] == 'premise'
                                constraint['_conclusion'] = constraint[k] if constraint[k]['_subtype'] == 'conclusion'
                        }
                        @global_simple_implications[id] = constraint
                else
                        raise Exception, "Bug: non-simple formulae detected - #{constraint['_type']}"
                end
                global.delete(id)
        end
end
process_conditions(cond) click to toggle source

process the conditions of an operator and return all possible set of conditions

# File lib/sfp/sas_translator.rb, line 807
def process_conditions(cond)
        map = Hash.new
        cond.each { |k,v|
                next if k[0,1] == '_'
                if v['_type'] == 'equals'
                        map[k] = v['_value']
                end
        }
        return map
end
process_effects(eff) click to toggle source

process the effects of operator and return all possible sets of effects

# File lib/sfp/sas_translator.rb, line 827
def process_effects(eff)
        map = Hash.new
        eff.each { |k,v|
                next if k[0,1] == '_'
                if v['_type'] = 'equals'
                        map[k] = v['_value']
                end
        }
        return map
end
process_global_constraint() click to toggle source

 End of methods for processing simple global constraints #####

# File lib/sfp/sas_translator.rb, line 507
def process_global_constraint
        @total_complex_global_constraints = 0

        ### normalize global constraint formula ###
        if @root.has_key?('global') and @root['global'].isconstraint
                preprocess_simple_global_constraint if ActivateSimpleGlobalConstraint

                keys = @root['global'].keys.select { |k| k[0,1] != '_' }
                @total_complex_global_constraints = keys.length

                raise TranslationException, 'Invalid global constraint' if 
                                not normalize_formula(@root['global'], true)

                if GlobalConstraintMethod == 1 and @total_complex_global_constraints > 0
                        # dummy variable
                        @global_var = Variable.new(GlobalVariable, '$.Boolean', -1, false, true)
                        @global_var << true
                        @global_var << false
                        @variables[@global_var.name] = @global_var
                        # dummy operator
                        eff = Parameter.new(@global_var, false, true)
                        if @root['global']['_type'] == 'and'
                                op = Operator.new(GlobalOperator, 0)
                                op[eff.var.name] = eff
                                @operators[op.name] = op
                        else
                                index = 0
                                @root['global'].each do |name,constraint|
                                        next if name[0,1] == '_'
                                        map_cond = and_equals_constraint_to_map(constraint)
                                        op = Operator.new(GlobalOperator + index.to_s, 0)
                                        op[eff.var.name] = eff
                                        map_cond.each do |k,v|
                                                next if k[0,1] == '_'
                                                raise VariableNotFoundException, k if not @variables.has_key?(k)
                                                op[@variables[k].name] = Parameter.new(@variables[k], v)
                                        end
                                        @operators[op.name] = op
                                end
                        end
                end
        end
end
process_goal(goal) click to toggle source
# File lib/sfp/sas_translator.rb, line 589
def process_goal(goal)
        raise TranslationException, 'invalid goal constraint' if not normalize_formula(goal)
        @goals = []
        if goal['_type'] == 'and'
                map = and_equals_constraint_to_map(goal)
                map.each { |name,value|
                        var = @variables[name]
                        value = @types[var.type][0] if value.is_a?(Hash) and value.isnull
                        value = @root['initial'].at?(value) if value.is_a?(String) and value.isref
                        var.goal = value
                        if not var.mutable
                                var.init = var.goal
                                var.clear
                                var << var.init
                        end
                }
                @goals << map
        elsif goal['_type'] == 'or'
                count = 0
                var = Variable.new(GoalVariable, '$.Boolean', -1, false, true)
                var << true
                var << false
                @variables[var.name] = var
                eff = Parameter.new(var, false, true)

                goal.each { |k,g|
                        next if k[0,1] == '_'
                        op = Operator.new("#{GoalOperator}#{count}", 0)
                        op[var.name] = eff
                        map = and_equals_constraint_to_map(g)
                        map.each { |k1,v1|
                                var = @variables[k1]
                                op[@variables[k1].name] = Parameter.new(@variables[k1], v1, nil)
                        }
                        @operators[op.name] = op
                        @goals << map
                }
        end
end
process_grounded_operator(op, conditions, effects) click to toggle source

process grounded operator (no parameter exists)

# File lib/sfp/sas_translator.rb, line 861
def process_grounded_operator(op, conditions, effects)
        map_cond = and_equals_constraint_to_map(conditions)
        map_eff = and_equals_constraint_to_map(effects)
        keys = map_cond.keys.concat(map_eff.keys)

        # combine map_cond & map_eff if any of them has >1 items
        op_id = Sfp::SasTranslator.next_operator_id
        sas_op = Operator.new(op.ref, op['_cost'])
        sas_op.params = op['_parameters']

        keys.each { |k|
                return if not @variables.has_key?(k)
                pre = (!map_cond.has_key?(k) ? nil : map_cond[k])
                #pre = @root['initial'].at?(pre) if pre.is_a?(String) and pre.isref
                post = (!map_eff.has_key?(k) ? nil : map_eff[k])
                #post = @root['initial'].at?(post) if post.is_a?(String) and post.isref
                sas_op[@variables[k].name] = Parameter.new(@variables[k], pre, post)
        }

        if GlobalConstraintMethod == 1 and @total_complex_global_constraints > 0
                @operators[sas_op.name] = sas_op if apply_global_constraint_method_1(sas_op)
        elsif GlobalConstraintMethod == 2 or GlobalConstraintMethod == 3
                @operators[sas_op.name] = sas_op if apply_global_constraint_method_2(sas_op)
        else
                @operators[sas_op.name] = sas_op
        end
end
process_operator(op) click to toggle source

process given operator

# File lib/sfp/sas_translator.rb, line 839
def process_operator(op)
        # return if given operator is not valid
        # - method "normalize_formula" return false
        # - there's an exception during normalization process
        begin
                return if not normalize_formula(op['_condition'])
        rescue Exception => exp
                return
        end
        # at this step, the conditions formula has been normalized (AND/OR tree)
        # AND conditions
        if op['_condition']['_type'] == 'and'
                process_grounded_operator(op, op['_condition'], op['_effect'])
        else
                op['_condition'].each { |k,v|
                        next if k[0,1] == '_'
                        process_grounded_operator(op, v, op['_effect'])
                }
        end
end
process_procedure(procedure, object) click to toggle source

process all object procedures in order to get grounded SAS-operator

# File lib/sfp/sas_translator.rb, line 900
def process_procedure(procedure, object)
        #substitute_goal_value_in_effects(procedure)

        operators = ground_procedure_parameters(procedure)
        if operators != nil
                operators.each { |op| process_operator(op) }
        end
        # remove the procedure because we don't need it anymore
        object.delete(procedure['_self'])
end
process_sometime() click to toggle source
# File lib/sfp/sas_translator.rb, line 551
def process_sometime
        @root['sometime'].each do |k,v|
                next if k[0,1] == '_'
                # dummy-variable
                var = Variable.new(SometimeVariablePrefix + k, '$.Boolean', -1, false, true)
                var << true
                var << false
                @variables[var.name] = var
                # dummy-operator
                op = Operator.new(SometimeOperatorPrefix + k, 0)
                eff = Parameter.new(var, false, true)
                op[eff.var.name] = eff
                map = and_equals_constraint_to_map(v)
                map.each { |k1,v1|
                        op[@variables[k1].name] = Parameter.new(@variables[k1], v1, nil)
                }
                @operators[op.name] = op
        end
end
process_sometime_after() click to toggle source
# File lib/sfp/sas_translator.rb, line 571
def process_sometime_after
        # TODO
        @root['sometime-after'].each do |k,v|
                next if k[0,1] == '_'
                # dummy-variable
                var = Variable.new('sometime_after_' + k, '$.Boolean', -1, true, true)
                var << true
                var << false
                @variables[var.name] = var
                # normalize formula
                
                # dummy-operator
                op = Operator.new('-sometime_after_activate-' + k, 0)
                eff = Parameter.new(var, true, false)
                op[eff.var.name] = eff
        end
end
ref_combinator(bucket, parent, names, last_value, last_names=nil, index=0, selected=Hash.new) click to toggle source

combinatorial method for all possible values of nested reference using recursive method

# File lib/sfp/sas_translator.rb, line 1152
def ref_combinator(bucket, parent, names, last_value, last_names=nil,
                index=0, selected=Hash.new)

        return if names[index] == nil
        var_name = parent + '.' + names[index]
        if not @variables.has_key?(var_name)
                raise VariableNotFoundException, 'Variable not found: ' + var_name
        end

        if index >= names.length or (index >= names.length-1 and last_value != nil)
                selected[var_name] = last_value if last_value != nil
                last_names << var_name if last_names != nil
                result = selected.clone
                result['_context'] = 'constraint'
                result['_type'] = 'and'
                bucket << result
        else
                @variables[var_name].each { |v|
                        next if v.is_a?(Hash) and v.isnull
                        v = v.ref if v.is_a?(Hash) and v.isobject
                        selected[var_name] = create_equals_constraint(v)
                        ref_combinator(bucket, v, names, last_value, last_names, index+1, selected)
                }
        end
        selected.delete(var_name)
end
remove_not_and_iterator_constraint(formula) click to toggle source

Remove the following type of constraint in the given formula:

  • NOT constraints by transforming them into EQUALS, NOT-EQUALS, AND, OR constraints

  • ARRAY-Iterator constraint by extracting all possible values of given ARRAY

# File lib/sfp/sas_translator.rb, line 1419
def remove_not_and_iterator_constraint(formula)
        # (not (equals) (not-equals) (and) (or))
        if formula.isconstraint and formula['_type'] == 'not'
                formula['_type'] = 'and'
                formula.each { |k,v|
                        next if k[0,1] == '_'
                        if v.is_a?(Hash) and v.isconstraint
                                case v['_type']
                                when 'equals'
                                        v['_type'] = 'not-equals'
                                when 'not-equals'
                                        v['_type'] = 'equals'
                                when 'and'
                                        v['_type'] = 'or'
                                        v.keys.each { |k1|
                                                next if k1[0,1] == '_'
                                                v1 = v[k1]
                                                k2 = Sfp::SasTranslator.next_constraint_key
                                                c_not = create_not_constraint(k2, v)
                                                c_not[k1] = v1
                                                v1['_parent'] = c_not
                                                v.delete(k1)
                                                remove_not_and_iterator_constraint(c_not)
                                        }
                                when 'or'
                                        v['_type'] = 'and'
                                        v.keys.each { |k1|
                                                next if k1[0,1] == '_'
                                                v1 = v[k1]
                                                k2 = Sfp::SasTranslator.next_constraint_key
                                                c_not = create_not_constraint(k2, v)
                                                c_not[k1] = v1
                                                v1['_parent'] = c_not
                                                v.delete(k1)
                                                remove_not_and_iterator_constraint(c_not)
                                        }
                                else
                                        raise TranslationException, 'unknown rules: ' + v['_type']
                                end
                        end
                }
        elsif formula.isconstraint and formula['_type'] == 'iterator'
                ref = formula['_value']
                var = '$.' + formula['_variable']
                if @arrays.has_key?(ref)
                        # substitute ARRAY
                        total = @arrays[ref]
                        grounder = ParameterGrounder.new(@root['initial'], {})
                        for i in 0..(total-1)
                                grounder.map.clear
                                grounder.map[var] = ref + "[#{i}]"
                                substitute_template(grounder, formula['_template'], formula)
                        end
                else
                        setvalue = (ref.is_a?(Array) ? ref : @root['initial'].at?(ref))
                        if setvalue.is_a?(Hash) and setvalue.isset
                                # substitute SET
                                grounder = ParameterGrounder.new(@root['initial'], {})
                                setvalue['_values'].each do |v|
                                        grounder.map.clear
                                        grounder.map[var] = v
                                        substitute_template(grounder, formula['_template'], formula)
                                end
                        elsif setvalue.is_a?(Array)
                                grounder = ParameterGrounder.new(@root['initial'], {})
                                setvalue.each do |v|
                                        grounder.map.clear
                                        grounder.map[var] = v
                                        substitute_template(grounder, formula['_template'], formula)
                                end
                        else
                                #puts setvalue.inspect + ' -- ' + formula.ref + ' -- ' + var.to_s
                                #raise UndefinedValueException, 'Undefined'
                                raise UndefinedValueException.new(var)
                        end
                end
                formula['_type'] = 'and'
                formula.delete('_value')
                formula.delete('_variable')
                formula.delete('_template')
        elsif formula.isconstraint and formula['_type'] == 'forall'
                classref = '$.' + formula['_class']
                raise TypeNotFoundException, classref if not @types.has_key?(classref)
                var = '$.' + formula['_variable']
                grounder = ParameterGrounder.new(@root['initial'], {})
                @types[classref].each do |v|
                        next if v == nil or (v.is_a?(Hash) and v.isnull)
                        grounder.map.clear
                        grounder.map[var] = v.ref
                        substitute_template(grounder, formula['_template'], formula)
                end
                formula['_type'] = 'and'
                formula.delete('_class')
                formula.delete('_variable')
                formula.delete('_template')
        else
                formula.each { |k,v|
                        next if k[0,1] == '_'
                        remove_not_and_iterator_constraint(v) if v.is_a?(Hash) and v.isconstraint
                }
        end
end
reset_operators_name() click to toggle source
# File lib/sfp/sas_translator.rb, line 756
def reset_operators_name
        Sfp::SasTranslator.reset_operator_id
        ops = Hash.new
        @operators.each_value { |op|
                op.id = Sfp::SasTranslator.next_operator_id
                @operators.delete(op.name)
                op.update_name
                ops[op.name] = op
        }
        @operators = ops
end
sas() click to toggle source
# File lib/sfp/sas_translator.rb, line 690
def sas
        # version
        out = "begin_version\n3\nend_version\n"
        # metric
        out << "begin_metric\n1\nend_metric\n"

        benchmarks = {}

        ### use symbolic as key in map of variables
        vars = {}
        @variables.each { |k,v| vars[k.to_sym] = v }
        names = vars.keys

        # variables
        out << "#{names.length}\n"
        names.sort!
        names.each_index do |i|
                var = vars[ names[i] ]
                var.id = i
                out << var.to_sas(@root['initial'])
        end

        # mutex
        out << "0\n"

        # initial & goal state
        out << "begin_state\n"
        goal = ''
        goal_count = 0
        names.each do |name|
                var = vars[name]
                if var.init.is_a?(Hash) and var.init.isnull
                        out << "0\n"
                elsif var.init.is_a?(::Sfp::Unknown)
                        out << "#{var.length - 1}\n"
                else
                        val = var.index(var.init).to_s
                        raise TranslationException, "Unknown init: #{var.name}=#{var.init.inspect}" if val.length <= 0
                        out << "#{val}\n"
                end

                if var.goal != nil
                        goal << "#{var.id} #{var.index(var.goal)}\n"
                        goal_count += 1
                end
        end
        out << "end_state\nbegin_goal\n#{goal_count}\n#{goal}end_goal\n"

        # operators
        ops = ''
        total = 0
        @operators.each_value do |operator|
                next if operator.total_preposts <= 0
                sas = operator.to_sas(@root['initial'], vars)
                if not sas.nil?
                        ops << sas
                        total += 1
                end
        end
        out << "#{total}\n"
        out << ops

        # axioms
        out << "0"
end
search_and_merge_mutually_inclusive_operators() click to toggle source
# File lib/sfp/sas_translator.rb, line 244
def search_and_merge_mutually_inclusive_operators
        return if GlobalConstraintMethod != 3
        last = @g_operators.length-1
        @g_operators.each_index do |i|
                op1 = @g_operators[i]
                for j in i+1..last
                        op2 = @g_operators[j]
                        next if op1.modifier_id != op2.modifier_id or op1.conflict?(op2)
                        next if not (op1.supports?(op2) and op2.supports?(op1))
                        if op1.supports?(op2) and op2.supports?(op1)
                                op = op1.merge(op2)
                                op.modifier_id = op1.modifier_id
                                op1 = op
                        end
                end
                @operators[op1.name] = op1 if op1 != @g_operators[i]
        end
end
set_variable_values() click to toggle source

set possible values for each variable

# File lib/sfp/sas_translator.rb, line 1027
def set_variable_values
        @variables.each_value { |var|
                var.clear
                if not var.is_final
                        @types[var.type].each { |v| var << v }
                else
                        var << var.init
                end
        }
end
simple_formulae(id, f) click to toggle source
# File lib/sfp/sas_translator.rb, line 468
def simple_formulae(id, f)
        if f['_type'] == 'imply'
                f.each { |k,v| return false if k[0,1] != '_' and not conjunction_only(k, v) }
                return true
        end
        conjunction_only(id, f)
end
substitute_template(grounder, template, parent) click to toggle source
# File lib/sfp/sas_translator.rb, line 1405
def substitute_template(grounder, template, parent)
        id = Sfp::SasTranslator.next_constraint_key
        c_and = Sfp::Helper.deep_clone(template)
        c_and['_self'] = id
        c_and.accept(grounder)
        parent[id] = c_and
        remove_not_and_iterator_constraint(c_and)
        c_and
end
to_and_or_graph(formula) click to toggle source

transform a first-order formula into AND/OR graph

# File lib/sfp/sas_translator.rb, line 1253
def to_and_or_graph(formula)
        keys = formula.keys
        keys.each { |k|
                next if k[0,1] == '_'
                v = formula[k]
                if k.isref and not @variables.has_key?(k)
                        if v.is_a?(Hash) and v.isconstraint
                                if (v['_type'] == 'equals' or v['_type'] == 'not-equals') and
                                                v['_value'].is_a?(String) and v['_value'].isref and
                                                not @variables.has_key?(v['_value'])
                                        # nested left & right
                                        normalize_nested_left_right(k, v, formula)
                                elsif (v['_type'] == 'or' or v['_type'] == 'and')
                                        to_and_or_graph(v)
                                else
                                        # nested left only
                                        normalize_nested_left_only(k, v, formula)
                                end
                        end
                else
                        if v.is_a?(Hash) and v.isconstraint
                                if (v['_type'] == 'equals' or v['_type'] == 'not-equals') and
                                                v['_value'].is_a?(String) and v['_value'].isref 
                                        # nested right only
                                        normalize_nested_right_only(k, v, formula)
                                elsif (v['_type'] == 'or' or v['_type'] == 'and')
                                        to_and_or_graph(v)
                                end
                        end
                end
        }
end
to_sas() click to toggle source
# File lib/sfp/sas_translator.rb, line 59
def to_sas
        self.compile_step_1
        self.compile_step_2
        return self.sas
end
to_set(array) click to toggle source
# File lib/sfp/sas_translator.rb, line 225
def to_set(array)
        array.inject([]) { |result,item| result << item unless result.include?(item); result }
end
total_element(formula, total=0, total_or=0, total_and=0) click to toggle source
# File lib/sfp/sas_translator.rb, line 1532
def total_element(formula, total=0, total_or=0, total_and=0)
        formula.each { |k,v|
                next if k[0,1] == '_'
                if v['_type'] == 'or'
                        total_or += 1
                elsif v['_type'] == 'and'
                        total_and += 1
                else
                end
                total, total_or, total_and = total_element(v, total+1, total_or, total_and)
        }
        [total,total_or,total_and]
end
variable_name_and_value(var_id, value_index) click to toggle source
# File lib/sfp/sas_translator.rb, line 229
def variable_name_and_value(var_id, value_index)
        i = @vars.index { |v| v.id == var_id }
        var = @vars[i]
        return nil, nil if var.nil?
        return var.name, nil if value_index >= var.length or
                                value_index < 0
        value = var[value_index]
        if value.is_a?(Hash)
                return var.name, value.ref if value.isobject
                return var.name, nil
        else
                return var.name, value
        end
end
visit_and_or_graph(formula, map={}, total=0) click to toggle source
# File lib/sfp/sas_translator.rb, line 1546
def visit_and_or_graph(formula, map={}, total=0)
        if formula['_type'] == 'and'
                map = map.clone
                is_end = true
                formula.each do |k,v|
                        next if k[0,1] == '_'
                        if v['_type'] == 'equals'
                                # bad branch
                                if map.has_key?(k) and map[k] != v['_value']
                                        return
                                end
                                map[k] = v['_value']
                        elsif v['_type'] == 'and' or v['_type'] == 'or'
                                is_end = false
                        end
                end

                if is_end
                        # map is valid conjunction
                else
                        formula.each do |k,v|
                                next if k[0,1] == '_'
                                if v['_type'] == 'and' or v['_type'] == 'or'
                                        return visit_and_or_graph(v, map, total)
                                end
                        end
                end

        elsif formula['_type'] == 'or'
                formula.each do |k,v|
                        next if k[0,1] == '_'
                        if v['_type'] == 'equals'
                                # bad branch
                                if map.has_key?(k) and map[k] != v['_value']
                                end
                                final_map = map.clone
                                final_map[k] = v['_value']
                                # map is valid conjunction
                        elsif v['_type'] == 'and' or v['_type'] == 'or'
                                visit_and_or_graph(v, map, total)
                        end
                end

        end
        total
end