Module: PgVerify::Doctor
- Defined in:
- lib/pg-verify/doctor/doctor.rb
Defined Under Namespace
Classes: DoctorError, Warning
Class Method Summary
collapse
Class Method Details
.check ⇒ Object
22
23
24
25
26
27
28
29
|
# File 'lib/pg-verify/doctor/doctor.rb', line 22
def self.check()
checks = Doctor.methods
.select { |method| method.to_s.start_with?("check_") }
.map { |sym| sym.to_s.sub("check_", "").to_sym }
.sort
warnings = checks.map { |check| run_check(check) }.flatten.compact
raise DoctorError.new(warnings) unless warnings.empty?
end
|
.check_01_Can_find_NuSMV ⇒ Object
44
45
46
47
48
49
50
51
52
|
# File 'lib/pg-verify/doctor/doctor.rb', line 44
def self.check_01_Can_find_NuSMV()
return [] unless PgVerify::NuSMV::Runner.new.find_nusmv_path.nil?
return Warning.new("Unable to locate the NuSMV executable",
"Make sure to install NuSMV by unpacking it and placing the entire folder into\n" \
"the #{'addon'.c_file} directory of your project. " \
"(#{File.expand_path('addon').c_sidenote})\n" \
"Alternatively you can set the #{'nusmv.path'.c_string} in the configuration."
)
end
|
.check_02_Can_run_NuSMV ⇒ Object
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
|
# File 'lib/pg-verify/doctor/doctor.rb', line 54
def self.check_02_Can_run_NuSMV()
path = PgVerify::NuSMV::Runner.new.find_nusmv_path
return :skip if path.nil?
example_file = File.join(PgVerify.root, "data", "nusmv.sample.smv")
return [] if Core::CMDRunner.run_for_exit_code("#{path} #{example_file}") == 0
return Warning.new("Unable to run the NuSMV executable",
"NuSMV could be found here: #{path.c_file}\n" \
"However it could not be executed. Here are a few things to try:\n" \
" - Make sure the file is executable\n" \
" - Make sure you have the required permissions"
)
end
|
.check_03_Run_integration_tests ⇒ Object
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
|
# File 'lib/pg-verify/doctor/doctor.rb', line 70
def self.check_03_Run_integration_tests()
return :skip if PgVerify::NuSMV::Runner.new.find_nusmv_path.nil?
warnings = []
test_files = Dir[File.join(PgVerify.root, "integration_tests", "ruby_dsl", "*.rb")].sort
warnings += test_files.map { |test_file|
model = Interpret::PgScript.new.interpret(test_file).first
PgVerify::Model::Validation.validate!(model)
results = NuSMV::Runner.new().run_specs(model)
failures = results.reject(&:success)
next if failures.empty?
test_name = File.basename(test_file, '.*').gsub("_", "-")
failures_s = failures.map { |f| "#{f.spec.text} (#{f.spec.expression.to_s.c_blue})" }
show_command = "$ pg-verify show nusmv --script #{File.expand_path(test_file)}".c_cyan
test_command = "$ pg-verify test --script #{File.expand_path(test_file)}".c_cyan
Warning.new("Failed integration test in #{test_name}",
"The test #{test_name.c_string} contains the following unsatisfied specifications:\n" \
"\t- #{failures_s.join("\n\t- ")}\n" \
"These specifications should be valid if pg-verify works as expected.\n" \
"You can use the following commands to debug this:\n" \
" #{show_command}\n #{test_command}"
)
}.compact
warnings += test_files.map { |test_file|
model = Interpret::PgScript.new.interpret(test_file).first
next if model.hazards.empty?
require 'set'
dcca = Model::DCCA.new(model, NuSMV::Runner.new)
result = dcca.perform()
expected_cut_sets = File.read(test_file)
.split("\n")
.find { |l| l.include?("Expected Cut Sets") }
.scan(/\{([^}]+)\}/).flatten
.map { |string| string.split(",").map(&:strip).map(&:to_sym) }
.map { |cut_set| Set.new(cut_set) }
actual_cut_sets = result.values.first.map { |cut_set| Set.new(cut_set) }
next if Set.new(actual_cut_sets) == Set.new(expected_cut_sets)
Warning.new("Failed DCCA for #{File.basename(test_file)}",
"The DCCA for hazard #{result.keys.first.expression.to_s.c_blue} yielded unexpected cut sets:\n" \
"Expected: #{expected_cut_sets}\n" \
"Got : #{actual_cut_sets}\n"
)
}.compact
return warnings
end
|
.check_04_Check_project_files ⇒ Object
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
|
# File 'lib/pg-verify/doctor/doctor.rb', line 126
def self.check_04_Check_project_files()
warnings = []
script = Settings.ruby_dsl.default_script_name
return Warning.new("Failed to find model definition at #{script}",
"If you run PG verify without any arguments it expects a program graph definition\n" \
"at your working directory, which should be named #{script.c_file} by default.\n" \
"Based on your current working directory this would be this full path:\n" \
"\t#{File.expand_path(script).c_file}"
) unless File.file?(script)
begin
Interpret::PgScript.new.interpret(script)
rescue Exception => e
return Warning.new("Failed to interpret model at #{script}",
"Your default model definition at #{script.c_file}\n" \
"(Full path: #{File.expand_path(script).c_sidenote})\n" \
"Could not be interpreted. Make sure there are no syntax errors."
)
end
return []
end
|
.run_check(symbol) ⇒ Object
31
32
33
34
35
36
37
38
39
40
41
42
|
# File 'lib/pg-verify/doctor/doctor.rb', line 31
def self.run_check(symbol)
Shell::LoadingPrompt.while_loading("Checking #{symbol.to_s.gsub('_', ' ').c_string}") {
warnings = ([self.send(:"check_#{symbol}")] || []).flatten.compact
state = warnings.empty? ? :success : :error
msg = warnings.empty? ? "Ok" : "#{warnings.length} warning(s)!"
if warnings.length == 1 && warnings.first == :skip
state, msg, warnings = :empty, "Skipped!", []
end
Shell::LoadingPrompt::LoadingResult.new(warnings, msg, state: state)
}
end
|