Making progressing on MBT

I've started implementing a model based testing framework for my project. The model I used is a finite state machine. The main structure is:
Each page of the web application represents a state and the links and buttons are the actions that lead to other states. The internal states in the server side are implemented as constraints. To generate test cases, just traverse through the state machine, randomize the order of traversing through each branch from a given node.
I've started with a simple model that contains around 10% of the features of the SUT with 6 states and 10 actions, 1 constraint. But I can already generate thousands of the test cases from it. I'm running one thousand of them tonight. I don't expect them to find any subtle bugs yet because the model they are based on is still very simplistic. The exciting thing is I was thinking about how to extend the model to enable the generation of more subtle test cases on my way home. Exactly as Harry Robinson said, test engineers don't enjoy writing test code, they enjoy thinking devious thoughts. It's exciting to think about what kind of test cases the tool will generate when I gradually add my knowledge about the application to the model. Also I know the knowledge is conveyed in a more abstract way than test scripts, and stored in a single place. No application specific details is repeated. This means much less maintenance cost than writing test scripts.
However, it's not all good news. One thing I realised is that MBT is not going to cover all the testing I want in the project. For example, details like numbers, text, layout are difficult to test with MBT, because the abstract model only contains the keyword of each page that are just enough to identify the page and the actions. Another problem is it's not easy to tell what has been tested because the large number of test cases are not really readable. I guess code coverage analysis can compensate this a bit, but not completely.
Will continue with this work and report here again!