Class: PgVerify::Interpret::GraphContext

Inherits:
Object
  • Object
show all
Defined in:
lib/pg-verify/interpret/graph_context.rb

Instance Attribute Summary collapse

Instance Method Summary collapse

Constructor Details

#initialize(name, parent_script) ⇒ GraphContext

Returns a new instance of GraphContext.



15
16
17
18
19
# File 'lib/pg-verify/interpret/graph_context.rb', line 15

def initialize(name, parent_script)
    @parent_script = parent_script
    @name = name
    @components, @specs, @hazards = [], [], []
end

Instance Attribute Details

#componentsObject

The list of currently declared components



9
10
11
# File 'lib/pg-verify/interpret/graph_context.rb', line 9

def components
  @components
end

#hazardsObject

Returns the value of attribute hazards.



11
12
13
# File 'lib/pg-verify/interpret/graph_context.rb', line 11

def hazards
  @hazards
end

#nameObject

The name of this graph



13
14
15
# File 'lib/pg-verify/interpret/graph_context.rb', line 13

def name
  @name
end

#parent_scriptObject

Returns the value of attribute parent_script.



7
8
9
# File 'lib/pg-verify/interpret/graph_context.rb', line 7

def parent_script
  @parent_script
end

#specsObject

Returns the value of attribute specs.



10
11
12
# File 'lib/pg-verify/interpret/graph_context.rb', line 10

def specs
  @specs
end

Instance Method Details

#disable_error(name) ⇒ Object



50
51
52
53
54
55
56
# File 'lib/pg-verify/interpret/graph_context.rb', line 50

def disable_error(name)
    cmp = @components.find { |c| c.name == name.to_sym }
    raise "No such component: #{name}" if cmp.nil?
    raise "Not an error component: #{name}" unless cmp.represents_fault
    cmp.transition_list = [ ]
    cmp.init_expressions = [ "#{name} == No" ]
end

#error(name) ⇒ Object



58
59
60
# File 'lib/pg-verify/interpret/graph_context.rb', line 58

def error(name)
    return name
end

#graph(name, &blk) ⇒ Object

DSL method for declaring a new component in this graph

Raises:



22
23
24
25
26
27
28
# File 'lib/pg-verify/interpret/graph_context.rb', line 22

def graph(name, &blk)
    raise InvalidDSL_graph.new("Name '#{name}' is neither a symbol nor string") unless name.is_a?(Symbol) || name.is_a?(String)
    cmp = ComponentContext.new(name, self)
    cmp.instance_eval(&blk)
    @components << cmp
    return cmp
end

#hazard(hash) ⇒ Object



69
70
71
72
73
# File 'lib/pg-verify/interpret/graph_context.rb', line 69

def hazard(hash)
    text = hash.keys.first
    expression = hash[text]
    @hazards << Model::Hazard.new(text, expression)
end

#persistent(name) ⇒ Object



40
41
42
43
44
45
46
47
48
# File 'lib/pg-verify/interpret/graph_context.rb', line 40

def persistent(name)
    cmp = graph(name) do
        states(:No, :Yes)
        transition :No => :No
        transition :No => :Yes
    end
    cmp.represents_fault = true
    return cmp
end

#specify(text, &blk) ⇒ Object

DSL method for declaring a new specification in this graph



63
64
65
66
67
# File 'lib/pg-verify/interpret/graph_context.rb', line 63

def specify(text, &blk)
    specset = SpecSetContext.new(text, self, nil)
    specset.instance_eval(&blk)
    @specs << specset
end

#to_modelObject



75
76
77
78
79
80
# File 'lib/pg-verify/interpret/graph_context.rb', line 75

def to_model()
    components = @components.map(&:to_model)
    variables = Model::VariableSet.new(*@components.map(&:owned_variables).flatten())
    specification = Model::Specification.new(@specs.map { |s| s.to_model(nil) })
    Model::Graph.new(@name, components: components, variables: variables, specification: specification, hazards: @hazards)
end

#transient(name) ⇒ Object



30
31
32
33
34
35
36
37
38
# File 'lib/pg-verify/interpret/graph_context.rb', line 30

def transient(name)
    cmp = graph(name) do
        all_states = [ :No, :Yes ]
        states(*all_states)
        all_states.product(all_states).each { |s1, s2| transition({ s1 => s2}) }
    end
    cmp.represents_fault = true
    return cmp
end