diff --git a/integration_tests/ruby_dsl/019_multiple_actions.rb b/integration_tests/ruby_dsl/019_multiple_actions.rb new file mode 100644 index 0000000..0b286c8 --- /dev/null +++ b/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 diff --git a/lib/pg-verify/nusmv/runner.rb b/lib/pg-verify/nusmv/runner.rb index 367fc90..cc38879 100644 --- a/lib/pg-verify/nusmv/runner.rb +++ b/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 = {}