Renaming an action

[matifch]

Can we write the renaming rule for the following process

P(lst:List(Nat)) = a(0) + a(maxList(lst));

where we want to rename a(maxList(lst)) to some action and maxList is a function to determine the maximum value in a list of natural numbers.

[tneele]

I don't think this is possible, since the documentation states that

All arguments of the action at the left hand side must either be closed terms or variables.

Perhaps @jgroote has a suggestion for a trick to work around this limitation.

[jgroote]

Hello Muhammad, Your example revealed a nasty bug, which we had to resolve first. This bug is still in the new release, but should be repaired in one of the upcoming nightly builds. You can use conditions in rename files (e.g. rename.ren): act a_max:Nat; var n:Nat; rename (n > 0) -> a(n) => a_max(0); This renames each action a(n) to a_max(0) (but this 0 can be any expression containing n), for instance a_max(n+n). As an illustration you could apply it to act a: Nat; map f:Nat -> Nat; c1,c2,c3: Bool; proc P=c1 -> a(0).P + c2 -> a(1).P + c3 -> a(f(0)).P; init P; Use mcrl22lps -n test.mcrl2 test.lps lpsactionrename -frename.ren test.lps -v testr.lps ; lpspp testr.lps So, in your case, you cannot rename an expression in which "maxList" occurs, because maxList(lst) can return 0. But if you know that "maxList" always returns a value larger than 0 it works. Hope this helps, Jan Friso

…

On 19 Jul 2020, at 21:23, Thomas Neele ***@***.***> wrote: I don't think this is possible, since the documentation states that All arguments of the action at the left hand side must either be closed terms or variables. Perhaps @jgroote has a suggestion for a trick to work around this limitation. — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub, or unsubscribe.

------------------------------------------------------------------------------------------------------------------------ Jan Friso Groote, Eindhoven University of Technology, Department of Mathematics and Computer Science, Metaforum room MF 6.079b, Groene Loper 5, 5612 AE Eindhoven. The Netherlands. +31-40-247 5003, secretary: +31-40-247 5145, J.F.Groote@tue.nl, www.win.tue.nl/~jfg, Skype: janfriso Home: Hoekstraat 56, 5674 NP Nederwetten, +31 40 2845414, +31 6 81922128