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

---

← End User