THE INPUT FORMULA
The specification is:
{L0}:[-1]:E_ICP_I50FC_SENSOR(i) -2 < [-1]:S_ICP_I50FC_SENSOR(i)
{L1}:[-1]:E_FCP_I50FC(i) -1 < [-1]:S_FCP_I50FC(i)
{L2}:[-1]:E_FCP_P50FC(i) -5 < [-1]:S_FCP_P50FC(i)
{L3}:[-1]:E_FCP_O50FC(i) -1 < [-1]:S_FCP_O50(i)
{L4}:[-1]:E_ICP_I50FC_CMDS(i) -1 < [-1]:S_ICP_I50FC_CMDS(i)
{L5}:[-1]:E_ICP_I10FC_SENSOR(i) -2 < [-1]:S_ICP_I10FC_SENSOR(i)
{L6}:[-1]:E_FCP_I10FC(i) -1 < [-1]:S_FCP_I10FC(i)
{L7}:[-1]:E_FCP_P10FC(i) -40 < [-1]:S_FCP_P10FC(i)
{L8}:[-1]:E_FCP_O10FC(i) -1 < [-1]:S_FCP_O10FC(i)
{L9}:[-1]:E_ICP_I10FC_CMDS(i) -1 < [-1]:S_ICP_I10FC_CMDS(i)
{L10}:[-1]:E_ICP_I50NFC_SENSOR(i) -5 < [-1]:S_ICP_I50NFC_SENSOR(i)
{L11}:[-1]:E_FCP_I50NFC(i) -1 < [-1]:S_FCP_I50NFC(i)
{L12}:[-1]:E_FCP_P50NFC(i) -2 < [-1]:S_FCP_P50NFC(i)
{L13}:[-1]:S_ICP_I50FC_SENSOR(i) +0 < [-1]:E_ICP_I50FC_SENSOR(i)
{L14}:[-1]:S_FCP_I50FC(i) +0 < [-1]:E_FCP_I50FC(i)
{L15}:[-1]:S_FCP_P50FC(i) +0 < [-1]:E_FCP_P50FC(i)
{L16}:[-1]:S_FCP_O50FC(i) +0 < [-1]:E_FCP_O50FC(i)
{L17}:[-1]:S_ICP_I50FC_CMDS(i) +0 < [-1]:E_ICP_I50FC_CMDS(i)
{L18}:[-1]:S_ICP_I10FC_SENSOR(i) +0 < [-1]:E_ICP_I10FC_SENSOR(i)
{L19}:[-1]:S_FCP_I10FC(i) +0 < [-1]:E_FCP_I10FC(i)
{L20}:[-1]:S_FCP_P10FC(i) +0 < [-1]:E_FCP_P10FC(i)
{L21}:[-1]:S_FCP_O10FC(i) +0 < [-1]:E_FCP_O10FC(i)
{L22}:[-1]:S_ICP_I10FC_CMDS(i) +0 < [-1]:E_ICP_I10FC_CMDS(i)
{L23}:[-1]:S_ICP_I50NFC_SENSOR(i) +0 < [-1]:E_ICP_I50NFC_SENSOR(i)
{L24}:[-1]:S_FCP_I50NFC(i) +0 < [-1]:E_FCP_I50NFC(i)
{L25}:[-1]:S_FCP_P50NFC(i) +0 < [-1]:E_FCP_P50NFC(i)
{L26}:[-1]:E_ICP_I50FC_SENSOR(i) +0 < [-1]:S_FCP_I50FC(i)
{L27}:[-1]:E_FCP_I50FC(i) +0 < [-1]:S_FCP_P50FC(i)
{L28}:[-1]:E_FCP_P50FC(i) +0 < [-1]:S_FCP_O50FC(i)
{L29}:[-1]:E_FCP_O50FC(i) +0 < [-1]:S_FCP_I50FC_CMDS(i)
{L30}:[-1]:E_ICP_I10FC_SENSOR(i) +0 < [-1]:S_FCP_I10FC(i)
{L31}:[-1]:E_FCP_I10FC(i) +0 < [-1]:S_FCP_P10FC(i)
{L32}:[-1]:E_FCP_P10FC(i) +0 < [-1]:S_FCP_O10FC(i)
{L33}:[-1]:E_FCP_O10FC(i) +0 < [-1]:S_FCP_I10FC_CMDS(i)
{L34}:[-1]:E_ICP_I50NFC_SENSOR(i) +0 < [-1]:S_FCP_I50NFC(i)
{L35}:[-1]:E_FCP_I50NFC(i) +0 < [-1]:S_FCP_P50NFC(i)
{L36}:[-1]:S_FCP_I50FC(i) -2 < [-1]:S_ICP_I50FC_SENSOR(i)
{L37}:[-1]:S_FCP_P50FC(i) -1 < [-1]:S_FCP_I50FC(i)
{L38}:[-1]:S_FCP_O50FC(i) -5 < [-1]:S_FCP_P50FC(i)
{L39}:[-1]:S_ICP_I50FC_CMDS(i) -1 < [-1]:S_FCP_O50FC(i)
{L40}:[-1]:S_FCP_I10FC(i) -2 < [-1]:S_ICP_I10FC_SENSOR(i)
{L41}:[-1]:S_FCP_P10FC(i) -1 < [-1]:S_FCP_I10FC(i)
{L42}:[-1]:S_FCP_O10FC(i) -40 < [-1]:S_FCP_P10FC(i)
{L43}:[-1]:S_ICP_I10FC_CMDS(i) -1 < [-1]:S_FCP_O10FC(i)
{L44}:[-1]:S_FCP_I50NFC(i) -2 < [-1]:S_ICP_I50NFC_SENSOR(i)
{L45}:[-1]:S_FCP_P50NFC(i) -1 < [-1]:S_FCP_I50NFC(i)
{L46}:[-1]:S_ICP_I50FC_SENSOR(i) +20 < [-1]:S_ICP_I50FC_SENSOR(i+1)
{L47}:[-1]:S_FCP_I50FC(i) +20 < [-1]:S_FCP_I50FC(i+1)
{L48}:[-1]:S_FCP_P50FC(i) +20 < [-1]:S_FCP_P50FC(i+1)
{L49}:[-1]:S_FCP_O50FC(i) +20 < [-1]:S_FCP_O50FC(i+1)
{L50}:[-1]:S_ICP_I50FC_CMDS(i) +20 < [-1]:S_ICP_I50FC_CMDS(i+1)
{L51}:[-1]:S_ICP_I50FC_SENSOR(i+1) -20 < [-1]:S_ICP_I50FC_SENSOR(i)
{L52}:[-1]:S_FCP_I50FC(i+1) -20 < [-1]:S_FCP_I50FC(i)
{L53}:[-1]:S_FCP_P50FC(i+1) -20 < [-1]:S_FCP_P50FC(i)
{L54}:[-1]:S_FCP_O50FC(i+1) -20 < [-1]:S_FCP_O50FC(i)
{L55}:[-1]:S_ICP_I50FC_CMDS(i+1) -20 < [-1]:S_ICP_I50FC_CMDS(i)
{L56}:[-1]:S_ICP_I10FC_SENSOR(i) +100 < [-1]:S_ICP_I10FC_SENSOR(i+1)
{L57}:[-1]:S_FCP_I10FC(i) +100 < [-1]:S_FCP_I10FC(i+1)
{L58}:[-1]:S_FCP_P10FC(i) +100 < [-1]:S_FCP_P10FC(i+1)
{L59}:[-1]:S_FCP_O10FC(i) +100 < [-1]:S_FCP_O10FC(i+1)
{L60}:[-1]:S_ICP_I10FC_CMDS(i) +100 < [-1]:S_ICP_I10FC_CMDS(i+1)
{L61}:[-1]:S_ICP_I10FC_SENSOR(i+1) -100 < [-1]:S_ICP_I10FC_SENSOR(i)
{L62}:[-1]:S_FCP_I10FC(i+1) -100 < [-1]:S_FCP_I10FC(i)
{L63}:[-1]:S_FCP_P10FC(i+1) -100 < [-1]:S_FCP_P10FC(i)
{L64}:[-1]:S_FCP_O10FC(i+1) -100 < [-1]:S_FCP_O10FC(i)
{L65}:[-1]:S_ICP_I10FC_CMDS(i+1) -100 < [-1]:S_ICP_I10FC_CMDS(i)
{L66}:[-1]:S_ICP_I50NFC_SENSOR(i) +20 < [-1]:S_ICP_I50NFC_SENSOR(i+1)
{L67}:[-1]:S_FCP_I50NFC(i) +20 < [-1]:S_FCP_I50NFC(i+1)
{L68}:[-1]:S_FCP_P50NFC(i) +20 < [-1]:S_FCP_P50NFC(i+1)
{L69}:[-1]:S_ICP_I50NFC_SENSOR(i+1) -20 < [-1]:S_ICP_I50NFC_SENSOR(i)
{L70}:[-1]:S_FCP_I50NFC(i+1) -20 < [-1]:S_FCP_I50NFC(i)
{L71}:[-1]:S_FCP_P50NFC(i+1) -20 < [-1]:S_FCP_P50NFC(i)
{L72}:[-1]:E_FCP_I50FC(i) +0 < [-1]:S_FCP_I10FC(i)
{L73}:[-1]:E_FCP_I50FC(i) +0 < [-1]:S_FCP_I50NFC(i)
The safety assertion is:
{L74}:[-1]:S_ICP_I50FC_SENSOR(I) +11 < [-1]:E_ICP_I50FC_CMDS(I) OR {L75}:[-1]:S_ICP_I10FC_SENSOR(I) +51 < [-1]:E_ICP_I10FC_CMDS(I)

THE UNOPTIMIZED FORMULA
The specification is:
{L0}:[0]:E_ICP_I50FC_SENSOR(i) -2 < [1]:S_ICP_I50FC_SENSOR(i)
{L1}:[2]:E_FCP_I50FC(i) -1 < [3]:S_FCP_I50FC(i)
{L2}:[4]:E_FCP_P50FC(i) -5 < [5]:S_FCP_P50FC(i)
{L3}:[6]:E_FCP_O50FC(i) -1 < [7]:S_FCP_O50(i)
{L4}:[8]:E_ICP_I50FC_CMDS(i) -1 < [9]:S_ICP_I50FC_CMDS(i)
{L5}:[10]:E_ICP_I10FC_SENSOR(i) -2 < [11]:S_ICP_I10FC_SENSOR(i)
{L6}:[12]:E_FCP_I10FC(i) -1 < [13]:S_FCP_I10FC(i)
{L7}:[14]:E_FCP_P10FC(i) -40 < [15]:S_FCP_P10FC(i)
{L8}:[16]:E_FCP_O10FC(i) -1 < [17]:S_FCP_O10FC(i)
{L9}:[18]:E_ICP_I10FC_CMDS(i) -1 < [19]:S_ICP_I10FC_CMDS(i)
{L10}:[20]:E_ICP_I50NFC_SENSOR(i) -5 < [21]:S_ICP_I50NFC_SENSOR(i)
{L11}:[22]:E_FCP_I50NFC(i) -1 < [23]:S_FCP_I50NFC(i)
{L12}:[24]:E_FCP_P50NFC(i) -2 < [25]:S_FCP_P50NFC(i)
{L13}:[1]:S_ICP_I50FC_SENSOR(i) +0 < [0]:E_ICP_I50FC_SENSOR(i)
{L14}:[3]:S_FCP_I50FC(i) +0 < [2]:E_FCP_I50FC(i)
{L15}:[5]:S_FCP_P50FC(i) +0 < [4]:E_FCP_P50FC(i)
{L16}:[26]:S_FCP_O50FC(i) +0 < [6]:E_FCP_O50FC(i)
{L17}:[9]:S_ICP_I50FC_CMDS(i) +0 < [8]:E_ICP_I50FC_CMDS(i)
{L18}:[11]:S_ICP_I10FC_SENSOR(i) +0 < [10]:E_ICP_I10FC_SENSOR(i)
{L19}:[13]:S_FCP_I10FC(i) +0 < [12]:E_FCP_I10FC(i)
{L20}:[15]:S_FCP_P10FC(i) +0 < [14]:E_FCP_P10FC(i)
{L21}:[17]:S_FCP_O10FC(i) +0 < [16]:E_FCP_O10FC(i)
{L22}:[19]:S_ICP_I10FC_CMDS(i) +0 < [18]:E_ICP_I10FC_CMDS(i)
{L23}:[21]:S_ICP_I50NFC_SENSOR(i) +0 < [20]:E_ICP_I50NFC_SENSOR(i)
{L24}:[23]:S_FCP_I50NFC(i) +0 < [22]:E_FCP_I50NFC(i)
{L25}:[25]:S_FCP_P50NFC(i) +0 < [24]:E_FCP_P50NFC(i)
{L26}:[0]:E_ICP_I50FC_SENSOR(i) +0 < [3]:S_FCP_I50FC(i)
{L27}:[2]:E_FCP_I50FC(i) +0 < [5]:S_FCP_P50FC(i)
{L28}:[4]:E_FCP_P50FC(i) +0 < [26]:S_FCP_O50FC(i)
{L29}:[6]:E_FCP_O50FC(i) +0 < [27]:S_FCP_I50FC_CMDS(i)
{L30}:[10]:E_ICP_I10FC_SENSOR(i) +0 < [13]:S_FCP_I10FC(i)
{L31}:[12]:E_FCP_I10FC(i) +0 < [15]:S_FCP_P10FC(i)
{L32}:[14]:E_FCP_P10FC(i) +0 < [17]:S_FCP_O10FC(i)
{L33}:[16]:E_FCP_O10FC(i) +0 < [28]:S_FCP_I10FC_CMDS(i)
{L34}:[20]:E_ICP_I50NFC_SENSOR(i) +0 < [23]:S_FCP_I50NFC(i)
{L35}:[22]:E_FCP_I50NFC(i) +0 < [25]:S_FCP_P50NFC(i)
{L36}:[3]:S_FCP_I50FC(i) -2 < [1]:S_ICP_I50FC_SENSOR(i)
{L37}:[5]:S_FCP_P50FC(i) -1 < [3]:S_FCP_I50FC(i)
{L38}:[26]:S_FCP_O50FC(i) -5 < [5]:S_FCP_P50FC(i)
{L39}:[9]:S_ICP_I50FC_CMDS(i) -1 < [26]:S_FCP_O50FC(i)
{L40}:[13]:S_FCP_I10FC(i) -2 < [11]:S_ICP_I10FC_SENSOR(i)
{L41}:[15]:S_FCP_P10FC(i) -1 < [13]:S_FCP_I10FC(i)
{L42}:[17]:S_FCP_O10FC(i) -40 < [15]:S_FCP_P10FC(i)
{L43}:[19]:S_ICP_I10FC_CMDS(i) -1 < [17]:S_FCP_O10FC(i)
{L44}:[23]:S_FCP_I50NFC(i) -2 < [21]:S_ICP_I50NFC_SENSOR(i)
{L45}:[25]:S_FCP_P50NFC(i) -1 < [23]:S_FCP_I50NFC(i)
{L46}:[1]:S_ICP_I50FC_SENSOR(i) +20 < [29]:S_ICP_I50FC_SENSOR(i+1)
{L47}:[3]:S_FCP_I50FC(i) +20 < [30]:S_FCP_I50FC(i+1)
{L48}:[5]:S_FCP_P50FC(i) +20 < [31]:S_FCP_P50FC(i+1)
{L49}:[26]:S_FCP_O50FC(i) +20 < [32]:S_FCP_O50FC(i+1)
{L50}:[9]:S_ICP_I50FC_CMDS(i) +20 < [33]:S_ICP_I50FC_CMDS(i+1)
{L51}:[29]:S_ICP_I50FC_SENSOR(i+1) -20 < [1]:S_ICP_I50FC_SENSOR(i)
{L52}:[30]:S_FCP_I50FC(i+1) -20 < [3]:S_FCP_I50FC(i)
{L53}:[31]:S_FCP_P50FC(i+1) -20 < [5]:S_FCP_P50FC(i)
{L54}:[32]:S_FCP_O50FC(i+1) -20 < [26]:S_FCP_O50FC(i)
{L55}:[33]:S_ICP_I50FC_CMDS(i+1) -20 < [9]:S_ICP_I50FC_CMDS(i)
{L56}:[11]:S_ICP_I10FC_SENSOR(i) +100 < [34]:S_ICP_I10FC_SENSOR(i+1)
{L57}:[13]:S_FCP_I10FC(i) +100 < [35]:S_FCP_I10FC(i+1)
{L58}:[15]:S_FCP_P10FC(i) +100 < [36]:S_FCP_P10FC(i+1)
{L59}:[17]:S_FCP_O10FC(i) +100 < [37]:S_FCP_O10FC(i+1)
{L60}:[19]:S_ICP_I10FC_CMDS(i) +100 < [38]:S_ICP_I10FC_CMDS(i+1)
{L61}:[34]:S_ICP_I10FC_SENSOR(i+1) -100 < [11]:S_ICP_I10FC_SENSOR(i)
{L62}:[35]:S_FCP_I10FC(i+1) -100 < [13]:S_FCP_I10FC(i)
{L63}:[36]:S_FCP_P10FC(i+1) -100 < [15]:S_FCP_P10FC(i)
{L64}:[37]:S_FCP_O10FC(i+1) -100 < [17]:S_FCP_O10FC(i)
{L65}:[38]:S_ICP_I10FC_CMDS(i+1) -100 < [19]:S_ICP_I10FC_CMDS(i)
{L66}:[21]:S_ICP_I50NFC_SENSOR(i) +20 < [39]:S_ICP_I50NFC_SENSOR(i+1)
{L67}:[23]:S_FCP_I50NFC(i) +20 < [40]:S_FCP_I50NFC(i+1)
{L68}:[25]:S_FCP_P50NFC(i) +20 < [41]:S_FCP_P50NFC(i+1)
{L69}:[39]:S_ICP_I50NFC_SENSOR(i+1) -20 < [21]:S_ICP_I50NFC_SENSOR(i)
{L70}:[40]:S_FCP_I50NFC(i+1) -20 < [23]:S_FCP_I50NFC(i)
{L71}:[41]:S_FCP_P50NFC(i+1) -20 < [25]:S_FCP_P50NFC(i)
{L72}:[2]:E_FCP_I50FC(i) +0 < [13]:S_FCP_I10FC(i)
{L73}:[2]:E_FCP_I50FC(i) +0 < [23]:S_FCP_I50NFC(i)
The safety assertion is:
{L74}:[42]:S_ICP_I50FC_SENSOR(I) +11 < [43]:E_ICP_I50FC_CMDS(I) OR {L75}:[44]:S_ICP_I10FC_SENSOR(I) +51 < [45]:E_ICP_I10FC_CMDS(I)
The set of positive cycles:
NOT {L46}:[1]:S_ICP_I50FC_SENSOR(i) +20 < [29]:S_ICP_I50FC_SENSOR(i+1) OR NOT {L74}:[42]:S_ICP_I50FC_SENSOR(I) +11 < [43]:E_ICP_I50FC_CMDS(I) OR NOT {L4}:[8]:E_ICP_I50FC_CMDS(i) -1 < [9]:S_ICP_I50FC_CMDS(i) OR NOT {L39}:[9]:S_ICP_I50FC_CMDS(i) -1 < [26]:S_FCP_O50FC(i) OR NOT {L38}:[26]:S_FCP_O50FC(i) -5 < [5]:S_FCP_P50FC(i) OR NOT {L37}:[5]:S_FCP_P50FC(i) -1 < [3]:S_FCP_I50FC(i) OR NOT {L36}:[3]:S_FCP_I50FC(i) -2 < [1]:S_ICP_I50FC_SENSOR(i)
NOT {L74}:[42]:S_ICP_I50FC_SENSOR(I) +11 < [43]:E_ICP_I50FC_CMDS(I) OR NOT {L4}:[8]:E_ICP_I50FC_CMDS(i) -1 < [9]:S_ICP_I50FC_CMDS(i) OR NOT {L39}:[9]:S_ICP_I50FC_CMDS(i) -1 < [26]:S_FCP_O50FC(i) OR NOT {L38}:[26]:S_FCP_O50FC(i) -5 < [5]:S_FCP_P50FC(i) OR NOT {L37}:[5]:S_FCP_P50FC(i) -1 < [3]:S_FCP_I50FC(i) OR NOT {L36}:[3]:S_FCP_I50FC(i) -2 < [1]:S_ICP_I50FC_SENSOR(i)
NOT {L56}:[11]:S_ICP_I10FC_SENSOR(i) +100 < [34]:S_ICP_I10FC_SENSOR(i+1) OR NOT {L75}:[44]:S_ICP_I10FC_SENSOR(I) +51 < [45]:E_ICP_I10FC_CMDS(I) OR NOT {L9}:[18]:E_ICP_I10FC_CMDS(i) -1 < [19]:S_ICP_I10FC_CMDS(i) OR NOT {L43}:[19]:S_ICP_I10FC_CMDS(i) -1 < [17]:S_FCP_O10FC(i) OR NOT {L42}:[17]:S_FCP_O10FC(i) -40 < [15]:S_FCP_P10FC(i) OR NOT {L41}:[15]:S_FCP_P10FC(i) -1 < [13]:S_FCP_I10FC(i) OR NOT {L40}:[13]:S_FCP_I10FC(i) -2 < [11]:S_ICP_I10FC_SENSOR(i)
NOT {L75}:[44]:S_ICP_I10FC_SENSOR(I) +51 < [45]:E_ICP_I10FC_CMDS(I) OR NOT {L9}:[18]:E_ICP_I10FC_CMDS(i) -1 < [19]:S_ICP_I10FC_CMDS(i) OR NOT {L43}:[19]:S_ICP_I10FC_CMDS(i) -1 < [17]:S_FCP_O10FC(i) OR NOT {L42}:[17]:S_FCP_O10FC(i) -40 < [15]:S_FCP_P10FC(i) OR NOT {L41}:[15]:S_FCP_P10FC(i) -1 < [13]:S_FCP_I10FC(i) OR NOT {L40}:[13]:S_FCP_I10FC(i) -2 < [11]:S_ICP_I10FC_SENSOR(i)

The determinant of the unoptimized formula:0.0 (so the real-time specification implies the safety assertion)

THE OPTIMIZED FORMULA
The specification is:
{L0}:[0]:E_ICP_I50FC_SENSOR(i) -2 < [1]:S_ICP_I50FC_SENSOR(i)
{L1}:[2]:E_FCP_I50FC(i) -1 < [3]:S_FCP_I50FC(i)
{L2}:[4]:E_FCP_P50FC(i) -5 < [5]:S_FCP_P50FC(i)
{L3}:[6]:E_FCP_O50FC(i) -1 < [7]:S_FCP_O50(i)
{L4}:[8]:E_ICP_I50FC_CMDS(i) -1 < [9]:S_ICP_I50FC_CMDS(i)
{L5}:[10]:E_ICP_I10FC_SENSOR(i) -2 < [11]:S_ICP_I10FC_SENSOR(i)
{L6}:[12]:E_FCP_I10FC(i) -1 < [13]:S_FCP_I10FC(i)
{L7}:[14]:E_FCP_P10FC(i) -40 < [15]:S_FCP_P10FC(i)
{L8}:[16]:E_FCP_O10FC(i) -1 < [17]:S_FCP_O10FC(i)
{L9}:[18]:E_ICP_I10FC_CMDS(i) -1 < [19]:S_ICP_I10FC_CMDS(i)
{L10}:[20]:E_ICP_I50NFC_SENSOR(i) -5 < [21]:S_ICP_I50NFC_SENSOR(i)
{L11}:[22]:E_FCP_I50NFC(i) -1 < [23]:S_FCP_I50NFC(i)
{L12}:[24]:E_FCP_P50NFC(i) -2 < [25]:S_FCP_P50NFC(i)
{L13}:[1]:S_ICP_I50FC_SENSOR(i) +0 < [0]:E_ICP_I50FC_SENSOR(i)
{L14}:[3]:S_FCP_I50FC(i) +0 < [2]:E_FCP_I50FC(i)
{L15}:[5]:S_FCP_P50FC(i) +0 < [4]:E_FCP_P50FC(i)
{L16}:[26]:S_FCP_O50FC(i) +0 < [6]:E_FCP_O50FC(i)
{L17}:[9]:S_ICP_I50FC_CMDS(i) +0 < [8]:E_ICP_I50FC_CMDS(i)
{L18}:[11]:S_ICP_I10FC_SENSOR(i) +0 < [10]:E_ICP_I10FC_SENSOR(i)
{L19}:[13]:S_FCP_I10FC(i) +0 < [12]:E_FCP_I10FC(i)
{L20}:[15]:S_FCP_P10FC(i) +0 < [14]:E_FCP_P10FC(i)
{L21}:[17]:S_FCP_O10FC(i) +0 < [16]:E_FCP_O10FC(i)
{L22}:[19]:S_ICP_I10FC_CMDS(i) +0 < [18]:E_ICP_I10FC_CMDS(i)
{L23}:[21]:S_ICP_I50NFC_SENSOR(i) +0 < [20]:E_ICP_I50NFC_SENSOR(i)
{L24}:[23]:S_FCP_I50NFC(i) +0 < [22]:E_FCP_I50NFC(i)
{L25}:[25]:S_FCP_P50NFC(i) +0 < [24]:E_FCP_P50NFC(i)
{L26}:[0]:E_ICP_I50FC_SENSOR(i) +0 < [3]:S_FCP_I50FC(i)
{L27}:[2]:E_FCP_I50FC(i) +0 < [5]:S_FCP_P50FC(i)
{L28}:[4]:E_FCP_P50FC(i) +0 < [26]:S_FCP_O50FC(i)
{L29}:[6]:E_FCP_O50FC(i) +0 < [27]:S_FCP_I50FC_CMDS(i)
{L30}:[10]:E_ICP_I10FC_SENSOR(i) +0 < [13]:S_FCP_I10FC(i)
{L31}:[12]:E_FCP_I10FC(i) +0 < [15]:S_FCP_P10FC(i)
{L32}:[14]:E_FCP_P10FC(i) +0 < [17]:S_FCP_O10FC(i)
{L33}:[16]:E_FCP_O10FC(i) +0 < [28]:S_FCP_I10FC_CMDS(i)
{L34}:[20]:E_ICP_I50NFC_SENSOR(i) +0 < [23]:S_FCP_I50NFC(i)
{L35}:[22]:E_FCP_I50NFC(i) +0 < [25]:S_FCP_P50NFC(i)
{L36}:[3]:S_FCP_I50FC(i) -2 < [1]:S_ICP_I50FC_SENSOR(i)
{L37}:[5]:S_FCP_P50FC(i) -1 < [3]:S_FCP_I50FC(i)
{L38}:[26]:S_FCP_O50FC(i) -5 < [5]:S_FCP_P50FC(i)
{L39}:[9]:S_ICP_I50FC_CMDS(i) -1 < [26]:S_FCP_O50FC(i)
{L40}:[13]:S_FCP_I10FC(i) -2 < [11]:S_ICP_I10FC_SENSOR(i)
{L41}:[15]:S_FCP_P10FC(i) -1 < [13]:S_FCP_I10FC(i)
{L42}:[17]:S_FCP_O10FC(i) -40 < [15]:S_FCP_P10FC(i)
{L43}:[19]:S_ICP_I10FC_CMDS(i) -1 < [17]:S_FCP_O10FC(i)
{L44}:[23]:S_FCP_I50NFC(i) -2 < [21]:S_ICP_I50NFC_SENSOR(i)
{L45}:[25]:S_FCP_P50NFC(i) -1 < [23]:S_FCP_I50NFC(i)
{L46}:[1]:S_ICP_I50FC_SENSOR(i) +0 < [29]:S_ICP_I50FC_SENSOR(i+1)
{L47}:[3]:S_FCP_I50FC(i) +20 < [30]:S_FCP_I50FC(i+1)
{L48}:[5]:S_FCP_P50FC(i) +20 < [31]:S_FCP_P50FC(i+1)
{L49}:[26]:S_FCP_O50FC(i) +20 < [32]:S_FCP_O50FC(i+1)
{L50}:[9]:S_ICP_I50FC_CMDS(i) +20 < [33]:S_ICP_I50FC_CMDS(i+1)
{L51}:[29]:S_ICP_I50FC_SENSOR(i+1) -20 < [1]:S_ICP_I50FC_SENSOR(i)
{L52}:[30]:S_FCP_I50FC(i+1) -20 < [3]:S_FCP_I50FC(i)
{L53}:[31]:S_FCP_P50FC(i+1) -20 < [5]:S_FCP_P50FC(i)
{L54}:[32]:S_FCP_O50FC(i+1) -20 < [26]:S_FCP_O50FC(i)
{L55}:[33]:S_ICP_I50FC_CMDS(i+1) -20 < [9]:S_ICP_I50FC_CMDS(i)
{L56}:[11]:S_ICP_I10FC_SENSOR(i) -27 < [34]:S_ICP_I10FC_SENSOR(i+1)
{L57}:[13]:S_FCP_I10FC(i) +100 < [35]:S_FCP_I10FC(i+1)
{L58}:[15]:S_FCP_P10FC(i) +100 < [36]:S_FCP_P10FC(i+1)
{L59}:[17]:S_FCP_O10FC(i) +100 < [37]:S_FCP_O10FC(i+1)
{L60}:[19]:S_ICP_I10FC_CMDS(i) +100 < [38]:S_ICP_I10FC_CMDS(i+1)
{L61}:[34]:S_ICP_I10FC_SENSOR(i+1) -100 < [11]:S_ICP_I10FC_SENSOR(i)
{L62}:[35]:S_FCP_I10FC(i+1) -100 < [13]:S_FCP_I10FC(i)
{L63}:[36]:S_FCP_P10FC(i+1) -100 < [15]:S_FCP_P10FC(i)
{L64}:[37]:S_FCP_O10FC(i+1) -100 < [17]:S_FCP_O10FC(i)
{L65}:[38]:S_ICP_I10FC_CMDS(i+1) -100 < [19]:S_ICP_I10FC_CMDS(i)
{L66}:[21]:S_ICP_I50NFC_SENSOR(i) +20 < [39]:S_ICP_I50NFC_SENSOR(i+1)
{L67}:[23]:S_FCP_I50NFC(i) +20 < [40]:S_FCP_I50NFC(i+1)
{L68}:[25]:S_FCP_P50NFC(i) +20 < [41]:S_FCP_P50NFC(i+1)
{L69}:[39]:S_ICP_I50NFC_SENSOR(i+1) -20 < [21]:S_ICP_I50NFC_SENSOR(i)
{L70}:[40]:S_FCP_I50NFC(i+1) -20 < [23]:S_FCP_I50NFC(i)
{L71}:[41]:S_FCP_P50NFC(i+1) -20 < [25]:S_FCP_P50NFC(i)
{L72}:[2]:E_FCP_I50FC(i) +0 < [13]:S_FCP_I10FC(i)
{L73}:[2]:E_FCP_I50FC(i) +0 < [23]:S_FCP_I50NFC(i)
The safety assertion is:
{L74}:[42]:S_ICP_I50FC_SENSOR(I) +11 < [43]:E_ICP_I50FC_CMDS(I) OR {L75}:[44]:S_ICP_I10FC_SENSOR(I) +51 < [45]:E_ICP_I10FC_CMDS(I)
The set of positive cycles:
NOT {L46}:[1]:S_ICP_I50FC_SENSOR(i) +0 < [29]:S_ICP_I50FC_SENSOR(i+1) OR NOT {L74}:[42]:S_ICP_I50FC_SENSOR(I) +11 < [43]:E_ICP_I50FC_CMDS(I) OR NOT {L4}:[8]:E_ICP_I50FC_CMDS(i) -1 < [9]:S_ICP_I50FC_CMDS(i) OR NOT {L39}:[9]:S_ICP_I50FC_CMDS(i) -1 < [26]:S_FCP_O50FC(i) OR NOT {L38}:[26]:S_FCP_O50FC(i) -5 < [5]:S_FCP_P50FC(i) OR NOT {L37}:[5]:S_FCP_P50FC(i) -1 < [3]:S_FCP_I50FC(i) OR NOT {L36}:[3]:S_FCP_I50FC(i) -2 < [1]:S_ICP_I50FC_SENSOR(i)
NOT {L74}:[42]:S_ICP_I50FC_SENSOR(I) +11 < [43]:E_ICP_I50FC_CMDS(I) OR NOT {L4}:[8]:E_ICP_I50FC_CMDS(i) -1 < [9]:S_ICP_I50FC_CMDS(i) OR NOT {L39}:[9]:S_ICP_I50FC_CMDS(i) -1 < [26]:S_FCP_O50FC(i) OR NOT {L38}:[26]:S_FCP_O50FC(i) -5 < [5]:S_FCP_P50FC(i) OR NOT {L37}:[5]:S_FCP_P50FC(i) -1 < [3]:S_FCP_I50FC(i) OR NOT {L36}:[3]:S_FCP_I50FC(i) -2 < [1]:S_ICP_I50FC_SENSOR(i)
NOT {L56}:[11]:S_ICP_I10FC_SENSOR(i) -27 < [34]:S_ICP_I10FC_SENSOR(i+1) OR NOT {L75}:[44]:S_ICP_I10FC_SENSOR(I) +51 < [45]:E_ICP_I10FC_CMDS(I) OR NOT {L9}:[18]:E_ICP_I10FC_CMDS(i) -1 < [19]:S_ICP_I10FC_CMDS(i) OR NOT {L43}:[19]:S_ICP_I10FC_CMDS(i) -1 < [17]:S_FCP_O10FC(i) OR NOT {L42}:[17]:S_FCP_O10FC(i) -40 < [15]:S_FCP_P10FC(i) OR NOT {L41}:[15]:S_FCP_P10FC(i) -1 < [13]:S_FCP_I10FC(i) OR NOT {L40}:[13]:S_FCP_I10FC(i) -2 < [11]:S_ICP_I10FC_SENSOR(i)
NOT {L75}:[44]:S_ICP_I10FC_SENSOR(I) +51 < [45]:E_ICP_I10FC_CMDS(I) OR NOT {L9}:[18]:E_ICP_I10FC_CMDS(i) -1 < [19]:S_ICP_I10FC_CMDS(i) OR NOT {L43}:[19]:S_ICP_I10FC_CMDS(i) -1 < [17]:S_FCP_O10FC(i) OR NOT {L42}:[17]:S_FCP_O10FC(i) -40 < [15]:S_FCP_P10FC(i) OR NOT {L41}:[15]:S_FCP_P10FC(i) -1 < [13]:S_FCP_I10FC(i) OR NOT {L40}:[13]:S_FCP_I10FC(i) -2 < [11]:S_ICP_I10FC_SENSOR(i)

The determinant of the optimized formula: 0.0 (so the real-time specification implies the safety assertion)