lpsconfcheck related problem

[matifch]

The following two specifications give same LPS (seen using lpsxsim) but the first one has 1 summand confluent while the other has not.

Specification-1

act  a,c;

proc P1=a;
        P2=c;

init hide({a},
      allow({a,c},
            P1||P2
          )
         );

Specification-2

act  a,c;

proc P1=a.c+c.a;

init hide({a},
      allow({a,c},
            P1
          )
         );

[Valo13]

I can reproduce this:
With the following specification as test1.mcrl2:

act a,c;

proc P1 = a;
P2 = c;

init hide({a}, allow({a,c}, P1 || P2));

Executing mcrl22lps test1.mcrl2 test1.lps followed by lpsconfcheck test1.lps gives the output

summand   1 of 3 (condition = c): +:+Confluent with all summands.
1 of 1 tau summands were found to be confluent

With the following specification as test2.mcrl2:

act a,c;

proc P1 = a.c + c.a;

init hide({a}, allow({a,c}, P1));

Executing mcrl22lps test2.mcrl2 test2.lps followed by lpsconfcheck test2.lps gives the output

summand   2 of 3 (condition = c): ++Not confluent with summand 3.
0 of 1 tau summands were found to be confluent

However, the behaviour of both processes (that is the LTSs generated from them) is (are) identical.
This probably has to do with how the LPSs are structured and how lpsconfcheck uses these LPSs. The LPS test1.lps is

act  Terminate,a,c;

proc P(s1_P5,s2_P4: Pos) =
       (s1_P5 == 3) ->
         tau .
         P(s1_P5 = 2)
     + (s2_P4 == 3) ->
         c .
         P(s2_P4 = 2)
     + (s1_P5 == 2 && s2_P4 == 2) ->
         Terminate .
         P(s1_P5 = 1, s2_P4 = 1)
     + delta;

init P(3, 3);

and the LPS test2.lps is

act  Terminate,a,c;

proc P(s1_P3: Pos) =
       (s1_P3 == 2) ->
         Terminate .
         P(s1_P3 = 1)
     + sum e_P3: Bool.
         (if(e_P3, s1_P3 == 5, s1_P3 == 3)) ->
         tau .
         P(s1_P3 = if(e_P3, 2, 4))
     + sum e1_P3: Bool.
         (if(e1_P3, s1_P3 == 4, s1_P3 == 3)) ->
         c .
         P(s1_P3 = if(e1_P3, 2, 5))
     + delta;

init P(3);

[jgroote]

This is intended behaviour. The confluence checker only looks at the same summand to mimic a confluent summand.
If it would have to look at all other summands confluence checking would be too slow. The first confluence checker was made by me, and did not perform well. The second one was made by Jaco van de Pol, and used this trick.
So, it indeed behaves differently for a||b and a.b+b.a.

[tneele]

I agree with @Valo13's observations, but not completely with @jgroote's. The simplification made in lpsconfcheck that causes it to under-approximate in this case, is the avoidance of expressions with quantifier alternations. Namely, in this example, to create the diamond, sum variables e_P3 and e1_P3 have to take on different values in different interleavings. We compute the approximation forall d1,d2,e1,e2. f1(d1,e1) && f2(d2,e2) => f1(g2(d2,e2),e1) && f2(g1(d1,e1),e2) && g1(g2(d2,e2),e1) == g2(g1(d1,e1),e2) instead of the more powerful forall d1,d2,e1,e2. f1(d1,e1) && f2(d2,e2) => exists e1',e2'. f1(g2(d2,e2),e1') && f2(g1(d1,e1),e2') && g1(g2(d2,e2),e1') == g2(g1(d1,e1),e2'). The latter has been implemented in pbespor, and seems to work sometimes.

To come back to your report @matifch, this is indeed expected behaviour, as @jgroote mentioned. If you really need reduction in the second case, you may try your luck with pbespor, but it's a very experimental tool.

[Valo13]

Wouldn't it be better to change the output slightly? For test2.lps it says that it is not confluent, while in reality it is confluent but the tool did not manage to find this (as far as I understand). So instead of Not confluent with summand 3 I would rather see something like Could not find confluence with summand 3.

[tneele]

Wouldn't it be better to change the output slightly?

That is perhaps a good idea. However, I also want to add that it might be more fruitful to spend our time on replacing the current implementation of lpsconfcheck with the new implementation in confcheck.

[matifch]

Agreed to @tneele to have the new implementation.
Rephrasing @jgroote' s verdict, tau.c has a summand confluent but tau.c+tau has nothing like that.