Class: Gisele::Analysis::Glts::Invariants

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

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(glts) ⇒ Invariants

Returns a new instance of Invariants.



6
7
8
 
# File 'lib/gisele/analysis/glts/invariants.rb', line 6

def initialize(glts)
  @glts = glts
end

Instance Attribute Details

#glts ⇒ Object (readonly)

Returns the value of attribute glts.



9
10
11
 
# File 'lib/gisele/analysis/glts/invariants.rb', line 9

def glts
  @glts
end

Instance Method Details

#init_deco(s) ⇒ Object 



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

def init_deco(s)
  s.initial? ? glts.c0 : zero
end

#propagate(deco, edge) ⇒ Object 



19
20
21
22
23
24
25
26
27
28
 
# File 'lib/gisele/analysis/glts/invariants.rb', line 19

def propagate(deco, edge)
  event = edge[:event]
  deco  = (deco & edge[:guard]).ref
  session.variables.each do |var|
    old_deco, deco = deco, var.apply_on_invariant(deco, event)
    deco.ref
    old_deco.deref
  end
  deco
end

#session ⇒ Object 



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

def session
  glts.session
end

#suppremum(d0, d1) ⇒ Object 



15
16
17
 
# File 'lib/gisele/analysis/glts/invariants.rb', line 15

def suppremum(d0, d1)
  (d0 | d1).ref
end

#take_at_start?(s) ⇒ Boolean

Returns:

  • (Boolean) 


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

def take_at_start?(s)
  s.initial?
end