Class: Gisele::Analysis::Glts::Minimize

Inherits:
Object
  • Object
show all
Includes:
Mixin::BddManagement
Defined in:
lib/gisele/analysis/glts/minimize.rb

Constant Summary collapse

STATE_AGGREGATOR = 
Stamina::Utils::Aggregator.new{|g|
  g.ignore(:eclosure)
  g.ignore(:origin)
  g.register(:initial, &:|)
  g.register(:accepting, &:&)
  g.register(:error, &:|)
  g.register(:invariant){|v1,v2|
    (v1 | v2).ref
  }
  g.default{|v1,v2|
    raise "Unexpected state marks: #{v1} vs. #{v2}" unless v1==v2
    v1
  }
}

Instance Attribute Summary collapse

Instance Method Summary collapse

Methods included from Mixin::BddManagement

#bdd, #bdd_interface, #cudd_manager, #one, #with_bdd, #zero

Instance Attribute Details

#glts ⇒ Object (readonly)

Returns the value of attribute glts.



23
24
25
 
# File 'lib/gisele/analysis/glts/minimize.rb', line 23

def glts
  @glts
end

Instance Method Details

#call(glts) ⇒ Object 



29
30
31
32
33
34
35
 
# File 'lib/gisele/analysis/glts/minimize.rb', line 29

def call(glts)
  @glts = glts
  while pair = find_compatible_pair
    merge!(*pair)
  end
  glts
end

#session ⇒ Object 



25
26
27
 
# File 'lib/gisele/analysis/glts/minimize.rb', line 25

def session
  glts.session
end