Improvements and bug fixes

integration_tests/ruby_dsl/017_ctl_specifications.rb

@@ -14,7 +14,6 @@
         it "cannot stay in one" => :"! G Example == one"
         it "can stay in three" => :"EX AG Example == three"
         it "cannot go back to one from three" => :"AG ( (Example == three) => ! EF Example == one)"
-        it "this is false" => :"AG Example == one"
     end
 
 end

integration_tests/ruby_dsl/018_non_atomic_hazard.rb

@@ -0,0 +1,17 @@
+model :NonAtomicHazard do
+
+    persistent error :KeysForgotten
+
+    graph :Person do
+        states :inside, :outside, init: :inside
+        transition :inside => :outside
+        transition :outside => :inside do
+            guard "KeysForgotten == No"
+        end
+    end
+
+    # This does not work as at any point the fault could not have occurred
+    # (KeysForgotten == No) already but then it happens at a later point
+    # Expected Cut Sets: { :"" }
+    # hazard "The person can't get in" => :"G Person == outside"
+end

lib/pg-verify/cli/cli.rb

@@ -118,7 +118,7 @@ def test()
 
                 models.each { |model|
                     Shell::LoadingPrompt.while_loading("Checking for deadlocks") {
-                        NuSMV::Runner.new().run_check!(model)
+                        NuSMV::Runner.new().run_check!(model); "ok"
                     }
 
                     results = Shell::LoadingPrompt.while_loading("Running specifications") {
@@ -130,8 +130,8 @@ def test()
                         puts "[ #{stat_string} ] #{result.spec.text}"
                         puts "           #{result.spec.expression.to_s.c_blue}"
                         unless result.success
-                            puts "Here is the trace:".c_red
-                            trace_s = result.trace.to_s.indented(str: " >> ".c_red)
+                            puts "           Here is an counter example:".c_red
+                            trace_s = result.trace.to_s.indented(str: "           >>  ".c_red)
                             puts trace_s + "\n"
                         end
                     }
@@ -146,7 +146,7 @@ def dcca()
 
                 models.each { |model|
                     Shell::LoadingPrompt.while_loading("Checking for deadlocks") {
-                        NuSMV::Runner.new().run_check!(model)
+                        NuSMV::Runner.new().run_check!(model); "ok"
                     }
 
                     dcca = Model::DCCA.new(model, NuSMV::Runner.new)
@@ -156,7 +156,8 @@ def dcca()
                     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 cut set#{s}:"
+                        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(', ')} }"
@@ -178,7 +179,7 @@ def simulate()
 
                 models.each { |model|
                     Shell::LoadingPrompt.while_loading("Checking for deadlocks") {
-                        NuSMV::Runner.new().run_check!(model)
+                        NuSMV::Runner.new().run_check!(model); "ok"
                     }
 
                     trace = Shell::LoadingPrompt.while_loading("Simulating model #{model.name.to_s.c_string}") {

lib/pg-verify/nusmv/runner.rb

@@ -119,6 +119,15 @@ def parse_trace(program_graph, nusmv_output)
                     next if key.nil? || val.nil?
                     current_var_state[key] = val
                 }
+                # Finish up
+                unless current_var_state.nil?
+                    missing_keys = var_states.empty? ? [] :  var_states[-1].keys - current_var_state.keys
+                    missing_keys.each { |key|
+                        current_var_state[key] = var_states[-1][key]
+                    }  
+                    var_states << current_var_state
+                end
+
                 return Model::Trace.new(program_graph, var_states)
             end
 

lib/pg-verify/transform/puml_transformation.rb

@@ -17,7 +17,7 @@ def transform_graph(graph, variable_state: nil, only: nil)
                 components = components.select { |c| only.map(&:to_s).include?(c.name.to_s) } unless only.nil?
 
                 parts = []
-                parts << components.map { |c| transform_component(graph, c) }.join("\n\n")
+                parts << components.map { |c| transform_component(graph, c, variable_state) }.join("\n\n")
                 parts << transform_variable_state(graph, variable_state) unless variable_state.nil?
                 parts = parts.compact.join("\n\n")
                 return "@startuml Programmgraph\n#{parts}\n@enduml\n"
@@ -31,14 +31,14 @@ def transform_variable_state(graph, variable_state)
                 }.join("\n")
             end
 
-            def transform_component(graph, component)
+            def transform_component(graph, component, variable_state)
                 # Transform component states
                 states_s  = component.states.map { |s| transform_state(component, s) }.join("\n")
                 # Transform component transitions
                 trans_s   = component.transitions.map { |t| transform_transition(component, t) }.join("\n")
                 # Transform component variables
                 vars = graph.variables.select_by_owner(component.name)
-                vars_s    = transform_variables(component, vars)
+                vars_s    = transform_variables(component, vars, variable_state)
                 # Transform the initial state 
                 initial_s = transform_initial(graph, component)
 
@@ -76,9 +76,12 @@ def indented(str)
                 str.split("\n").map { |s| "\t#{s}" }.join("\n")
             end
 
-            def transform_variables(component, variables)
-                return nil if variables.empty? 
-                body =  variables.map { |v| "#{v.name} => #{transform_range(v.range)}" }.join("\n")
+            def transform_variables(component, variables, variable_state)
+                return nil if variables.empty?
+                body =  variables.map { |var| 
+                    value = variable_state.nil? ? transform_range(v.range) : variable_state[var.name]
+                    "#{var.name} => #{value}"
+                }.join("\n")
                 return "map #{component.name}Variables {\n#{body}\n}"
             end