|
|
For GR1 specifications, to check if the assumptions are compatible (i.e., the environment can achieve the assumptions for any controller), which is desirable (see Nicolás Roque D'Ippolito, Victor Braberman, Nir Piterman, and Sebastián Uchitel. 2010. Synthesis of live behaviour models. In Proceedings of the eighteenth ACM SIGSOFT international symposium on Foundations of software engineering (FSE '10). Association for Computing Machinery, New York, NY, USA, 77–86. [pdf](https://doi.org/10.1145/1882291.1882305))
|
|
For GR1 specifications, to check if the assumptions are compatible (i.e., the environment can achieve the assumptions for any controller), which is desirable (see Nicolás Roque D'Ippolito, Victor Braberman, Nir Piterman, and Sebastián Uchitel. 2010. Synthesis of live behaviour models. In Proceedings of the eighteenth ACM SIGSOFT international symposium on Foundations of software engineering (FSE '10). Association for Computing Machinery, New York, NY, USA, 77–86. [pdf](https://doi.org/10.1145/1882291.1882305))
|