In both get_lock() and get_token(), there is an issue of incorrectly counting the current number of given resources after crashing the bg-mgr and restarting it. Here is a traceback that is similar to tokens as well...


bg_manager_eqc:start_process() -> <0.12345.0>
bg_manager_eqc:start_process() -> <0.12346.0>
bg_manager_eqc:set_concurrency_limit(b, 2, false) -> 0
bg_manager_eqc:get_lock(b, <0.12345.0>, []) -> #Ref<0.0.0.43163>
bg_manager_eqc:get_lock(b, <0.12346.0>, []) -> #Ref<0.0.0.43165>
bg_manager_eqc:crash() -> ok
bg_manager_eqc:revive() -> true
bg_manager_eqc:get_lock(b, <0.12346.0>, []) -> #Ref<0.0.0.43172>

Reason: {postcondition, {2, 'not <', 2}}
false