Component A makes requests, and Component B responds. Although the (commented out) assumption on Component B should be valid, uncommenting it results in nearly all guarantees showing invalid. There is co-dependence between the two components, but it is reasonable. I defer to the models to justify that point. It would be nice if we could support this and deem this kind of co-dependence as valid. I realize that might not be easy and maybe not even doable. But I've run into this kind of behavior/issue more than once, and as a result I've had to remove assumptions that I think are reasonable and worth checking.
I've pushed an example of a simple system with two components. It is available here:
https://github.com/loonwerks/formal-methods-workbench/tree/master/models/agree/co-dependence
Component A makes requests, and Component B responds. Although the (commented out) assumption on Component B should be valid, uncommenting it results in nearly all guarantees showing invalid. There is co-dependence between the two components, but it is reasonable. I defer to the models to justify that point. It would be nice if we could support this and deem this kind of co-dependence as valid. I realize that might not be easy and maybe not even doable. But I've run into this kind of behavior/issue more than once, and as a result I've had to remove assumptions that I think are reasonable and worth checking.