The counter should generally be part of the API as well for simple property tests. However property tests are not just about reverse testing but about invariant testing, like have it generate inputs into a state system, test that the state of it is valid each time and make sure it ends at a proper place given the inputs, even without knowing the values you catch a significant amount of bugs.
As a good example of state testing see the Elevator example for the C side of the QuickCheck library (which uses Erlang to do the testing) for how to think about it. 
