From 33528bfecd3d685eb18a7a047d8597e04b4fc3e2 Mon Sep 17 00:00:00 2001 From: Arian Weber Date: Tue, 19 Mar 2024 10:25:32 +0100 Subject: [PATCH] Show loops in traces --- lib/pg-verify/cli/cli.rb | 2 +- lib/pg-verify/model/simulation/trace.rb | 12 ++++++++++-- lib/pg-verify/nusmv/runner.rb | 14 +++++++------- 3 files changed, 18 insertions(+), 10 deletions(-) diff --git a/lib/pg-verify/cli/cli.rb b/lib/pg-verify/cli/cli.rb index afacd08..af5bdf5 100644 --- a/lib/pg-verify/cli/cli.rb +++ b/lib/pg-verify/cli/cli.rb @@ -136,7 +136,7 @@ def test() puts "[ #{stat_string} ] #{result.spec.text}" puts " #{result.spec.expression.to_s.c_blue}" unless result.success - puts " Here is an counter example:".c_red + puts " Here is a counter example:".c_red trace_s = result.trace.to_s.indented(str: " >> ".c_red) puts trace_s + "\n" end diff --git a/lib/pg-verify/model/simulation/trace.rb b/lib/pg-verify/model/simulation/trace.rb index 23bbc31..45ffbf8 100644 --- a/lib/pg-verify/model/simulation/trace.rb +++ b/lib/pg-verify/model/simulation/trace.rb @@ -5,9 +5,11 @@ class Trace attr_accessor :model attr_accessor :states + attr_accessor :loop_index - def initialize(model, states) + def initialize(model, states, loop_index: -1) @model, @states = model, states + @loop_index = loop_index end def to_s(include_steps: true) @@ -18,11 +20,17 @@ def to_s(include_steps: true) parts = vars.map { |var| var_string = state_vars.varname?(var) ? var.to_s.c_state.c_bold : var.to_s.c_string - var_string + "\n" + @states.each_with_index.map{ |state, index| value_str(var, state[var], index) }.join("\n") + var_string + "\n" + @states.each_with_index.map{ |state, index| value_str(var, state[var], index) }.join("\n") } str = "Step".c_num.c_bold + "\n" + (0...@states.length).map { |i| "#{i + 1}" } .join("\n") str = "" unless include_steps parts.each { |part| str = str.line_combine(part, separator: " ") } + + unless @loop_index.nil? || @loop_index < 0 + loop_str = (0...@states.length).map { |i| i == @loop_index + 1 ? "<- loop".c_blue : "" } .join("\n") + str = str.line_combine(loop_str, separator: " ") + str += "\n" + "Loop starts at #{@loop_index + 1}".c_sidenote + end return str end diff --git a/lib/pg-verify/nusmv/runner.rb b/lib/pg-verify/nusmv/runner.rb index d905607..367fc90 100644 --- a/lib/pg-verify/nusmv/runner.rb +++ b/lib/pg-verify/nusmv/runner.rb @@ -92,6 +92,12 @@ def parse_trace(program_graph, nusmv_output) loop_index = -1 nusmv_output.split("\n").each { |line| + # Mark a loop for the following state + if line.include?("Loop starts here") + loop_index = var_states.length + next + end + # Wait for heading of new state if line.match(/\s*-> State: .+ <-/) # Complete and store the old state if any @@ -109,11 +115,6 @@ def parse_trace(program_graph, nusmv_output) # Skip lines before the first state next if current_var_state.nil? - if line.include?("Loop starts here") - loop_index == var_states.length - 1 - next - end - # Parse the variable state key, val = parse_var_assignment_in_trace(line) next if key.nil? || val.nil? @@ -127,8 +128,7 @@ def parse_trace(program_graph, nusmv_output) } var_states << current_var_state end - - return Model::Trace.new(program_graph, var_states) + return Model::Trace.new(program_graph, var_states, loop_index: loop_index) end def parse_var_assignment_in_trace(line)