Class: Falluto::NuSMV::CodeGenerator

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

Instance Method Summary collapse

Instance Method Details

#define(var, expr) ⇒ Object 



4
5
6
 
# File 'lib/falluto/nusmv/codegen.rb', line 4

def define var, expr
  %Q|DEFINE #{var} := (#{expr});|
end

#fairness(expr) ⇒ Object 



12
13
14
 
# File 'lib/falluto/nusmv/codegen.rb', line 12

def fairness expr
  %Q|FAIRNESS #{expr}|
end

#implies(p, q) ⇒ Object 



32
33
34
 
# File 'lib/falluto/nusmv/codegen.rb', line 32

def implies(p, q)
  %Q|((#{p}) -> (#{q}))|
end

#instance_process(type, *args) ⇒ Object 



20
21
22
 
# File 'lib/falluto/nusmv/codegen.rb', line 20

def instance_process type, *args
  "process #{type}(#{args.join(', ')});"
end

#ltlspec(expr) ⇒ Object 



28
29
30
 
# File 'lib/falluto/nusmv/codegen.rb', line 28

def ltlspec expr
  %Q|LTLSPEC #{expr}|
end

#module(signature) ⇒ Object 



16
17
18
 
# File 'lib/falluto/nusmv/codegen.rb', line 16

def module signature
  %Q|MODULE #{signature}|
end

#process(type) ⇒ Object 



24
25
26
 
# File 'lib/falluto/nusmv/codegen.rb', line 24

def process type
  %Q|process #{type}|
end

#variable_declaration(var, type) ⇒ Object 



8
9
10
 
# File 'lib/falluto/nusmv/codegen.rb', line 8

def variable_declaration var, type
  %Q|VAR #{var} : #{type};|
end