Module: Sfp::SasTranslator

Included in:
Parser
Defined in:
lib/sfp/sas_translator.rb

Overview

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

TODO:

  • nested reference on right-side statement (value of EQUALS/NOT-EQUALS)

  • a first-order logic formula

  • enumeration of values of particular type

  • SET abstract data-type, membership operators

Defined Under Namespace

Classes: GoalVisitor, ParameterGrounder, TypeNotFoundException, UndefinedValueException, ValueCollector, VariableCollector, VariableNotFoundException, Visitor

Constant Summary collapse

GlobalOperator = 
'-globalop-'
GlobalVariable = 
'_global_var'
SometimeOperatorPrefix = 
'-sometime-'
SometimeVariablePrefix = 
'-sometime-'
GoalOperator = 
'-goal-'
GoalVariable = 
'-goal-'
GlobalConstraintMethod =

1: proposed method, 2: patrik’s, 3: concurrent-actions

1
ActivateSimpleGlobalConstraint =

true

false
ImplicationToDisjunction = 
Object.new

Instance Attribute Summary collapse

Class Method Summary collapse

Instance Method Summary collapse

Instance Attribute Details

#axioms ⇒ Object (readonly)

Returns the value of attribute axioms.



57
58
59
 
# File 'lib/sfp/sas_translator.rb', line 57

def axioms
  @axioms
end

#benchmarks ⇒ Object (readonly)

Returns the value of attribute benchmarks.



57
58
59
 
# File 'lib/sfp/sas_translator.rb', line 57

def benchmarks
  @benchmarks
end

#goals ⇒ Object (readonly)

Returns the value of attribute goals.



57
58
59
 
# File 'lib/sfp/sas_translator.rb', line 57

def goals
  @goals
end

#operators ⇒ Object (readonly)

Returns the value of attribute operators.



57
58
59
 
# File 'lib/sfp/sas_translator.rb', line 57

def operators
  @operators
end

#root ⇒ Object

Returns the value of attribute root.



56
57
58
 
# File 'lib/sfp/sas_translator.rb', line 56

def root
  @root
end

#types ⇒ Object (readonly)

Returns the value of attribute types.



57
58
59
 
# File 'lib/sfp/sas_translator.rb', line 57

def types
  @types
end

#variables ⇒ Object (readonly)

Returns the value of attribute variables.



57
58
59
 
# File 'lib/sfp/sas_translator.rb', line 57

def variables
  @variables
end

Class Method Details

.next_axiom_id ⇒ Object

return the next axiom’s id



737
738
739
740
741
 
# File 'lib/sfp/sas_translator.rb', line 737

def self.next_axiom_id
  return (@@axiom_id += 1) if defined?(@@axiom_id) != nil
  @@axiom_id = 0
  return @@axiom_id
end

.next_constraint_id ⇒ Object

return the next constraint’s id



719
720
721
722
723
 
# File 'lib/sfp/sas_translator.rb', line 719

def self.next_constraint_id
  return (@@constraint_id += 1) if defined?(@@constraint_id) != nil
  @@constraint_id = 0
  return @@constraint_id
end

.next_constraint_key ⇒ Object 



725
726
727
 
# File 'lib/sfp/sas_translator.rb', line 725

def self.next_constraint_key
  return 'constraint_' + next_constraint_id.to_s
end

.next_operator_id ⇒ Object

return the next operator’s id



712
713
714
715
716
 
# File 'lib/sfp/sas_translator.rb', line 712

def self.next_operator_id
  return (@@op_id += 1) if defined?(@@op_id) != nil
  @@op_id = 0
  return @@op_id
end

.next_variable_id ⇒ Object

return the next variable’s id



730
731
732
733
734
 
# File 'lib/sfp/sas_translator.rb', line 730

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) ⇒ Object 



1514
1515
1516
1517
1518
 
# File 'lib/sfp/sas_translator.rb', line 1514

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



707
708
709
 
# File 'lib/sfp/sas_translator.rb', line 707

def self.reset_operator_id
  @@op_id = -1
end

Instance Method Details

#add_unknown_undefined_value_to_variables ⇒ Object 



957
958
959
960
961
962
963
964
 
# File 'lib/sfp/sas_translator.rb', line 957

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



950
951
952
953
954
955
 
# File 'lib/sfp/sas_translator.rb', line 950

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) ⇒ Object 



757
758
759
760
761
762
 
# File 'lib/sfp/sas_translator.rb', line 757

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) ⇒ Object 



966
967
968
969
 
# File 'lib/sfp/sas_translator.rb', line 966

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) ⇒ Object

return true if global constraint could be applied, otherwise false



972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
 
# File 'lib/sfp/sas_translator.rb', line 972

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) ⇒ Object 



1056
1057
1058
1059
1060
 
# File 'lib/sfp/sas_translator.rb', line 1056

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) ⇒ Object 



1091
1092
1093
1094
1095
1096
1097
1098
1099
1100
1101
 
# File 'lib/sfp/sas_translator.rb', line 1091

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) ⇒ Object

testing/debugging methods



1435
1436
1437
1438
1439
1440
1441
1442
 
# File 'lib/sfp/sas_translator.rb', line 1435

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) ⇒ Object

combinatorial method for all possible values of parameters using recursive method



878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
 
# File 'lib/sfp/sas_translator.rb', line 878

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



71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
 
# 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 { |type| type.uniq! }

    # 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.each_value { |type| type.uniq! }

  # 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 ⇒ Object 



65
66
67
68
69
 
# 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) ⇒ Object 



452
453
454
455
456
457
458
459
460
461
 
# File 'lib/sfp/sas_translator.rb', line 452

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) ⇒ Object

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



984
985
986
987
988
989
990
 
# File 'lib/sfp/sas_translator.rb', line 984

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) ⇒ Object

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



977
978
979
980
981
 
# File 'lib/sfp/sas_translator.rb', line 977

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) ⇒ Object 



1048
1049
1050
 
# File 'lib/sfp/sas_translator.rb', line 1048

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

#create_equals_constraint(value) ⇒ Object 



1036
1037
1038
 
# File 'lib/sfp/sas_translator.rb', line 1036

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

#create_not_constraint(key, parent) ⇒ Object 



1044
1045
1046
 
# File 'lib/sfp/sas_translator.rb', line 1044

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

#create_not_equals_constraint(value) ⇒ Object 



1040
1041
1042
 
# File 'lib/sfp/sas_translator.rb', line 1040

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

#create_or_constraint(key, parent) ⇒ Object 



1052
1053
1054
 
# File 'lib/sfp/sas_translator.rb', line 1052

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

#create_output ⇒ Object 



624
625
626
 
# File 'lib/sfp/sas_translator.rb', line 624

def create_output
  self.to_s
end

#cross_product_and(bucket, names, formula, values = Hash.new, index = 0) ⇒ Object

dot-product the nodes



1238
1239
1240
1241
1242
1243
1244
1245
1246
1247
1248
1249
1250
1251
1252
1253
1254
1255
1256
1257
1258
1259
1260
1261
1262
 
# File 'lib/sfp/sas_translator.rb', line 1238

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_axioms ⇒ Object 



933
934
935
936
 
# File 'lib/sfp/sas_translator.rb', line 933

def dump_axioms
  puts '--- axioms'
  @axioms.each { |ax| puts ax.to_s }
end

#dump_operators ⇒ Object 



928
929
930
931
 
# File 'lib/sfp/sas_translator.rb', line 928

def dump_operators
  puts '--- operators'
  @operators.each_value { |op| puts op.to_s + ' -- ' + op.params.inspect }
end

#dump_types ⇒ Object 



907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
 
# File 'lib/sfp/sas_translator.rb', line 907

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



923
924
925
926
 
# File 'lib/sfp/sas_translator.rb', line 923

def dump_vars
  puts '--- variables'
  @variables.each_value { |value| puts value.to_s }
end

#enforce_equals_constraint(operator, var, val) ⇒ Object 



345
346
347
348
349
350
351
352
353
 
# File 'lib/sfp/sas_translator.rb', line 345

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



258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
 
# File 'lib/sfp/sas_translator.rb', line 258

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) ⇒ Object

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



1203
1204
1205
1206
1207
1208
1209
1210
1211
1212
1213
1214
1215
1216
1217
1218
1219
1220
1221
1222
1223
1224
1225
1226
1227
1228
1229
1230
1231
1232
1233
1234
1235
1236
1237
1238
1239
1240
1241
1242
1243
1244
1245
1246
1247
1248
1249
1250
1251
1252
1253
1254
1255
1256
1257
1258
1259
1260
1261
1262
1263
1264
1265
1266
1267
1268
1269
1270
1271
1272
1273
1274
 
# File 'lib/sfp/sas_translator.rb', line 1203

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) ⇒ Object

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

Raises:



1279
1280
1281
1282
1283
1284
1285
1286
1287
1288
 
# File 'lib/sfp/sas_translator.rb', line 1279

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) ⇒ Object

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



852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
 
# File 'lib/sfp/sas_translator.rb', line 852

def ground_procedure_parameters(procedure)
  params = Hash.new
  procedure.each { |k,v|
    next if k[0,1] == '_'
    # if the specified parameter does not have any value,
    # then it's invalid procedure
    if not @types.has_key?( v['_isa'] )
      return nil
    end
    params[k] = Array.new
    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)
    @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) }
    #puts k.to_s + ": " + params[k].length.to_s
  }
  # 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 ⇒ Object

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



289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
 
# File 'lib/sfp/sas_translator.rb', line 289

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) ⇒ Object 



290
291
292
 
# File 'lib/sfp/sas_translator.rb', line 290

def is_this(ref)
  ref.length > 7 and (ref[0,7] == '$.this.' or ref[0,7] == '$.self.')
end

#normalize_formula(formula, dump = false) ⇒ Object

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



1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
1057
1058
1059
1060
1061
1062
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
1078
1079
1080
1081
1082
1083
1084
1085
1086
1087
1088
1089
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
1108
1109
1110
1111
1112
1113
1114
1115
1116
1117
1118
1119
1120
1121
1122
1123
1124
1125
1126
1127
1128
1129
1130
1131
1132
1133
1134
1135
1136
1137
1138
1139
1140
1141
1142
1143
1144
1145
1146
1147
1148
1149
1150
1151
1152
1153
1154
1155
1156
1157
1158
1159
1160
1161
1162
1163
1164
1165
1166
1167
1168
1169
1170
1171
1172
1173
1174
1175
1176
1177
1178
1179
1180
1181
1182
1183
1184
1185
1186
1187
1188
1189
1190
1191
1192
1193
1194
1195
1196
1197
1198
1199
1200
1201
1202
1203
1204
1205
1206
1207
1208
1209
1210
1211
1212
1213
1214
1215
1216
1217
1218
1219
1220
1221
1222
1223
1224
1225
1226
1227
1228
1229
1230
1231
1232
1233
1234
1235
1236
1237
1238
1239
1240
1241
1242
1243
1244
1245
1246
1247
1248
1249
1250
1251
1252
1253
1254
1255
1256
1257
1258
1259
1260
1261
1262
1263
1264
1265
1266
1267
1268
1269
1270
1271
1272
1273
1274
1275
1276
1277
1278
1279
1280
1281
1282
1283
1284
1285
1286
1287
1288
1289
1290
1291
1292
1293
1294
1295
1296
1297
1298
1299
1300
1301
1302
1303
1304
1305
1306
1307
1308
1309
1310
1311
1312
1313
1314
1315
1316
1317
1318
1319
1320
1321
1322
1323
1324
1325
1326
1327
1328
1329
1330
1331
1332
1333
1334
1335
1336
1337
1338
1339
1340
1341
1342
1343
1344
1345
1346
1347
1348
1349
1350
1351
1352
1353
1354
1355
1356
1357
1358
1359
1360
1361
1362
1363
1364
1365
1366
1367
1368
1369
1370
1371
1372
1373
1374
1375
1376
1377
1378
1379
1380
1381
1382
1383
1384
1385
1386
1387
1388
1389
1390
1391
1392
1393
1394
1395
1396
1397
1398
1399
1400
1401
1402
1403
1404
1405
1406
1407
1408
1409
1410
1411
1412
1413
1414
1415
1416
1417
1418
1419
1420
1421
1422
1423
1424
1425
1426
1427
1428
1429
1430
1431
1432
1433
1434
1435
1436
1437
1438
1439
1440
1441
1442
1443
1444
1445
1446
1447
1448
1449
1450
1451
1452
1453
1454
1455
1456
1457
1458
1459
1460
1461
1462
1463
1464
1465
1466
1467
1468
1469
1470
1471
1472
1473
1474
1475
1476
1477
1478
1479
1480
1481
1482
1483
1484
1485
1486
1487
1488
1489
1490
1491
1492
1493
1494
1495
1496
1497
1498
1499
1500
1501
1502
1503
1504
1505
1506
1507
1508
1509
1510
1511
 
# File 'lib/sfp/sas_translator.rb', line 1033

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) ⇒ Object 



1151
1152
1153
1154
1155
1156
1157
1158
1159
1160
1161
1162
 
# File 'lib/sfp/sas_translator.rb', line 1151

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) ⇒ Object

Raises:



1140
1141
1142
1143
1144
1145
1146
1147
1148
1149
 
# File 'lib/sfp/sas_translator.rb', line 1140

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) ⇒ Object 



1129
1130
1131
1132
1133
1134
1135
1136
1137
1138
 
# File 'lib/sfp/sas_translator.rb', line 1129

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) ⇒ Object 



1103
1104
1105
1106
1107
1108
1109
1110
1111
1112
1113
1114
1115
1116
1117
1118
1119
1120
 
# File 'lib/sfp/sas_translator.rb', line 1103

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) ⇒ Object

Raises:



1122
1123
1124
1125
1126
1127
 
# File 'lib/sfp/sas_translator.rb', line 1122

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) ⇒ Object

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



1293
1294
1295
1296
1297
1298
1299
1300
1301
1302
1303
1304
1305
1306
1307
1308
1309
1310
1311
1312
1313
1314
1315
 
# File 'lib/sfp/sas_translator.rb', line 1293

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) ⇒ Object

return true if postcondition supports premise



376
377
378
379
380
381
382
 
# File 'lib/sfp/sas_translator.rb', line 376

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) ⇒ Object 



384
385
386
387
388
389
390
 
# File 'lib/sfp/sas_translator.rb', line 384

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

Method for postprocessing simple global constraints



326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
 
# File 'lib/sfp/sas_translator.rb', line 326

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) ⇒ Object 



342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
 
# File 'lib/sfp/sas_translator.rb', line 342

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) ⇒ Object

return true if precondition supports premise



367
368
369
370
371
372
373
 
# File 'lib/sfp/sas_translator.rb', line 367

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) ⇒ Object 



392
393
394
395
396
397
398
 
# File 'lib/sfp/sas_translator.rb', line 392

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



449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
 
# File 'lib/sfp/sas_translator.rb', line 449

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) ⇒ Object

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



746
747
748
749
750
751
752
753
754
755
 
# File 'lib/sfp/sas_translator.rb', line 746

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) ⇒ Object

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



766
767
768
769
770
771
772
773
774
775
 
# File 'lib/sfp/sas_translator.rb', line 766

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



502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
 
# File 'lib/sfp/sas_translator.rb', line 502

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) ⇒ Object

Raises:



584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
 
# File 'lib/sfp/sas_translator.rb', line 584

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) ⇒ Object

process grounded operator (no parameter exists)



800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
 
# File 'lib/sfp/sas_translator.rb', line 800

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) ⇒ Object

process given operator



778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
 
# File 'lib/sfp/sas_translator.rb', line 778

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) ⇒ Object

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



839
840
841
842
843
844
845
846
847
848
 
# File 'lib/sfp/sas_translator.rb', line 839

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



546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
 
# File 'lib/sfp/sas_translator.rb', line 546

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



566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
 
# File 'lib/sfp/sas_translator.rb', line 566

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) ⇒ Object

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



1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
1078
1079
1080
1081
1082
1083
1084
1085
1086
1087
1088
1089
 
# File 'lib/sfp/sas_translator.rb', line 1064

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) ⇒ Object

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



1331
1332
1333
1334
1335
1336
1337
1338
1339
1340
1341
1342
1343
1344
1345
1346
1347
1348
1349
1350
1351
1352
1353
1354
1355
1356
1357
1358
1359
1360
1361
1362
1363
1364
1365
1366
1367
1368
1369
1370
1371
1372
1373
1374
1375
1376
1377
1378
1379
1380
1381
1382
1383
1384
1385
1386
1387
1388
1389
1390
1391
1392
1393
1394
1395
1396
1397
1398
1399
1400
1401
1402
1403
1404
1405
1406
1407
1408
1409
1410
1411
1412
1413
1414
1415
1416
1417
1418
1419
1420
1421
1422
1423
1424
1425
1426
1427
1428
1429
1430
1431
1432
 
# File 'lib/sfp/sas_translator.rb', line 1331

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



695
696
697
698
699
700
701
702
703
704
705
 
# File 'lib/sfp/sas_translator.rb', line 695

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



628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
 
# File 'lib/sfp/sas_translator.rb', line 628

def sas
  # version
  out = "begin_version\n3\nend_version\n"
  # metric
  out += "begin_metric\n1\nend_metric\n"
  # variables
  variable_index = @variables.keys
  variable_index.sort!
  out += "#{variable_index.length}\n"
  variable_index.each { |i|
    @variables[i].id = variable_index.index(i) # set variable's index
    out += @variables[i].to_sas(@root['initial']) + "\n"
  }
  # mutex
  out += "0\n"
  # initial state
  out += "begin_state\n"
  #pre = ( (pre.is_a?(Hash) and pre.isnull) ? 0 : (pre == nil ? -1 : @var.index(pre)) )
  variable_index.each { |i|
    if @variables[i].init.is_a?(Hash) and @variables[i].init.isnull
      out += "0\n"
    elsif @variables[i].init.is_a?(::Sfp::Unknown)
      out += "#{@variables[i].length-1}\n"
    else
      val = @variables[i].index(@variables[i].init).to_s
      out += "#{val}\n"
      if val.length <= 0
        raise TranslationException,
          "Unknown init: #{@variables[i].name} = #{@variables[i].init.inspect}"
      end
    end
  }
  out += "end_state\n"
  # goal
  out += "begin_goal\n"
  count = 0
  goal = ''
  variable_index.each { |i|
    if @variables[i].goal != nil
      goal += variable_index.index(i).to_s + ' ' +
        @variables[i].index(@variables[i].goal).to_s + "\n"
      count += 1
    end
  }
  out += "#{count}\n#{goal}end_goal\n"
  # operators
  #out += "#{@operators.length}\n"
  ops = ''
  total = 0
  @operators.each_value { |op|
    next if op.total_preposts <= 0
    # HACK! - an exception may arise if a value in condition or effect is not in variable's domain
    begin
      ops += op.to_sas(@root['initial'], @variables) + "\n"
      total += 1
    rescue Exception => exp
      #puts "#{exp}\n#{exp.backtrace.join("\n")}"
    end
  }
  out += "#{total}\n"
  out += ops
  # axioms
  out += "0"

  return out
end

#search_and_merge_mutually_inclusive_operators ⇒ Object 



239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
 
# File 'lib/sfp/sas_translator.rb', line 239

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

set possible values for each variable



939
940
941
942
943
944
945
946
947
948
 
# File 'lib/sfp/sas_translator.rb', line 939

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) ⇒ Object 



463
464
465
466
467
468
469
 
# File 'lib/sfp/sas_translator.rb', line 463

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) ⇒ Object 



1317
1318
1319
1320
1321
1322
1323
1324
1325
 
# File 'lib/sfp/sas_translator.rb', line 1317

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) ⇒ Object

transform a first-order formula into AND/OR graph



1165
1166
1167
1168
1169
1170
1171
1172
1173
1174
1175
1176
1177
1178
1179
1180
1181
1182
1183
1184
1185
1186
1187
1188
1189
1190
1191
1192
1193
1194
1195
1196
 
# File 'lib/sfp/sas_translator.rb', line 1165

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



59
60
61
62
63
 
# File 'lib/sfp/sas_translator.rb', line 59

def to_sas
  self.compile_step_1
  self.compile_step_2
  return self.sas
end

#total_element(formula, total = 0, total_or = 0, total_and = 0) ⇒ Object 



1444
1445
1446
1447
1448
1449
1450
1451
1452
1453
1454
1455
1456
 
# File 'lib/sfp/sas_translator.rb', line 1444

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) ⇒ Object 



224
225
226
227
228
229
230
231
232
233
234
235
236
237
 
# File 'lib/sfp/sas_translator.rb', line 224

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) ⇒ Object 



1458
1459
1460
1461
1462
1463
1464
1465
1466
1467
1468
1469
1470
1471
1472
1473
1474
1475
1476
1477
1478
1479
1480
1481
1482
1483
1484
1485
1486
1487
1488
1489
1490
1491
1492
1493
1494
1495
1496
1497
1498
1499
1500
1501
1502
1503
 
# File 'lib/sfp/sas_translator.rb', line 1458

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