Feature Request: Standard Library implementation of Char and String?

[gjveltink]

I am currently developing a larger specification for a real-life industrial production system, which we use in our education. One of the objectives of this specification is to incorporate the "Asset Administration Shell" standard for Industrie 4.0 components (IEC TR 62794 & IEC 62832 Digital Factory). This standard heavily relies on common representations of "strings".

To faithfully adhere to the standard, I had to introduce a custom sort "String" While this is technically possible, the implementation becomes quite cumbersome—particularly when it comes to representing digits within strings.

% -----------------------------------------------------------------------------------------------------------------------
%
% self-defined characters and strings
%

sort Char = struct
	a | b | c | d | e | f | g | h | i | j | k | l | m | n | o | p | q | r | s | t | u | v | w | x | y | z
	| A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z
        | _0 | _1 | _2 | _3 | _4 | _5 | _6 | _7 | _8 | _9 
;

sort String = List(Char);

% example usage
map mCRL2: String;
eqn mCRL2 = [m,C,R,L,_2];

Unfortunately, this scheme also eliminates the possibility of using single-character variables throughout the rest of the specification, which can be a nuisance as well.

Therefore, I would strongly advocate for the inclusion of Characters and Strings in the standard library of data types in a future version of mCRL2.
This addition would not only enhance the functionality of the language but also make it more appealing to my students.
In fact, I often encounter discussions during lectures where I have to justify the absence of these fundamental data types in mCRL2.

[mlaveaux]

Are the strings actually being operated on (operations such as contains, concatenated etc) or are they merely string literals used as e.g. identifiers? In the latter case I would imagine some structured sort containing all possible string literals as elements might be a slightly more readable approach. I can understand that a String sort could be useful, although perhaps modelling the specification faithfully might slow down model checking.

[gjveltink]

For my current primary use case, having just string literals would be sufficient.
In my view, this addition by itself could have a significant positive impact!

That said, I am concerned that my students might eventually expect string operations, as these are commonly available in other (programming) languages. To manage these expectations, it would be essential to clarify this distinction in the documentation.

[gjveltink]

I have given this issue some more thoughts yesterday.
A possible alternative approach could be to actually give standard representations for characters as a predefined data type (e.g. Char), like in programming languages, e.g. 'a', '3', '_'.
Then define Strings literally as 'List(Char)' but make sure the external representation of Strings is "just" syntactic sugar, e.g. "mCRL2" instead of ['m', 'C', 'R', 'L', '2'].
As far as I can judge it, this might even be the least intrusive way to implement this feature.
But hey, I am not the expert of course, maybe I am missing things.

[mlaveaux]

Currently we have decided not to change the language as it is, because there seem to be only minor benefits with the potential to cause all kinds of changes to the tool set. However, we will keep this issue as a long term issue to see if this can be integrated in case other changes to the language are also integrated that are currently being thought up by some of our PhD students.