cycle1: [guard1,1] Po -enum< P1 >conc= P2

In cycle1 guard1,1 specifies if the problem set P2 is empty then control is transferred to cycle1. In other words if cycle1 produces no solutions then M_sis should switch back to cycle1. The initial problem P0 is reset to P1. If P2 is non-empty then M_sis halts.

---

Customization: The Continuous Diabetes Meter cgm is the enumerator enum that keeps on producing blood sugar measurements.

The Alert App on the smart phone is the concentrator conc that uses a threshold to detect high (or low) blood sugar level.

With the above customization, the computation cycle can be rewritten as:

cycle1: [guard1,1] Po -cgm< P1 >alert= P2