class ADSL::DS::DSSpec

Public Instance Methods

translate_action(action_name, *listed_invariants) click to toggle source
# File lib/adsl/spass/spass_ds_extensions.rb, line 11
def translate_action(action_name, *listed_invariants)
  translation = ADSL::Spass::SpassTranslator::Translation.new

  if action_name
    action = @actions.select{ |a| a.name == action_name }
    raise ArgumentError, "Action '#{action_name}' not found" if action.empty?
    action = action.first
  end

  translation.classes.concat @classes
  @classes.each do |klass|
    klass.translate(translation)
  end

  relations = @classes.map{ |c| c.relations }.flatten
  relations.select{ |r| r.inverse_of.nil? }.each do |relation|
    relation.translate(translation)
  end
  relations.select{ |r| r.inverse_of }.each do |relation|
    relation.translate(translation)
  end

  action.prepare(translation) if action_name

  translation.create_formula FOL::ForAll.new(:o, FOL::Equiv.new(
    translation.is_object[:o],
    FOL::Or.new(@classes.map{ |c| c[:o] })
  ))
  @classes.group_by{ |klass| klass.parent }.each do |common_parent, children|
    unless common_parent.nil?
      translation.create_formula FOL::ForAll.new(:o, FOL::Implies.new(
        FOL::Or.new(children.map{ |c| c[:o] }),
        common_parent[:o]
      ))
    end
    if children.length > 1
      children.each do |child|
        translation.create_formula FOL::ForAll.new(:o, FOL::Implies.new(
          child[:o],
          FOL::Not.new(children.select{ |c| c != child}.map{ |c| c[:o] })
        ))
      end
    end
  end

  relations = @classes.map{ |c| c.relations }.flatten.map{ |rel| rel.type_pred }.uniq
  translation.create_formula FOL::ForAll.new(:o, FOL::Equiv.new(
    translation.is_tuple[:o],
    FOL::Or.new(relations.map{ |r| r[:o] })
  ))
  if relations.length > 1
    relations.each do |relation|
      translation.create_formula FOL::ForAll.new(:o, FOL::Implies.new(
        relation[:o],
        FOL::Not.new(relations.select{ |c| c != relation}.map{ |c| c[:o] })
      ))
    end
  end

  translation.create_formula FOL::ForAll.new(:o, FOL::OneOf.new(
    translation.is_object[:o],
    translation.is_tuple[:o],
    translation.is_either_resolution[:o]
  ))
  translation.create_formula FOL::ForAll.new(:o, FOL::Implies.new(
    translation.existed_initially[:o],
    FOL::Or.new(translation.is_object[:o], translation.is_tuple[:o])
  ))
  translation.create_formula FOL::ForAll.new(:o, FOL::Equiv.new(
    translation.existed_initially[:o], 
    translation.prev_state[:o]
  ))

  action.translate(translation) if action_name

  if action_name
    translation.invariant_state = translation.existed_initially
    pre_invariants = @invariants.map{ |invariant| invariant.formula.resolve_invariant_formula(translation) }
  
    listed_invariants = @invariants if listed_invariants.empty?
    translation.invariant_state = translation.exists_finally
    post_invariants = listed_invariants.map{ |invariant| invariant.formula.resolve_invariant_formula(translation) }
    
    translation.create_conjecture FOL::Implies.new(
      FOL::And.new(pre_invariants),
      FOL::And.new(post_invariants)
    ).resolve_spass
  else
    # used to check for contradictions in the model
    invariants_formulae = invariants.map do |invariant|
      formula = invariant.formula
      dummy_state = translation.create_predicate 'always_true', 1
      translation.create_formula FOL::ForAll.new(:o, dummy_state[:o])
      translation.invariant_state = dummy_state
      formula.resolve_invariant_formula(translation)
    end
    translation.create_conjecture FOL::Not.new(FOL::And.new(invariants_formulae))
  end

  return translation.to_spass_string
end