Class: PgVerify::Simulation::Simulator

Inherits:
Object
  • Object
show all
Defined in:
lib/pg-verify/simulation/simulator.rb

Instance Attribute Summary collapse

Instance Method Summary collapse

Constructor Details

#initialize(graph) ⇒ Simulator

Returns a new instance of Simulator.



8
9
10
 
# File 'lib/pg-verify/simulation/simulator.rb', line 8

def initialize(graph)
    @graph = graph
end

Instance Attribute Details

#graph ⇒ Object

Returns the value of attribute graph.



6
7
8
 
# File 'lib/pg-verify/simulation/simulator.rb', line 6

def graph
  @graph
end

Instance Method Details

#eval_expression(expression, state) ⇒ Object 



72
73
74
75
76
77
78
79
80
81
82
83
84
85
 
# File 'lib/pg-verify/simulation/simulator.rb', line 72

def eval_expression(expression, state)
    state.names.sort_by(&:length).reverse.each { |var|
        value = state[var]
        expression = expression.gsub(var.to_s, value.to_s)
    }
    
    expression = Model::ParsedExpression.new(expression, nil)
    words = expression.word_tokens.uniq
    expression = expression.to_s
    words.each { |word|
        expression = expression.gsub(word.to_s, "'#{word}'")
    }
    return eval(expression)
end

#find_next_transitions(state) ⇒ Object

Returns a map from ‘component’ to ‘transition’ which should be used for that component based in the state. If there is no matching transition for a component, that component is omitted as to use the “tau-transition”.



26
27
28
29
30
31
32
33
34
35
36
37
38
 
# File 'lib/pg-verify/simulation/simulator.rb', line 26

def find_next_transitions(state)
     return @graph.components.map { |cmp|
        matching_transitions = cmp.transitions.select { |trans|
            transition_accepted?(trans, cmp, state)
        }
        # Do not change the state if no transitions match
        next if matching_transitions.empty?

        # TODO: Choose random one using seed
        chosen_transition = matching_transitions.shuffle().first
        [cmp, chosen_transition]
    }.compact.to_h
end

#run(steps: 10, state: State.for_variable_set(@graph.all_variables)) ⇒ Object 



12
13
14
15
16
17
18
19
20
 
# File 'lib/pg-verify/simulation/simulator.rb', line 12

def run(steps: 10, state: State.for_variable_set(@graph.all_variables))
    state_stack = [ state ]
    steps.times {
        component_transitions = find_next_transitions(state)
        state = run_transitions(component_transitions, state)
        state_stack << state
    }
    return state_stack
end

#run_transitions(component_transitions, state) ⇒ Object

Performs the specified transitions on the specified state and returns a new updated state.



42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
 
# File 'lib/pg-verify/simulation/simulator.rb', line 42

def run_transitions(component_transitions, state)
    new_state = state.clone()
    component_transitions.each { |component, transition|
        # Update the component state
        new_state[component.name] = transition.tgt_state

        # Perform the action
        next if transition.action.nil?
        parts = transition.action.to_s.split(":=")
        assigned_variable = parts[0].strip
        expression = parts[1].strip

        new_state[assigned_variable.to_sym] = eval_expression(expression, state)
    }
    return new_state
end

#transition_accepted?(transition, component, state) ⇒ Boolean

Returns:

  • (Boolean) 


59
60
61
62
63
64
65
66
67
68
69
70
 
# File 'lib/pg-verify/simulation/simulator.rb', line 59

def transition_accepted?(transition, component, state)
    # Transition can't be used unless the component is in the required
    # source state.
    return false unless transition.src_state == state[component.name]
    
    guard_expression = [ transition.guard, transition.precon ]
        .map(&:to_s).reject(&:empty?).join(" && ")

    return false if eval_expression(guard_expression, state) == false

    return true
end