Systematic/Automatic Debugging for path Real Time Logic -- SDRTL/ADRTL

Home

 People Papers Tool description Java docs

 

Description
Sample 1 - Railroad
Sample 2 - Reactor
Sample 3 - X38 avionics
Description of the automatic debugging of path real-time logic

 

 

 

Description

The Systematic Debugging for path Real Time Logic Tool (SDRTL v1.0) is implemented in Java.

The class files can be downloaded freely from here (Copyright of its respective owners).

All tests have been conducted on a Pentium4 PC 1600Mhz, 256RAM, running on Windows XP and using Java SDK1.4.2_03.

Sample 1 - Railroad

Description of case study

“When the train approaches the sensor, a signal will initiate the lowering of the gate”, and “Gate is moved to the down position within 30s from being detected by the sensor”, and “The gate needs at least 15s to lower itself to the down position”.

The goal of this real-time system is described by the following safety assertions (denoted as SA):

“If the train needs at least 45s to travel from the sensor to the railroad crossing”, and “the train crossing is completed within 60s from being detected by the sensor”, then “we are assured that at the start of the train crossing, the gate has moved down and that the train leaves the railroad crossing within 45s from the time the gate has completed moving down”.

Problem specification:

In terms of RTL:

Conjunctive Normal Form (after skolemizing):

Constraints graph:

Specification file

One clause missing
In this situation, we have intentionally left out of the new specification one constraint, linking n3 to g1, as seen below (the dotted line).

Here is the file specifying the constraints to be added and here is the file specifying the constraints that will be removed from the old specification.

After running the algorithm (see here the transcript of the computer-user dialog), we get the following formula: 
Final formula:
{L0}:[0]:f(x) +0 < [1]:g1(x) AND 
{L1}:[2]:g2(x) -30 < [0]:f(x) AND 
{L2}:[3]:g1(y) +15 < [4]:g2(y) AND 
{L3}:[5]:f(T) +45 < [6]:h1(U) AND 
{L4}:[7]:h2(U) -59 < [5]:f(T) AND 
NOT {L0}:[0]:f(x) +0 < [1]:g1(x) OR NOT {L2}:[3]:g1(y) +15 < [4]:g2(y) OR NOT {L6}:[8]:g2(T) +46 < [7]:h2(U) OR 
NOT {L4}:[7]:h2(U) -59 < [5]:f(T) AND 
NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L5}:[6]:h1(U) +1 < [8]:g2(T) OR NOT {L1}:[2]:g2(x) -30 < [0]:f(x) AND 
NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L5}:[6]:h1(U) +1 < [8]:g2(T) OR NOT {L6}:[8]:g2(T) +46 < [7]:h2(U) OR 
NOT {L4}:[7]:h2(U) -59 < [5]:f(T) AND 
{L7}:[9]:n2(z1) -10 < [10]:n1(z1) AND 
{L8}:[11]:n4(z2) -10 < [12]:n3(z2) AND 
{L9}:[13]:n1(V1) -15 < [3]:g1(y) AND 
{L5}:[6]:h1(U) +1 < [8]:g2(T) OR {L6}:[8]:g2(T) +46 < [7]:h2(U) OR {L10}:[6]:h1(U) -4 < [14]:n2(V1) OR 
{L11}:[6]:h1(U) -4 < [15]:n4(V2) AND 
NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L10}:[6]:h1(U) -4 < [14]:n2(V1) OR NOT {L7}:[9]:n2(z1) -10 < [10]:n1(z1) OR 
NOT {L9}:[13]:n1(V1) -15 < [3]:g1(y) OR NOT {L2}:[3]:g1(y) +15 < [4]:g2(y) OR NOT {L1}:[2]:g2(x) -30 < [0]:f(x) AND 
NOT {L6}:[8]:g2(T) +46 < [7]:h2(U) OR NOT {L4}:[7]:h2(U) -59 < [5]:f(T) OR NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR 
NOT {L10}:[6]:h1(U) -4 < [14]:n2(V1) OR NOT {L7}:[9]:n2(z1) -10 < [10]:n1(z1) OR NOT {L9}:[13]:n1(V1) -15 < [3]:g1(y) OR
 NOT {L2}:[3]:g1(y) +15 < [4]:g2(y) AND 
NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L11}:[6]:h1(U) -4 < [15]:n4(V2) OR NOT {L8}:[11]:n4(z2) -10 < [12]:n3(z2) OR
 NOT {L12}:[16]:n3(V2) -15 < [17]:g1(T) OR NOT {L2}:[3]:g1(y) +15 < [4]:g2(y) OR NOT {L1}:[2]:g2(x) -30 < [0]:f(x) AND 
{L12}:[16]:n3(V2) -15 < [17]:g1(T)

Determinant:0.0
As you can see, a new unit clause has been added (denoted {L12} in our example) as well as a negative clause (the last one in our example), correspondig to a new negative cycle in the graph, involving the newly added edge. The software has correctly checked, identified and applied the substitutions necessary according to the parameters of the functional symbols that take part in the shown cycle.

Running time: 0,15s
Efficiency: 0.43
See here the log file.
Two clauses missing
In this situation, we have intentionally left out of the new specification two constraints, linking n1 to g1 and n3 to g1, as seen below (the dotted lines).

Here is the file specifying the constraints to be added and here is the file specifying the constraints that will be removed from the old specification.

After running the algorithm (see here the transcript of the computer-user dialog), we get the following formula (very similar to the one in the previous case): 
Final formula:
{L0}:[0]:f(x) +0 < [1]:g1(x) AND 
{L1}:[2]:g2(x) -30 < [0]:f(x) AND 
{L2}:[3]:g1(y) +15 < [4]:g2(y) AND 
{L3}:[5]:f(T) +45 < [6]:h1(U) AND 
{L4}:[7]:h2(U) -59 < [5]:f(T) AND 
NOT {L0}:[0]:f(x) +0 < [1]:g1(x) OR NOT {L2}:[3]:g1(y) +15 < [4]:g2(y) OR NOT {L6}:[8]:g2(T) +46 < [7]:h2(U) OR 
NOT {L4}:[7]:h2(U) -59 < [5]:f(T) AND 
NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L5}:[6]:h1(U) +1 < [8]:g2(T) OR NOT {L1}:[2]:g2(x) -30 < [0]:f(x) AND 
NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L5}:[6]:h1(U) +1 < [8]:g2(T) OR NOT {L6}:[8]:g2(T) +46 < [7]:h2(U) OR 
NOT {L4}:[7]:h2(U) -59 < [5]:f(T) AND 
{L7}:[9]:n2(z1) -10 < [10]:n1(z1) AND 
{L8}:[11]:n4(z2) -10 < [12]:n3(z2) AND 
{L5}:[6]:h1(U) +1 < [8]:g2(T) OR {L6}:[8]:g2(T) +46 < [7]:h2(U) OR {L9}:[6]:h1(U) -4 < [13]:n2(V1) OR 
{L10}:[6]:h1(U) -4 < [14]:n4(V2) AND 
NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L9}:[6]:h1(U) -4 < [13]:n2(V1) OR NOT {L7}:[9]:n2(z1) -10 < [10]:n1(z1) OR 
NOT {L11}:[15]:n1(V1) -15 < [16]:g1(T) OR NOT {L2}:[3]:g1(y) +15 < [4]:g2(y) OR NOT {L1}:[2]:g2(x) -30 < [0]:f(x) AND 
{L11}:[15]:n1(V1) -15 < [16]:g1(T) AND 
NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L10}:[6]:h1(U) -4 < [14]:n4(V2) OR NOT {L8}:[11]:n4(z2) -10 < [12]:n3(z2) OR
 NOT {L12}:[17]:n3(V2) -15 < [16]:g1(T) OR NOT {L2}:[3]:g1(y) +15 < [4]:g2(y) OR NOT {L1}:[2]:g2(x) -30 < [0]:f(x) AND 
{L12}:[17]:n3(V2) -15 < [16]:g1(T)

Determinant:0.0
As you can see, two new unit clauses have been added (denoted {L11} and {L12} in our example) as well as two negative clauses (the last two in our example), correspondig to two new negative cycles in the graph, involving the newly added edges. The software has correctly checked, identified and applied the substitutions necessary according to the parameters of the functional symbols that take part in the shown cycles.

Running time: 0,27s
Efficiency: 0.40
See here the log file.
Three clauses missing
In this situation, we have intentionally left out of the new specification three constraints, linking n1 to g1, n3 to g1 and n6 to g1.
Here is the file specifying the constraints to be added and here is the file specifying the constraints that will be removed from the old specification.

After running the algorithm (see here the transcript of the computer-user dialog), we get the following formula (very similar to the one in the previous case): 
Final formula:
{L0}:[0]:f(x) +0 < [1]:g1(x) AND 
{L1}:[2]:g2(x) -30 < [0]:f(x) AND 
{L2}:[3]:g1(y) +15 < [4]:g2(y) AND 
{L3}:[5]:f(T) +45 < [6]:h1(U) AND 
{L4}:[7]:h2(U) -59 < [5]:f(T) AND 
NOT {L0}:[0]:f(x) +0 < [1]:g1(x) OR NOT {L2}:[3]:g1(y) +15 < [4]:g2(y) OR NOT {L6}:[8]:g2(T) +46 < [7]:h2(U) OR 
NOT {L4}:[7]:h2(U) -59 < [5]:f(T) AND 
NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L5}:[6]:h1(U) +1 < [8]:g2(T) OR NOT {L1}:[2]:g2(x) -30 < [0]:f(x) AND 
NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L5}:[6]:h1(U) +1 < [8]:g2(T) OR NOT {L6}:[8]:g2(T) +46 < [7]:h2(U) OR 
NOT {L4}:[7]:h2(U) -59 < [5]:f(T) AND 
{L7}:[9]:n2(z1) -10 < [10]:n1(z1) AND 
{L8}:[11]:n4(z2) -10 < [12]:n3(z2) AND 
{L9}:[13]:n5(z) -10 < [14]:n6(z) AND 
{L5}:[6]:h1(U) +1 < [8]:g2(T) OR {L6}:[8]:g2(T) +46 < [7]:h2(U) OR {L10}:[6]:h1(U) -4 < [15]:n2(V1) OR 
{L11}:[6]:h1(U) -4 < [16]:n4(V2) OR {L12}:[6]:h1(U) -4 < [17]:n5(V3) AND 
NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L10}:[6]:h1(U) -4 < [15]:n2(V1) OR NOT {L7}:[9]:n2(z1) -10 < [10]:n1(z1) OR 
NOT {L13}:[18]:n1(V1) -15 < [19]:g1(T) OR NOT {L2}:[3]:g1(y) +15 < [4]:g2(y) OR NOT {L1}:[2]:g2(x) -30 < [0]:f(x) AND 
{L13}:[18]:n1(V1) -15 < [19]:g1(T) AND 
NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L11}:[6]:h1(U) -4 < [16]:n4(V2) OR NOT {L8}:[11]:n4(z2) -10 < [12]:n3(z2) OR 
NOT {L14}:[20]:n3(V2) -15 < [19]:g1(T) OR NOT {L2}:[3]:g1(y) +15 < [4]:g2(y) OR NOT {L1}:[2]:g2(x) -30 < [0]:f(x) AND 
{L14}:[20]:n3(V2) -15 < [19]:g1(T) AND 
NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L12}:[6]:h1(U) -4 < [17]:n5(V3) OR NOT {L9}:[13]:n5(z) -10 < [14]:n6(z) OR 
NOT {L15}:[21]:n6(V3) -15 < [19]:g1(T) OR NOT {L2}:[3]:g1(y) +15 < [4]:g2(y) OR NOT {L1}:[2]:g2(x) -30 < [0]:f(x) AND 
{L15}:[21]:n6(V3) -15 < [19]:g1(T)

Determinant:0.0
As you can see, three new unit clauses have been added (denoted {L13}, {L14} and {L15} in our example) as well as three negative clauses, correspondig to three new negative cycles in the graph, involving the newly added edges. The software has correctly checked, identified and applied the substitutions necessary according to the parameters of the functional symbols that take part in the shown cycles.

Running time: 0,39s
Efficiency: 0.36
See here the log file.
Four clauses missing
In this situation, we have intentionally left out of the new specification four constraints, linking n1 to g1, n3 to g1, n6 to g1 and n8 to g1.
Here is the file specifying the constraints to be added and here is the file specifying the constraints that will be removed from the old specification.

After running the algorithm (see here the transcript of the computer-user dialog), we get the following formula (very similar to the one in the previous case): 
Final formula:
{L0}:[0]:f(x) +0 < [1]:g1(x) AND 
{L1}:[2]:g2(x) -30 < [0]:f(x) AND 
{L2}:[3]:g1(y) +15 < [4]:g2(y) AND 
{L3}:[5]:f(T) +45 < [6]:h1(U) AND 
{L4}:[7]:h2(U) -59 < [5]:f(T) AND 
NOT {L0}:[0]:f(x) +0 < [1]:g1(x) OR NOT {L2}:[3]:g1(y) +15 < [4]:g2(y) OR NOT {L6}:[8]:g2(T) +46 < [7]:h2(U) OR 
NOT {L4}:[7]:h2(U) -59 < [5]:f(T) AND 
NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L5}:[6]:h1(U) +1 < [8]:g2(T) OR NOT {L1}:[2]:g2(x) -30 < [0]:f(x) AND 
NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L5}:[6]:h1(U) +1 < [8]:g2(T) OR NOT {L6}:[8]:g2(T) +46 < [7]:h2(U) OR 
NOT {L4}:[7]:h2(U) -59 < [5]:f(T) AND 
{L7}:[9]:n2(z1) -10 < [10]:n1(z1) AND 
{L8}:[11]:n4(z2) -10 < [12]:n3(z2) AND 
{L9}:[13]:n5(z) -10 < [14]:n6(z) AND 
{L10}:[15]:n7(z4) -10 < [16]:n8(z4) AND 
{L5}:[6]:h1(U) +1 < [8]:g2(T) OR {L6}:[8]:g2(T) +46 < [7]:h2(U) OR {L11}:[6]:h1(U) -4 < [17]:n2(V1) OR 
{L12}:[6]:h1(U) -4 < [18]:n4(V2) OR {L13}:[6]:h1(U) -4 < [19]:n5(V3) OR {L14}:[6]:h1(U) -4 < [20]:n7(v4) AND 
NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L11}:[6]:h1(U) -4 < [17]:n2(V1) OR NOT {L7}:[9]:n2(z1) -10 < [10]:n1(z1) OR 
NOT {L15}:[21]:n1(V1) -15 < [22]:g1(T) OR NOT {L2}:[3]:g1(y) +15 < [4]:g2(y) OR NOT {L1}:[2]:g2(x) -30 < [0]:f(x) AND 
{L15}:[21]:n1(V1) -15 < [22]:g1(T) AND 
NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L12}:[6]:h1(U) -4 < [18]:n4(V2) OR NOT {L8}:[11]:n4(z2) -10 < [12]:n3(z2) OR 
NOT {L16}:[23]:n3(V2) -15 < [22]:g1(T) OR NOT {L2}:[3]:g1(y) +15 < [4]:g2(y) OR NOT {L1}:[2]:g2(x) -30 < [0]:f(x) AND 
{L16}:[23]:n3(V2) -15 < [22]:g1(T) AND 
NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L13}:[6]:h1(U) -4 < [19]:n5(V3) OR NOT {L9}:[13]:n5(z) -10 < [14]:n6(z) OR 
NOT {L17}:[24]:n6(V3) -15 < [22]:g1(T) OR NOT {L2}:[3]:g1(y) +15 < [4]:g2(y) OR NOT {L1}:[2]:g2(x) -30 < [0]:f(x) AND 
{L17}:[24]:n6(V3) -15 < [22]:g1(T) AND 
NOT {L3}:[5]:f(T) +45 < [6]:h1(U) OR NOT {L14}:[6]:h1(U) -4 < [20]:n7(v4) OR NOT {L10}:[15]:n7(z4) -10 < [16]:n8(z4) OR
 NOT {L18}:[16]:n8(z4) -15 < [22]:g1(T) OR NOT {L2}:[3]:g1(y) +15 < [4]:g2(y) OR NOT {L1}:[2]:g2(x) -30 < [0]:f(x) AND 
{L18}:[16]:n8(z4) -15 < [22]:g1(T)

Determinant:0.0
As you can see, four new unit clauses have been added (denoted {L15}, {L16}, {L17} and {L18} in our example) as well as four negative clauses, correspondig to four new negative cycles in the graph, involving the newly added edges. The software has correctly checked, identified and applied the substitutions necessary according to the parameters of the functional symbols that take part in the shown cycles.

Running time: 0,57s
Efficiency: 0.34
See here the log file.

Sample 2 - Reactor

This second case study is taken from [Jahanian, Mok, 1987]. It describes a system used to monitor and control a reactor. Please refer to the above mentioned paper for specification details.

For this sample we have also considered four situations, where we have intentionally "missed" one, two, three or four constraints. Following the same idea described above, we have considered the Jahanian-Mok specification as the "old" specification (see here our input file) and we have added and removed some constraints. Just for testing purposes, we have added up to four new, meaningless, nodes in the graph (new1 to new4).

One clause missing

We have inserted a new node (new1) and these new clauses.

After running the algorithm (see here the transcript of the computer-user dialog), we get the following formula: 
Final formula:
{L0}:[0]:BUTTON1(x1) +0 < [1]:StartRA1(x1) AND 
{L1}:[2]:StartRA1(x2) +40 < [3]:StopRA1(x2) AND 
{L2}:[4]:StopRA1(x3) +0 < [5]:GRANT1true(x3) AND 
{L3}:[6]:GRANT1true(x4) +0 < [7]:StartMOVE1(x4) AND 
{L4}:[7]:StartMOVE1(x4) -5 < [6]:GRANT1true(x4) AND 
{L5}:[8]:StopMOVE1(x6) -20 < [9]:StartMOVE1(x6) AND 
{L6}:[10]:BUTTON2(x7) +0 < [11]:StartRA2(x7) AND 
{L7}:[12]:StartRA2(x8) +40 < [13]:StopRA2(x8) AND 
{L8}:[14]:StopRA2(x9) +0 < [15]:GRANT2true(x9) AND 
{L9}:[16]:GRANT2true(x10) +0 < [17]:StartMOVE2(x10) AND 
{L10}:[17]:StartMOVE2(x10) -5 < [16]:GRANT2true(x10) AND 
{L11}:[18]:StopMOVE2(x12) -20 < [19]:StartMOVE2(x12) AND 
{L12}:[20]:GRANT1true(x5) +30 < [21]:GRANT1false(x5) AND 
{L13}:[22]:GRANT2true(x11) +30 < [23]:GRANT2false(x11) AND 
{L16}:[24]:StartMOVE1(I) +0 < [25]:StopMOVE2(J) AND 
{L17}:[26]:StartMOVE2(J) +0 < [27]:StopMOVE1(I) AND 
NOT {L3}:[6]:GRANT1true(x4) +0 < [7]:StartMOVE1(x4) OR NOT {L16}:[24]:StartMOVE1(I) +0 < [25]:StopMOVE2(J) OR
  NOT {L11}:[18]:StopMOVE2(x12) -20 < [19]:StartMOVE2(x12) OR NOT {L10}:[17]:StartMOVE2(x10) -5 < [16]:GRANT2true(x10) OR
  NOT {L13}:[22]:GRANT2true(x11) +30 < [23]:GRANT2false(x11) OR
  NOT {L15}:[28]:GRANT2false(x14) +0 < [29]:GRANT1true(x13) AND 
NOT {L12}:[20]:GRANT1true(x5) +30 < [21]:GRANT1false(x5) OR NOT {L14}:[30]:GRANT1false(x13) +0 < [31]:GRANT2true(x14) OR
  NOT {L9}:[16]:GRANT2true(x10) +0 < [17]:StartMOVE2(x10) OR NOT {L17}:[26]:StartMOVE2(J) +0 < [27]:StopMOVE1(I) OR 
  NOT {L5}:[8]:StopMOVE1(x6) -20 < [9]:StartMOVE1(x6) OR NOT {L4}:[7]:StartMOVE1(x4) -5 < [6]:GRANT1true(x4) AND 
NOT {L12}:[20]:GRANT1true(x5) +30 < [21]:GRANT1false(x5) OR NOT {L14}:[30]:GRANT1false(x13) +0 < [31]:GRANT2true(x14) OR
  NOT {L13}:[22]:GRANT2true(x11) +30 < [23]:GRANT2false(x11) OR 
  NOT {L15}:[28]:GRANT2false(x14) +0 < [29]:GRANT1true(x13) AND 
{L18}:[32]:GRANT1true(y1) +1 < [33]:new1(y1) OR {L14}:[30]:GRANT1false(x13) +0 < [31]:GRANT2true(x14) OR
  {L15}:[28]:GRANT2false(x14) +0 < [29]:GRANT1true(x13) AND 
NOT {L18}:[32]:GRANT1true(y1) +1 < [33]:new1(y1) OR NOT {L19}:[33]:new1(y1) +5 < [34]:StartMOVE1(y1) OR
  NOT {L4}:[7]:StartMOVE1(x4) -5 < [6]:GRANT1true(x4) AND 
{L19}:[33]:new1(y1) +5 < [34]:StartMOVE1(y1)

Determinant:0.0
As you can see, one new unit clause has been added (denoted {L19} in our example) as well as a negative clause, correspondig to the new negative cycle in the graph, involving the newly added edge. The software has correctly checked, identified and applied the substitutions necessary according to the parameters of the functional symbols that take part in the shown cycles.

Running time: 0.86s
Efficiency: 0.18
See here the log file.

Two clauses missing

We have inserted two new nodes (new1 and new2) and these new clauses.

After running the algorithm (see here the transcript of the computer-user dialog), we get the following formula: 
Final formula:
{L0}:[0]:BUTTON1(x1) +0 < [1]:StartRA1(x1) AND 
{L1}:[2]:StartRA1(x2) +40 < [3]:StopRA1(x2) AND 
{L2}:[4]:StopRA1(x3) +0 < [5]:GRANT1true(x3) AND 
{L3}:[6]:GRANT1true(x4) +0 < [7]:StartMOVE1(x4) AND 
{L4}:[7]:StartMOVE1(x4) -5 < [6]:GRANT1true(x4) AND 
{L5}:[8]:StopMOVE1(x6) -20 < [9]:StartMOVE1(x6) AND 
{L6}:[10]:BUTTON2(x7) +0 < [11]:StartRA2(x7) AND 
{L7}:[12]:StartRA2(x8) +40 < [13]:StopRA2(x8) AND 
{L8}:[14]:StopRA2(x9) +0 < [15]:GRANT2true(x9) AND 
{L9}:[16]:GRANT2true(x10) +0 < [17]:StartMOVE2(x10) AND 
{L10}:[17]:StartMOVE2(x10) -5 < [16]:GRANT2true(x10) AND 
{L11}:[18]:StopMOVE2(x12) -20 < [19]:StartMOVE2(x12) AND 
{L12}:[20]:GRANT1true(x5) +30 < [21]:GRANT1false(x5) AND 
{L13}:[22]:GRANT2true(x11) +30 < [23]:GRANT2false(x11) AND 
{L16}:[24]:StartMOVE1(I) +0 < [25]:StopMOVE2(J) AND 
{L17}:[26]:StartMOVE2(J) +0 < [27]:StopMOVE1(I) AND 
NOT {L3}:[6]:GRANT1true(x4) +0 < [7]:StartMOVE1(x4) OR NOT {L16}:[24]:StartMOVE1(I) +0 < [25]:StopMOVE2(J) OR
  NOT {L11}:[18]:StopMOVE2(x12) -20 < [19]:StartMOVE2(x12) OR NOT {L10}:[17]:StartMOVE2(x10) -5 < [16]:GRANT2true(x10) OR
  NOT {L13}:[22]:GRANT2true(x11) +30 < [23]:GRANT2false(x11) OR NOT {L15}:[28]:GRANT2false(x14) +0 < [29]:GRANT1true(x13) AND 
NOT {L12}:[20]:GRANT1true(x5) +30 < [21]:GRANT1false(x5) OR NOT {L14}:[30]:GRANT1false(x13) +0 < [31]:GRANT2true(x14) OR
  NOT {L9}:[16]:GRANT2true(x10) +0 < [17]:StartMOVE2(x10) OR NOT {L17}:[26]:StartMOVE2(J) +0 < [27]:StopMOVE1(I) OR 
  NOT {L5}:[8]:StopMOVE1(x6) -20 < [9]:StartMOVE1(x6) OR NOT {L4}:[7]:StartMOVE1(x4) -5 < [6]:GRANT1true(x4) AND 
NOT {L12}:[20]:GRANT1true(x5) +30 < [21]:GRANT1false(x5) OR NOT {L14}:[30]:GRANT1false(x13) +0 < [31]:GRANT2true(x14) OR
  NOT {L13}:[22]:GRANT2true(x11) +30 < [23]:GRANT2false(x11) OR NOT {L15}:[28]:GRANT2false(x14) +0 < [29]:GRANT1true(x13) AND 
{L18}:[32]:GRANT1true(y1) -4 < [33]:new1(y1) OR {L19}:[34]:GRANT2true(y2) -4 < [35]:new2(y2) OR 
  {L14}:[30]:GRANT1false(x13) +0 < [31]:GRANT2true(x14) OR {L15}:[28]:GRANT2false(x14) +0 < [29]:GRANT1true(x13) AND 
NOT {L18}:[32]:GRANT1true(y1) -4 < [33]:new1(y1) OR NOT {L20}:[33]:new1(y1) +10 < [36]:StartMOVE1(y1) OR 
  NOT {L4}:[7]:StartMOVE1(x4) -5 < [6]:GRANT1true(x4) AND 
{L20}:[33]:new1(y1) +10 < [36]:StartMOVE1(y1) AND 
NOT {L19}:[34]:GRANT2true(y2) -4 < [35]:new2(y2) OR NOT {L21}:[35]:new2(y2) +10 < [37]:StartMOVE2(y2) OR 
  NOT {L10}:[17]:StartMOVE2(x10) -5 < [16]:GRANT2true(x10) AND 
{L21}:[35]:new2(y2) +10 < [37]:StartMOVE2(y2)

Determinant:0.0
As you can see, two new unit clauses have been added (denoted {} and {} in our example) as well as two negative clauses, correspondig to the two new negative cycles in the graph, involving the newly added edges. The software has correctly checked, identified and applied the substitutions necessary according to the parameters of the functional symbols that take part in the shown cycles.

Running time: s
Efficiency:
See here the log file.

Three clauses missing

We have inserted thre new nodes (new2, new and new3) and these new clauses.

After running the algorithm (see here the transcript of the computer-user dialog), we get the following formula: 
Final formula:
{L0}:[0]:BUTTON1(x1) +0 < [1]:StartRA1(x1) AND 
{L1}:[2]:StartRA1(x2) +40 < [3]:StopRA1(x2) AND 
{L2}:[4]:StopRA1(x3) +0 < [5]:GRANT1true(x3) AND 
{L3}:[6]:GRANT1true(x4) +0 < [7]:StartMOVE1(x4) AND 
{L4}:[7]:StartMOVE1(x4) -5 < [6]:GRANT1true(x4) AND 
{L5}:[8]:StopMOVE1(x6) -20 < [9]:StartMOVE1(x6) AND 
{L6}:[10]:BUTTON2(x7) +0 < [11]:StartRA2(x7) AND 
{L7}:[12]:StartRA2(x8) +40 < [13]:StopRA2(x8) AND 
{L8}:[14]:StopRA2(x9) +0 < [15]:GRANT2true(x9) AND 
{L9}:[16]:GRANT2true(x10) +0 < [17]:StartMOVE2(x10) AND 
{L10}:[17]:StartMOVE2(x10) -5 < [16]:GRANT2true(x10) AND 
{L11}:[18]:StopMOVE2(x12) -20 < [19]:StartMOVE2(x12) AND 
{L12}:[20]:GRANT1true(x5) +30 < [21]:GRANT1false(x5) AND 
{L13}:[22]:GRANT2true(x11) +30 < [23]:GRANT2false(x11) AND 
{L16}:[24]:StartMOVE1(I) +0 < [25]:StopMOVE2(J) AND 
{L17}:[26]:StartMOVE2(J) +0 < [27]:StopMOVE1(I) AND 
NOT {L3}:[6]:GRANT1true(x4) +0 < [7]:StartMOVE1(x4) OR NOT {L16}:[24]:StartMOVE1(I) +0 < [25]:StopMOVE2(J) OR
  NOT {L11}:[18]:StopMOVE2(x12) -20 < [19]:StartMOVE2(x12) OR NOT {L10}:[17]:StartMOVE2(x10) -5 < [16]:GRANT2true(x10) OR
  NOT {L13}:[22]:GRANT2true(x11) +30 < [23]:GRANT2false(x11) OR 
  NOT {L15}:[28]:GRANT2false(x14) +0 < [29]:GRANT1true(x13) AND 
NOT {L12}:[20]:GRANT1true(x5) +30 < [21]:GRANT1false(x5) OR NOT {L14}:[30]:GRANT1false(x13) +0 < [31]:GRANT2true(x14) OR
  NOT {L9}:[16]:GRANT2true(x10) +0 < [17]:StartMOVE2(x10) OR NOT {L17}:[26]:StartMOVE2(J) +0 < [27]:StopMOVE1(I) OR 
  NOT {L5}:[8]:StopMOVE1(x6) -20 < [9]:StartMOVE1(x6) OR NOT {L4}:[7]:StartMOVE1(x4) -5 < [6]:GRANT1true(x4) AND 
NOT {L12}:[20]:GRANT1true(x5) +30 < [21]:GRANT1false(x5) OR NOT {L14}:[30]:GRANT1false(x13) +0 < [31]:GRANT2true(x14) OR
  NOT {L13}:[22]:GRANT2true(x11) +30 < [23]:GRANT2false(x11) OR 
  NOT {L15}:[28]:GRANT2false(x14) +0 < [29]:GRANT1true(x13) AND 
{L18}:[32]:GRANT1true(y) -4 < [33]:new2(y2) OR {L19}:[32]:GRANT1true(y) -6 < [34]:new(y) OR 
  {L14}:[30]:GRANT1false(x13) +0 < [31]:GRANT2true(x14) OR {L15}:[28]:GRANT2false(x14) +0 < [29]:GRANT1true(x13) OR
  {L20}:[35]:GRANT1true(y3) -8 < [36]:new3(y3) AND 
NOT {L18}:[32]:GRANT1true(y) -4 < [33]:new2(y2) OR NOT {L21}:[37]:new2(sdrtl1) +10 < [38]:StartMOVE1(y) OR 
  NOT {L4}:[7]:StartMOVE1(x4) -5 < [6]:GRANT1true(x4) AND 
{L21}:[37]:new2(sdrtl1) +10 < [38]:StartMOVE1(y) AND 
NOT {L19}:[32]:GRANT1true(y) -6 < [34]:new(y) OR NOT {L22}:[34]:new(y) +12 < [38]:StartMOVE1(y) OR 
  NOT {L4}:[7]:StartMOVE1(x4) -5 < [6]:GRANT1true(x4) AND 
{L22}:[34]:new(y) +12 < [38]:StartMOVE1(y) AND 
NOT {L20}:[35]:GRANT1true(y3) -8 < [36]:new3(y3) OR NOT {L23}:[36]:new3(y3) +14 < [39]:StartMOVE1(y3) OR 
  NOT {L4}:[7]:StartMOVE1(x4) -5 < [6]:GRANT1true(x4) AND 
{L23}:[36]:new3(y3) +14 < [39]:StartMOVE1(y3)

Determinant:0.0
As you can see, three new unit clauses have been added (denoted {L21}, {L22} and {L23} in our example) as well as three negative clauses, correspondig to three new negative cycles in the graph, involving the newly added edges. The software has correctly checked, identified and applied the substitutions necessary according to the parameters of the functional symbols that take part in the shown cycles.

Running time: 3.85s
Efficiency: 0.13
See here the log file.

Four clauses missing

We have inserted four new nodes (new1, new2, new3 and new4) and these new clauses.

After running the algorithm (see here the transcript of the computer-user dialog), we get the following formula: 
Final formula:
{L0}:[0]:BUTTON1(x1) +0 < [1]:StartRA1(x1) AND 
{L1}:[2]:StartRA1(x2) +40 < [3]:StopRA1(x2) AND 
{L2}:[4]:StopRA1(x3) +0 < [5]:GRANT1true(x3) AND 
{L3}:[6]:GRANT1true(x4) +0 < [7]:StartMOVE1(x4) AND 
{L4}:[7]:StartMOVE1(x4) -5 < [6]:GRANT1true(x4) AND 
{L5}:[8]:StopMOVE1(x6) -20 < [9]:StartMOVE1(x6) AND 
{L6}:[10]:BUTTON2(x7) +0 < [11]:StartRA2(x7) AND 
{L7}:[12]:StartRA2(x8) +40 < [13]:StopRA2(x8) AND 
{L8}:[14]:StopRA2(x9) +0 < [15]:GRANT2true(x9) AND 
{L9}:[16]:GRANT2true(x10) +0 < [17]:StartMOVE2(x10) AND 
{L10}:[17]:StartMOVE2(x10) -5 < [16]:GRANT2true(x10) AND 
{L11}:[18]:StopMOVE2(x12) -20 < [19]:StartMOVE2(x12) AND 
{L12}:[20]:GRANT1true(x5) +30 < [21]:GRANT1false(x5) AND 
{L13}:[22]:GRANT2true(x11) +30 < [23]:GRANT2false(x11) AND 
{L16}:[24]:StartMOVE1(I) +0 < [25]:StopMOVE2(J) AND 
{L17}:[26]:StartMOVE2(J) +0 < [27]:StopMOVE1(I) AND 
NOT {L3}:[6]:GRANT1true(x4) +0 < [7]:StartMOVE1(x4) OR NOT {L16}:[24]:StartMOVE1(I) +0 < [25]:StopMOVE2(J) OR 
  NOT {L11}:[18]:StopMOVE2(x12) -20 < [19]:StartMOVE2(x12) OR NOT {L10}:[17]:StartMOVE2(x10) -5 < [16]:GRANT2true(x10) OR 
  NOT {L13}:[22]:GRANT2true(x11) +30 < [23]:GRANT2false(x11) OR NOT {L15}:[28]:GRANT2false(x14) +0 < [29]:GRANT1true(x13) AND 
NOT {L12}:[20]:GRANT1true(x5) +30 < [21]:GRANT1false(x5) OR NOT {L14}:[30]:GRANT1false(x13) +0 < [31]:GRANT2true(x14) OR 
  NOT {L9}:[16]:GRANT2true(x10) +0 < [17]:StartMOVE2(x10) OR NOT {L17}:[26]:StartMOVE2(J) +0 < [27]:StopMOVE1(I) OR 
  NOT {L5}:[8]:StopMOVE1(x6) -20 < [9]:StartMOVE1(x6) OR NOT {L4}:[7]:StartMOVE1(x4) -5 < [6]:GRANT1true(x4) AND 
NOT {L12}:[20]:GRANT1true(x5) +30 < [21]:GRANT1false(x5) OR NOT {L14}:[30]:GRANT1false(x13) +0 < [31]:GRANT2true(x14) OR 
  NOT {L13}:[22]:GRANT2true(x11) +30 < [23]:GRANT2false(x11) OR NOT {L15}:[28]:GRANT2false(x14) +0 < [29]:GRANT1true(x13) AND 
{L18}:[32]:GRANT1true(y1) -2 < [33]:new1(y1) OR {L19}:[34]:GRANT1true(y2) -4 < [35]:new2(y2) OR 
  {L14}:[30]:GRANT1false(x13) +0 < [31]:GRANT2true(x14) OR {L15}:[28]:GRANT2false(x14) +0 < [29]:GRANT1true(x13) OR 
  {L20}:[36]:GRANT2true(y3) -6 < [37]:new3(y3) OR {L21}:[36]:GRANT2true(y3) -8 < [38]:new4(y4) AND 
NOT {L18}:[32]:GRANT1true(y1) -2 < [33]:new1(y1) OR NOT {L22}:[33]:new1(y1) +8 < [39]:StartMOVE1(y1) OR 
  NOT {L4}:[7]:StartMOVE1(x4) -5 < [6]:GRANT1true(x4) AND 
{L22}:[33]:new1(y1) +8 < [39]:StartMOVE1(y1) AND 
NOT {L19}:[34]:GRANT1true(y2) -4 < [35]:new2(y2) OR NOT {L23}:[40]:new2(I) +30 < [26]:StartMOVE2(J) OR 
  NOT {L17}:[26]:StartMOVE2(J) +0 < [27]:StopMOVE1(I) OR NOT {L5}:[8]:StopMOVE1(x6) -20 < [9]:StartMOVE1(x6) OR 
  NOT {L4}:[7]:StartMOVE1(x4) -5 < [6]:GRANT1true(x4) AND 
{L23}:[40]:new2(I) +30 < [26]:StartMOVE2(J) AND 
NOT {L20}:[36]:GRANT2true(y3) -6 < [37]:new3(y3) OR NOT {L24}:[37]:new3(y3) +12 < [41]:StartMOVE2(y3) OR 
  NOT {L10}:[17]:StartMOVE2(x10) -5 < [16]:GRANT2true(x10) AND 
{L24}:[37]:new3(y3) +12 < [41]:StartMOVE2(y3) AND 
NOT {L21}:[36]:GRANT2true(y3) -8 < [38]:new4(y4) OR NOT {L25}:[42]:new4(sdrtl1) +14 < [41]:StartMOVE2(y3) OR 
  NOT {L10}:[17]:StartMOVE2(x10) -5 < [16]:GRANT2true(x10) AND 
{L25}:[42]:new4(sdrtl1) +14 < [41]:StartMOVE2(y3)

Determinant:0.0
As you can see, four new unit clauses has been added (denoted {L22}, {L23}, {L24} and {L25} in our example) as well as four negative clauses, correspondig to four new negative cycles in the graph, involving the newly added edges. The software has correctly checked, identified and applied the substitutions necessary according to the parameters of the functional symbols that take part in the shown cycles.

Running time: 13.02s
Efficiency: 0.075
See here the log file.

Sample 3 - X38 avionics

This sample case is taken from [Rice, Cheng, 1999]. Please refer to this paper for complete specification of the sistem. The X-38 is an autonomous spacecraft designed and built by NASA as a prototype of the International Space Station Crew Return Vehicle.

For this sample we have also considered four situations, where we have intentionally "missed" one, two, three or four constraints. Following the same idea described above, we have considered the given specification as the "old" specification (see here our input file) and we have added and removed some constraints. Just for testing purposes, we have added up to four new, meaningless, nodes in the graph (new1 to new4).

One clause missing

We have inserted a new node (new1) and these new clauses.

After running the algorithm (see here the transcript of the computer-user dialog), we get the following formula: 
Final formula:
{L0}:[0]:E_ICP_I50FC_SENSOR(i) -2 < [1]:S_ICP_I50FC_SENSOR(i) AND 
{L1}:[2]:E_FCP_I50FC(i) -1 < [3]:S_FCP_I50FC(i) AND 
{L2}:[4]:E_FCP_P50FC(i) -5 < [5]:S_FCP_P50FC(i) AND 
{L3}:[6]:E_FCP_O50FC(i) -1 < [7]:S_FCP_O50(i) AND 
{L4}:[8]:E_ICP_I50FC_CMDS(i) -1 < [9]:S_ICP_I50FC_CMDS(i) AND 
{L5}:[10]:E_ICP_I10FC_SENSOR(i) -2 < [11]:S_ICP_I10FC_SENSOR(i) AND 
{L6}:[12]:E_FCP_I10FC(i) -1 < [13]:S_FCP_I10FC(i) AND 
{L7}:[14]:E_FCP_P10FC(i) -40 < [15]:S_FCP_P10FC(i) AND 
{L8}:[16]:E_FCP_O10FC(i) -1 < [17]:S_FCP_O10FC(i) AND 
{L9}:[18]:E_ICP_I10FC_CMDS(i) -1 < [19]:S_ICP_I10FC_CMDS(i) AND 
{L10}:[20]:E_ICP_I50NFC_SENSOR(i) -5 < [21]:S_ICP_I50NFC_SENSOR(i) AND 
{L11}:[22]:E_FCP_I50NFC(i) -1 < [23]:S_FCP_I50NFC(i) AND 
{L12}:[24]:E_FCP_P50NFC(i) -2 < [25]:S_FCP_P50NFC(i) AND 
{L13}:[1]:S_ICP_I50FC_SENSOR(i) +0 < [0]:E_ICP_I50FC_SENSOR(i) AND 
{L14}:[3]:S_FCP_I50FC(i) +0 < [2]:E_FCP_I50FC(i) AND 
{L15}:[5]:S_FCP_P50FC(i) +0 < [4]:E_FCP_P50FC(i) AND 
{L16}:[26]:S_FCP_O50FC(i) +0 < [6]:E_FCP_O50FC(i) AND 
{L17}:[9]:S_ICP_I50FC_CMDS(i) +0 < [8]:E_ICP_I50FC_CMDS(i) AND 
{L18}:[11]:S_ICP_I10FC_SENSOR(i) +0 < [10]:E_ICP_I10FC_SENSOR(i) AND 
{L19}:[13]:S_FCP_I10FC(i) +0 < [12]:E_FCP_I10FC(i) AND 
{L20}:[15]:S_FCP_P10FC(i) +0 < [14]:E_FCP_P10FC(i) AND 
{L21}:[17]:S_FCP_O10FC(i) +0 < [16]:E_FCP_O10FC(i) AND 
{L22}:[19]:S_ICP_I10FC_CMDS(i) +0 < [18]:E_ICP_I10FC_CMDS(i) AND 
{L23}:[21]:S_ICP_I50NFC_SENSOR(i) +0 < [20]:E_ICP_I50NFC_SENSOR(i) AND 
{L24}:[23]:S_FCP_I50NFC(i) +0 < [22]:E_FCP_I50NFC(i) AND 
{L25}:[25]:S_FCP_P50NFC(i) +0 < [24]:E_FCP_P50NFC(i) AND 
{L26}:[0]:E_ICP_I50FC_SENSOR(i) +0 < [3]:S_FCP_I50FC(i) AND 
{L27}:[2]:E_FCP_I50FC(i) +0 < [5]:S_FCP_P50FC(i) AND 
{L28}:[4]:E_FCP_P50FC(i) +0 < [26]:S_FCP_O50FC(i) AND 
{L29}:[6]:E_FCP_O50FC(i) +0 < [27]:S_FCP_I50FC_CMDS(i) AND 
{L30}:[10]:E_ICP_I10FC_SENSOR(i) +0 < [13]:S_FCP_I10FC(i) AND 
{L31}:[12]:E_FCP_I10FC(i) +0 < [15]:S_FCP_P10FC(i) AND 
{L32}:[14]:E_FCP_P10FC(i) +0 < [17]:S_FCP_O10FC(i) AND 
{L33}:[16]:E_FCP_O10FC(i) +0 < [28]:S_FCP_I10FC_CMDS(i) AND 
{L34}:[20]:E_ICP_I50NFC_SENSOR(i) +0 < [23]:S_FCP_I50NFC(i) AND 
{L35}:[22]:E_FCP_I50NFC(i) +0 < [25]:S_FCP_P50NFC(i) AND 
{L36}:[3]:S_FCP_I50FC(i) -2 < [1]:S_ICP_I50FC_SENSOR(i) AND 
{L37}:[5]:S_FCP_P50FC(i) -1 < [3]:S_FCP_I50FC(i) AND 
{L38}:[26]:S_FCP_O50FC(i) -5 < [5]:S_FCP_P50FC(i) AND 
{L39}:[9]:S_ICP_I50FC_CMDS(i) -1 < [26]:S_FCP_O50FC(i) AND 
{L40}:[13]:S_FCP_I10FC(i) -2 < [11]:S_ICP_I10FC_SENSOR(i) AND 
{L41}:[15]:S_FCP_P10FC(i) -1 < [13]:S_FCP_I10FC(i) AND 
{L42}:[17]:S_FCP_O10FC(i) -40 < [15]:S_FCP_P10FC(i) AND 
{L43}:[19]:S_ICP_I10FC_CMDS(i) -1 < [17]:S_FCP_O10FC(i) AND 
{L44}:[23]:S_FCP_I50NFC(i) -2 < [21]:S_ICP_I50NFC_SENSOR(i) AND 
{L45}:[25]:S_FCP_P50NFC(i) -1 < [23]:S_FCP_I50NFC(i) AND 
{L46}:[1]:S_ICP_I50FC_SENSOR(i) +20 < [29]:S_ICP_I50FC_SENSOR(i+1) AND 
{L47}:[3]:S_FCP_I50FC(i) +20 < [30]:S_FCP_I50FC(i+1) AND 
{L48}:[5]:S_FCP_P50FC(i) +20 < [31]:S_FCP_P50FC(i+1) AND 
{L49}:[26]:S_FCP_O50FC(i) +20 < [32]:S_FCP_O50FC(i+1) AND 
{L50}:[9]:S_ICP_I50FC_CMDS(i) +20 < [33]:S_ICP_I50FC_CMDS(i+1) AND 
{L51}:[29]:S_ICP_I50FC_SENSOR(i+1) -20 < [1]:S_ICP_I50FC_SENSOR(i) AND 
{L52}:[30]:S_FCP_I50FC(i+1) -20 < [3]:S_FCP_I50FC(i) AND 
{L53}:[31]:S_FCP_P50FC(i+1) -20 < [5]:S_FCP_P50FC(i) AND 
{L54}:[32]:S_FCP_O50FC(i+1) -20 < [26]:S_FCP_O50FC(i) AND 
{L55}:[33]:S_ICP_I50FC_CMDS(i+1) -20 < [9]:S_ICP_I50FC_CMDS(i) AND 
{L56}:[11]:S_ICP_I10FC_SENSOR(i) +100 < [34]:S_ICP_I10FC_SENSOR(i+1) AND 
{L57}:[13]:S_FCP_I10FC(i) +100 < [35]:S_FCP_I10FC(i+1) AND 
{L58}:[15]:S_FCP_P10FC(i) +100 < [36]:S_FCP_P10FC(i+1) AND 
{L59}:[17]:S_FCP_O10FC(i) +100 < [37]:S_FCP_O10FC(i+1) AND 
{L60}:[19]:S_ICP_I10FC_CMDS(i) +100 < [38]:S_ICP_I10FC_CMDS(i+1) AND 
{L61}:[34]:S_ICP_I10FC_SENSOR(i+1) -100 < [11]:S_ICP_I10FC_SENSOR(i) AND 
{L62}:[35]:S_FCP_I10FC(i+1) -100 < [13]:S_FCP_I10FC(i) AND 
{L63}:[36]:S_FCP_P10FC(i+1) -100 < [15]:S_FCP_P10FC(i) AND 
{L64}:[37]:S_FCP_O10FC(i+1) -100 < [17]:S_FCP_O10FC(i) AND 
{L65}:[38]:S_ICP_I10FC_CMDS(i+1) -100 < [19]:S_ICP_I10FC_CMDS(i) AND 
{L66}:[21]:S_ICP_I50NFC_SENSOR(i) +20 < [39]:S_ICP_I50NFC_SENSOR(i+1) AND 
{L67}:[23]:S_FCP_I50NFC(i) +20 < [40]:S_FCP_I50NFC(i+1) AND 
{L68}:[25]:S_FCP_P50NFC(i) +20 < [41]:S_FCP_P50NFC(i+1) AND 
{L69}:[39]:S_ICP_I50NFC_SENSOR(i+1) -20 < [21]:S_ICP_I50NFC_SENSOR(i) AND 
{L70}:[40]:S_FCP_I50NFC(i+1) -20 < [23]:S_FCP_I50NFC(i) AND 
{L71}:[41]:S_FCP_P50NFC(i+1) -20 < [25]:S_FCP_P50NFC(i) AND 
{L72}:[2]:E_FCP_I50FC(i) +0 < [13]:S_FCP_I10FC(i) AND 
{L73}:[2]:E_FCP_I50FC(i) +0 < [23]:S_FCP_I50NFC(i) AND 
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) AND 
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) AND 
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) AND 
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) AND 
{L76}:[46]:S_ICP_I50FC_SENSOR(x) -4 < [47]:new1(x) OR {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) AND  
NOT {L0}:[0]:E_ICP_I50FC_SENSOR(i) -2 < [1]:S_ICP_I50FC_SENSOR(i) OR 
  NOT {L46}:[1]:S_ICP_I50FC_SENSOR(i) +20 < [29]:S_ICP_I50FC_SENSOR(i+1) OR 
  NOT {L76}:[46]:S_ICP_I50FC_SENSOR(x) -4 < [47]:new1(x) OR NOT {L77}:[47]:new1(x) -13 < [0]:E_ICP_I50FC_SENSOR(i) AND 
{L77}:[47]:new1(x) -13 < [0]:E_ICP_I50FC_SENSOR(i)

Determinant:0.0
As you can see, one new unit clause has been added (denoted {L77} in our example) as well as a negative clause, correspondig to the new negative cycle in the graph, involving the newly added edge. The software has correctly checked, identified and applied the substitutions necessary according to the parameters of the functional symbols that take part in the shown cycles.

Running time: 4.719s
Efficiency: 0.3
See here the log file.

Two clauses missing

We have inserted two new nodes (new1 and new2) and these new clauses.

After running the algorithm (see here the transcript of the computer-user dialog), we get the following formula: 
Final formula:
{L0}:[0]:E_ICP_I50FC_SENSOR(i) -2 < [1]:S_ICP_I50FC_SENSOR(i) AND 
{L1}:[2]:E_FCP_I50FC(i) -1 < [3]:S_FCP_I50FC(i) AND 
{L2}:[4]:E_FCP_P50FC(i) -5 < [5]:S_FCP_P50FC(i) AND 
{L3}:[6]:E_FCP_O50FC(i) -1 < [7]:S_FCP_O50(i) AND 
{L4}:[8]:E_ICP_I50FC_CMDS(i) -1 < [9]:S_ICP_I50FC_CMDS(i) AND 
{L5}:[10]:E_ICP_I10FC_SENSOR(i) -2 < [11]:S_ICP_I10FC_SENSOR(i) AND 
{L6}:[12]:E_FCP_I10FC(i) -1 < [13]:S_FCP_I10FC(i) AND 
{L7}:[14]:E_FCP_P10FC(i) -40 < [15]:S_FCP_P10FC(i) AND 
{L8}:[16]:E_FCP_O10FC(i) -1 < [17]:S_FCP_O10FC(i) AND 
{L9}:[18]:E_ICP_I10FC_CMDS(i) -1 < [19]:S_ICP_I10FC_CMDS(i) AND 
{L10}:[20]:E_ICP_I50NFC_SENSOR(i) -5 < [21]:S_ICP_I50NFC_SENSOR(i) AND 
{L11}:[22]:E_FCP_I50NFC(i) -1 < [23]:S_FCP_I50NFC(i) AND 
{L12}:[24]:E_FCP_P50NFC(i) -2 < [25]:S_FCP_P50NFC(i) AND 
{L13}:[1]:S_ICP_I50FC_SENSOR(i) +0 < [0]:E_ICP_I50FC_SENSOR(i) AND 
{L14}:[3]:S_FCP_I50FC(i) +0 < [2]:E_FCP_I50FC(i) AND 
{L15}:[5]:S_FCP_P50FC(i) +0 < [4]:E_FCP_P50FC(i) AND 
{L16}:[26]:S_FCP_O50FC(i) +0 < [6]:E_FCP_O50FC(i) AND 
{L17}:[9]:S_ICP_I50FC_CMDS(i) +0 < [8]:E_ICP_I50FC_CMDS(i) AND 
{L18}:[11]:S_ICP_I10FC_SENSOR(i) +0 < [10]:E_ICP_I10FC_SENSOR(i) AND 
{L19}:[13]:S_FCP_I10FC(i) +0 < [12]:E_FCP_I10FC(i) AND 
{L20}:[15]:S_FCP_P10FC(i) +0 < [14]:E_FCP_P10FC(i) AND 
{L21}:[17]:S_FCP_O10FC(i) +0 < [16]:E_FCP_O10FC(i) AND 
{L22}:[19]:S_ICP_I10FC_CMDS(i) +0 < [18]:E_ICP_I10FC_CMDS(i) AND 
{L23}:[21]:S_ICP_I50NFC_SENSOR(i) +0 < [20]:E_ICP_I50NFC_SENSOR(i) AND 
{L24}:[23]:S_FCP_I50NFC(i) +0 < [22]:E_FCP_I50NFC(i) AND 
{L25}:[25]:S_FCP_P50NFC(i) +0 < [24]:E_FCP_P50NFC(i) AND 
{L26}:[0]:E_ICP_I50FC_SENSOR(i) +0 < [3]:S_FCP_I50FC(i) AND 
{L27}:[2]:E_FCP_I50FC(i) +0 < [5]:S_FCP_P50FC(i) AND 
{L28}:[4]:E_FCP_P50FC(i) +0 < [26]:S_FCP_O50FC(i) AND 
{L29}:[6]:E_FCP_O50FC(i) +0 < [27]:S_FCP_I50FC_CMDS(i) AND 
{L30}:[10]:E_ICP_I10FC_SENSOR(i) +0 < [13]:S_FCP_I10FC(i) AND 
{L31}:[12]:E_FCP_I10FC(i) +0 < [15]:S_FCP_P10FC(i) AND 
{L32}:[14]:E_FCP_P10FC(i) +0 < [17]:S_FCP_O10FC(i) AND 
{L33}:[16]:E_FCP_O10FC(i) +0 < [28]:S_FCP_I10FC_CMDS(i) AND 
{L34}:[20]:E_ICP_I50NFC_SENSOR(i) +0 < [23]:S_FCP_I50NFC(i) AND 
{L35}:[22]:E_FCP_I50NFC(i) +0 < [25]:S_FCP_P50NFC(i) AND 
{L36}:[3]:S_FCP_I50FC(i) -2 < [1]:S_ICP_I50FC_SENSOR(i) AND 
{L37}:[5]:S_FCP_P50FC(i) -1 < [3]:S_FCP_I50FC(i) AND 
{L38}:[26]:S_FCP_O50FC(i) -5 < [5]:S_FCP_P50FC(i) AND 
{L39}:[9]:S_ICP_I50FC_CMDS(i) -1 < [26]:S_FCP_O50FC(i) AND 
{L40}:[13]:S_FCP_I10FC(i) -2 < [11]:S_ICP_I10FC_SENSOR(i) AND 
{L41}:[15]:S_FCP_P10FC(i) -1 < [13]:S_FCP_I10FC(i) AND 
{L42}:[17]:S_FCP_O10FC(i) -40 < [15]:S_FCP_P10FC(i) AND 
{L43}:[19]:S_ICP_I10FC_CMDS(i) -1 < [17]:S_FCP_O10FC(i) AND 
{L44}:[23]:S_FCP_I50NFC(i) -2 < [21]:S_ICP_I50NFC_SENSOR(i) AND 
{L45}:[25]:S_FCP_P50NFC(i) -1 < [23]:S_FCP_I50NFC(i) AND 
{L46}:[1]:S_ICP_I50FC_SENSOR(i) +20 < [29]:S_ICP_I50FC_SENSOR(i+1) AND 
{L47}:[3]:S_FCP_I50FC(i) +20 < [30]:S_FCP_I50FC(i+1) AND 
{L48}:[5]:S_FCP_P50FC(i) +20 < [31]:S_FCP_P50FC(i+1) AND 
{L49}:[26]:S_FCP_O50FC(i) +20 < [32]:S_FCP_O50FC(i+1) AND 
{L50}:[9]:S_ICP_I50FC_CMDS(i) +20 < [33]:S_ICP_I50FC_CMDS(i+1) AND 
{L51}:[29]:S_ICP_I50FC_SENSOR(i+1) -20 < [1]:S_ICP_I50FC_SENSOR(i) AND 
{L52}:[30]:S_FCP_I50FC(i+1) -20 < [3]:S_FCP_I50FC(i) AND 
{L53}:[31]:S_FCP_P50FC(i+1) -20 < [5]:S_FCP_P50FC(i) AND 
{L54}:[32]:S_FCP_O50FC(i+1) -20 < [26]:S_FCP_O50FC(i) AND 
{L55}:[33]:S_ICP_I50FC_CMDS(i+1) -20 < [9]:S_ICP_I50FC_CMDS(i) AND 
{L56}:[11]:S_ICP_I10FC_SENSOR(i) +100 < [34]:S_ICP_I10FC_SENSOR(i+1) AND 
{L57}:[13]:S_FCP_I10FC(i) +100 < [35]:S_FCP_I10FC(i+1) AND 
{L58}:[15]:S_FCP_P10FC(i) +100 < [36]:S_FCP_P10FC(i+1) AND 
{L59}:[17]:S_FCP_O10FC(i) +100 < [37]:S_FCP_O10FC(i+1) AND 
{L60}:[19]:S_ICP_I10FC_CMDS(i) +100 < [38]:S_ICP_I10FC_CMDS(i+1) AND 
{L61}:[34]:S_ICP_I10FC_SENSOR(i+1) -100 < [11]:S_ICP_I10FC_SENSOR(i) AND 
{L62}:[35]:S_FCP_I10FC(i+1) -100 < [13]:S_FCP_I10FC(i) AND 
{L63}:[36]:S_FCP_P10FC(i+1) -100 < [15]:S_FCP_P10FC(i) AND 
{L64}:[37]:S_FCP_O10FC(i+1) -100 < [17]:S_FCP_O10FC(i) AND 
{L65}:[38]:S_ICP_I10FC_CMDS(i+1) -100 < [19]:S_ICP_I10FC_CMDS(i) AND 
{L66}:[21]:S_ICP_I50NFC_SENSOR(i) +20 < [39]:S_ICP_I50NFC_SENSOR(i+1) AND 
{L67}:[23]:S_FCP_I50NFC(i) +20 < [40]:S_FCP_I50NFC(i+1) AND 
{L68}:[25]:S_FCP_P50NFC(i) +20 < [41]:S_FCP_P50NFC(i+1) AND 
{L69}:[39]:S_ICP_I50NFC_SENSOR(i+1) -20 < [21]:S_ICP_I50NFC_SENSOR(i) AND 
{L70}:[40]:S_FCP_I50NFC(i+1) -20 < [23]:S_FCP_I50NFC(i) AND 
{L71}:[41]:S_FCP_P50NFC(i+1) -20 < [25]:S_FCP_P50NFC(i) AND 
{L72}:[2]:E_FCP_I50FC(i) +0 < [13]:S_FCP_I10FC(i) AND 
{L73}:[2]:E_FCP_I50FC(i) +0 < [23]:S_FCP_I50NFC(i) AND 
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) AND 
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) AND 
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) AND 
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) AND 
{L76}:[46]:S_ICP_I10FC_SENSOR(x2) -6 < [47]:new2(x2) OR {L77}:[48]:S_ICP_I50FC_SENSOR(x1) -4 < [49]:new1(x1) OR
  {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) AND 
NOT {L5}:[10]:E_ICP_I10FC_SENSOR(i) -2 < [11]:S_ICP_I10FC_SENSOR(i) OR 
  NOT {L56}:[11]:S_ICP_I10FC_SENSOR(i) +100 < [34]:S_ICP_I10FC_SENSOR(i+1) OR 
  NOT {L76}:[46]:S_ICP_I10FC_SENSOR(x2) -6 < [47]:new2(x2) OR 
  NOT {L78}:[47]:new2(x2) -91 < [10]:E_ICP_I10FC_SENSOR(i) AND 
{L78}:[47]:new2(x2) -91 < [10]:E_ICP_I10FC_SENSOR(i) AND 
NOT {L26}:[0]:E_ICP_I50FC_SENSOR(i) +0 < [3]:S_FCP_I50FC(i) OR 
  NOT {L36}:[3]:S_FCP_I50FC(i) -2 < [1]:S_ICP_I50FC_SENSOR(i) OR 
  NOT {L77}:[48]:S_ICP_I50FC_SENSOR(x1) -4 < [49]:new1(x1) OR 
  NOT {L79}:[49]:new1(x1) +7 < [50]:E_ICP_I50FC_SENSOR(x1) AND 
{L79}:[49]:new1(x1) +7 < [50]:E_ICP_I50FC_SENSOR(x1)

Determinant:0.0
As you can see, two new unit clauses have been added (denoted {L78} and {L79} in our example) as well as two negative clauses, correspondig to the two new negative cycles in the graph, involving the newly added edges. The software has correctly checked, identified and applied the substitutions necessary according to the parameters of the functional symbols that take part in the shown cycles.

Running time: 7.098s
Efficiency: 0.46
See here the log file.

Three clauses missing

We have inserted thre new nodes (new2, new and new3) and these new clauses.

After running the algorithm (see here the transcript of the computer-user dialog), we get the following formula: 
Final formula:
{L0}:[0]:E_ICP_I50FC_SENSOR(i) -2 < [1]:S_ICP_I50FC_SENSOR(i) AND 
{L1}:[2]:E_FCP_I50FC(i) -1 < [3]:S_FCP_I50FC(i) AND 
{L2}:[4]:E_FCP_P50FC(i) -5 < [5]:S_FCP_P50FC(i) AND 
{L3}:[6]:E_FCP_O50FC(i) -1 < [7]:S_FCP_O50(i) AND 
{L4}:[8]:E_ICP_I50FC_CMDS(i) -1 < [9]:S_ICP_I50FC_CMDS(i) AND 
{L5}:[10]:E_ICP_I10FC_SENSOR(i) -2 < [11]:S_ICP_I10FC_SENSOR(i) AND 
{L6}:[12]:E_FCP_I10FC(i) -1 < [13]:S_FCP_I10FC(i) AND 
{L7}:[14]:E_FCP_P10FC(i) -40 < [15]:S_FCP_P10FC(i) AND 
{L8}:[16]:E_FCP_O10FC(i) -1 < [17]:S_FCP_O10FC(i) AND 
{L9}:[18]:E_ICP_I10FC_CMDS(i) -1 < [19]:S_ICP_I10FC_CMDS(i) AND 
{L10}:[20]:E_ICP_I50NFC_SENSOR(i) -5 < [21]:S_ICP_I50NFC_SENSOR(i) AND 
{L11}:[22]:E_FCP_I50NFC(i) -1 < [23]:S_FCP_I50NFC(i) AND 
{L12}:[24]:E_FCP_P50NFC(i) -2 < [25]:S_FCP_P50NFC(i) AND 
{L13}:[1]:S_ICP_I50FC_SENSOR(i) +0 < [0]:E_ICP_I50FC_SENSOR(i) AND 
{L14}:[3]:S_FCP_I50FC(i) +0 < [2]:E_FCP_I50FC(i) AND 
{L15}:[5]:S_FCP_P50FC(i) +0 < [4]:E_FCP_P50FC(i) AND 
{L16}:[26]:S_FCP_O50FC(i) +0 < [6]:E_FCP_O50FC(i) AND 
{L17}:[9]:S_ICP_I50FC_CMDS(i) +0 < [8]:E_ICP_I50FC_CMDS(i) AND 
{L18}:[11]:S_ICP_I10FC_SENSOR(i) +0 < [10]:E_ICP_I10FC_SENSOR(i) AND 
{L19}:[13]:S_FCP_I10FC(i) +0 < [12]:E_FCP_I10FC(i) AND 
{L20}:[15]:S_FCP_P10FC(i) +0 < [14]:E_FCP_P10FC(i) AND 
{L21}:[17]:S_FCP_O10FC(i) +0 < [16]:E_FCP_O10FC(i) AND 
{L22}:[19]:S_ICP_I10FC_CMDS(i) +0 < [18]:E_ICP_I10FC_CMDS(i) AND 
{L23}:[21]:S_ICP_I50NFC_SENSOR(i) +0 < [20]:E_ICP_I50NFC_SENSOR(i) AND 
{L24}:[23]:S_FCP_I50NFC(i) +0 < [22]:E_FCP_I50NFC(i) AND 
{L25}:[25]:S_FCP_P50NFC(i) +0 < [24]:E_FCP_P50NFC(i) AND 
{L26}:[0]:E_ICP_I50FC_SENSOR(i) +0 < [3]:S_FCP_I50FC(i) AND 
{L27}:[2]:E_FCP_I50FC(i) +0 < [5]:S_FCP_P50FC(i) AND 
{L28}:[4]:E_FCP_P50FC(i) +0 < [26]:S_FCP_O50FC(i) AND 
{L29}:[6]:E_FCP_O50FC(i) +0 < [27]:S_FCP_I50FC_CMDS(i) AND 
{L30}:[10]:E_ICP_I10FC_SENSOR(i) +0 < [13]:S_FCP_I10FC(i) AND 
{L31}:[12]:E_FCP_I10FC(i) +0 < [15]:S_FCP_P10FC(i) AND 
{L32}:[14]:E_FCP_P10FC(i) +0 < [17]:S_FCP_O10FC(i) AND 
{L33}:[16]:E_FCP_O10FC(i) +0 < [28]:S_FCP_I10FC_CMDS(i) AND 
{L34}:[20]:E_ICP_I50NFC_SENSOR(i) +0 < [23]:S_FCP_I50NFC(i) AND 
{L35}:[22]:E_FCP_I50NFC(i) +0 < [25]:S_FCP_P50NFC(i) AND 
{L36}:[3]:S_FCP_I50FC(i) -2 < [1]:S_ICP_I50FC_SENSOR(i) AND 
{L37}:[5]:S_FCP_P50FC(i) -1 < [3]:S_FCP_I50FC(i) AND 
{L38}:[26]:S_FCP_O50FC(i) -5 < [5]:S_FCP_P50FC(i) AND 
{L39}:[9]:S_ICP_I50FC_CMDS(i) -1 < [26]:S_FCP_O50FC(i) AND 
{L40}:[13]:S_FCP_I10FC(i) -2 < [11]:S_ICP_I10FC_SENSOR(i) AND 
{L41}:[15]:S_FCP_P10FC(i) -1 < [13]:S_FCP_I10FC(i) AND 
{L42}:[17]:S_FCP_O10FC(i) -40 < [15]:S_FCP_P10FC(i) AND 
{L43}:[19]:S_ICP_I10FC_CMDS(i) -1 < [17]:S_FCP_O10FC(i) AND 
{L44}:[23]:S_FCP_I50NFC(i) -2 < [21]:S_ICP_I50NFC_SENSOR(i) AND 
{L45}:[25]:S_FCP_P50NFC(i) -1 < [23]:S_FCP_I50NFC(i) AND 
{L46}:[1]:S_ICP_I50FC_SENSOR(i) +20 < [29]:S_ICP_I50FC_SENSOR(i+1) AND 
{L47}:[3]:S_FCP_I50FC(i) +20 < [30]:S_FCP_I50FC(i+1) AND 
{L48}:[5]:S_FCP_P50FC(i) +20 < [31]:S_FCP_P50FC(i+1) AND 
{L49}:[26]:S_FCP_O50FC(i) +20 < [32]:S_FCP_O50FC(i+1) AND 
{L50}:[9]:S_ICP_I50FC_CMDS(i) +20 < [33]:S_ICP_I50FC_CMDS(i+1) AND 
{L51}:[29]:S_ICP_I50FC_SENSOR(i+1) -20 < [1]:S_ICP_I50FC_SENSOR(i) AND 
{L52}:[30]:S_FCP_I50FC(i+1) -20 < [3]:S_FCP_I50FC(i) AND 
{L53}:[31]:S_FCP_P50FC(i+1) -20 < [5]:S_FCP_P50FC(i) AND 
{L54}:[32]:S_FCP_O50FC(i+1) -20 < [26]:S_FCP_O50FC(i) AND 
{L55}:[33]:S_ICP_I50FC_CMDS(i+1) -20 < [9]:S_ICP_I50FC_CMDS(i) AND 
{L56}:[11]:S_ICP_I10FC_SENSOR(i) +100 < [34]:S_ICP_I10FC_SENSOR(i+1) AND 
{L57}:[13]:S_FCP_I10FC(i) +100 < [35]:S_FCP_I10FC(i+1) AND 
{L58}:[15]:S_FCP_P10FC(i) +100 < [36]:S_FCP_P10FC(i+1) AND 
{L59}:[17]:S_FCP_O10FC(i) +100 < [37]:S_FCP_O10FC(i+1) AND 
{L60}:[19]:S_ICP_I10FC_CMDS(i) +100 < [38]:S_ICP_I10FC_CMDS(i+1) AND 
{L61}:[34]:S_ICP_I10FC_SENSOR(i+1) -100 < [11]:S_ICP_I10FC_SENSOR(i) AND 
{L62}:[35]:S_FCP_I10FC(i+1) -100 < [13]:S_FCP_I10FC(i) AND 
{L63}:[36]:S_FCP_P10FC(i+1) -100 < [15]:S_FCP_P10FC(i) AND 
{L64}:[37]:S_FCP_O10FC(i+1) -100 < [17]:S_FCP_O10FC(i) AND 
{L65}:[38]:S_ICP_I10FC_CMDS(i+1) -100 < [19]:S_ICP_I10FC_CMDS(i) AND 
{L66}:[21]:S_ICP_I50NFC_SENSOR(i) +20 < [39]:S_ICP_I50NFC_SENSOR(i+1) AND 
{L67}:[23]:S_FCP_I50NFC(i) +20 < [40]:S_FCP_I50NFC(i+1) AND 
{L68}:[25]:S_FCP_P50NFC(i) +20 < [41]:S_FCP_P50NFC(i+1) AND 
{L69}:[39]:S_ICP_I50NFC_SENSOR(i+1) -20 < [21]:S_ICP_I50NFC_SENSOR(i) AND 
{L70}:[40]:S_FCP_I50NFC(i+1) -20 < [23]:S_FCP_I50NFC(i) AND 
{L71}:[41]:S_FCP_P50NFC(i+1) -20 < [25]:S_FCP_P50NFC(i) AND 
{L72}:[2]:E_FCP_I50FC(i) +0 < [13]:S_FCP_I10FC(i) AND 
{L73}:[2]:E_FCP_I50FC(i) +0 < [23]:S_FCP_I50NFC(i) AND 
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) AND 
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) AND 
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) AND 
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) AND 
{L76}:[46]:S_ICP_I10FC_SENSOR(x3) -8 < [47]:new3(x3) OR {L77}:[48]:S_ICP_I10FC_SENSOR(x2) -6 < [49]:new2(x2) OR
  {L78}:[50]:S_ICP_I50FC_SENSOR(x1) -4 < [51]:new1(x1) OR 
  {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) AND 
NOT {L5}:[10]:E_ICP_I10FC_SENSOR(i) -2 < [11]:S_ICP_I10FC_SENSOR(i) OR 
  NOT {L56}:[11]:S_ICP_I10FC_SENSOR(i) +100 < [34]:S_ICP_I10FC_SENSOR(i+1) OR 
  NOT {L76}:[46]:S_ICP_I10FC_SENSOR(x3) -8 < [47]:new3(x3) OR 
  NOT {L79}:[47]:new3(x3) -89 < [10]:E_ICP_I10FC_SENSOR(i) AND 
{L79}:[47]:new3(x3) -89 < [10]:E_ICP_I10FC_SENSOR(i) AND 
NOT {L5}:[10]:E_ICP_I10FC_SENSOR(i) -2 < [11]:S_ICP_I10FC_SENSOR(i) OR 
  NOT {L56}:[11]:S_ICP_I10FC_SENSOR(i) +100 < [34]:S_ICP_I10FC_SENSOR(i+1) OR 
  NOT {L77}:[48]:S_ICP_I10FC_SENSOR(x2) -6 < [49]:new2(x2) OR 
  NOT {L80}:[49]:new2(x2) -91 < [10]:E_ICP_I10FC_SENSOR(i) AND 
{L80}:[49]:new2(x2) -91 < [10]:E_ICP_I10FC_SENSOR(i) AND 
NOT {L0}:[0]:E_ICP_I50FC_SENSOR(i) -2 < [1]:S_ICP_I50FC_SENSOR(i) OR 
  NOT {L46}:[1]:S_ICP_I50FC_SENSOR(i) +20 < [29]:S_ICP_I50FC_SENSOR(i+1) OR 
  NOT {L78}:[50]:S_ICP_I50FC_SENSOR(x1) -4 < [51]:new1(x1) OR NOT {L81}:[51]:new1(x1) -13 < [0]:E_ICP_I50FC_SENSOR(i) AND 
{L81}:[51]:new1(x1) -13 < [0]:E_ICP_I50FC_SENSOR(i)

Determinant:0.0
As you can see, three new unit clauses have been added (denoted {L79}, {L80} and {L81} in our example) as well as three negative clauses, correspondig to three new negative cycles in the graph, involving the newly added edges. The software has correctly checked, identified and applied the substitutions necessary according to the parameters of the functional symbols that take part in the shown cycles.

Running time: 10.339s
Efficiency: 0.53
See here the log file.

Four clauses missing

We have inserted four new nodes (new1, new2, new3 and new4) and these new clauses.

After running the algorithm (see here the transcript of the computer-user dialog), we get the following formula: 
Final formula:
{L0}:[0]:E_ICP_I50FC_SENSOR(i) -2 < [1]:S_ICP_I50FC_SENSOR(i) AND 
{L1}:[2]:E_FCP_I50FC(i) -1 < [3]:S_FCP_I50FC(i) AND 
{L2}:[4]:E_FCP_P50FC(i) -5 < [5]:S_FCP_P50FC(i) AND 
{L3}:[6]:E_FCP_O50FC(i) -1 < [7]:S_FCP_O50(i) AND 
{L4}:[8]:E_ICP_I50FC_CMDS(i) -1 < [9]:S_ICP_I50FC_CMDS(i) AND 
{L5}:[10]:E_ICP_I10FC_SENSOR(i) -2 < [11]:S_ICP_I10FC_SENSOR(i) AND 
{L6}:[12]:E_FCP_I10FC(i) -1 < [13]:S_FCP_I10FC(i) AND 
{L7}:[14]:E_FCP_P10FC(i) -40 < [15]:S_FCP_P10FC(i) AND 
{L8}:[16]:E_FCP_O10FC(i) -1 < [17]:S_FCP_O10FC(i) AND 
{L9}:[18]:E_ICP_I10FC_CMDS(i) -1 < [19]:S_ICP_I10FC_CMDS(i) AND 
{L10}:[20]:E_ICP_I50NFC_SENSOR(i) -5 < [21]:S_ICP_I50NFC_SENSOR(i) AND 
{L11}:[22]:E_FCP_I50NFC(i) -1 < [23]:S_FCP_I50NFC(i) AND 
{L12}:[24]:E_FCP_P50NFC(i) -2 < [25]:S_FCP_P50NFC(i) AND 
{L13}:[1]:S_ICP_I50FC_SENSOR(i) +0 < [0]:E_ICP_I50FC_SENSOR(i) AND 
{L14}:[3]:S_FCP_I50FC(i) +0 < [2]:E_FCP_I50FC(i) AND 
{L15}:[5]:S_FCP_P50FC(i) +0 < [4]:E_FCP_P50FC(i) AND 
{L16}:[26]:S_FCP_O50FC(i) +0 < [6]:E_FCP_O50FC(i) AND 
{L17}:[9]:S_ICP_I50FC_CMDS(i) +0 < [8]:E_ICP_I50FC_CMDS(i) AND 
{L18}:[11]:S_ICP_I10FC_SENSOR(i) +0 < [10]:E_ICP_I10FC_SENSOR(i) AND 
{L19}:[13]:S_FCP_I10FC(i) +0 < [12]:E_FCP_I10FC(i) AND 
{L20}:[15]:S_FCP_P10FC(i) +0 < [14]:E_FCP_P10FC(i) AND 
{L21}:[17]:S_FCP_O10FC(i) +0 < [16]:E_FCP_O10FC(i) AND 
{L22}:[19]:S_ICP_I10FC_CMDS(i) +0 < [18]:E_ICP_I10FC_CMDS(i) AND 
{L23}:[21]:S_ICP_I50NFC_SENSOR(i) +0 < [20]:E_ICP_I50NFC_SENSOR(i) AND 
{L24}:[23]:S_FCP_I50NFC(i) +0 < [22]:E_FCP_I50NFC(i) AND 
{L25}:[25]:S_FCP_P50NFC(i) +0 < [24]:E_FCP_P50NFC(i) AND 
{L26}:[0]:E_ICP_I50FC_SENSOR(i) +0 < [3]:S_FCP_I50FC(i) AND 
{L27}:[2]:E_FCP_I50FC(i) +0 < [5]:S_FCP_P50FC(i) AND 
{L28}:[4]:E_FCP_P50FC(i) +0 < [26]:S_FCP_O50FC(i) AND 
{L29}:[6]:E_FCP_O50FC(i) +0 < [27]:S_FCP_I50FC_CMDS(i) AND 
{L30}:[10]:E_ICP_I10FC_SENSOR(i) +0 < [13]:S_FCP_I10FC(i) AND 
{L31}:[12]:E_FCP_I10FC(i) +0 < [15]:S_FCP_P10FC(i) AND 
{L32}:[14]:E_FCP_P10FC(i) +0 < [17]:S_FCP_O10FC(i) AND 
{L33}:[16]:E_FCP_O10FC(i) +0 < [28]:S_FCP_I10FC_CMDS(i) AND 
{L34}:[20]:E_ICP_I50NFC_SENSOR(i) +0 < [23]:S_FCP_I50NFC(i) AND 
{L35}:[22]:E_FCP_I50NFC(i) +0 < [25]:S_FCP_P50NFC(i) AND 
{L36}:[3]:S_FCP_I50FC(i) -2 < [1]:S_ICP_I50FC_SENSOR(i) AND 
{L37}:[5]:S_FCP_P50FC(i) -1 < [3]:S_FCP_I50FC(i) AND 
{L38}:[26]:S_FCP_O50FC(i) -5 < [5]:S_FCP_P50FC(i) AND 
{L39}:[9]:S_ICP_I50FC_CMDS(i) -1 < [26]:S_FCP_O50FC(i) AND 
{L40}:[13]:S_FCP_I10FC(i) -2 < [11]:S_ICP_I10FC_SENSOR(i) AND 
{L41}:[15]:S_FCP_P10FC(i) -1 < [13]:S_FCP_I10FC(i) AND 
{L42}:[17]:S_FCP_O10FC(i) -40 < [15]:S_FCP_P10FC(i) AND 
{L43}:[19]:S_ICP_I10FC_CMDS(i) -1 < [17]:S_FCP_O10FC(i) AND 
{L44}:[23]:S_FCP_I50NFC(i) -2 < [21]:S_ICP_I50NFC_SENSOR(i) AND 
{L45}:[25]:S_FCP_P50NFC(i) -1 < [23]:S_FCP_I50NFC(i) AND 
{L46}:[1]:S_ICP_I50FC_SENSOR(i) +20 < [29]:S_ICP_I50FC_SENSOR(i+1) AND 
{L47}:[3]:S_FCP_I50FC(i) +20 < [30]:S_FCP_I50FC(i+1) AND 
{L48}:[5]:S_FCP_P50FC(i) +20 < [31]:S_FCP_P50FC(i+1) AND 
{L49}:[26]:S_FCP_O50FC(i) +20 < [32]:S_FCP_O50FC(i+1) AND 
{L50}:[9]:S_ICP_I50FC_CMDS(i) +20 < [33]:S_ICP_I50FC_CMDS(i+1) AND 
{L51}:[29]:S_ICP_I50FC_SENSOR(i+1) -20 < [1]:S_ICP_I50FC_SENSOR(i) AND 
{L52}:[30]:S_FCP_I50FC(i+1) -20 < [3]:S_FCP_I50FC(i) AND 
{L53}:[31]:S_FCP_P50FC(i+1) -20 < [5]:S_FCP_P50FC(i) AND 
{L54}:[32]:S_FCP_O50FC(i+1) -20 < [26]:S_FCP_O50FC(i) AND 
{L55}:[33]:S_ICP_I50FC_CMDS(i+1) -20 < [9]:S_ICP_I50FC_CMDS(i) AND 
{L56}:[11]:S_ICP_I10FC_SENSOR(i) +100 < [34]:S_ICP_I10FC_SENSOR(i+1) AND 
{L57}:[13]:S_FCP_I10FC(i) +100 < [35]:S_FCP_I10FC(i+1) AND 
{L58}:[15]:S_FCP_P10FC(i) +100 < [36]:S_FCP_P10FC(i+1) AND 
{L59}:[17]:S_FCP_O10FC(i) +100 < [37]:S_FCP_O10FC(i+1) AND 
{L60}:[19]:S_ICP_I10FC_CMDS(i) +100 < [38]:S_ICP_I10FC_CMDS(i+1) AND 
{L61}:[34]:S_ICP_I10FC_SENSOR(i+1) -100 < [11]:S_ICP_I10FC_SENSOR(i) AND 
{L62}:[35]:S_FCP_I10FC(i+1) -100 < [13]:S_FCP_I10FC(i) AND 
{L63}:[36]:S_FCP_P10FC(i+1) -100 < [15]:S_FCP_P10FC(i) AND 
{L64}:[37]:S_FCP_O10FC(i+1) -100 < [17]:S_FCP_O10FC(i) AND 
{L65}:[38]:S_ICP_I10FC_CMDS(i+1) -100 < [19]:S_ICP_I10FC_CMDS(i) AND 
{L66}:[21]:S_ICP_I50NFC_SENSOR(i) +20 < [39]:S_ICP_I50NFC_SENSOR(i+1) AND 
{L67}:[23]:S_FCP_I50NFC(i) +20 < [40]:S_FCP_I50NFC(i+1) AND 
{L68}:[25]:S_FCP_P50NFC(i) +20 < [41]:S_FCP_P50NFC(i+1) AND 
{L69}:[39]:S_ICP_I50NFC_SENSOR(i+1) -20 < [21]:S_ICP_I50NFC_SENSOR(i) AND 
{L70}:[40]:S_FCP_I50NFC(i+1) -20 < [23]:S_FCP_I50NFC(i) AND 
{L71}:[41]:S_FCP_P50NFC(i+1) -20 < [25]:S_FCP_P50NFC(i) AND 
{L72}:[2]:E_FCP_I50FC(i) +0 < [13]:S_FCP_I10FC(i) AND 
{L73}:[2]:E_FCP_I50FC(i) +0 < [23]:S_FCP_I50NFC(i) AND 
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) AND 
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) AND 
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) AND 
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) AND 
{L76}:[46]:S_ICP_I50FC_SENSOR(x4) -10 < [47]:new4(x4) OR {L77}:[48]:S_ICP_I10FC_SENSOR(x3) -8 < [49]:new3(x3) OR
  {L78}:[50]:S_ICP_I10FC_SENSOR(x2) -6 < [51]:new2(x2) OR {L79}:[52]:S_ICP_I50FC_SENSOR(x1) -4 < [53]:new1(x1) OR
  {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) AND 
NOT {L0}:[0]:E_ICP_I50FC_SENSOR(i) -2 < [1]:S_ICP_I50FC_SENSOR(i) OR 
  NOT {L46}:[1]:S_ICP_I50FC_SENSOR(i) +20 < [29]:S_ICP_I50FC_SENSOR(i+1) OR 
  NOT {L76}:[46]:S_ICP_I50FC_SENSOR(x4) -10 < [47]:new4(x4) OR NOT {L80}:[47]:new4(x4) -7 < [0]:E_ICP_I50FC_SENSOR(i) AND 
{L80}:[47]:new4(x4) -7 < [0]:E_ICP_I50FC_SENSOR(i) AND 
NOT {L5}:[10]:E_ICP_I10FC_SENSOR(i) -2 < [11]:S_ICP_I10FC_SENSOR(i) OR 
  NOT {L56}:[11]:S_ICP_I10FC_SENSOR(i) +100 < [34]:S_ICP_I10FC_SENSOR(i+1) OR 
  NOT {L77}:[48]:S_ICP_I10FC_SENSOR(x3) -8 < [49]:new3(x3) OR 
  NOT {L81}:[49]:new3(x3) -89 < [10]:E_ICP_I10FC_SENSOR(i) AND 
{L81}:[49]:new3(x3) -89 < [10]:E_ICP_I10FC_SENSOR(i) AND 
NOT {L5}:[10]:E_ICP_I10FC_SENSOR(i) -2 < [11]:S_ICP_I10FC_SENSOR(i) OR 
NOT {L56}:[11]:S_ICP_I10FC_SENSOR(i) +100 < [34]:S_ICP_I10FC_SENSOR(i+1) OR 
NOT {L78}:[50]:S_ICP_I10FC_SENSOR(x2) -6 < [51]:new2(x2) OR NOT {L82}:[51]:new2(x2) -91 < [10]:E_ICP_I10FC_SENSOR(i) AND 
{L82}:[51]:new2(x2) -91 < [10]:E_ICP_I10FC_SENSOR(i) AND 
NOT {L0}:[0]:E_ICP_I50FC_SENSOR(i) -2 < [1]:S_ICP_I50FC_SENSOR(i) OR 
NOT {L46}:[1]:S_ICP_I50FC_SENSOR(i) +20 < [29]:S_ICP_I50FC_SENSOR(i+1) OR 
NOT {L79}:[52]:S_ICP_I50FC_SENSOR(x1) -4 < [53]:new1(x1) OR NOT {L83}:[53]:new1(x1) -13 < [0]:E_ICP_I50FC_SENSOR(i) AND 
{L83}:[53]:new1(x1) -13 < [0]:E_ICP_I50FC_SENSOR(i)

Determinant:0.0
As you can see, four new unit clauses has been added (denoted {L80}, {L81}, {L82} and {L83} in our example) as well as four negative clauses, correspondig to four new negative cycles in the graph, involving the newly added edges. The software has correctly checked, identified and applied the substitutions necessary according to the parameters of the functional symbols that take part in the shown cycles.

Running time: 13.217s
Efficiency: 0.5
See here the log file.

Description of the Automatic Debugging for Real-Time Logic

The Automatic Debugging for path Real Time Logic Tool (ADRTL v1.0) is implemented in Java.

The class files can be downloaded freely from here (Copyright of its respective owners).

All tests have been conducted on a 1.7Mobile Pentium, 768MB RAM, running on Linux (Fedora Core 3) and using Java SDK1.5.

 

 

 

***