Class: Falluto::NuSMV::Fault

Inherits:
Object
  • Object
show all
Defined in:
lib/falluto/nusmv/fault.rb

Constant Summary collapse

GUARD_VARIABLE_FORMAT = 
'%s_g%d'

Instance Attribute Summary collapse

Instance Method Summary collapse

Constructor Details

#initialize(modul, name, precondition, restore, effect) ⇒ Fault

Returns a new instance of Fault.



18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
 
# File 'lib/falluto/nusmv/fault.rb', line 18

def initialize modul, name, precondition, restore, effect
  @name = name
  @process_name = "#{modul}_#{name}"
  @precondition = precondition
  @restore = restore
  @system_effect = effect

  @fairness_variable = "#{@name}_vfair"
  @precondition_variable = "#{@name}_pre"
  @restore_variable = "#{@name}_restore"
  @active_variable = "active"

  @auxiliar_variables = []

end

Instance Attribute Details

#active_variable ⇒ Object (readonly)

Returns the value of attribute active_variable.



15
16
17
 
# File 'lib/falluto/nusmv/fault.rb', line 15

def active_variable
  @active_variable
end

#fairness_variable ⇒ Object (readonly)

Returns the value of attribute fairness_variable.



15
16
17
 
# File 'lib/falluto/nusmv/fault.rb', line 15

def fairness_variable
  @fairness_variable
end

#name ⇒ Object (readonly)

Returns the value of attribute name.



13
14
15
 
# File 'lib/falluto/nusmv/fault.rb', line 13

def name
  @name
end

#precondition ⇒ Object (readonly)

Returns the value of attribute precondition.



14
15
16
 
# File 'lib/falluto/nusmv/fault.rb', line 14

def precondition
  @precondition
end

#precondition_variable ⇒ Object (readonly)

Returns the value of attribute precondition_variable.



15
16
17
 
# File 'lib/falluto/nusmv/fault.rb', line 15

def precondition_variable
  @precondition_variable
end

#process_name ⇒ Object (readonly)

Returns the value of attribute process_name.



13
14
15
 
# File 'lib/falluto/nusmv/fault.rb', line 13

def process_name
  @process_name
end

#restore ⇒ Object (readonly)

Returns the value of attribute restore.



14
15
16
 
# File 'lib/falluto/nusmv/fault.rb', line 14

def restore
  @restore
end

#restore_variable ⇒ Object (readonly)

Returns the value of attribute restore_variable.



15
16
17
 
# File 'lib/falluto/nusmv/fault.rb', line 15

def restore_variable
  @restore_variable
end

Instance Method Details

#add_auxiliar_variable(guard) ⇒ Object 



34
35
36
37
 
# File 'lib/falluto/nusmv/fault.rb', line 34

def add_auxiliar_variable guard
  vname = next_auxiliar_variable
  @auxiliar_variables << AuxiliarVariable.new(vname, guard)
end

#each_affected_variable(&block) ⇒ Object

Variables affected by system effect



49
50
51
 
# File 'lib/falluto/nusmv/fault.rb', line 49

def each_affected_variable &block
  @system_effect.variables.each{ |v| yield v }
end

#each_affected_variable_with_effect(&block) ⇒ Object 



53
54
55
 
# File 'lib/falluto/nusmv/fault.rb', line 53

def each_affected_variable_with_effect &block
  @system_effect.each_pair{ |v, effect| yield v, effect }
end

#each_auxiliar_variable(&block) ⇒ Object 



63
64
65
 
# File 'lib/falluto/nusmv/fault.rb', line 63

def each_auxiliar_variable &block
  @auxiliar_variables.each {|v| yield v}
end

#fairness_condition(inst = nil) ⇒ Object 



67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
 
# File 'lib/falluto/nusmv/fault.rb', line 67

def fairness_condition inst = nil
  if inst.nil?
    not_effect = "! #{@name}.#{active_variable}"
    #      not_effect = "! #{active_variable}"
  else
    not_effect = "! #{inst}.#{@name}.#{active_variable}"
  end

  if @auxiliar_variables.empty?
    not_effect
  else
    vars = @auxiliar_variables.collect do |v|
      (inst.nil? ? '' : "#{inst}.") + v.name
    end
    '( ' + vars.join(' | ') + " ) & #{not_effect}"
  end
end

#instance_signature ⇒ Object 



57
58
59
60
61
 
# File 'lib/falluto/nusmv/fault.rb', line 57

def instance_signature
  parameters = "#{precondition_variable}, #{restore_variable}"
  each_affected_variable{|v| parameters << ", #{v}"}
  %Q|#{process_name}(#{parameters})|
end

#next_auxiliar_variable ⇒ Object 



39
40
41
42
 
# File 'lib/falluto/nusmv/fault.rb', line 39

def next_auxiliar_variable
  i = @auxiliar_variables.length + 1
  GUARD_VARIABLE_FORMAT % [@name, i]
end

#strong_fairness(inst) ⇒ Object 



44
45
46
 
# File 'lib/falluto/nusmv/fault.rb', line 44

def strong_fairness inst
  "((G F (#{fairness_condition(inst)})) -> (G F (#{inst}.#{fairness_variable})))"
end