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