PLCgen: use 'while' loop bounds calculated by controller checker in generated PLC code

In the controller checker, we will compute 'while' loop bounds, separately for uncontrollable events and controllable events. Add we will have the controller checker add them to the model as an annotation. See #621.

Once that is done, PLCgen should read the annotation and use them to determine the 'while' loop bounds.

Changes to do:

• Give warnings if the input model does not have bounded response or confluence properties in the annotation. Indicate the the CIF controller properties checker should be used before generating code. Do not warn for finite response, as that is replaced by bounded response.
• Give warnings if the input model has bounded response, confluence, or finite response properties in the annotation, but they don't hold or may not hold. Indicate that the control code may not perform as desired/expected. If the finite response property is present, it should still be checked and warned about.
• Add a default option value to the PLC maximum iterations option. It uses the bounds from the annotation in the model, if present. Otherwise it defaults to inf,inf as before. Users can still override the value of the option as before.

Addresses #679.