Add integration test for multiple actions and fix deadock detection

integration_tests/ruby_dsl/019_multiple_actions.rb

@@ -0,0 +1,21 @@
+model :MultipleActions do
+
+    graph :GraphWithMultipleActions do
+        states :one, :two, init: :one
+
+        var a: (0..10), init: 0
+        var b: (0..10), init: 0
+        var c: (0..10), init: 0
+
+        transition :one => :two do
+           action "a := 1 + 1 | b := 0 | c := 25 - (2 * 10)"
+        end
+    end
+
+    specify "The graph" do
+        it "set a = 2" => :"X a == 2"
+        it "set b = 0" => :"X b == 0"
+        it "set c = 5" => :"X c == 5"
+    end
+
+end

lib/pg-verify/nusmv/runner.rb

@@ -66,14 +66,17 @@ def run_check!(program_graph)
 
             def run_check(program_graph)
                 commands = [ "go", "check_fsm", "quit" ]
-                nusmv_s = Transform::NuSmvTransformation.new.transform_graph(program_graph)
+                nusmv_s = Transform::NuSmvTransformation.new.transform_graph(program_graph, include_specs: false)
                 output = eval_nusmv(nusmv_s, commands: commands)
 
                 # Return "ok" if the FSM has no deadlocks
                 return nil if output.include?("The transition relation is total: No deadlock state exists")
 
                 # Otherwise compute and return the deadlock state
-                lines = output.split("\n").drop_while { |str| !str.start_with?("A deadlock state is:") }
+                lines = output.split("\n").drop_while { |str| 
+                    !(str.start_with?("A deadlock state is:") || str.start_with?("successors is:"))
+                }
+                lines = output.split("\n").drop_while { |str| !str.start_with?("A deadlock state is:") } if lines.empty?
                 lines = lines[1, lines.length - 1]
 
                 var_state = {}