| ... | ... | @@ -50,7 +50,7 @@ controller ||C = (Plant)~{Spec}. |
|
|
|
|
|
|
|
|
|
|
|
# Compatibility
|
|
|
|
To check if the assumptions in a controller specification are compatible (i.e., the environment can achieve the assumptions for any controller), which is diserable (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)
|
|
|
|
To check if the assumptions in a controller specification are compatible (i.e., the environment can achieve the assumptions for any controller), which is diserable (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))
|
|
|
|
|
|
|
|
```
|
|
|
|
checkCompatibility ||Compatible = (Plant)~{Spec}.
|
| ... | ... | |