Class: PgVerify::Transform::NuSmvTransformation

Inherits:
Object
  • Object
show all
Defined in:
lib/pg-verify/transform/nusmv_transformation.rb

Instance Method Summary collapse

Instance Method Details

#module_string(name, hash = {}) ⇒ Object 



221
222
223
224
225
226
227
228
 
# File 'lib/pg-verify/transform/nusmv_transformation.rb', line 221

def module_string(name, hash = {})
    blocks = [ "MODULE #{name}" ]
    hash.each { |key, val|
        blocks << key.to_s.upcase.indented
        blocks << val.indented(num: 2)
    }
    return blocks.join("\n")
end

#transform_assignment(assignment_expression, component, varset) ⇒ Object 



134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
 
# File 'lib/pg-verify/transform/nusmv_transformation.rb', line 134

def transform_assignment(assignment_expression, component, varset)
    return nil if assignment_expression.nil?

    # Handle composite actions (a := 1 | b := 2) by recursively transforming
    # the individual actions and then combining them
    sub_assignments = assignment_expression.to_s.split("|")
    if sub_assignments.length > 1
        action_s_acc, assigned_vars_acc = [], []
        sub_assignments = sub_assignments.map { |a|
            action_s, assigned_vars = transform_assignment(a, component, varset)
            action_s_acc << action_s
            assigned_vars_acc += assigned_vars
        }
        return action_s_acc.join(" & "), assigned_vars_acc.uniq
    end


    parts = assignment_expression.to_s.split(":=")

    assigned_variable = parts[0].strip

    unless varset.varname?(assigned_variable)
        raise Model::Validation::UnknownVariableError.new(assigned_variable, assignment_expression, varset)
    end
    unless varset[assigned_variable].owner_name == component.name
        raise Model::Validation::ForeignVariableAssignmentError.new(assigned_variable, assignment_expression, varset, component)
    end
    if varset[assigned_variable].state_variable?
        raise Model::Validation::AssignmentToStateVariableError.new(assigned_variable, assignment_expression, varset)
    end

    assigned_variable_s = "next(v.#{transform_varname(assigned_variable)})"

    expression = parts[1].strip
    expression = transform_expression(Model::ParsedExpression.new(expression, Model::ParsedExpression::TYPE_TERM), varset)

    assignment_s = "#{assigned_variable_s} = #{expression}"

    return assignment_s, [assigned_variable]
end

#transform_component(component, varset) ⇒ Object 



41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
 
# File 'lib/pg-verify/transform/nusmv_transformation.rb', line 41

def transform_component(component, varset)
    # Name of the component module
    name = transform_module_name(component.name)
    # The component takes all variables v
    name += "(v)"

    # Grab all variables which this component defines and thus owns
    owned_vars = varset.select_by_owner(component.name).to_a

    # Create the INIT block expression which must hold initially
    # This is used to initialize variables and decide on the initial
    # state of this component. This can all be randomized by setting
    # the init state to true
    init_expression = transform_init_expression(component, varset, owned_vars)

    # Transform all transitions which are defined in this component
    trans = component.transitions.map { |transition|
        trans_s = transform_transition(varset, component, transition)
        "( #{trans_s} )"
    }

    # Create a default transition which is taken whenever no other
    # transitions can.
    tau_transition = []
    # Combine the precondition, guard and source state conditions
    # For each transition of this component
    other_transitions = component.transitions.map { |transition| 
        precon_s = transform_expression(transition.precon, varset)
        guard_s  = transform_expression(transition.guard, varset)

        cmp_varname = transform_varname(component.name)
        this_state = transform_const(transition.src_state)
        state_s = "v.#{cmp_varname} = #{this_state}"

        [ state_s, precon_s, guard_s ].compact.reject(&:empty?).map{ |s| "( #{s} )" }.join(' & ')
    }.compact.reject(&:empty?)
    # Only take the tau transition when all other transitions do not match 
    tau_transition << "!(\n\t#{other_transitions.join(" | \n\t")})\n\t" unless other_transitions.empty?

    # Keep this components state when using the default transition
    # Keep all owned variables equal when using the default transition
    tau_transition += owned_vars.map { |var|
        varname = "v.#{transform_varname(var.name)}"
        "next(#{varname}) = #{varname}"
    }
    # Add the tau transition
    trans << "(#{tau_transition.join(" & ")})"

    trans = trans.join(" | \n") + ";"

    return module_string(name, init: init_expression, trans: trans)
end

#transform_components(components, varset) ⇒ Object 



24
25
26
 
# File 'lib/pg-verify/transform/nusmv_transformation.rb', line 24

def transform_components(components, varset)
    return components.map { |c| transform_component(c, varset) }.join("\n\n")
end

#transform_const(value) ⇒ Object 



234
235
236
237
 
# File 'lib/pg-verify/transform/nusmv_transformation.rb', line 234

def transform_const(value)
    return value.to_s unless value.is_a?(Symbol) || value.is_a?(String)
    "L_#{value}"
end

#transform_expression(expression, varset) ⇒ Object 



175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
 
# File 'lib/pg-verify/transform/nusmv_transformation.rb', line 175

def transform_expression(expression, varset)
    return nil if expression.nil?

    variables, constants = [], []
    expression.word_tokens.select { |w| 
        if varset.names.include?(w)
            variables << w
        elsif  varset.values.include?(w)
            constants << w
        else
            raise Model::Validation::UnknownTokenError.new(w, expression, varset)
        end
    }
    variables, constants = variables.uniq, constants.uniq

    constants = expression.word_tokens.select { |w| varset.values.include?(w) }.uniq

    expression_tokens = expression.tokenize

    variables.each { |v| expression_tokens = expression_tokens.gsub(v.to_s, "v." + transform_varname(v))  }
    constants.each { |c| expression_tokens = expression_tokens.gsub(c.to_s, transform_const(c))  }

    expression_tokens = expression_tokens.gsub('&&', '&')
    expression_tokens = expression_tokens.gsub('||', '|')
    expression_tokens = expression_tokens.gsub('||', '|')
    expression_tokens = expression_tokens.gsub('==', '=')
    expression_tokens = expression_tokens.gsub('=>', '->')
    expression_tokens = expression_tokens.gsub('<=>', '<->')

    expression_s = expression_tokens.join(" ")

    return expression_s
end

#transform_graph(program_graph, include_specs: true) ⇒ Object 



6
7
8
9
10
11
12
13
14
15
16
17
 
# File 'lib/pg-verify/transform/nusmv_transformation.rb', line 6

def transform_graph(program_graph, include_specs: true)
    variables  = program_graph.all_variables
    components = program_graph.components

    var_s  = transform_variables(variables)
    cmp_s  = transform_components(components, variables)
    main_s = transform_main_module(components)

    specs = transform_specification(program_graph.specification, variables) if include_specs

    return "#{var_s}\n\n#{cmp_s}\n\n#{main_s}\n\n#{specs}\n"
end

#transform_init_expression(component, varset, owned_vars) ⇒ Object 



94
95
96
97
98
99
100
101
102
103
 
# File 'lib/pg-verify/transform/nusmv_transformation.rb', line 94

def transform_init_expression(component, varset, owned_vars)
    init = owned_vars.map { |var|
        next if var.init_expression.nil?
        transform_expression(var.init_expression, varset)
    }
    init << transform_expression(component.init_expression, varset) unless  component.init_expression.nil?
    init = init.compact.join(" & ")
    init = "TRUE" if init.empty?
    return init
end

#transform_main_module(components) ⇒ Object 



209
210
211
212
213
214
215
216
217
218
219
 
# File 'lib/pg-verify/transform/nusmv_transformation.rb', line 209

def transform_main_module(components)
    # Instantiate variable module as v
    var_s = "v : _VARS();\n"
    # Instantiate all component modules, passing in v
    var_s += components.map { |component|
        instance = transform_module_instance_name(component.name)
        modul    = transform_module_name(component.name)
        "#{instance} : #{modul}(v);"
    }.join("\n")
    return module_string("main", var: var_s)
end

#transform_module_instance_name(name) ⇒ Object 



243
244
245
 
# File 'lib/pg-verify/transform/nusmv_transformation.rb', line 243

def transform_module_instance_name(name)
    "p_#{name}"
end

#transform_module_name(name) ⇒ Object 



239
240
241
 
# File 'lib/pg-verify/transform/nusmv_transformation.rb', line 239

def transform_module_name(name)
    "_P_#{name}"
end

#transform_range(range) ⇒ Object 



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

def transform_range(range)
    # Transform state variables
    return "{#{range.map { |e| transform_const(e) }.join(", ")}};" if range.is_a?(Array)
    # Transform small integer variables
    return "{#{range.to_a.join(", ")}};" if (range.last - range.first) < 5
    # Transform regular integer variables
    return "#{range.first}..#{range.last};"
end

#transform_spec(spec, varset) ⇒ Object 



251
252
253
254
255
256
257
 
# File 'lib/pg-verify/transform/nusmv_transformation.rb', line 251

def transform_spec(spec, varset)
    expression_s  = "-- #{spec.text}\n"
    expression_s += "-- Defined in: #{spec.source_location.to_s}\n"
    keyword = {  ltl: "LTLSPEC", ctl: "CTLSPEC" }[spec.expression.predict_type]
    expression_s += keyword + " " + transform_expression(spec.expression, varset)
    return expression_s
end

#transform_specification(specification, varset) ⇒ Object 



247
248
249
 
# File 'lib/pg-verify/transform/nusmv_transformation.rb', line 247

def transform_specification(specification, varset)
    return specification.flatten().map { |s| transform_spec(s, varset) }.join("\n")
end

#transform_transition(varset, component, transition) ⇒ Object 



105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
 
# File 'lib/pg-verify/transform/nusmv_transformation.rb', line 105

def transform_transition(varset, component, transition)
    expression = []

    cmp_varname = transform_varname(component.name)
    prev_state  = transform_const(transition.src_state)
    expression << "v.#{cmp_varname} = #{prev_state}"

    next_state = transform_const(transition.tgt_state)
    expression << "next(v.#{cmp_varname}) = #{next_state}"

    precon_s = transform_expression(transition.precon, varset)
    guard_s  = transform_expression(transition.guard, varset)

    action_s, assigned_vars = transform_assignment(transition.action, component, varset)
    
    keep_vars_constant = varset.select_by_owner(component.name).names
        .reject { |v| assigned_vars&.map(&:to_s)&.include?(v.to_s) }
        .reject { |v| v.to_s == component.name.to_s }
        .map { |v| "next(v.#{transform_varname(v)}) = v.#{transform_varname(v)}" }
        .join(' & ')

    expression << precon_s
    expression << guard_s
    expression << action_s
    expression << keep_vars_constant

    return expression.compact.reject(&:empty?).map{ |s| "( #{s} )" }.join(' & ')
end

#transform_variable(variable) ⇒ Object 



28
29
30
 
# File 'lib/pg-verify/transform/nusmv_transformation.rb', line 28

def transform_variable(variable)
    return "#{transform_varname(variable.name)} : #{transform_range(variable.range)}"
end

#transform_variables(varset) ⇒ Object 



19
20
21
22
 
# File 'lib/pg-verify/transform/nusmv_transformation.rb', line 19

def transform_variables(varset)
    vars_s = varset.to_a.map { |v| transform_variable(v) }.join("\n")
    return module_string("_VARS", var: vars_s)
end

#transform_varname(name) ⇒ Object 



230
231
232
 
# File 'lib/pg-verify/transform/nusmv_transformation.rb', line 230

def transform_varname(name)
    "V_#{name}"
end