Class: PgVerify::Cli::BaseCommand

Inherits:

Thor

• Object
• Thor
• PgVerify::Cli::BaseCommand

Defined in:

lib/pg-verify/cli/cli.rb

Class Method Summary

• .exit_on_failure? ⇒ Boolean

  Make Thor exit with non-0 in case of errors.

Instance Method Summary

• #dcca ⇒ Object
• #doctor ⇒ Object
• #init ⇒ Object
• #simulate ⇒ Object
• #test ⇒ Object
• #version ⇒ Object

Class Method Details

.exit_on_failure? ⇒ Boolean

Make Thor exit with non-0 in case of errors

Returns:

• (Boolean)

# File 'lib/pg-verify/cli/cli.rb', line 300

def self.exit_on_failure?(); true end

Instance Method Details

#dcca ⇒ Object

# File 'lib/pg-verify/cli/cli.rb', line 169

def dcca()
    models = CliUtils.load_models(options)

    models.each { |model|
        Shell::LoadingPrompt.while_loading("Checking for deadlocks") {
            NuSMV::Runner.new().run_check!(model); "ok"
        }

        dcca = Model::DCCA.new(model, NuSMV::Runner.new)
        result = Shell::LoadingPrompt.while_loading("Calculating DCCA for #{model.name.to_s.c_string}") {
            dcca.perform()
        }
        result.each { |hazard, crit_sets|
            s = crit_sets.length == 1 ? "" : "s"
            message = "Hazard #{hazard.text.to_s.c_string} (#{hazard.expression.to_s.c_blue}) "
            message += "has #{crit_sets.length.to_s.c_num} minimal critical fault set#{s}:" if crit_sets.length > 0
            message += "has no minimal critical fault sets, meaning it is safe!".c_success if crit_sets.length == 0
            puts message
            crit_sets.each { |set|
                puts "\t{ #{set.map(&:to_s).map(&:c_blue).join(', ')} }"
            }
        }
    }
end

#doctor ⇒ Object

# File 'lib/pg-verify/cli/cli.rb', line 292

def doctor()
    Doctor.check()
end

#init ⇒ Object

# File 'lib/pg-verify/cli/cli.rb', line 253

def init()

    target = options[:directory].blank? ? Dir.pwd() : File.expand_path(options[:directory])
    if Dir.exist?(target) && Dir.entries(target).size > 2
        puts "The target directory #{target.c_file} isn't empty!"
        exit 1
    end

    # Create target dir
    FileUtils.mkdir_p(target)

    # Copy files to target
    template_dir = File.join(PgVerify.root, "data", "project-template")
    files = Dir.glob(File.join(template_dir, '**', '*'), File::FNM_DOTMATCH).select { |f| File.file?(f) }
    files.each { |f| 
        target_file = File.join(target, f.sub(template_dir, ""))
        target_file = target_file.gsub(".resource", "")
        FileUtils.mkdir_p(File.dirname(target_file))
        FileUtils.cp(f, target_file) unless File.basename(f) == ".keep"
    }
    # Copy the actual default config into the project as that
    # will contain all keys and should be commented
    FileUtils.cp(File.join(PgVerify.root, "data", "config", "pg-verify.yml"), File.join(target, ".pg-verify.yml"))
    prelude_pg_file = File.join(PgVerify.root, "integration_tests", "ruby_dsl", "016_pressure_tank.rb")
    FileUtils.cp(prelude_pg_file, File.join(target, Settings.ruby_dsl.default_script_name))

    # Initialize git project
    Dir.chdir(target) { 
        Core::CMDRunner.run_cmd("git init")
        Core::CMDRunner.run_cmd("git add .")
        Core::CMDRunner.run_cmd("git commit -m \"Initial Commit\"")
    }

    puts "Successfully initialized project at #{target.c_file}!"
    puts "You can read the #{'README.md'.c_file} to get started."
    puts "Run #{'pg-verify doctor'.c_blue} and follow the instructions to set up your environment!"
end

#simulate ⇒ Object

# File 'lib/pg-verify/cli/cli.rb', line 207

def simulate()
    render_options = {
        render_labels: !options[:"hide-labels"],
        render_precons: !options[:"hide-precons"],
        render_guards: !options[:"hide-guards"],
        render_actions: !options[:"hide-actions"]
    }

    models = CliUtils.load_models(options)
    runner = NuSMV::Runner.new

    models.each { |model|
        Shell::LoadingPrompt.while_loading("Checking for deadlocks") {
            NuSMV::Runner.new().run_check!(model); "ok"
        }

        trace = Shell::LoadingPrompt.while_loading("Simulating model #{model.name.to_s.c_string}") {
            runner.run_simulation(model, options[:steps], random: options[:random])
        }

        # Print the trace
        puts trace.to_s

        next unless options[:png]

        # Prepare output dir
        out_dir = File.expand_path("simulate-" + model.name.to_s.gsub(/\W+/, '_').downcase, Settings.outdir)
        FileUtils.mkdir_p(out_dir)

        # Generate images
        Shell::LoadingPrompt.while_loading("Rendering states") { |printer|
            trace.states.each_with_index { |variable_state, index|
                printer.printl("Step #{index + 1}/#{trace.states.length}")
                puml = Transform::PumlTransformation.new(render_options).transform_graph(model, variable_state: variable_state)
                png = PlantumlBuilder::Formats::PNG.new(puml).load
                out_path = File.expand_path("step-#{index}.png", out_dir)
                File.binwrite(out_path, png)
            }
        }
        puts "Wrote #{trace.states.length.to_s.c_num} files to #{out_dir.c_file}"
    }

end

#test ⇒ Object

# File 'lib/pg-verify/cli/cli.rb', line 140

def test()
    models = CliUtils.load_models(options)

    models.each { |model|
        Shell::LoadingPrompt.while_loading("Checking for deadlocks") {
            NuSMV::Runner.new().run_check!(model); "ok"
        }

        results = Shell::LoadingPrompt.while_loading("Running specifications") {
            NuSMV::Runner.new().run_specs(model)
        }

        results.each { |result|
            stat_string = result.success ? "PASSED".c_success : "FAILED".c_error
            puts "[ #{stat_string} ] #{result.spec.text}"
            puts "           #{result.spec.expression.to_s.c_blue}"
            unless result.success
                puts "           Here is a counter example:".c_red
                trace_s = result.trace.to_s.indented(str: "           >>  ".c_red)
                puts trace_s + "\n"
            end
        }
    }
end

#version ⇒ Object

# File 'lib/pg-verify/cli/cli.rb', line 125

def version()
    banner = File.read(File.join(PgVerify.root, "data", "banner.txt"))
    banner = banner.gsub("0.1.0", PgVerify::VERSION)
    colors = [ "red", "orange", "yellow", "orange", "red" ]
    banner = banner.split("\n").each_with_index.map { |l, i| l.send(:"c_#{colors[i]}") }.join("\n")
    puts banner
    puts 
    puts "You are running #{'pg-verify'.c_string} version #{PgVerify::VERSION.to_s.c_num}"
    puts "Installation root: #{PgVerify.root.to_s.c_file}"
end