This simple example walks you through a first test using QuickCheck's new module, eqc_fsm. You'll need QuickCheck version 1.16 (or later), and these two files: lock.erl and lock_eqc.erl--right-click on these links to download them.
lock.erl defines a simple API for storing keys and values, implemented as a gen_fsm, with operations to read, write, lock, and unlock, plus start and stop the server. Of course, writing is only allowed in the locked state... so we need to track the state during test-case generation, and ensure that we only write when the state is locked. Compile the file and test it:
22> lock:start().
{ok,<0.555.0>}
23> lock:read(a).
undefined
24> lock:lock().
ok
25> lock:write(a,42).
ok
26> lock:unlock().
ok
27> lock:read(a).
42
28> lock:stop().
ok
|
Using the new eqc_fsm library, all we have to do is specify each state by a function, whose result is a list of transitions from that state. Each transition is a pair of a target state, and a QuickCheck generator for a symbolic call. In this case, the locked and unlocked states are just defined by
unlocked(S) ->
read_transition(S) ++
[{locked,{call,lock,lock,[]}}].
locked(S) ->
read_transition(S) ++
[{unlocked,{call,lock,unlock,[]}},
{locked,{call,lock,write,[key(),value()]}}].
|
Notice that the read transition is possible in both states, but we avoid specifying it twice by placing the transition in a separate function.
read_transition(S) ->
[{history,{call,lock,read,[elements(proplists:get_keys(S))]}}].
|
The 'history' target state indicates that the read transition does not change the state--no matter what state it is embedded into. The parameter S is the state data--in this case the stored key-value list--which is independent of which named state we are currently in.
We still have to define the behaviour of the locker via other call-backs, similar to those used with eqc_statem--but they are simpler to define, because all the information about transitions between the named states is already represented in the few lines above. For example, we only have to define the effect of transitions on the state data:
next_state_data(_,_,S,_,{call,_,write,[Key,Value]}) ->
[{Key,Value}|proplists:delete(Key,S)];
next_state_data(_,_,S,_,{call,_,_,_}) ->
S.
|
This, and other definitions, can be found in lock_eqc.erl... but for now, just compile it and run some tests (if this fails, you're probably running an old version of QuickCheck):
29> c(lock_eqc).
{ok,lock_eqc}
30> eqc:quickcheck(lock_eqc:prop_locker()).
....................................................................................................
OK, passed 100 tests
25% {unlocked,{lock,lock,0}}
22% {locked,{lock,write,2}}
20% {locked,{lock,unlock,0}}
17% {locked,{lock,read,1}}
14% {unlocked,{lock,read,1}}
true
|
The property we're testing here looks just like an eqc_statem property, but in addition collects the distribution of transitions in the tests--hence the useful output above.
prop_locker() ->
?FORALL(Cmds,commands(lock_eqc),
begin
lock:start(),
{H,_S,Res} = run_commands(lock_eqc,Cmds),
lock:stop(),
aggregate(zip(state_names(H),command_names(Cmds)),
Res == ok)
end).
|
Not satisfied with the distribution above? The read transitions seem to be tested a little rarely compared to the others. Let QuickCheck weight your transitions for you:
31> eqc_fsm:automate_weights(lock_eqc).
============================================================
weight(locked,locked,{call,lock,read,[_]}) -> 2;
weight(locked,locked,{call,lock,write,[_,_]}) -> 1;
weight(locked,unlocked,{call,lock,unlock,[]}) -> 1;
weight(unlocked,locked,{call,lock,lock,[]}) -> 1;
weight(unlocked,unlocked,{call,lock,read,[_]}) -> 2.
============================================================
Running dot -Tjpg lock_eqc.dot -olock_eqc.jpg (set EQC_DOT to change)
Running lock_eqc.jpg (set EQC_VIEWER to change)
<0.681.0>
|
Copy the generated function definition into lock_eqc, compile and test again, and you'll see a much better result. If you have GraphViz installed (and a few environment variables correctly set), then QuickCheck will not only calculate suitable weights for you, but display a visualization of the result:
Much better!
Now why not study the new features in more detail? The examples folder in your eqc distribution contains an extended version of this very example, covering more of the details, and introducing a little more functionality. Once you've read that, you'll be ready for the manual pages!