|
|
# Using Directed Controller Synthesis
|
|
|
|
|
|
To use this part of the project, the keyword `heuristic` must be used at the moment of the composition of the `controllerSpec`
|
|
|
|
|
|
# Modes
|
|
|
|
|
|
You can solve various different problems with DCS, including:
|
|
|
|
|
|
1)-NonBlocking requirements for a set of marked states
|
|
|
2)-Blocking requirements for a set of marked states
|
|
|
3)-LTL properties of the form []<>(F1 ^ .. ^ Fn V Fn+1 .. V Fm) where each Fi is a Fluent
|
|
|
|
|
|
-Full GR1 solving is on the works |