Show loops in traces

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

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

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)