Convert Tests to Use Cases

[crisdut]

Today, all tests written in BMC adopt "functional style"; that is, the focus is on testing functionality isolate. However, this approach needs to reflect the real-world usages.

So I suggest that the tests adopt use cases, such as "Alice needs to transfer one or more UDAs to Bob", and going through stressful scenarios too like "Bob tries to send a fraudulent consig to Alice".

We can start the test files with a brief description of the use case, and the tests in this file need reflect the description. We can even open issues with the "use case" tag describing a usage scenario so any contributor feels encouraged to contribute to the project.