|
|
|
MTSA supports a synthesising behaviour models that control a given plant to satisfy a given property. The plant is defined using an FSP composite process. The property is defined using the controllerSpec keyword.
|
|
|
|
|
|
|
|
|
|
|
|
```
|
|
|
|
controller ||CONTROLLER = (PLANT)~{SPECIFICATIONS}.
|
|
|
|
```
|
|
|
|
|
|
|
|
# GR1
|
|
|
|
|
|
|
|
For GR1 controller synthesis specification includes various items
|
| ... | ... | |
