class ADSL::DS::DSDereference

Public Instance Methods

prepare_action(translation) click to toggle source
# File lib/adsl/spass/spass_ds_extensions.rb, line 695
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 699
def resolve_action_objset(translation, ps, var)
  translation.reserve_names :temp, :r do |temp, r|
    return FOL::Exists.new(temp, r, FOL::And.new(
      translation.prev_state[ps, r],
      translation.prev_state[ps, temp],
      @objset.resolve_action_objset(translation, ps, temp),
      @relation.left_link[r, temp],
      @relation.right_link[r, var]
    ))
  end
end
resolve_invariant_objset(translation, var) click to toggle source
# File lib/adsl/spass/spass_ds_extensions.rb, line 711
def resolve_invariant_objset(translation, var)
  translation.reserve_names :temp, :r do |temp, r|
    return FOL::Exists.new(temp, r, FOL::And.new(
      translation.invariant_state[temp],
      translation.invariant_state[r],
      @objset.resolve_invariant_objset(translation, temp),
      @relation.left_link[r, temp],
      @relation.right_link[r, var]
    ))
  end
end
type() click to toggle source
# File lib/adsl/ds/data_store_spec.rb, line 231
def type
  @relation.to_class
end