Class: PgVerify::Interpret::SpecSetContext

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

Instance Attribute Summary collapse

Instance Method Summary collapse

Constructor Details

#initialize(text, parent_graph, parent, children = []) ⇒ SpecSetContext

Returns a new instance of SpecSetContext.



20
21
22
23
24
 
# File 'lib/pg-verify/interpret/spec/spec_set_context.rb', line 20

def initialize(text, parent_graph, parent, children = [])
    @text, @parent, @children = text, parent, children
    @parent_graph = parent_graph
    @source_location = parent_graph.parent_script.find_source_location()
end

Instance Attribute Details

#assumption ⇒ Object

Returns the value of attribute assumption.



14
15
16
 
# File 'lib/pg-verify/interpret/spec/spec_set_context.rb', line 14

def assumption
  @assumption
end

#children ⇒ Object

The sub-spec sets contained in this spec set



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

def children
  @children
end

#parent ⇒ Object

Returns the value of attribute parent.



12
13
14
 
# File 'lib/pg-verify/interpret/spec/spec_set_context.rb', line 12

def parent
  @parent
end

#parent_graph ⇒ Object

Returns the value of attribute parent_graph.



16
17
18
 
# File 'lib/pg-verify/interpret/spec/spec_set_context.rb', line 16

def parent_graph
  @parent_graph
end

#source_location ⇒ Object

Returns the value of attribute source_location.



18
19
20
 
# File 'lib/pg-verify/interpret/spec/spec_set_context.rb', line 18

def source_location
  @source_location
end

#text ⇒ Object

The text of this spec set as a string.



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

def text
  @text
end

Instance Method Details

#assuming(hash, &blk) ⇒ Object 



32
33
34
35
36
37
38
39
 
# File 'lib/pg-verify/interpret/spec/spec_set_context.rb', line 32

def assuming(hash, &blk)
    assumption_text = hash.keys.first
    assumption_expression = hash.values.first
    subset = SpecSetContext.new("", @parent_graph, self)
    subset.assumption = { text: assumption_text, expression: assumption_expression }
    subset.instance_eval(&blk)
    children << subset
end

#it(hash) ⇒ Object 



47
48
49
50
51
52
 
# File 'lib/pg-verify/interpret/spec/spec_set_context.rb', line 47

def it(hash)
    # TODO: Handle errors
    text = hash.keys.first
    expression = hash[text]
    children << SpecContext.new(text, expression.to_s, self)
end

#ltl ⇒ Object 



54
55
56
 
# File 'lib/pg-verify/interpret/spec/spec_set_context.rb', line 54

def ltl()
    return LTLBuilder.new()
end

#no_errors ⇒ Object 



41
42
43
44
45
 
# File 'lib/pg-verify/interpret/spec/spec_set_context.rb', line 41

def no_errors()
    err_graphs = @parent_graph.components.select(&:represents_fault)
    expression = err_graphs.map { |g| "#{g.name} == No" }.join(" && ")
    return { "there are no errors" => "G ( #{expression} )" }
end

#specify(text, &blk) ⇒ Object 



26
27
28
29
30
 
# File 'lib/pg-verify/interpret/spec/spec_set_context.rb', line 26

def specify(text, &blk)
    subset = SpecSetContext.new(text, @parent_graph, self)
    subset.instance_eval(&blk)
    children << subset
end

#to_model(parent) ⇒ Object 



58
59
60
61
62
 
# File 'lib/pg-verify/interpret/spec/spec_set_context.rb', line 58

def to_model(parent)
    model = Model::SpecSet.new(@text, @assumption, parent, [])
    model.children = @children.map { |child| child.to_model(model) }
    return model
end