Consider the following scenario:
The app developer creates a model which accurately models a faulty system. Checking invariants against the model creates traces that violate the invariants, and concrete executions generated from the traces indeed crash the running system.
A possible strategy from the developer is to correct the model and the code and then archive the old incorrect model, while steel keeping around the tests generated from the traces of the incorrect model, as regression tests.
The above story should be explained in some kind of guide, and our tooling should support the story by adding helpful features, e.g. linking generated tests to particular models, particular commits, ect.
Consider the following scenario:
The app developer creates a model which accurately models a faulty system. Checking invariants against the model creates traces that violate the invariants, and concrete executions generated from the traces indeed crash the running system.
A possible strategy from the developer is to correct the model and the code and then archive the old incorrect model, while steel keeping around the tests generated from the traces of the incorrect model, as regression tests.
The above story should be explained in some kind of guide, and our tooling should support the story by adding helpful features, e.g. linking generated tests to particular models, particular commits, ect.