Class: Gisele::Analysis::Glts::Eclosure

Inherits:
Stamina::Utils::Decorate
  • Object
show all
Includes:
Mixin::BddManagement
Defined in:
lib/gisele/analysis/glts/eclosure.rb

Constant Summary collapse

EMPTY = 
{}.freeze

Instance Attribute Summary collapse

Instance Method Summary collapse

Methods included from Mixin::BddManagement

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

Constructor Details

#initialize(session) ⇒ Eclosure

Returns a new instance of Eclosure.



8
9
10
 
# File 'lib/gisele/analysis/glts/eclosure.rb', line 8

def initialize(session)
  @session = session
end

Instance Attribute Details

#session ⇒ Object (readonly)

Returns the value of attribute session.



11
12
13
 
# File 'lib/gisele/analysis/glts/eclosure.rb', line 11

def session
  @session
end

Instance Method Details

#backward? ⇒ Boolean

Returns:

  • (Boolean) 


34
35
36
 
# File 'lib/gisele/analysis/glts/eclosure.rb', line 34

def backward?
  true
end

#init_deco(s) ⇒ Object 



26
27
28
 
# File 'lib/gisele/analysis/glts/eclosure.rb', line 26

def init_deco(s)
  {s => one}
end

#propagate(deco, edge) ⇒ Object 



17
18
19
20
21
22
23
24
 
# File 'lib/gisele/analysis/glts/eclosure.rb', line 17

def propagate(deco, edge)
  return EMPTY if edge[:event]
  propagated = {}
  deco.each_pair do |k,v|
    propagated[k] = (v & edge[:guard])
  end
  propagated
end

#suppremum(d0, d1) ⇒ Object 



13
14
15
 
# File 'lib/gisele/analysis/glts/eclosure.rb', line 13

def suppremum(d0, d1)
  d0.merge(d1){|k,l,r| (l | r)}
end

#take_at_start?(s) ⇒ Boolean

Returns:

  • (Boolean) 


30
31
32
 
# File 'lib/gisele/analysis/glts/eclosure.rb', line 30

def take_at_start?(s)
  s.in_edges.any?{|e| e[:event].nil? }
end