Error: Temporal properties were violated.

Error: The following behavior constitutes a counter-example:

State 1: <Initial predicate>
/\ TURN = <<1, 1>>
/\ Q = <<0, 0, 0>>
/\ j = <<defaultInitValue, defaultInitValue, defaultInitValue>>
/\ pc = <<"init", "init", "init">>

State 2: <Action line 46, col 15 to line 49, col 40 of module Petterson>
/\ TURN = <<1, 1>>
/\ Q = <<0, 0, 0>>
/\ j = <<1, defaultInitValue, defaultInitValue>>
/\ pc = <<"want", "init", "init">>

State 3: <Action line 51, col 15 to line 58, col 23 of module Petterson>
/\ TURN = <<1, 1>>
/\ Q = <<1, 0, 0>>
/\ j = <<1, defaultInitValue, defaultInitValue>>
/\ pc = <<"wait", "init", "init">>

State 4: <Action line 60, col 15 to line 67, col 40 of module Petterson>
/\ TURN = <<1, 1>>
/\ Q = <<1, 0, 0>>
/\ j = <<2, defaultInitValue, defaultInitValue>>
/\ pc = <<"want", "init", "init">>

State 5: <Action line 51, col 15 to line 58, col 23 of module Petterson>
/\ TURN = <<1, 1>>
/\ Q = <<2, 0, 0>>
/\ j = <<2, defaultInitValue, defaultInitValue>>
/\ pc = <<"wait", "init", "init">>

State 6: <Action line 60, col 15 to line 67, col 40 of module Petterson>
/\ TURN = <<1, 1>>
/\ Q = <<2, 0, 0>>
/\ j = <<3, defaultInitValue, defaultInitValue>>
/\ pc = <<"want", "init", "init">>

State 7: <Action line 51, col 15 to line 58, col 23 of module Petterson>
/\ TURN = <<1, 1>>
/\ Q = <<2, 0, 0>>
/\ j = <<3, defaultInitValue, defaultInitValue>>
/\ pc = <<"critical", "init", "init">>

State 8: <Action line 69, col 19 to line 75, col 44 of module Petterson>
/\ TURN = <<1, 1>>
/\ Q = <<0, 0, 0>>
/\ j = <<3, defaultInitValue, defaultInitValue>>
/\ pc = <<"Done", "init", "init">>

State 9: <Action line 46, col 15 to line 49, col 40 of module Petterson>
/\ TURN = <<1, 1>>
/\ Q = <<0, 0, 0>>
/\ j = <<3, 1, defaultInitValue>>
/\ pc = <<"Done", "want", "init">>

State 10: <Action line 46, col 15 to line 49, col 40 of module Petterson>
/\ TURN = <<1, 1>>
/\ Q = <<0, 0, 0>>
/\ j = <<3, 1, 1>>
/\ pc = <<"Done", "want", "want">>

State 11: <Action line 51, col 15 to line 58, col 23 of module Petterson>
/\ TURN = <<3, 1>>
/\ Q = <<0, 0, 1>>
/\ j = <<3, 1, 1>>
/\ pc = <<"Done", "want", "wait">>

State 12: <Action line 51, col 15 to line 58, col 23 of module Petterson>
/\ TURN = <<2, 1>>
/\ Q = <<0, 1, 1>>
/\ j = <<3, 1, 1>>
/\ pc = <<"Done", "wait", "wait">>

State 13: <Action line 60, col 15 to line 67, col 40 of module Petterson>
/\ TURN = <<2, 1>>
/\ Q = <<0, 1, 1>>
/\ j = <<3, 1, 2>>
/\ pc = <<"Done", "wait", "want">>

State 14: <Action line 51, col 15 to line 58, col 23 of module Petterson>
/\ TURN = <<2, 3>>
/\ Q = <<0, 1, 2>>
/\ j = <<3, 1, 2>>
/\ pc = <<"Done", "wait", "wait">>

State 15: <Action line 60, col 15 to line 67, col 40 of module Petterson>
/\ TURN = <<2, 3>>
/\ Q = <<0, 1, 2>>
/\ j = <<3, 1, 3>>
/\ pc = <<"Done", "wait", "want">>

State 16: <Action line 51, col 15 to line 58, col 23 of module Petterson>
/\ TURN = <<2, 3>>
/\ Q = <<0, 1, 2>>
/\ j = <<3, 1, 3>>
/\ pc = <<"Done", "wait", "critical">>

State 17: <Action line 69, col 19 to line 75, col 44 of module Petterson>
/\ TURN = <<2, 3>>
/\ Q = <<0, 1, 0>>
/\ j = <<3, 1, 3>>
/\ pc = <<"Done", "wait", "Done">>

State 18: <Action line 60, col 15 to line 67, col 40 of module Petterson>
/\ TURN = <<2, 3>>
/\ Q = <<0, 1, 0>>
/\ j = <<3, 2, 3>>
/\ pc = <<"Done", "want", "Done">>

State 19: <Action line 51, col 15 to line 58, col 23 of module Petterson>
/\ TURN = <<2, 2>>
/\ Q = <<0, 2, 0>>
/\ j = <<3, 2, 3>>
/\ pc = <<"Done", "wait", "Done">>

State 20: <Action line 60, col 15 to line 67, col 40 of module Petterson>
/\ TURN = <<2, 2>>
/\ Q = <<0, 2, 0>>
/\ j = <<3, 3, 3>>
/\ pc = <<"Done", "want", "Done">>

State 21: <Action line 51, col 15 to line 58, col 23 of module Petterson>
/\ TURN = <<2, 2>>
/\ Q = <<0, 2, 0>>
/\ j = <<3, 3, 3>>
/\ pc = <<"Done", "critical", "Done">>

State 22: <Action line 69, col 19 to line 75, col 44 of module Petterson>
/\ TURN = <<2, 2>>
/\ Q = <<0, 0, 0>>
/\ j = <<3, 3, 3>>
/\ pc = <<"Done", "init", "Done">>

State 23: <Action line 46, col 15 to line 49, col 40 of module Petterson>
/\ TURN = <<2, 2>>
/\ Q = <<0, 0, 0>>
/\ j = <<3, 1, 3>>
/\ pc = <<"Done", "want", "Done">>

State 24: <Action line 51, col 15 to line 58, col 23 of module Petterson>
/\ TURN = <<2, 2>>
/\ Q = <<0, 1, 0>>
/\ j = <<3, 1, 3>>
/\ pc = <<"Done", "wait", "Done">>

State 25: <Action line 60, col 15 to line 67, col 40 of module Petterson>
/\ TURN = <<2, 2>>
/\ Q = <<0, 1, 0>>
/\ j = <<3, 2, 3>>
/\ pc = <<"Done", "want", "Done">>

State 26: <Action line 51, col 15 to line 58, col 23 of module Petterson>
/\ TURN = <<2, 2>>
/\ Q = <<0, 2, 0>>
/\ j = <<3, 2, 3>>
/\ pc = <<"Done", "wait", "Done">>

Back to state 19.

2230 states generated, 838 distinct states found, 0 states left on queue.
Finished. (2012-12-20 12:31:33)