class ADSL::DS::DSForAll
Public Instance Methods
resolve_invariant_formula(translation)
click to toggle source
# File lib/adsl/spass/spass_ds_extensions.rb, line 865 def resolve_invariant_formula(translation) subformula = @subformula.resolve_invariant_formula translation var_constraints = [] @vars.length.times do |index| var_constraints << @objsets[index].resolve_invariant_objset(translation, @vars[index].invariant_name) end return FOL::ForAll.new(@vars.map{ |v| v.invariant_name }, FOL::Implies.new( FOL::And.new( @vars.map{ |v| translation.invariant_state[v.invariant_name] }, var_constraints ), subformula )).resolve_spass end
type()
click to toggle source
# File lib/adsl/ds/data_store_spec.rb, line 262 def type :formula end