TLSF allows identifiers with primes, but prime means "next" in Slugs output

[johnyf]

The TLSF format allows variable names that contain the character ', for example:

INFO {
  TITLE: "simple"
  DESCRIPTION: "example"
  SEMANTICS:   Mealy
  TARGET:      Mealy
}

MAIN {
  OUTPUTS { c'; }
  GUARANTEES { G X c'; }
}

But syfco --mode fully -f slugs primed_identifiers.tlsf produces the invalid output:

[INPUT]

[OUTPUT]
c'

[SYS_TRANS]
c''

However the prime is interpreted (character in variable name, or next operator), the above does not correspond to the input.

Moreover, the prime is used as the next operator in several tools (gr1c, slugs, widely used logics in the literature). The possible solutions appear to be:

1. exclude primes from characters that can be in a TLSF identifier, or
2. just not use primes in the benchmarks of the competition:
   prone to errors in wider use or if forgotten
3. automatically replace the primes within identifier names with syfco:
   changes variable names used in TLSF and output, which makes tracking things more difficult).
4. translate primes only as X in the output:
   some tools (like gr1c) don't support X at all, and others (like omega and tulip support both ' and X for "next", so they would be confused.

Therefore, alternative No.1 seems preferable.

[johnyf]

It should also be noted that SlugsIn is a lower-level format where no temporal X can appear in a transition relation, but the ' in a variable is interpreted as the primed copy of that variable (primed variables are generated automatically).

[kleinreact]

Primes usually occur in function names to denote an updated or extended version of a function. This is why they are part of the identifier syntax at the moment.

However, I agree that it might be confusing if primes are used for input and output signals. We will disuss a possible restriction of the signal identifier symbols for the next version of TLSF.

For the current version, I would suggest to use both, the second and the third solution together. Hence, we first add an option that allows to change the prime symbol (similar to the 'delimiter' option), which is set to the prime symbol by default. Hence, as long as the option is not changed everything works as before. Furthermore, for formats causing problems, such as slugs and slugsin, an error is thrown unless the option is adapted to some conflict-free alternative.

Additionally, we try to take care that primes are not used for input and output signals during the competition to avoid conflicts for later changes and updates.

[johnyf]

Thanks for the explanation. Primes are quite widely used, in various temporal logics to denote the next values of variables, so users are likely to expect that meaning. If not used at all in SYNTCOMP, then the issue doesn't seem to have any other effect. If renaming is used, then the same comments apply as for #11, regarding variable names and syfco output.

[kleinreact]

You can now replace the symbols by using the -ps option and you have to replace them when using the slugs output.

Beside that, we also will take care that all benchmarks used for the competition are prime free.