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