wrong CPF output for models with patterns

[jwaldmann]

how to reproduce: add numPatterns=2 (or whatever) in tc/MB.hs, then run on tpdb-8.0/TRS/Zantema_05/z27.xml, send to ceta, result:

REJECTED
termination proof not accepted
1: error below switch to dependency pairs
1.1: error below the reduction pair processor
 1.1.1: error below the split processor
  1.1.1.1: error when applying the semlab processor on the DP problem
   pairs:

   f#(0, 1, x1) -> f#(g(x1), g(x1), x1)
   weak pairs:

   f#(g(x1), x2, x3) ->= f#(x1, x2, x3)
   f#(x1, g(x2), x3) ->= f#(x1, x2, x3)
   rules:

   f(0, 1, x1) -> f(g(x1), g(x1), x1)
   f(g(x1), x2, x3) -> g(f(x1, x2, x3))
   f(x1, g(x2), x3) -> g(f(x1, x2, x3))
   f(x1, x2, g(x3)) -> g(f(x1, x2, x3))

   (minimal)
   problem during labeling:
   labeled rule f[[0, 0, 0]](g[[0]](x1), x2, x3) -> g[[0]](f[[0, 0, 0]](x1, x2, x3)) missing

the mode is dumped as

Model:
f# * * * |-> 0
f# * * * |-> 0

0  |-> 1

1  |-> 0

g 0 |-> 0
g 1 |-> 1

f * * 0 |-> 1
f * * * |-> 1

There is something wrong because f[0,0,0] is 1, so the g[0] in the error message should really be g[1]. This is shown correctly in the dump of the labelled system.

[jwaldmann]

(Rene says) there is something wrong in the CPF:

According to the CPF you used the interpretation

[f(x1, x2, x3)] = (if x3 = 0 then 1 else 0) + 1

with f(0,0,0) = (if 0 = 0 then 1 else 0) + 1 = 1 + 1 = 0

Then indeed f(0,0,0) is 0, so the g[0] in the error message is correct.

[jwaldmann]

Ah. The problem seems to be that case distictions (from patterns) are not exclusive, so we cannot sum the values from different branches.

[rene-thiemann]

CPF also specifies min and max-operators, perhaps these are more appropriate. all operators like +, , min, max, etc. have the semantics sem(x op y) = (x op y) mod carrier-size where op is executed on the naturals. So with two element carriers: sem(x max y) = x or y sem(x min y) = sem(x \ y) = x and y sem(x + y) = x excl.or y sem(x + 1) = negate x

[jwaldmann]

(The carrier can be larger.)

We should just translate the pattern match into a nest of if-then-elses, as a direct implementation of the pattern matching semantics.