Class: Compiler

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

Instance Attribute Summary collapse

Instance Method Summary collapse

Constructor Details

#initialize ⇒ Compiler

Returns a new instance of Compiler.



42
43
44
45
46
47
48
 
# File 'lib/falluto/compiler.rb', line 42

def initialize
  @parser = Falluto::GrammarParser.new
  #@parser.root = "Choose your favorite rule"
  @generator = Falluto::NuSMV::CodeGenerator.new
  @context = CompilerContext.new
  @specs = []
end

Instance Attribute Details

#compiled_string ⇒ Object (readonly)

Returns the value of attribute compiled_string.



40
41
42
 
# File 'lib/falluto/compiler.rb', line 40

def compiled_string
  @compiled_string
end

#input_string ⇒ Object (readonly)

Returns the value of attribute input_string.



40
41
42
 
# File 'lib/falluto/compiler.rb', line 40

def input_string
  @input_string
end

#parsed_tree ⇒ Object (readonly)

Returns the value of attribute parsed_tree.



40
41
42
 
# File 'lib/falluto/compiler.rb', line 40

def parsed_tree
  @parsed_tree
end

#specs ⇒ Object (readonly)

Returns the value of attribute specs.



40
41
42
 
# File 'lib/falluto/compiler.rb', line 40

def specs
  @specs
end

Instance Method Details

#add_condition_to_faults(condition, faults) ⇒ Object 



279
280
281
 
# File 'lib/falluto/compiler.rb', line 279

def add_condition_to_faults condition, faults
  faults.each { |fault| fault.add_auxiliar_variable condition }
end

#auxiliar_variables ⇒ Object 



58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
 
# File 'lib/falluto/compiler.rb', line 58

def auxiliar_variables
  variables = Set.new

  each_module do |m|
    m.each_fault do |f|
      f.each_auxiliar_variable do |v|
        variables << v.name
      end
      variables << f.precondition_variable
      variables << f.restore_variable
      variables << f.fairness_variable
    end
  end

  variables.sort
end

#build_condition_with_faults(condition, faults) ⇒ Object 



275
276
277
 
# File 'lib/falluto/compiler.rb', line 275

def build_condition_with_faults condition, faults
  "(#{condition}) & #{no_fault_active faults}"
end

#compile(node) ⇒ Object 



79
80
81
82
83
84
85
86
87
88
89
90
 
# File 'lib/falluto/compiler.rb', line 79

def compile node
  method = nil
  begin
    method = "compile_#{node.class.human_name}"
    #puts "compiling with #{method} '#{node.text}'"
    send method, node
  rescue => e
    puts e.message
    puts e.backtrace
    raise "[ERROR] Don't know how to compile #{node.class} (#{node.text})"
  end
end

#compile_falluto_assignment_node(node) ⇒ Object

Compile the following construct

next(v) := val;

into

next(v) := compile(val);

so that we can propagate fault compilation into the value. (when val is a ‘case’ construct)



174
175
176
177
178
179
 
# File 'lib/falluto/compiler.rb', line 174

def compile_falluto_assignment_node node
  variable = node.variable
  value = node.value
  @context.variable = variable
  %Q|  next(#{@context.variable}) := #{compile value};\n|
end

#compile_falluto_case_element_node(node) ⇒ Object

Compile the folllowing construct

c : v disabled_by f,g;

into

© & !f.active & !g.active : v;

if the construct is not disabled by faults, then the input code is unchanged.



223
224
225
226
227
228
229
230
231
232
233
234
235
236
 
# File 'lib/falluto/compiler.rb', line 223

def compile_falluto_case_element_node node
  condition = node.condition
  value = node.value

  if node.has_faults?
    faults = @context.current_module.get_faults *node.faults
    raise UndeclaredFault.new fname if faults.any?{ |f| f.nil? }
    new_condition = build_condition_with_faults condition, faults
    add_condition_to_faults condition, faults
    "#{new_condition} : #{value};\n"
  else
    "#{condition} : #{value};\n"
  end
end

#compile_falluto_case_node(node) ⇒ Object

Compile the following construct

next(v) := 

case
  c_1 : v_1 disabled_by {f, g};
  ...
  c_n : v_n;
esac;

into

next(v) :=

case
  (c_1) & !f.active & !g.active : compile(v1);
  ...
  c_n : v_n;
  1 : v;
esac;



200
201
202
203
204
205
206
207
208
209
210
 
# File 'lib/falluto/compiler.rb', line 200

def compile_falluto_case_node node
  new_cases = []
  has_faults = false
  node.each_case do |c|
    has_faults ||= c.has_faults?
    new_cases << c.compile(self)
  end
  new_cases << "  1 : #{@context.variable};\n" if has_faults
  
  "case\n" + new_cases.join('') + "esac"
end

#compile_falluto_fault_assignment_node(node) ⇒ Object

Compile the following construct

next(v) := val disabled_by f,g;

into

next(v) :=

case
  (1) & !f.active & !g.active : compile(val);
  1 : v;
esac;



144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
 
# File 'lib/falluto/compiler.rb', line 144

def compile_falluto_fault_assignment_node node
  variable = node.variable
  value = node.value
  faults = @context.current_module.get_faults *node.faults
  raise UndeclaredFault.new fname if faults.any?{ |f| f.nil? }
  @context.variable = variable

  new_condition = build_condition_with_faults "1", faults

  <<-END
next(#{@context.variable}) :=
  case
    #{new_condition} : #{compile value};
    1 : #{@context.variable};
  esac;
  END

end

#compile_falluto_fault_declaration_node(node) ⇒ Object

Create a new fault object for this declaration. No code is output for this construct.

Raises:



119
120
121
122
123
124
125
126
127
128
129
130
 
# File 'lib/falluto/compiler.rb', line 119

def compile_falluto_fault_declaration_node node
  modname = @context.current_module.name
  name = node.name
  precondition = node.precondition
  restores = node.restores
  effect = node.effect

  f = Falluto::NuSMV::Fault.new modname, name, precondition, restores, effect
  raise RedefinedFault.new(f.name) if @context.current_module.is_defined? f
  @context.current_module.add_fault f
  ''
end

#compile_falluto_ltl_spec_node(node) ⇒ Object

Compile the following construct

LTLSPEC s

into

LTLSPEC ((faults and processes are fair) -> (s))



255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
 
# File 'lib/falluto/compiler.rb', line 255

def compile_falluto_ltl_spec_node node
  spec = node.specification
  sf_list = ['1']

  @context.main_module.each_variable do |variable|
    type = @context[variable.type]
    # NOTE nusmvmodule will be nil if type is undeclared
    sf = dump_module_strong_fairness(type, variable.name) unless type.nil?
    sf_list << sf if sf
  end
 
  @specs << spec

  "LTLSPEC (( #{sf_list.join(" & ")} ) -> #{spec})"
end

#compile_falluto_module_declaration_node(node) ⇒ Object 



103
104
105
106
107
108
109
110
111
112
113
114
 
# File 'lib/falluto/compiler.rb', line 103

def compile_falluto_module_declaration_node node
  m = Falluto::NuSMV::Module.new node.name
  @context << m

  result = "MODULE " + node.signature + "\n"
  result << compile(node.declarations)
  if @context.current_module.has_faults?
    result << dump_faulty_module_declarations 
    result << dump_system_effect_declaration
  end
  result
end

#compile_falluto_var_decl_node(node) ⇒ Object

Compile a variable will output the original code. However, we also need to track variables and their types to modify the model specifications.



241
242
243
244
245
 
# File 'lib/falluto/compiler.rb', line 241

def compile_falluto_var_decl_node node
  v = Falluto::NuSMV::Variable.new node.name, node.vartype
  @context.current_module.add_variable v
  compile_treetop_runtime_syntax_node node
end

#compile_treetop_runtime_syntax_node(node) ⇒ Object

Recursively compile a syntax node descending into its elements.



93
94
95
96
97
98
99
100
101
 
# File 'lib/falluto/compiler.rb', line 93

def compile_treetop_runtime_syntax_node node
  if node.elements
    node.elements.map{|element| 
#        puts "Invoking on #{element.class}"
      compile element}.to_s
  else
    node.text
  end 
end

#declare_affected_variable_modification(fault, variable, effect) ⇒ Object 



396
397
398
399
400
401
402
403
404
405
406
 
# File 'lib/falluto/compiler.rb', line 396

def declare_affected_variable_modification fault, variable, effect
  active = fault.active_variable

  <<-END_DECL
next(#{variable}) :=
  case
    !#{active} & next(#{active}) : #{effect};
    1 : #{variable};
  esac;
  END_DECL
end

#declare_affected_variables_modifications(fault) ⇒ Object 



386
387
388
389
390
391
392
393
394
 
# File 'lib/falluto/compiler.rb', line 386

def declare_affected_variables_modifications fault
  decls = ''

  fault.each_affected_variable_with_effect do |v, effect|
    decls << declare_affected_variable_modification(fault, v, effect)
  end

  decls
end

#declare_auxiliar_variables(fault) ⇒ Object 



337
338
339
340
341
342
343
 
# File 'lib/falluto/compiler.rb', line 337

def declare_auxiliar_variables fault
  str = ''
  fault.each_auxiliar_variable do |v|
    str << %Q|DEFINE #{v.name} := (#{v.condition});\n|
  end
  str
end

#declare_fault_fairness(fault) ⇒ Object 



345
346
347
348
349
350
351
352
353
354
355
356
 
# File 'lib/falluto/compiler.rb', line 345

def declare_fault_fairness fault
  fv = fault.fairness_variable
  result =<<-END_DECL
VAR #{fv} : boolean;
ASSIGN
next(#{fv}) :=
  case
    #{fault.fairness_condition} & !#{fv} : 1;
    1 : 0;
  esac;
  END_DECL
end

#declare_fault_instance(fault) ⇒ Object 



333
334
335
 
# File 'lib/falluto/compiler.rb', line 333

def declare_fault_instance fault
  %Q|VAR #{fault.name} : process #{fault.instance_signature};\n|
end

#declare_fault_module(fault) ⇒ Object 



367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
 
# File 'lib/falluto/compiler.rb', line 367

def declare_fault_module fault
  instance_signature = fault.instance_signature
  active = fault.active_variable
  pre = fault.precondition_variable
  restore = fault.restore_variable

  <<-END_DECL
MODULE #{instance_signature}
VAR #{active} : boolean;
ASSIGN
next(#{active}) :=
  case
    #{pre} & !#{active} : {0, 1};
    #{active} & next(#{restore}) : 0;
    1 : #{active};
  esac;
  END_DECL
end

#declare_fault_precondition(fault) ⇒ Object 



325
326
327
 
# File 'lib/falluto/compiler.rb', line 325

def declare_fault_precondition fault
  %Q|DEFINE #{fault.precondition_variable} := (#{fault.precondition});\n|
end

#declare_fault_restore(fault) ⇒ Object 



329
330
331
 
# File 'lib/falluto/compiler.rb', line 329

def declare_fault_restore fault
  %Q|DEFINE #{fault.restore_variable} := (#{fault.restore});\n|
end

#declare_sytem_effect(fault) ⇒ Object 



358
359
360
361
362
363
364
365
 
# File 'lib/falluto/compiler.rb', line 358

def declare_sytem_effect fault
  # The system effect is a module which takes all variables affected by
  # faults as parameters and modifies them when the fault occurs.

  declare_fault_module(fault) +
    declare_affected_variables_modifications(fault) +
    "FAIRNESS running\n"
end

#dump_faulty_module_declarations ⇒ Object 



283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
 
# File 'lib/falluto/compiler.rb', line 283

def dump_faulty_module_declarations 
  decls = ''

  @context.current_module.each_fault do |fault|
    decls << "-- Begin declarations for (#{fault.name})\n"
    decls << declare_fault_precondition(fault)
    decls << declare_fault_restore(fault)
    decls << declare_fault_instance(fault)
    decls << declare_auxiliar_variables(fault)
    decls << declare_fault_fairness(fault)
    decls << "-- End declarations for (#{fault.name})\n"
  end

  decls << "FAIRNESS running\n" if @context.current_module.has_faults?
  decls
end

#dump_module_strong_fairness(m, inst) ⇒ Object

NOTE: Can we return true when the module has no faults?



314
315
316
317
318
319
320
321
322
323
 
# File 'lib/falluto/compiler.rb', line 314

def dump_module_strong_fairness m, inst
  sf = []
  m.each_fault{ |f| sf << f.strong_fairness(inst) }

  if sf.empty?
    nil
  else
    "(#{sf.join(" & ")})"
  end
end

#dump_system_effect_declaration ⇒ Object 



300
301
302
303
304
305
306
307
308
309
310
311
 
# File 'lib/falluto/compiler.rb', line 300

def dump_system_effect_declaration
  decls = ''

  @context.current_module.each_fault do |fault|
    name = @context.current_module.name
    decls << "-- Begin system effect for (#{name}, #{fault.name})\n"
    decls << declare_sytem_effect(fault)
    decls << "-- End system effect for (#{name}, #{fault.name})\n"
  end

  decls
end

#each_module(&block) ⇒ Object 



75
76
77
 
# File 'lib/falluto/compiler.rb', line 75

def each_module &block
  @context.modules.each{|m| yield m}
end

#no_fault_active(faults) ⇒ Object 



271
272
273
 
# File 'lib/falluto/compiler.rb', line 271

def no_fault_active faults
  faults.collect{|f| "! #{f.name}.#{f.active_variable}"}.join(' & ')
end

#run(input) ⇒ Object 



50
51
52
53
54
55
56
 
# File 'lib/falluto/compiler.rb', line 50

def run input
  @input_string = input
  @parsed_tree = @parser.parse @input_string
  if @parsed_tree
    @compiled_string = @parsed_tree.send :compile, self
  end
end