State Space analysis
Between two handle_call(request,_,_) there should be a
handle_call(release,_,_).
[-*,“handle_call(request,_,_)”,
(not “handle_call(release,_,_)”)*,
“handle_call(request,_,_)” ]false
Properties are specified as regular expressions over
Erlang function calls in combination with [] and <> operators.
After a gen_server:call(locker, request) there is always a
gen_server:call(locker,release) possible.
[-*,“gen_server:call(locker, request)”]
< -*,“gen_server:call(locker, request)”>true