class ADSL::DS::DSSubset
Public Instance Methods
prepare_action(translation)
click to toggle source
# File lib/adsl/spass/spass_ds_extensions.rb, line 725 def prepare_action(translation) @objset.prepare_action translation end
resolve_action_objset(translation, ps, var)
click to toggle source
# File lib/adsl/spass/spass_ds_extensions.rb, line 729 def resolve_action_objset(translation, ps, var) context = translation.context pred = translation.create_predicate :subset, context.level + 1 translation.reserve_names context.p_names do |ps| translation.create_formula FOL::ForAll.new(ps, :o, FOL::Implies.new(pred[ps, :o], @objset.resolve_action_objset(translation, ps, :o)) ) end return pred[ps, var] end
resolve_invariant_objset(translation, var)
click to toggle source
# File lib/adsl/spass/spass_ds_extensions.rb, line 740 def resolve_invariant_objset(translation, var) pred = translation.create_predicate :subset, 1 translation.create_formula FOL::ForAll.new(:o, FOL::Implies.new(pred[:o], @objset.resolve_invariant_objset(translation, :o)) ) return pred[var] end
type()
click to toggle source
# File lib/adsl/ds/data_store_spec.rb, line 200 def type @objset.type end