class ADSL::DS::DSOneOf
Public Instance Methods
prepare_action(translation)
click to toggle source
# File lib/adsl/spass/spass_ds_extensions.rb, line 829 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 833 def resolve_action_objset(translation, ps, var) context = translation.context pred = translation.create_predicate :one_of, context.level + 1 translation.gen_formula_for_unique_arg(pred, context.level) translation.reserve_names context.p_names, :o do |subps, o| co_in_objset = @objset.resolve_action_objset(translation, subps, o) translation.create_formula FOL::ForAll.new(subps, FOL::Equiv.new( FOL::Exists.new(o, FOL::And.new(translation.prev_state[subps, o], pred[subps, o])), FOL::Exists.new(o, FOL::And.new(translation.prev_state[subps, o], co_in_objset)) )) translation.create_formula FOL::ForAll.new(subps, o, FOL::Implies.new(pred[subps, o], FOL::And.new(translation.prev_state[subps, o], co_in_objset)) ) end return pred[ps, var] end
type()
click to toggle source
# File lib/adsl/ds/data_store_spec.rb, line 223 def type @objset.type end