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



798
799
800
801
802
 
# 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 ⇒ Object

return the next constraint’s id



780
781
782
783
784
 
# 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 ⇒ Object 



786
787
788
 
# File 'lib/sfp/sas_translator.rb', line 786

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

.next_operator_id ⇒ Object

return the next operator’s id



773
774
775
776
777
 
# 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 ⇒ Object

return the next variable’s id



791
792
793
794
795
 
# 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) ⇒ Object 



1602
1603
1604
1605
1606
 
# 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 ⇒ Object 



768
769
770
 
# File 'lib/sfp/sas_translator.rb', line 768

def self.reset_operator_id
	@@op_id = -1
end

Instance Method Details

#add_unknown_undefined_value_to_variables ⇒ Object 



1045
1046
1047
1048
1049
1050
1051
1052
 
# 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 ⇒ Object 



1038
1039
1040
1041
1042
1043
 
# 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) ⇒ Object 



818
819
820
821
822
823
 
# 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) ⇒ Object 



1054
1055
1056
1057
 
# 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) ⇒ Object

return true if global constraint could be applied, otherwise false



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



1144
1145
1146
1147
1148
 
# 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) ⇒ Object 



1179
1180
1181
1182
1183
1184
1185
1186
1187
1188
1189
 
# 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) ⇒ Object

testing/debugging methods



1523
1524
1525
1526
1527
1528
1529
1530
 
# 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) ⇒ Object

combinatorial method for all possible values of parameters using recursive method



966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
 
# 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 ⇒ 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
223
 
# 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 ⇒ 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 



457
458
459
460
461
462
463
464
465
466
 
# 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) ⇒ Object

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



1072
1073
1074
1075
1076
1077
1078
 
# 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) ⇒ Object

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



1065
1066
1067
1068
1069
 
# 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) ⇒ Object 



1136
1137
1138
 
# 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) ⇒ Object 



1124
1125
1126
 
# 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) ⇒ Object 



1132
1133
1134
 
# 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) ⇒ Object 



1128
1129
1130
 
# 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) ⇒ Object 



1140
1141
1142
 
# 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 ⇒ Object 



629
630
631
 
# 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) ⇒ Object

dot-product the nodes



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



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



1021
1022
1023
1024
 
# File 'lib/sfp/sas_translator.rb', line 1021

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

#dump_operators ⇒ Object 



1016
1017
1018
1019
 
# 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 ⇒ Object 



995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
 
# 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 ⇒ Object 



1011
1012
1013
1014
 
# 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) ⇒ Object 



350
351
352
353
354
355
356
357
358
 
# 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 ⇒ Object 



263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
 
# 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) ⇒ 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



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

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

Raises:



1367
1368
1369
1370
1371
1372
1373
1374
1375
1376
 
# 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) ⇒ Object

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



913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
 
# 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 ⇒ 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



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
322
323
324
325
326
 
# 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) ⇒ Object 



295
296
297
 
# 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) ⇒ Object

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



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
1512
1513
1514
1515
1516
1517
1518
1519
1520
1521
1522
1523
1524
1525
1526
1527
1528
1529
1530
1531
1532
1533
1534
1535
1536
1537
1538
1539
1540
1541
1542
1543
1544
1545
1546
1547
1548
1549
1550
1551
1552
1553
1554
1555
1556
1557
1558
1559
1560
1561
1562
1563
1564
1565
1566
1567
1568
1569
1570
1571
1572
1573
1574
1575
1576
1577
1578
1579
1580
1581
1582
1583
1584
1585
1586
1587
1588
1589
1590
1591
1592
1593
1594
1595
1596
1597
1598
1599
 
# 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) ⇒ Object 



1239
1240
1241
1242
1243
1244
1245
1246
1247
1248
1249
1250
 
# 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) ⇒ Object

Raises:



1228
1229
1230
1231
1232
1233
1234
1235
1236
1237
 
# 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) ⇒ Object 



1217
1218
1219
1220
1221
1222
1223
1224
1225
1226
 
# 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) ⇒ Object 



1191
1192
1193
1194
1195
1196
1197
1198
1199
1200
1201
1202
1203
1204
1205
1206
1207
1208
 
# 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) ⇒ Object

Raises:



1210
1211
1212
1213
1214
1215
 
# 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) ⇒ Object

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



1381
1382
1383
1384
1385
1386
1387
1388
1389
1390
1391
1392
1393
1394
1395
1396
1397
1398
1399
1400
1401
1402
1403
 
# 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) ⇒ Object

return true if postcondition supports premise



381
382
383
384
385
386
387
 
# 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) ⇒ Object 



389
390
391
392
393
394
395
 
# 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 ⇒ Object

Method for postprocessing simple global constraints



331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
 
# 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) ⇒ Object 



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
448
449
450
451
452
 
# 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) ⇒ Object

return true if precondition supports premise



372
373
374
375
376
377
378
 
# 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) ⇒ Object 



397
398
399
400
401
402
403
 
# 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 ⇒ Object 



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
499
500
501
502
503
 
# 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) ⇒ Object

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



807
808
809
810
811
812
813
814
815
816
 
# 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) ⇒ Object

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



827
828
829
830
831
832
833
834
835
836
 
# 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 ⇒ Object 



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
545
546
547
548
549
 
# 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) ⇒ Object

Raises:



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
623
624
625
626
627
 
# 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) ⇒ Object

process grounded operator (no parameter exists)



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

process given operator



839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
 
# 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) ⇒ Object

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



900
901
902
903
904
905
906
907
908
909
 
# 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 ⇒ Object 



551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
 
# 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 ⇒ Object 



571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
 
# 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) ⇒ Object

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



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



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
1512
1513
1514
1515
1516
1517
1518
1519
1520
 
# 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 ⇒ Object 



756
757
758
759
760
761
762
763
764
765
766
 
# 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 ⇒ Object 



690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
 
# 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 ⇒ Object 



244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
 
# 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 ⇒ Object

set possible values for each variable



1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
 
# 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) ⇒ Object 



468
469
470
471
472
473
474
 
# 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) ⇒ Object 



1405
1406
1407
1408
1409
1410
1411
1412
1413
 
# 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) ⇒ Object

transform a first-order formula into AND/OR graph



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

#to_set(array) ⇒ Object 



225
226
227
 
# 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) ⇒ Object 



1532
1533
1534
1535
1536
1537
1538
1539
1540
1541
1542
1543
1544
 
# 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) ⇒ Object 



229
230
231
232
233
234
235
236
237
238
239
240
241
242
 
# 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) ⇒ Object 



1546
1547
1548
1549
1550
1551
1552
1553
1554
1555
1556
1557
1558
1559
1560
1561
1562
1563
1564
1565
1566
1567
1568
1569
1570
1571
1572
1573
1574
1575
1576
1577
1578
1579
1580
1581
1582
1583
1584
1585
1586
1587
1588
1589
1590
1591
 
# 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