lpsparunfold is of no use on lists

[jgroote]

Issue migrated from trac ticket # 1149

component: lpsparunfold | priority: minor

2013-03-14 10:17:31: @jkeiren created the issue

---

If we linearise the attached specification test.mcrl2 using

mcrl22lps -nf test.mcrl2 test.lps

and then try to remove the lists over Booleans using lpsparunfold, followed by rewriting, as follows

lpsparunfold -s"List(Bool)" -l -n1 -v test.lps | lpsrewr > test1.lps

we obtain the following LPS.

act  a,b: Bool;

proc P(S_pp: S1, S_pp1: Bool, S_pp2: List(Bool)) #        (#C_S1_(S_pp, [], S_pp1 |> S_pp2)= 2) ->
         b(head(C_S1_(S_pp, [], S_pp1 |> S_pp2))) .
         P(S_pp # Det_S1_(tail(C_S1_(S_pp, [], S_pp1 |> S_pp2))), S_pp1pi_S1_(tail(C_S1_(S_pp, [], S_pp1 |> S_pp2))), S_pp2 = pi_S1_1(tail(C_S1_(S_pp, [], S_pp1 |> S_pp2))))
     + (#C_S1_(S_pp, [], S_pp1 |> S_pp2) <= 1) ->
         a(true) .
         P(S_pp # c_1, S_pp1true, S_pp2 = C_S1_(S_pp, [], S_pp1 |> S_pp2))
     + delta;

init P(c_, pi_S1_([]), pi_S1_1([]));

Observe that pi_S1_([]) and pi_S1_1([]) cannot be rewritten further. It seems that the tool does not conclude that the list could only be simplified a limited number of times, whereas we might expect that it could.

Furthermore, the fact that we cannot reduce these projection functions to a constant value does not allow us to remove the parameter using constelm. One would especially expect that pi_S1_1([]) = [], such that it does reduce.

[jgroote]

2013-03-14 10:17:51: @jkeiren uploaded file test.mcrl2 (0.1 KiB)

[jgroote]

2014-09-03 14:12:11: [email protected] changed status from new to assigned

[jgroote]

2014-09-03 14:12:11: [email protected] changed owner from fstapper to jfg

[jgroote]

2014-09-03 21:33:08: @jgroote changed status from assigned to accepted

[jgroote]

2014-09-03 21:33:08: @jgroote changed type from defect to enhancement

[jgroote]

2014-09-03 21:33:08: @jgroote

[jgroote]

2014-09-03 21:33:08: @jgroote commented

---

Adding the suggested equations does not immediately lead lpsconstelm to remove the parameters. More needs to be done, probably adding the equation tail([])=[] or something similar.

It is obvious that more could be desired here, but what is being done is correct. Therefore I change this report from a defect to an enhancement. It may require a substantial study to figure out what the effective rewrite rules are that are required to resolve this.

The problem which is shown in this ticket plays a role in the formulation of the game of the goose. In that case it also turns out to be impossible (yet) to remove list parameters after expansion with lpsparunfold.

[jgroote]

2016-11-24 19:30:10: @wiegerw

[jgroote]

2017-05-27 18:55:17: @jgroote

[jgroote]

2017-05-27 18:55:17: @jgroote commented

---

Investigated this example once again and added the suggested rewrite rules in revision r14833, commit 758bd167d1e82e41c69668e99fc27a4e2e5f3c82. This simplified the process to which lpsparunfold was applied, but it is not enough to let lpsconstelm see that the list is not needed.

My impression is that at least uniform distribution of case functions of other functions is required, and furthermore, lpsconstelm must become much stronger.

I leave the example for further investigation, but expect that it will require substantial effort to make the tools so strong that lpsparunfold and lpsconstelm will work as suggested in this ticket.