Class: Gisele::Analysis::Glts

Inherits:
Stamina::Automaton
  • Object
show all
Includes:
Mixin::BddManagement
Defined in:
lib/gisele/analysis/glts.rb,
lib/gisele/analysis/glts/merge.rb,
lib/gisele/analysis/glts/union.rb,
lib/gisele/analysis/glts/guards.rb,
lib/gisele/analysis/glts/eclosure.rb,
lib/gisele/analysis/glts/minimize.rb,
lib/gisele/analysis/glts/separate.rb,
lib/gisele/analysis/glts/invariants.rb,
lib/gisele/analysis/glts/determinize.rb,
lib/gisele/analysis/glts/equivalence.rb

Defined Under Namespace

Classes: Determinize, Eclosure, Invariants, Merge, Minimize, WeakEquivalence

Constant Summary collapse

TO_DNF_OPERATORS =

OUTPUT ###########################################################################

{:not => 'not', :or => 'or', :and => 'and'}

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) ⇒ Glts

Returns a new instance of Glts.



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

def initialize(session)
  @session = session
  super(false)
end

Instance Attribute Details

#session ⇒ Object (readonly)

Returns the value of attribute session.



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

def session
  @session
end

Instance Method Details

#add_state(data = {}) ⇒ Object 



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

def add_state(data = {})
  data[:accepting] = true
  super
end

#c0 ⇒ Object 



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

def c0
  with_bdd session.c0_from_variables do |s_c0|
    (@c0 || one) & s_c0
  end
end

#c0=(c0) ⇒ Object 



18
19
20
 
# File 'lib/gisele/analysis/glts.rb', line 18

def c0=(c0)
  @c0 = session.bdd(c0)
end

#connect(from, to, data) ⇒ Object 



27
28
29
30
31
 
# File 'lib/gisele/analysis/glts.rb', line 27

def connect(from, to, data)
  data[:symbol] ||= data[:event] || nil
  data[:guard]    = session.bdd(data[:guard] || true).ref
  super(from, to, data)
end

#determinize ⇒ Object

Returns a deterministic version of this glts.



86
87
88
 
# File 'lib/gisele/analysis/glts/determinize.rb', line 86

def determinize
  Determinize.new(self.dup.explicit_guards!).target.simplify_guards!
end

#dup(glts = nil) ⇒ Object 



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

def dup(glts = nil)
  glts ||= Glts.new(session){|g| g.c0 = self.c0}
  super(glts)
end

#eclosure! ⇒ Object

Ensure that epsilon-closure info is present as a state decoration.



41
42
43
 
# File 'lib/gisele/analysis/glts/eclosure.rb', line 41

def eclosure!
  Eclosure.new(session).call(self, :eclosure)
end

#explicit_guards! ⇒ Object 



4
5
6
7
8
9
10
 
# File 'lib/gisele/analysis/glts/guards.rb', line 4

def explicit_guards!
  unless @guards_mode == :explicit
    apply_on_guards!{|g, inv| g & inv }
    @guards_mode = :explicit
  end
  self
end

#invariants! ⇒ Object

class Invariants



40
41
42
43
44
45
46
 
# File 'lib/gisele/analysis/glts/invariants.rb', line 40

def invariants!
  unless @invariants_generated
    Invariants.new(self).call(self, :invariant)
    @invariants_generated = true
  end
  self
end

#merge(other) ⇒ Object Also known as: |

class Merge



122
123
124
125
 
# File 'lib/gisele/analysis/glts/merge.rb', line 122

def merge(other)
  union = (self + other).determinize
  Merge.new.call(union.explicit_guards!).simplify_guards!
end

#minimize ⇒ Object

class Minimize



90
91
92
 
# File 'lib/gisele/analysis/glts/minimize.rb', line 90

def minimize
  dup.minimize!
end

#minimize! ⇒ Object 



94
95
96
 
# File 'lib/gisele/analysis/glts/minimize.rb', line 94

def minimize!
  Minimize.new.call(simplify_guards!)
end

#separate ⇒ Object 



4
5
6
 
# File 'lib/gisele/analysis/glts/separate.rb', line 4

def separate
  dup.separate!
end

#separate! ⇒ Object 



8
9
10
11
12
13
14
15
16
17
 
# File 'lib/gisele/analysis/glts/separate.rb', line 8

def separate!
  edges.dup.each do |e|
    next if e[:guard] == one
    middle = add_state(:initial => false)
    connect(e.source, middle, e.data.merge(:event => nil))
    connect(middle, e.target, :event => e[:event])
    drop_edge(e)
  end
  self
end

#simplify_guards! ⇒ Object 



12
13
14
15
16
17
18
 
# File 'lib/gisele/analysis/glts/guards.rb', line 12

def simplify_guards!
  unless @guards_mode == :simplified
    apply_on_guards!{|g, inv| g.restrict(inv) }
    @guards_mode = :simplified
  end
  self
end

#to_dot ⇒ Object 



42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
 
# File 'lib/gisele/analysis/glts.rb', line 42

def to_dot
  super(false) do |elm, kind|
    case kind
      when :automaton
        {:rankdir => "LR",
         :margin  => "0",
         :pack    => "true",
         :ranksep => "0"}
      when :state
        {:shape     => "circle",
         :style     => "filled",
         :color     => "black",
         :fillcolor => (elm.initial? ? "green" : "white"),
         :fixedsize => "true",
         :height    => "0.6",
         :width     => "0.6"}
      when :edge
        {:label     => edge_label(elm),
         :arrowsize => "0.7"}
    end
  end
end

#to_ruby_literal ⇒ Object 



65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
 
# File 'lib/gisele/analysis/glts.rb', line 65

def to_ruby_literal
  buf = ""
  buf << "Glts.new(session) do |g|\n"
  buf << "  g.add_state :initial => true\n"
  buf << "  g.add_n_states #{state_count - 1}\n"
  each_edge do |e|
    s, t = e.source.index, e.target.index
    event, guard = e[:event], e[:guard]
    event = event.inspect if event
    buf << "  g.connect #{e.source.index}, #{e.target.index}"
    buf << ", :guard => #{guard.to_dnf(TO_DNF_OPERATORS).inspect}"
    buf << ", :event => #{event}" if event
    buf << "\n"
  end
  buf << "end\n"
  buf
end

#union(other) ⇒ Object Also known as: + 



4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
 
# File 'lib/gisele/analysis/glts/union.rb', line 4

def union(other)
  Glts.new(session) do |g|
    init_state = g.add_state(:initial => true)
    add_glts = lambda do |from, to, origin|
      from.dup(to) do |s, t|
        if s.initial?
          t.initial!(false)
          to.connect(init_state, t, :guard => from.c0)
        end
        t[:origin] = origin
      end
    end
    add_glts[self,  g, :wf1]
    add_glts[other, g, :wf2]
  end
end

#weakly_equivalent?(other, &explain) ⇒ Boolean

class WeakEquivalence

Returns:

  • (Boolean) 


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

def weakly_equivalent?(other, &explain)
  WeakEquivalence.new.call(self, other, &explain)
end